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 #include "parser/antlr_tracing.h"
64 }/* @lexer::includes */
67 #include "parser/smt2/smt2.h"
68 #include "parser/antlr_input.h"
71 using namespace cvc5::parser;
74 #define PARSER_STATE ((Smt2*)LEXER->super)
75 }/* @lexer::postinclude */
81 #include "base/check.h"
82 #include "parser/antlr_tracing.h"
83 #include "parser/parse_op.h"
84 #include "parser/parser.h"
85 #include "smt/command.h"
96 }/* @parser::includes */
98 @parser::postinclude {
103 #include <unordered_set>
106 #include "api/cpp/cvc5.h"
107 #include "base/output.h"
108 #include "options/set_language.h"
109 #include "parser/antlr_input.h"
110 #include "parser/parser.h"
111 #include "parser/smt2/smt2.h"
112 #include "util/floatingpoint_size.h"
113 #include "util/hash.h"
115 using namespace cvc5;
116 using namespace cvc5::parser;
118 /* These need to be macros so they can refer to the PARSER macro, which
119 * will be defined by ANTLR *after* this section. (If they were functions,
120 * PARSER would be undefined.) */
122 #define PARSER_STATE ((Smt2*)PARSER->super)
124 #define SOLVER PARSER_STATE->getSolver()
126 #define SYM_MAN PARSER_STATE->getSymbolManager()
128 #define MK_TERM SOLVER->mkTerm
129 #define UNSUPPORTED PARSER_STATE->unimplementedFeature
131 }/* parser::postinclude */
134 * Parses an expression.
135 * @return the parsed expression, or the Null Expr if we've reached the
138 parseExpr returns [cvc5::api::Term expr = cvc5::api::Term()]
140 cvc5::api::Term expr2;
148 * @return the parsed command, or NULL if we've reached the end of the input
150 parseCommand returns [cvc5::Command* cmd_return = NULL]
152 std::unique_ptr<cvc5::Command> cmd;
156 cmd_return = cmd.release();
158 : LPAREN_TOK command[&cmd] RPAREN_TOK
160 /* This extended command has to be in the outermost production so that
161 * the RPAREN_TOK is properly eaten and we are in a good state to read
162 * the included file's tokens. */
163 | LPAREN_TOK INCLUDE_TOK str[name,true] RPAREN_TOK
164 { if(!PARSER_STATE->canIncludeFile()) {
165 PARSER_STATE->parseError("include-file feature was disabled for this "
168 if(PARSER_STATE->strictModeEnabled()) {
169 PARSER_STATE->parseError("Extended commands are not permitted while "
170 "operating in strict compliance mode.");
172 PARSER_STATE->includeFile(name);
173 // The command of the included file will be produced at the next
174 // parseCommand() call
175 cmd.reset(new EmptyCommand("include::" + name));
182 * Parses a SyGuS command.
183 * @return the parsed SyGuS command, or NULL if we've reached the end of the
186 parseSygus returns [cvc5::Command* cmd_return = NULL]
191 cmd_return = cmd.release();
193 : LPAREN_TOK cmd=sygusCommand RPAREN_TOK
198 * Parse the internal portion of the command, ignoring the surrounding
201 command [std::unique_ptr<cvc5::Command>* cmd]
204 std::vector<std::string> names;
205 cvc5::api::Term expr, expr2;
207 std::vector<cvc5::api::Term> terms;
208 std::vector<api::Sort> sorts;
209 std::vector<std::pair<std::string, cvc5::api::Sort> > sortedVarNames;
210 std::vector<cvc5::api::Term> flattenVars;
212 : /* set the logic */
213 SET_LOGIC_TOK symbol[name,CHECK_NONE,SYM_SORT]
215 cmd->reset(PARSER_STATE->setLogic(name));
218 SET_INFO_TOK setInfoInternal[cmd]
221 { cmd->reset(new GetInfoCommand(
222 AntlrInput::tokenText($KEYWORD).c_str() + 1));
225 SET_OPTION_TOK setOptionInternal[cmd]
227 GET_OPTION_TOK KEYWORD
228 { cmd->reset(new GetOptionCommand(
229 AntlrInput::tokenText($KEYWORD).c_str() + 1));
231 | /* sort declaration */
234 PARSER_STATE->checkThatLogicIsSet();
235 PARSER_STATE->checkLogicAllowsFreeSorts();
237 symbol[name,CHECK_UNDECLARED,SYM_SORT]
238 { PARSER_STATE->checkUserSymbol(name); }
240 { Debug("parser") << "declare sort: '" << name
241 << "' arity=" << n << std::endl;
242 unsigned arity = AntlrInput::tokenToUnsigned(n);
244 api::Sort type = PARSER_STATE->mkSort(name);
245 cmd->reset(new DeclareSortCommand(name, 0, type));
247 api::Sort type = PARSER_STATE->mkSortConstructor(name, arity);
248 cmd->reset(new DeclareSortCommand(name, arity, type));
251 | /* sort definition */
252 DEFINE_SORT_TOK { PARSER_STATE->checkThatLogicIsSet(); }
253 symbol[name,CHECK_UNDECLARED,SYM_SORT]
254 { PARSER_STATE->checkUserSymbol(name); }
255 LPAREN_TOK symbolList[names,CHECK_NONE,SYM_SORT] RPAREN_TOK
256 { PARSER_STATE->pushScope();
257 for(std::vector<std::string>::const_iterator i = names.begin(),
261 sorts.push_back(PARSER_STATE->mkSort(*i));
264 sortSymbol[t,CHECK_DECLARED]
265 { PARSER_STATE->popScope();
266 // Do NOT call mkSort, since that creates a new sort!
267 // This name is not its own distinct sort, it's an alias.
268 PARSER_STATE->defineParameterizedType(name, sorts, t);
269 cmd->reset(new DefineSortCommand(name, sorts, t));
271 | /* function declaration */
272 DECLARE_FUN_TOK { PARSER_STATE->checkThatLogicIsSet(); }
273 symbol[name,CHECK_NONE,SYM_VARIABLE]
274 { PARSER_STATE->checkUserSymbol(name); }
275 LPAREN_TOK sortList[sorts] RPAREN_TOK
276 sortSymbol[t,CHECK_DECLARED]
277 { Debug("parser") << "declare fun: '" << name << "'" << std::endl;
278 if( !sorts.empty() ) {
279 t = PARSER_STATE->mkFlatFunctionType(sorts, t);
283 PARSER_STATE->checkLogicAllowsFunctions();
285 // we allow overloading for function declarations
286 if( PARSER_STATE->sygus() )
288 PARSER_STATE->parseErrorLogic("declare-fun are not allowed in sygus "
294 PARSER_STATE->bindVar(name, t, false, true);
295 cmd->reset(new DeclareFunctionCommand(name, func, t));
298 | /* function definition */
299 DEFINE_FUN_TOK { PARSER_STATE->checkThatLogicIsSet(); }
300 symbol[name,CHECK_UNDECLARED,SYM_VARIABLE]
301 { PARSER_STATE->checkUserSymbol(name); }
302 LPAREN_TOK sortedVarList[sortedVarNames] RPAREN_TOK
303 sortSymbol[t,CHECK_DECLARED]
304 { /* add variables to parser state before parsing term */
305 Debug("parser") << "define fun: '" << name << "'" << std::endl;
306 if( sortedVarNames.size() > 0 ) {
307 sorts.reserve(sortedVarNames.size());
308 for(std::vector<std::pair<std::string, api::Sort> >::const_iterator i =
309 sortedVarNames.begin(), iend = sortedVarNames.end();
312 sorts.push_back((*i).second);
316 t = PARSER_STATE->mkFlatFunctionType(sorts, t, flattenVars);
317 if (sortedVarNames.size() > 0)
319 PARSER_STATE->pushScope();
321 terms = PARSER_STATE->bindBoundVars(sortedVarNames);
325 if( !flattenVars.empty() ){
326 // if this function has any implicit variables flattenVars,
327 // we apply the body of the definition to the flatten vars
328 expr = PARSER_STATE->mkHoApply(expr, flattenVars);
329 terms.insert(terms.end(), flattenVars.begin(), flattenVars.end());
331 if (sortedVarNames.size() > 0)
333 PARSER_STATE->popScope();
335 // declare the name down here (while parsing term, signature
336 // must not be extended with the name itself; no recursion
338 // we allow overloading for function definitions
339 api::Term func = PARSER_STATE->bindVar(name, t, false, true);
340 cmd->reset(new DefineFunctionCommand(
341 name, func, terms, expr, SYM_MAN->getGlobalDeclarations()));
343 | DECLARE_DATATYPE_TOK datatypeDefCommand[false, cmd]
344 | DECLARE_DATATYPES_TOK datatypesDefCommand[false, cmd]
346 GET_VALUE_TOK { PARSER_STATE->checkThatLogicIsSet(); }
347 ( LPAREN_TOK termList[terms,expr] RPAREN_TOK
348 { cmd->reset(new GetValueCommand(terms)); }
350 { PARSER_STATE->parseError("The get-value command expects a list of "
351 "terms. Perhaps you forgot a pair of "
355 | /* get-assignment */
356 GET_ASSIGNMENT_TOK { PARSER_STATE->checkThatLogicIsSet(); }
357 { cmd->reset(new GetAssignmentCommand()); }
359 ASSERT_TOK { PARSER_STATE->checkThatLogicIsSet(); }
360 { PARSER_STATE->clearLastNamedTerm(); }
362 { cmd->reset(new AssertCommand(expr));
363 if (PARSER_STATE->lastNamedTerm().first == expr)
365 // set the expression name, if there was a named term
366 std::pair<api::Term, std::string> namedTerm =
367 PARSER_STATE->lastNamedTerm();
368 SYM_MAN->setExpressionName(namedTerm.first, namedTerm.second, true);
372 CHECK_SAT_TOK { PARSER_STATE->checkThatLogicIsSet(); }
373 { if( PARSER_STATE->sygus() ){
374 PARSER_STATE->parseError("Sygus does not support check-sat command.");
378 { if(PARSER_STATE->strictModeEnabled()) {
379 PARSER_STATE->parseError(
380 "Extended commands (such as check-sat with an argument) are not "
381 "permitted while operating in strict compliance mode.");
384 | { expr = api::Term(); }
386 { cmd->reset(new CheckSatCommand(expr)); }
387 | /* check-sat-assuming */
388 CHECK_SAT_ASSUMING_TOK { PARSER_STATE->checkThatLogicIsSet(); }
389 ( LPAREN_TOK termList[terms,expr] RPAREN_TOK
391 cmd->reset(new CheckSatAssumingCommand(terms));
394 { PARSER_STATE->parseError("The check-sat-assuming command expects a "
395 "list of terms. Perhaps you forgot a pair of "
399 | /* get-assertions */
400 GET_ASSERTIONS_TOK { PARSER_STATE->checkThatLogicIsSet(); }
401 { cmd->reset(new GetAssertionsCommand()); }
403 GET_PROOF_TOK { PARSER_STATE->checkThatLogicIsSet(); }
404 { cmd->reset(new GetProofCommand()); }
405 | /* get-unsat-assumptions */
406 GET_UNSAT_ASSUMPTIONS_TOK { PARSER_STATE->checkThatLogicIsSet(); }
407 { cmd->reset(new GetUnsatAssumptionsCommand); }
408 | /* get-unsat-core */
409 GET_UNSAT_CORE_TOK { PARSER_STATE->checkThatLogicIsSet(); }
410 { cmd->reset(new GetUnsatCoreCommand); }
412 PUSH_TOK { PARSER_STATE->checkThatLogicIsSet(); }
413 { if( PARSER_STATE->sygus() ){
414 PARSER_STATE->parseError("Sygus does not support push command.");
418 { unsigned num = AntlrInput::tokenToUnsigned(k);
420 cmd->reset(new EmptyCommand());
421 } else if(num == 1) {
422 PARSER_STATE->pushScope(true);
423 cmd->reset(new PushCommand());
425 std::unique_ptr<CommandSequence> seq(new CommandSequence());
427 PARSER_STATE->pushScope(true);
428 Command* push_cmd = new PushCommand();
429 push_cmd->setMuted(num > 1);
430 seq->addCommand(push_cmd);
433 cmd->reset(seq.release());
436 | { if(PARSER_STATE->strictModeEnabled()) {
437 PARSER_STATE->parseError(
438 "Strict compliance mode demands an integer to be provided to "
439 "PUSH. Maybe you want (push 1)?");
441 PARSER_STATE->pushScope(true);
442 cmd->reset(new PushCommand());
445 | POP_TOK { PARSER_STATE->checkThatLogicIsSet(); }
446 { if( PARSER_STATE->sygus() ){
447 PARSER_STATE->parseError("Sygus does not support pop command.");
451 { unsigned num = AntlrInput::tokenToUnsigned(k);
452 if(num > PARSER_STATE->scopeLevel()) {
453 PARSER_STATE->parseError("Attempted to pop above the top stack "
457 cmd->reset(new EmptyCommand());
458 } else if(num == 1) {
459 PARSER_STATE->popScope();
460 cmd->reset(new PopCommand());
462 std::unique_ptr<CommandSequence> seq(new CommandSequence());
464 PARSER_STATE->popScope();
465 Command* pop_command = new PopCommand();
466 pop_command->setMuted(num > 1);
467 seq->addCommand(pop_command);
470 cmd->reset(seq.release());
473 | { if(PARSER_STATE->strictModeEnabled()) {
474 PARSER_STATE->parseError(
475 "Strict compliance mode demands an integer to be provided to POP."
476 "Maybe you want (pop 1)?");
478 PARSER_STATE->popScope();
479 cmd->reset(new PopCommand());
485 { cmd->reset(new QuitCommand()); }
487 /* New SMT-LIB 2.5 command set */
490 /* cvc5-extended SMT-LIB commands */
491 | extendedCommand[cmd]
492 { if(PARSER_STATE->strictModeEnabled()) {
493 PARSER_STATE->parseError(
494 "Extended commands are not permitted while operating in strict "
501 { std::string id = AntlrInput::tokenText($SIMPLE_SYMBOL);
502 if(id == "benchmark") {
503 PARSER_STATE->parseError(
504 "In SMT-LIBv2 mode, but got something that looks like SMT-LIBv1, "
505 "which is not supported anymore.");
507 PARSER_STATE->parseError("expected SMT-LIBv2 command, got `" + id +
513 sygusCommand returns [std::unique_ptr<cvc5::Command> cmd]
515 cvc5::api::Term expr, expr2, fun;
516 cvc5::api::Sort t, range;
517 std::vector<std::string> names;
518 std::vector<std::pair<std::string, cvc5::api::Sort> > sortedVarNames;
519 std::vector<cvc5::api::Term> sygusVars;
523 cvc5::api::Grammar* grammar = nullptr;
526 DECLARE_VAR_TOK { PARSER_STATE->checkThatLogicIsSet(); }
527 symbol[name,CHECK_UNDECLARED,SYM_VARIABLE]
528 { PARSER_STATE->checkUserSymbol(name); }
529 sortSymbol[t,CHECK_DECLARED]
531 api::Term var = SOLVER->mkSygusVar(t, name);
532 PARSER_STATE->defineVar(name, var);
533 cmd.reset(new DeclareSygusVarCommand(name, var, t));
536 ( SYNTH_FUN_TOK { isInv = false; }
537 | SYNTH_INV_TOK { isInv = true; range = SOLVER->getBooleanSort(); }
539 { PARSER_STATE->checkThatLogicIsSet(); }
540 symbol[name,CHECK_UNDECLARED,SYM_VARIABLE]
541 LPAREN_TOK sortedVarList[sortedVarNames] RPAREN_TOK
542 ( sortSymbol[range,CHECK_DECLARED] )?
544 PARSER_STATE->pushScope();
545 sygusVars = PARSER_STATE->bindBoundVars(sortedVarNames);
548 // optionally, read the sygus grammar
550 // `grammar` specifies the required grammar for the function to
551 // synthesize, expressed as a type
552 sygusGrammar[grammar, sygusVars, name]
555 Debug("parser-sygus") << "Define synth fun : " << name << std::endl;
557 fun = isInv ? (grammar == nullptr
558 ? SOLVER->synthInv(name, sygusVars)
559 : SOLVER->synthInv(name, sygusVars, *grammar))
560 : (grammar == nullptr
561 ? SOLVER->synthFun(name, sygusVars, range)
562 : SOLVER->synthFun(name, sygusVars, range, *grammar));
564 Debug("parser-sygus") << "...read synth fun " << name << std::endl;
565 PARSER_STATE->popScope();
566 // we do not allow overloading for synth fun
567 PARSER_STATE->defineVar(name, fun);
568 cmd = std::unique_ptr<Command>(
569 new SynthFunCommand(name, fun, sygusVars, range, isInv, grammar));
572 ( CONSTRAINT_TOK { isAssume = false; } | ASSUME_TOK { isAssume = true; } )
574 PARSER_STATE->checkThatLogicIsSet();
577 { Debug("parser-sygus") << "...read constraint " << expr << std::endl;
578 cmd.reset(new SygusConstraintCommand(expr, isAssume));
580 | /* inv-constraint */
582 ( symbol[name,CHECK_NONE,SYM_VARIABLE] { names.push_back(name); } )+
584 cmd = PARSER_STATE->invConstraint(names);
589 PARSER_STATE->checkThatLogicIsSet();
590 cmd.reset(new CheckSynthCommand());
593 SET_FEATURE_TOK keyword[name] symbolicExpr[expr]
595 PARSER_STATE->checkThatLogicIsSet();
596 // ":grammars" is defined in the SyGuS version 2.1 standard and is by
597 // default supported, all other features are not.
598 if (name != ":grammars")
600 std::stringstream ss;
601 ss << "SyGuS feature " << name << " not currently supported";
602 PARSER_STATE->warning(ss.str());
604 cmd.reset(new EmptyCommand());
610 /** Reads a sygus grammar in the sygus version 2 format
612 * The resulting sygus datatype encoding the grammar is stored in ret.
613 * The argument sygusVars indicates the sygus bound variable list, which is
614 * the argument list of the function-to-synthesize (or null if the grammar
615 * has bound variables).
616 * The argument fun is a unique identifier to avoid naming clashes for the
617 * datatypes constructed by this call.
619 sygusGrammar[cvc5::api::Grammar*& ret,
620 const std::vector<cvc5::api::Term>& sygusVars,
621 const std::string& fun]
624 // the pre-declaration
625 std::vector<std::pair<std::string, cvc5::api::Sort>> sortedVarNames;
626 // non-terminal symbols of the grammar
627 std::vector<cvc5::api::Term> ntSyms;
630 cvc5::api::Term e, e2;
631 unsigned dtProcessed = 0;
636 // We read a sorted variable list here in a custom way that throws an
637 // error to recognize if the user is using the (deprecated) version 1.0
639 ( LPAREN_TOK symbol[name,CHECK_NONE,SYM_VARIABLE]
640 sortSymbol[t,CHECK_DECLARED] (
641 // SyGuS version 1.0 expects a grammar ((Start Int ( ...
642 // SyGuS version 2.0 expects a predeclaration ((Start Int) ...
645 std::stringstream sse;
646 if (sortedVarNames.empty())
648 sse << "The expected SyGuS language is version 2.0, whereas the "
649 << "input appears to be SyGuS version 1.0 format. The version "
650 << "2.0 format requires a predeclaration of the non-terminal "
651 << "symbols of the grammar to be given prior to the definition "
652 << "of the grammar. See https://sygus.org/language/ for details "
653 << "and examples. cvc5 versions past 1.8 do not support SyGuS "
658 // an unknown syntax error
659 sse << "Unexpected syntax for SyGuS predeclaration.";
661 PARSER_STATE->parseError(sse.str().c_str());
664 { sortedVarNames.push_back(make_pair(name, t)); }
668 // non-terminal symbols in the pre-declaration are locally scoped
669 PARSER_STATE->pushScope();
670 for (std::pair<std::string, api::Sort>& i : sortedVarNames)
672 PARSER_STATE->checkDeclaration(name, CHECK_UNDECLARED, SYM_SORT);
673 // make the non-terminal symbol, which will be parsed as an ordinary
675 api::Term nts = PARSER_STATE->bindBoundVar(i.first, i.second);
676 ntSyms.push_back(nts);
678 ret = PARSER_STATE->mkGrammar(sygusVars, ntSyms);
680 // the grouped rule listing
684 symbol[name, CHECK_DECLARED, SYM_VARIABLE] sortSymbol[t, CHECK_DECLARED]
686 // check that it matches sortedVarNames
687 if (sortedVarNames[dtProcessed].first != name)
689 std::stringstream sse;
690 sse << "Grouped rule listing " << name
691 << " does not match the name (in order) from the predeclaration ("
692 << sortedVarNames[dtProcessed].first << ")." << std::endl;
693 PARSER_STATE->parseError(sse.str().c_str());
695 if (sortedVarNames[dtProcessed].second != t)
697 std::stringstream sse;
698 sse << "Type for grouped rule listing " << name
699 << " does not match the type (in order) from the predeclaration ("
700 << sortedVarNames[dtProcessed].second << ")." << std::endl;
701 PARSER_STATE->parseError(sse.str().c_str());
707 // add term as constructor to datatype
708 ret->addRule(ntSyms[dtProcessed], e);
710 | LPAREN_TOK SYGUS_CONSTANT_TOK sortSymbol[t, CHECK_DECLARED] RPAREN_TOK {
711 // allow constants in datatype for ntSyms[dtProcessed]
712 ret->addAnyConstant(ntSyms[dtProcessed]);
714 | LPAREN_TOK SYGUS_VARIABLE_TOK sortSymbol[t, CHECK_DECLARED] RPAREN_TOK {
715 // add variable constructors to datatype
716 ret->addAnyVariable(ntSyms[dtProcessed]);
727 // pop scope from the pre-declaration
728 PARSER_STATE->popScope();
732 setInfoInternal[std::unique_ptr<cvc5::Command>* cmd]
737 : KEYWORD symbolicExpr[sexpr]
738 { name = AntlrInput::tokenText($KEYWORD);
739 cmd->reset(new SetInfoCommand(name.c_str() + 1, sexprToString(sexpr)));
743 setOptionInternal[std::unique_ptr<cvc5::Command>* cmd]
748 : keyword[name] symbolicExpr[sexpr]
749 { cmd->reset(new SetOptionCommand(name.c_str() + 1, sexprToString(sexpr)));
750 // Ugly that this changes the state of the parser; but
751 // global-declarations affects parsing, so we can't hold off
752 // on this until some SmtEngine eventually (if ever) executes it.
753 if(name == ":global-declarations")
755 SYM_MAN->setGlobalDeclarations(sexprToString(sexpr) == "true");
760 smt25Command[std::unique_ptr<cvc5::Command>* cmd]
764 cvc5::api::Term expr, expr2;
765 std::vector<std::pair<std::string, cvc5::api::Sort> > sortedVarNames;
768 cvc5::api::Term func;
769 std::vector<cvc5::api::Term> bvs;
770 std::vector<std::vector<std::pair<std::string, cvc5::api::Sort>>>
772 std::vector<std::vector<cvc5::api::Term>> flattenVarsList;
773 std::vector<std::vector<cvc5::api::Term>> formals;
774 std::vector<cvc5::api::Term> funcs;
775 std::vector<cvc5::api::Term> func_defs;
776 cvc5::api::Term aexpr;
777 std::unique_ptr<cvc5::CommandSequence> seq;
778 std::vector<api::Sort> sorts;
779 std::vector<cvc5::api::Term> flattenVars;
782 : DECLARE_CONST_TOK { PARSER_STATE->checkThatLogicIsSet(); }
783 symbol[name,CHECK_NONE,SYM_VARIABLE]
784 { PARSER_STATE->checkUserSymbol(name); }
785 sortSymbol[t,CHECK_DECLARED]
786 { // allow overloading here
787 if( PARSER_STATE->sygus() )
789 PARSER_STATE->parseErrorLogic("declare-const is not allowed in sygus "
793 PARSER_STATE->bindVar(name, t, false, true);
794 cmd->reset(new DeclareFunctionCommand(name, c, t)); }
797 | GET_MODEL_TOK { PARSER_STATE->checkThatLogicIsSet(); }
798 { cmd->reset(new GetModelCommand()); }
802 ( simpleSymbolicExpr[s]
803 { cmd->reset(new EchoCommand(s)); }
804 | { cmd->reset(new EchoCommand()); }
807 /* reset: reset everything, returning solver to initial state.
808 * Logic and options must be set again. */
811 cmd->reset(new ResetCommand());
812 // reset the state of the parser, which is independent of the symbol
814 PARSER_STATE->reset();
816 /* reset-assertions: reset assertions, assertion stack, declarations,
817 * etc., but the logic and options remain as they were. */
818 | RESET_ASSERTIONS_TOK
819 { cmd->reset(new ResetAssertionsCommand());
822 { PARSER_STATE->checkThatLogicIsSet(); }
823 symbol[fname,CHECK_NONE,SYM_VARIABLE]
824 { PARSER_STATE->checkUserSymbol(fname); }
825 LPAREN_TOK sortedVarList[sortedVarNames] RPAREN_TOK
826 sortSymbol[t,CHECK_DECLARED]
829 PARSER_STATE->bindDefineFunRec(fname, sortedVarNames, t, flattenVars);
830 PARSER_STATE->pushDefineFunRecScope(
831 sortedVarNames, func, flattenVars, bvs);
834 { PARSER_STATE->popScope();
835 if( !flattenVars.empty() ){
836 expr = PARSER_STATE->mkHoApply( expr, flattenVars );
838 cmd->reset(new DefineFunctionRecCommand(
839 func, bvs, expr, SYM_MAN->getGlobalDeclarations()));
841 | DEFINE_FUNS_REC_TOK
842 { PARSER_STATE->checkThatLogicIsSet();}
845 symbol[fname,CHECK_UNDECLARED,SYM_VARIABLE]
846 { PARSER_STATE->checkUserSymbol(fname); }
847 LPAREN_TOK sortedVarList[sortedVarNames] RPAREN_TOK
848 sortSymbol[t,CHECK_DECLARED]
851 func = PARSER_STATE->bindDefineFunRec(
852 fname, sortedVarNames, t, flattenVars);
853 funcs.push_back( func );
855 // add to lists (need to remember for when parsing the bodies)
856 sortedVarNamesList.push_back( sortedVarNames );
857 flattenVarsList.push_back( flattenVars );
859 // set up parsing the next variable list block
860 sortedVarNames.clear();
868 //set up the first scope
869 if( sortedVarNamesList.empty() ){
870 PARSER_STATE->parseError("Must define at least one function in "
874 PARSER_STATE->pushDefineFunRecScope( sortedVarNamesList[0], funcs[0],
875 flattenVarsList[0], bvs);
880 unsigned j = func_defs.size();
881 if( !flattenVarsList[j].empty() ){
882 expr = PARSER_STATE->mkHoApply( expr, flattenVarsList[j] );
884 func_defs.push_back( expr );
885 formals.push_back(bvs);
887 //set up the next scope
888 PARSER_STATE->popScope();
889 if( func_defs.size()<funcs.size() ){
891 PARSER_STATE->pushDefineFunRecScope( sortedVarNamesList[j], funcs[j],
892 flattenVarsList[j], bvs);
897 { if( funcs.size()!=func_defs.size() ){
898 PARSER_STATE->parseError(std::string(
899 "Number of functions defined does not match number listed in "
902 cmd->reset(new DefineFunctionRecCommand(
903 funcs, formals, func_defs, SYM_MAN->getGlobalDeclarations()));
907 extendedCommand[std::unique_ptr<cvc5::Command>* cmd]
909 std::vector<api::DatatypeDecl> dts;
910 cvc5::api::Term e, e2;
911 cvc5::api::Sort t, s;
913 std::vector<std::string> names;
914 std::vector<cvc5::api::Term> terms;
915 std::vector<api::Sort> sorts;
916 std::vector<std::pair<std::string, cvc5::api::Sort> > sortedVarNames;
917 std::unique_ptr<cvc5::CommandSequence> seq;
918 api::Grammar* g = nullptr;
920 /* Extended SMT-LIB set of commands syntax, not permitted in
921 * --smtlib2 compliance mode. */
922 : DECLARE_CODATATYPE_TOK datatypeDefCommand[true, cmd]
923 | DECLARE_CODATATYPES_TOK datatypesDefCommand[true, cmd]
925 /* Support some of Z3's extended SMT-LIB commands */
929 PARSER_STATE->checkThatLogicIsSet();
930 PARSER_STATE->checkLogicAllowsFreeSorts();
931 seq.reset(new cvc5::CommandSequence());
934 ( symbol[name,CHECK_UNDECLARED,SYM_SORT]
935 { PARSER_STATE->checkUserSymbol(name);
936 api::Sort type = PARSER_STATE->mkSort(name);
937 seq->addCommand(new DeclareSortCommand(name, 0, type));
941 { cmd->reset(seq.release()); }
943 | DECLARE_FUNS_TOK { PARSER_STATE->checkThatLogicIsSet(); }
944 { seq.reset(new cvc5::CommandSequence()); }
946 ( LPAREN_TOK symbol[name,CHECK_UNDECLARED,SYM_VARIABLE]
947 { PARSER_STATE->checkUserSymbol(name); }
948 nonemptySortList[sorts] RPAREN_TOK
950 if(sorts.size() > 1) {
951 PARSER_STATE->checkLogicAllowsFunctions();
953 api::Sort range = sorts.back();
955 tt = PARSER_STATE->mkFlatFunctionType(sorts, range);
961 PARSER_STATE->bindVar(name, tt, false, true);
962 seq->addCommand(new DeclareFunctionCommand(name, func, tt));
967 { cmd->reset(seq.release()); }
968 | DECLARE_PREDS_TOK { PARSER_STATE->checkThatLogicIsSet(); }
969 { seq.reset(new cvc5::CommandSequence()); }
971 ( LPAREN_TOK symbol[name,CHECK_UNDECLARED,SYM_VARIABLE]
972 { PARSER_STATE->checkUserSymbol(name); }
973 sortList[sorts] RPAREN_TOK
974 { t = SOLVER->getBooleanSort();
975 if(sorts.size() > 0) {
976 PARSER_STATE->checkLogicAllowsFunctions();
977 t = SOLVER->mkFunctionSort(sorts, t);
981 PARSER_STATE->bindVar(name, t, false, true);
982 seq->addCommand(new DeclareFunctionCommand(name, func, t));
987 { cmd->reset(seq.release()); }
989 | DEFINE_TOK { PARSER_STATE->checkThatLogicIsSet(); }
991 symbol[name,CHECK_UNDECLARED,SYM_VARIABLE]
992 { PARSER_STATE->checkUserSymbol(name); }
995 api::Term func = PARSER_STATE->bindVar(name, e.getSort());
996 cmd->reset(new DefineFunctionCommand(
997 name, func, e, SYM_MAN->getGlobalDeclarations()));
999 | // (define (f (v U) ...) t)
1001 symbol[name,CHECK_UNDECLARED,SYM_VARIABLE]
1002 { PARSER_STATE->checkUserSymbol(name); }
1003 sortedVarList[sortedVarNames] RPAREN_TOK
1004 { /* add variables to parser state before parsing term */
1005 Debug("parser") << "define fun: '" << name << "'" << std::endl;
1006 PARSER_STATE->pushScope();
1007 terms = PARSER_STATE->bindBoundVars(sortedVarNames);
1011 PARSER_STATE->popScope();
1012 // declare the name down here (while parsing term, signature
1013 // must not be extended with the name itself; no recursion
1015 api::Sort tt = e.getSort();
1016 if( sortedVarNames.size() > 0 ) {
1017 sorts.reserve(sortedVarNames.size());
1018 for(std::vector<std::pair<std::string, api::Sort> >::const_iterator
1019 i = sortedVarNames.begin(), iend = sortedVarNames.end();
1021 sorts.push_back((*i).second);
1023 tt = SOLVER->mkFunctionSort(sorts, tt);
1025 api::Term func = PARSER_STATE->bindVar(name, tt);
1026 cmd->reset(new DefineFunctionCommand(
1027 name, func, terms, e, SYM_MAN->getGlobalDeclarations()));
1030 | // (define-const x U t)
1031 DEFINE_CONST_TOK { PARSER_STATE->checkThatLogicIsSet(); }
1032 symbol[name,CHECK_UNDECLARED,SYM_VARIABLE]
1033 { PARSER_STATE->checkUserSymbol(name); }
1034 sortSymbol[t,CHECK_DECLARED]
1037 // declare the name down here (while parsing term, signature
1038 // must not be extended with the name itself; no recursion
1040 api::Term func = PARSER_STATE->bindVar(name, t);
1041 cmd->reset(new DefineFunctionCommand(
1042 name, func, terms, e, SYM_MAN->getGlobalDeclarations()));
1045 | SIMPLIFY_TOK { PARSER_STATE->checkThatLogicIsSet(); }
1047 { cmd->reset(new SimplifyCommand(e)); }
1048 | GET_QE_TOK { PARSER_STATE->checkThatLogicIsSet(); }
1050 { cmd->reset(new GetQuantifierEliminationCommand(e, true)); }
1051 | GET_QE_DISJUNCT_TOK { PARSER_STATE->checkThatLogicIsSet(); }
1053 { cmd->reset(new GetQuantifierEliminationCommand(e, false)); }
1055 PARSER_STATE->checkThatLogicIsSet();
1057 symbol[name,CHECK_UNDECLARED,SYM_VARIABLE]
1060 sygusGrammar[g, terms, name]
1063 cmd->reset(new GetAbductCommand(name, e, g));
1065 | GET_INTERPOL_TOK {
1066 PARSER_STATE->checkThatLogicIsSet();
1068 symbol[name,CHECK_UNDECLARED,SYM_VARIABLE]
1071 sygusGrammar[g, terms, name]
1074 cmd->reset(new GetInterpolCommand(name, e, g));
1076 | DECLARE_HEAP LPAREN_TOK
1077 sortSymbol[t, CHECK_DECLARED]
1078 sortSymbol[s, CHECK_DECLARED]
1079 { cmd->reset(new DeclareHeapCommand(t, s)); }
1081 | DECLARE_POOL { PARSER_STATE->checkThatLogicIsSet(); }
1082 symbol[name,CHECK_NONE,SYM_VARIABLE]
1083 { PARSER_STATE->checkUserSymbol(name); }
1084 sortSymbol[t,CHECK_DECLARED]
1087 { terms.push_back( e ); }
1089 { Debug("parser") << "declare pool: '" << name << "'" << std::endl;
1090 api::Term pool = SOLVER->declarePool(name, t, terms);
1091 PARSER_STATE->defineVar(name, pool);
1092 cmd->reset(new DeclarePoolCommand(name, pool, t, terms));
1094 | BLOCK_MODEL_TOK { PARSER_STATE->checkThatLogicIsSet(); }
1095 { cmd->reset(new BlockModelCommand()); }
1097 | BLOCK_MODEL_VALUES_TOK { PARSER_STATE->checkThatLogicIsSet(); }
1098 ( LPAREN_TOK termList[terms,e] RPAREN_TOK
1099 { cmd->reset(new BlockModelValuesCommand(terms)); }
1101 { PARSER_STATE->parseError("The block-model-value command expects a list "
1102 "of terms. Perhaps you forgot a pair of "
1108 datatypeDefCommand[bool isCo, std::unique_ptr<cvc5::Command>* cmd]
1110 std::vector<api::DatatypeDecl> dts;
1112 std::vector<std::string> dnames;
1113 std::vector<int> arities;
1115 : { PARSER_STATE->checkThatLogicIsSet(); }
1116 symbol[name,CHECK_UNDECLARED,SYM_SORT]
1118 dnames.push_back(name);
1119 arities.push_back(-1);
1121 datatypesDef[isCo, dnames, arities, cmd]
1124 datatypesDefCommand[bool isCo, std::unique_ptr<cvc5::Command>* cmd]
1126 std::vector<api::DatatypeDecl> dts;
1128 std::vector<std::string> dnames;
1129 std::vector<int> arities;
1131 : { PARSER_STATE->checkThatLogicIsSet(); }
1132 LPAREN_TOK /* datatype definition prelude */
1133 ( LPAREN_TOK symbol[name,CHECK_UNDECLARED,SYM_SORT] n=INTEGER_LITERAL RPAREN_TOK
1134 { unsigned arity = AntlrInput::tokenToUnsigned(n);
1135 Debug("parser-dt") << "Datatype : " << name << ", arity = " << arity << std::endl;
1136 dnames.push_back(name);
1137 arities.push_back( static_cast<int>(arity) );
1142 datatypesDef[isCo, dnames, arities, cmd]
1147 * Read a list of datatype definitions for datatypes with names dnames and
1148 * parametric arities arities. A negative value in arities indicates that the
1149 * arity for the corresponding datatype has not been fixed: notice that we do
1150 * not know the arity of datatypes in the declare-datatype command prior to
1151 * parsing their body, whereas the arity of datatypes in declare-datatypes is
1152 * given in the preamble of that command and thus is known prior to this call.
1154 datatypesDef[bool isCo,
1155 const std::vector<std::string>& dnames,
1156 const std::vector<int>& arities,
1157 std::unique_ptr<cvc5::Command>* cmd]
1159 std::vector<api::DatatypeDecl> dts;
1161 std::vector<api::Sort> params;
1163 : { PARSER_STATE->pushScope();
1164 // Declare the datatypes that are currently being defined as unresolved
1165 // types. If we do not know the arity of the datatype yet, we wait to
1166 // define it until parsing the preamble of its body, which may optionally
1167 // involve `par`. This is limited to the case of single datatypes defined
1168 // via declare-datatype, and hence no datatype body is parsed without
1169 // having all types declared. This ensures we can parse datatypes with
1170 // nested recursion, e.g. datatypes D having a subfield type
1172 for (unsigned i=0, dsize=dnames.size(); i<dsize; i++)
1176 // do not know the arity yet
1179 unsigned arity = static_cast<unsigned>(arities[i]);
1180 PARSER_STATE->mkUnresolvedType(dnames[i], arity);
1185 Debug("parser-dt") << "Processing datatype #" << dts.size() << std::endl;
1186 if( dts.size()>=dnames.size() ){
1187 PARSER_STATE->parseError("Too many datatypes defined in this block.");
1190 ( PAR_TOK { PARSER_STATE->pushScope(); } LPAREN_TOK
1191 ( symbol[name,CHECK_UNDECLARED,SYM_SORT]
1193 params.push_back( PARSER_STATE->mkSort(name)); }
1196 // if the arity was fixed by prelude and is not equal to the number of parameters
1197 if( arities[dts.size()]>=0 && static_cast<int>(params.size())!=arities[dts.size()] ){
1198 PARSER_STATE->parseError("Wrong number of parameters for datatype.");
1200 if (arities[dts.size()]<0)
1202 // now declare it as an unresolved type
1203 PARSER_STATE->mkUnresolvedType(dnames[dts.size()], params.size());
1205 Debug("parser-dt") << params.size() << " parameters for " << dnames[dts.size()] << std::endl;
1206 dts.push_back(SOLVER->mkDatatypeDecl(dnames[dts.size()], params, isCo));
1209 ( LPAREN_TOK constructorDef[dts.back()] RPAREN_TOK )+
1210 RPAREN_TOK { PARSER_STATE->popScope(); }
1211 | { // if the arity was fixed by prelude and is not equal to 0
1212 if( arities[dts.size()]>0 ){
1213 PARSER_STATE->parseError("No parameters given for datatype.");
1215 else if (arities[dts.size()]<0)
1217 // now declare it as an unresolved type
1218 PARSER_STATE->mkUnresolvedType(dnames[dts.size()], 0);
1220 Debug("parser-dt") << params.size() << " parameters for " << dnames[dts.size()] << std::endl;
1221 dts.push_back(SOLVER->mkDatatypeDecl(dnames[dts.size()],
1225 ( LPAREN_TOK constructorDef[dts.back()] RPAREN_TOK )+
1230 if (dts.size() != dnames.size())
1232 PARSER_STATE->parseError("Wrong number of datatypes provided.");
1234 PARSER_STATE->popScope();
1235 cmd->reset(new DatatypeDeclarationCommand(
1236 PARSER_STATE->bindMutualDatatypeTypes(dts, true)));
1240 simpleSymbolicExprNoKeyword[std::string& s]
1242 { s = AntlrInput::tokenText($INTEGER_LITERAL); }
1244 { s = AntlrInput::tokenText($DECIMAL_LITERAL); }
1246 { s = AntlrInput::tokenText($HEX_LITERAL); }
1248 { s = AntlrInput::tokenText($BINARY_LITERAL); }
1250 | symbol[s,CHECK_NONE,SYM_SORT]
1251 | tok=(ASSERT_TOK | CHECK_SAT_TOK | CHECK_SAT_ASSUMING_TOK | DECLARE_FUN_TOK
1253 | DEFINE_FUN_TOK | DEFINE_FUN_REC_TOK | DEFINE_FUNS_REC_TOK
1254 | DEFINE_SORT_TOK | GET_VALUE_TOK | GET_ASSIGNMENT_TOK
1255 | GET_ASSERTIONS_TOK | GET_PROOF_TOK | GET_UNSAT_ASSUMPTIONS_TOK
1256 | GET_UNSAT_CORE_TOK | EXIT_TOK
1257 | RESET_TOK | RESET_ASSERTIONS_TOK | SET_LOGIC_TOK | SET_INFO_TOK
1258 | GET_INFO_TOK | SET_OPTION_TOK | GET_OPTION_TOK | PUSH_TOK | POP_TOK
1259 | DECLARE_DATATYPES_TOK | GET_MODEL_TOK | ECHO_TOK | SIMPLIFY_TOK)
1260 { s = AntlrInput::tokenText($tok); }
1263 keyword[std::string& s]
1265 { s = AntlrInput::tokenText($KEYWORD); }
1268 simpleSymbolicExpr[std::string& s]
1269 : simpleSymbolicExprNoKeyword[s]
1270 | KEYWORD { s = AntlrInput::tokenText($KEYWORD); }
1273 symbolicExpr[cvc5::api::Term& sexpr]
1276 std::vector<api::Term> children;
1278 : simpleSymbolicExpr[s]
1279 { sexpr = SOLVER->mkString(PARSER_STATE->processAdHocStringEsc(s)); }
1281 ( symbolicExpr[sexpr] { children.push_back(sexpr); } )* RPAREN_TOK
1282 { sexpr = SOLVER->mkTerm(cvc5::api::SEXPR, children); }
1287 * @return the expression representing the term.
1289 term[cvc5::api::Term& expr, cvc5::api::Term& expr2]
1291 api::Kind kind = api::NULL_EXPR;
1294 cvc5::api::Sort type;
1297 : termNonVariable[expr, expr2]
1299 // a qualified identifier (section 3.6 of SMT-LIB version 2.6)
1303 expr = PARSER_STATE->parseOpToExpr(p);
1308 * Matches a non-variable term.
1309 * @return the expression expr representing the term or formula, and expr2, an
1310 * optional annotation for expr (for instance, for attributed expressions).
1312 termNonVariable[cvc5::api::Term& expr, cvc5::api::Term& expr2]
1314 Debug("parser") << "term: " << AntlrInput::tokenText(LT(1)) << std::endl;
1315 api::Kind kind = api::NULL_EXPR;
1317 std::vector<cvc5::api::Term> args;
1318 std::vector< std::pair<std::string, cvc5::api::Sort> > sortedVarNames;
1319 cvc5::api::Term bvl;
1320 cvc5::api::Term f, f2, f3;
1322 cvc5::api::Term attexpr;
1323 std::vector<cvc5::api::Term> patexprs;
1324 std::vector<cvc5::api::Term> matchcases;
1325 std::unordered_set<std::string> names;
1326 std::vector< std::pair<std::string, cvc5::api::Term> > binders;
1327 cvc5::api::Sort type;
1328 cvc5::api::Sort type2;
1331 std::vector<api::Sort> argTypes;
1333 : LPAREN_TOK quantOp[kind]
1335 if (!PARSER_STATE->isTheoryEnabled(theory::THEORY_QUANTIFIERS))
1337 PARSER_STATE->parseError("Quantifier used in non-quantified logic.");
1339 PARSER_STATE->pushScope();
1342 term[f, f2] RPAREN_TOK
1344 args.push_back(bvl);
1346 PARSER_STATE->popScope();
1351 expr = MK_TERM(kind, args);
1353 | LPAREN_TOK COMPREHENSION_TOK
1354 { PARSER_STATE->pushScope(); }
1357 args.push_back(bvl);
1359 term[f, f2] { args.push_back(f); }
1362 expr = MK_TERM(api::COMPREHENSION, args);
1365 | LPAREN_TOK qualIdentifier[p]
1366 termList[args,expr] RPAREN_TOK
1368 expr = PARSER_STATE->applyParseOp(p, args);
1370 | /* a let or sygus let binding */
1373 { PARSER_STATE->pushScope(); }
1374 ( LPAREN_TOK symbol[name,CHECK_NONE,SYM_VARIABLE]
1377 // this is a parallel let, so we have to save up all the contributions
1378 // of the let and define them only later on
1379 { if(names.count(name) == 1) {
1380 std::stringstream ss;
1381 ss << "warning: symbol `" << name << "' bound multiple times by let;"
1382 << " the last binding will be used, shadowing earlier ones";
1383 PARSER_STATE->warning(ss.str());
1387 binders.push_back(std::make_pair(name, expr)); } )+
1388 { // now implement these bindings
1389 for (const std::pair<std::string, api::Term>& binder : binders)
1392 PARSER_STATE->defineVar(binder.first, binder.second);
1399 { PARSER_STATE->popScope(); }
1400 | /* match expression */
1401 LPAREN_TOK MATCH_TOK term[expr, f2] {
1402 if( !expr.getSort().isDatatype() ){
1403 PARSER_STATE->parseError("Cannot match on non-datatype term.");
1408 // case with non-nullary pattern
1409 LPAREN_TOK LPAREN_TOK term[f, f2] {
1411 PARSER_STATE->pushScope();
1412 // f should be a constructor
1414 Debug("parser-dt") << "Pattern head : " << f << " " << type << std::endl;
1415 if (!type.isConstructor())
1417 PARSER_STATE->parseError("Pattern must be application of a constructor or a variable.");
1419 api::Datatype dt = type.getConstructorCodomainSort().getDatatype();
1420 if (dt.isParametric())
1422 // lookup constructor by name
1423 api::DatatypeConstructor dc = dt.getConstructor(f.toString());
1424 api::Term scons = dc.getSpecializedConstructorTerm(expr.getSort());
1425 // take the type of the specialized constructor instead
1426 type = scons.getSort();
1428 argTypes = type.getConstructorDomainSorts();
1430 // arguments of the pattern
1431 ( symbol[name,CHECK_NONE,SYM_VARIABLE] {
1432 if (args.size() >= argTypes.size())
1434 PARSER_STATE->parseError("Too many arguments for pattern.");
1436 //make of proper type
1437 api::Term arg = PARSER_STATE->bindBoundVar(name, argTypes[args.size()]);
1438 args.push_back( arg );
1441 RPAREN_TOK term[f3, f2] {
1442 // make the match case
1443 std::vector<cvc5::api::Term> cargs;
1445 cargs.insert(cargs.end(),args.begin(),args.end());
1446 api::Term c = MK_TERM(api::APPLY_CONSTRUCTOR,cargs);
1447 api::Term bvla = MK_TERM(api::BOUND_VAR_LIST,args);
1448 api::Term mc = MK_TERM(api::MATCH_BIND_CASE, bvla, c, f3);
1449 matchcases.push_back(mc);
1450 // now, pop the scope
1451 PARSER_STATE->popScope();
1454 // case with nullary or variable pattern
1455 | LPAREN_TOK symbol[name,CHECK_NONE,SYM_VARIABLE] {
1456 if (PARSER_STATE->isDeclared(name,SYM_VARIABLE))
1458 f = PARSER_STATE->getVariable(name);
1460 if (!type.isConstructor() ||
1461 !type.getConstructorDomainSorts().empty())
1463 PARSER_STATE->parseError("Must apply constructors of arity greater than 0 to arguments in pattern.");
1465 // make nullary constructor application
1466 f = MK_TERM(api::APPLY_CONSTRUCTOR, f);
1470 // it has the type of the head expr
1471 f = PARSER_STATE->bindBoundVar(name, expr.getSort());
1476 if (f.getKind() == api::VARIABLE)
1478 api::Term bvlf = MK_TERM(api::BOUND_VAR_LIST, f);
1479 mc = MK_TERM(api::MATCH_BIND_CASE, bvlf, f, f3);
1483 mc = MK_TERM(api::MATCH_CASE, f, f3);
1485 matchcases.push_back(mc);
1489 RPAREN_TOK RPAREN_TOK {
1490 //now, make the match
1491 if (matchcases.empty())
1493 PARSER_STATE->parseError("Must have at least one case in match.");
1495 std::vector<api::Term> mchildren;
1496 mchildren.push_back(expr);
1497 mchildren.insert(mchildren.end(), matchcases.begin(), matchcases.end());
1498 expr = MK_TERM(api::MATCH, mchildren);
1501 /* attributed expressions */
1502 | LPAREN_TOK ATTRIBUTE_TOK term[expr, f2]
1503 ( attribute[expr, attexpr]
1504 { if( ! attexpr.isNull()) {
1505 patexprs.push_back( attexpr );
1510 if(! patexprs.empty()) {
1511 if( !f2.isNull() && f2.getKind()==api::INST_PATTERN_LIST ){
1512 for( size_t i=0; i<f2.getNumChildren(); i++ ){
1513 patexprs.push_back( f2[i] );
1516 expr2 = MK_TERM(api::INST_PATTERN_LIST, patexprs);
1522 LPAREN_TOK HO_LAMBDA_TOK
1523 { PARSER_STATE->pushScope(); }
1525 term[f, f2] RPAREN_TOK
1527 args.push_back(bvl);
1529 PARSER_STATE->popScope();
1530 expr = MK_TERM(api::LAMBDA, args);
1532 | LPAREN_TOK TUPLE_CONST_TOK termList[args,expr] RPAREN_TOK
1534 std::vector<api::Sort> sorts;
1535 std::vector<api::Term> terms;
1536 for (const api::Term& arg : args)
1538 sorts.emplace_back(arg.getSort());
1539 terms.emplace_back(arg);
1541 expr = SOLVER->mkTuple(sorts, terms);
1543 | LPAREN_TOK TUPLE_PROJECT_TOK term[expr,expr2] RPAREN_TOK
1545 std::vector<uint32_t> indices;
1546 api::Op op = SOLVER->mkOp(api::TUPLE_PROJECT, indices);
1547 expr = SOLVER->mkTerm(op, expr);
1549 | /* an atomic term (a term with no subterms) */
1550 termAtomic[atomTerm] { expr = atomTerm; }
1555 * Matches a qualified identifier, which can be a combination of one or more of
1556 * the following, stored in the ParseOp utility class:
1558 * (2) A string name.
1559 * (3) An expression expr.
1562 * A qualified identifier is the generic case of function heads.
1563 * With respect to the standard definition (Section 3.6 of SMT-LIB version 2.6)
1564 * of qualified identifiers, we additionally parse:
1565 * - "Array constant specifications" of the form (as const (Array T1 T2)),
1566 * which notice are used as function heads e.g. ((as const (Array Int Int)) 0)
1567 * specifies the constant array over integers consisting of constant 0. This
1568 * is handled as if it were a special case of an operator here.
1574 * - For declared functions f, we return (2).
1575 * - For indexed functions like testers (_ is C) and bitvector extract
1576 * (_ extract n m), we return (3) for the appropriate operator.
1577 * - For tuple selectors (_ tupSel n), we return (1) and (3). api::Kind is set to
1578 * APPLY_SELECTOR, and expr is set to n, which is to be interpreted by the
1579 * caller as the n^th generic tuple selector. We do this since there is no
1580 * AST expression representing generic tuple select, and we do not have enough
1581 * type information at this point to know the type of the tuple we will be
1584 * (Ascripted Identifiers)
1586 * - For ascripted nullary parametric datatype constructors like
1587 * (as nil (List Int)), we return (APPLY_CONSTRUCTOR C) for the appropriate
1588 * specialized constructor C as (3).
1589 * - For ascripted non-nullary parametric datatype constructors like
1590 * (as cons (List Int)), we return the appropriate specialized constructor C
1592 * - Overloaded non-parametric constructors (as C T) return the appropriate
1593 * expression, analogous to the parametric cases above.
1594 * - For other ascripted nullary constants like (as emptyset (Set T)),
1595 * (as sep.nil T), we return the appropriate expression (3).
1596 * - For array constant specifications (as const (Array T1 T2)), we return (1)
1597 * and (4), where kind is set to STORE_ALL and type is set to (Array T1 T2),
1598 * where this is to be interpreted by the caller as converting the next parsed
1599 * constant of type T2 to an Array of type (Array T1 T2) over that constant.
1600 * - For ascriptions on normal symbols (as f T), we return the appropriate
1601 * expression (3), which may involve disambiguating f based on type T if it is
1604 qualIdentifier[cvc5::ParseOp& p]
1607 std::string baseName;
1609 cvc5::api::Sort type;
1613 ( CONST_TOK sortSymbol[type, CHECK_DECLARED]
1615 p.d_kind = api::CONST_ARRAY;
1616 PARSER_STATE->parseOpApplyTypeAscription(p, type);
1619 sortSymbol[type, CHECK_DECLARED]
1621 PARSER_STATE->parseOpApplyTypeAscription(p, type);
1628 * Matches an identifier, which can be a combination of one or more of the
1629 * following, stored in the ParseOp utility class:
1631 * (2) A string name.
1632 * (3) An expression expr.
1633 * For examples, see documentation of qualIdentifier.
1635 identifier[cvc5::ParseOp& p]
1639 std::vector<uint64_t> numerals;
1641 : functionName[p.d_name, CHECK_NONE]
1643 // indexed functions
1645 | LPAREN_TOK INDEX_TOK
1646 ( TESTER_TOK term[f, f2]
1648 if (f.getKind() == api::APPLY_CONSTRUCTOR && f.getNumChildren() == 1)
1650 // for nullary constructors, must get the operator
1653 if (!f.getSort().isConstructor())
1655 PARSER_STATE->parseError(
1656 "Bad syntax for test (_ is X), X must be a constructor.");
1658 // get the datatype that f belongs to
1659 api::Sort sf = f.getSort().getConstructorCodomainSort();
1660 api::Datatype d = sf.getDatatype();
1662 api::DatatypeConstructor dc = d.getConstructor(f.toString());
1663 p.d_expr = dc.getTesterTerm();
1665 | UPDATE_TOK term[f, f2]
1667 if (!f.getSort().isSelector())
1669 PARSER_STATE->parseError(
1670 "Bad syntax for test (_ update X), X must be a selector.");
1672 std::string sname = f.toString();
1673 // get the datatype that f belongs to
1674 api::Sort sf = f.getSort().getSelectorDomainSort();
1675 api::Datatype d = sf.getDatatype();
1676 // find the selector
1677 api::DatatypeSelector ds = d.getSelector(f.toString());
1678 // get the updater term
1679 p.d_expr = ds.getUpdaterTerm();
1681 | TUPLE_SEL_TOK m=INTEGER_LITERAL
1683 // we adopt a special syntax (_ tupSel n)
1684 p.d_kind = api::APPLY_SELECTOR;
1685 // put m in expr so that the caller can deal with this case
1686 p.d_expr = SOLVER->mkInteger(AntlrInput::tokenToUnsigned($m));
1688 | TUPLE_PROJECT_TOK nonemptyNumeralList[numerals]
1690 // we adopt a special syntax (_ tuple_project i_1 ... i_n) where
1691 // i_1, ..., i_n are numerals
1692 p.d_kind = api::TUPLE_PROJECT;
1693 std::vector<uint32_t> indices(numerals.size());
1694 for(size_t i = 0; i < numerals.size(); ++i)
1696 // convert uint64_t to uint32_t
1697 indices[i] = numerals[i];
1699 p.d_op = SOLVER->mkOp(api::TUPLE_PROJECT, indices);
1701 | sym=SIMPLE_SYMBOL nonemptyNumeralList[numerals]
1703 p.d_op = PARSER_STATE->mkIndexedOp(AntlrInput::tokenText($sym), numerals);
1710 * Matches an atomic term (a term with no subterms).
1711 * @return the expression expr representing the term or formula.
1713 termAtomic[cvc5::api::Term& atomTerm]
1715 cvc5::api::Sort type;
1716 cvc5::api::Sort type2;
1718 std::vector<uint64_t> numerals;
1723 std::string intStr = AntlrInput::tokenText($INTEGER_LITERAL);
1724 atomTerm = SOLVER->mkInteger(intStr);
1728 std::string realStr = AntlrInput::tokenText($DECIMAL_LITERAL);
1729 atomTerm = SOLVER->ensureTermSort(SOLVER->mkReal(realStr),
1730 SOLVER->getRealSort());
1733 // Constants using indexed identifiers, e.g. (_ +oo 8 24) (positive infinity
1734 // as a 32-bit floating-point constant)
1735 | LPAREN_TOK INDEX_TOK
1737 sortSymbol[type,CHECK_DECLARED]
1738 sortSymbol[type2,CHECK_DECLARED]
1740 // Empty heap constant in seperation logic
1741 api::Term v1 = SOLVER->mkConst(api::Sort(type), "_emp1");
1742 api::Term v2 = SOLVER->mkConst(api::Sort(type2), "_emp2");
1743 atomTerm = SOLVER->mkTerm(api::SEP_EMP, v1, v2);
1745 | CHAR_TOK HEX_LITERAL
1747 std::string hexStr = AntlrInput::tokenTextSubstr($HEX_LITERAL, 2);
1748 atomTerm = PARSER_STATE->mkCharConstant(hexStr);
1750 | sym=SIMPLE_SYMBOL nonemptyNumeralList[numerals]
1753 PARSER_STATE->mkIndexedConstant(AntlrInput::tokenText($sym),
1759 // Bit-vector constants
1762 Assert(AntlrInput::tokenText($HEX_LITERAL).find("#x") == 0);
1763 std::string hexStr = AntlrInput::tokenTextSubstr($HEX_LITERAL, 2);
1764 atomTerm = SOLVER->mkBitVector(hexStr.size() * 4, hexStr, 16);
1768 Assert(AntlrInput::tokenText($BINARY_LITERAL).find("#b") == 0);
1769 std::string binStr = AntlrInput::tokenTextSubstr($BINARY_LITERAL, 2);
1770 atomTerm = SOLVER->mkBitVector(binStr.size(), binStr, 2);
1774 | str[s,false] { atomTerm = PARSER_STATE->mkStringConstant(s); }
1776 // NOTE: Theory constants go here
1778 // Empty tuple constant
1781 atomTerm = SOLVER->mkTuple(std::vector<api::Sort>(),
1782 std::vector<api::Term>());
1789 attribute[cvc5::api::Term& expr, cvc5::api::Term& retExpr]
1793 cvc5::api::Term patexpr;
1794 std::vector<cvc5::api::Term> patexprs;
1796 bool hasValue = false;
1799 : KEYWORD ( simpleSymbolicExprNoKeyword[s] { hasValue = true; } )?
1801 PARSER_STATE->attributeNotSupported(AntlrInput::tokenText($KEYWORD));
1803 | ( ATTRIBUTE_PATTERN_TOK { k = api::INST_PATTERN; } |
1804 ATTRIBUTE_POOL_TOK { k = api::INST_POOL; } |
1805 ATTRIBUTE_INST_ADD_TO_POOL_TOK { k = api::INST_ADD_TO_POOL; } |
1806 ATTRIBUTE_SKOLEM_ADD_TO_POOL_TOK{ k = api::SKOLEM_ADD_TO_POOL; }
1810 { patexprs.push_back( patexpr ); }
1813 retExpr = MK_TERM(k, patexprs);
1815 | ATTRIBUTE_NO_PATTERN_TOK term[patexpr, e2]
1817 retExpr = MK_TERM(api::INST_NO_PATTERN, patexpr);
1819 | tok=( ATTRIBUTE_INST_LEVEL ) INTEGER_LITERAL
1821 std::stringstream sIntLit;
1822 sIntLit << $INTEGER_LITERAL;
1823 api::Term keyword = SOLVER->mkString("quant-inst-max-level");
1824 api::Term n = SOLVER->mkInteger(sIntLit.str());
1825 retExpr = MK_TERM(api::INST_ATTRIBUTE, keyword, n);
1827 | tok=( ATTRIBUTE_QUANTIFIER_ID_TOK ) symbolicExpr[sexpr]
1829 api::Term keyword = SOLVER->mkString("qid");
1830 api::Term name = SOLVER->mkString(sexprToString(sexpr));
1831 retExpr = MK_TERM(api::INST_ATTRIBUTE, keyword, name);
1833 | ATTRIBUTE_NAMED_TOK symbolicExpr[sexpr]
1835 // notify that expression was given a name
1836 PARSER_STATE->notifyNamedExpression(expr, sexprToString(sexpr));
1841 * Matches a sequence of terms and puts them into the formulas
1843 * @param formulas the vector to fill with terms
1844 * @param expr an cvc5::api::Term reference for the elements of the sequence
1846 /* NOTE: We pass an cvc5::api::Term in here just to avoid allocating a fresh cvc5::api::Term every
1847 * time through this rule. */
1848 termList[std::vector<cvc5::api::Term>& formulas, cvc5::api::Term& expr]
1850 cvc5::api::Term expr2;
1852 : ( term[expr, expr2] { formulas.push_back(expr); } )+
1856 * Matches a string, and strips off the quotes.
1858 str[std::string& s, bool fsmtlib]
1861 s = AntlrInput::tokenText($STRING_LITERAL);
1862 /* strip off the quotes */
1863 s = s.substr(1, s.size() - 2);
1864 for (size_t i = 0; i < s.size(); i++)
1866 if ((unsigned)s[i] > 127 && !isprint(s[i]))
1868 PARSER_STATE->parseError(
1869 "Extended/unprintable characters are not "
1870 "part of SMT-LIB, and they must be encoded "
1871 "as escape sequences");
1874 if (fsmtlib || PARSER_STATE->escapeDupDblQuote())
1876 char* p_orig = strdup(s.c_str());
1877 char *p = p_orig, *q = p_orig;
1880 if (PARSER_STATE->escapeDupDblQuote() && *q == '"')
1882 // Handle SMT-LIB >=2.5 standard escape '""'.
1886 else if (!PARSER_STATE->escapeDupDblQuote() && *q == '\\')
1889 // Handle SMT-LIB 2.0 standard escapes '\\' and '\"'.
1890 if (*q != '\\' && *q != '"')
1905 quantOp[cvc5::api::Kind& kind]
1907 Debug("parser") << "quant: " << AntlrInput::tokenText(LT(1)) << std::endl;
1909 : EXISTS_TOK { $kind = api::EXISTS; }
1910 | FORALL_TOK { $kind = api::FORALL; }
1914 * Matches a (possibly undeclared) function symbol (returning the string)
1915 * @param check what kind of check to do with the symbol
1917 functionName[std::string& name, cvc5::parser::DeclarationCheck check]
1918 : symbol[name,check,SYM_VARIABLE]
1922 * Matches a sequence of sort symbols and fills them into the given
1925 sortList[std::vector<cvc5::api::Sort>& sorts]
1929 : ( sortSymbol[t,CHECK_DECLARED] { sorts.push_back(t); } )*
1932 nonemptySortList[std::vector<cvc5::api::Sort>& sorts]
1936 : ( sortSymbol[t,CHECK_DECLARED] { sorts.push_back(t); } )+
1940 * Matches a sequence of (variable,sort) symbol pairs and fills them
1941 * into the given vector.
1943 sortedVarList[std::vector<std::pair<std::string, cvc5::api::Sort> >& sortedVars]
1948 : ( LPAREN_TOK symbol[name,CHECK_NONE,SYM_VARIABLE]
1949 sortSymbol[t,CHECK_DECLARED] RPAREN_TOK
1950 { sortedVars.push_back(make_pair(name, t)); }
1955 * Matches a sequence of (variable, sort) symbol pairs, registers them as bound
1956 * variables, and returns a term corresponding to the list of pairs.
1958 boundVarList[cvc5::api::Term& expr]
1960 std::vector<std::pair<std::string, cvc5::api::Sort>> sortedVarNames;
1962 : LPAREN_TOK sortedVarList[sortedVarNames] RPAREN_TOK
1964 std::vector<cvc5::api::Term> args =
1965 PARSER_STATE->bindBoundVars(sortedVarNames);
1966 expr = MK_TERM(api::BOUND_VAR_LIST, args);
1971 * Matches the sort symbol, which can be an arbitrary symbol.
1972 * @param check the check to perform on the name
1974 sortName[std::string& name, cvc5::parser::DeclarationCheck check]
1975 : symbol[name,check,SYM_SORT]
1978 sortSymbol[cvc5::api::Sort& t, cvc5::parser::DeclarationCheck check]
1981 std::vector<cvc5::api::Sort> args;
1982 std::vector<uint64_t> numerals;
1983 bool indexed = false;
1985 : sortName[name,CHECK_NONE]
1987 if(check == CHECK_DECLARED || PARSER_STATE->isDeclared(name, SYM_SORT)) {
1988 t = PARSER_STATE->getSort(name);
1990 t = PARSER_STATE->mkUnresolvedType(name);
1993 | LPAREN_TOK (INDEX_TOK {indexed = true;} | {indexed = false;})
1994 symbol[name,CHECK_NONE,SYM_SORT]
1995 ( nonemptyNumeralList[numerals]
1999 std::stringstream ss;
2000 ss << "SMT-LIB requires use of an indexed sort here, e.g. (_ " << name
2002 PARSER_STATE->parseError(ss.str());
2004 if( name == "BitVec" ) {
2005 if( numerals.size() != 1 ) {
2006 PARSER_STATE->parseError("Illegal bitvector type.");
2008 if(numerals.front() == 0) {
2009 PARSER_STATE->parseError("Illegal bitvector size: 0");
2011 t = SOLVER->mkBitVectorSort(numerals.front());
2012 } else if ( name == "FloatingPoint" ) {
2013 if( numerals.size() != 2 ) {
2014 PARSER_STATE->parseError("Illegal floating-point type.");
2016 if(!validExponentSize(numerals[0])) {
2017 PARSER_STATE->parseError("Illegal floating-point exponent size");
2019 if(!validSignificandSize(numerals[1])) {
2020 PARSER_STATE->parseError("Illegal floating-point significand size");
2022 t = SOLVER->mkFloatingPointSort(numerals[0],numerals[1]);
2024 std::stringstream ss;
2025 ss << "unknown indexed sort symbol `" << name << "'";
2026 PARSER_STATE->parseError(ss.str());
2031 std::stringstream ss;
2032 ss << "Unexpected use of indexing operator `_' before `" << name
2033 << "', try leaving it out";
2034 PARSER_STATE->parseError(ss.str());
2037 PARSER_STATE->parseError("Extra parentheses around sort name not "
2038 "permitted in SMT-LIB");
2039 } else if(name == "Array" &&
2040 PARSER_STATE->isTheoryEnabled(theory::THEORY_ARRAYS) ) {
2041 if(args.size() != 2) {
2042 PARSER_STATE->parseError("Illegal array type.");
2044 t = SOLVER->mkArraySort( args[0], args[1] );
2045 } else if(name == "Set" &&
2046 PARSER_STATE->isTheoryEnabled(theory::THEORY_SETS) ) {
2047 if(args.size() != 1) {
2048 PARSER_STATE->parseError("Illegal set type.");
2050 t = SOLVER->mkSetSort( args[0] );
2052 else if(name == "Bag" &&
2053 PARSER_STATE->isTheoryEnabled(theory::THEORY_BAGS) ) {
2054 if(args.size() != 1) {
2055 PARSER_STATE->parseError("Illegal bag type.");
2057 t = SOLVER->mkBagSort( args[0] );
2059 else if(name == "Seq" && !PARSER_STATE->strictModeEnabled() &&
2060 PARSER_STATE->isTheoryEnabled(theory::THEORY_STRINGS) ) {
2061 if(args.size() != 1) {
2062 PARSER_STATE->parseError("Illegal sequence type.");
2064 t = SOLVER->mkSequenceSort( args[0] );
2065 } else if (name == "Tuple" && !PARSER_STATE->strictModeEnabled()) {
2066 t = SOLVER->mkTupleSort(args);
2067 } else if(check == CHECK_DECLARED ||
2068 PARSER_STATE->isDeclared(name, SYM_SORT)) {
2069 t = PARSER_STATE->getSort(name, args);
2071 // make unresolved type
2073 t = PARSER_STATE->mkUnresolvedType(name);
2074 Debug("parser-param") << "param: make unres type " << name
2077 t = PARSER_STATE->mkUnresolvedTypeConstructor(name,args);
2078 t = t.instantiate( args );
2079 Debug("parser-param")
2080 << "param: make unres param type " << name << " " << args.size()
2081 << " " << PARSER_STATE->getArity( name ) << std::endl;
2086 | LPAREN_TOK HO_ARROW_TOK sortList[args] RPAREN_TOK
2089 PARSER_STATE->parseError("Arrow types must have at least 2 arguments");
2092 api::Sort rangeType = args.back();
2094 t = PARSER_STATE->mkFlatFunctionType( args, rangeType );
2099 * Matches a list of symbols, with check and type arguments as for the
2100 * symbol[] rule below.
2102 symbolList[std::vector<std::string>& names,
2103 cvc5::parser::DeclarationCheck check,
2104 cvc5::parser::SymbolType type]
2108 : ( symbol[id,check,type] { names.push_back(id); } )*
2112 * Matches an symbol and sets the string reference parameter id.
2113 * @param id string to hold the symbol
2114 * @param check what kinds of check to do on the symbol
2115 * @param type the intended namespace for the symbol
2117 symbol[std::string& id,
2118 cvc5::parser::DeclarationCheck check,
2119 cvc5::parser::SymbolType type]
2121 { id = AntlrInput::tokenText($SIMPLE_SYMBOL);
2122 if(!PARSER_STATE->isAbstractValue(id)) {
2123 // if an abstract value, SmtEngine handles declaration
2124 PARSER_STATE->checkDeclaration(id, check, type);
2128 { id = AntlrInput::tokenText($QUOTED_SYMBOL);
2129 /* strip off the quotes */
2130 id = id.substr(1, id.size() - 2);
2131 if(!PARSER_STATE->isAbstractValue(id)) {
2132 // if an abstract value, SmtEngine handles declaration
2133 PARSER_STATE->checkDeclaration(id, check, type);
2136 | UNTERMINATED_QUOTED_SYMBOL
2138 { PARSER_STATE->unexpectedEOF("unterminated |quoted| symbol"); }
2140 { PARSER_STATE->unexpectedEOF("backslash not permitted in |quoted| "
2146 * Matches a nonempty list of numerals.
2147 * @param numerals the (empty) vector to house the numerals.
2149 nonemptyNumeralList[std::vector<uint64_t>& numerals]
2151 { numerals.push_back(AntlrInput::tokenToUnsigned($INTEGER_LITERAL)); }
2156 * Parses a datatype definition
2158 datatypeDef[bool isCo, std::vector<cvc5::api::DatatypeDecl>& datatypes,
2159 std::vector< cvc5::api::Sort >& params]
2163 /* This really needs to be CHECK_NONE, or mutually-recursive
2164 * datatypes won't work, because this type will already be
2165 * "defined" as an unresolved type; don't worry, we check
2167 : symbol[id,CHECK_NONE,SYM_SORT] { PARSER_STATE->pushScope(); }
2169 datatypes.push_back(SOLVER->mkDatatypeDecl(id, params, isCo));
2171 ( LPAREN_TOK constructorDef[datatypes.back()] RPAREN_TOK )+
2172 { PARSER_STATE->popScope(); }
2176 * Parses a constructor defintion for type
2178 constructorDef[cvc5::api::DatatypeDecl& type]
2181 cvc5::api::DatatypeConstructorDecl* ctor = NULL;
2183 : symbol[id,CHECK_NONE,SYM_VARIABLE]
2185 ctor = new api::DatatypeConstructorDecl(
2186 SOLVER->mkDatatypeConstructorDecl(id));
2188 ( LPAREN_TOK selector[*ctor] RPAREN_TOK )*
2189 { // make the constructor
2190 type.addConstructor(*ctor);
2191 Debug("parser-idt") << "constructor: " << id.c_str() << std::endl;
2196 selector[cvc5::api::DatatypeConstructorDecl& ctor]
2199 cvc5::api::Sort t, t2;
2201 : symbol[id,CHECK_NONE,SYM_SORT] sortSymbol[t,CHECK_NONE]
2203 ctor.addSelector(id, t);
2204 Debug("parser-idt") << "selector: " << id.c_str()
2205 << " of type " << t << std::endl;
2209 // Base SMT-LIB tokens
2210 ASSERT_TOK : 'assert';
2211 CHECK_SAT_TOK : 'check-sat';
2212 CHECK_SAT_ASSUMING_TOK : 'check-sat-assuming';
2213 DECLARE_FUN_TOK : 'declare-fun';
2214 DECLARE_SORT_TOK : 'declare-sort';
2215 DEFINE_FUN_TOK : 'define-fun';
2216 DEFINE_FUN_REC_TOK : 'define-fun-rec';
2217 DEFINE_FUNS_REC_TOK : 'define-funs-rec';
2218 DEFINE_SORT_TOK : 'define-sort';
2219 GET_VALUE_TOK : 'get-value';
2220 GET_ASSIGNMENT_TOK : 'get-assignment';
2221 GET_ASSERTIONS_TOK : 'get-assertions';
2222 GET_PROOF_TOK : 'get-proof';
2223 GET_UNSAT_ASSUMPTIONS_TOK : 'get-unsat-assumptions';
2224 GET_UNSAT_CORE_TOK : 'get-unsat-core';
2226 RESET_TOK : 'reset';
2227 RESET_ASSERTIONS_TOK : 'reset-assertions';
2229 ATTRIBUTE_TOK : '!';
2233 SET_LOGIC_TOK : 'set-logic';
2234 SET_INFO_TOK : 'set-info';
2235 GET_INFO_TOK : 'get-info';
2236 SET_OPTION_TOK : 'set-option';
2237 GET_OPTION_TOK : 'get-option';
2241 CONST_TOK : { !PARSER_STATE->strictModeEnabled() }? 'const';
2243 // extended commands
2244 DECLARE_CODATATYPE_TOK : { PARSER_STATE->v2_6() || PARSER_STATE->sygus() }? 'declare-codatatype';
2245 DECLARE_DATATYPE_TOK : { PARSER_STATE->v2_6() || PARSER_STATE->sygus() }? 'declare-datatype';
2246 DECLARE_DATATYPES_2_5_TOK : { !( PARSER_STATE->v2_6() || PARSER_STATE->sygus() ) }?'declare-datatypes';
2247 DECLARE_DATATYPES_TOK : { PARSER_STATE->v2_6() || PARSER_STATE->sygus() }?'declare-datatypes';
2248 DECLARE_CODATATYPES_2_5_TOK : { !( PARSER_STATE->v2_6() || PARSER_STATE->sygus() ) }?'declare-codatatypes';
2249 DECLARE_CODATATYPES_TOK : { PARSER_STATE->v2_6() || PARSER_STATE->sygus() }?'declare-codatatypes';
2250 PAR_TOK : { PARSER_STATE->v2_6() || PARSER_STATE->sygus() }?'par';
2251 COMPREHENSION_TOK : { PARSER_STATE->isTheoryEnabled(theory::THEORY_SETS) }?'comprehension';
2252 TESTER_TOK : { ( PARSER_STATE->v2_6() || PARSER_STATE->sygus() ) && PARSER_STATE->isTheoryEnabled(theory::THEORY_DATATYPES) }?'is';
2253 UPDATE_TOK : { ( PARSER_STATE->v2_6() || PARSER_STATE->sygus() ) && PARSER_STATE->isTheoryEnabled(theory::THEORY_DATATYPES) }?'update';
2254 MATCH_TOK : { ( PARSER_STATE->v2_6() || PARSER_STATE->sygus() ) && PARSER_STATE->isTheoryEnabled(theory::THEORY_DATATYPES) }?'match';
2255 GET_MODEL_TOK : 'get-model';
2256 BLOCK_MODEL_TOK : 'block-model';
2257 BLOCK_MODEL_VALUES_TOK : 'block-model-values';
2259 DECLARE_SORTS_TOK : 'declare-sorts';
2260 DECLARE_FUNS_TOK : 'declare-funs';
2261 DECLARE_PREDS_TOK : 'declare-preds';
2262 DEFINE_TOK : 'define';
2263 DECLARE_CONST_TOK : 'declare-const';
2264 DEFINE_CONST_TOK : 'define-const';
2265 SIMPLIFY_TOK : 'simplify';
2266 INCLUDE_TOK : 'include';
2267 GET_QE_TOK : 'get-qe';
2268 GET_QE_DISJUNCT_TOK : 'get-qe-disjunct';
2269 GET_ABDUCT_TOK : 'get-abduct';
2270 GET_INTERPOL_TOK : 'get-interpol';
2271 DECLARE_HEAP : 'declare-heap';
2272 DECLARE_POOL : 'declare-pool';
2275 SYNTH_FUN_TOK : { PARSER_STATE->sygus() }?'synth-fun';
2276 SYNTH_INV_TOK : { PARSER_STATE->sygus()}?'synth-inv';
2277 CHECK_SYNTH_TOK : { PARSER_STATE->sygus()}?'check-synth';
2278 DECLARE_VAR_TOK : { PARSER_STATE->sygus()}?'declare-var';
2279 CONSTRAINT_TOK : { PARSER_STATE->sygus()}?'constraint';
2280 ASSUME_TOK : { PARSER_STATE->sygus()}?'assume';
2281 INV_CONSTRAINT_TOK : { PARSER_STATE->sygus()}?'inv-constraint';
2282 SET_FEATURE_TOK : { PARSER_STATE->sygus() }? 'set-feature';
2283 SYGUS_CONSTANT_TOK : { PARSER_STATE->sygus() }? 'Constant';
2284 SYGUS_VARIABLE_TOK : { PARSER_STATE->sygus() }? 'Variable';
2287 ATTRIBUTE_PATTERN_TOK : ':pattern';
2288 ATTRIBUTE_NO_PATTERN_TOK : ':no-pattern';
2289 ATTRIBUTE_POOL_TOK : ':pool';
2290 ATTRIBUTE_INST_ADD_TO_POOL_TOK : ':inst-add-to-pool';
2291 ATTRIBUTE_SKOLEM_ADD_TO_POOL_TOK : ':skolem-add-to-pool';
2292 ATTRIBUTE_NAMED_TOK : ':named';
2293 ATTRIBUTE_INST_LEVEL : ':quant-inst-max-level';
2294 ATTRIBUTE_QUANTIFIER_ID_TOK : ':qid';
2296 // operators (NOTE: theory symbols go here)
2297 EXISTS_TOK : 'exists';
2298 FORALL_TOK : 'forall';
2300 EMP_TOK : { PARSER_STATE->isTheoryEnabled(theory::THEORY_SEP) }? 'emp';
2301 CHAR_TOK : { PARSER_STATE->isTheoryEnabled(theory::THEORY_STRINGS) }? 'char';
2302 TUPLE_CONST_TOK: { PARSER_STATE->isTheoryEnabled(theory::THEORY_DATATYPES) }? 'mkTuple';
2303 TUPLE_SEL_TOK: { PARSER_STATE->isTheoryEnabled(theory::THEORY_DATATYPES) }? 'tupSel';
2304 TUPLE_PROJECT_TOK: { PARSER_STATE->isTheoryEnabled(theory::THEORY_DATATYPES) }? 'tuple_project';
2306 HO_ARROW_TOK : { PARSER_STATE->isHoEnabled() }? '->';
2307 HO_LAMBDA_TOK : { PARSER_STATE->isHoEnabled() }? 'lambda';
2310 * A sequence of printable ASCII characters (except backslash) that starts
2311 * and ends with | and does not otherwise contain |.
2313 * You shouldn't generally use this in parser rules, as the |quoting|
2314 * will be part of the token text. Use the symbol[] parser rule instead.
2317 : '|' ~('|' | '\\')* '|'
2319 UNTERMINATED_QUOTED_SYMBOL
2320 : '|' ~('|' | '\\')*
2324 * Matches a keyword from the input. A keyword is a simple symbol prefixed
2328 : ':' (ALPHA | DIGIT | SYMBOL_CHAR)+
2332 * Matches a "simple" symbol: a non-empty sequence of letters, digits and
2333 * the characters + - / * = % ? ! . $ ~ & ^ < > @ that does not start with a
2334 * digit, and is not the special reserved symbols '!' or '_'.
2337 : ALPHA (ALPHA | DIGIT | SYMBOL_CHAR)*
2338 | SYMBOL_CHAR (ALPHA | DIGIT | SYMBOL_CHAR)+
2339 | SYMBOL_CHAR_NOUNDERSCORE_NOATTRIBUTE
2343 * Matches and skips whitespace in the input.
2346 : (' ' | '\t' | '\f' | '\r' | '\n')+ { SKIP(); }
2350 * Matches an integer constant from the input (non-empty sequence of
2351 * digits, with no leading zeroes).
2358 * Match an integer constant. In non-strict mode, this is any sequence
2359 * of digits. In strict mode, non-zero integers can't have leading
2364 char *start = (char*) GETCHARINDEX();
2367 { Debug("parser-extra") << "NUMERAL: "
2368 << (uintptr_t)start << ".." << GETCHARINDEX()
2369 << " strict? " << (bool)(PARSER_STATE->strictModeEnabled())
2370 << " ^0? " << (bool)(*start == '0')
2371 << " len>1? " << (bool)(start < (char*)(GETCHARINDEX() - 1))
2373 { !PARSER_STATE->strictModeEnabled() ||
2375 start == (char*)(GETCHARINDEX() - 1) }?
2379 * Matches a decimal constant from the input.
2382 : NUMERAL '.' DIGIT+
2386 * Matches a hexadecimal constant.
2393 * Matches a binary constant.
2400 * Matches a double-quoted string literal. Depending on the language that is
2401 * being parsed, different escape sequences are supported:
2403 * For SMT-LIB 2.0 the sequence \" is interpreted as a double quote (") and the
2404 * sequence \\ is interpreted as a backslash (\).
2406 * For SMT-LIB >=2.5 and SyGuS a double-quote inside a string is escaped with
2407 * "", e.g., "This is a string literal with "" a single, embedded double
2410 * You shouldn't generally use this in parser rules, as the quotes
2411 * will be part of the token text. Use the str[] parser rule instead.
2414 : { !PARSER_STATE->escapeDupDblQuote() }?=>
2415 '"' ('\\' . | ~('\\' | '"'))* '"'
2416 | { PARSER_STATE->escapeDupDblQuote() }?=>
2417 '"' (~('"') | '""')* '"'
2421 * Matches the comments and ignores them
2424 : ';' (~('\n' | '\r'))* { SKIP(); }
2428 * Matches any letter ('a'-'z' and 'A'-'Z').
2437 * Matches the digits (0-9)
2439 fragment DIGIT : '0'..'9';
2441 fragment HEX_DIGIT : DIGIT | 'a'..'f' | 'A'..'F';
2444 * Matches the characters that may appear as a one-character "symbol"
2445 * (which excludes _ and !, which are reserved words in SMT-LIB).
2447 fragment SYMBOL_CHAR_NOUNDERSCORE_NOATTRIBUTE
2448 : '+' | '-' | '/' | '*' | '=' | '%' | '?' | '.' | '$' | '~'
2449 | '&' | '^' | '<' | '>' | '@'
2453 * Matches the characters that may appear in a "symbol" (i.e., an identifier)
2455 fragment SYMBOL_CHAR
2456 : SYMBOL_CHAR_NOUNDERSCORE_NOATTRIBUTE | '_' | '!'