1 /* ******************* */
4 ** Top contributors (to current version):
5 ** Morgan Deters, Andrew Reynolds, Tim King
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2019 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.\endverbatim
12 ** \brief Parser for SMT-LIB v2 input language
14 ** Parser for SMT-LIB v2 input language.
23 // Skip the default error handling, just break with exceptions
24 // defaultErrorHandler = false;
26 // Only lookahead of <= k requested (disable for LL* parsing)
27 // Note that CVC4's BoundedTokenBuffer requires a fixed k !
28 // If you change this k, change it also in smt2_input.cpp !
34 ** This file is part of the CVC4 project.
35 ** Copyright (c) 2009-2016 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.
44 /** This suppresses warnings about the redefinition of token symbols between
45 * different parsers. The redefinitions should be harmless as long as no
46 * client: (a) #include's the lexer headers for two grammars AND (b) uses the
47 * token symbol definitions.
49 #pragma GCC system_header
51 #if defined(CVC4_COMPETITION_MODE) && !defined(CVC4_SMTCOMP_APPLICATION_TRACK)
52 /* This improves performance by ~10 percent on big inputs.
53 * This option is only valid if we know the input is ASCII (or some 8-bit encoding).
54 * If we know the input is UTF-16, we can use ANTLR3_INLINE_INPUT_UTF16.
55 * Otherwise, we have to let the lexer detect the encoding at runtime.
57 # define ANTLR3_INLINE_INPUT_ASCII
58 # define ANTLR3_INLINE_INPUT_8BIT
59 #endif /* CVC4_COMPETITION_MODE && !CVC4_SMTCOMP_APPLICATION_TRACK */
61 #include "parser/antlr_tracing.h"
63 }/* @lexer::includes */
68 #include "parser/smt2/smt2.h"
69 #include "parser/antlr_input.h"
72 using namespace CVC4::parser;
75 #define PARSER_STATE ((Smt2*)LEXER->super)
76 }/* @lexer::postinclude */
82 #include "parser/antlr_tracing.h"
83 #include "parser/parse_op.h"
84 #include "parser/parser.h"
85 #include "smt/command.h"
98 * Just exists to provide the uintptr_t constructor that ANTLR
101 struct myExpr : public CVC4::api::Term {
102 myExpr() : CVC4::api::Term() {}
103 myExpr(void*) : CVC4::api::Term() {}
104 myExpr(const Expr& e) : CVC4::api::Term(e) {}
105 myExpr(const myExpr& e) : CVC4::api::Term(e) {}
106 };/* struct myExpr */
107 }/* CVC4::parser::smt2 namespace */
108 }/* CVC4::parser namespace */
110 }/* CVC4 namespace */
112 }/* @parser::includes */
114 @parser::postinclude {
119 #include <unordered_set>
122 #include "api/cvc4cpp.h"
123 #include "base/output.h"
124 #include "expr/expr.h"
125 #include "expr/kind.h"
126 #include "expr/type.h"
127 #include "options/set_language.h"
128 #include "parser/antlr_input.h"
129 #include "parser/parser.h"
130 #include "parser/smt2/smt2.h"
131 #include "util/floatingpoint.h"
132 #include "util/hash.h"
133 #include "util/integer.h"
134 #include "util/rational.h"
135 // \todo Review the need for this header
138 using namespace CVC4;
139 using namespace CVC4::parser;
141 /* These need to be macros so they can refer to the PARSER macro, which
142 * will be defined by ANTLR *after* this section. (If they were functions,
143 * PARSER would be undefined.) */
145 #define PARSER_STATE ((Smt2*)PARSER->super)
147 #define SOLVER PARSER_STATE->getSolver()
149 #define MK_TERM SOLVER->mkTerm
150 #define UNSUPPORTED PARSER_STATE->unimplementedFeature
152 }/* parser::postinclude */
155 * Parses an expression.
156 * @return the parsed expression, or the Null Expr if we've reached the
159 parseExpr returns [CVC4::parser::smt2::myExpr expr]
161 CVC4::api::Term expr2;
169 * @return the parsed command, or NULL if we've reached the end of the input
171 parseCommand returns [CVC4::Command* cmd_return = NULL]
173 std::unique_ptr<CVC4::Command> cmd;
177 cmd_return = cmd.release();
179 : LPAREN_TOK command[&cmd] RPAREN_TOK
181 /* This extended command has to be in the outermost production so that
182 * the RPAREN_TOK is properly eaten and we are in a good state to read
183 * the included file's tokens. */
184 | LPAREN_TOK INCLUDE_TOK str[name,true] RPAREN_TOK
185 { if(!PARSER_STATE->canIncludeFile()) {
186 PARSER_STATE->parseError("include-file feature was disabled for this "
189 if(PARSER_STATE->strictModeEnabled()) {
190 PARSER_STATE->parseError("Extended commands are not permitted while "
191 "operating in strict compliance mode.");
193 PARSER_STATE->includeFile(name);
194 // The command of the included file will be produced at the next
195 // parseCommand() call
196 cmd.reset(new EmptyCommand("include::" + name));
203 * Parses a SyGuS command.
204 * @return the parsed SyGuS command, or NULL if we've reached the end of the
207 parseSygus returns [CVC4::Command* cmd_return = NULL]
212 cmd_return = cmd.release();
214 : LPAREN_TOK cmd=sygusCommand RPAREN_TOK
219 * Parse the internal portion of the command, ignoring the surrounding
222 command [std::unique_ptr<CVC4::Command>* cmd]
225 std::vector<std::string> names;
226 CVC4::api::Term expr, expr2;
228 std::vector<CVC4::api::Term> terms;
229 std::vector<api::Sort> sorts;
230 std::vector<std::pair<std::string, CVC4::api::Sort> > sortedVarNames;
231 std::vector<CVC4::api::Term> flattenVars;
233 : /* set the logic */
234 SET_LOGIC_TOK symbol[name,CHECK_NONE,SYM_SORT]
236 cmd->reset(PARSER_STATE->setLogic(name));
239 SET_INFO_TOK setInfoInternal[cmd]
242 { cmd->reset(new GetInfoCommand(
243 AntlrInput::tokenText($KEYWORD).c_str() + 1));
246 SET_OPTION_TOK setOptionInternal[cmd]
248 GET_OPTION_TOK KEYWORD
249 { cmd->reset(new GetOptionCommand(
250 AntlrInput::tokenText($KEYWORD).c_str() + 1));
252 | /* sort declaration */
255 PARSER_STATE->checkThatLogicIsSet();
256 PARSER_STATE->checkLogicAllowsFreeSorts();
258 symbol[name,CHECK_UNDECLARED,SYM_SORT]
259 { PARSER_STATE->checkUserSymbol(name); }
261 { Debug("parser") << "declare sort: '" << name
262 << "' arity=" << n << std::endl;
263 unsigned arity = AntlrInput::tokenToUnsigned(n);
265 api::Sort type = PARSER_STATE->mkSort(name);
266 cmd->reset(new DeclareTypeCommand(name, 0, type.getType()));
268 api::Sort type = PARSER_STATE->mkSortConstructor(name, arity);
269 cmd->reset(new DeclareTypeCommand(name, arity, type.getType()));
272 | /* sort definition */
273 DEFINE_SORT_TOK { PARSER_STATE->checkThatLogicIsSet(); }
274 symbol[name,CHECK_UNDECLARED,SYM_SORT]
275 { PARSER_STATE->checkUserSymbol(name); }
276 LPAREN_TOK symbolList[names,CHECK_NONE,SYM_SORT] RPAREN_TOK
277 { PARSER_STATE->pushScope(true);
278 for(std::vector<std::string>::const_iterator i = names.begin(),
282 sorts.push_back(PARSER_STATE->mkSort(*i));
285 sortSymbol[t,CHECK_DECLARED]
286 { PARSER_STATE->popScope();
287 // Do NOT call mkSort, since that creates a new sort!
288 // This name is not its own distinct sort, it's an alias.
289 PARSER_STATE->defineParameterizedType(name, sorts, t.getType());
290 cmd->reset(new DefineTypeCommand(
291 name, api::sortVectorToTypes(sorts), t.getType()));
293 | /* function declaration */
294 DECLARE_FUN_TOK { PARSER_STATE->checkThatLogicIsSet(); }
295 symbol[name,CHECK_NONE,SYM_VARIABLE]
296 { PARSER_STATE->checkUserSymbol(name); }
297 LPAREN_TOK sortList[sorts] RPAREN_TOK
298 sortSymbol[t,CHECK_DECLARED]
299 { Debug("parser") << "declare fun: '" << name << "'" << std::endl;
300 if( !sorts.empty() ) {
301 t = PARSER_STATE->mkFlatFunctionType(sorts, t);
305 PARSER_STATE->checkLogicAllowsFunctions();
307 // we allow overloading for function declarations
308 if (PARSER_STATE->sygus_v1())
310 // it is a higher-order universal variable
311 api::Term func = PARSER_STATE->bindBoundVar(name, t);
313 new DeclareSygusFunctionCommand(name, func.getExpr(), t.getType()));
315 else if( PARSER_STATE->sygus() )
317 PARSER_STATE->parseErrorLogic("declare-fun are not allowed in sygus "
323 PARSER_STATE->bindVar(name, t, ExprManager::VAR_FLAG_NONE, true);
325 new DeclareFunctionCommand(name, func.getExpr(), t.getType()));
328 | /* function definition */
329 DEFINE_FUN_TOK { PARSER_STATE->checkThatLogicIsSet(); }
330 symbol[name,CHECK_UNDECLARED,SYM_VARIABLE]
331 { PARSER_STATE->checkUserSymbol(name); }
332 LPAREN_TOK sortedVarList[sortedVarNames] RPAREN_TOK
333 sortSymbol[t,CHECK_DECLARED]
334 { /* add variables to parser state before parsing term */
335 Debug("parser") << "define fun: '" << name << "'" << std::endl;
336 if( sortedVarNames.size() > 0 ) {
337 sorts.reserve(sortedVarNames.size());
338 for(std::vector<std::pair<std::string, api::Sort> >::const_iterator i =
339 sortedVarNames.begin(), iend = sortedVarNames.end();
342 sorts.push_back((*i).second);
344 t = PARSER_STATE->mkFlatFunctionType(sorts, t, flattenVars);
346 PARSER_STATE->pushScope(true);
347 terms = PARSER_STATE->bindBoundVars(sortedVarNames);
351 if( !flattenVars.empty() ){
352 // if this function has any implicit variables flattenVars,
353 // we apply the body of the definition to the flatten vars
354 expr = PARSER_STATE->mkHoApply(expr, flattenVars);
355 terms.insert(terms.end(), flattenVars.begin(), flattenVars.end());
357 PARSER_STATE->popScope();
358 // declare the name down here (while parsing term, signature
359 // must not be extended with the name itself; no recursion
361 // we allow overloading for function definitions
362 api::Term func = PARSER_STATE->bindVar(name, t,
363 ExprManager::VAR_FLAG_DEFINED, true);
364 cmd->reset(new DefineFunctionCommand(
365 name, func.getExpr(), api::termVectorToExprs(terms), expr.getExpr()));
367 | DECLARE_DATATYPE_TOK datatypeDefCommand[false, cmd]
368 | DECLARE_DATATYPES_TOK datatypesDefCommand[false, cmd]
370 GET_VALUE_TOK { PARSER_STATE->checkThatLogicIsSet(); }
371 ( LPAREN_TOK termList[terms,expr] RPAREN_TOK
372 { cmd->reset(new GetValueCommand(api::termVectorToExprs(terms))); }
374 { PARSER_STATE->parseError("The get-value command expects a list of "
375 "terms. Perhaps you forgot a pair of "
379 | /* get-assignment */
380 GET_ASSIGNMENT_TOK { PARSER_STATE->checkThatLogicIsSet(); }
381 { cmd->reset(new GetAssignmentCommand()); }
383 ASSERT_TOK { PARSER_STATE->checkThatLogicIsSet(); }
384 { PARSER_STATE->clearLastNamedTerm(); }
386 { bool inUnsatCore = PARSER_STATE->lastNamedTerm().first == expr;
387 cmd->reset(new AssertCommand(expr.getExpr(), inUnsatCore));
389 // set the expression name, if there was a named term
390 std::pair<api::Term, std::string> namedTerm =
391 PARSER_STATE->lastNamedTerm();
392 Command* csen = new SetExpressionNameCommand(namedTerm.first.getExpr(),
394 csen->setMuted(true);
395 PARSER_STATE->preemptCommand(csen);
399 CHECK_SAT_TOK { PARSER_STATE->checkThatLogicIsSet(); }
400 { if( PARSER_STATE->sygus() ){
401 PARSER_STATE->parseError("Sygus does not support check-sat command.");
405 { if(PARSER_STATE->strictModeEnabled()) {
406 PARSER_STATE->parseError(
407 "Extended commands (such as check-sat with an argument) are not "
408 "permitted while operating in strict compliance mode.");
411 | { expr = api::Term(); }
413 { cmd->reset(new CheckSatCommand(expr.getExpr())); }
414 | /* check-sat-assuming */
415 CHECK_SAT_ASSUMING_TOK { PARSER_STATE->checkThatLogicIsSet(); }
416 ( LPAREN_TOK termList[terms,expr] RPAREN_TOK
418 cmd->reset(new CheckSatAssumingCommand(api::termVectorToExprs(terms)));
421 { PARSER_STATE->parseError("The check-sat-assuming command expects a "
422 "list of terms. Perhaps you forgot a pair of "
426 | /* get-assertions */
427 GET_ASSERTIONS_TOK { PARSER_STATE->checkThatLogicIsSet(); }
428 { cmd->reset(new GetAssertionsCommand()); }
430 GET_PROOF_TOK { PARSER_STATE->checkThatLogicIsSet(); }
431 { cmd->reset(new GetProofCommand()); }
432 | /* get-unsat-assumptions */
433 GET_UNSAT_ASSUMPTIONS_TOK { PARSER_STATE->checkThatLogicIsSet(); }
434 { cmd->reset(new GetUnsatAssumptionsCommand); }
435 | /* get-unsat-core */
436 GET_UNSAT_CORE_TOK { PARSER_STATE->checkThatLogicIsSet(); }
437 { cmd->reset(new GetUnsatCoreCommand); }
439 PUSH_TOK { PARSER_STATE->checkThatLogicIsSet(); }
440 { if( PARSER_STATE->sygus() ){
441 PARSER_STATE->parseError("Sygus does not support push command.");
445 { unsigned num = AntlrInput::tokenToUnsigned(k);
447 cmd->reset(new EmptyCommand());
448 } else if(num == 1) {
449 PARSER_STATE->pushScope();
450 cmd->reset(new PushCommand());
452 std::unique_ptr<CommandSequence> seq(new CommandSequence());
454 PARSER_STATE->pushScope();
455 Command* push_cmd = new PushCommand();
456 push_cmd->setMuted(num > 1);
457 seq->addCommand(push_cmd);
460 cmd->reset(seq.release());
463 | { if(PARSER_STATE->strictModeEnabled()) {
464 PARSER_STATE->parseError(
465 "Strict compliance mode demands an integer to be provided to "
466 "PUSH. Maybe you want (push 1)?");
468 PARSER_STATE->pushScope();
469 cmd->reset(new PushCommand());
472 | POP_TOK { PARSER_STATE->checkThatLogicIsSet(); }
473 { if( PARSER_STATE->sygus() ){
474 PARSER_STATE->parseError("Sygus does not support pop command.");
478 { unsigned num = AntlrInput::tokenToUnsigned(k);
479 if(num > PARSER_STATE->scopeLevel()) {
480 PARSER_STATE->parseError("Attempted to pop above the top stack "
484 cmd->reset(new EmptyCommand());
485 } else if(num == 1) {
486 PARSER_STATE->popScope();
487 cmd->reset(new PopCommand());
489 std::unique_ptr<CommandSequence> seq(new CommandSequence());
491 PARSER_STATE->popScope();
492 Command* pop_command = new PopCommand();
493 pop_command->setMuted(num > 1);
494 seq->addCommand(pop_command);
497 cmd->reset(seq.release());
500 | { if(PARSER_STATE->strictModeEnabled()) {
501 PARSER_STATE->parseError(
502 "Strict compliance mode demands an integer to be provided to POP."
503 "Maybe you want (pop 1)?");
505 PARSER_STATE->popScope();
506 cmd->reset(new PopCommand());
512 { cmd->reset(new QuitCommand()); }
514 /* New SMT-LIB 2.5 command set */
516 { if(PARSER_STATE->v2_0() && PARSER_STATE->strictModeEnabled()) {
517 PARSER_STATE->parseError(
518 "SMT-LIB 2.5 commands are not permitted while operating in strict "
519 "compliance mode and in SMT-LIB 2.0 mode.");
523 /* CVC4-extended SMT-LIB commands */
524 | extendedCommand[cmd]
525 { if(PARSER_STATE->strictModeEnabled()) {
526 PARSER_STATE->parseError(
527 "Extended commands are not permitted while operating in strict "
534 { std::string id = AntlrInput::tokenText($SIMPLE_SYMBOL);
535 if(id == "benchmark") {
536 PARSER_STATE->parseError(
537 "In SMT-LIBv2 mode, but got something that looks like SMT-LIBv1, "
538 "which is not supported anymore.");
540 PARSER_STATE->parseError("expected SMT-LIBv2 command, got `" + id +
546 sygusCommand returns [std::unique_ptr<CVC4::Command> cmd]
548 CVC4::api::Term expr, expr2;
549 CVC4::api::Sort t, range;
550 std::vector<std::string> names;
551 std::vector<std::pair<std::string, CVC4::api::Sort> > sortedVarNames;
552 std::unique_ptr<Smt2::SynthFunFactory> synthFunFactory;
553 std::string name, fun;
555 CVC4::api::Sort grammar;
558 DECLARE_VAR_TOK { PARSER_STATE->checkThatLogicIsSet(); }
559 symbol[name,CHECK_UNDECLARED,SYM_VARIABLE]
560 { PARSER_STATE->checkUserSymbol(name); }
561 sortSymbol[t,CHECK_DECLARED]
563 api::Term var = PARSER_STATE->bindBoundVar(name, t);
564 cmd.reset(new DeclareSygusVarCommand(name, var.getExpr(), t.getType()));
566 | /* declare-primed-var */
567 DECLARE_PRIMED_VAR_TOK { PARSER_STATE->checkThatLogicIsSet(); }
568 symbol[name,CHECK_UNDECLARED,SYM_VARIABLE]
569 { PARSER_STATE->checkUserSymbol(name); }
570 sortSymbol[t,CHECK_DECLARED]
572 // spurious command, we do not need to create a variable. We only keep
573 // track of the command for sanity checking / dumping
574 cmd.reset(new DeclareSygusPrimedVarCommand(name, t.getType()));
578 ( SYNTH_FUN_V1_TOK { isInv = false; }
579 | SYNTH_INV_V1_TOK { isInv = true; range = SOLVER->getBooleanSort(); }
581 { PARSER_STATE->checkThatLogicIsSet(); }
582 symbol[fun,CHECK_UNDECLARED,SYM_VARIABLE]
583 LPAREN_TOK sortedVarList[sortedVarNames] RPAREN_TOK
584 ( sortSymbol[range,CHECK_DECLARED] )?
586 synthFunFactory.reset(new Smt2::SynthFunFactory(
587 PARSER_STATE, fun, isInv, range, sortedVarNames));
590 // optionally, read the sygus grammar
592 // `grammar` specifies the required grammar for the function to
593 // synthesize, expressed as a type
594 sygusGrammarV1[grammar, synthFunFactory->getSygusVars(), fun]
597 cmd = synthFunFactory->mkCommand(grammar);
600 ( SYNTH_FUN_TOK { isInv = false; }
601 | SYNTH_INV_TOK { isInv = true; range = SOLVER->getBooleanSort(); }
603 { PARSER_STATE->checkThatLogicIsSet(); }
604 symbol[fun,CHECK_UNDECLARED,SYM_VARIABLE]
605 LPAREN_TOK sortedVarList[sortedVarNames] RPAREN_TOK
606 ( sortSymbol[range,CHECK_DECLARED] )?
608 synthFunFactory.reset(new Smt2::SynthFunFactory(
609 PARSER_STATE, fun, isInv, range, sortedVarNames));
612 // optionally, read the sygus grammar
614 // `grammar` specifies the required grammar for the function to
615 // synthesize, expressed as a type
616 sygusGrammar[grammar, synthFunFactory->getSygusVars(), fun]
619 cmd = synthFunFactory->mkCommand(grammar);
623 PARSER_STATE->checkThatLogicIsSet();
624 Debug("parser-sygus") << "Sygus : define sygus funs..." << std::endl;
625 Debug("parser-sygus") << "Sygus : read constraint..." << std::endl;
628 { Debug("parser-sygus") << "...read constraint " << expr << std::endl;
629 cmd.reset(new SygusConstraintCommand(expr.getExpr()));
631 | /* inv-constraint */
633 ( symbol[name,CHECK_NONE,SYM_VARIABLE] { names.push_back(name); } )+
635 cmd = PARSER_STATE->invConstraint(names);
639 { PARSER_STATE->checkThatLogicIsSet(); }
641 cmd.reset(new CheckSynthCommand());
646 /** Reads a sygus grammar
648 * The resulting sygus datatype encoding the grammar is stored in ret.
649 * The argument sygus_vars indicates the sygus bound variable list, which is
650 * the argument list of the function-to-synthesize (or null if the grammar
651 * has bound variables).
652 * The argument fun is a unique identifier to avoid naming clashes for the
653 * datatypes constructed by this call.
655 sygusGrammarV1[CVC4::api::Sort & ret,
656 const std::vector<CVC4::api::Term>& sygus_vars,
657 const std::string& fun]
662 unsigned startIndex = 0;
663 std::vector<std::vector<CVC4::SygusGTerm>> sgts;
664 std::vector<api::DatatypeDecl> datatypes;
665 std::vector<api::Sort> sorts;
666 std::vector<std::vector<ParseOp>> ops;
667 std::vector<std::vector<std::string>> cnames;
668 std::vector<std::vector<std::vector<CVC4::api::Sort>>> cargs;
669 std::vector<bool> allow_const;
670 std::vector<std::vector<std::string>> unresolved_gterm_sym;
671 std::map<CVC4::api::Sort, CVC4::api::Sort> sygus_to_builtin;
672 std::map<CVC4::api::Sort, CVC4::api::Term> sygus_to_builtin_expr;
674 : LPAREN_TOK { PARSER_STATE->pushScope(); }
676 symbol[name, CHECK_NONE, SYM_VARIABLE] sortSymbol[t, CHECK_DECLARED] {
679 startIndex = datatypes.size();
681 sgts.push_back(std::vector<CVC4::SygusGTerm>());
682 sgts.back().push_back(CVC4::SygusGTerm());
683 PARSER_STATE->pushSygusDatatypeDef(t,
691 unresolved_gterm_sym);
693 if (!PARSER_STATE->isUnresolvedType(name))
695 // if not unresolved, must be undeclared
696 Debug("parser-sygus") << "Make unresolved type : " << name
698 PARSER_STATE->checkDeclaration(name, CHECK_UNDECLARED, SYM_SORT);
699 unres_t = PARSER_STATE->mkUnresolvedType(name);
703 Debug("parser-sygus") << "Get sort : " << name << std::endl;
704 unres_t = PARSER_STATE->getSort(name);
706 sygus_to_builtin[unres_t] = t;
707 Debug("parser-sygus") << "--- Read sygus grammar " << name
708 << " under function " << fun << "..."
710 << " type to resolve " << unres_t << std::endl
711 << " builtin type " << t << std::endl;
713 // Note the official spec for NTDef is missing the ( parens )
714 // but they are necessary to parse SyGuS examples
715 LPAREN_TOK(sygusGTerm[sgts.back().back(), fun] {
716 sgts.back().push_back(CVC4::SygusGTerm());
718 + RPAREN_TOK { sgts.back().pop_back(); } RPAREN_TOK)
721 unsigned numSTerms = sgts.size();
722 Debug("parser-sygus") << "--- Process " << numSTerms << " sygus gterms..."
724 for (unsigned i = 0; i < numSTerms; i++)
726 for (unsigned j = 0, size = sgts[i].size(); j < size; j++)
729 PARSER_STATE->processSygusGTerm(sgts[i][j],
737 unresolved_gterm_sym,
740 sygus_to_builtin_expr,
744 // swap index if necessary
745 Debug("parser-sygus") << "--- Making sygus datatypes..." << std::endl;
746 unsigned ndatatypes = datatypes.size();
747 for (unsigned i = 0; i < ndatatypes; i++)
749 Debug("parser-sygus") << "..." << datatypes[i].getName()
750 << " has builtin sort " << sorts[i] << std::endl;
753 if (!sygus_vars.empty())
755 bvl = MK_TERM(api::BOUND_VAR_LIST, sygus_vars);
757 for (unsigned i = 0; i < ndatatypes; i++)
759 Debug("parser-sygus") << "...make " << datatypes[i].getName()
760 << " with builtin sort " << sorts[i] << std::endl;
761 if (sorts[i].isNull())
763 PARSER_STATE->parseError(
764 "Internal error : could not infer "
765 "builtin sort for nested gterm.");
767 datatypes[i].getDatatype().setSygus(
768 sorts[i].getType(), bvl.getExpr(), allow_const[i], false);
769 PARSER_STATE->mkSygusDatatype(datatypes[i],
773 unresolved_gterm_sym[i],
776 PARSER_STATE->setSygusStartIndex(fun, startIndex, datatypes, sorts, ops);
777 PARSER_STATE->popScope();
778 Debug("parser-sygus") << "--- Make " << ndatatypes
779 << " mutual datatypes..." << std::endl;
780 for (unsigned i = 0; i < ndatatypes; i++)
782 Debug("parser-sygus") << " " << i << " : " << datatypes[i].getName()
786 std::vector<CVC4::Datatype> dtypes;
787 dtypes.reserve(ndatatypes);
789 for (api::DatatypeDecl i : datatypes)
791 dtypes.push_back(i.getDatatype());
794 std::set<Type> tset =
795 api::sortSetToTypes(PARSER_STATE->getUnresolvedSorts());
797 std::vector<DatatypeType> datatypeTypes =
798 SOLVER->getExprManager()->mkMutualDatatypeTypes(
799 dtypes, tset, ExprManager::DATATYPE_FLAG_PLACEHOLDER);
801 PARSER_STATE->getUnresolvedSorts().clear();
803 ret = datatypeTypes[0];
806 // SyGuS grammar term.
808 // fun is the name of the synth-fun this grammar term is for.
809 // This method adds N operators to ops[index], N names to cnames[index] and N
810 // type argument vectors to cargs[index] (where typically N=1)
811 // This method may also add new elements pairwise into
812 // datatypes/sorts/ops/cnames/cargs in the case of non-flat gterms.
813 sygusGTerm[CVC4::SygusGTerm& sgt, const std::string& fun]
815 std::string name, name2;
819 std::vector< CVC4::api::Term > let_vars;
821 CVC4::api::Term atomTerm;
825 ( SYGUS_CONSTANT_TOK sortSymbol[t,CHECK_DECLARED]
826 { sgt.d_gterm_type = SygusGTerm::gterm_constant;
828 Debug("parser-sygus") << "Sygus grammar constant." << std::endl;
830 | SYGUS_VARIABLE_TOK sortSymbol[t,CHECK_DECLARED]
831 { sgt.d_gterm_type = SygusGTerm::gterm_variable;
833 Debug("parser-sygus") << "Sygus grammar variable." << std::endl;
835 | SYGUS_LOCAL_VARIABLE_TOK sortSymbol[t,CHECK_DECLARED]
836 { sgt.d_gterm_type = SygusGTerm::gterm_local_variable;
838 Debug("parser-sygus") << "Sygus grammar local variable...ignore."
841 | SYGUS_INPUT_VARIABLE_TOK sortSymbol[t,CHECK_DECLARED]
842 { sgt.d_gterm_type = SygusGTerm::gterm_input_variable;
844 Debug("parser-sygus") << "Sygus grammar (input) variable."
847 | symbol[name,CHECK_NONE,SYM_VARIABLE] {
848 bool isBuiltinOperator = PARSER_STATE->isOperatorEnabled(name);
849 if(isBuiltinOperator) {
850 Debug("parser-sygus") << "Sygus grammar " << fun << " : builtin op : "
851 << name << std::endl;
852 k = PARSER_STATE->getOperatorKind(name);
853 sgt.d_name = api::kindToString(k);
854 sgt.d_gterm_type = SygusGTerm::gterm_op;
857 // what is this sygus term trying to accomplish here, if the
858 // symbol isn't yet declared?! probably the following line will
859 // fail, but we need an operator to continue here..
860 Debug("parser-sygus")
861 << "Sygus grammar " << fun << " : op (declare="
862 << PARSER_STATE->isDeclared(name) << ") : " << name
864 if (!PARSER_STATE->isDeclared(name))
866 PARSER_STATE->parseError("Functions in sygus grammars must be "
870 sgt.d_gterm_type = SygusGTerm::gterm_op;
871 sgt.d_op.d_expr = PARSER_STATE->getVariable(name) ;
876 { Debug("parser-sygus") << "Read arguments under " << sgt.d_name
880 ( sygusGTerm[sgt.d_children.back(), fun]
881 { Debug("parser-sygus") << "Finished read argument #"
882 << sgt.d_children.size() << "..." << std::endl;
887 //pop last child index
888 sgt.d_children.pop_back();
890 | termAtomic[atomTerm]
892 Debug("parser-sygus") << "Sygus grammar " << fun << " : atomic "
893 << "expression " << atomTerm << std::endl;
894 std::stringstream ss;
896 sgt.d_op.d_expr = atomTerm.getExpr();
897 sgt.d_name = ss.str();
898 sgt.d_gterm_type = SygusGTerm::gterm_op;
900 | symbol[name,CHECK_NONE,SYM_VARIABLE]
902 if( name[0] == '-' ){ //hack for unary minus
903 Debug("parser-sygus") << "Sygus grammar " << fun
904 << " : unary minus integer literal " << name
906 sgt.d_op.d_expr = SOLVER->mkReal(name);
908 sgt.d_gterm_type = SygusGTerm::gterm_op;
909 }else if( PARSER_STATE->isDeclared(name,SYM_VARIABLE) ){
910 Debug("parser-sygus") << "Sygus grammar " << fun << " : symbol "
911 << name << std::endl;
912 sgt.d_op.d_expr = PARSER_STATE->getExpressionForName(name);
914 sgt.d_gterm_type = SygusGTerm::gterm_op;
916 if( PARSER_STATE->isDeclared(name, SYM_SORT) ){
917 Debug("parser-sygus") << "Sygus grammar " << fun
918 << " : nested sort " << name << std::endl;
919 sgt.d_type = PARSER_STATE->getSort(name);
920 sgt.d_gterm_type = SygusGTerm::gterm_nested_sort;
922 Debug("parser-sygus") << "Sygus grammar " << fun
923 << " : unresolved symbol " << name
925 sgt.d_gterm_type = SygusGTerm::gterm_unresolved;
933 /** Reads a sygus grammar in the sygus version 2 format
935 * The resulting sygus datatype encoding the grammar is stored in ret.
936 * The argument sygusVars indicates the sygus bound variable list, which is
937 * the argument list of the function-to-synthesize (or null if the grammar
938 * has bound variables).
939 * The argument fun is a unique identifier to avoid naming clashes for the
940 * datatypes constructed by this call.
942 sygusGrammar[CVC4::api::Sort & ret,
943 const std::vector<CVC4::api::Term>& sygusVars,
944 const std::string& fun]
947 // the pre-declaration
948 std::vector<std::pair<std::string, CVC4::api::Sort> > sortedVarNames;
949 // non-terminal symbols of the grammar
950 std::vector<CVC4::api::Term> ntSyms;
953 CVC4::api::Term e, e2;
954 std::vector<api::DatatypeDecl> datatypes;
955 std::set<api::Sort> unresTypes;
956 std::map<CVC4::api::Term, CVC4::api::Sort> ntsToUnres;
957 unsigned dtProcessed = 0;
958 std::unordered_set<unsigned> allowConst;
963 // We read a sorted variable list here in a custom way that throws an
964 // error to recognize if the user is using the (deprecated) version 1.0
966 ( LPAREN_TOK symbol[name,CHECK_NONE,SYM_VARIABLE]
967 sortSymbol[t,CHECK_DECLARED] (
968 // SyGuS version 1.0 expects a grammar ((Start Int ( ...
969 // SyGuS version 2.0 expects a predeclaration ((Start Int) ...
972 std::stringstream sse;
973 if (sortedVarNames.empty())
975 sse << "The expected SyGuS language is version 2.0, whereas the "
976 << "input appears to be SyGuS version 1.0 format. The version "
977 << "2.0 format requires a predeclaration of the non-terminal "
978 << "symbols of the grammar to be given prior to the definition "
979 << "of the grammar. See https://sygus.org/language/ for details "
980 << "and examples. CVC4 versions past 1.8 do not support SyGuS "
985 // an unknown syntax error
986 sse << "Unexpected syntax for SyGuS predeclaration.";
988 PARSER_STATE->parseError(sse.str().c_str());
991 { sortedVarNames.push_back(make_pair(name, t)); }
995 // non-terminal symbols in the pre-declaration are locally scoped
996 PARSER_STATE->pushScope(true);
997 for (std::pair<std::string, api::Sort>& i : sortedVarNames)
999 Trace("parser-sygus2") << "Declare datatype " << i.first << std::endl;
1000 // make the datatype, which encodes terms generated by this non-terminal
1001 std::string dname = i.first;
1002 datatypes.push_back(SOLVER->mkDatatypeDecl(dname));
1003 // make its unresolved type, used for referencing the final version of
1005 PARSER_STATE->checkDeclaration(dname, CHECK_UNDECLARED, SYM_SORT);
1006 api::Sort urt = PARSER_STATE->mkUnresolvedType(dname);
1007 unresTypes.insert(urt);
1008 // make the non-terminal symbol, which will be parsed as an ordinary
1010 api::Term nts = PARSER_STATE->bindBoundVar(i.first, i.second);
1011 ntSyms.push_back(nts);
1012 ntsToUnres[nts] = urt;
1015 // the grouped rule listing
1019 symbol[name, CHECK_DECLARED, SYM_VARIABLE] sortSymbol[t, CHECK_DECLARED]
1021 // check that it matches sortedVarNames
1022 if (sortedVarNames[dtProcessed].first != name)
1024 std::stringstream sse;
1025 sse << "Grouped rule listing " << name
1026 << " does not match the name (in order) from the predeclaration ("
1027 << sortedVarNames[dtProcessed].first << ")." << std::endl;
1028 PARSER_STATE->parseError(sse.str().c_str());
1030 if (sortedVarNames[dtProcessed].second != t)
1032 std::stringstream sse;
1033 sse << "Type for grouped rule listing " << name
1034 << " does not match the type (in order) from the predeclaration ("
1035 << sortedVarNames[dtProcessed].second << ")." << std::endl;
1036 PARSER_STATE->parseError(sse.str().c_str());
1042 // add term as constructor to datatype
1043 PARSER_STATE->addSygusConstructorTerm(
1044 datatypes[dtProcessed], e, ntsToUnres);
1046 | LPAREN_TOK SYGUS_CONSTANT_TOK sortSymbol[t, CHECK_DECLARED] RPAREN_TOK {
1047 // allow constants in datatypes[dtProcessed]
1048 allowConst.insert(dtProcessed);
1050 | LPAREN_TOK SYGUS_VARIABLE_TOK sortSymbol[t, CHECK_DECLARED] RPAREN_TOK {
1051 // add variable constructors to datatype
1052 PARSER_STATE->addSygusConstructorVariables(
1053 datatypes[dtProcessed], sygusVars, t);
1064 if (dtProcessed != sortedVarNames.size())
1066 PARSER_STATE->parseError(
1067 "Number of grouped rule listings does not match "
1068 "number of symbols in predeclaration.");
1071 if (!sygusVars.empty())
1073 bvl = MK_TERM(api::BOUND_VAR_LIST, sygusVars);
1075 Trace("parser-sygus2") << "Process " << dtProcessed << " sygus datatypes..." << std::endl;
1076 for (unsigned i = 0; i < dtProcessed; i++)
1078 bool aci = allowConst.find(i)!=allowConst.end();
1079 api::Sort btt = sortedVarNames[i].second;
1080 datatypes[i].getDatatype().setSygus(btt.getType(), bvl.getExpr(), aci, false);
1081 Trace("parser-sygus2") << "- " << datatypes[i].getName()
1082 << ", #cons= " << datatypes[i].getNumConstructors()
1083 << ", aci= " << aci << std::endl;
1084 // We can be in a case where the only rule specified was (Variable T)
1085 // and there are no variables of type T, in which case this is a bogus
1086 // grammar. This results in the error below.
1087 if (datatypes[i].getNumConstructors() == 0)
1089 std::stringstream se;
1090 se << "Grouped rule listing for " << datatypes[i].getName()
1091 << " produced an empty rule list.";
1092 PARSER_STATE->parseError(se.str());
1095 // pop scope from the pre-declaration
1096 PARSER_STATE->popScope();
1097 // now, make the sygus datatype
1098 Trace("parser-sygus2") << "Make the sygus datatypes..." << std::endl;
1099 std::vector<api::Sort> datatypeTypes =
1100 SOLVER->mkDatatypeSorts(datatypes, unresTypes);
1101 // return is the first datatype
1102 ret = api::Sort(datatypeTypes[0]);
1106 setInfoInternal[std::unique_ptr<CVC4::Command>* cmd]
1111 : KEYWORD symbolicExpr[sexpr]
1112 { name = AntlrInput::tokenText($KEYWORD);
1113 PARSER_STATE->setInfo(name.c_str() + 1, sexpr);
1114 cmd->reset(new SetInfoCommand(name.c_str() + 1, sexpr));
1118 setOptionInternal[std::unique_ptr<CVC4::Command>* cmd]
1123 : keyword[name] symbolicExpr[sexpr]
1124 { PARSER_STATE->setOption(name.c_str() + 1, sexpr);
1125 cmd->reset(new SetOptionCommand(name.c_str() + 1, sexpr));
1126 // Ugly that this changes the state of the parser; but
1127 // global-declarations affects parsing, so we can't hold off
1128 // on this until some SmtEngine eventually (if ever) executes it.
1129 if(name == ":global-declarations") {
1130 PARSER_STATE->setGlobalDeclarations(sexpr.getValue() == "true");
1135 smt25Command[std::unique_ptr<CVC4::Command>* cmd]
1139 CVC4::api::Term expr, expr2;
1140 std::vector<std::pair<std::string, CVC4::api::Sort> > sortedVarNames;
1143 CVC4::api::Term func;
1144 std::vector<CVC4::api::Term> bvs;
1145 std::vector<std::vector<std::pair<std::string, CVC4::api::Sort>>>
1147 std::vector<std::vector<CVC4::api::Term>> flattenVarsList;
1148 std::vector<std::vector<CVC4::api::Term>> formals;
1149 std::vector<CVC4::api::Term> funcs;
1150 std::vector<CVC4::api::Term> func_defs;
1151 CVC4::api::Term aexpr;
1152 std::unique_ptr<CVC4::CommandSequence> seq;
1153 std::vector<api::Sort> sorts;
1154 std::vector<CVC4::api::Term> flattenVars;
1157 : DECLARE_CONST_TOK { PARSER_STATE->checkThatLogicIsSet(); }
1158 symbol[name,CHECK_NONE,SYM_VARIABLE]
1159 { PARSER_STATE->checkUserSymbol(name); }
1160 sortSymbol[t,CHECK_DECLARED]
1161 { // allow overloading here
1163 PARSER_STATE->bindVar(name, t, ExprManager::VAR_FLAG_NONE, true);
1164 cmd->reset(new DeclareFunctionCommand(name, c.getExpr(), t.getType())); }
1167 | GET_MODEL_TOK { PARSER_STATE->checkThatLogicIsSet(); }
1168 { cmd->reset(new GetModelCommand()); }
1172 ( simpleSymbolicExpr[sexpr]
1173 { cmd->reset(new EchoCommand(sexpr.toString())); }
1174 | { cmd->reset(new EchoCommand()); }
1177 /* reset: reset everything, returning solver to initial state.
1178 * Logic and options must be set again. */
1180 { cmd->reset(new ResetCommand());
1181 PARSER_STATE->reset();
1183 /* reset-assertions: reset assertions, assertion stack, declarations,
1184 * etc., but the logic and options remain as they were. */
1185 | RESET_ASSERTIONS_TOK
1186 { cmd->reset(new ResetAssertionsCommand());
1187 PARSER_STATE->resetAssertions();
1189 | DEFINE_FUN_REC_TOK
1190 { PARSER_STATE->checkThatLogicIsSet(); }
1191 symbol[fname,CHECK_NONE,SYM_VARIABLE]
1192 { PARSER_STATE->checkUserSymbol(fname); }
1193 LPAREN_TOK sortedVarList[sortedVarNames] RPAREN_TOK
1194 sortSymbol[t,CHECK_DECLARED]
1197 PARSER_STATE->bindDefineFunRec(fname, sortedVarNames, t, flattenVars);
1198 PARSER_STATE->pushDefineFunRecScope(
1199 sortedVarNames, func, flattenVars, bvs, true);
1202 { PARSER_STATE->popScope();
1203 if( !flattenVars.empty() ){
1204 expr = PARSER_STATE->mkHoApply( expr, flattenVars );
1206 cmd->reset(new DefineFunctionRecCommand(
1207 func.getExpr(), api::termVectorToExprs(bvs), expr.getExpr()));
1209 | DEFINE_FUNS_REC_TOK
1210 { PARSER_STATE->checkThatLogicIsSet();}
1213 symbol[fname,CHECK_UNDECLARED,SYM_VARIABLE]
1214 { PARSER_STATE->checkUserSymbol(fname); }
1215 LPAREN_TOK sortedVarList[sortedVarNames] RPAREN_TOK
1216 sortSymbol[t,CHECK_DECLARED]
1218 flattenVars.clear();
1219 func = PARSER_STATE->bindDefineFunRec(
1220 fname, sortedVarNames, t, flattenVars);
1221 funcs.push_back( func );
1223 // add to lists (need to remember for when parsing the bodies)
1224 sortedVarNamesList.push_back( sortedVarNames );
1225 flattenVarsList.push_back( flattenVars );
1227 // set up parsing the next variable list block
1228 sortedVarNames.clear();
1229 flattenVars.clear();
1236 //set up the first scope
1237 if( sortedVarNamesList.empty() ){
1238 PARSER_STATE->parseError("Must define at least one function in "
1242 PARSER_STATE->pushDefineFunRecScope( sortedVarNamesList[0], funcs[0],
1243 flattenVarsList[0], bvs, true);
1248 unsigned j = func_defs.size();
1249 if( !flattenVarsList[j].empty() ){
1250 expr = PARSER_STATE->mkHoApply( expr, flattenVarsList[j] );
1252 func_defs.push_back( expr );
1253 formals.push_back(bvs);
1255 //set up the next scope
1256 PARSER_STATE->popScope();
1257 if( func_defs.size()<funcs.size() ){
1259 PARSER_STATE->pushDefineFunRecScope( sortedVarNamesList[j], funcs[j],
1260 flattenVarsList[j], bvs, true);
1265 { if( funcs.size()!=func_defs.size() ){
1266 PARSER_STATE->parseError(std::string(
1267 "Number of functions defined does not match number listed in "
1268 "define-funs-rec"));
1270 std::vector<std::vector<Expr>> eformals;
1271 for (unsigned i=0, fsize = formals.size(); i<fsize; i++)
1273 eformals.push_back(api::termVectorToExprs(formals[i]));
1276 new DefineFunctionRecCommand(api::termVectorToExprs(funcs),
1278 api::termVectorToExprs(func_defs)));
1282 extendedCommand[std::unique_ptr<CVC4::Command>* cmd]
1284 std::vector<api::DatatypeDecl> dts;
1285 CVC4::api::Term e, e2;
1288 std::vector<std::string> names;
1289 std::vector<CVC4::api::Term> terms;
1290 std::vector<api::Sort> sorts;
1291 std::vector<std::pair<std::string, CVC4::api::Sort> > sortedVarNames;
1292 std::unique_ptr<CVC4::CommandSequence> seq;
1294 /* Extended SMT-LIB set of commands syntax, not permitted in
1295 * --smtlib2 compliance mode. */
1296 : DECLARE_DATATYPES_2_5_TOK datatypes_2_5_DefCommand[false, cmd]
1297 | DECLARE_CODATATYPES_2_5_TOK datatypes_2_5_DefCommand[true, cmd]
1298 | DECLARE_CODATATYPE_TOK datatypeDefCommand[true, cmd]
1299 | DECLARE_CODATATYPES_TOK datatypesDefCommand[true, cmd]
1301 /* Support some of Z3's extended SMT-LIB commands */
1305 PARSER_STATE->checkThatLogicIsSet();
1306 PARSER_STATE->checkLogicAllowsFreeSorts();
1307 seq.reset(new CVC4::CommandSequence());
1310 ( symbol[name,CHECK_UNDECLARED,SYM_SORT]
1311 { PARSER_STATE->checkUserSymbol(name);
1312 api::Sort type = PARSER_STATE->mkSort(name);
1313 seq->addCommand(new DeclareTypeCommand(name, 0, type.getType()));
1317 { cmd->reset(seq.release()); }
1319 | DECLARE_FUNS_TOK { PARSER_STATE->checkThatLogicIsSet(); }
1320 { seq.reset(new CVC4::CommandSequence()); }
1322 ( LPAREN_TOK symbol[name,CHECK_UNDECLARED,SYM_VARIABLE]
1323 { PARSER_STATE->checkUserSymbol(name); }
1324 nonemptySortList[sorts] RPAREN_TOK
1326 if(sorts.size() > 1) {
1327 PARSER_STATE->checkLogicAllowsFunctions();
1329 api::Sort range = sorts.back();
1331 tt = PARSER_STATE->mkFlatFunctionType(sorts, range);
1335 // allow overloading
1337 PARSER_STATE->bindVar(name, tt, ExprManager::VAR_FLAG_NONE, true);
1339 new DeclareFunctionCommand(name, func.getExpr(), tt.getType()));
1344 { cmd->reset(seq.release()); }
1345 | DECLARE_PREDS_TOK { PARSER_STATE->checkThatLogicIsSet(); }
1346 { seq.reset(new CVC4::CommandSequence()); }
1348 ( LPAREN_TOK symbol[name,CHECK_UNDECLARED,SYM_VARIABLE]
1349 { PARSER_STATE->checkUserSymbol(name); }
1350 sortList[sorts] RPAREN_TOK
1351 { t = SOLVER->getBooleanSort();
1352 if(sorts.size() > 0) {
1353 PARSER_STATE->checkLogicAllowsFunctions();
1354 t = SOLVER->mkFunctionSort(sorts, t);
1356 // allow overloading
1358 PARSER_STATE->bindVar(name, t, ExprManager::VAR_FLAG_NONE, true);
1360 new DeclareFunctionCommand(name, func.getExpr(), t.getType()));
1365 { cmd->reset(seq.release()); }
1367 | DEFINE_TOK { PARSER_STATE->checkThatLogicIsSet(); }
1368 ( symbol[name,CHECK_UNDECLARED,SYM_VARIABLE]
1369 { PARSER_STATE->checkUserSymbol(name); }
1371 { api::Term func = PARSER_STATE->bindVar(name, e.getSort(),
1372 ExprManager::VAR_FLAG_DEFINED);
1373 cmd->reset(new DefineFunctionCommand(name, func.getExpr(), e.getExpr()));
1376 symbol[name,CHECK_UNDECLARED,SYM_VARIABLE]
1377 { PARSER_STATE->checkUserSymbol(name); }
1378 sortedVarList[sortedVarNames] RPAREN_TOK
1379 { /* add variables to parser state before parsing term */
1380 Debug("parser") << "define fun: '" << name << "'" << std::endl;
1381 PARSER_STATE->pushScope(true);
1382 terms = PARSER_STATE->bindBoundVars(sortedVarNames);
1385 { PARSER_STATE->popScope();
1386 // declare the name down here (while parsing term, signature
1387 // must not be extended with the name itself; no recursion
1389 api::Sort tt = e.getSort();
1390 if( sortedVarNames.size() > 0 ) {
1391 sorts.reserve(sortedVarNames.size());
1392 for(std::vector<std::pair<std::string, api::Sort> >::const_iterator
1393 i = sortedVarNames.begin(), iend = sortedVarNames.end();
1395 sorts.push_back((*i).second);
1397 tt = SOLVER->mkFunctionSort(sorts, tt);
1399 api::Term func = PARSER_STATE->bindVar(name, tt,
1400 ExprManager::VAR_FLAG_DEFINED);
1401 cmd->reset(new DefineFunctionCommand(
1402 name, func.getExpr(), api::termVectorToExprs(terms), e.getExpr()));
1405 | DEFINE_CONST_TOK { PARSER_STATE->checkThatLogicIsSet(); }
1406 symbol[name,CHECK_UNDECLARED,SYM_VARIABLE]
1407 { PARSER_STATE->checkUserSymbol(name); }
1408 sortSymbol[t,CHECK_DECLARED]
1409 { /* add variables to parser state before parsing term */
1410 Debug("parser") << "define const: '" << name << "'" << std::endl;
1411 PARSER_STATE->pushScope(true);
1412 terms = PARSER_STATE->bindBoundVars(sortedVarNames);
1415 { PARSER_STATE->popScope();
1416 // declare the name down here (while parsing term, signature
1417 // must not be extended with the name itself; no recursion
1419 api::Term func = PARSER_STATE->bindVar(name, t,
1420 ExprManager::VAR_FLAG_DEFINED);
1421 cmd->reset(new DefineFunctionCommand(
1422 name, func.getExpr(), api::termVectorToExprs(terms), e.getExpr()));
1425 | SIMPLIFY_TOK { PARSER_STATE->checkThatLogicIsSet(); }
1427 { cmd->reset(new SimplifyCommand(e.getExpr())); }
1428 | GET_QE_TOK { PARSER_STATE->checkThatLogicIsSet(); }
1430 { cmd->reset(new GetQuantifierEliminationCommand(e.getExpr(), true)); }
1431 | GET_QE_DISJUNCT_TOK { PARSER_STATE->checkThatLogicIsSet(); }
1433 { cmd->reset(new GetQuantifierEliminationCommand(e.getExpr(), false)); }
1435 PARSER_STATE->checkThatLogicIsSet();
1437 symbol[name,CHECK_UNDECLARED,SYM_VARIABLE]
1440 sygusGrammar[t, terms, name]
1443 cmd->reset(new GetAbductCommand(name,e.getExpr(), t.getType()));
1445 | DECLARE_HEAP LPAREN_TOK
1446 sortSymbol[t, CHECK_DECLARED]
1447 sortSymbol[t, CHECK_DECLARED]
1448 // We currently do nothing with the type information declared for the heap.
1449 { cmd->reset(new EmptyCommand()); }
1451 | BLOCK_MODEL_TOK { PARSER_STATE->checkThatLogicIsSet(); }
1452 { cmd->reset(new BlockModelCommand()); }
1454 | BLOCK_MODEL_VALUES_TOK { PARSER_STATE->checkThatLogicIsSet(); }
1455 ( LPAREN_TOK termList[terms,e] RPAREN_TOK
1456 { cmd->reset(new BlockModelValuesCommand(api::termVectorToExprs(terms))); }
1458 { PARSER_STATE->parseError("The block-model-value command expects a list "
1459 "of terms. Perhaps you forgot a pair of "
1466 datatypes_2_5_DefCommand[bool isCo, std::unique_ptr<CVC4::Command>* cmd]
1468 std::vector<api::DatatypeDecl> dts;
1470 std::vector<api::Sort> sorts;
1471 std::vector<std::string> dnames;
1472 std::vector<unsigned> arities;
1474 : { PARSER_STATE->checkThatLogicIsSet();
1475 /* open a scope to keep the UnresolvedTypes contained */
1476 PARSER_STATE->pushScope(true); }
1477 LPAREN_TOK /* parametric sorts */
1478 ( symbol[name,CHECK_UNDECLARED,SYM_SORT]
1480 sorts.push_back(PARSER_STATE->mkSort(name, ExprManager::SORT_FLAG_PLACEHOLDER));
1484 LPAREN_TOK ( LPAREN_TOK datatypeDef[isCo, dts, sorts] RPAREN_TOK )+ RPAREN_TOK
1485 { PARSER_STATE->popScope();
1486 cmd->reset(new DatatypeDeclarationCommand(
1487 api::sortVectorToTypes(
1488 PARSER_STATE->bindMutualDatatypeTypes(dts, true))));
1492 datatypeDefCommand[bool isCo, std::unique_ptr<CVC4::Command>* cmd]
1494 std::vector<api::DatatypeDecl> dts;
1496 std::vector<std::string> dnames;
1497 std::vector<int> arities;
1499 : { PARSER_STATE->checkThatLogicIsSet(); }
1500 symbol[name,CHECK_UNDECLARED,SYM_SORT]
1502 dnames.push_back(name);
1503 arities.push_back(-1);
1505 datatypesDef[isCo, dnames, arities, cmd]
1508 datatypesDefCommand[bool isCo, std::unique_ptr<CVC4::Command>* cmd]
1510 std::vector<api::DatatypeDecl> dts;
1512 std::vector<std::string> dnames;
1513 std::vector<int> arities;
1515 : { PARSER_STATE->checkThatLogicIsSet(); }
1516 LPAREN_TOK /* datatype definition prelude */
1517 ( LPAREN_TOK symbol[name,CHECK_UNDECLARED,SYM_SORT] n=INTEGER_LITERAL RPAREN_TOK
1518 { unsigned arity = AntlrInput::tokenToUnsigned(n);
1519 Debug("parser-dt") << "Datatype : " << name << ", arity = " << arity << std::endl;
1520 dnames.push_back(name);
1521 arities.push_back( static_cast<int>(arity) );
1526 datatypesDef[isCo, dnames, arities, cmd]
1531 * Read a list of datatype definitions for datatypes with names dnames and
1532 * parametric arities arities. A negative value in arities indicates that the
1533 * arity for the corresponding datatype has not been fixed.
1535 datatypesDef[bool isCo,
1536 const std::vector<std::string>& dnames,
1537 const std::vector<int>& arities,
1538 std::unique_ptr<CVC4::Command>* cmd]
1540 std::vector<api::DatatypeDecl> dts;
1542 std::vector<api::Sort> params;
1544 : { PARSER_STATE->pushScope(true); }
1547 Debug("parser-dt") << "Processing datatype #" << dts.size() << std::endl;
1548 if( dts.size()>=dnames.size() ){
1549 PARSER_STATE->parseError("Too many datatypes defined in this block.");
1552 ( PAR_TOK { PARSER_STATE->pushScope(true); } LPAREN_TOK
1553 ( symbol[name,CHECK_UNDECLARED,SYM_SORT]
1555 params.push_back( PARSER_STATE->mkSort(name, ExprManager::SORT_FLAG_PLACEHOLDER)); }
1558 // if the arity was fixed by prelude and is not equal to the number of parameters
1559 if( arities[dts.size()]>=0 && static_cast<int>(params.size())!=arities[dts.size()] ){
1560 PARSER_STATE->parseError("Wrong number of parameters for datatype.");
1562 Debug("parser-dt") << params.size() << " parameters for " << dnames[dts.size()] << std::endl;
1563 dts.push_back(SOLVER->mkDatatypeDecl(dnames[dts.size()], params, isCo));
1566 ( LPAREN_TOK constructorDef[dts.back()] RPAREN_TOK )+
1567 RPAREN_TOK { PARSER_STATE->popScope(); }
1568 | { // if the arity was fixed by prelude and is not equal to 0
1569 if( arities[dts.size()]>0 ){
1570 PARSER_STATE->parseError("No parameters given for datatype.");
1572 Debug("parser-dt") << params.size() << " parameters for " << dnames[dts.size()] << std::endl;
1573 dts.push_back(SOLVER->mkDatatypeDecl(dnames[dts.size()],
1577 ( LPAREN_TOK constructorDef[dts.back()] RPAREN_TOK )+
1582 PARSER_STATE->popScope();
1583 cmd->reset(new DatatypeDeclarationCommand(
1584 api::sortVectorToTypes(
1585 PARSER_STATE->bindMutualDatatypeTypes(dts, true))));
1589 simpleSymbolicExprNoKeyword[CVC4::SExpr& sexpr]
1593 std::vector<unsigned int> s_vec;
1596 { sexpr = SExpr(Integer(AntlrInput::tokenText($INTEGER_LITERAL))); }
1598 { sexpr = SExpr(AntlrInput::tokenToRational($DECIMAL_LITERAL)); }
1600 { assert( AntlrInput::tokenText($HEX_LITERAL).find("#x") == 0 );
1601 std::string hexString = AntlrInput::tokenTextSubstr($HEX_LITERAL, 2);
1602 sexpr = SExpr(Integer(hexString, 16));
1605 { assert( AntlrInput::tokenText($BINARY_LITERAL).find("#b") == 0 );
1606 std::string binString = AntlrInput::tokenTextSubstr($BINARY_LITERAL, 2);
1607 sexpr = SExpr(Integer(binString, 2));
1610 { sexpr = SExpr(s); }
1611 | symbol[s,CHECK_NONE,SYM_SORT]
1612 { sexpr = SExpr(SExpr::Keyword(s)); }
1613 | tok=(ASSERT_TOK | CHECK_SAT_TOK | CHECK_SAT_ASSUMING_TOK | DECLARE_FUN_TOK
1615 | DEFINE_FUN_TOK | DEFINE_FUN_REC_TOK | DEFINE_FUNS_REC_TOK
1616 | DEFINE_SORT_TOK | GET_VALUE_TOK | GET_ASSIGNMENT_TOK
1617 | GET_ASSERTIONS_TOK | GET_PROOF_TOK | GET_UNSAT_ASSUMPTIONS_TOK
1618 | GET_UNSAT_CORE_TOK | EXIT_TOK
1619 | RESET_TOK | RESET_ASSERTIONS_TOK | SET_LOGIC_TOK | SET_INFO_TOK
1620 | GET_INFO_TOK | SET_OPTION_TOK | GET_OPTION_TOK | PUSH_TOK | POP_TOK
1621 | DECLARE_DATATYPES_TOK | GET_MODEL_TOK | ECHO_TOK | SIMPLIFY_TOK)
1622 { sexpr = SExpr(SExpr::Keyword(AntlrInput::tokenText($tok))); }
1625 keyword[std::string& s]
1627 { s = AntlrInput::tokenText($KEYWORD); }
1630 simpleSymbolicExpr[CVC4::SExpr& sexpr]
1631 : simpleSymbolicExprNoKeyword[sexpr]
1633 { sexpr = SExpr(AntlrInput::tokenText($KEYWORD)); }
1636 symbolicExpr[CVC4::SExpr& sexpr]
1638 std::vector<SExpr> children;
1640 : simpleSymbolicExpr[sexpr]
1642 ( symbolicExpr[sexpr] { children.push_back(sexpr); } )* RPAREN_TOK
1643 { sexpr = SExpr(children); }
1648 * @return the expression representing the term.
1650 term[CVC4::api::Term& expr, CVC4::api::Term& expr2]
1652 api::Kind kind = api::NULL_EXPR;
1655 CVC4::api::Sort type;
1658 : termNonVariable[expr, expr2]
1660 // a qualified identifier (section 3.6 of SMT-LIB version 2.6)
1664 expr = PARSER_STATE->parseOpToExpr(p);
1669 * Matches a non-variable term.
1670 * @return the expression expr representing the term or formula, and expr2, an
1671 * optional annotation for expr (for instance, for attributed expressions).
1673 termNonVariable[CVC4::api::Term& expr, CVC4::api::Term& expr2]
1675 Debug("parser") << "term: " << AntlrInput::tokenText(LT(1)) << std::endl;
1676 api::Kind kind = api::NULL_EXPR;
1678 std::vector<CVC4::api::Term> args;
1679 std::vector< std::pair<std::string, CVC4::api::Sort> > sortedVarNames;
1680 CVC4::api::Term bvl;
1681 CVC4::api::Term f, f2, f3;
1683 CVC4::api::Term attexpr;
1684 std::vector<CVC4::api::Term> patexprs;
1685 std::vector<CVC4::api::Term> matchcases;
1686 std::unordered_set<std::string> names;
1687 std::vector< std::pair<std::string, CVC4::api::Term> > binders;
1688 CVC4::api::Sort type;
1689 CVC4::api::Sort type2;
1692 std::vector<api::Sort> argTypes;
1694 : LPAREN_TOK quantOp[kind]
1695 { PARSER_STATE->pushScope(true); }
1697 term[f, f2] RPAREN_TOK
1699 args.push_back(bvl);
1701 PARSER_STATE->popScope();
1706 expr = MK_TERM(kind, args);
1708 | LPAREN_TOK COMPREHENSION_TOK
1709 { PARSER_STATE->pushScope(true); }
1712 args.push_back(bvl);
1714 term[f, f2] { args.push_back(f); }
1717 expr = MK_TERM(api::COMPREHENSION, args);
1720 | LPAREN_TOK qualIdentifier[p]
1721 termList[args,expr] RPAREN_TOK
1723 expr = PARSER_STATE->applyParseOp(p, args);
1725 | /* a let or sygus let binding */
1728 { PARSER_STATE->pushScope(true); }
1729 ( LPAREN_TOK symbol[name,CHECK_NONE,SYM_VARIABLE]
1732 // this is a parallel let, so we have to save up all the contributions
1733 // of the let and define them only later on
1734 { if(names.count(name) == 1) {
1735 std::stringstream ss;
1736 ss << "warning: symbol `" << name << "' bound multiple times by let;"
1737 << " the last binding will be used, shadowing earlier ones";
1738 PARSER_STATE->warning(ss.str());
1742 binders.push_back(std::make_pair(name, expr)); } )+ |
1743 SYGUS_LET_TOK LPAREN_TOK
1744 { PARSER_STATE->pushScope(true); }
1745 ( LPAREN_TOK symbol[name,CHECK_NONE,SYM_VARIABLE]
1746 sortSymbol[type,CHECK_DECLARED]
1749 // this is a parallel let, so we have to save up all the contributions
1750 // of the let and define them only later on
1751 { if(names.count(name) == 1) {
1752 std::stringstream ss;
1753 ss << "warning: symbol `" << name << "' bound multiple times by let;"
1754 << " the last binding will be used, shadowing earlier ones";
1755 PARSER_STATE->warning(ss.str());
1759 binders.push_back(std::make_pair(name, expr)); } )+ )
1760 { // now implement these bindings
1761 for (const std::pair<std::string, api::Term>& binder : binders)
1764 PARSER_STATE->defineVar(binder.first, binder.second);
1771 { PARSER_STATE->popScope(); }
1772 | /* match expression */
1773 LPAREN_TOK MATCH_TOK term[expr, f2] {
1774 if( !expr.getSort().isDatatype() ){
1775 PARSER_STATE->parseError("Cannot match on non-datatype term.");
1780 // case with non-nullary pattern
1781 LPAREN_TOK LPAREN_TOK term[f, f2] {
1783 PARSER_STATE->pushScope(true);
1784 // f should be a constructor
1786 Debug("parser-dt") << "Pattern head : " << f << " " << type << std::endl;
1787 if (!type.isConstructor())
1789 PARSER_STATE->parseError("Pattern must be application of a constructor or a variable.");
1791 Expr ef = f.getExpr();
1792 if (Datatype::datatypeOf(ef).isParametric())
1794 type = Datatype::datatypeOf(ef)[Datatype::indexOf(ef)]
1795 .getSpecializedConstructorType(expr.getSort().getType());
1797 argTypes = type.getConstructorDomainSorts();
1799 // arguments of the pattern
1800 ( symbol[name,CHECK_NONE,SYM_VARIABLE] {
1801 if (args.size() >= argTypes.size())
1803 PARSER_STATE->parseError("Too many arguments for pattern.");
1805 //make of proper type
1806 api::Term arg = PARSER_STATE->bindBoundVar(name, argTypes[args.size()]);
1807 args.push_back( arg );
1810 RPAREN_TOK term[f3, f2] {
1811 // make the match case
1812 std::vector<CVC4::api::Term> cargs;
1814 cargs.insert(cargs.end(),args.begin(),args.end());
1815 api::Term c = MK_TERM(api::APPLY_CONSTRUCTOR,cargs);
1816 api::Term bvla = MK_TERM(api::BOUND_VAR_LIST,args);
1817 api::Term mc = MK_TERM(api::MATCH_BIND_CASE, bvla, c, f3);
1818 matchcases.push_back(mc);
1819 // now, pop the scope
1820 PARSER_STATE->popScope();
1823 // case with nullary or variable pattern
1824 | LPAREN_TOK symbol[name,CHECK_NONE,SYM_VARIABLE] {
1825 if (PARSER_STATE->isDeclared(name,SYM_VARIABLE))
1827 f = PARSER_STATE->getVariable(name);
1829 if (!type.isConstructor() ||
1830 !type.getConstructorDomainSorts().empty())
1832 PARSER_STATE->parseError("Must apply constructors of arity greater than 0 to arguments in pattern.");
1834 // make nullary constructor application
1835 f = MK_TERM(api::APPLY_CONSTRUCTOR, f);
1839 // it has the type of the head expr
1840 f = PARSER_STATE->bindBoundVar(name, expr.getSort());
1845 if (f.getKind() == api::VARIABLE)
1847 api::Term bvlf = MK_TERM(api::BOUND_VAR_LIST, f);
1848 mc = MK_TERM(api::MATCH_BIND_CASE, bvlf, f, f3);
1852 mc = MK_TERM(api::MATCH_CASE, f, f3);
1854 matchcases.push_back(mc);
1858 RPAREN_TOK RPAREN_TOK {
1859 //now, make the match
1860 if (matchcases.empty())
1862 PARSER_STATE->parseError("Must have at least one case in match.");
1864 std::vector<api::Term> mchildren;
1865 mchildren.push_back(expr);
1866 mchildren.insert(mchildren.end(), matchcases.begin(), matchcases.end());
1867 expr = MK_TERM(api::MATCH, mchildren);
1870 /* attributed expressions */
1871 | LPAREN_TOK ATTRIBUTE_TOK term[expr, f2]
1872 ( attribute[expr, attexpr, attr]
1873 { if( ! attexpr.isNull()) {
1874 patexprs.push_back( attexpr );
1879 if(! patexprs.empty()) {
1880 if( !f2.isNull() && f2.getKind()==api::INST_PATTERN_LIST ){
1881 for( size_t i=0; i<f2.getNumChildren(); i++ ){
1882 if( f2[i].getKind()==api::INST_PATTERN ){
1883 patexprs.push_back( f2[i] );
1885 std::stringstream ss;
1886 ss << "warning: rewrite rules do not support " << f2[i]
1887 << " within instantiation pattern list";
1888 PARSER_STATE->warning(ss.str());
1892 expr2 = MK_TERM(api::INST_PATTERN_LIST, patexprs);
1898 LPAREN_TOK HO_LAMBDA_TOK
1899 { PARSER_STATE->pushScope(true); }
1901 term[f, f2] RPAREN_TOK
1903 args.push_back(bvl);
1905 PARSER_STATE->popScope();
1906 expr = MK_TERM(api::LAMBDA, args);
1908 | LPAREN_TOK TUPLE_CONST_TOK termList[args,expr] RPAREN_TOK
1910 std::vector<api::Sort> sorts;
1911 std::vector<api::Term> terms;
1912 for (const api::Term& arg : args)
1914 sorts.emplace_back(arg.getSort());
1915 terms.emplace_back(arg);
1917 expr = SOLVER->mkTuple(sorts, terms).getExpr();
1919 | /* an atomic term (a term with no subterms) */
1920 termAtomic[atomTerm] { expr = atomTerm.getExpr(); }
1925 * Matches a qualified identifier, which can be a combination of one or more of
1926 * the following, stored in the ParseOp utility class:
1928 * (2) A string name.
1929 * (3) An expression expr.
1932 * A qualified identifier is the generic case of function heads.
1933 * With respect to the standard definition (Section 3.6 of SMT-LIB version 2.6)
1934 * of qualified identifiers, we additionally parse:
1935 * - "Array constant specifications" of the form (as const (Array T1 T2)),
1936 * which notice are used as function heads e.g. ((as const (Array Int Int)) 0)
1937 * specifies the constant array over integers consisting of constant 0. This
1938 * is handled as if it were a special case of an operator here.
1944 * - For declared functions f, we return (2).
1945 * - For indexed functions like testers (_ is C) and bitvector extract
1946 * (_ extract n m), we return (3) for the appropriate operator.
1947 * - For tuple selectors (_ tupSel n), we return (1) and (3). api::Kind is set to
1948 * APPLY_SELECTOR, and expr is set to n, which is to be interpreted by the
1949 * caller as the n^th generic tuple selector. We do this since there is no
1950 * AST expression representing generic tuple select, and we do not have enough
1951 * type information at this point to know the type of the tuple we will be
1954 * (Ascripted Identifiers)
1956 * - For ascripted nullary parametric datatype constructors like
1957 * (as nil (List Int)), we return (APPLY_CONSTRUCTOR C) for the appropriate
1958 * specialized constructor C as (3).
1959 * - For ascripted non-nullary parametric datatype constructors like
1960 * (as cons (List Int)), we return the appropriate specialized constructor C
1962 * - Overloaded non-parametric constructors (as C T) return the appropriate
1963 * expression, analogous to the parametric cases above.
1964 * - For other ascripted nullary constants like (as emptyset (Set T)),
1965 * (as sep.nil T), we return the appropriate expression (3).
1966 * - For array constant specifications (as const (Array T1 T2)), we return (1)
1967 * and (4), where kind is set to STORE_ALL and type is set to (Array T1 T2),
1968 * where this is to be interpreted by the caller as converting the next parsed
1969 * constant of type T2 to an Array of type (Array T1 T2) over that constant.
1970 * - For ascriptions on normal symbols (as f T), we return the appropriate
1971 * expression (3), which may involve disambiguating f based on type T if it is
1974 qualIdentifier[CVC4::ParseOp& p]
1977 std::string baseName;
1979 CVC4::api::Sort type;
1983 ( CONST_TOK sortSymbol[type, CHECK_DECLARED]
1985 p.d_kind = api::STORE_ALL;
1986 PARSER_STATE->parseOpApplyTypeAscription(p, type);
1989 sortSymbol[type, CHECK_DECLARED]
1991 PARSER_STATE->parseOpApplyTypeAscription(p, type);
1998 * Matches an identifier, which can be a combination of one or more of the
1999 * following, stored in the ParseOp utility class:
2001 * (2) A string name.
2002 * (3) An expression expr.
2003 * For examples, see documentation of qualIdentifier.
2005 identifier[CVC4::ParseOp& p]
2009 std::vector<uint64_t> numerals;
2011 : functionName[p.d_name, CHECK_NONE]
2013 // indexed functions
2015 | LPAREN_TOK INDEX_TOK
2016 ( TESTER_TOK term[f, f2]
2018 if (f.getKind() == api::APPLY_CONSTRUCTOR && f.getNumChildren() == 1)
2020 // for nullary constructors, must get the operator
2023 if (!f.getSort().isConstructor())
2025 PARSER_STATE->parseError(
2026 "Bad syntax for test (_ is X), X must be a constructor.");
2028 // get the datatype that f belongs to
2029 api::Sort sf = f.getSort().getConstructorCodomainSort();
2030 api::Datatype d = sf.getDatatype();
2032 api::DatatypeConstructor dc = d.getConstructor(f.toString());
2033 p.d_expr = dc.getTesterTerm();
2035 | TUPLE_SEL_TOK m=INTEGER_LITERAL
2037 // we adopt a special syntax (_ tupSel n)
2038 p.d_kind = api::APPLY_SELECTOR;
2039 // put m in expr so that the caller can deal with this case
2040 p.d_expr = SOLVER->mkReal(AntlrInput::tokenToUnsigned($m));
2042 | sym=SIMPLE_SYMBOL nonemptyNumeralList[numerals]
2044 p.d_op = PARSER_STATE->mkIndexedOp(AntlrInput::tokenText($sym), numerals);
2051 * Matches an atomic term (a term with no subterms).
2052 * @return the expression expr representing the term or formula.
2054 termAtomic[CVC4::api::Term& atomTerm]
2056 CVC4::api::Sort type;
2057 CVC4::api::Sort type2;
2059 std::vector<uint64_t> numerals;
2064 std::string intStr = AntlrInput::tokenText($INTEGER_LITERAL);
2065 atomTerm = SOLVER->mkReal(intStr);
2069 std::string realStr = AntlrInput::tokenText($DECIMAL_LITERAL);
2070 atomTerm = SOLVER->ensureTermSort(SOLVER->mkReal(realStr),
2071 SOLVER->getRealSort());
2074 // Constants using indexed identifiers, e.g. (_ +oo 8 24) (positive infinity
2075 // as a 32-bit floating-point constant)
2076 | LPAREN_TOK INDEX_TOK
2078 sortSymbol[type,CHECK_DECLARED]
2079 sortSymbol[type2,CHECK_DECLARED]
2081 // Empty heap constant in seperation logic
2082 api::Term v1 = SOLVER->mkConst(api::Sort(type), "_emp1");
2083 api::Term v2 = SOLVER->mkConst(api::Sort(type2), "_emp2");
2084 atomTerm = SOLVER->mkTerm(api::SEP_EMP, v1, v2);
2086 | CHAR_TOK HEX_LITERAL
2088 std::string hexStr = AntlrInput::tokenTextSubstr($HEX_LITERAL, 2);
2089 atomTerm = SOLVER->mkChar(hexStr);
2091 | sym=SIMPLE_SYMBOL nonemptyNumeralList[numerals]
2094 PARSER_STATE->mkIndexedConstant(AntlrInput::tokenText($sym),
2100 // Bit-vector constants
2103 assert(AntlrInput::tokenText($HEX_LITERAL).find("#x") == 0);
2104 std::string hexStr = AntlrInput::tokenTextSubstr($HEX_LITERAL, 2);
2105 atomTerm = SOLVER->mkBitVector(hexStr, 16);
2109 assert(AntlrInput::tokenText($BINARY_LITERAL).find("#b") == 0);
2110 std::string binStr = AntlrInput::tokenTextSubstr($BINARY_LITERAL, 2);
2111 atomTerm = SOLVER->mkBitVector(binStr, 2);
2115 | str[s,false] { atomTerm = PARSER_STATE->mkStringConstant(s); }
2117 // NOTE: Theory constants go here
2119 // Empty tuple constant
2122 atomTerm = SOLVER->mkTuple(std::vector<api::Sort>(),
2123 std::vector<api::Term>());
2130 attribute[CVC4::api::Term& expr, CVC4::api::Term& retExpr, std::string& attr]
2133 CVC4::api::Term patexpr;
2134 std::vector<CVC4::api::Term> patexprs;
2136 bool hasValue = false;
2138 : KEYWORD ( simpleSymbolicExprNoKeyword[sexpr] { hasValue = true; } )?
2140 attr = AntlrInput::tokenText($KEYWORD);
2141 PARSER_STATE->attributeNotSupported(attr);
2143 | ATTRIBUTE_PATTERN_TOK LPAREN_TOK
2145 { patexprs.push_back( patexpr ); }
2148 attr = std::string(":pattern");
2149 retExpr = MK_TERM(api::INST_PATTERN, patexprs);
2151 | ATTRIBUTE_NO_PATTERN_TOK term[patexpr, e2]
2153 attr = std::string(":no-pattern");
2154 retExpr = MK_TERM(api::INST_NO_PATTERN, patexpr);
2156 | tok=( ATTRIBUTE_INST_LEVEL ) INTEGER_LITERAL
2158 std::stringstream sIntLit;
2159 sIntLit << $INTEGER_LITERAL;
2160 api::Term n = SOLVER->mkReal(sIntLit.str());
2161 std::vector<api::Term> values;
2162 values.push_back( n );
2163 std::string attr_name(AntlrInput::tokenText($tok));
2164 attr_name.erase( attr_name.begin() );
2165 api::Sort boolType = SOLVER->getBooleanSort();
2166 api::Term avar = PARSER_STATE->bindVar(attr_name, boolType);
2167 retExpr = MK_TERM(api::INST_ATTRIBUTE, avar);
2168 Command* c = new SetUserAttributeCommand(
2169 attr_name, avar.getExpr(), api::termVectorToExprs(values));
2171 PARSER_STATE->preemptCommand(c);
2173 | ATTRIBUTE_NAMED_TOK symbolicExpr[sexpr]
2175 attr = std::string(":named");
2176 api::Term func = PARSER_STATE->setNamedAttribute(expr, sexpr);
2177 std::string name = sexpr.getValue();
2178 // bind name to expr with define-fun
2179 Command* c = new DefineNamedFunctionCommand(
2180 name, func.getExpr(), std::vector<Expr>(), expr.getExpr());
2182 PARSER_STATE->preemptCommand(c);
2187 * Matches a sequence of terms and puts them into the formulas
2189 * @param formulas the vector to fill with terms
2190 * @param expr an CVC4::api::Term reference for the elements of the sequence
2192 /* NOTE: We pass an CVC4::api::Term in here just to avoid allocating a fresh CVC4::api::Term every
2193 * time through this rule. */
2194 termList[std::vector<CVC4::api::Term>& formulas, CVC4::api::Term& expr]
2196 CVC4::api::Term expr2;
2198 : ( term[expr, expr2] { formulas.push_back(expr); } )+
2202 * Matches a string, and strips off the quotes.
2204 str[std::string& s, bool fsmtlib]
2207 s = AntlrInput::tokenText($STRING_LITERAL);
2208 /* strip off the quotes */
2209 s = s.substr(1, s.size() - 2);
2210 for (size_t i = 0; i < s.size(); i++)
2212 if ((unsigned)s[i] > 127 && !isprint(s[i]))
2214 PARSER_STATE->parseError(
2215 "Extended/unprintable characters are not "
2216 "part of SMT-LIB, and they must be encoded "
2217 "as escape sequences");
2220 if (fsmtlib || PARSER_STATE->escapeDupDblQuote())
2222 char* p_orig = strdup(s.c_str());
2223 char *p = p_orig, *q = p_orig;
2226 if (PARSER_STATE->escapeDupDblQuote() && *q == '"')
2228 // Handle SMT-LIB >=2.5 standard escape '""'.
2232 else if (!PARSER_STATE->escapeDupDblQuote() && *q == '\\')
2235 // Handle SMT-LIB 2.0 standard escapes '\\' and '\"'.
2236 if (*q != '\\' && *q != '"')
2251 quantOp[CVC4::api::Kind& kind]
2253 Debug("parser") << "quant: " << AntlrInput::tokenText(LT(1)) << std::endl;
2255 : EXISTS_TOK { $kind = api::EXISTS; }
2256 | FORALL_TOK { $kind = api::FORALL; }
2260 * Matches a (possibly undeclared) function symbol (returning the string)
2261 * @param check what kind of check to do with the symbol
2263 functionName[std::string& name, CVC4::parser::DeclarationCheck check]
2264 : symbol[name,check,SYM_VARIABLE]
2268 * Matches a sequence of sort symbols and fills them into the given
2271 sortList[std::vector<CVC4::api::Sort>& sorts]
2275 : ( sortSymbol[t,CHECK_DECLARED] { sorts.push_back(t); } )*
2278 nonemptySortList[std::vector<CVC4::api::Sort>& sorts]
2282 : ( sortSymbol[t,CHECK_DECLARED] { sorts.push_back(t); } )+
2286 * Matches a sequence of (variable,sort) symbol pairs and fills them
2287 * into the given vector.
2289 sortedVarList[std::vector<std::pair<std::string, CVC4::api::Sort> >& sortedVars]
2294 : ( LPAREN_TOK symbol[name,CHECK_NONE,SYM_VARIABLE]
2295 sortSymbol[t,CHECK_DECLARED] RPAREN_TOK
2296 { sortedVars.push_back(make_pair(name, t)); }
2301 * Matches a sequence of (variable, sort) symbol pairs, registers them as bound
2302 * variables, and returns a term corresponding to the list of pairs.
2304 boundVarList[CVC4::api::Term& expr]
2306 std::vector<std::pair<std::string, CVC4::api::Sort>> sortedVarNames;
2308 : LPAREN_TOK sortedVarList[sortedVarNames] RPAREN_TOK
2310 std::vector<CVC4::api::Term> args =
2311 PARSER_STATE->bindBoundVars(sortedVarNames);
2312 expr = MK_TERM(api::BOUND_VAR_LIST, args);
2317 * Matches the sort symbol, which can be an arbitrary symbol.
2318 * @param check the check to perform on the name
2320 sortName[std::string& name, CVC4::parser::DeclarationCheck check]
2321 : symbol[name,check,SYM_SORT]
2324 sortSymbol[CVC4::api::Sort& t, CVC4::parser::DeclarationCheck check]
2327 std::vector<CVC4::api::Sort> args;
2328 std::vector<uint64_t> numerals;
2329 bool indexed = false;
2331 : sortName[name,CHECK_NONE]
2333 if(check == CHECK_DECLARED || PARSER_STATE->isDeclared(name, SYM_SORT)) {
2334 t = PARSER_STATE->getSort(name);
2336 t = PARSER_STATE->mkUnresolvedType(name);
2339 | LPAREN_TOK (INDEX_TOK {indexed = true;} | {indexed = false;})
2340 symbol[name,CHECK_NONE,SYM_SORT]
2341 ( nonemptyNumeralList[numerals]
2342 { // allow sygus inputs to elide the `_'
2343 if( !indexed && !PARSER_STATE->sygus_v1() ) {
2344 std::stringstream ss;
2345 ss << "SMT-LIB requires use of an indexed sort here, e.g. (_ " << name
2347 PARSER_STATE->parseError(ss.str());
2349 if( name == "BitVec" ) {
2350 if( numerals.size() != 1 ) {
2351 PARSER_STATE->parseError("Illegal bitvector type.");
2353 if(numerals.front() == 0) {
2354 PARSER_STATE->parseError("Illegal bitvector size: 0");
2356 t = SOLVER->mkBitVectorSort(numerals.front());
2357 } else if ( name == "FloatingPoint" ) {
2358 if( numerals.size() != 2 ) {
2359 PARSER_STATE->parseError("Illegal floating-point type.");
2361 if(!validExponentSize(numerals[0])) {
2362 PARSER_STATE->parseError("Illegal floating-point exponent size");
2364 if(!validSignificandSize(numerals[1])) {
2365 PARSER_STATE->parseError("Illegal floating-point significand size");
2367 t = SOLVER->mkFloatingPointSort(numerals[0],numerals[1]);
2369 std::stringstream ss;
2370 ss << "unknown indexed sort symbol `" << name << "'";
2371 PARSER_STATE->parseError(ss.str());
2376 std::stringstream ss;
2377 ss << "Unexpected use of indexing operator `_' before `" << name
2378 << "', try leaving it out";
2379 PARSER_STATE->parseError(ss.str());
2382 PARSER_STATE->parseError("Extra parentheses around sort name not "
2383 "permitted in SMT-LIB");
2384 } else if(name == "Array" &&
2385 PARSER_STATE->isTheoryEnabled(theory::THEORY_ARRAYS) ) {
2386 if(args.size() != 2) {
2387 PARSER_STATE->parseError("Illegal array type.");
2389 t = SOLVER->mkArraySort( args[0], args[1] );
2390 } else if(name == "Set" &&
2391 PARSER_STATE->isTheoryEnabled(theory::THEORY_SETS) ) {
2392 if(args.size() != 1) {
2393 PARSER_STATE->parseError("Illegal set type.");
2395 t = SOLVER->mkSetSort( args[0] );
2396 } else if(name == "Tuple") {
2397 t = SOLVER->mkTupleSort(args);
2398 } else if(check == CHECK_DECLARED ||
2399 PARSER_STATE->isDeclared(name, SYM_SORT)) {
2400 t = PARSER_STATE->getSort(name, args);
2402 // make unresolved type
2404 t = PARSER_STATE->mkUnresolvedType(name);
2405 Debug("parser-param") << "param: make unres type " << name
2408 t = PARSER_STATE->mkUnresolvedTypeConstructor(name,args);
2409 t = t.instantiate( args );
2410 Debug("parser-param")
2411 << "param: make unres param type " << name << " " << args.size()
2412 << " " << PARSER_STATE->getArity( name ) << std::endl;
2417 | LPAREN_TOK HO_ARROW_TOK sortList[args] RPAREN_TOK
2420 PARSER_STATE->parseError("Arrow types must have at least 2 arguments");
2423 api::Sort rangeType = args.back();
2425 t = PARSER_STATE->mkFlatFunctionType( args, rangeType );
2430 * Matches a list of symbols, with check and type arguments as for the
2431 * symbol[] rule below.
2433 symbolList[std::vector<std::string>& names,
2434 CVC4::parser::DeclarationCheck check,
2435 CVC4::parser::SymbolType type]
2439 : ( symbol[id,check,type] { names.push_back(id); } )*
2443 * Matches an symbol and sets the string reference parameter id.
2444 * @param id string to hold the symbol
2445 * @param check what kinds of check to do on the symbol
2446 * @param type the intended namespace for the symbol
2448 symbol[std::string& id,
2449 CVC4::parser::DeclarationCheck check,
2450 CVC4::parser::SymbolType type]
2452 { id = AntlrInput::tokenText($SIMPLE_SYMBOL);
2453 if(!PARSER_STATE->isAbstractValue(id)) {
2454 // if an abstract value, SmtEngine handles declaration
2455 PARSER_STATE->checkDeclaration(id, check, type);
2459 { id = AntlrInput::tokenText($QUOTED_SYMBOL);
2460 /* strip off the quotes */
2461 id = id.substr(1, id.size() - 2);
2462 if(!PARSER_STATE->isAbstractValue(id)) {
2463 // if an abstract value, SmtEngine handles declaration
2464 PARSER_STATE->checkDeclaration(id, check, type);
2467 | UNTERMINATED_QUOTED_SYMBOL
2469 { PARSER_STATE->unexpectedEOF("unterminated |quoted| symbol"); }
2471 { PARSER_STATE->unexpectedEOF("backslash not permitted in |quoted| "
2477 * Matches a nonempty list of numerals.
2478 * @param numerals the (empty) vector to house the numerals.
2480 nonemptyNumeralList[std::vector<uint64_t>& numerals]
2482 { numerals.push_back(AntlrInput::tokenToUnsigned($INTEGER_LITERAL)); }
2487 * Parses a datatype definition
2489 datatypeDef[bool isCo, std::vector<CVC4::api::DatatypeDecl>& datatypes,
2490 std::vector< CVC4::api::Sort >& params]
2494 /* This really needs to be CHECK_NONE, or mutually-recursive
2495 * datatypes won't work, because this type will already be
2496 * "defined" as an unresolved type; don't worry, we check
2498 : symbol[id,CHECK_NONE,SYM_SORT] { PARSER_STATE->pushScope(true); }
2500 datatypes.push_back(SOLVER->mkDatatypeDecl(id, params, isCo));
2502 ( LPAREN_TOK constructorDef[datatypes.back()] RPAREN_TOK )+
2503 { PARSER_STATE->popScope(); }
2507 * Parses a constructor defintion for type
2509 constructorDef[CVC4::api::DatatypeDecl& type]
2512 CVC4::api::DatatypeConstructorDecl* ctor = NULL;
2514 : symbol[id,CHECK_NONE,SYM_VARIABLE]
2516 ctor = new api::DatatypeConstructorDecl(id);
2518 ( LPAREN_TOK selector[*ctor] RPAREN_TOK )*
2519 { // make the constructor
2520 type.addConstructor(*ctor);
2521 Debug("parser-idt") << "constructor: " << id.c_str() << std::endl;
2526 selector[CVC4::api::DatatypeConstructorDecl& ctor]
2529 CVC4::api::Sort t, t2;
2531 : symbol[id,CHECK_NONE,SYM_SORT] sortSymbol[t,CHECK_NONE]
2533 ctor.addSelector(id, t);
2534 Debug("parser-idt") << "selector: " << id.c_str()
2535 << " of type " << t << std::endl;
2539 // Base SMT-LIB tokens
2540 ASSERT_TOK : 'assert';
2541 CHECK_SAT_TOK : 'check-sat';
2542 CHECK_SAT_ASSUMING_TOK : 'check-sat-assuming';
2543 DECLARE_FUN_TOK : 'declare-fun';
2544 DECLARE_SORT_TOK : 'declare-sort';
2545 DEFINE_FUN_TOK : 'define-fun';
2546 DEFINE_FUN_REC_TOK : 'define-fun-rec';
2547 DEFINE_FUNS_REC_TOK : 'define-funs-rec';
2548 DEFINE_SORT_TOK : 'define-sort';
2549 GET_VALUE_TOK : 'get-value';
2550 GET_ASSIGNMENT_TOK : 'get-assignment';
2551 GET_ASSERTIONS_TOK : 'get-assertions';
2552 GET_PROOF_TOK : 'get-proof';
2553 GET_UNSAT_ASSUMPTIONS_TOK : 'get-unsat-assumptions';
2554 GET_UNSAT_CORE_TOK : 'get-unsat-core';
2556 RESET_TOK : { PARSER_STATE->v2_5() }? 'reset';
2557 RESET_ASSERTIONS_TOK : 'reset-assertions';
2558 LET_TOK : { !PARSER_STATE->sygus_v1() }? 'let';
2559 SYGUS_LET_TOK : { PARSER_STATE->sygus_v1() }? 'let';
2560 ATTRIBUTE_TOK : '!';
2564 SET_LOGIC_TOK : 'set-logic';
2565 SET_INFO_TOK : 'set-info';
2566 GET_INFO_TOK : 'get-info';
2567 SET_OPTION_TOK : 'set-option';
2568 GET_OPTION_TOK : 'get-option';
2572 CONST_TOK : { !PARSER_STATE->strictModeEnabled() }? 'const';
2574 // extended commands
2575 DECLARE_CODATATYPE_TOK : { PARSER_STATE->v2_6() || PARSER_STATE->sygus() }? 'declare-codatatype';
2576 DECLARE_DATATYPE_TOK : { PARSER_STATE->v2_6() || PARSER_STATE->sygus() }? 'declare-datatype';
2577 DECLARE_DATATYPES_2_5_TOK : { !( PARSER_STATE->v2_6() || PARSER_STATE->sygus() ) }?'declare-datatypes';
2578 DECLARE_DATATYPES_TOK : { PARSER_STATE->v2_6() || PARSER_STATE->sygus() }?'declare-datatypes';
2579 DECLARE_CODATATYPES_2_5_TOK : { !( PARSER_STATE->v2_6() || PARSER_STATE->sygus() ) }?'declare-codatatypes';
2580 DECLARE_CODATATYPES_TOK : { PARSER_STATE->v2_6() || PARSER_STATE->sygus() }?'declare-codatatypes';
2581 PAR_TOK : { PARSER_STATE->v2_6() }?'par';
2582 COMPREHENSION_TOK : { PARSER_STATE->isTheoryEnabled(theory::THEORY_SETS) }?'comprehension';
2583 TESTER_TOK : { ( PARSER_STATE->v2_6() || PARSER_STATE->sygus() ) && PARSER_STATE->isTheoryEnabled(theory::THEORY_DATATYPES) }?'is';
2584 MATCH_TOK : { ( PARSER_STATE->v2_6() || PARSER_STATE->sygus() ) && PARSER_STATE->isTheoryEnabled(theory::THEORY_DATATYPES) }?'match';
2585 GET_MODEL_TOK : 'get-model';
2586 BLOCK_MODEL_TOK : 'block-model';
2587 BLOCK_MODEL_VALUES_TOK : 'block-model-values';
2589 DECLARE_SORTS_TOK : 'declare-sorts';
2590 DECLARE_FUNS_TOK : 'declare-funs';
2591 DECLARE_PREDS_TOK : 'declare-preds';
2592 DEFINE_TOK : 'define';
2593 DECLARE_CONST_TOK : 'declare-const';
2594 DEFINE_CONST_TOK : 'define-const';
2595 SIMPLIFY_TOK : 'simplify';
2596 INCLUDE_TOK : 'include';
2597 GET_QE_TOK : 'get-qe';
2598 GET_QE_DISJUNCT_TOK : 'get-qe-disjunct';
2599 GET_ABDUCT_TOK : 'get-abduct';
2600 DECLARE_HEAP : 'declare-heap';
2603 SYNTH_FUN_V1_TOK : { PARSER_STATE->sygus_v1() }?'synth-fun';
2604 SYNTH_FUN_TOK : { PARSER_STATE->sygus() && !PARSER_STATE->sygus_v1() }?'synth-fun';
2605 SYNTH_INV_V1_TOK : { PARSER_STATE->sygus_v1()}?'synth-inv';
2606 SYNTH_INV_TOK : { PARSER_STATE->sygus() && !PARSER_STATE->sygus_v1()}?'synth-inv';
2607 CHECK_SYNTH_TOK : { PARSER_STATE->sygus()}?'check-synth';
2608 DECLARE_VAR_TOK : { PARSER_STATE->sygus()}?'declare-var';
2609 DECLARE_PRIMED_VAR_TOK : { PARSER_STATE->sygus_v1() }?'declare-primed-var';
2610 CONSTRAINT_TOK : { PARSER_STATE->sygus()}?'constraint';
2611 INV_CONSTRAINT_TOK : { PARSER_STATE->sygus()}?'inv-constraint';
2612 SET_OPTIONS_TOK : { PARSER_STATE->sygus() }? 'set-options';
2613 SYGUS_CONSTANT_TOK : { PARSER_STATE->sygus() }? 'Constant';
2614 SYGUS_VARIABLE_TOK : { PARSER_STATE->sygus() }? 'Variable';
2615 SYGUS_INPUT_VARIABLE_TOK : { PARSER_STATE->sygus_v1() }? 'InputVariable';
2616 SYGUS_LOCAL_VARIABLE_TOK : { PARSER_STATE->sygus_v1() }? 'LocalVariable';
2619 ATTRIBUTE_PATTERN_TOK : ':pattern';
2620 ATTRIBUTE_NO_PATTERN_TOK : ':no-pattern';
2621 ATTRIBUTE_NAMED_TOK : ':named';
2622 ATTRIBUTE_INST_LEVEL : ':quant-inst-max-level';
2624 // operators (NOTE: theory symbols go here)
2625 EXISTS_TOK : 'exists';
2626 FORALL_TOK : 'forall';
2628 EMP_TOK : { PARSER_STATE->isTheoryEnabled(theory::THEORY_SEP) }? 'emp';
2629 CHAR_TOK : { PARSER_STATE->isTheoryEnabled(theory::THEORY_STRINGS) }? 'char';
2630 TUPLE_CONST_TOK: { PARSER_STATE->isTheoryEnabled(theory::THEORY_DATATYPES) }? 'mkTuple';
2631 TUPLE_SEL_TOK: { PARSER_STATE->isTheoryEnabled(theory::THEORY_DATATYPES) }? 'tupSel';
2633 HO_ARROW_TOK : { PARSER_STATE->isHoEnabled() }? '->';
2634 HO_LAMBDA_TOK : { PARSER_STATE->isHoEnabled() }? 'lambda';
2637 * A sequence of printable ASCII characters (except backslash) that starts
2638 * and ends with | and does not otherwise contain |.
2640 * You shouldn't generally use this in parser rules, as the |quoting|
2641 * will be part of the token text. Use the symbol[] parser rule instead.
2644 : '|' ~('|' | '\\')* '|'
2646 UNTERMINATED_QUOTED_SYMBOL
2647 : '|' ~('|' | '\\')*
2651 * Matches a keyword from the input. A keyword is a simple symbol prefixed
2655 : ':' (ALPHA | DIGIT | SYMBOL_CHAR)+
2659 * Matches a "simple" symbol: a non-empty sequence of letters, digits and
2660 * the characters + - / * = % ? ! . $ ~ & ^ < > @ that does not start with a
2661 * digit, and is not the special reserved symbols '!' or '_'.
2664 : ALPHA (ALPHA | DIGIT | SYMBOL_CHAR)*
2665 | SYMBOL_CHAR (ALPHA | DIGIT | SYMBOL_CHAR)+
2666 | SYMBOL_CHAR_NOUNDERSCORE_NOATTRIBUTE
2670 * Matches and skips whitespace in the input.
2673 : (' ' | '\t' | '\f' | '\r' | '\n')+ { SKIP(); }
2677 * Matches an integer constant from the input (non-empty sequence of
2678 * digits, with no leading zeroes).
2685 * Match an integer constant. In non-strict mode, this is any sequence
2686 * of digits. In strict mode, non-zero integers can't have leading
2691 char *start = (char*) GETCHARINDEX();
2694 { Debug("parser-extra") << "NUMERAL: "
2695 << (uintptr_t)start << ".." << GETCHARINDEX()
2696 << " strict? " << (bool)(PARSER_STATE->strictModeEnabled())
2697 << " ^0? " << (bool)(*start == '0')
2698 << " len>1? " << (bool)(start < (char*)(GETCHARINDEX() - 1))
2700 { !PARSER_STATE->strictModeEnabled() ||
2702 start == (char*)(GETCHARINDEX() - 1) }?
2706 * Matches a decimal constant from the input.
2709 : NUMERAL '.' DIGIT+
2713 * Matches a hexadecimal constant.
2720 * Matches a binary constant.
2727 * Matches a double-quoted string literal. Depending on the language that is
2728 * being parsed, different escape sequences are supported:
2730 * For SMT-LIB 2.0 the sequence \" is interpreted as a double quote (") and the
2731 * sequence \\ is interpreted as a backslash (\).
2733 * For SMT-LIB >=2.5 and SyGuS a double-quote inside a string is escaped with
2734 * "", e.g., "This is a string literal with "" a single, embedded double
2737 * You shouldn't generally use this in parser rules, as the quotes
2738 * will be part of the token text. Use the str[] parser rule instead.
2741 : { !PARSER_STATE->escapeDupDblQuote() }?=>
2742 '"' ('\\' . | ~('\\' | '"'))* '"'
2743 | { PARSER_STATE->escapeDupDblQuote() }?=>
2744 '"' (~('"') | '""')* '"'
2748 * Matches the comments and ignores them
2751 : ';' (~('\n' | '\r'))* { SKIP(); }
2755 * Matches any letter ('a'-'z' and 'A'-'Z').
2764 * Matches the digits (0-9)
2766 fragment DIGIT : '0'..'9';
2768 fragment HEX_DIGIT : DIGIT | 'a'..'f' | 'A'..'F';
2771 * Matches the characters that may appear as a one-character "symbol"
2772 * (which excludes _ and !, which are reserved words in SMT-LIB).
2774 fragment SYMBOL_CHAR_NOUNDERSCORE_NOATTRIBUTE
2775 : '+' | '-' | '/' | '*' | '=' | '%' | '?' | '.' | '$' | '~'
2776 | '&' | '^' | '<' | '>' | '@'
2780 * Matches the characters that may appear in a "symbol" (i.e., an identifier)
2782 fragment SYMBOL_CHAR
2783 : SYMBOL_CHAR_NOUNDERSCORE_NOATTRIBUTE | '_' | '!'