Branch data Line data Source code
1 : : /******************************************************************************
2 : : * This file is part of the cvc5 project.
3 : : *
4 : : * Copyright (c) 2009-2026 by the authors listed in the file AUTHORS
5 : : * in the top-level source directory and their institutional affiliations.
6 : : * All rights reserved. See the file COPYING in the top-level source
7 : : * directory for licensing information.
8 : : * ****************************************************************************
9 : : *
10 : : * The smt2 command parser.
11 : : */
12 : :
13 : : #include "parser/smt2/smt2_cmd_parser.h"
14 : :
15 : : #include "base/check.h"
16 : : #include "base/output.h"
17 : : #include "parser/commands.h"
18 : :
19 : : namespace cvc5 {
20 : : namespace parser {
21 : :
22 : 24437 : Smt2CmdParser::Smt2CmdParser(Smt2Lexer& lex,
23 : : Smt2State& state,
24 : 24437 : Smt2TermParser& tparser)
25 : 24437 : : d_lex(lex), d_state(state), d_tparser(tparser)
26 : : {
27 : : // initialize the command tokens
28 : 24437 : d_table["assert"] = Token::ASSERT_TOK;
29 : 24437 : d_table["check-sat-assuming"] = Token::CHECK_SAT_ASSUMING_TOK;
30 : 24437 : d_table["check-sat"] = Token::CHECK_SAT_TOK;
31 : 24437 : d_table["declare-codatatypes"] = Token::DECLARE_CODATATYPES_TOK;
32 : 24437 : d_table["declare-codatatype"] = Token::DECLARE_CODATATYPE_TOK;
33 : 24437 : d_table["declare-const"] = Token::DECLARE_CONST_TOK;
34 : 24437 : d_table["declare-datatypes"] = Token::DECLARE_DATATYPES_TOK;
35 : 24437 : d_table["declare-datatype"] = Token::DECLARE_DATATYPE_TOK;
36 : 24437 : d_table["declare-fun"] = Token::DECLARE_FUN_TOK;
37 : 24437 : d_table["declare-sort"] = Token::DECLARE_SORT_TOK;
38 : 24437 : d_table["declare-sort-parameter"] = Token::DECLARE_SORT_PARAMETER_TOK;
39 : 24437 : d_table["define-const"] = Token::DEFINE_CONST_TOK;
40 : 24437 : d_table["define-funs-rec"] = Token::DEFINE_FUNS_REC_TOK;
41 : 24437 : d_table["define-fun-rec"] = Token::DEFINE_FUN_REC_TOK;
42 : 24437 : d_table["define-fun"] = Token::DEFINE_FUN_TOK;
43 : 24437 : d_table["define-sort"] = Token::DEFINE_SORT_TOK;
44 : 24437 : d_table["echo"] = Token::ECHO_TOK;
45 : 24437 : d_table["exit"] = Token::EXIT_TOK;
46 : 24437 : d_table["get-assertions"] = Token::GET_ASSERTIONS_TOK;
47 : 24437 : d_table["get-assignment"] = Token::GET_ASSIGNMENT_TOK;
48 : 24437 : d_table["get-info"] = Token::GET_INFO_TOK;
49 : 24437 : d_table["get-model"] = Token::GET_MODEL_TOK;
50 : 24437 : d_table["get-option"] = Token::GET_OPTION_TOK;
51 : 24437 : d_table["get-proof"] = Token::GET_PROOF_TOK;
52 : 24437 : d_table["get-timeout-core"] = Token::GET_TIMEOUT_CORE_TOK;
53 : 24437 : d_table["get-timeout-core-assuming"] = Token::GET_TIMEOUT_CORE_ASSUMING_TOK;
54 : 24437 : d_table["get-unsat-assumptions"] = Token::GET_UNSAT_ASSUMPTIONS_TOK;
55 : 24437 : d_table["get-unsat-core"] = Token::GET_UNSAT_CORE_TOK;
56 : 24437 : d_table["get-unsat-core-lemmas"] = Token::GET_UNSAT_CORE_LEMMAS_TOK;
57 : 24437 : d_table["get-value"] = Token::GET_VALUE_TOK;
58 : 24437 : d_table["get-model-domain-elements"] = Token::GET_MODEL_DOMAIN_ELEMENTS_TOK;
59 : 24437 : d_table["pop"] = Token::POP_TOK;
60 : 24437 : d_table["push"] = Token::PUSH_TOK;
61 : 24437 : d_table["reset-assertions"] = Token::RESET_ASSERTIONS_TOK;
62 : 24437 : d_table["reset"] = Token::RESET_TOK;
63 : 24437 : d_table["set-info"] = Token::SET_INFO_TOK;
64 : 24437 : d_table["set-logic"] = Token::SET_LOGIC_TOK;
65 : 24437 : d_table["set-option"] = Token::SET_OPTION_TOK;
66 [ + + ]: 24437 : if (!d_lex.isStrict())
67 : : {
68 : 24398 : d_table["block-model"] = Token::BLOCK_MODEL_TOK;
69 : 24398 : d_table["block-model-values"] = Token::BLOCK_MODEL_VALUES_TOK;
70 : 24398 : d_table["declare-heap"] = Token::DECLARE_HEAP_TOK;
71 : 24398 : d_table["declare-oracle-fun"] = Token::DECLARE_ORACLE_FUN_TOK;
72 : 24398 : d_table["declare-pool"] = Token::DECLARE_POOL_TOK;
73 : 24398 : d_table["find-synth"] = Token::FIND_SYNTH_TOK;
74 : 24398 : d_table["find-synth-next"] = Token::FIND_SYNTH_NEXT_TOK;
75 : 24398 : d_table["get-abduct-next"] = Token::GET_ABDUCT_NEXT_TOK;
76 : 24398 : d_table["get-abduct"] = Token::GET_ABDUCT_TOK;
77 : 24398 : d_table["get-difficulty"] = Token::GET_DIFFICULTY_TOK;
78 : 24398 : d_table["get-interpolant-next"] = Token::GET_INTERPOL_NEXT_TOK;
79 : 24398 : d_table["get-interpolant"] = Token::GET_INTERPOL_TOK;
80 : 24398 : d_table["get-learned-literals"] = Token::GET_LEARNED_LITERALS_TOK;
81 : 24398 : d_table["get-qe-disjunct"] = Token::GET_QE_DISJUNCT_TOK;
82 : 24398 : d_table["get-qe"] = Token::GET_QE_TOK;
83 : 24398 : d_table["include"] = Token::INCLUDE_TOK;
84 : 24398 : d_table["simplify"] = Token::SIMPLIFY_TOK;
85 : : }
86 [ + + ]: 24437 : if (d_lex.isSygus())
87 : : {
88 : 969 : d_table["assume"] = Token::ASSUME_TOK;
89 : 969 : d_table["check-synth-next"] = Token::CHECK_SYNTH_NEXT_TOK;
90 : 969 : d_table["check-synth"] = Token::CHECK_SYNTH_TOK;
91 : 969 : d_table["constraint"] = Token::CONSTRAINT_TOK;
92 : 969 : d_table["declare-var"] = Token::DECLARE_VAR_TOK;
93 : 969 : d_table["inv-constraint"] = Token::INV_CONSTRAINT_TOK;
94 : 969 : d_table["set-feature"] = Token::SET_FEATURE_TOK;
95 : 969 : d_table["synth-fun"] = Token::SYNTH_FUN_TOK;
96 : 969 : d_table["synth-inv"] = Token::SYNTH_INV_TOK;
97 : : }
98 : 24437 : }
99 : :
100 : 669743 : Token Smt2CmdParser::nextCommandToken()
101 : : {
102 : 669743 : Token tok = d_lex.nextToken();
103 : : // symbols as commands
104 [ + - ]: 669743 : if (tok == Token::SYMBOL)
105 : : {
106 : 669743 : std::string str(d_lex.tokenStr());
107 : 669743 : std::map<std::string, Token>::iterator it = d_table.find(str);
108 [ + - ]: 669743 : if (it != d_table.end())
109 : : {
110 : 669743 : return it->second;
111 : : }
112 [ - + ]: 669743 : }
113 : 0 : return tok;
114 : : }
115 : :
116 : 690781 : std::unique_ptr<Cmd> Smt2CmdParser::parseNextCommand()
117 : : {
118 : : // if we are at the end of file, return the null command
119 [ + + ]: 690781 : if (d_lex.eatTokenChoice(Token::EOF_TOK, Token::LPAREN_TOK))
120 : : {
121 : 21037 : return nullptr;
122 : : }
123 : 669743 : std::unique_ptr<Cmd> cmd;
124 : 669743 : Token tok = nextCommandToken();
125 [ + + ][ + + ]: 669743 : switch (tok)
[ + + ][ + + ]
[ + + ][ + + ]
[ - + ][ + + ]
[ + + ][ + + ]
[ + + ][ + + ]
[ + + ][ + + ]
[ + + ][ + + ]
[ + + ][ + + ]
[ + + ][ + + ]
[ + + ][ + + ]
[ + + ][ + + ]
[ + + ][ + + ]
[ + + ][ + + ]
[ + - ][ - ]
126 : : {
127 : : // (assert <term>)
128 : 209969 : case Token::ASSERT_TOK:
129 : : {
130 : 209969 : d_state.checkThatLogicIsSet();
131 : 209968 : d_state.clearLastNamedTerm();
132 : 209968 : Term t = d_tparser.parseTerm();
133 : 209933 : cmd.reset(new AssertCommand(t));
134 [ + + ]: 209933 : if (d_state.lastNamedTerm().first == t)
135 : : {
136 [ + - ]: 11026 : Trace("parser") << "Process top-level name: " << t << std::endl;
137 : : // set the expression name, if there was a named term
138 : 11026 : std::pair<Term, std::string> namedTerm = d_state.lastNamedTerm();
139 : 11026 : d_state.getSymbolManager()->setExpressionName(
140 : : namedTerm.first, namedTerm.second, true);
141 [ + - ]: 11026 : Trace("parser") << "finished process top-level name" << std::endl;
142 : 11026 : }
143 : 209933 : }
144 : 209933 : break;
145 : : // sygus assume/constraint
146 : : // (assume <term>)
147 : : // (constraint <term>)
148 : 2811 : case Token::ASSUME_TOK:
149 : : case Token::CONSTRAINT_TOK:
150 : : {
151 : 2811 : bool isAssume = (tok == Token::ASSUME_TOK);
152 : 2811 : d_state.checkThatLogicIsSet();
153 : 2811 : Term t = d_tparser.parseTerm();
154 : 2808 : cmd.reset(new SygusConstraintCommand(t, isAssume));
155 : 2808 : }
156 : 2808 : break;
157 : : // (block-model <keyword>)
158 : 38 : case Token::BLOCK_MODEL_TOK:
159 : : {
160 : 38 : std::string key = d_tparser.parseKeyword();
161 : 38 : d_state.checkThatLogicIsSet();
162 : 38 : modes::BlockModelsMode mode = d_state.getBlockModelsMode(key);
163 : 38 : cmd.reset(new BlockModelCommand(mode));
164 : 38 : }
165 : 38 : break;
166 : : // (block-model-values (<term>*))
167 : 18 : case Token::BLOCK_MODEL_VALUES_TOK:
168 : : {
169 : 18 : d_state.checkThatLogicIsSet();
170 : 18 : std::vector<Term> terms = d_tparser.parseTermList();
171 : 18 : cmd.reset(new BlockModelValuesCommand(terms));
172 : 18 : }
173 : 18 : break;
174 : : // (check-sat)
175 : 26551 : case Token::CHECK_SAT_TOK:
176 : : {
177 : 26551 : d_state.checkThatLogicIsSet();
178 [ - + ]: 26551 : if (d_state.sygus())
179 : : {
180 : 0 : d_lex.parseError("Sygus does not support check-sat command.");
181 : : }
182 : 26551 : cmd.reset(new CheckSatCommand());
183 : : }
184 : 26551 : break;
185 : : // (check-sat-assuming (<term>*))
186 : 4136 : case Token::CHECK_SAT_ASSUMING_TOK:
187 : : {
188 : 4136 : d_state.checkThatLogicIsSet();
189 : 4136 : std::vector<Term> terms = d_tparser.parseTermList();
190 : 4133 : cmd.reset(new CheckSatAssumingCommand(terms));
191 : 4133 : }
192 : 4133 : break;
193 : : // (check-synth)
194 : 926 : case Token::CHECK_SYNTH_TOK:
195 : : {
196 : 926 : d_state.checkThatLogicIsSet();
197 : 926 : cmd.reset(new CheckSynthCommand());
198 : : }
199 : 926 : break;
200 : : // (check-synth-next)
201 : 24 : case Token::CHECK_SYNTH_NEXT_TOK:
202 : : {
203 : 24 : d_state.checkThatLogicIsSet();
204 : 24 : cmd.reset(new CheckSynthCommand(true));
205 : : }
206 : 24 : break;
207 : : // single datatype
208 : : // (declare-datatype <symbol> <datatype_dec>)
209 : : // (declare-codatatype <symbol> <datatype_dec>)
210 : 609 : case Token::DECLARE_CODATATYPE_TOK:
211 : : case Token::DECLARE_DATATYPE_TOK:
212 : : {
213 : 609 : d_state.checkThatLogicIsSet();
214 : 609 : std::vector<std::string> dnames;
215 : 609 : std::vector<size_t> arities;
216 : 609 : std::string name = d_tparser.parseSymbol(CHECK_UNDECLARED, SYM_SORT);
217 : 609 : dnames.push_back(name);
218 : 609 : bool isCo = (tok == Token::DECLARE_CODATATYPE_TOK);
219 : : // parse <datatype_dec>
220 : : std::vector<DatatypeDecl> dts =
221 : 609 : d_tparser.parseDatatypesDef(isCo, dnames, arities);
222 : 607 : cmd.reset(
223 : 1216 : new DatatypeDeclarationCommand(d_state.mkMutualDatatypeTypes(dts)));
224 : 615 : }
225 : 607 : break;
226 : : // multiple datatype
227 : : // (declare-datatypes (<sort_dec>^{n+1}) (<datatype_dec>^{n+1}) )
228 : : // (declare-codatatypes (<sort_dec>^{n+1}) (<datatype_dec>^{n+1}) )
229 : 3243 : case Token::DECLARE_CODATATYPES_TOK:
230 : : case Token::DECLARE_DATATYPES_TOK:
231 : : {
232 : 3243 : d_state.checkThatLogicIsSet();
233 : 3243 : d_lex.eatToken(Token::LPAREN_TOK);
234 : 3243 : std::vector<std::string> dnames;
235 : 3243 : std::vector<size_t> arities;
236 : : // parse (<sort_dec>^{n+1})
237 : : // while the next token is LPAREN, exit if RPAREN
238 [ + + ]: 7506 : while (d_lex.eatTokenChoice(Token::LPAREN_TOK, Token::RPAREN_TOK))
239 : : {
240 : 4263 : std::string name = d_tparser.parseSymbol(CHECK_UNDECLARED, SYM_SORT);
241 : 4263 : size_t arity = d_tparser.parseIntegerNumeral();
242 : 4263 : dnames.push_back(name);
243 : 4263 : arities.push_back(arity);
244 : 4263 : d_lex.eatToken(Token::RPAREN_TOK);
245 : 4263 : }
246 [ - + ]: 3243 : if (dnames.empty())
247 : : {
248 : 0 : d_lex.parseError("Empty list of datatypes");
249 : : }
250 : 3243 : bool isCo = (tok == Token::DECLARE_CODATATYPES_TOK);
251 : : // parse (<datatype_dec>^{n+1})
252 : 3243 : d_lex.eatToken(Token::LPAREN_TOK);
253 : : std::vector<DatatypeDecl> dts =
254 : 3243 : d_tparser.parseDatatypesDef(isCo, dnames, arities);
255 : 3243 : d_lex.eatToken(Token::RPAREN_TOK);
256 : 3242 : cmd.reset(
257 : 6485 : new DatatypeDeclarationCommand(d_state.mkMutualDatatypeTypes(dts)));
258 : 3245 : }
259 : 3242 : break;
260 : : // (declare-fun <symbol> (<sort>∗) <sort>)
261 : : // (declare-const <symbol> <sort>)
262 : 332265 : case Token::DECLARE_CONST_TOK:
263 : : case Token::DECLARE_FUN_TOK:
264 : : {
265 : 332265 : d_state.checkThatLogicIsSet();
266 : 332264 : std::string name = d_tparser.parseSymbol(CHECK_NONE, SYM_VARIABLE);
267 : 332264 : d_state.checkUserSymbol(name);
268 : 332262 : std::vector<Sort> sorts;
269 [ + + ]: 332262 : if (tok == Token::DECLARE_FUN_TOK)
270 : : {
271 : 320532 : sorts = d_tparser.parseSortList();
272 : : }
273 : 332260 : Sort t = d_tparser.parseSort();
274 [ + - ]: 332257 : Trace("parser") << "declare fun: '" << name << "'" << std::endl;
275 [ + + ][ + + ]: 332257 : if (!sorts.empty() || t.isFunction())
[ + + ]
276 : : {
277 : 41579 : t = d_state.flattenFunctionType(sorts, t);
278 : : }
279 [ + + ]: 332257 : if (!sorts.empty())
280 : : {
281 : 41579 : d_state.checkLogicAllowsFunctions();
282 : : }
283 : : // Note that we previously disallowed declare-fun in sygus here.
284 : : // we allow overloading for function declarations
285 : 332257 : cmd.reset(new DeclareFunctionCommand(name, sorts, t));
286 : 332269 : }
287 : 332257 : break;
288 : : // (declare-heap (<sort> <sort>))
289 : 258 : case Token::DECLARE_HEAP_TOK:
290 : : {
291 : 258 : d_lex.eatToken(Token::LPAREN_TOK);
292 : 258 : Sort t = d_tparser.parseSort();
293 : 258 : Sort s = d_tparser.parseSort();
294 : 258 : cmd.reset(new DeclareHeapCommand(t, s));
295 : 258 : d_lex.eatToken(Token::RPAREN_TOK);
296 : 258 : }
297 : 258 : break;
298 : : // (declare-oracle-fun <symbol> (<sort>∗) <sort> <symbol>)
299 : 0 : case Token::DECLARE_ORACLE_FUN_TOK:
300 : : {
301 : 0 : d_state.checkThatLogicIsSet();
302 : 0 : std::string name = d_tparser.parseSymbol(CHECK_NONE, SYM_VARIABLE);
303 : 0 : d_state.checkUserSymbol(name);
304 : 0 : std::vector<Sort> sorts;
305 : 0 : sorts = d_tparser.parseSortList();
306 : 0 : Sort t = d_tparser.parseSort();
307 [ - - ]: 0 : if (!sorts.empty())
308 : : {
309 : 0 : t = d_state.flattenFunctionType(sorts, t);
310 : : }
311 : 0 : tok = d_lex.peekToken();
312 : 0 : std::string binName;
313 [ - - ]: 0 : if (tok != Token::RPAREN_TOK)
314 : : {
315 : 0 : binName = d_tparser.parseSymbol(CHECK_NONE, SYM_VARIABLE);
316 : : }
317 : : // not supported
318 : 0 : d_state.warning(
319 : : "Oracles not supported via the text interface in this version");
320 : 0 : cmd.reset(new EmptyCommand());
321 : 0 : }
322 : 0 : break;
323 : : // (declare-pool <symbol> <sort> (<term>∗))
324 : 29 : case Token::DECLARE_POOL_TOK:
325 : : {
326 : 29 : d_state.checkThatLogicIsSet();
327 : 29 : std::string name = d_tparser.parseSymbol(CHECK_NONE, SYM_VARIABLE);
328 : 29 : d_state.checkUserSymbol(name);
329 : 29 : Sort t = d_tparser.parseSort();
330 : 29 : std::vector<Term> terms = d_tparser.parseTermList();
331 [ + - ]: 29 : Trace("parser") << "declare pool: '" << name << "'" << std::endl;
332 : 29 : cmd.reset(new DeclarePoolCommand(name, t, terms));
333 : 29 : }
334 : 29 : break;
335 : : // (declare-sort <symbol> <numeral>)
336 : 11516 : case Token::DECLARE_SORT_TOK:
337 : : {
338 : 11516 : d_state.checkThatLogicIsSet();
339 : 11516 : d_state.checkLogicAllowsFreeSorts();
340 : 11516 : std::string name = d_tparser.parseSymbol(CHECK_UNDECLARED, SYM_SORT);
341 : 11515 : d_state.checkUserSymbol(name);
342 : 11515 : size_t arity = d_tparser.parseIntegerNumeral();
343 [ + - ]: 23028 : Trace("parser") << "declare sort: '" << name << "' arity=" << arity
344 : 11514 : << std::endl;
345 : 11514 : cmd.reset(new DeclareSortCommand(name, arity));
346 : 11515 : }
347 : 11514 : break;
348 : : // (declare-sort-parameter <symbol>)
349 : 3 : case Token::DECLARE_SORT_PARAMETER_TOK:
350 : : {
351 : 3 : d_state.checkThatLogicIsSet();
352 : 3 : std::string name = d_tparser.parseSymbol(CHECK_NONE, SYM_VARIABLE);
353 : 3 : d_state.checkUserSymbol(name);
354 : : // not supported
355 : 3 : d_state.warning("Sort parameters not supported in this version");
356 : 3 : cmd.reset(new EmptyCommand());
357 : 3 : }
358 : 3 : break;
359 : : // (declare-var <symbol> <sort>)
360 : 1379 : case Token::DECLARE_VAR_TOK:
361 : : {
362 : 1379 : d_state.checkThatLogicIsSet();
363 : 1379 : std::string name = d_tparser.parseSymbol(CHECK_UNDECLARED, SYM_VARIABLE);
364 : 1379 : d_state.checkUserSymbol(name);
365 : 1379 : Sort t = d_tparser.parseSort();
366 : 1379 : cmd.reset(new DeclareSygusVarCommand(name, t));
367 : 1379 : }
368 : 1379 : break;
369 : : // (define-const <symbol> <sort> <term>)
370 : 38 : case Token::DEFINE_CONST_TOK:
371 : : {
372 : 38 : d_state.checkThatLogicIsSet();
373 : 38 : std::string name = d_tparser.parseSymbol(CHECK_UNDECLARED, SYM_VARIABLE);
374 : 38 : d_state.checkUserSymbol(name);
375 : 38 : Sort t = d_tparser.parseSort();
376 : 38 : Term e = d_tparser.parseTerm();
377 : :
378 : : // declare the name down here (while parsing term, signature
379 : : // must not be extended with the name itself; no recursion
380 : : // permitted)
381 : 38 : cmd.reset(new DefineFunctionCommand(name, t, e));
382 : 38 : }
383 : 38 : break;
384 : : // (define-fun <symbol> (<sorted_var>*) <sort> <term>)
385 : 7280 : case Token::DEFINE_FUN_TOK:
386 : : {
387 : 7280 : d_state.checkThatLogicIsSet();
388 : 7280 : std::string name = d_tparser.parseSymbol(CHECK_UNDECLARED, SYM_VARIABLE);
389 : 7280 : d_state.checkUserSymbol(name);
390 : : std::vector<std::pair<std::string, Sort>> sortedVarNames =
391 : 7280 : d_tparser.parseSortedVarList();
392 : 7280 : Sort t = d_tparser.parseSort();
393 : : /* add variables to parser state before parsing term */
394 [ + - ]: 7280 : Trace("parser") << "define fun: '" << name << "'" << std::endl;
395 : 7280 : std::vector<Sort> sorts;
396 [ + + ]: 7280 : if (sortedVarNames.size() > 0)
397 : : {
398 : 4492 : sorts.reserve(sortedVarNames.size());
399 [ + + ]: 15771 : for (const std::pair<std::string, Sort>& i : sortedVarNames)
400 : : {
401 : 11279 : sorts.push_back(i.second);
402 : : }
403 : : }
404 : 7280 : std::vector<Term> flattenVars;
405 : 7280 : t = d_state.flattenFunctionType(sorts, t, flattenVars);
406 [ + + ]: 7280 : if (sortedVarNames.size() > 0)
407 : : {
408 : 4492 : d_state.pushScope();
409 : : }
410 : 7280 : bool freshBinders = d_state.usingFreshBinders();
411 : : // If freshBinders is false, we use fresh=false here to ensure that
412 : : // variables introduced by define-fun are accurate with respect to proofs,
413 : : // i.e. variables of the same name and type are indeed the same variable.
414 : : std::vector<Term> terms =
415 : 7280 : d_state.bindBoundVars(sortedVarNames, freshBinders);
416 : 7280 : Term expr = d_tparser.parseTerm();
417 [ + + ]: 7276 : if (!flattenVars.empty())
418 : : {
419 : : // if this function has any implicit variables flattenVars,
420 : : // we apply the body of the definition to the flatten vars
421 : 7 : expr = d_state.mkHoApply(expr, flattenVars);
422 : 7 : terms.insert(terms.end(), flattenVars.begin(), flattenVars.end());
423 : : }
424 [ + + ]: 7276 : if (sortedVarNames.size() > 0)
425 : : {
426 : 4489 : d_state.popScope();
427 : : }
428 : 7276 : cmd.reset(new DefineFunctionCommand(name, terms, t, expr));
429 : 7300 : }
430 : 7276 : break;
431 : : // (define-fun-rec <symbol> (<sorted_var>*) <sort> <term>)
432 : 564 : case Token::DEFINE_FUN_REC_TOK:
433 : : {
434 : 564 : d_state.checkThatLogicIsSet();
435 : : // outermost scope to handle the definition of the function
436 : 564 : d_state.pushScope();
437 : 564 : std::string fname = d_tparser.parseSymbol(CHECK_NONE, SYM_VARIABLE);
438 : 564 : d_state.checkUserSymbol(fname);
439 : : std::vector<std::pair<std::string, Sort>> sortedVarNames =
440 : 564 : d_tparser.parseSortedVarList();
441 : 564 : Sort t = d_tparser.parseSort();
442 : 564 : std::vector<Term> flattenVars;
443 : 564 : std::vector<Term> bvs;
444 : : Term func =
445 : 564 : d_state.setupDefineFunRecScope(fname, sortedVarNames, t, flattenVars);
446 : 564 : d_state.pushDefineFunRecScope(sortedVarNames, flattenVars, bvs);
447 : 564 : Term expr = d_tparser.parseTerm();
448 : 564 : d_state.popScope();
449 [ - + ]: 564 : if (!flattenVars.empty())
450 : : {
451 : 0 : expr = d_state.mkHoApply(expr, flattenVars);
452 : : }
453 : 564 : cmd.reset(new DefineFunctionRecCommand(func, bvs, expr));
454 : : // pop the scope
455 : 564 : d_state.popScope();
456 : 564 : }
457 : 564 : break;
458 : : // (define-funs-rec (<function_dec>^{n+1}) (<term>^{n+1}))
459 : : // where
460 : : // <function_dec> := (<symbol> (<sorted_var>*) <sort>)
461 : 75 : case Token::DEFINE_FUNS_REC_TOK:
462 : : {
463 : 75 : d_state.checkThatLogicIsSet();
464 : : // outermost scope to handle the definition of the functions
465 : 75 : d_state.pushScope();
466 : 75 : d_lex.eatToken(Token::LPAREN_TOK);
467 : 75 : std::vector<Term> funcs;
468 : 75 : std::vector<std::vector<std::pair<std::string, Sort>>> sortedVarNamesList;
469 : 75 : std::vector<std::vector<Term>> flattenVarsList;
470 : : // while the next token is LPAREN, exit if RPAREN
471 : : // parse <function_dec>^{n+1}
472 [ + + ]: 269 : while (d_lex.eatTokenChoice(Token::LPAREN_TOK, Token::RPAREN_TOK))
473 : : {
474 : : std::string fname =
475 : 194 : d_tparser.parseSymbol(CHECK_UNDECLARED, SYM_VARIABLE);
476 : 194 : d_state.checkUserSymbol(fname);
477 : : std::vector<std::pair<std::string, Sort>> sortedVarNames =
478 : 194 : d_tparser.parseSortedVarList();
479 : 194 : Sort t = d_tparser.parseSort();
480 : 194 : std::vector<Term> flattenVars;
481 : 194 : Term func = d_state.setupDefineFunRecScope(
482 : 194 : fname, sortedVarNames, t, flattenVars);
483 : 194 : funcs.push_back(func);
484 : :
485 : : // add to lists (need to remember for when parsing the bodies)
486 : 194 : sortedVarNamesList.push_back(sortedVarNames);
487 : 194 : flattenVarsList.push_back(flattenVars);
488 : 194 : d_lex.eatToken(Token::RPAREN_TOK);
489 : 194 : }
490 : :
491 : : // parse the bodies
492 : 75 : d_lex.eatToken(Token::LPAREN_TOK);
493 : 75 : std::vector<Term> funcDefs;
494 : 75 : std::vector<std::vector<Term>> formals;
495 : : // parse <term>^{n+1}
496 [ + + ]: 269 : for (size_t j = 0, nfuncs = funcs.size(); j < nfuncs; j++)
497 : : {
498 : 194 : std::vector<Term> bvs;
499 : 194 : d_state.pushDefineFunRecScope(
500 : 194 : sortedVarNamesList[j], flattenVarsList[j], bvs);
501 : 194 : Term expr = d_tparser.parseTerm();
502 : 194 : d_state.popScope();
503 : 194 : funcDefs.push_back(expr);
504 : 194 : formals.push_back(bvs);
505 : 194 : }
506 : 75 : d_lex.eatToken(Token::RPAREN_TOK);
507 [ - + ][ - + ]: 75 : Assert(funcs.size() == funcDefs.size());
[ - - ]
508 : 75 : cmd.reset(new DefineFunctionRecCommand(funcs, formals, funcDefs));
509 : : // pop the scope
510 : 75 : d_state.popScope();
511 : 75 : }
512 : 75 : break;
513 : : // (define-sort <symbol> (<symbol>*) <sort>)
514 : 753 : case Token::DEFINE_SORT_TOK:
515 : : {
516 : 753 : d_state.checkThatLogicIsSet();
517 : 753 : std::string name = d_tparser.parseSymbol(CHECK_UNDECLARED, SYM_SORT);
518 : 753 : d_state.checkUserSymbol(name);
519 : : std::vector<std::string> snames =
520 : 753 : d_tparser.parseSymbolList(CHECK_UNDECLARED, SYM_SORT);
521 : 753 : d_state.pushScope();
522 : 753 : std::vector<Sort> sorts;
523 [ + + ]: 757 : for (const std::string& sname : snames)
524 : : {
525 : 4 : sorts.push_back(d_state.mkSort(sname));
526 : : }
527 : 753 : Sort t = d_tparser.parseSort();
528 : 753 : d_state.popScope();
529 : 753 : cmd.reset(new DefineSortCommand(name, sorts, t));
530 : 753 : }
531 : 753 : break;
532 : : // (echo <string>)
533 : 28 : case Token::ECHO_TOK:
534 : : {
535 : : // optional string literal
536 : 28 : tok = d_lex.peekToken();
537 [ + - ]: 28 : if (tok == Token::STRING_LITERAL)
538 : : {
539 : 28 : std::string msg = d_tparser.parseStr(true);
540 : 28 : cmd.reset(new EchoCommand(msg));
541 : 28 : }
542 : : else
543 : : {
544 : 0 : cmd.reset(new EchoCommand());
545 : : }
546 : : }
547 : 28 : break;
548 : : // (exit)
549 : 3040 : case Token::EXIT_TOK:
550 : : {
551 : 3040 : cmd.reset(new QuitCommand());
552 : : }
553 : 3040 : break;
554 : 93 : case Token::FIND_SYNTH_TOK:
555 : : {
556 : 93 : d_state.checkThatLogicIsSet();
557 : 93 : std::string key = d_tparser.parseKeyword();
558 : 93 : modes::FindSynthTarget fst = d_state.getFindSynthTarget(key);
559 : 93 : std::vector<Term> emptyVarList;
560 : 93 : Grammar* g = d_tparser.parseGrammarOrNull(emptyVarList);
561 : 93 : cmd.reset(new FindSynthCommand(fst, g));
562 : 93 : }
563 : 93 : break;
564 : 3 : case Token::FIND_SYNTH_NEXT_TOK:
565 : : {
566 : 3 : d_state.checkThatLogicIsSet();
567 : 3 : cmd.reset(new FindSynthNextCommand);
568 : : }
569 : 3 : break;
570 : : // (get-abduct <symbol> <term> <grammar>?)
571 : 132 : case Token::GET_ABDUCT_TOK:
572 : : {
573 : 132 : d_state.checkThatLogicIsSet();
574 : 132 : std::string name = d_tparser.parseSymbol(CHECK_UNDECLARED, SYM_VARIABLE);
575 : 132 : Term t = d_tparser.parseTerm();
576 : : // parse optional grammar
577 : 132 : std::vector<Term> emptyVarList;
578 : 132 : Grammar* g = d_tparser.parseGrammarOrNull(emptyVarList);
579 : 132 : cmd.reset(new GetAbductCommand(name, t, g));
580 : 132 : }
581 : 132 : break;
582 : : // (get-abduct-next)
583 : 24 : case Token::GET_ABDUCT_NEXT_TOK:
584 : : {
585 : 24 : d_state.checkThatLogicIsSet();
586 : 24 : cmd.reset(new GetAbductNextCommand);
587 : : }
588 : 24 : break;
589 : : // (get-assertions)
590 : 4 : case Token::GET_ASSERTIONS_TOK:
591 : : {
592 : 4 : d_state.checkThatLogicIsSet();
593 : 4 : cmd.reset(new GetAssertionsCommand());
594 : : }
595 : 4 : break;
596 : : // (get-assignment)
597 : 20 : case Token::GET_ASSIGNMENT_TOK:
598 : : {
599 : 20 : d_state.checkThatLogicIsSet();
600 : 20 : cmd.reset(new GetAssignmentCommand());
601 : : }
602 : 20 : break;
603 : : // (get-difficulty)
604 : 10 : case Token::GET_DIFFICULTY_TOK:
605 : : {
606 : 10 : d_state.checkThatLogicIsSet();
607 : 10 : cmd.reset(new GetDifficultyCommand);
608 : : }
609 : 10 : break;
610 : : // (get-info <keyword>)
611 : 47 : case Token::GET_INFO_TOK:
612 : : {
613 : 47 : std::string key = d_tparser.parseKeyword();
614 : 47 : cmd.reset(new GetInfoCommand(key));
615 : 47 : }
616 : 47 : break;
617 : : // (get-interpolant <symbol> <term> <grammar>?)
618 : 69 : case Token::GET_INTERPOL_TOK:
619 : : {
620 : 69 : d_state.checkThatLogicIsSet();
621 : 69 : std::string name = d_tparser.parseSymbol(CHECK_UNDECLARED, SYM_VARIABLE);
622 : 69 : Term t = d_tparser.parseTerm();
623 : 69 : std::vector<Term> emptyVarList;
624 : 69 : Grammar* g = d_tparser.parseGrammarOrNull(emptyVarList);
625 : 69 : cmd.reset(new GetInterpolantCommand(name, t, g));
626 : 69 : }
627 : 69 : break;
628 : : // (get-interpolant-next)
629 : 3 : case Token::GET_INTERPOL_NEXT_TOK:
630 : : {
631 : 3 : d_state.checkThatLogicIsSet();
632 : 3 : cmd.reset(new GetInterpolantNextCommand);
633 : : }
634 : 3 : break;
635 : : // (get-learned-literals <keyword>?)
636 : 28 : case Token::GET_LEARNED_LITERALS_TOK:
637 : : {
638 : : // optional keyword
639 : 28 : tok = d_lex.peekToken();
640 : 28 : modes::LearnedLitType llt = modes::LearnedLitType::INPUT;
641 [ + + ]: 28 : if (tok == Token::KEYWORD)
642 : : {
643 : 23 : std::string key = d_tparser.parseKeyword();
644 : 23 : llt = d_state.getLearnedLitType(key);
645 : 23 : }
646 : 28 : d_state.checkThatLogicIsSet();
647 : 28 : cmd.reset(new GetLearnedLiteralsCommand(llt));
648 : : }
649 : 28 : break;
650 : : // (get-model)
651 : 105 : case Token::GET_MODEL_TOK:
652 : : {
653 : 105 : d_state.checkThatLogicIsSet();
654 : 105 : cmd.reset(new GetModelCommand());
655 : : }
656 : 105 : break;
657 : : // (get-option <keyword>)
658 : 135 : case Token::GET_OPTION_TOK:
659 : : {
660 : 135 : std::string key = d_tparser.parseKeyword();
661 : 135 : cmd.reset(new GetOptionCommand(key));
662 : 135 : }
663 : 135 : break;
664 : : // (get-proof <keyword>?)
665 : 38 : case Token::GET_PROOF_TOK:
666 : : {
667 : : // optional keyword
668 : 38 : tok = d_lex.peekToken();
669 : 38 : modes::ProofComponent pc = modes::ProofComponent::FULL;
670 [ + + ]: 38 : if (tok == Token::KEYWORD)
671 : : {
672 : 25 : std::string key = d_tparser.parseKeyword();
673 : 25 : pc = d_state.getProofComponent(key);
674 : 25 : }
675 : 38 : d_state.checkThatLogicIsSet();
676 : 38 : cmd.reset(new GetProofCommand(pc));
677 : : }
678 : 38 : break;
679 : : // quantifier elimination commands
680 : : // (get-qe <term>)
681 : : // (get-qe-disjunct <term>)
682 : 57 : case Token::GET_QE_TOK:
683 : : case Token::GET_QE_DISJUNCT_TOK:
684 : : {
685 : 57 : d_state.checkThatLogicIsSet();
686 : 57 : Term t = d_tparser.parseTerm();
687 : 57 : bool isFull = (tok == Token::GET_QE_TOK);
688 : 57 : cmd.reset(new GetQuantifierEliminationCommand(t, isFull));
689 : 57 : }
690 : 57 : break;
691 : : // (get-timeout-core)
692 : 27 : case Token::GET_TIMEOUT_CORE_TOK:
693 : : {
694 : 27 : d_state.checkThatLogicIsSet();
695 : 27 : cmd.reset(new GetTimeoutCoreCommand);
696 : : }
697 : 27 : break;
698 : 16 : case Token::GET_TIMEOUT_CORE_ASSUMING_TOK:
699 : : {
700 : 16 : d_state.checkThatLogicIsSet();
701 : : // read optional assumptions
702 : 16 : d_lex.eatToken(Token::LPAREN_TOK);
703 : 16 : std::vector<Term> assumptions;
704 : 16 : tok = d_lex.peekToken();
705 [ + + ]: 44 : while (tok != Token::RPAREN_TOK)
706 : : {
707 : 28 : d_state.clearLastNamedTerm();
708 : 28 : Term t = d_tparser.parseTerm();
709 : 28 : std::pair<Term, std::string> namedTerm = d_state.lastNamedTerm();
710 [ + + ]: 28 : if (namedTerm.first == t)
711 : : {
712 : 12 : d_state.getSymbolManager()->setExpressionName(
713 : : namedTerm.first, namedTerm.second, true);
714 : : }
715 : 28 : assumptions.push_back(t);
716 : 28 : tok = d_lex.peekToken();
717 : 28 : }
718 [ - + ]: 16 : if (assumptions.empty())
719 : : {
720 : 0 : d_lex.parseError(
721 : : "Expected non-empty list of assumptions for "
722 : : "get-timeout-core-assuming");
723 : : }
724 : 16 : d_lex.nextToken();
725 : 16 : cmd.reset(new GetTimeoutCoreCommand(assumptions));
726 : 16 : }
727 : 16 : break;
728 : : // (get-unsat-assumptions)
729 : 32 : case Token::GET_UNSAT_ASSUMPTIONS_TOK:
730 : : {
731 : 32 : d_state.checkThatLogicIsSet();
732 : 32 : cmd.reset(new GetUnsatAssumptionsCommand);
733 : : }
734 : 32 : break;
735 : : // (get-unsat-core)
736 : 56 : case Token::GET_UNSAT_CORE_TOK:
737 : : {
738 : 56 : d_state.checkThatLogicIsSet();
739 : 56 : cmd.reset(new GetUnsatCoreCommand);
740 : : }
741 : 56 : break;
742 : : // (get-unsat-core-lemmas)
743 : 8 : case Token::GET_UNSAT_CORE_LEMMAS_TOK:
744 : : {
745 : 8 : d_state.checkThatLogicIsSet();
746 : 8 : cmd.reset(new GetUnsatCoreLemmasCommand);
747 : : }
748 : 8 : break;
749 : : // (get-value (<term>+))
750 : 221 : case Token::GET_VALUE_TOK:
751 : : {
752 : 221 : d_state.checkThatLogicIsSet();
753 : : // bind all symbols specific to the model, e.g. uninterpreted constant
754 : : // values
755 : 221 : d_state.pushGetValueScope();
756 : 221 : std::vector<Term> terms = d_tparser.parseTermList();
757 [ + + ]: 219 : if (terms.empty())
758 : : {
759 : 3 : d_lex.parseError("Expected non-empty list of terms for get-value");
760 : : }
761 : 218 : cmd.reset(new GetValueCommand(terms));
762 : 218 : d_state.popScope();
763 : 219 : }
764 : 218 : break;
765 : : // (get-model-domain-elements <sort>)
766 : 8 : case Token::GET_MODEL_DOMAIN_ELEMENTS_TOK:
767 : : {
768 : 8 : d_state.checkThatLogicIsSet();
769 : 8 : cvc5::Sort sort = d_tparser.parseSort();
770 : 8 : cmd.reset(new GetModelDomainElementsCommand(sort));
771 : 8 : }
772 : 8 : break;
773 : : // (inv-constraint <symbol> <symbol> <symbol> <symbol>)
774 : 51 : case Token::INV_CONSTRAINT_TOK:
775 : : {
776 : 51 : std::vector<std::string> names;
777 [ + + ]: 255 : for (size_t i = 0; i < 4; i++)
778 : : {
779 : 204 : std::string name = d_tparser.parseSymbol(CHECK_NONE, SYM_VARIABLE);
780 : 204 : names.push_back(name);
781 : 204 : }
782 : 51 : d_state.checkThatLogicIsSet();
783 : 51 : cmd = d_state.invConstraint(names);
784 : 51 : }
785 : 51 : break;
786 : : // (pop <numeral>?)
787 : 4564 : case Token::POP_TOK:
788 : : {
789 : : // optional integer
790 : 4564 : tok = d_lex.peekToken();
791 [ + + ]: 4564 : if (tok == Token::INTEGER_LITERAL)
792 : : {
793 : 4205 : size_t num = d_tparser.parseIntegerNumeral();
794 : 4205 : cmd = d_state.handlePop(num);
795 : : }
796 : : else
797 : : {
798 : 359 : cmd = d_state.handlePop(std::nullopt);
799 : : }
800 : : }
801 : 4564 : break;
802 : : // (push <numeral>?)
803 : 5681 : case Token::PUSH_TOK:
804 : : {
805 : : // optional integer
806 : 5681 : tok = d_lex.peekToken();
807 [ + + ]: 5681 : if (tok == Token::INTEGER_LITERAL)
808 : : {
809 : 5228 : size_t num = d_tparser.parseIntegerNumeral();
810 : 5228 : cmd = d_state.handlePush(num);
811 : : }
812 : : else
813 : : {
814 : 453 : cmd = d_state.handlePush(std::nullopt);
815 : : }
816 : : }
817 : 5681 : break;
818 : : // (reset)
819 : 83 : case Token::RESET_TOK:
820 : : {
821 : 83 : cmd.reset(new ResetCommand());
822 : : // reset the state of the parser, which is independent of the symbol
823 : : // manager
824 : 83 : d_state.reset();
825 : : }
826 : 83 : break;
827 : : // (reset-assertions)
828 : 62 : case Token::RESET_ASSERTIONS_TOK:
829 : : {
830 : 62 : cmd.reset(new ResetAssertionsCommand());
831 : : }
832 : 62 : break;
833 : : // (set-feature <attribute>)
834 : 11 : case Token::SET_FEATURE_TOK:
835 : : {
836 : 11 : std::string key = d_tparser.parseKeyword();
837 : 11 : Term s = d_tparser.parseSymbolicExpr();
838 : : // ":grammars" and "fwd-decls" are defined in the SyGuS version 2.1
839 : : // standard and are supported by default, all other features are not.
840 [ + + ][ + + ]: 11 : if (key != "grammars" && key != "fwd-decls")
[ + + ]
841 : : {
842 : 3 : std::stringstream ss;
843 : 3 : ss << "SyGuS feature " << key << " not currently supported";
844 : 3 : d_state.warning(ss.str());
845 : 3 : }
846 : 11 : cmd.reset(new EmptyCommand());
847 : 11 : }
848 : 11 : break;
849 : : // (set-info <attribute>)
850 : 19072 : case Token::SET_INFO_TOK:
851 : : {
852 : 19072 : std::string key = d_tparser.parseKeyword();
853 : 19072 : Term sexpr = d_tparser.parseSymbolicExpr();
854 : 19072 : cmd.reset(new SetInfoCommand(key, sexprToString(sexpr)));
855 : 19072 : }
856 : 19072 : break;
857 : : // (set-logic <symbol>)
858 : 24206 : case Token::SET_LOGIC_TOK:
859 : : {
860 : 24206 : SymManager* sm = d_state.getSymbolManager();
861 : 24206 : std::string name = d_tparser.parseSymbol(CHECK_NONE, SYM_SORT);
862 : : // If the logic was forced, we ignore all set-logic commands.
863 [ + + ]: 24206 : if (!sm->isLogicForced())
864 : : {
865 : 24199 : d_state.setLogic(name);
866 : 24189 : cmd.reset(new SetBenchmarkLogicCommand(name));
867 : : }
868 : : else
869 : : {
870 : : // otherwise ignore the command
871 : 12 : cmd.reset(new EmptyCommand());
872 : : }
873 : 24206 : }
874 : 24201 : break;
875 : : // (set-option <option>)
876 : 7711 : case Token::SET_OPTION_TOK:
877 : : {
878 : 7711 : std::string key = d_tparser.parseKeyword();
879 : 7711 : Term sexpr = d_tparser.parseSymbolicExpr();
880 : 7710 : std::string ss = sexprToString(sexpr);
881 : : // special case: for channel settings, we are expected to parse e.g.
882 : : // `"stdin"` which should be treated as `stdin`
883 : : // Note we could consider a more general solution where knowing whether
884 : : // this special case holds can be queried via OptionInfo.
885 [ + + ]: 15414 : if (key == "diagnostic-output-channel" || key == "regular-output-channel"
886 [ + + ][ + + ]: 15414 : || key == "in" || key == "out")
[ - + ][ + + ]
887 : : {
888 : 12 : ss = d_state.stripQuotes(ss);
889 : : }
890 [ + + ]: 7698 : else if (key == "use-portfolio")
891 : : {
892 : : // we don't allow setting portfolio via the command line
893 : 3 : d_lex.parseError("Can only enable use-portfolio via the command line");
894 : : }
895 : 7709 : cmd.reset(new SetOptionCommand(key, ss));
896 : : // Ugly that this changes the state of the parser; but
897 : : // global-declarations affects parsing, so we can't hold off
898 : : // on this until some SolverEngine eventually (if ever) executes it.
899 [ + + ]: 7709 : if (key == "global-declarations")
900 : : {
901 : 129 : d_state.getSymbolManager()->setGlobalDeclarations(ss == "true");
902 : : }
903 [ - + ]: 7580 : else if (key == "fresh-declarations")
904 : : {
905 : 0 : d_state.getSymbolManager()->setFreshDeclarations(ss == "true");
906 : : }
907 [ - + ]: 7580 : else if (key == "term-sort-overload")
908 : : {
909 : 0 : d_state.getSymbolManager()->setTermSortOverload(ss == "true");
910 : : }
911 : 7713 : }
912 : 7709 : break;
913 : : // (simplify <term>)
914 : 1 : case Token::SIMPLIFY_TOK:
915 : : {
916 : 1 : d_state.checkThatLogicIsSet();
917 : 1 : Term t = d_tparser.parseTerm();
918 : 0 : cmd.reset(new SimplifyCommand(t));
919 : 0 : }
920 : 0 : break;
921 : : // (synth-fun <symbol> (<sorted_var>*) <sort> <grammar>?)
922 : : // (synth-inv <symbol> (<sorted_var>*) <grammar>?)
923 : 1612 : case Token::SYNTH_FUN_TOK:
924 : : case Token::SYNTH_INV_TOK:
925 : : {
926 : 1612 : d_state.checkThatLogicIsSet();
927 : 1612 : std::string name = d_tparser.parseSymbol(CHECK_UNDECLARED, SYM_VARIABLE);
928 : : std::vector<std::pair<std::string, Sort>> sortedVarNames =
929 : 1612 : d_tparser.parseSortedVarList();
930 : 1611 : Sort range;
931 : 1611 : bool isInv = (tok == Token::SYNTH_INV_TOK);
932 [ + + ]: 1611 : if (isInv)
933 : : {
934 : 38 : range = d_state.getSolver()->getTermManager().getBooleanSort();
935 : : }
936 : : else
937 : : {
938 : 1573 : range = d_tparser.parseSort();
939 : : }
940 : 1611 : d_state.pushScope();
941 : 1611 : std::vector<cvc5::Term> sygusVars = d_state.bindBoundVars(sortedVarNames);
942 : 1611 : Grammar* g = d_tparser.parseGrammarOrNull(sygusVars);
943 : :
944 [ + - ]: 1609 : Trace("parser-sygus") << "Define synth fun : " << name << std::endl;
945 : 1609 : d_state.popScope();
946 : 1609 : cmd.reset(new SynthFunCommand(name, sygusVars, range, g));
947 : 1618 : }
948 : 1609 : break;
949 : 0 : case Token::EOF_TOK:
950 : 0 : d_lex.parseError("Expected SMT-LIBv2 command", true);
951 : 0 : break;
952 : 0 : default:
953 : 0 : d_lex.unexpectedTokenError(tok, "Expected SMT-LIBv2 command");
954 : 0 : break;
955 : : }
956 : 669670 : d_lex.eatToken(Token::RPAREN_TOK);
957 : 669668 : return cmd;
958 : 669743 : }
959 : :
960 : : } // namespace parser
961 : : } // namespace cvc5
|
