1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Morgan Deters, Christopher L. Conway, Andrew Reynolds |
4 |
|
* |
5 |
|
* This file is part of the cvc5 project. |
6 |
|
* |
7 |
|
* Copyright (c) 2009-2021 by the authors listed in the file AUTHORS |
8 |
|
* in the top-level source directory and their institutional affiliations. |
9 |
|
* All rights reserved. See the file COPYING in the top-level source |
10 |
|
* directory for licensing information. |
11 |
|
* **************************************************************************** |
12 |
|
* |
13 |
|
* A builder for parsers. |
14 |
|
*/ |
15 |
|
|
16 |
|
#include "cvc5parser_public.h" |
17 |
|
|
18 |
|
#ifndef CVC5__PARSER__PARSER_BUILDER_H |
19 |
|
#define CVC5__PARSER__PARSER_BUILDER_H |
20 |
|
|
21 |
|
#include <string> |
22 |
|
|
23 |
|
#include "cvc5_export.h" |
24 |
|
#include "options/language.h" |
25 |
|
#include "parser/input.h" |
26 |
|
|
27 |
|
namespace cvc5 { |
28 |
|
|
29 |
|
namespace api { |
30 |
|
class Solver; |
31 |
|
} |
32 |
|
|
33 |
|
class Options; |
34 |
|
class SymbolManager; |
35 |
|
|
36 |
|
namespace parser { |
37 |
|
|
38 |
|
class Parser; |
39 |
|
|
40 |
|
/** |
41 |
|
* A builder for input language parsers. <code>build()</code> can be |
42 |
|
* called any number of times on an instance and will generate a fresh |
43 |
|
* parser each time. |
44 |
|
*/ |
45 |
12853 |
class CVC5_EXPORT ParserBuilder |
46 |
|
{ |
47 |
|
/** The input language */ |
48 |
|
std::string d_lang; |
49 |
|
|
50 |
|
/** The API Solver object. */ |
51 |
|
api::Solver* d_solver; |
52 |
|
|
53 |
|
/** The symbol manager */ |
54 |
|
SymbolManager* d_symman; |
55 |
|
|
56 |
|
/** Should semantic checks be enabled during parsing? */ |
57 |
|
bool d_checksEnabled; |
58 |
|
|
59 |
|
/** Should we parse in strict mode? */ |
60 |
|
bool d_strictMode; |
61 |
|
|
62 |
|
/** Should we allow include-file commands? */ |
63 |
|
bool d_canIncludeFile; |
64 |
|
|
65 |
|
/** Are we parsing only? */ |
66 |
|
bool d_parseOnly; |
67 |
|
|
68 |
|
/** Is the logic forced by the user? */ |
69 |
|
bool d_logicIsForced; |
70 |
|
|
71 |
|
/** The forced logic name */ |
72 |
|
std::string d_forcedLogic; |
73 |
|
|
74 |
|
/** Initialize this parser builder */ |
75 |
|
void init(api::Solver* solver, SymbolManager* sm); |
76 |
|
|
77 |
|
public: |
78 |
|
/** Create a parser builder using the given Solver and filename. */ |
79 |
|
ParserBuilder(api::Solver* solver, SymbolManager* sm, bool useOptions); |
80 |
|
|
81 |
|
/** Build the parser, using the current settings. */ |
82 |
|
Parser* build(); |
83 |
|
|
84 |
|
/** Should semantic checks be enabled in the parser? (Default: yes) */ |
85 |
|
ParserBuilder& withChecks(bool flag = true); |
86 |
|
|
87 |
|
/** |
88 |
|
* Set the input language to be used by the parser. |
89 |
|
* |
90 |
|
* (Default: LANG_AUTO) |
91 |
|
*/ |
92 |
|
ParserBuilder& withInputLanguage(const std::string& lang); |
93 |
|
|
94 |
|
/** |
95 |
|
* Are we only parsing, or doing something with the resulting |
96 |
|
* commands and expressions? This setting affects whether the |
97 |
|
* parser will raise certain errors about unimplemented features, |
98 |
|
* even if there isn't a parsing error, because the result of the |
99 |
|
* parse would otherwise be an incorrect parse tree and the error |
100 |
|
* would go undetected. This is specifically for circumstances |
101 |
|
* where the parser is ahead of the functionality present elsewhere |
102 |
|
* in cvc5 (such as quantifiers, subtypes, records, etc. in the CVC |
103 |
|
* language parser). |
104 |
|
*/ |
105 |
|
ParserBuilder& withParseOnly(bool flag = true); |
106 |
|
|
107 |
|
/** Derive settings from the solver's options. */ |
108 |
|
ParserBuilder& withOptions(); |
109 |
|
|
110 |
|
/** |
111 |
|
* Should the parser use strict mode? |
112 |
|
* |
113 |
|
* (Default: no) |
114 |
|
*/ |
115 |
|
ParserBuilder& withStrictMode(bool flag = true); |
116 |
|
|
117 |
|
/** |
118 |
|
* Should the include-file commands be enabled? |
119 |
|
* |
120 |
|
* (Default: yes) |
121 |
|
*/ |
122 |
|
ParserBuilder& withIncludeFile(bool flag = true); |
123 |
|
|
124 |
|
/** Set the parser to use the given logic string. */ |
125 |
|
ParserBuilder& withForcedLogic(const std::string& logic); |
126 |
|
}; /* class ParserBuilder */ |
127 |
|
|
128 |
|
} // namespace parser |
129 |
|
} // namespace cvc5 |
130 |
|
|
131 |
|
#endif /* CVC5__PARSER__PARSER_BUILDER_H */ |