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