1 /* ****************************************************************************
2 * Top contributors (to current version):
3 * Andrew Reynolds, Morgan Deters, Christopher L. Conway
5 * This file is part of the cvc5 project.
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 * ****************************************************************************
13 * Parser for SMT-LIB v2 input language.
22 // Skip the default error handling, just break with exceptions
23 // defaultErrorHandler = false;
25 // Only lookahead of <= k requested (disable for LL* parsing)
26 // Note that cvc5's BoundedTokenBuffer requires a fixed k !
27 // If you change this k, change it also in smt2_input.cpp !
32 /* ****************************************************************************
33 * This file is part of the cvc5 project.
35 * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
36 * in the top-level source directory and their institutional affiliations.
37 * All rights reserved. See the file COPYING in the top-level source
38 * directory for licensing information.
39 * ****************************************************************************
45 /** This suppresses warnings about the redefinition of token symbols between
46 * different parsers. The redefinitions should be harmless as long as no
47 * client: (a) #include's the lexer headers for two grammars AND (b) uses the
48 * token symbol definitions.
50 #pragma GCC system_header
52 #if defined(CVC5_COMPETITION_MODE) && !defined(CVC5_SMTCOMP_APPLICATION_TRACK)
53 /* This improves performance by ~10 percent on big inputs.
54 * This option is only valid if we know the input is ASCII (or some 8-bit encoding).
55 * If we know the input is UTF-16, we can use ANTLR3_INLINE_INPUT_UTF16.
56 * Otherwise, we have to let the lexer detect the encoding at runtime.
58 # define ANTLR3_INLINE_INPUT_ASCII
59 # define ANTLR3_INLINE_INPUT_8BIT
60 #endif /* CVC5_COMPETITION_MODE && !CVC5_SMTCOMP_APPLICATION_TRACK */
62 }/* @lexer::includes */
65 #include "parser/smt2/smt2.h"
66 #include "parser/antlr_input.h"
69 using namespace cvc5::parser;
72 #define PARSER_STATE ((Smt2*)LEXER->super)
73 }/* @lexer::postinclude */
79 #include "base/check.h"
80 #include "parser/parse_op.h"
81 #include "parser/parser.h"
82 #include "smt/command.h"
91 }/* @parser::includes */
93 @parser::postinclude {
98 #include <unordered_set>
101 #include "api/cpp/cvc5.h"
102 #include "base/output.h"
103 #include "parser/antlr_input.h"
104 #include "parser/parser.h"
105 #include "parser/smt2/smt2.h"
106 #include "util/floatingpoint_size.h"
107 #include "util/hash.h"
109 using namespace cvc5;
110 using namespace cvc5::parser;
112 /* These need to be macros so they can refer to the PARSER macro, which
113 * will be defined by ANTLR *after* this section. (If they were functions,
114 * PARSER would be undefined.) */
116 #define PARSER_STATE ((Smt2*)PARSER->super)
118 #define SOLVER PARSER_STATE->getSolver()
120 #define SYM_MAN PARSER_STATE->getSymbolManager()
122 #define MK_TERM(KIND, ...) SOLVER->mkTerm(KIND, {__VA_ARGS__})
123 #define UNSUPPORTED PARSER_STATE->unimplementedFeature
125 }/* parser::postinclude */
128 * Parses an expression.
129 * @return the parsed expression, or the Null Expr if we've reached the
132 parseExpr returns [cvc5::Term expr = cvc5::Term()]
142 * @return the parsed command, or NULL if we've reached the end of the input
144 parseCommand returns [cvc5::Command* cmd_return = NULL]
146 std::unique_ptr<cvc5::Command> cmd;
150 cmd_return = cmd.release();
152 : LPAREN_TOK command[&cmd] RPAREN_TOK
154 /* This extended command has to be in the outermost production so that
155 * the RPAREN_TOK is properly eaten and we are in a good state to read
156 * the included file's tokens. */
157 | LPAREN_TOK INCLUDE_TOK str[name,true] RPAREN_TOK
158 { if(!PARSER_STATE->canIncludeFile()) {
159 PARSER_STATE->parseError("include-file feature was disabled for this "
162 if(PARSER_STATE->strictModeEnabled()) {
163 PARSER_STATE->parseError("Extended commands are not permitted while "
164 "operating in strict compliance mode.");
166 PARSER_STATE->includeFile(name);
167 // The command of the included file will be produced at the next
168 // parseCommand() call
169 cmd.reset(new EmptyCommand("include::" + name));
176 * Parses a SyGuS command.
177 * @return the parsed SyGuS command, or NULL if we've reached the end of the
180 parseSygus returns [cvc5::Command* cmd_return = NULL]
185 cmd_return = cmd.release();
187 : LPAREN_TOK cmd=sygusCommand RPAREN_TOK
192 * Parse the internal portion of the command, ignoring the surrounding
195 command [std::unique_ptr<cvc5::Command>* cmd]
198 std::vector<std::string> names;
199 cvc5::Term expr, expr2;
201 std::vector<cvc5::Term> terms;
202 std::vector<cvc5::Sort> sorts;
203 std::vector<std::pair<std::string, cvc5::Sort> > sortedVarNames;
204 std::vector<cvc5::Term> flattenVars;
206 : /* set the logic */
207 SET_LOGIC_TOK symbol[name,CHECK_NONE,SYM_SORT]
209 cmd->reset(PARSER_STATE->setLogic(name));
212 SET_INFO_TOK setInfoInternal[cmd]
215 { cmd->reset(new GetInfoCommand(
216 AntlrInput::tokenText($KEYWORD).c_str() + 1));
219 SET_OPTION_TOK setOptionInternal[cmd]
221 GET_OPTION_TOK KEYWORD
222 { cmd->reset(new GetOptionCommand(
223 AntlrInput::tokenText($KEYWORD).c_str() + 1));
225 | /* sort declaration */
228 PARSER_STATE->checkThatLogicIsSet();
229 PARSER_STATE->checkLogicAllowsFreeSorts();
231 symbol[name,CHECK_UNDECLARED,SYM_SORT]
232 { PARSER_STATE->checkUserSymbol(name); }
234 { Trace("parser") << "declare sort: '" << name
235 << "' arity=" << n << std::endl;
236 unsigned arity = AntlrInput::tokenToUnsigned(n);
238 cvc5::Sort type = PARSER_STATE->mkSort(name);
239 cmd->reset(new DeclareSortCommand(name, 0, type));
241 cvc5::Sort type = PARSER_STATE->mkSortConstructor(name, arity);
242 cmd->reset(new DeclareSortCommand(name, arity, type));
245 | /* sort definition */
246 DEFINE_SORT_TOK { PARSER_STATE->checkThatLogicIsSet(); }
247 symbol[name,CHECK_UNDECLARED,SYM_SORT]
248 { PARSER_STATE->checkUserSymbol(name); }
249 LPAREN_TOK symbolList[names,CHECK_UNDECLARED,SYM_SORT] RPAREN_TOK
250 { PARSER_STATE->pushScope();
251 for(std::vector<std::string>::const_iterator i = names.begin(),
255 sorts.push_back(PARSER_STATE->mkSort(*i));
258 sortSymbol[t,CHECK_DECLARED]
259 { PARSER_STATE->popScope();
260 // Do NOT call mkSort, since that creates a new sort!
261 // This name is not its own distinct sort, it's an alias.
262 PARSER_STATE->defineParameterizedType(name, sorts, t);
263 cmd->reset(new DefineSortCommand(name, sorts, t));
265 | /* function declaration */
266 DECLARE_FUN_TOK { PARSER_STATE->checkThatLogicIsSet(); }
267 symbol[name,CHECK_NONE,SYM_VARIABLE]
268 { PARSER_STATE->checkUserSymbol(name); }
269 LPAREN_TOK sortList[sorts] RPAREN_TOK
270 sortSymbol[t,CHECK_DECLARED]
271 { Trace("parser") << "declare fun: '" << name << "'" << std::endl;
272 if( !sorts.empty() ) {
273 t = PARSER_STATE->mkFlatFunctionType(sorts, t);
277 PARSER_STATE->checkLogicAllowsFunctions();
279 // we allow overloading for function declarations
280 if( PARSER_STATE->sygus() )
282 PARSER_STATE->parseError("declare-fun are not allowed in sygus "
288 PARSER_STATE->bindVar(name, t, true);
289 cmd->reset(new DeclareFunctionCommand(name, func, t));
292 | /* function definition */
293 DEFINE_FUN_TOK { PARSER_STATE->checkThatLogicIsSet(); }
294 symbol[name,CHECK_UNDECLARED,SYM_VARIABLE]
295 { PARSER_STATE->checkUserSymbol(name); }
296 LPAREN_TOK sortedVarList[sortedVarNames] RPAREN_TOK
297 sortSymbol[t,CHECK_DECLARED]
298 { /* add variables to parser state before parsing term */
299 Trace("parser") << "define fun: '" << name << "'" << std::endl;
300 if( sortedVarNames.size() > 0 ) {
301 sorts.reserve(sortedVarNames.size());
302 for(std::vector<std::pair<std::string, cvc5::Sort> >::const_iterator i =
303 sortedVarNames.begin(), iend = sortedVarNames.end();
306 sorts.push_back((*i).second);
310 t = PARSER_STATE->mkFlatFunctionType(sorts, t, flattenVars);
313 t = t.getFunctionCodomainSort();
315 if (sortedVarNames.size() > 0)
317 PARSER_STATE->pushScope();
319 terms = PARSER_STATE->bindBoundVars(sortedVarNames);
323 if( !flattenVars.empty() ){
324 // if this function has any implicit variables flattenVars,
325 // we apply the body of the definition to the flatten vars
326 expr = PARSER_STATE->mkHoApply(expr, flattenVars);
327 terms.insert(terms.end(), flattenVars.begin(), flattenVars.end());
329 if (sortedVarNames.size() > 0)
331 PARSER_STATE->popScope();
333 cmd->reset(new DefineFunctionCommand(name, terms, t, expr));
335 | DECLARE_DATATYPE_TOK datatypeDefCommand[false, cmd]
336 | DECLARE_DATATYPES_TOK datatypesDefCommand[false, cmd]
340 PARSER_STATE->checkThatLogicIsSet();
341 // bind all symbols specific to the model, e.g. uninterpreted constant
343 PARSER_STATE->pushGetValueScope();
345 ( LPAREN_TOK termList[terms,expr] RPAREN_TOK
346 { cmd->reset(new GetValueCommand(terms)); }
348 { PARSER_STATE->parseError("The get-value command expects a list of "
349 "terms. Perhaps you forgot a pair of "
353 { PARSER_STATE->popScope(); }
354 | /* get-assignment */
355 GET_ASSIGNMENT_TOK { PARSER_STATE->checkThatLogicIsSet(); }
356 { cmd->reset(new GetAssignmentCommand()); }
358 ASSERT_TOK { PARSER_STATE->checkThatLogicIsSet(); }
359 { PARSER_STATE->clearLastNamedTerm(); }
361 { cmd->reset(new AssertCommand(expr));
362 if (PARSER_STATE->lastNamedTerm().first == expr)
364 // set the expression name, if there was a named term
365 std::pair<cvc5::Term, std::string> namedTerm =
366 PARSER_STATE->lastNamedTerm();
367 SYM_MAN->setExpressionName(namedTerm.first, namedTerm.second, true);
371 CHECK_SAT_TOK { PARSER_STATE->checkThatLogicIsSet(); }
373 if (PARSER_STATE->sygus()) {
374 PARSER_STATE->parseError("Sygus does not support check-sat command.");
376 cmd->reset(new CheckSatCommand());
378 | /* check-sat-assuming */
379 CHECK_SAT_ASSUMING_TOK { PARSER_STATE->checkThatLogicIsSet(); }
380 ( LPAREN_TOK termList[terms,expr] RPAREN_TOK
382 cmd->reset(new CheckSatAssumingCommand(terms));
385 { PARSER_STATE->parseError("The check-sat-assuming command expects a "
386 "list of terms. Perhaps you forgot a pair of "
390 | /* get-assertions */
391 GET_ASSERTIONS_TOK { PARSER_STATE->checkThatLogicIsSet(); }
392 { cmd->reset(new GetAssertionsCommand()); }
394 GET_PROOF_TOK { PARSER_STATE->checkThatLogicIsSet(); }
395 { cmd->reset(new GetProofCommand()); }
396 | /* get-unsat-assumptions */
397 GET_UNSAT_ASSUMPTIONS_TOK { PARSER_STATE->checkThatLogicIsSet(); }
398 { cmd->reset(new GetUnsatAssumptionsCommand); }
399 | /* get-unsat-core */
400 GET_UNSAT_CORE_TOK { PARSER_STATE->checkThatLogicIsSet(); }
401 { cmd->reset(new GetUnsatCoreCommand); }
402 | /* get-difficulty */
403 GET_DIFFICULTY_TOK { PARSER_STATE->checkThatLogicIsSet(); }
404 { cmd->reset(new GetDifficultyCommand); }
405 | /* get-learned-literals */
406 GET_LEARNED_LITERALS_TOK { PARSER_STATE->checkThatLogicIsSet(); }
407 { cmd->reset(new GetLearnedLiteralsCommand); }
409 PUSH_TOK { PARSER_STATE->checkThatLogicIsSet(); }
411 { unsigned num = AntlrInput::tokenToUnsigned(k);
413 cmd->reset(new EmptyCommand());
414 } else if(num == 1) {
415 PARSER_STATE->pushScope(true);
416 cmd->reset(new PushCommand());
418 std::unique_ptr<CommandSequence> seq(new CommandSequence());
420 PARSER_STATE->pushScope(true);
421 Command* push_cmd = new PushCommand();
422 push_cmd->setMuted(num > 1);
423 seq->addCommand(push_cmd);
426 cmd->reset(seq.release());
429 | { if(PARSER_STATE->strictModeEnabled()) {
430 PARSER_STATE->parseError(
431 "Strict compliance mode demands an integer to be provided to "
432 "PUSH. Maybe you want (push 1)?");
434 PARSER_STATE->pushScope(true);
435 cmd->reset(new PushCommand());
438 | POP_TOK { PARSER_STATE->checkThatLogicIsSet(); }
440 { unsigned num = AntlrInput::tokenToUnsigned(k);
441 // we don't compare num to PARSER_STATE->scopeLevel() here, since
442 // when global declarations is true, the scope level of the parser
443 // is not indicative of the context level.
445 cmd->reset(new EmptyCommand());
446 } else if(num == 1) {
447 PARSER_STATE->popScope();
448 cmd->reset(new PopCommand());
450 std::unique_ptr<CommandSequence> seq(new CommandSequence());
452 PARSER_STATE->popScope();
453 Command* pop_command = new PopCommand();
454 pop_command->setMuted(num > 1);
455 seq->addCommand(pop_command);
458 cmd->reset(seq.release());
461 | { if(PARSER_STATE->strictModeEnabled()) {
462 PARSER_STATE->parseError(
463 "Strict compliance mode demands an integer to be provided to POP."
464 "Maybe you want (pop 1)?");
466 PARSER_STATE->popScope();
467 cmd->reset(new PopCommand());
473 { cmd->reset(new QuitCommand()); }
475 /* New SMT-LIB 2.5 command set */
478 /* cvc5-extended SMT-LIB commands */
479 | extendedCommand[cmd]
480 { if(PARSER_STATE->strictModeEnabled()) {
481 PARSER_STATE->parseError(
482 "Extended commands are not permitted while operating in strict "
489 { std::string id = AntlrInput::tokenText($SIMPLE_SYMBOL);
490 if(id == "benchmark") {
491 PARSER_STATE->parseError(
492 "In SMT-LIBv2 mode, but got something that looks like SMT-LIBv1, "
493 "which is not supported anymore.");
495 PARSER_STATE->parseError("expected SMT-LIBv2 command, got `" + id +
501 sygusCommand returns [std::unique_ptr<cvc5::Command> cmd]
503 cvc5::Term expr, expr2, fun;
505 std::vector<std::string> names;
506 std::vector<std::pair<std::string, cvc5::Sort> > sortedVarNames;
507 std::vector<cvc5::Term> sygusVars;
511 cvc5::Grammar* grammar = nullptr;
514 DECLARE_VAR_TOK { PARSER_STATE->checkThatLogicIsSet(); }
515 symbol[name,CHECK_UNDECLARED,SYM_VARIABLE]
516 { PARSER_STATE->checkUserSymbol(name); }
517 sortSymbol[t,CHECK_DECLARED]
519 cvc5::Term var = SOLVER->declareSygusVar(name, t);
520 PARSER_STATE->defineVar(name, var);
521 cmd.reset(new DeclareSygusVarCommand(name, var, t));
524 ( SYNTH_FUN_TOK { isInv = false; }
525 | SYNTH_INV_TOK { isInv = true; range = SOLVER->getBooleanSort(); }
527 { PARSER_STATE->checkThatLogicIsSet(); }
528 symbol[name,CHECK_UNDECLARED,SYM_VARIABLE]
529 LPAREN_TOK sortedVarList[sortedVarNames] RPAREN_TOK
530 ( sortSymbol[range,CHECK_DECLARED] )?
532 PARSER_STATE->pushScope();
533 sygusVars = PARSER_STATE->bindBoundVars(sortedVarNames);
536 // optionally, read the sygus grammar
538 // `grammar` specifies the required grammar for the function to
539 // synthesize, expressed as a type
540 sygusGrammar[grammar, sygusVars, name]
543 Trace("parser-sygus") << "Define synth fun : " << name << std::endl;
545 fun = isInv ? (grammar == nullptr
546 ? SOLVER->synthInv(name, sygusVars)
547 : SOLVER->synthInv(name, sygusVars, *grammar))
548 : (grammar == nullptr
549 ? SOLVER->synthFun(name, sygusVars, range)
550 : SOLVER->synthFun(name, sygusVars, range, *grammar));
552 Trace("parser-sygus") << "...read synth fun " << name << std::endl;
553 PARSER_STATE->popScope();
554 // we do not allow overloading for synth fun
555 PARSER_STATE->defineVar(name, fun);
556 cmd = std::unique_ptr<Command>(
557 new SynthFunCommand(name, fun, sygusVars, range, isInv, grammar));
560 ( CONSTRAINT_TOK { isAssume = false; } | ASSUME_TOK { isAssume = true; } )
562 PARSER_STATE->checkThatLogicIsSet();
565 { Trace("parser-sygus") << "...read constraint " << expr << std::endl;
566 cmd.reset(new SygusConstraintCommand(expr, isAssume));
568 | /* inv-constraint */
570 ( symbol[name,CHECK_NONE,SYM_VARIABLE] { names.push_back(name); } )+
572 cmd = PARSER_STATE->invConstraint(names);
577 PARSER_STATE->checkThatLogicIsSet();
578 cmd.reset(new CheckSynthCommand());
580 | /* check-synth-next */
583 PARSER_STATE->checkThatLogicIsSet();
584 cmd.reset(new CheckSynthCommand(true));
587 SET_FEATURE_TOK keyword[name] symbolicExpr[expr]
589 PARSER_STATE->checkThatLogicIsSet();
590 // ":grammars" is defined in the SyGuS version 2.1 standard and is by
591 // default supported, all other features are not.
592 if (name != ":grammars")
594 std::stringstream ss;
595 ss << "SyGuS feature " << name << " not currently supported";
596 PARSER_STATE->warning(ss.str());
598 cmd.reset(new EmptyCommand());
604 /** Reads a sygus grammar in the sygus version 2 format
606 * The resulting sygus datatype encoding the grammar is stored in ret.
607 * The argument sygusVars indicates the sygus bound variable list, which is
608 * the argument list of the function-to-synthesize (or null if the grammar
609 * has bound variables).
610 * The argument fun is a unique identifier to avoid naming clashes for the
611 * datatypes constructed by this call.
613 sygusGrammar[cvc5::Grammar*& ret,
614 const std::vector<cvc5::Term>& sygusVars,
615 const std::string& fun]
618 // the pre-declaration
619 std::vector<std::pair<std::string, cvc5::Sort>> sortedVarNames;
620 // non-terminal symbols of the grammar
621 std::vector<cvc5::Term> ntSyms;
625 unsigned dtProcessed = 0;
630 // We read a sorted variable list here in a custom way that throws an
631 // error to recognize if the user is using the (deprecated) version 1.0
633 ( LPAREN_TOK symbol[name,CHECK_NONE,SYM_VARIABLE]
634 sortSymbol[t,CHECK_DECLARED] (
635 // SyGuS version 1.0 expects a grammar ((Start Int ( ...
636 // SyGuS version 2.0 expects a predeclaration ((Start Int) ...
639 std::stringstream sse;
640 if (sortedVarNames.empty())
642 sse << "The expected SyGuS language is version 2.0, whereas the "
643 << "input appears to be SyGuS version 1.0 format. The version "
644 << "2.0 format requires a predeclaration of the non-terminal "
645 << "symbols of the grammar to be given prior to the definition "
646 << "of the grammar. See https://sygus.org/language/ for details "
647 << "and examples. cvc5 versions past 1.8 do not support SyGuS "
652 // an unknown syntax error
653 sse << "Unexpected syntax for SyGuS predeclaration.";
655 PARSER_STATE->parseError(sse.str().c_str());
658 { sortedVarNames.push_back(make_pair(name, t)); }
662 // non-terminal symbols in the pre-declaration are locally scoped
663 PARSER_STATE->pushScope();
664 for (std::pair<std::string, cvc5::Sort>& i : sortedVarNames)
666 PARSER_STATE->checkDeclaration(name, CHECK_UNDECLARED, SYM_SORT);
667 // make the non-terminal symbol, which will be parsed as an ordinary
669 cvc5::Term nts = PARSER_STATE->bindBoundVar(i.first, i.second);
670 ntSyms.push_back(nts);
672 ret = PARSER_STATE->mkGrammar(sygusVars, ntSyms);
674 // the grouped rule listing
678 symbol[name, CHECK_DECLARED, SYM_VARIABLE] sortSymbol[t, CHECK_DECLARED]
680 // check that it matches sortedVarNames
681 if (sortedVarNames[dtProcessed].first != name)
683 std::stringstream sse;
684 sse << "Grouped rule listing " << name
685 << " does not match the name (in order) from the predeclaration ("
686 << sortedVarNames[dtProcessed].first << ")." << std::endl;
687 PARSER_STATE->parseError(sse.str().c_str());
689 if (sortedVarNames[dtProcessed].second != t)
691 std::stringstream sse;
692 sse << "Type for grouped rule listing " << name
693 << " does not match the type (in order) from the predeclaration ("
694 << sortedVarNames[dtProcessed].second << ")." << std::endl;
695 PARSER_STATE->parseError(sse.str().c_str());
701 // add term as constructor to datatype
702 ret->addRule(ntSyms[dtProcessed], e);
704 | LPAREN_TOK SYGUS_CONSTANT_TOK sortSymbol[t, CHECK_DECLARED] RPAREN_TOK {
705 // allow constants in datatype for ntSyms[dtProcessed]
706 ret->addAnyConstant(ntSyms[dtProcessed]);
708 | LPAREN_TOK SYGUS_VARIABLE_TOK sortSymbol[t, CHECK_DECLARED] RPAREN_TOK {
709 // add variable constructors to datatype
710 ret->addAnyVariable(ntSyms[dtProcessed]);
721 // pop scope from the pre-declaration
722 PARSER_STATE->popScope();
726 setInfoInternal[std::unique_ptr<cvc5::Command>* cmd]
731 : keyword[name] symbolicExpr[sexpr]
732 { cmd->reset(new SetInfoCommand(name.c_str() + 1, sexprToString(sexpr))); }
735 setOptionInternal[std::unique_ptr<cvc5::Command>* cmd]
740 : keyword[name] symbolicExpr[sexpr]
741 { cmd->reset(new SetOptionCommand(name.c_str() + 1, sexprToString(sexpr)));
742 // Ugly that this changes the state of the parser; but
743 // global-declarations affects parsing, so we can't hold off
744 // on this until some SolverEngine eventually (if ever) executes it.
745 if(name == ":global-declarations")
747 SYM_MAN->setGlobalDeclarations(sexprToString(sexpr) == "true");
752 smt25Command[std::unique_ptr<cvc5::Command>* cmd]
756 cvc5::Term expr, expr2;
757 std::vector<std::pair<std::string, cvc5::Sort> > sortedVarNames;
761 std::vector<cvc5::Term> bvs;
762 std::vector<std::vector<std::pair<std::string, cvc5::Sort>>>
764 std::vector<std::vector<cvc5::Term>> flattenVarsList;
765 std::vector<std::vector<cvc5::Term>> formals;
766 std::vector<cvc5::Term> funcs;
767 std::vector<cvc5::Term> func_defs;
769 std::unique_ptr<cvc5::CommandSequence> seq;
770 std::vector<cvc5::Sort> sorts;
771 std::vector<cvc5::Term> flattenVars;
774 : DECLARE_CONST_TOK { PARSER_STATE->checkThatLogicIsSet(); }
775 symbol[name,CHECK_NONE,SYM_VARIABLE]
776 { PARSER_STATE->checkUserSymbol(name); }
777 sortSymbol[t,CHECK_DECLARED]
778 { // allow overloading here
779 if( PARSER_STATE->sygus() )
781 PARSER_STATE->parseError("declare-const is not allowed in sygus "
785 PARSER_STATE->bindVar(name, t, true);
786 cmd->reset(new DeclareFunctionCommand(name, c, t)); }
789 | GET_MODEL_TOK { PARSER_STATE->checkThatLogicIsSet(); }
790 { cmd->reset(new GetModelCommand()); }
795 { cmd->reset(new EchoCommand(s)); }
796 | { cmd->reset(new EchoCommand()); }
799 /* reset: reset everything, returning solver to initial state.
800 * Logic and options must be set again. */
803 cmd->reset(new ResetCommand());
804 // reset the state of the parser, which is independent of the symbol
806 PARSER_STATE->reset();
808 /* reset-assertions: reset assertions, assertion stack, declarations,
809 * etc., but the logic and options remain as they were. */
810 | RESET_ASSERTIONS_TOK
811 { cmd->reset(new ResetAssertionsCommand());
814 { PARSER_STATE->checkThatLogicIsSet(); }
815 symbol[fname,CHECK_NONE,SYM_VARIABLE]
816 { PARSER_STATE->checkUserSymbol(fname); }
817 LPAREN_TOK sortedVarList[sortedVarNames] RPAREN_TOK
818 sortSymbol[t,CHECK_DECLARED]
821 PARSER_STATE->bindDefineFunRec(fname, sortedVarNames, t, flattenVars);
822 PARSER_STATE->pushDefineFunRecScope(
823 sortedVarNames, func, flattenVars, bvs);
826 { PARSER_STATE->popScope();
827 if( !flattenVars.empty() ){
828 expr = PARSER_STATE->mkHoApply( expr, flattenVars );
830 cmd->reset(new DefineFunctionRecCommand(func, bvs, expr));
832 | DEFINE_FUNS_REC_TOK
833 { PARSER_STATE->checkThatLogicIsSet();}
836 symbol[fname,CHECK_UNDECLARED,SYM_VARIABLE]
837 { PARSER_STATE->checkUserSymbol(fname); }
838 LPAREN_TOK sortedVarList[sortedVarNames] RPAREN_TOK
839 sortSymbol[t,CHECK_DECLARED]
842 func = PARSER_STATE->bindDefineFunRec(
843 fname, sortedVarNames, t, flattenVars);
844 funcs.push_back( func );
846 // add to lists (need to remember for when parsing the bodies)
847 sortedVarNamesList.push_back( sortedVarNames );
848 flattenVarsList.push_back( flattenVars );
850 // set up parsing the next variable list block
851 sortedVarNames.clear();
859 //set up the first scope
860 if( sortedVarNamesList.empty() ){
861 PARSER_STATE->parseError("Must define at least one function in "
865 PARSER_STATE->pushDefineFunRecScope( sortedVarNamesList[0], funcs[0],
866 flattenVarsList[0], bvs);
871 unsigned j = func_defs.size();
872 if( !flattenVarsList[j].empty() ){
873 expr = PARSER_STATE->mkHoApply( expr, flattenVarsList[j] );
875 func_defs.push_back( expr );
876 formals.push_back(bvs);
878 //set up the next scope
879 PARSER_STATE->popScope();
880 if( func_defs.size()<funcs.size() ){
882 PARSER_STATE->pushDefineFunRecScope( sortedVarNamesList[j], funcs[j],
883 flattenVarsList[j], bvs);
888 { if( funcs.size()!=func_defs.size() ){
889 PARSER_STATE->parseError(std::string(
890 "Number of functions defined does not match number listed in "
893 cmd->reset(new DefineFunctionRecCommand(funcs, formals, func_defs));
897 extendedCommand[std::unique_ptr<cvc5::Command>* cmd]
899 std::vector<cvc5::DatatypeDecl> dts;
903 std::vector<std::string> names;
904 std::vector<cvc5::Term> terms;
905 std::vector<cvc5::Sort> sorts;
906 std::vector<std::pair<std::string, cvc5::Sort> > sortedVarNames;
907 std::unique_ptr<cvc5::CommandSequence> seq;
908 cvc5::Grammar* g = nullptr;
910 /* Extended SMT-LIB set of commands syntax, not permitted in
911 * --smtlib2 compliance mode. */
912 : DECLARE_CODATATYPE_TOK datatypeDefCommand[true, cmd]
913 | DECLARE_CODATATYPES_TOK datatypesDefCommand[true, cmd]
915 /* Support some of Z3's extended SMT-LIB commands */
919 PARSER_STATE->checkThatLogicIsSet();
920 PARSER_STATE->checkLogicAllowsFreeSorts();
921 seq.reset(new cvc5::CommandSequence());
924 ( symbol[name,CHECK_UNDECLARED,SYM_SORT]
925 { PARSER_STATE->checkUserSymbol(name);
926 cvc5::Sort type = PARSER_STATE->mkSort(name);
927 seq->addCommand(new DeclareSortCommand(name, 0, type));
931 { cmd->reset(seq.release()); }
933 | DECLARE_FUNS_TOK { PARSER_STATE->checkThatLogicIsSet(); }
934 { seq.reset(new cvc5::CommandSequence()); }
936 ( LPAREN_TOK symbol[name,CHECK_UNDECLARED,SYM_VARIABLE]
937 { PARSER_STATE->checkUserSymbol(name); }
938 nonemptySortList[sorts] RPAREN_TOK
940 if(sorts.size() > 1) {
941 PARSER_STATE->checkLogicAllowsFunctions();
943 cvc5::Sort range = sorts.back();
945 tt = PARSER_STATE->mkFlatFunctionType(sorts, range);
951 PARSER_STATE->bindVar(name, tt, true);
952 seq->addCommand(new DeclareFunctionCommand(name, func, tt));
957 { cmd->reset(seq.release()); }
958 | DECLARE_PREDS_TOK { PARSER_STATE->checkThatLogicIsSet(); }
959 { seq.reset(new cvc5::CommandSequence()); }
961 ( LPAREN_TOK symbol[name,CHECK_UNDECLARED,SYM_VARIABLE]
962 { PARSER_STATE->checkUserSymbol(name); }
963 sortList[sorts] RPAREN_TOK
964 { t = SOLVER->getBooleanSort();
965 if(sorts.size() > 0) {
966 PARSER_STATE->checkLogicAllowsFunctions();
967 t = SOLVER->mkFunctionSort(sorts, t);
971 PARSER_STATE->bindVar(name, t, true);
972 seq->addCommand(new DeclareFunctionCommand(name, func, t));
977 { cmd->reset(seq.release()); }
978 | // (define-const x U t)
979 DEFINE_CONST_TOK { PARSER_STATE->checkThatLogicIsSet(); }
980 symbol[name,CHECK_UNDECLARED,SYM_VARIABLE]
981 { PARSER_STATE->checkUserSymbol(name); }
982 sortSymbol[t,CHECK_DECLARED]
985 // declare the name down here (while parsing term, signature
986 // must not be extended with the name itself; no recursion
988 cmd->reset(new DefineFunctionCommand(name, t, e));
991 | SIMPLIFY_TOK { PARSER_STATE->checkThatLogicIsSet(); }
993 { cmd->reset(new SimplifyCommand(e)); }
994 | GET_QE_TOK { PARSER_STATE->checkThatLogicIsSet(); }
996 { cmd->reset(new GetQuantifierEliminationCommand(e, true)); }
997 | GET_QE_DISJUNCT_TOK { PARSER_STATE->checkThatLogicIsSet(); }
999 { cmd->reset(new GetQuantifierEliminationCommand(e, false)); }
1001 PARSER_STATE->checkThatLogicIsSet();
1003 symbol[name,CHECK_UNDECLARED,SYM_VARIABLE]
1006 sygusGrammar[g, terms, name]
1009 cmd->reset(new GetAbductCommand(name, e, g));
1011 | GET_ABDUCT_NEXT_TOK {
1012 PARSER_STATE->checkThatLogicIsSet();
1013 cmd->reset(new GetAbductNextCommand);
1015 | GET_INTERPOL_TOK {
1016 PARSER_STATE->checkThatLogicIsSet();
1018 symbol[name,CHECK_UNDECLARED,SYM_VARIABLE]
1021 sygusGrammar[g, terms, name]
1024 cmd->reset(new GetInterpolantCommand(name, e, g));
1026 | GET_INTERPOL_NEXT_TOK {
1027 PARSER_STATE->checkThatLogicIsSet();
1028 cmd->reset(new GetInterpolantNextCommand);
1030 | DECLARE_HEAP LPAREN_TOK
1031 sortSymbol[t, CHECK_DECLARED]
1032 sortSymbol[s, CHECK_DECLARED]
1033 { cmd->reset(new DeclareHeapCommand(t, s)); }
1035 | DECLARE_POOL { PARSER_STATE->checkThatLogicIsSet(); }
1036 symbol[name,CHECK_NONE,SYM_VARIABLE]
1037 { PARSER_STATE->checkUserSymbol(name); }
1038 sortSymbol[t,CHECK_DECLARED]
1041 { terms.push_back( e ); }
1043 { Trace("parser") << "declare pool: '" << name << "'" << std::endl;
1044 cvc5::Term pool = SOLVER->declarePool(name, t, terms);
1045 PARSER_STATE->defineVar(name, pool);
1046 cmd->reset(new DeclarePoolCommand(name, pool, t, terms));
1048 | BLOCK_MODEL_TOK KEYWORD { PARSER_STATE->checkThatLogicIsSet(); }
1050 modes::BlockModelsMode mode =
1051 PARSER_STATE->getBlockModelsMode(
1052 AntlrInput::tokenText($KEYWORD).c_str() + 1);
1053 cmd->reset(new BlockModelCommand(mode));
1055 | BLOCK_MODEL_VALUES_TOK { PARSER_STATE->checkThatLogicIsSet(); }
1056 ( LPAREN_TOK termList[terms,e] RPAREN_TOK
1057 { cmd->reset(new BlockModelValuesCommand(terms)); }
1059 { PARSER_STATE->parseError("The block-model-value command expects a list "
1060 "of terms. Perhaps you forgot a pair of "
1066 datatypeDefCommand[bool isCo, std::unique_ptr<cvc5::Command>* cmd]
1068 std::vector<cvc5::DatatypeDecl> dts;
1070 std::vector<std::string> dnames;
1071 std::vector<int> arities;
1073 : { PARSER_STATE->checkThatLogicIsSet(); }
1074 symbol[name,CHECK_UNDECLARED,SYM_SORT]
1076 dnames.push_back(name);
1077 arities.push_back(-1);
1079 datatypesDef[isCo, dnames, arities, cmd]
1082 datatypesDefCommand[bool isCo, std::unique_ptr<cvc5::Command>* cmd]
1084 std::vector<cvc5::DatatypeDecl> dts;
1086 std::vector<std::string> dnames;
1087 std::vector<int> arities;
1089 : { PARSER_STATE->checkThatLogicIsSet(); }
1090 LPAREN_TOK /* datatype definition prelude */
1091 ( LPAREN_TOK symbol[name,CHECK_UNDECLARED,SYM_SORT] n=INTEGER_LITERAL RPAREN_TOK
1092 { unsigned arity = AntlrInput::tokenToUnsigned(n);
1093 Trace("parser-dt") << "Datatype : " << name << ", arity = " << arity << std::endl;
1094 dnames.push_back(name);
1095 arities.push_back( static_cast<int>(arity) );
1100 datatypesDef[isCo, dnames, arities, cmd]
1105 * Read a list of datatype definitions for datatypes with names dnames and
1106 * parametric arities arities. A negative value in arities indicates that the
1107 * arity for the corresponding datatype has not been fixed: notice that we do
1108 * not know the arity of datatypes in the declare-datatype command prior to
1109 * parsing their body, whereas the arity of datatypes in declare-datatypes is
1110 * given in the preamble of that command and thus is known prior to this call.
1112 datatypesDef[bool isCo,
1113 const std::vector<std::string>& dnames,
1114 const std::vector<int>& arities,
1115 std::unique_ptr<cvc5::Command>* cmd]
1117 std::vector<cvc5::DatatypeDecl> dts;
1119 std::vector<cvc5::Sort> params;
1121 : { PARSER_STATE->pushScope();
1122 // Declare the datatypes that are currently being defined as unresolved
1123 // types. If we do not know the arity of the datatype yet, we wait to
1124 // define it until parsing the preamble of its body, which may optionally
1125 // involve `par`. This is limited to the case of single datatypes defined
1126 // via declare-datatype, and hence no datatype body is parsed without
1127 // having all types declared. This ensures we can parse datatypes with
1128 // nested recursion, e.g. datatypes D having a subfield type
1130 for (unsigned i=0, dsize=dnames.size(); i<dsize; i++)
1134 // do not know the arity yet
1137 unsigned arity = static_cast<unsigned>(arities[i]);
1138 PARSER_STATE->mkUnresolvedType(dnames[i], arity);
1143 Trace("parser-dt") << "Processing datatype #" << dts.size() << std::endl;
1144 if( dts.size()>=dnames.size() ){
1145 PARSER_STATE->parseError("Too many datatypes defined in this block.");
1148 ( PAR_TOK { PARSER_STATE->pushScope(); } LPAREN_TOK
1149 ( symbol[name,CHECK_UNDECLARED,SYM_SORT]
1151 params.push_back( PARSER_STATE->mkSort(name)); }
1154 // if the arity was fixed by prelude and is not equal to the number of parameters
1155 if( arities[dts.size()]>=0 && static_cast<int>(params.size())!=arities[dts.size()] ){
1156 PARSER_STATE->parseError("Wrong number of parameters for datatype.");
1158 if (arities[dts.size()]<0)
1160 // now declare it as an unresolved type
1161 PARSER_STATE->mkUnresolvedType(dnames[dts.size()], params.size());
1163 Trace("parser-dt") << params.size() << " parameters for " << dnames[dts.size()] << std::endl;
1164 dts.push_back(SOLVER->mkDatatypeDecl(dnames[dts.size()], params, isCo));
1167 ( LPAREN_TOK constructorDef[dts.back()] RPAREN_TOK )+
1168 RPAREN_TOK { PARSER_STATE->popScope(); }
1169 | { // if the arity was fixed by prelude and is not equal to 0
1170 if( arities[dts.size()]>0 ){
1171 PARSER_STATE->parseError("No parameters given for datatype.");
1173 else if (arities[dts.size()]<0)
1175 // now declare it as an unresolved type
1176 PARSER_STATE->mkUnresolvedType(dnames[dts.size()], 0);
1178 Trace("parser-dt") << params.size() << " parameters for " << dnames[dts.size()] << std::endl;
1179 dts.push_back(SOLVER->mkDatatypeDecl(dnames[dts.size()],
1183 ( LPAREN_TOK constructorDef[dts.back()] RPAREN_TOK )+
1188 if (dts.size() != dnames.size())
1190 PARSER_STATE->parseError("Wrong number of datatypes provided.");
1192 PARSER_STATE->popScope();
1193 cmd->reset(new DatatypeDeclarationCommand(
1194 PARSER_STATE->bindMutualDatatypeTypes(dts, true)));
1198 simpleSymbolicExprNoKeyword[std::string& s]
1200 { s = AntlrInput::tokenText($INTEGER_LITERAL); }
1202 { s = AntlrInput::tokenText($DECIMAL_LITERAL); }
1204 { s = AntlrInput::tokenText($HEX_LITERAL); }
1206 { s = AntlrInput::tokenText($BINARY_LITERAL); }
1208 { s = AntlrInput::tokenText($SIMPLE_SYMBOL); }
1210 { s = AntlrInput::tokenText($QUOTED_SYMBOL); }
1212 { s = AntlrInput::tokenText($STRING_LITERAL); }
1213 | tok=(ASSERT_TOK | CHECK_SAT_TOK | CHECK_SAT_ASSUMING_TOK | DECLARE_FUN_TOK
1215 | DEFINE_FUN_TOK | DEFINE_FUN_REC_TOK | DEFINE_FUNS_REC_TOK
1216 | DEFINE_SORT_TOK | GET_VALUE_TOK | GET_ASSIGNMENT_TOK
1217 | GET_ASSERTIONS_TOK | GET_PROOF_TOK | GET_UNSAT_ASSUMPTIONS_TOK
1218 | GET_UNSAT_CORE_TOK | GET_DIFFICULTY_TOK | EXIT_TOK
1219 | RESET_TOK | RESET_ASSERTIONS_TOK | SET_LOGIC_TOK | SET_INFO_TOK
1220 | GET_INFO_TOK | SET_OPTION_TOK | GET_OPTION_TOK | PUSH_TOK | POP_TOK
1221 | DECLARE_DATATYPES_TOK | GET_MODEL_TOK | ECHO_TOK | SIMPLIFY_TOK)
1222 { s = AntlrInput::tokenText($tok); }
1225 keyword[std::string& s]
1227 { s = AntlrInput::tokenText($KEYWORD); }
1230 simpleSymbolicExpr[std::string& s]
1231 : simpleSymbolicExprNoKeyword[s]
1232 | KEYWORD { s = AntlrInput::tokenText($KEYWORD); }
1235 symbolicExpr[cvc5::Term& sexpr]
1238 std::vector<cvc5::Term> children;
1240 : simpleSymbolicExpr[s]
1241 { sexpr = SOLVER->mkString(PARSER_STATE->processAdHocStringEsc(s)); }
1243 ( symbolicExpr[sexpr] { children.push_back(sexpr); } )* RPAREN_TOK
1244 { sexpr = SOLVER->mkTerm(cvc5::SEXPR, children); }
1249 * @return the expression representing the term.
1251 term[cvc5::Term& expr, cvc5::Term& expr2]
1253 cvc5::Kind kind = cvc5::NULL_TERM;
1259 : termNonVariable[expr, expr2]
1261 // a qualified identifier (section 3.6 of SMT-LIB version 2.6)
1265 expr = PARSER_STATE->parseOpToExpr(p);
1270 * Matches a non-variable term.
1271 * @return the expression expr representing the term or formula, and expr2, an
1272 * optional annotation for expr (for instance, for attributed expressions).
1274 termNonVariable[cvc5::Term& expr, cvc5::Term& expr2]
1276 Trace("parser") << "term: " << AntlrInput::tokenText(LT(1)) << std::endl;
1277 cvc5::Kind kind = cvc5::NULL_TERM;
1279 std::vector<cvc5::Term> args;
1280 std::vector< std::pair<std::string, cvc5::Sort> > sortedVarNames;
1282 cvc5::Term f, f2, f3;
1285 std::vector<cvc5::Term> patexprs;
1286 std::vector<cvc5::Term> matchcases;
1287 std::unordered_set<std::string> names;
1288 std::vector< std::pair<std::string, cvc5::Term> > binders;
1291 cvc5::Term atomTerm;
1293 std::vector<cvc5::Sort> argTypes;
1295 : LPAREN_TOK quantOp[kind]
1297 if (!PARSER_STATE->isTheoryEnabled(internal::theory::THEORY_QUANTIFIERS))
1299 PARSER_STATE->parseError("Quantifier used in non-quantified logic.");
1301 PARSER_STATE->pushScope();
1304 term[f, f2] RPAREN_TOK
1306 args.push_back(bvl);
1308 PARSER_STATE->popScope();
1313 expr = MK_TERM(kind, args);
1315 | LPAREN_TOK SET_COMPREHENSION_TOK
1316 { PARSER_STATE->pushScope(); }
1319 args.push_back(bvl);
1321 term[f, f2] { args.push_back(f); }
1324 expr = MK_TERM(cvc5::SET_COMPREHENSION, args);
1327 | LPAREN_TOK qualIdentifier[p]
1328 termList[args,expr] RPAREN_TOK
1330 expr = PARSER_STATE->applyParseOp(p, args);
1332 | /* a let or sygus let binding */
1335 { PARSER_STATE->pushScope(); }
1336 ( LPAREN_TOK symbol[name,CHECK_NONE,SYM_VARIABLE]
1339 // this is a parallel let, so we have to save up all the contributions
1340 // of the let and define them only later on
1341 { if(names.count(name) == 1) {
1342 std::stringstream ss;
1343 ss << "warning: symbol `" << name << "' bound multiple times by let;"
1344 << " the last binding will be used, shadowing earlier ones";
1345 PARSER_STATE->warning(ss.str());
1349 binders.push_back(std::make_pair(name, expr)); } )+
1350 { // now implement these bindings
1351 for (const std::pair<std::string, cvc5::Term>& binder : binders)
1354 PARSER_STATE->defineVar(binder.first, binder.second);
1361 { PARSER_STATE->popScope(); }
1362 | /* match expression */
1363 LPAREN_TOK MATCH_TOK term[expr, f2] {
1364 if( !expr.getSort().isDatatype() ){
1365 PARSER_STATE->parseError("Cannot match on non-datatype term.");
1370 // case with non-nullary pattern
1371 LPAREN_TOK LPAREN_TOK term[f, f2] {
1373 PARSER_STATE->pushScope();
1374 // f should be a constructor
1376 Trace("parser-dt") << "Pattern head : " << f << " " << type << std::endl;
1377 if (!type.isDatatypeConstructor())
1379 PARSER_STATE->parseError("Pattern must be application of a constructor or a variable.");
1382 type.getDatatypeConstructorCodomainSort().getDatatype();
1383 if (dt.isParametric())
1385 // lookup constructor by name
1386 cvc5::DatatypeConstructor dc = dt.getConstructor(f.toString());
1387 cvc5::Term scons = dc.getInstantiatedTerm(expr.getSort());
1388 // take the type of the specialized constructor instead
1389 type = scons.getSort();
1391 argTypes = type.getDatatypeConstructorDomainSorts();
1393 // arguments of the pattern
1394 ( symbol[name,CHECK_NONE,SYM_VARIABLE] {
1395 if (args.size() >= argTypes.size())
1397 PARSER_STATE->parseError("Too many arguments for pattern.");
1399 //make of proper type
1400 cvc5::Term arg = PARSER_STATE->bindBoundVar(name, argTypes[args.size()]);
1401 args.push_back( arg );
1404 RPAREN_TOK term[f3, f2] {
1405 // make the match case
1406 std::vector<cvc5::Term> cargs;
1408 cargs.insert(cargs.end(),args.begin(),args.end());
1409 cvc5::Term c = MK_TERM(cvc5::APPLY_CONSTRUCTOR,cargs);
1410 cvc5::Term bvla = MK_TERM(cvc5::VARIABLE_LIST,args);
1411 cvc5::Term mc = MK_TERM(cvc5::MATCH_BIND_CASE, bvla, c, f3);
1412 matchcases.push_back(mc);
1413 // now, pop the scope
1414 PARSER_STATE->popScope();
1417 // case with nullary or variable pattern
1418 | LPAREN_TOK symbol[name,CHECK_NONE,SYM_VARIABLE] {
1419 if (PARSER_STATE->isDeclared(name,SYM_VARIABLE))
1421 f = PARSER_STATE->getVariable(name);
1423 if (!type.isDatatypeConstructor() ||
1424 !type.getDatatypeConstructorDomainSorts().empty())
1426 PARSER_STATE->parseError("Must apply constructors of arity greater than 0 to arguments in pattern.");
1428 // make nullary constructor application
1429 f = MK_TERM(cvc5::APPLY_CONSTRUCTOR, f);
1433 // it has the type of the head expr
1434 f = PARSER_STATE->bindBoundVar(name, expr.getSort());
1439 if (f.getKind() == cvc5::VARIABLE)
1441 cvc5::Term bvlf = MK_TERM(cvc5::VARIABLE_LIST, f);
1442 mc = MK_TERM(cvc5::MATCH_BIND_CASE, bvlf, f, f3);
1446 mc = MK_TERM(cvc5::MATCH_CASE, f, f3);
1448 matchcases.push_back(mc);
1452 RPAREN_TOK RPAREN_TOK {
1453 //now, make the match
1454 if (matchcases.empty())
1456 PARSER_STATE->parseError("Must have at least one case in match.");
1458 std::vector<cvc5::Term> mchildren;
1459 mchildren.push_back(expr);
1460 mchildren.insert(mchildren.end(), matchcases.begin(), matchcases.end());
1461 expr = MK_TERM(cvc5::MATCH, mchildren);
1464 /* attributed expressions */
1465 | LPAREN_TOK ATTRIBUTE_TOK term[expr, f2]
1466 ( attribute[expr, attexpr]
1467 { if( ! attexpr.isNull()) {
1468 patexprs.push_back( attexpr );
1473 if(! patexprs.empty()) {
1474 if( !f2.isNull() && f2.getKind()==cvc5::INST_PATTERN_LIST ){
1475 for( size_t i=0; i<f2.getNumChildren(); i++ ){
1476 patexprs.push_back( f2[i] );
1479 expr2 = MK_TERM(cvc5::INST_PATTERN_LIST, patexprs);
1485 LPAREN_TOK HO_LAMBDA_TOK
1486 { PARSER_STATE->pushScope(); }
1488 term[f, f2] RPAREN_TOK
1490 args.push_back(bvl);
1492 PARSER_STATE->popScope();
1493 expr = MK_TERM(cvc5::LAMBDA, args);
1495 | LPAREN_TOK TUPLE_CONST_TOK termList[args,expr] RPAREN_TOK
1497 std::vector<cvc5::Sort> sorts;
1498 std::vector<cvc5::Term> terms;
1499 for (const cvc5::Term& arg : args)
1501 sorts.emplace_back(arg.getSort());
1502 terms.emplace_back(arg);
1504 expr = SOLVER->mkTuple(sorts, terms);
1506 | LPAREN_TOK TUPLE_PROJECT_TOK term[expr,expr2] RPAREN_TOK
1508 std::vector<uint32_t> indices;
1509 cvc5::Op op = SOLVER->mkOp(cvc5::TUPLE_PROJECT, indices);
1510 expr = SOLVER->mkTerm(op, {expr});
1512 | /* an atomic term (a term with no subterms) */
1513 termAtomic[atomTerm] { expr = atomTerm; }
1518 * Matches a qualified identifier, which can be a combination of one or more of
1519 * the following, stored in the ParseOp utility class:
1521 * (2) A string name.
1522 * (3) An expression expr.
1525 * A qualified identifier is the generic case of function heads.
1526 * With respect to the standard definition (Section 3.6 of SMT-LIB version 2.6)
1527 * of qualified identifiers, we additionally parse:
1528 * - "Array constant specifications" of the form (as const (Array T1 T2)),
1529 * which notice are used as function heads e.g. ((as const (Array Int Int)) 0)
1530 * specifies the constant array over integers consisting of constant 0. This
1531 * is handled as if it were a special case of an operator here.
1537 * - For declared functions f, we return (2).
1538 * - For indexed functions like testers (_ is C) and bitvector extract
1539 * (_ extract n m), we return (3) for the appropriate operator.
1540 * - For tuple selectors (_ tuple_select n) and updaters (_ tuple_update n), we
1541 * return (1) and (3). cvc5::Kind is set to APPLY_SELECTOR or APPLY_UPDATER
1542 * respectively, and expr is set to n, which is to be interpreted by the
1543 * caller as the n^th generic tuple selector or updater. We do this since there
1544 * is no AST expression representing generic tuple select, and we do not have
1545 * enough type information at this point to know the type of the tuple we will
1546 * be selecting from.
1548 * (Ascripted Identifiers)
1550 * - For ascripted nullary parametric datatype constructors like
1551 * (as nil (List Int)), we return (APPLY_CONSTRUCTOR C) for the appropriate
1552 * specialized constructor C as (3).
1553 * - For ascripted non-nullary parametric datatype constructors like
1554 * (as cons (List Int)), we return the appropriate specialized constructor C
1556 * - Overloaded non-parametric constructors (as C T) return the appropriate
1557 * expression, analogous to the parametric cases above.
1558 * - For other ascripted nullary constants like (as set.empty (Set T)),
1559 * (as sep.nil T), we return the appropriate expression (3).
1560 * - For array constant specifications (as const (Array T1 T2)), we return (1)
1561 * and (4), where kind is set to STORE_ALL and type is set to (Array T1 T2),
1562 * where this is to be interpreted by the caller as converting the next parsed
1563 * constant of type T2 to an Array of type (Array T1 T2) over that constant.
1564 * - For ascriptions on normal symbols (as f T), we return the appropriate
1565 * expression (3), which may involve disambiguating f based on type T if it is
1568 qualIdentifier[cvc5::ParseOp& p]
1571 std::string baseName;
1577 ( CONST_TOK sortSymbol[type, CHECK_DECLARED]
1579 p.d_kind = cvc5::CONST_ARRAY;
1580 PARSER_STATE->parseOpApplyTypeAscription(p, type);
1583 sortSymbol[type, CHECK_DECLARED]
1585 PARSER_STATE->parseOpApplyTypeAscription(p, type);
1592 * Matches an identifier, which can be a combination of one or more of the
1593 * following, stored in the ParseOp utility class:
1595 * (2) A string name.
1596 * (3) An expression expr.
1597 * For examples, see documentation of qualIdentifier.
1599 identifier[cvc5::ParseOp& p]
1603 std::vector<uint32_t> numerals;
1606 : functionName[p.d_name, CHECK_NONE]
1608 // indexed functions
1610 | LPAREN_TOK INDEX_TOK
1611 ( TESTER_TOK term[f, f2]
1613 if (f.getKind() == cvc5::APPLY_CONSTRUCTOR && f.getNumChildren() == 1)
1615 // for nullary constructors, must get the operator
1618 if (!f.getSort().isDatatypeConstructor())
1620 PARSER_STATE->parseError(
1621 "Bad syntax for (_ is X), X must be a constructor.");
1623 // get the datatype that f belongs to
1624 cvc5::Sort sf = f.getSort().getDatatypeConstructorCodomainSort();
1625 cvc5::Datatype d = sf.getDatatype();
1627 cvc5::DatatypeConstructor dc = d.getConstructor(f.toString());
1628 p.d_expr = dc.getTesterTerm();
1630 | UPDATE_TOK term[f, f2]
1632 if (!f.getSort().isDatatypeSelector())
1634 PARSER_STATE->parseError(
1635 "Bad syntax for (_ update X), X must be a selector.");
1637 std::string sname = f.toString();
1638 // get the datatype that f belongs to
1639 cvc5::Sort sf = f.getSort().getDatatypeSelectorDomainSort();
1640 cvc5::Datatype d = sf.getDatatype();
1641 // find the selector
1642 cvc5::DatatypeSelector ds = d.getSelector(f.toString());
1643 // get the updater term
1644 p.d_expr = ds.getUpdaterTerm();
1646 | TUPLE_PROJECT_TOK nonemptyNumeralList[numerals]
1648 // we adopt a special syntax (_ tuple.project i_1 ... i_n) where
1649 // i_1, ..., i_n are numerals
1650 p.d_kind = cvc5::TUPLE_PROJECT;
1651 p.d_op = SOLVER->mkOp(cvc5::TUPLE_PROJECT, numerals);
1653 | functionName[opName, CHECK_NONE] nonemptyNumeralList[numerals]
1655 cvc5::Kind k = PARSER_STATE->getIndexedOpKind(opName);
1656 if (k == cvc5::UNDEFINED_KIND)
1658 // We don't know which kind to use until we know the type of the
1661 p.d_indices = numerals;
1662 p.d_kind = cvc5::UNDEFINED_KIND;
1664 else if (k == cvc5::APPLY_SELECTOR || k == cvc5::APPLY_UPDATER)
1666 // we adopt a special syntax (_ tuple_select n) and (_ tuple_update n)
1667 // for tuple selectors and updaters
1668 if (numerals.size() != 1)
1670 PARSER_STATE->parseError(
1671 "Unexpected syntax for tuple selector or updater.");
1673 // The operator is dependent upon inferring the type of the arguments,
1674 // and hence the type is not available yet. Hence, we remember the
1675 // index as a numeral in the parse operator.
1677 p.d_expr = SOLVER->mkInteger(numerals[0]);
1679 else if (numerals.size() == 1 || numerals.size() == 2)
1681 p.d_op = SOLVER->mkOp(k, numerals);
1685 PARSER_STATE->parseError(
1686 "Unexpected number of numerals for indexed symbol.");
1694 * Matches an atomic term (a term with no subterms).
1695 * @return the expression expr representing the term or formula.
1697 termAtomic[cvc5::Term& atomTerm]
1701 std::vector<uint32_t> numerals;
1706 std::string intStr = AntlrInput::tokenText($INTEGER_LITERAL);
1707 atomTerm = SOLVER->mkInteger(intStr);
1711 std::string realStr = AntlrInput::tokenText($DECIMAL_LITERAL);
1712 atomTerm = SOLVER->mkReal(realStr);
1715 // Constants using indexed identifiers, e.g. (_ +oo 8 24) (positive infinity
1716 // as a 32-bit floating-point constant)
1717 | LPAREN_TOK INDEX_TOK
1718 ( CHAR_TOK HEX_LITERAL
1720 std::string hexStr = AntlrInput::tokenTextSubstr($HEX_LITERAL, 2);
1721 atomTerm = PARSER_STATE->mkCharConstant(hexStr);
1723 | FMF_CARD_TOK sortSymbol[t,CHECK_DECLARED] INTEGER_LITERAL
1725 uint32_t ubound = AntlrInput::tokenToUnsigned($INTEGER_LITERAL);
1726 atomTerm = SOLVER->mkCardinalityConstraint(t, ubound);
1728 | sym=SIMPLE_SYMBOL nonemptyNumeralList[numerals]
1731 PARSER_STATE->mkIndexedConstant(AntlrInput::tokenText($sym),
1737 // Bit-vector constants
1740 Assert(AntlrInput::tokenText($HEX_LITERAL).find("#x") == 0);
1741 std::string hexStr = AntlrInput::tokenTextSubstr($HEX_LITERAL, 2);
1742 atomTerm = SOLVER->mkBitVector(hexStr.size() * 4, hexStr, 16);
1746 Assert(AntlrInput::tokenText($BINARY_LITERAL).find("#b") == 0);
1747 std::string binStr = AntlrInput::tokenTextSubstr($BINARY_LITERAL, 2);
1748 atomTerm = SOLVER->mkBitVector(binStr.size(), binStr, 2);
1752 | str[s,false] { atomTerm = PARSER_STATE->mkStringConstant(s); }
1754 // NOTE: Theory constants go here
1756 // Empty tuple constant
1759 atomTerm = SOLVER->mkTuple(std::vector<cvc5::Sort>(),
1760 std::vector<cvc5::Term>());
1767 attribute[cvc5::Term& expr, cvc5::Term& retExpr]
1772 std::vector<cvc5::Term> patexprs;
1774 bool hasValue = false;
1777 : KEYWORD ( simpleSymbolicExprNoKeyword[s] { hasValue = true; } )?
1779 PARSER_STATE->attributeNotSupported(AntlrInput::tokenText($KEYWORD));
1781 | ( ATTRIBUTE_PATTERN_TOK { k = cvc5::INST_PATTERN; } |
1782 ATTRIBUTE_POOL_TOK { k = cvc5::INST_POOL; } |
1783 ATTRIBUTE_INST_ADD_TO_POOL_TOK { k = cvc5::INST_ADD_TO_POOL; } |
1784 ATTRIBUTE_SKOLEM_ADD_TO_POOL_TOK{ k = cvc5::SKOLEM_ADD_TO_POOL; }
1788 { patexprs.push_back( patexpr ); }
1791 retExpr = MK_TERM(k, patexprs);
1793 | ATTRIBUTE_NO_PATTERN_TOK term[patexpr, e2]
1795 retExpr = MK_TERM(cvc5::INST_NO_PATTERN, patexpr);
1797 | tok=( ATTRIBUTE_INST_LEVEL ) INTEGER_LITERAL
1799 std::stringstream sIntLit;
1800 sIntLit << $INTEGER_LITERAL;
1801 cvc5::Term keyword = SOLVER->mkString("quant-inst-max-level");
1802 cvc5::Term n = SOLVER->mkInteger(sIntLit.str());
1803 retExpr = MK_TERM(cvc5::INST_ATTRIBUTE, keyword, n);
1805 | tok=( ATTRIBUTE_QUANTIFIER_ID_TOK ) symbol[s,CHECK_UNDECLARED,SYM_VARIABLE]
1807 cvc5::Term keyword = SOLVER->mkString("qid");
1808 // must create a variable whose name is the name of the quantified
1809 // formula, not a string.
1810 cvc5::Term name = SOLVER->mkConst(SOLVER->getBooleanSort(), s);
1811 retExpr = MK_TERM(cvc5::INST_ATTRIBUTE, keyword, name);
1813 | ATTRIBUTE_NAMED_TOK symbol[s,CHECK_UNDECLARED,SYM_VARIABLE]
1815 // notify that expression was given a name
1816 DefineFunctionCommand* defFunCmd =
1817 new DefineFunctionCommand(s, expr.getSort(), expr);
1818 defFunCmd->setMuted(true);
1819 PARSER_STATE->preemptCommand(defFunCmd);
1820 PARSER_STATE->notifyNamedExpression(expr, s);
1825 * Matches a sequence of terms and puts them into the formulas
1827 * @param formulas the vector to fill with terms
1828 * @param expr an cvc5::Term reference for the elements of the sequence
1830 /* NOTE: We pass an cvc5::Term in here just to avoid allocating a fresh cvc5::Term every
1831 * time through this rule. */
1832 termList[std::vector<cvc5::Term>& formulas, cvc5::Term& expr]
1836 : ( term[expr, expr2] { formulas.push_back(expr); } )+
1840 * Matches a string, and strips off the quotes.
1842 str[std::string& s, bool fsmtlib]
1845 s = AntlrInput::tokenText($STRING_LITERAL);
1846 /* strip off the quotes */
1847 s = s.substr(1, s.size() - 2);
1848 for (size_t i = 0; i < s.size(); i++)
1850 if ((unsigned)s[i] > 127 && !isprint(s[i]))
1852 PARSER_STATE->parseError(
1853 "Extended/unprintable characters are not "
1854 "part of SMT-LIB, and they must be encoded "
1855 "as escape sequences");
1858 if (fsmtlib || PARSER_STATE->escapeDupDblQuote())
1860 char* p_orig = strdup(s.c_str());
1861 char *p = p_orig, *q = p_orig;
1864 if (PARSER_STATE->escapeDupDblQuote() && *q == '"')
1866 // Handle SMT-LIB >=2.5 standard escape '""'.
1870 else if (!PARSER_STATE->escapeDupDblQuote() && *q == '\\')
1873 // Handle SMT-LIB 2.0 standard escapes '\\' and '\"'.
1874 if (*q != '\\' && *q != '"')
1889 quantOp[cvc5::Kind& kind]
1891 Trace("parser") << "quant: " << AntlrInput::tokenText(LT(1)) << std::endl;
1893 : EXISTS_TOK { $kind = cvc5::EXISTS; }
1894 | FORALL_TOK { $kind = cvc5::FORALL; }
1898 * Matches a (possibly undeclared) function symbol (returning the string)
1899 * @param check what kind of check to do with the symbol
1901 functionName[std::string& name, cvc5::parser::DeclarationCheck check]
1902 : symbol[name,check,SYM_VARIABLE]
1906 * Matches a sequence of sort symbols and fills them into the given
1909 sortList[std::vector<cvc5::Sort>& sorts]
1913 : ( sortSymbol[t,CHECK_DECLARED] { sorts.push_back(t); } )*
1916 nonemptySortList[std::vector<cvc5::Sort>& sorts]
1920 : ( sortSymbol[t,CHECK_DECLARED] { sorts.push_back(t); } )+
1924 * Matches a sequence of (variable,sort) symbol pairs and fills them
1925 * into the given vector.
1927 sortedVarList[std::vector<std::pair<std::string, cvc5::Sort> >& sortedVars]
1932 : ( LPAREN_TOK symbol[name,CHECK_NONE,SYM_VARIABLE]
1933 sortSymbol[t,CHECK_DECLARED] RPAREN_TOK
1934 { sortedVars.push_back(make_pair(name, t)); }
1939 * Matches a sequence of (variable, sort) symbol pairs, registers them as bound
1940 * variables, and returns a term corresponding to the list of pairs.
1942 boundVarList[cvc5::Term& expr]
1944 std::vector<std::pair<std::string, cvc5::Sort>> sortedVarNames;
1946 : LPAREN_TOK sortedVarList[sortedVarNames] RPAREN_TOK
1948 std::vector<cvc5::Term> args =
1949 PARSER_STATE->bindBoundVars(sortedVarNames);
1950 expr = MK_TERM(cvc5::VARIABLE_LIST, args);
1955 * Matches the sort symbol, which can be an arbitrary symbol.
1956 * @param check the check to perform on the name
1958 sortName[std::string& name, cvc5::parser::DeclarationCheck check]
1959 : symbol[name,check,SYM_SORT]
1962 sortSymbol[cvc5::Sort& t, cvc5::parser::DeclarationCheck check]
1965 std::vector<cvc5::Sort> args;
1966 std::vector<uint32_t> numerals;
1967 bool indexed = false;
1969 : sortName[name,CHECK_NONE]
1971 if(check == CHECK_DECLARED || PARSER_STATE->isDeclared(name, SYM_SORT)) {
1972 t = PARSER_STATE->getSort(name);
1974 t = PARSER_STATE->mkUnresolvedType(name);
1977 | LPAREN_TOK (INDEX_TOK {indexed = true;} | {indexed = false;})
1978 symbol[name,CHECK_NONE,SYM_SORT]
1979 ( nonemptyNumeralList[numerals]
1983 std::stringstream ss;
1984 ss << "SMT-LIB requires use of an indexed sort here, e.g. (_ " << name
1986 PARSER_STATE->parseError(ss.str());
1988 if( name == "BitVec" ) {
1989 if( numerals.size() != 1 ) {
1990 PARSER_STATE->parseError("Illegal bitvector type.");
1992 if(numerals.front() == 0) {
1993 PARSER_STATE->parseError("Illegal bitvector size: 0");
1995 t = SOLVER->mkBitVectorSort(numerals.front());
1996 } else if ( name == "FloatingPoint" ) {
1997 if( numerals.size() != 2 ) {
1998 PARSER_STATE->parseError("Illegal floating-point type.");
2000 if(!internal::validExponentSize(numerals[0])) {
2001 PARSER_STATE->parseError("Illegal floating-point exponent size");
2003 if(!internal::validSignificandSize(numerals[1])) {
2004 PARSER_STATE->parseError("Illegal floating-point significand size");
2006 t = SOLVER->mkFloatingPointSort(numerals[0],numerals[1]);
2008 std::stringstream ss;
2009 ss << "unknown indexed sort symbol `" << name << "'";
2010 PARSER_STATE->parseError(ss.str());
2015 std::stringstream ss;
2016 ss << "Unexpected use of indexing operator `_' before `" << name
2017 << "', try leaving it out";
2018 PARSER_STATE->parseError(ss.str());
2021 PARSER_STATE->parseError("Extra parentheses around sort name not "
2022 "permitted in SMT-LIB");
2023 } else if(name == "Array" &&
2024 PARSER_STATE->isTheoryEnabled(internal::theory::THEORY_ARRAYS) ) {
2025 if(args.size() != 2) {
2026 PARSER_STATE->parseError("Illegal array type.");
2028 t = SOLVER->mkArraySort( args[0], args[1] );
2029 } else if(name == "Set" &&
2030 PARSER_STATE->isTheoryEnabled(internal::theory::THEORY_SETS) ) {
2031 if(args.size() != 1) {
2032 PARSER_STATE->parseError("Illegal set type.");
2034 t = SOLVER->mkSetSort( args[0] );
2036 else if(name == "Bag" &&
2037 PARSER_STATE->isTheoryEnabled(internal::theory::THEORY_BAGS) ) {
2038 if(args.size() != 1) {
2039 PARSER_STATE->parseError("Illegal bag type.");
2041 t = SOLVER->mkBagSort( args[0] );
2043 else if(name == "Seq" && !PARSER_STATE->strictModeEnabled() &&
2044 PARSER_STATE->isTheoryEnabled(internal::theory::THEORY_STRINGS) ) {
2045 if(args.size() != 1) {
2046 PARSER_STATE->parseError("Illegal sequence type.");
2048 t = SOLVER->mkSequenceSort( args[0] );
2049 } else if (name == "Tuple" && !PARSER_STATE->strictModeEnabled()) {
2050 t = SOLVER->mkTupleSort(args);
2051 } else if(check == CHECK_DECLARED ||
2052 PARSER_STATE->isDeclared(name, SYM_SORT)) {
2053 t = PARSER_STATE->getSort(name, args);
2055 // make unresolved type
2057 t = PARSER_STATE->mkUnresolvedType(name);
2058 Trace("parser-param") << "param: make unres type " << name
2061 t = PARSER_STATE->mkUnresolvedTypeConstructor(name,args);
2062 t = t.instantiate( args );
2063 Trace("parser-param")
2064 << "param: make unres param type " << name << " " << args.size()
2065 << " " << PARSER_STATE->getArity( name ) << std::endl;
2070 | LPAREN_TOK HO_ARROW_TOK sortList[args] RPAREN_TOK
2073 PARSER_STATE->parseError("Arrow types must have at least 2 arguments");
2076 cvc5::Sort rangeType = args.back();
2078 t = PARSER_STATE->mkFlatFunctionType( args, rangeType );
2083 * Matches a list of symbols, with check and type arguments as for the
2084 * symbol[] rule below.
2086 symbolList[std::vector<std::string>& names,
2087 cvc5::parser::DeclarationCheck check,
2088 cvc5::parser::SymbolType type]
2092 : ( symbol[id,check,type] { names.push_back(id); } )*
2096 * Matches an symbol and sets the string reference parameter id.
2097 * @param id string to hold the symbol
2098 * @param check what kinds of check to do on the symbol
2099 * @param type the intended namespace for the symbol
2101 symbol[std::string& id,
2102 cvc5::parser::DeclarationCheck check,
2103 cvc5::parser::SymbolType type]
2105 { id = AntlrInput::tokenText($SIMPLE_SYMBOL);
2106 if(!PARSER_STATE->isAbstractValue(id)) {
2107 // if an abstract value, SolverEngine handles declaration
2108 PARSER_STATE->checkDeclaration(id, check, type);
2112 { id = AntlrInput::tokenText($QUOTED_SYMBOL);
2113 /* strip off the quotes */
2114 id = id.substr(1, id.size() - 2);
2115 if(!PARSER_STATE->isAbstractValue(id)) {
2116 // if an abstract value, SolverEngine handles declaration
2117 PARSER_STATE->checkDeclaration(id, check, type);
2120 | UNTERMINATED_QUOTED_SYMBOL
2122 { PARSER_STATE->unexpectedEOF("unterminated |quoted| symbol"); }
2124 { PARSER_STATE->unexpectedEOF("backslash not permitted in |quoted| "
2130 * Matches a nonempty list of numerals.
2131 * @param numerals the (empty) vector to house the numerals.
2133 nonemptyNumeralList[std::vector<uint32_t>& numerals]
2135 { numerals.push_back(AntlrInput::tokenToUnsigned($INTEGER_LITERAL)); }
2140 * Parses a datatype definition
2142 datatypeDef[bool isCo, std::vector<cvc5::DatatypeDecl>& datatypes,
2143 std::vector< cvc5::Sort >& params]
2147 /* This really needs to be CHECK_NONE, or mutually-recursive
2148 * datatypes won't work, because this type will already be
2149 * "defined" as an unresolved type; don't worry, we check
2151 : symbol[id,CHECK_NONE,SYM_SORT] { PARSER_STATE->pushScope(); }
2153 datatypes.push_back(SOLVER->mkDatatypeDecl(id, params, isCo));
2155 ( LPAREN_TOK constructorDef[datatypes.back()] RPAREN_TOK )+
2156 { PARSER_STATE->popScope(); }
2160 * Parses a constructor defintion for type
2162 constructorDef[cvc5::DatatypeDecl& type]
2165 cvc5::DatatypeConstructorDecl* ctor = NULL;
2167 : symbol[id,CHECK_NONE,SYM_VARIABLE]
2169 ctor = new cvc5::DatatypeConstructorDecl(
2170 SOLVER->mkDatatypeConstructorDecl(id));
2172 ( LPAREN_TOK selector[*ctor] RPAREN_TOK )*
2173 { // make the constructor
2174 type.addConstructor(*ctor);
2175 Trace("parser-idt") << "constructor: " << id.c_str() << std::endl;
2180 selector[cvc5::DatatypeConstructorDecl& ctor]
2185 : symbol[id,CHECK_NONE,SYM_SORT] sortSymbol[t,CHECK_NONE]
2187 ctor.addSelector(id, t);
2188 Trace("parser-idt") << "selector: " << id.c_str()
2189 << " of type " << t << std::endl;
2193 // Base SMT-LIB tokens
2194 ASSERT_TOK : 'assert';
2195 CHECK_SAT_TOK : 'check-sat';
2196 CHECK_SAT_ASSUMING_TOK : 'check-sat-assuming';
2197 DECLARE_FUN_TOK : 'declare-fun';
2198 DECLARE_SORT_TOK : 'declare-sort';
2199 DEFINE_FUN_TOK : 'define-fun';
2200 DEFINE_FUN_REC_TOK : 'define-fun-rec';
2201 DEFINE_FUNS_REC_TOK : 'define-funs-rec';
2202 DEFINE_SORT_TOK : 'define-sort';
2203 GET_VALUE_TOK : 'get-value';
2204 GET_ASSIGNMENT_TOK : 'get-assignment';
2205 GET_ASSERTIONS_TOK : 'get-assertions';
2206 GET_PROOF_TOK : 'get-proof';
2207 GET_UNSAT_ASSUMPTIONS_TOK : 'get-unsat-assumptions';
2208 GET_UNSAT_CORE_TOK : 'get-unsat-core';
2209 GET_DIFFICULTY_TOK : 'get-difficulty';
2210 GET_LEARNED_LITERALS_TOK : { !PARSER_STATE->strictModeEnabled() }? 'get-learned-literals';
2212 RESET_TOK : 'reset';
2213 RESET_ASSERTIONS_TOK : 'reset-assertions';
2215 ATTRIBUTE_TOK : '!';
2219 SET_LOGIC_TOK : 'set-logic';
2220 SET_INFO_TOK : 'set-info';
2221 GET_INFO_TOK : 'get-info';
2222 SET_OPTION_TOK : 'set-option';
2223 GET_OPTION_TOK : 'get-option';
2227 CONST_TOK : { !PARSER_STATE->strictModeEnabled() }? 'const';
2229 // extended commands
2230 DECLARE_CODATATYPE_TOK : { PARSER_STATE->v2_6() || PARSER_STATE->sygus() }? 'declare-codatatype';
2231 DECLARE_DATATYPE_TOK : { PARSER_STATE->v2_6() || PARSER_STATE->sygus() }? 'declare-datatype';
2232 DECLARE_DATATYPES_2_5_TOK : { !( PARSER_STATE->v2_6() || PARSER_STATE->sygus() ) }?'declare-datatypes';
2233 DECLARE_DATATYPES_TOK : { PARSER_STATE->v2_6() || PARSER_STATE->sygus() }?'declare-datatypes';
2234 DECLARE_CODATATYPES_2_5_TOK : { !( PARSER_STATE->v2_6() || PARSER_STATE->sygus() ) }?'declare-codatatypes';
2235 DECLARE_CODATATYPES_TOK : { PARSER_STATE->v2_6() || PARSER_STATE->sygus() }?'declare-codatatypes';
2236 PAR_TOK : { PARSER_STATE->v2_6() || PARSER_STATE->sygus() }?'par';
2237 SET_COMPREHENSION_TOK : { PARSER_STATE->isTheoryEnabled(internal::theory::THEORY_SETS) }?'set.comprehension';
2238 TESTER_TOK : { ( PARSER_STATE->v2_6() || PARSER_STATE->sygus() ) && PARSER_STATE->isTheoryEnabled(internal::theory::THEORY_DATATYPES) }?'is';
2239 UPDATE_TOK : { ( PARSER_STATE->v2_6() || PARSER_STATE->sygus() ) && PARSER_STATE->isTheoryEnabled(internal::theory::THEORY_DATATYPES) }?'update';
2240 MATCH_TOK : { ( PARSER_STATE->v2_6() || PARSER_STATE->sygus() ) && PARSER_STATE->isTheoryEnabled(internal::theory::THEORY_DATATYPES) }?'match';
2241 GET_MODEL_TOK : 'get-model';
2242 BLOCK_MODEL_TOK : 'block-model';
2243 BLOCK_MODEL_VALUES_TOK : 'block-model-values';
2245 DECLARE_SORTS_TOK : 'declare-sorts';
2246 DECLARE_FUNS_TOK : 'declare-funs';
2247 DECLARE_PREDS_TOK : 'declare-preds';
2248 DECLARE_CONST_TOK : 'declare-const';
2249 DEFINE_CONST_TOK : 'define-const';
2250 SIMPLIFY_TOK : 'simplify';
2251 INCLUDE_TOK : 'include';
2252 GET_QE_TOK : 'get-qe';
2253 GET_QE_DISJUNCT_TOK : 'get-qe-disjunct';
2254 GET_ABDUCT_TOK : 'get-abduct';
2255 GET_ABDUCT_NEXT_TOK : 'get-abduct-next';
2256 GET_INTERPOL_TOK : 'get-interpolant';
2257 GET_INTERPOL_NEXT_TOK : 'get-interpolant-next';
2258 DECLARE_HEAP : 'declare-heap';
2259 DECLARE_POOL : 'declare-pool';
2262 SYNTH_FUN_TOK : { PARSER_STATE->sygus() }?'synth-fun';
2263 SYNTH_INV_TOK : { PARSER_STATE->sygus()}?'synth-inv';
2264 CHECK_SYNTH_TOK : { PARSER_STATE->sygus()}?'check-synth';
2265 CHECK_SYNTH_NEXT_TOK : { PARSER_STATE->sygus()}?'check-synth-next';
2266 DECLARE_VAR_TOK : { PARSER_STATE->sygus()}?'declare-var';
2267 CONSTRAINT_TOK : { PARSER_STATE->sygus()}?'constraint';
2268 ASSUME_TOK : { PARSER_STATE->sygus()}?'assume';
2269 INV_CONSTRAINT_TOK : { PARSER_STATE->sygus()}?'inv-constraint';
2270 SET_FEATURE_TOK : { PARSER_STATE->sygus() }? 'set-feature';
2271 SYGUS_CONSTANT_TOK : { PARSER_STATE->sygus() }? 'Constant';
2272 SYGUS_VARIABLE_TOK : { PARSER_STATE->sygus() }? 'Variable';
2275 ATTRIBUTE_PATTERN_TOK : ':pattern';
2276 ATTRIBUTE_NO_PATTERN_TOK : ':no-pattern';
2277 ATTRIBUTE_POOL_TOK : ':pool';
2278 ATTRIBUTE_INST_ADD_TO_POOL_TOK : ':inst-add-to-pool';
2279 ATTRIBUTE_SKOLEM_ADD_TO_POOL_TOK : ':skolem-add-to-pool';
2280 ATTRIBUTE_NAMED_TOK : ':named';
2281 ATTRIBUTE_INST_LEVEL : ':quant-inst-max-level';
2282 ATTRIBUTE_QUANTIFIER_ID_TOK : ':qid';
2284 // operators (NOTE: theory symbols go here)
2285 EXISTS_TOK : 'exists';
2286 FORALL_TOK : 'forall';
2288 CHAR_TOK : { PARSER_STATE->isTheoryEnabled(internal::theory::THEORY_STRINGS) }? 'char';
2289 TUPLE_CONST_TOK: { PARSER_STATE->isTheoryEnabled(internal::theory::THEORY_DATATYPES) }? 'tuple';
2290 TUPLE_PROJECT_TOK: { PARSER_STATE->isTheoryEnabled(internal::theory::THEORY_DATATYPES) }? 'tuple.project';
2291 FMF_CARD_TOK: { !PARSER_STATE->strictModeEnabled() && PARSER_STATE->hasCardinalityConstraints() }? 'fmf.card';
2293 HO_ARROW_TOK : { PARSER_STATE->isHoEnabled() }? '->';
2294 HO_LAMBDA_TOK : { PARSER_STATE->isHoEnabled() }? 'lambda';
2297 * A sequence of printable ASCII characters (except backslash) that starts
2298 * and ends with | and does not otherwise contain |.
2300 * You shouldn't generally use this in parser rules, as the |quoting|
2301 * will be part of the token text. Use the symbol[] parser rule instead.
2304 : '|' ~('|' | '\\')* '|'
2306 UNTERMINATED_QUOTED_SYMBOL
2307 : '|' ~('|' | '\\')*
2311 * Matches a keyword from the input. A keyword is a simple symbol prefixed
2315 : ':' (ALPHA | DIGIT | SYMBOL_CHAR)+
2319 * Matches a "simple" symbol: a non-empty sequence of letters, digits and
2320 * the characters + - / * = % ? ! . $ ~ & ^ < > @ that does not start with a
2321 * digit, and is not the special reserved symbols '!' or '_'.
2324 : ALPHA (ALPHA | DIGIT | SYMBOL_CHAR)*
2325 | SYMBOL_CHAR (ALPHA | DIGIT | SYMBOL_CHAR)+
2326 | SYMBOL_CHAR_NOUNDERSCORE_NOATTRIBUTE
2330 * Matches and skips whitespace in the input.
2333 : (' ' | '\t' | '\f' | '\r' | '\n')+ { SKIP(); }
2337 * Matches an integer constant from the input (non-empty sequence of
2338 * digits, with no leading zeroes).
2345 * Match an integer constant. In non-strict mode, this is any sequence
2346 * of digits. In strict mode, non-zero integers can't have leading
2351 char *start = (char*) GETCHARINDEX();
2354 { Trace("parser-extra") << "NUMERAL: "
2355 << (uintptr_t)start << ".." << GETCHARINDEX()
2356 << " strict? " << (bool)(PARSER_STATE->strictModeEnabled())
2357 << " ^0? " << (bool)(*start == '0')
2358 << " len>1? " << (bool)(start < (char*)(GETCHARINDEX() - 1))
2360 { !PARSER_STATE->strictModeEnabled() ||
2362 start == (char*)(GETCHARINDEX() - 1) }?
2366 * Matches a decimal constant from the input.
2369 : NUMERAL '.' DIGIT+
2373 * Matches a hexadecimal constant.
2380 * Matches a binary constant.
2387 * Matches a double-quoted string literal. Depending on the language that is
2388 * being parsed, different escape sequences are supported:
2390 * For SMT-LIB 2.0 the sequence \" is interpreted as a double quote (") and the
2391 * sequence \\ is interpreted as a backslash (\).
2393 * For SMT-LIB >=2.5 and SyGuS a double-quote inside a string is escaped with
2394 * "", e.g., "This is a string literal with "" a single, embedded double
2397 * You shouldn't generally use this in parser rules, as the quotes
2398 * will be part of the token text. Use the str[] parser rule instead.
2401 : { !PARSER_STATE->escapeDupDblQuote() }?=>
2402 '"' ('\\' . | ~('\\' | '"'))* '"'
2403 | { PARSER_STATE->escapeDupDblQuote() }?=>
2404 '"' (~('"') | '""')* '"'
2408 * Matches the comments and ignores them
2411 : ';' (~('\n' | '\r'))* { SKIP(); }
2415 * Matches any letter ('a'-'z' and 'A'-'Z').
2424 * Matches the digits (0-9)
2426 fragment DIGIT : '0'..'9';
2428 fragment HEX_DIGIT : DIGIT | 'a'..'f' | 'A'..'F';
2431 * Matches the characters that may appear as a one-character "symbol"
2432 * (which excludes _ and !, which are reserved words in SMT-LIB).
2434 fragment SYMBOL_CHAR_NOUNDERSCORE_NOATTRIBUTE
2435 : '+' | '-' | '/' | '*' | '=' | '%' | '?' | '.' | '$' | '~'
2436 | '&' | '^' | '<' | '>' | '@'
2440 * Matches the characters that may appear in a "symbol" (i.e., an identifier)
2442 fragment SYMBOL_CHAR
2443 : SYMBOL_CHAR_NOUNDERSCORE_NOATTRIBUTE | '_' | '!'