1 /* ******************* */
4 ** Top contributors (to current version):
5 ** Morgan Deters, Andrew Reynolds, Christopher L. Conway
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2016 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 should come immediately after #include <antlr3.h> in the generated
45 // files. See the documentation in "parser/antlr_undefines.h" for more details.
46 #include "parser/antlr_undefines.h"
48 /** This suppresses warnings about the redefinition of token symbols between
49 * different parsers. The redefinitions should be harmless as long as no
50 * client: (a) #include's the lexer headers for two grammars AND (b) uses the
51 * token symbol definitions.
53 #pragma GCC system_header
55 #if defined(CVC4_COMPETITION_MODE) && !defined(CVC4_SMTCOMP_APPLICATION_TRACK)
56 /* This improves performance by ~10 percent on big inputs.
57 * This option is only valid if we know the input is ASCII (or some 8-bit encoding).
58 * If we know the input is UTF-16, we can use ANTLR3_INLINE_INPUT_UTF16.
59 * Otherwise, we have to let the lexer detect the encoding at runtime.
61 # define ANTLR3_INLINE_INPUT_ASCII
62 # define ANTLR3_INLINE_INPUT_8BIT
63 #endif /* CVC4_COMPETITION_MODE && !CVC4_SMTCOMP_APPLICATION_TRACK */
65 #include "parser/antlr_tracing.h"
67 }/* @lexer::includes */
72 #include "parser/smt2/smt2.h"
73 #include "parser/antlr_input.h"
76 using namespace CVC4::parser;
79 #define PARSER_STATE ((Smt2*)LEXER->super)
80 }/* @lexer::postinclude */
84 // This should come immediately after #include <antlr3.h> in the generated
85 // files. See the documentation in "parser/antlr_undefines.h" for more details.
86 #include "parser/antlr_undefines.h"
88 #include "base/ptr_closer.h"
89 #include "parser/parser.h"
90 #include "parser/antlr_tracing.h"
91 #include "smt/command.h"
99 * Just exists to provide the uintptr_t constructor that ANTLR
102 struct myExpr : public CVC4::Expr {
103 myExpr() : CVC4::Expr() {}
104 myExpr(void*) : CVC4::Expr() {}
105 myExpr(const Expr& e) : CVC4::Expr(e) {}
106 myExpr(const myExpr& e) : CVC4::Expr(e) {}
107 };/* struct myExpr */
108 }/* CVC4::parser::smt2 namespace */
109 }/* CVC4::parser namespace */
110 }/* CVC4 namespace */
112 }/* @parser::includes */
114 @parser::postinclude {
121 #include "base/output.h"
122 #include "expr/expr.h"
123 #include "expr/kind.h"
124 #include "expr/type.h"
125 #include "options/set_language.h"
126 #include "parser/antlr_input.h"
127 #include "parser/parser.h"
128 #include "parser/smt2/smt2.h"
129 #include "util/floatingpoint.h"
130 #include "util/hash.h"
131 #include "util/integer.h"
132 #include "util/rational.h"
133 // \todo Review the need for this header
136 using namespace CVC4;
137 using namespace CVC4::parser;
139 /* These need to be macros so they can refer to the PARSER macro, which
140 * will be defined by ANTLR *after* this section. (If they were functions,
141 * PARSER would be undefined.) */
143 #define PARSER_STATE ((Smt2*)PARSER->super)
145 #define EXPR_MANAGER PARSER_STATE->getExprManager()
147 #define MK_EXPR EXPR_MANAGER->mkExpr
149 #define MK_CONST EXPR_MANAGER->mkConst
150 #define UNSUPPORTED PARSER_STATE->unimplementedFeature
152 static bool isClosed(const Expr& e, std::set<Expr>& free, std::hash_set<Expr, ExprHashFunction>& closedCache) {
153 if(closedCache.find(e) != closedCache.end()) {
157 if(e.getKind() == kind::FORALL || e.getKind() == kind::EXISTS || e.getKind() == kind::LAMBDA) {
158 isClosed(e[1], free, closedCache);
159 for(Expr::const_iterator i = e[0].begin(); i != e[0].end(); ++i) {
162 } else if(e.getKind() == kind::BOUND_VARIABLE) {
166 if(e.hasOperator()) {
167 isClosed(e.getOperator(), free, closedCache);
169 for(Expr::const_iterator i = e.begin(); i != e.end(); ++i) {
170 isClosed(*i, free, closedCache);
175 closedCache.insert(e);
182 static inline bool isClosed(const Expr& e, std::set<Expr>& free) {
183 std::hash_set<Expr, ExprHashFunction> cache;
184 return isClosed(e, free, cache);
187 }/* parser::postinclude */
190 * Parses an expression.
191 * @return the parsed expression, or the Null Expr if we've reached the
194 parseExpr returns [CVC4::parser::smt2::myExpr expr]
204 * @return the parsed command, or NULL if we've reached the end of the input
206 parseCommand returns [CVC4::Command* cmd_return = NULL]
208 CVC4::PtrCloser<CVC4::Command> cmd;
212 cmd_return = cmd.release();
214 : LPAREN_TOK command[&cmd] RPAREN_TOK
216 /* This extended command has to be in the outermost production so that
217 * the RPAREN_TOK is properly eaten and we are in a good state to read
218 * the included file's tokens. */
219 | LPAREN_TOK INCLUDE_TOK str[name,true] RPAREN_TOK
220 { if(!PARSER_STATE->canIncludeFile()) {
221 PARSER_STATE->parseError("include-file feature was disabled for this "
224 if(PARSER_STATE->strictModeEnabled()) {
225 PARSER_STATE->parseError("Extended commands are not permitted while "
226 "operating in strict compliance mode.");
228 PARSER_STATE->includeFile(name);
229 // The command of the included file will be produced at the next
230 // parseCommand() call
231 cmd.reset(new EmptyCommand("include::" + name));
238 * Parses a SyGuS command.
239 * @return the parsed SyGuS command, or NULL if we've reached the end of the
242 parseSygus returns [CVC4::Command* cmd_return = NULL]
244 CVC4::PtrCloser<CVC4::Command> cmd;
248 cmd_return = cmd.release();
250 : LPAREN_TOK sygusCommand[&cmd] RPAREN_TOK
255 * Parse the internal portion of the command, ignoring the surrounding
258 command [CVC4::PtrCloser<CVC4::Command>* cmd]
261 std::vector<std::string> names;
264 std::vector<Expr> terms;
265 std::vector<Type> sorts;
266 std::vector<std::pair<std::string, Type> > sortedVarNames;
268 : /* set the logic */
269 SET_LOGIC_TOK symbol[name,CHECK_NONE,SYM_SORT]
270 { Debug("parser") << "set logic: '" << name << "'" << std::endl;
271 if( PARSER_STATE->logicIsSet() ) {
272 PARSER_STATE->parseError("Only one set-logic is allowed.");
274 PARSER_STATE->setLogic(name);
275 if( PARSER_STATE->sygus() ){
276 cmd->reset(new SetBenchmarkLogicCommand(PARSER_STATE->getLogic().getLogicString()));
278 cmd->reset(new SetBenchmarkLogicCommand(name));
282 SET_INFO_TOK metaInfoInternal[cmd]
285 { cmd->reset(new GetInfoCommand(
286 AntlrInput::tokenText($KEYWORD).c_str() + 1));
289 SET_OPTION_TOK setOptionInternal[cmd]
291 GET_OPTION_TOK KEYWORD
292 { cmd->reset(new GetOptionCommand(
293 AntlrInput::tokenText($KEYWORD).c_str() + 1));
295 | /* sort declaration */
296 DECLARE_SORT_TOK { PARSER_STATE->checkThatLogicIsSet(); }
297 { if(!PARSER_STATE->isTheoryEnabled(Smt2::THEORY_UF) &&
298 !PARSER_STATE->isTheoryEnabled(Smt2::THEORY_ARRAYS) &&
299 !PARSER_STATE->isTheoryEnabled(Smt2::THEORY_DATATYPES) &&
300 !PARSER_STATE->isTheoryEnabled(Smt2::THEORY_SETS)) {
301 PARSER_STATE->parseErrorLogic("Free sort symbols not allowed in ");
304 symbol[name,CHECK_UNDECLARED,SYM_SORT]
305 { PARSER_STATE->checkUserSymbol(name); }
307 { Debug("parser") << "declare sort: '" << name
308 << "' arity=" << n << std::endl;
309 unsigned arity = AntlrInput::tokenToUnsigned(n);
311 Type type = PARSER_STATE->mkSort(name);
312 cmd->reset(new DeclareTypeCommand(name, 0, type));
314 Type type = PARSER_STATE->mkSortConstructor(name, arity);
315 cmd->reset(new DeclareTypeCommand(name, arity, type));
318 | /* sort definition */
319 DEFINE_SORT_TOK { PARSER_STATE->checkThatLogicIsSet(); }
320 symbol[name,CHECK_UNDECLARED,SYM_SORT]
321 { PARSER_STATE->checkUserSymbol(name); }
322 LPAREN_TOK symbolList[names,CHECK_NONE,SYM_SORT] RPAREN_TOK
323 { PARSER_STATE->pushScope(true);
324 for(std::vector<std::string>::const_iterator i = names.begin(),
328 sorts.push_back(PARSER_STATE->mkSort(*i));
331 sortSymbol[t,CHECK_DECLARED]
332 { PARSER_STATE->popScope();
333 // Do NOT call mkSort, since that creates a new sort!
334 // This name is not its own distinct sort, it's an alias.
335 PARSER_STATE->defineParameterizedType(name, sorts, t);
336 cmd->reset(new DefineTypeCommand(name, sorts, t));
338 | /* function declaration */
339 DECLARE_FUN_TOK { PARSER_STATE->checkThatLogicIsSet(); }
340 symbol[name,CHECK_UNDECLARED,SYM_VARIABLE]
341 { PARSER_STATE->checkUserSymbol(name); }
342 LPAREN_TOK sortList[sorts] RPAREN_TOK
343 sortSymbol[t,CHECK_DECLARED]
344 { Debug("parser") << "declare fun: '" << name << "'" << std::endl;
345 if( sorts.size() > 0 ) {
346 if(!PARSER_STATE->isTheoryEnabled(Smt2::THEORY_UF)) {
347 PARSER_STATE->parseErrorLogic("Functions (of non-zero arity) cannot "
348 "be declared in logic ");
350 t = EXPR_MANAGER->mkFunctionType(sorts, t);
352 Expr func = PARSER_STATE->mkVar(name, t);
353 cmd->reset(new DeclareFunctionCommand(name, func, t));
355 | /* function definition */
356 DEFINE_FUN_TOK { PARSER_STATE->checkThatLogicIsSet(); }
357 symbol[name,CHECK_UNDECLARED,SYM_VARIABLE]
358 { PARSER_STATE->checkUserSymbol(name); }
359 LPAREN_TOK sortedVarList[sortedVarNames] RPAREN_TOK
360 sortSymbol[t,CHECK_DECLARED]
361 { /* add variables to parser state before parsing term */
362 Debug("parser") << "define fun: '" << name << "'" << std::endl;
363 if( sortedVarNames.size() > 0 ) {
364 std::vector<CVC4::Type> sorts;
365 sorts.reserve(sortedVarNames.size());
366 for(std::vector<std::pair<std::string, CVC4::Type> >::const_iterator i =
367 sortedVarNames.begin(), iend = sortedVarNames.end();
370 sorts.push_back((*i).second);
372 t = EXPR_MANAGER->mkFunctionType(sorts, t);
374 PARSER_STATE->pushScope(true);
375 for(std::vector<std::pair<std::string, CVC4::Type> >::const_iterator i =
376 sortedVarNames.begin(), iend = sortedVarNames.end();
379 terms.push_back(PARSER_STATE->mkBoundVar((*i).first, (*i).second));
383 { PARSER_STATE->popScope();
384 // declare the name down here (while parsing term, signature
385 // must not be extended with the name itself; no recursion
387 Expr func = PARSER_STATE->mkFunction(name, t,
388 ExprManager::VAR_FLAG_DEFINED);
389 cmd->reset(new DefineFunctionCommand(name, func, terms, expr));
392 GET_VALUE_TOK { PARSER_STATE->checkThatLogicIsSet(); }
393 ( LPAREN_TOK termList[terms,expr] RPAREN_TOK
394 { cmd->reset(new GetValueCommand(terms)); }
396 { PARSER_STATE->parseError("The get-value command expects a list of "
397 "terms. Perhaps you forgot a pair of "
401 | /* get-assignment */
402 GET_ASSIGNMENT_TOK { PARSER_STATE->checkThatLogicIsSet(); }
403 { cmd->reset(new GetAssignmentCommand()); }
405 ASSERT_TOK { PARSER_STATE->checkThatLogicIsSet(); }
406 /* { if( PARSER_STATE->sygus() ){
407 * PARSER_STATE->parseError("Sygus does not support assert command.");
410 { PARSER_STATE->clearLastNamedTerm(); }
412 { bool inUnsatCore = PARSER_STATE->lastNamedTerm().first == expr;
413 cmd->reset(new AssertCommand(expr, inUnsatCore));
415 PARSER_STATE->registerUnsatCoreName(PARSER_STATE->lastNamedTerm());
419 CHECKSAT_TOK { PARSER_STATE->checkThatLogicIsSet(); }
420 { if( PARSER_STATE->sygus() ){
421 PARSER_STATE->parseError("Sygus does not support check-sat command.");
425 { if(PARSER_STATE->strictModeEnabled()) {
426 PARSER_STATE->parseError(
427 "Extended commands (such as check-sat with an argument) are not "
428 "permitted while operating in strict compliance mode.");
431 | { expr = MK_CONST(bool(true)); }
433 { cmd->reset(new CheckSatCommand(expr)); }
434 | /* get-assertions */
435 GET_ASSERTIONS_TOK { PARSER_STATE->checkThatLogicIsSet(); }
436 { cmd->reset(new GetAssertionsCommand()); }
438 GET_PROOF_TOK { PARSER_STATE->checkThatLogicIsSet(); }
439 { cmd->reset(new GetProofCommand()); }
440 | /* get-unsat-core */
441 GET_UNSAT_CORE_TOK { PARSER_STATE->checkThatLogicIsSet(); }
442 { cmd->reset(new GetUnsatCoreCommand(PARSER_STATE->getUnsatCoreNames())); }
444 PUSH_TOK { PARSER_STATE->checkThatLogicIsSet(); }
445 { if( PARSER_STATE->sygus() ){
446 PARSER_STATE->parseError("Sygus does not support push command.");
450 { unsigned n = AntlrInput::tokenToUnsigned(k);
452 cmd->reset(new EmptyCommand());
454 PARSER_STATE->pushScope();
455 PARSER_STATE->pushUnsatCoreNameScope();
456 cmd->reset(new PushCommand());
458 CVC4::PtrCloser<CommandSequence> seq(new CommandSequence());
460 PARSER_STATE->pushScope();
461 PARSER_STATE->pushUnsatCoreNameScope();
462 Command* push_cmd = new PushCommand();
463 push_cmd->setMuted(n > 1);
464 seq->addCommand(push_cmd);
467 cmd->reset(seq.release());
470 | { if(PARSER_STATE->strictModeEnabled()) {
471 PARSER_STATE->parseError(
472 "Strict compliance mode demands an integer to be provided to "
473 "PUSH. Maybe you want (push 1)?");
475 PARSER_STATE->pushScope();
476 PARSER_STATE->pushUnsatCoreNameScope();
477 cmd->reset(new PushCommand());
480 | POP_TOK { PARSER_STATE->checkThatLogicIsSet(); }
481 { if( PARSER_STATE->sygus() ){
482 PARSER_STATE->parseError("Sygus does not support pop command.");
486 { unsigned n = AntlrInput::tokenToUnsigned(k);
487 if(n > PARSER_STATE->scopeLevel()) {
488 PARSER_STATE->parseError("Attempted to pop above the top stack "
492 cmd->reset(new EmptyCommand());
494 PARSER_STATE->popUnsatCoreNameScope();
495 PARSER_STATE->popScope();
496 cmd->reset(new PopCommand());
498 CVC4::PtrCloser<CommandSequence> seq(new CommandSequence());
500 PARSER_STATE->popUnsatCoreNameScope();
501 PARSER_STATE->popScope();
502 Command* pop_command = new PopCommand();
503 pop_command->setMuted(n > 1);
504 seq->addCommand(pop_command);
507 cmd->reset(seq.release());
510 | { if(PARSER_STATE->strictModeEnabled()) {
511 PARSER_STATE->parseError(
512 "Strict compliance mode demands an integer to be provided to POP."
513 "Maybe you want (pop 1)?");
515 PARSER_STATE->popUnsatCoreNameScope();
516 PARSER_STATE->popScope();
517 cmd->reset(new PopCommand());
523 { cmd->reset(new QuitCommand()); }
525 /* New SMT-LIB 2.5 command set */
527 { if(PARSER_STATE->v2_0() && PARSER_STATE->strictModeEnabled()) {
528 PARSER_STATE->parseError(
529 "SMT-LIB 2.5 commands are not permitted while operating in strict "
530 "compliance mode and in SMT-LIB 2.0 mode.");
534 /* CVC4-extended SMT-LIB commands */
535 | extendedCommand[cmd]
536 { if(PARSER_STATE->strictModeEnabled()) {
537 PARSER_STATE->parseError(
538 "Extended commands are not permitted while operating in strict "
545 { std::string id = AntlrInput::tokenText($SIMPLE_SYMBOL);
546 if(id == "benchmark") {
547 PARSER_STATE->parseError(
548 "In SMT-LIBv2 mode, but got something that looks like SMT-LIBv1. "
549 "Use --lang smt1 for SMT-LIBv1.");
551 PARSER_STATE->parseError("expected SMT-LIBv2 command, got `" + id +
557 sygusCommand [CVC4::PtrCloser<CVC4::Command>* cmd]
559 std::string name, fun;
560 std::vector<std::string> names;
563 std::vector<Expr> terms;
564 std::vector<Type> sorts;
565 std::vector<Expr> sygus_vars;
566 std::vector<std::pair<std::string, Type> > sortedVarNames;
568 CVC4::PtrCloser<CVC4::CommandSequence> seq;
569 std::vector< std::vector< CVC4::SygusGTerm > > sgts;
570 std::vector< CVC4::Datatype > datatypes;
571 std::vector< std::vector<Expr> > ops;
572 std::vector< std::vector< std::string > > cnames;
573 std::vector< std::vector< std::vector< CVC4::Type > > > cargs;
574 std::vector< bool > allow_const;
575 std::vector< std::vector< std::string > > unresolved_gterm_sym;
576 bool read_syntax = false;
578 std::map< CVC4::Type, CVC4::Type > sygus_to_builtin;
579 std::map< CVC4::Type, CVC4::Expr > sygus_to_builtin_expr;
583 DECLARE_VAR_TOK { PARSER_STATE->checkThatLogicIsSet(); }
584 symbol[name,CHECK_UNDECLARED,SYM_VARIABLE]
585 { PARSER_STATE->checkUserSymbol(name); }
586 sortSymbol[t,CHECK_DECLARED]
587 { PARSER_STATE->mkSygusVar(name, t);
588 cmd->reset(new EmptyCommand());
590 | /* declare-primed-var */
591 DECLARE_PRIMED_VAR_TOK { PARSER_STATE->checkThatLogicIsSet(); }
592 symbol[name,CHECK_UNDECLARED,SYM_VARIABLE]
593 { PARSER_STATE->checkUserSymbol(name); }
594 sortSymbol[t,CHECK_DECLARED]
595 { PARSER_STATE->mkSygusVar(name, t, true);
596 cmd->reset(new EmptyCommand());
600 ( SYNTH_FUN_TOK | SYNTH_INV_TOK { range = EXPR_MANAGER->booleanType(); } )
601 { PARSER_STATE->checkThatLogicIsSet(); }
602 symbol[fun,CHECK_UNDECLARED,SYM_VARIABLE]
603 LPAREN_TOK sortedVarList[sortedVarNames] RPAREN_TOK
604 { seq.reset(new CommandSequence());
605 PARSER_STATE->pushScope(true);
606 for(std::vector<std::pair<std::string, CVC4::Type> >::const_iterator i =
607 sortedVarNames.begin(), iend = sortedVarNames.end(); i != iend;
609 Expr v = PARSER_STATE->mkBoundVar((*i).first, (*i).second);
610 terms.push_back( v );
611 sygus_vars.push_back( v );
614 if( !terms.empty() ){
615 bvl = MK_EXPR(kind::BOUND_VAR_LIST, terms);
618 terms.push_back(bvl);
620 ( sortSymbol[range,CHECK_DECLARED] )? {
621 if( range.isNull() ){
622 PARSER_STATE->parseError("Must supply return type for synth-fun.");
627 symbol[name,CHECK_NONE,SYM_VARIABLE]
628 sortSymbol[t,CHECK_DECLARED]
629 { std::stringstream ss;
630 ss << fun << "_" << name;
632 startIndex = datatypes.size();
634 std::string dname = ss.str();
635 sgts.push_back( std::vector< CVC4::SygusGTerm >() );
636 sgts.back().push_back( CVC4::SygusGTerm() );
637 PARSER_STATE->pushSygusDatatypeDef(
638 t, dname, datatypes, sorts, ops, cnames, cargs, allow_const,
639 unresolved_gterm_sym);
641 if(!PARSER_STATE->isUnresolvedType(dname)) {
642 // if not unresolved, must be undeclared
643 Debug("parser-sygus") << "Make unresolved type : " << dname
645 PARSER_STATE->checkDeclaration(dname, CHECK_UNDECLARED, SYM_SORT);
646 unres_t = PARSER_STATE->mkUnresolvedType(dname);
648 Debug("parser-sygus") << "Get sort : " << dname << std::endl;
649 unres_t = PARSER_STATE->getSort(dname);
651 sygus_to_builtin[unres_t] = t;
652 Debug("parser-sygus") << "--- Read sygus grammar " << name
653 << " under function " << fun << "..."
655 << " type to resolve " << unres_t << std::endl
656 << " builtin type " << t << std::endl;
658 // Note the official spec for NTDef is missing the ( parens )
659 // but they are necessary to parse SyGuS examples
660 LPAREN_TOK ( sygusGTerm[ sgts.back().back(), fun]
661 { sgts.back().push_back( CVC4::SygusGTerm() ); } )+
662 RPAREN_TOK { sgts.back().pop_back(); }
665 RPAREN_TOK { read_syntax = true; }
669 //create the default grammar
670 Debug("parser-sygus") << "Make default grammar..." << std::endl;
671 PARSER_STATE->mkSygusDefaultGrammar(
672 range, terms[0], fun, datatypes, sorts, ops, sygus_vars,
675 Debug("parser-sygus") << "Set start index " << startIndex << "..."
677 PARSER_STATE->setSygusStartIndex(fun, startIndex, datatypes, sorts,
680 Debug("parser-sygus") << "--- Process " << sgts.size()
681 << " sygus gterms..." << std::endl;
682 for( unsigned i=0; i<sgts.size(); i++ ){
683 for( unsigned j=0; j<sgts[i].size(); j++ ){
685 PARSER_STATE->processSygusGTerm(
686 sgts[i][j], i, datatypes, sorts, ops, cnames, cargs,
687 allow_const, unresolved_gterm_sym, sygus_vars, sygus_to_builtin,
688 sygus_to_builtin_expr, sub_ret );
691 //swap index if necessary
692 Debug("parser-sygus") << "--- Making sygus datatypes..." << std::endl;
693 for( unsigned i=0; i<datatypes.size(); i++ ){
694 Debug("parser-sygus") << "..." << datatypes[i].getName()
695 << " has builtin sort " << sorts[i]
698 for( unsigned i=0; i<datatypes.size(); i++ ){
699 Debug("parser-sygus") << "...make " << datatypes[i].getName()
700 << " with builtin sort " << sorts[i]
702 if( sorts[i].isNull() ){
703 PARSER_STATE->parseError("Internal error : could not infer "
704 "builtin sort for nested gterm.");
706 datatypes[i].setSygus( sorts[i], terms[0], allow_const[i], false );
707 PARSER_STATE->mkSygusDatatype(
708 datatypes[i], ops[i], cnames[i], cargs[i],
709 unresolved_gterm_sym[i], sygus_to_builtin );
711 PARSER_STATE->setSygusStartIndex(fun, startIndex, datatypes, sorts,
714 //only care about datatypes/sorts/ops past here
715 PARSER_STATE->popScope();
716 Debug("parser-sygus") << "--- Make " << datatypes.size()
717 << " mutual datatypes..." << std::endl;
718 for( unsigned i=0; i<datatypes.size(); i++ ){
719 Debug("parser-sygus") << " " << i << " : " << datatypes[i].getName()
722 std::vector<DatatypeType> datatypeTypes =
723 PARSER_STATE->mkMutualDatatypeTypes(datatypes);
724 seq->addCommand(new DatatypeDeclarationCommand(datatypeTypes));
725 std::map<DatatypeType, Expr> evals;
726 if( sorts[0]!=range ){
727 PARSER_STATE->parseError(std::string("Bad return type in grammar for "
728 "SyGuS function ") + fun);
730 // make all the evals first, since they are mutually referential
731 for(size_t i = 0; i < datatypeTypes.size(); ++i) {
732 DatatypeType dtt = datatypeTypes[i];
733 const Datatype& dt = dtt.getDatatype();
734 Expr eval = dt.getSygusEvaluationFunc();
735 Debug("parser-sygus") << "Make eval " << eval << " for " << dt.getName()
737 evals.insert(std::make_pair(dtt, eval));
739 PARSER_STATE->addSygusFun(fun, eval);
742 // now go through and settle everything
743 for(size_t i = 0; i < datatypeTypes.size(); ++i) {
744 DatatypeType dtt = datatypeTypes[i];
745 const Datatype& dt = dtt.getDatatype();
746 Expr eval = evals[dtt];
747 Debug("parser-sygus") << "Sygus : process grammar : " << dt
749 for(size_t j = 0; j < dt.getNumConstructors(); ++j) {
750 Expr assertion = PARSER_STATE->getSygusAssertion(
751 datatypeTypes, ops, evals, terms, eval, dt, i, j );
752 seq->addCommand(new AssertCommand(assertion));
755 cmd->reset(seq.release());
759 PARSER_STATE->checkThatLogicIsSet();
760 Debug("parser-sygus") << "Sygus : define sygus funs..." << std::endl;
761 PARSER_STATE->defineSygusFuns();
762 Debug("parser-sygus") << "Sygus : read constraint..." << std::endl;
765 { Debug("parser-sygus") << "...read constraint " << expr << std::endl;
766 PARSER_STATE->addSygusConstraint(expr);
767 cmd->reset(new EmptyCommand());
769 | INV_CONSTRAINT_TOK {
770 PARSER_STATE->checkThatLogicIsSet();
771 Debug("parser-sygus") << "Sygus : define sygus funs..." << std::endl;
772 PARSER_STATE->defineSygusFuns();
773 Debug("parser-sygus") << "Sygus : read inv-constraint..." << std::endl;
775 ( symbol[name,CHECK_NONE,SYM_VARIABLE] {
776 if( !terms.empty() ){
777 if( !PARSER_STATE->isDefinedFunction(name) ){
778 std::stringstream ss;
779 ss << "Function " << name << " in inv-constraint is not defined.";
780 PARSER_STATE->parseError(ss.str());
783 terms.push_back( PARSER_STATE->getVariable(name) );
786 if( terms.size()!=4 ){
787 PARSER_STATE->parseError("Bad syntax for inv-constraint: expected 4 "
790 //get primed variables
791 std::vector< Expr > primed[2];
792 std::vector< Expr > all;
793 for( unsigned i=0; i<2; i++ ){
794 PARSER_STATE->getSygusPrimedVars( primed[i], i==1 );
795 all.insert( all.end(), primed[i].begin(), primed[i].end() );
797 //make relevant terms
798 for( unsigned i=0; i<4; i++ ){
799 Debug("parser-sygus") << "Make inv-constraint term #" << i << "..."
802 std::vector< Expr > children;
803 children.push_back( op );
805 children.insert( children.end(), all.begin(), all.end() );
807 children.insert( children.end(), primed[0].begin(), primed[0].end() );
809 terms[i] = EXPR_MANAGER->mkExpr(kind::APPLY,children);
811 std::vector< Expr > children2;
812 children2.push_back( op );
813 children2.insert(children2.end(), primed[1].begin(),
815 terms.push_back( EXPR_MANAGER->mkExpr(kind::APPLY,children2) );
819 std::vector< Expr > conj;
820 conj.push_back( EXPR_MANAGER->mkExpr(kind::IMPLIES, terms[1],
822 const Expr term0_and_2 = EXPR_MANAGER->mkExpr(kind::AND, terms[0],
824 conj.push_back( EXPR_MANAGER->mkExpr(kind::IMPLIES, term0_and_2,
826 conj.push_back( EXPR_MANAGER->mkExpr(kind::IMPLIES, terms[0], terms[3]) );
827 Expr ic = EXPR_MANAGER->mkExpr( kind::AND, conj );
828 Debug("parser-sygus") << "...read invariant constraint " << ic
830 PARSER_STATE->addSygusConstraint(ic);
831 cmd->reset(new EmptyCommand());
835 { PARSER_STATE->checkThatLogicIsSet(); PARSER_STATE->defineSygusFuns(); }
836 { Expr sygusVar = EXPR_MANAGER->mkVar("sygus", EXPR_MANAGER->booleanType());
837 Expr inst_attr =EXPR_MANAGER->mkExpr(kind::INST_ATTRIBUTE, sygusVar);
838 Expr sygusAttr = EXPR_MANAGER->mkExpr(kind::INST_PATTERN_LIST, inst_attr);
839 std::vector<Expr> bodyv;
840 Debug("parser-sygus") << "Sygus : Constructing sygus constraint..."
842 Expr body = EXPR_MANAGER->mkExpr(kind::NOT,
843 PARSER_STATE->getSygusConstraints());
844 Debug("parser-sygus") << "...constructed sygus constraint " << body
846 if( !PARSER_STATE->getSygusVars().empty() ){
847 Expr boundVars = EXPR_MANAGER->mkExpr(kind::BOUND_VAR_LIST,
848 PARSER_STATE->getSygusVars());
849 body = EXPR_MANAGER->mkExpr(kind::EXISTS, boundVars, body);
850 Debug("parser-sygus") << "...constructed exists " << body << std::endl;
852 if( !PARSER_STATE->getSygusFunSymbols().empty() ){
853 Expr boundVars = EXPR_MANAGER->mkExpr(
854 kind::BOUND_VAR_LIST, PARSER_STATE->getSygusFunSymbols());
855 body = EXPR_MANAGER->mkExpr(kind::FORALL, boundVars, body, sygusAttr);
857 Debug("parser-sygus") << "...constructed forall " << body << std::endl;
858 Command* c = new SetUserAttributeCommand("sygus", sygusVar);
860 PARSER_STATE->preemptCommand(c);
861 cmd->reset(new CheckSynthCommand(body));
864 // /* error handling */
865 // | (~(CHECK_SYNTH_TOK))=> token=.
866 // { std::string id = AntlrInput::tokenText($token);
867 // std::stringstream ss;
868 // ss << "Not a recognized SyGuS command: `" << id << "'";
869 // PARSER_STATE->parseError(ss.str());
873 // SyGuS grammar term.
875 // fun is the name of the synth-fun this grammar term is for.
876 // This method adds N operators to ops[index], N names to cnames[index] and N
877 // type argument vectors to cargs[index] (where typically N=1)
878 // This method may also add new elements pairwise into
879 // datatypes/sorts/ops/cnames/cargs in the case of non-flat gterms.
880 sygusGTerm[CVC4::SygusGTerm& sgt, std::string& fun]
882 std::string name, name2;
883 bool readEnum = false;
886 CVC4::DatatypeConstructor* ctor = NULL;
888 std::vector< Expr > let_vars;
889 bool readingLet = false;
895 Debug("parser-sygus") << "Sygus grammar " << fun << " : builtin op : "
896 << name << std::endl;
897 // Since we enforce satisfaction completeness, immediately convert to
899 if( k==CVC4::kind::BITVECTOR_UDIV ){
900 k = CVC4::kind::BITVECTOR_UDIV_TOTAL;
901 }else if( k==CVC4::kind::BITVECTOR_UREM ){
902 k = CVC4::kind::BITVECTOR_UREM_TOTAL;
904 sgt.d_name = kind::kindToString(k);
905 sgt.d_gterm_type = SygusGTerm::gterm_op;
906 sgt.d_expr = EXPR_MANAGER->operatorOf(k);
908 | LET_TOK LPAREN_TOK {
909 sgt.d_name = std::string("let");
910 sgt.d_gterm_type = SygusGTerm::gterm_let;
911 PARSER_STATE->pushScope(true);
915 symbol[sname,CHECK_NONE,SYM_VARIABLE]
916 sortSymbol[t,CHECK_DECLARED] {
917 Expr v = PARSER_STATE->mkBoundVar(sname,t);
918 sgt.d_let_vars.push_back( v );
921 sygusGTerm[sgt.d_children.back(), fun]
922 RPAREN_TOK )+ RPAREN_TOK
923 | SYGUS_CONSTANT_TOK sortSymbol[t,CHECK_DECLARED]
924 { sgt.d_gterm_type = SygusGTerm::gterm_constant;
926 Debug("parser-sygus") << "Sygus grammar constant." << std::endl;
928 | SYGUS_VARIABLE_TOK sortSymbol[t,CHECK_DECLARED]
929 { sgt.d_gterm_type = SygusGTerm::gterm_variable;
931 Debug("parser-sygus") << "Sygus grammar variable." << std::endl;
933 | SYGUS_LOCAL_VARIABLE_TOK sortSymbol[t,CHECK_DECLARED]
934 { sgt.d_gterm_type = SygusGTerm::gterm_local_variable;
936 Debug("parser-sygus") << "Sygus grammar local variable...ignore."
939 | SYGUS_INPUT_VARIABLE_TOK sortSymbol[t,CHECK_DECLARED]
940 { sgt.d_gterm_type = SygusGTerm::gterm_input_variable;
942 Debug("parser-sygus") << "Sygus grammar (input) variable."
945 | symbol[name,CHECK_NONE,SYM_VARIABLE] {
946 bool isBuiltinOperator = PARSER_STATE->isOperatorEnabled(name);
947 if(isBuiltinOperator) {
948 Debug("parser-sygus") << "Sygus grammar " << fun << " : builtin op : "
949 << name << std::endl;
950 k = PARSER_STATE->getOperatorKind(name);
951 if( k==CVC4::kind::BITVECTOR_UDIV ){
952 k = CVC4::kind::BITVECTOR_UDIV_TOTAL;
953 }else if( k==CVC4::kind::BITVECTOR_UREM ){
954 k = CVC4::kind::BITVECTOR_UREM_TOTAL;
956 sgt.d_name = kind::kindToString(k);
957 sgt.d_gterm_type = SygusGTerm::gterm_op;
958 sgt.d_expr = EXPR_MANAGER->operatorOf(k);
960 // what is this sygus term trying to accomplish here, if the
961 // symbol isn't yet declared?! probably the following line will
962 // fail, but we need an operator to continue here..
963 Debug("parser-sygus")
964 << "Sygus grammar " << fun << " : op (declare="
965 << PARSER_STATE->isDeclared(name) << ", define="
966 << PARSER_STATE->isDefinedFunction(name) << ") : " << name
968 if(!PARSER_STATE->isDeclared(name) &&
969 !PARSER_STATE->isDefinedFunction(name) ){
970 PARSER_STATE->parseError("Functions in sygus grammars must be "
974 sgt.d_gterm_type = SygusGTerm::gterm_op;
975 sgt.d_expr = PARSER_STATE->getVariable(name) ;
980 { Debug("parser-sygus") << "Read arguments under " << sgt.d_name
984 ( sygusGTerm[sgt.d_children.back(), fun]
985 { Debug("parser-sygus") << "Finished read argument #"
986 << sgt.d_children.size() << "..." << std::endl;
991 //pop last child index
992 sgt.d_children.pop_back();
994 PARSER_STATE->popScope();
998 { Debug("parser-sygus") << "Sygus grammar " << fun << " : integer literal "
999 << AntlrInput::tokenText($INTEGER_LITERAL)
1001 sgt.d_expr = MK_CONST(Rational(AntlrInput::tokenText($INTEGER_LITERAL)));
1002 sgt.d_name = AntlrInput::tokenText($INTEGER_LITERAL);
1003 sgt.d_gterm_type = SygusGTerm::gterm_op;
1006 { Debug("parser-sygus") << "Sygus grammar " << fun << " : hex literal "
1007 << AntlrInput::tokenText($HEX_LITERAL) << std::endl;
1008 assert( AntlrInput::tokenText($HEX_LITERAL).find("#x") == 0 );
1009 std::string hexString = AntlrInput::tokenTextSubstr($HEX_LITERAL, 2);
1010 sgt.d_expr = MK_CONST( BitVector(hexString, 16) );
1011 sgt.d_name = AntlrInput::tokenText($HEX_LITERAL);
1012 sgt.d_gterm_type = SygusGTerm::gterm_op;
1015 { Debug("parser-sygus") << "Sygus grammar " << fun << " : binary literal "
1016 << AntlrInput::tokenText($BINARY_LITERAL)
1018 assert( AntlrInput::tokenText($BINARY_LITERAL).find("#b") == 0 );
1019 std::string binString = AntlrInput::tokenTextSubstr($BINARY_LITERAL, 2);
1020 sgt.d_expr = MK_CONST( BitVector(binString, 2) );
1021 sgt.d_name = AntlrInput::tokenText($BINARY_LITERAL);
1022 sgt.d_gterm_type = SygusGTerm::gterm_op;
1025 { Debug("parser-sygus") << "Sygus grammar " << fun << " : string literal \""
1026 << s << "\"" << std::endl;
1027 sgt.d_expr = MK_CONST( ::CVC4::String(s) );
1029 sgt.d_gterm_type = SygusGTerm::gterm_op;
1031 | symbol[name,CHECK_NONE,SYM_VARIABLE]
1032 ( SYGUS_ENUM_CONS_TOK symbol[name2,CHECK_NONE,SYM_VARIABLE]
1033 { readEnum = true; }
1036 name = name + "__Enum__" + name2;
1037 Debug("parser-sygus") << "Sygus grammar " << fun << " : Enum constant "
1038 << name << std::endl;
1039 Expr c = PARSER_STATE->getVariable(name);
1040 sgt.d_expr = MK_EXPR(kind::APPLY_CONSTRUCTOR,c);
1042 sgt.d_gterm_type = SygusGTerm::gterm_op;
1044 if( name[0] == '-' ){ //hack for unary minus
1045 Debug("parser-sygus") << "Sygus grammar " << fun
1046 << " : unary minus integer literal " << name
1048 sgt.d_expr = MK_CONST(Rational(name));
1050 sgt.d_gterm_type = SygusGTerm::gterm_op;
1051 }else if( PARSER_STATE->isDeclared(name,SYM_VARIABLE) ){
1052 Debug("parser-sygus") << "Sygus grammar " << fun << " : symbol "
1053 << name << std::endl;
1054 sgt.d_expr = PARSER_STATE->getVariable(name);
1056 sgt.d_gterm_type = SygusGTerm::gterm_op;
1058 //prepend function name to base sorts when reading an operator
1059 std::stringstream ss;
1060 ss << fun << "_" << name;
1062 if( PARSER_STATE->isDeclared(name, SYM_SORT) ){
1063 Debug("parser-sygus") << "Sygus grammar " << fun
1064 << " : nested sort " << name << std::endl;
1065 sgt.d_type = PARSER_STATE->getSort(name);
1066 sgt.d_gterm_type = SygusGTerm::gterm_nested_sort;
1068 Debug("parser-sygus") << "Sygus grammar " << fun
1069 << " : unresolved symbol " << name
1071 sgt.d_gterm_type = SygusGTerm::gterm_unresolved;
1079 // Separate this into its own rule (can be invoked by set-info or meta-info)
1080 metaInfoInternal[CVC4::PtrCloser<CVC4::Command>* cmd]
1085 : KEYWORD symbolicExpr[sexpr]
1086 { name = AntlrInput::tokenText($KEYWORD);
1087 if(name == ":cvc4-logic" || name == ":cvc4_logic") {
1088 PARSER_STATE->setLogic(sexpr.getValue());
1089 } else if(name == ":smt-lib-version") {
1090 // if we don't recognize the revision name, just keep the current mode
1091 if( (sexpr.isRational() && sexpr.getRationalValue() == Rational(2)) ||
1092 sexpr.getValue() == "2" ||
1093 sexpr.getValue() == "2.0" ) {
1094 PARSER_STATE->setLanguage(language::input::LANG_SMTLIB_V2_0);
1095 } else if( (sexpr.isRational() &&
1096 sexpr.getRationalValue() == Rational(5, 2)) ||
1097 sexpr.getValue() == "2.5" ) {
1098 PARSER_STATE->setLanguage(language::input::LANG_SMTLIB_V2_5);
1099 } else if( (sexpr.isRational() &&
1100 sexpr.getRationalValue() == Rational(13, 5)) ||
1101 sexpr.getValue() == "2.6" ) {
1102 PARSER_STATE->setLanguage(language::input::LANG_SMTLIB_V2_6);
1105 PARSER_STATE->setInfo(name.c_str() + 1, sexpr);
1106 cmd->reset(new SetInfoCommand(name.c_str() + 1, sexpr));
1110 setOptionInternal[CVC4::PtrCloser<CVC4::Command>* cmd]
1115 : keyword[name] symbolicExpr[sexpr]
1116 { PARSER_STATE->setOption(name.c_str() + 1, sexpr);
1117 cmd->reset(new SetOptionCommand(name.c_str() + 1, sexpr));
1118 // Ugly that this changes the state of the parser; but
1119 // global-declarations affects parsing, so we can't hold off
1120 // on this until some SmtEngine eventually (if ever) executes it.
1121 if(name == ":global-declarations") {
1122 PARSER_STATE->setGlobalDeclarations(sexpr.getValue() == "true");
1127 smt25Command[CVC4::PtrCloser<CVC4::Command>* cmd]
1132 std::vector<std::pair<std::string, Type> > sortedVarNames;
1136 std::vector<Expr> bvs;
1137 std::vector< std::vector<std::pair<std::string, Type> > > sortedVarNamesList;
1138 std::vector<Expr> funcs;
1139 std::vector<Expr> func_defs;
1141 CVC4::PtrCloser<CVC4::CommandSequence> seq;
1144 : META_INFO_TOK metaInfoInternal[cmd]
1147 | DECLARE_CONST_TOK { PARSER_STATE->checkThatLogicIsSet(); }
1148 symbol[name,CHECK_UNDECLARED,SYM_VARIABLE]
1149 { PARSER_STATE->checkUserSymbol(name); }
1150 sortSymbol[t,CHECK_DECLARED]
1151 { Expr c = PARSER_STATE->mkVar(name, t);
1152 cmd->reset(new DeclareFunctionCommand(name, c, t)); }
1155 | GET_MODEL_TOK { PARSER_STATE->checkThatLogicIsSet(); }
1156 { cmd->reset(new GetModelCommand()); }
1160 ( simpleSymbolicExpr[sexpr]
1161 { cmd->reset(new EchoCommand(sexpr.toString())); }
1162 | { cmd->reset(new EchoCommand()); }
1165 /* reset: reset everything, returning solver to initial state.
1166 * Logic and options must be set again. */
1168 { cmd->reset(new ResetCommand());
1169 PARSER_STATE->reset();
1171 /* reset-assertions: reset assertions, assertion stack, declarations,
1172 * etc., but the logic and options remain as they were. */
1173 | RESET_ASSERTIONS_TOK
1174 { cmd->reset(new ResetAssertionsCommand());
1175 PARSER_STATE->resetAssertions();
1177 | DEFINE_FUN_REC_TOK
1178 { PARSER_STATE->checkThatLogicIsSet();
1179 seq.reset(new CVC4::CommandSequence());
1181 symbol[fname,CHECK_UNDECLARED,SYM_VARIABLE]
1182 { PARSER_STATE->checkUserSymbol(fname); }
1183 LPAREN_TOK sortedVarList[sortedVarNames] RPAREN_TOK
1184 sortSymbol[t,CHECK_DECLARED]
1185 { if( sortedVarNames.size() > 0 ) {
1186 std::vector<CVC4::Type> sorts;
1187 sorts.reserve(sortedVarNames.size());
1188 for(std::vector<std::pair<std::string, CVC4::Type> >::const_iterator i =
1189 sortedVarNames.begin(), iend = sortedVarNames.end(); i != iend;
1191 sorts.push_back((*i).second);
1193 t = EXPR_MANAGER->mkFunctionType(sorts, t);
1195 Expr func = PARSER_STATE->mkVar(fname, t);
1196 seq->addCommand(new DeclareFunctionCommand(fname, func, t));
1197 if( sortedVarNames.empty() ){
1200 std::vector< Expr > f_app;
1201 f_app.push_back( func );
1202 PARSER_STATE->pushScope(true);
1203 for(std::vector<std::pair<std::string, CVC4::Type> >::const_iterator i =
1204 sortedVarNames.begin(), iend = sortedVarNames.end(); i != iend;
1206 Expr v = PARSER_STATE->mkBoundVar((*i).first, (*i).second);
1208 f_app.push_back( v );
1210 func_app = MK_EXPR( kind::APPLY_UF, f_app );
1214 { PARSER_STATE->popScope();
1215 Expr as = MK_EXPR( kind::EQUAL, func_app, expr);
1217 std::string attr_name("fun-def");
1218 aexpr = MK_EXPR(kind::INST_ATTRIBUTE, func_app);
1219 aexpr = MK_EXPR(kind::INST_PATTERN_LIST, aexpr);
1220 //set the attribute to denote this is a function definition
1221 seq->addCommand( new SetUserAttributeCommand( attr_name, func_app ) );
1223 Expr boundVars = EXPR_MANAGER->mkExpr(kind::BOUND_VAR_LIST, bvs);
1224 as = EXPR_MANAGER->mkExpr(kind::FORALL, boundVars, as, aexpr);
1226 seq->addCommand( new AssertCommand(as, false) );
1227 cmd->reset(seq.release());
1229 | DEFINE_FUNS_REC_TOK
1230 { PARSER_STATE->checkThatLogicIsSet();
1231 seq.reset(new CVC4::CommandSequence());
1235 symbol[fname,CHECK_UNDECLARED,SYM_VARIABLE]
1236 { PARSER_STATE->checkUserSymbol(fname); }
1237 LPAREN_TOK sortedVarList[sortedVarNames] RPAREN_TOK
1238 sortSymbol[t,CHECK_DECLARED]
1239 { sortedVarNamesList.push_back( sortedVarNames );
1240 if( sortedVarNamesList[0].size() > 0 ) {
1241 if( !sortedVarNames.empty() ){
1242 std::vector<CVC4::Type> sorts;
1243 for(std::vector<std::pair<std::string, CVC4::Type> >::const_iterator
1244 i = sortedVarNames.begin(), iend = sortedVarNames.end();
1246 sorts.push_back((*i).second);
1248 t = EXPR_MANAGER->mkFunctionType(sorts, t);
1251 sortedVarNames.clear();
1252 Expr func = PARSER_STATE->mkVar(fname, t);
1253 seq->addCommand(new DeclareFunctionCommand(fname, func, t));
1254 funcs.push_back( func );
1261 //set up the first scope
1262 if( sortedVarNamesList.empty() ){
1263 PARSER_STATE->parseError("Must define at least one function in "
1266 PARSER_STATE->pushScope(true);
1268 if( sortedVarNamesList[0].empty() ){
1269 func_app = funcs[0];
1271 std::vector< Expr > f_app;
1272 f_app.push_back( funcs[0] );
1273 for(std::vector<std::pair<std::string, CVC4::Type> >::const_iterator
1274 i = sortedVarNamesList[0].begin(),
1275 iend = sortedVarNamesList[0].end(); i != iend; ++i) {
1276 Expr v = PARSER_STATE->mkBoundVar((*i).first, (*i).second);
1278 f_app.push_back( v );
1280 func_app = MK_EXPR( kind::APPLY_UF, f_app );
1286 func_defs.push_back( expr );
1287 Expr as = MK_EXPR( kind::EQUAL, func_app, expr );
1289 std::string attr_name("fun-def");
1290 aexpr = MK_EXPR(kind::INST_ATTRIBUTE, func_app);
1291 aexpr = MK_EXPR(kind::INST_PATTERN_LIST, aexpr );
1292 //set the attribute to denote these are function definitions
1293 seq->addCommand( new SetUserAttributeCommand( attr_name, func_app ) );
1295 as = EXPR_MANAGER->mkExpr( kind::FORALL,
1296 EXPR_MANAGER->mkExpr(kind::BOUND_VAR_LIST, bvs),
1299 seq->addCommand( new AssertCommand(as, false) );
1300 //set up the next scope
1301 PARSER_STATE->popScope();
1302 if( func_defs.size()<funcs.size() ){
1303 PARSER_STATE->pushScope(true);
1305 unsigned j = func_defs.size();
1306 if( sortedVarNamesList[j].empty() ){
1307 func_app = funcs[j];
1309 std::vector< Expr > f_app;
1310 f_app.push_back( funcs[j] );
1311 for(std::vector<std::pair<std::string, CVC4::Type> >::const_iterator
1312 i = sortedVarNamesList[j].begin(),
1313 iend = sortedVarNamesList[j].end(); i != iend; ++i) {
1314 Expr v = PARSER_STATE->mkBoundVar((*i).first, (*i).second);
1316 f_app.push_back( v );
1318 func_app = MK_EXPR( kind::APPLY_UF, f_app );
1324 { if( funcs.size()!=func_defs.size() ){
1325 PARSER_STATE->parseError(std::string(
1326 "Number of functions defined does not match number listed in "
1327 "define-funs-rec"));
1329 cmd->reset(seq.release());
1331 // CHECK_SAT_ASSUMING still being discussed
1332 // GET_UNSAT_ASSUMPTIONS
1335 extendedCommand[CVC4::PtrCloser<CVC4::Command>* cmd]
1337 std::vector<CVC4::Datatype> dts;
1341 std::vector<std::string> names;
1342 std::vector<Expr> terms;
1343 std::vector<Type> sorts;
1344 std::vector<std::pair<std::string, Type> > sortedVarNames;
1345 CVC4::PtrCloser<CVC4::CommandSequence> seq;
1347 /* Extended SMT-LIB set of commands syntax, not permitted in
1348 * --smtlib2 compliance mode. */
1349 : DECLARE_DATATYPES_2_5_TOK datatypes_2_5_DefCommand[false, cmd]
1350 | DECLARE_CODATATYPES_2_5_TOK datatypes_2_5_DefCommand[true, cmd]
1351 | DECLARE_DATATYPE_TOK datatypeDefCommand[false, cmd]
1352 | DECLARE_CODATATYPE_TOK datatypeDefCommand[true, cmd]
1353 | DECLARE_DATATYPES_TOK datatypesDefCommand[false, cmd]
1354 | DECLARE_CODATATYPES_TOK datatypesDefCommand[true, cmd]
1355 | rewriterulesCommand[cmd]
1357 /* Support some of Z3's extended SMT-LIB commands */
1359 | DECLARE_SORTS_TOK { PARSER_STATE->checkThatLogicIsSet(); }
1360 { if(!PARSER_STATE->isTheoryEnabled(Smt2::THEORY_UF) &&
1361 !PARSER_STATE->isTheoryEnabled(Smt2::THEORY_ARRAYS) &&
1362 !PARSER_STATE->isTheoryEnabled(Smt2::THEORY_DATATYPES) &&
1363 !PARSER_STATE->isTheoryEnabled(Smt2::THEORY_SETS)) {
1364 PARSER_STATE->parseErrorLogic("Free sort symbols not allowed in ");
1367 { seq.reset(new CVC4::CommandSequence()); }
1369 ( symbol[name,CHECK_UNDECLARED,SYM_SORT]
1370 { PARSER_STATE->checkUserSymbol(name);
1371 Type type = PARSER_STATE->mkSort(name);
1372 seq->addCommand(new DeclareTypeCommand(name, 0, type));
1376 { cmd->reset(seq.release()); }
1378 | DECLARE_FUNS_TOK { PARSER_STATE->checkThatLogicIsSet(); }
1379 { seq.reset(new CVC4::CommandSequence()); }
1381 ( LPAREN_TOK symbol[name,CHECK_UNDECLARED,SYM_VARIABLE]
1382 { PARSER_STATE->checkUserSymbol(name); }
1383 nonemptySortList[sorts] RPAREN_TOK
1385 if(sorts.size() > 1) {
1386 if(!PARSER_STATE->isTheoryEnabled(Smt2::THEORY_UF)) {
1387 PARSER_STATE->parseErrorLogic("Functions (of non-zero arity) "
1388 "cannot be declared in logic ");
1390 t = EXPR_MANAGER->mkFunctionType(sorts);
1394 Expr func = PARSER_STATE->mkVar(name, t);
1395 seq->addCommand(new DeclareFunctionCommand(name, func, t));
1400 { cmd->reset(seq.release()); }
1401 | DECLARE_PREDS_TOK { PARSER_STATE->checkThatLogicIsSet(); }
1402 { seq.reset(new CVC4::CommandSequence()); }
1404 ( LPAREN_TOK symbol[name,CHECK_UNDECLARED,SYM_VARIABLE]
1405 { PARSER_STATE->checkUserSymbol(name); }
1406 sortList[sorts] RPAREN_TOK
1407 { Type t = EXPR_MANAGER->booleanType();
1408 if(sorts.size() > 0) {
1409 if(!PARSER_STATE->isTheoryEnabled(Smt2::THEORY_UF)) {
1410 PARSER_STATE->parseErrorLogic("Predicates (of non-zero arity) "
1411 "cannot be declared in logic ");
1413 t = EXPR_MANAGER->mkFunctionType(sorts, t);
1415 Expr func = PARSER_STATE->mkVar(name, t);
1416 seq->addCommand(new DeclareFunctionCommand(name, func, t));
1421 { cmd->reset(seq.release()); }
1423 | DEFINE_TOK { PARSER_STATE->checkThatLogicIsSet(); }
1424 ( symbol[name,CHECK_UNDECLARED,SYM_VARIABLE]
1425 { PARSER_STATE->checkUserSymbol(name); }
1427 { Expr func = PARSER_STATE->mkFunction(name, e.getType(),
1428 ExprManager::VAR_FLAG_DEFINED);
1429 cmd->reset(new DefineFunctionCommand(name, func, e));
1432 symbol[name,CHECK_UNDECLARED,SYM_VARIABLE]
1433 { PARSER_STATE->checkUserSymbol(name); }
1434 sortedVarList[sortedVarNames] RPAREN_TOK
1435 { /* add variables to parser state before parsing term */
1436 Debug("parser") << "define fun: '" << name << "'" << std::endl;
1437 PARSER_STATE->pushScope(true);
1438 for(std::vector<std::pair<std::string, CVC4::Type> >::const_iterator i =
1439 sortedVarNames.begin(), iend = sortedVarNames.end(); i != iend;
1441 terms.push_back(PARSER_STATE->mkBoundVar((*i).first, (*i).second));
1445 { PARSER_STATE->popScope();
1446 // declare the name down here (while parsing term, signature
1447 // must not be extended with the name itself; no recursion
1449 Type t = e.getType();
1450 if( sortedVarNames.size() > 0 ) {
1451 std::vector<CVC4::Type> sorts;
1452 sorts.reserve(sortedVarNames.size());
1453 for(std::vector<std::pair<std::string, CVC4::Type> >::const_iterator
1454 i = sortedVarNames.begin(), iend = sortedVarNames.end();
1456 sorts.push_back((*i).second);
1458 t = EXPR_MANAGER->mkFunctionType(sorts, t);
1460 Expr func = PARSER_STATE->mkFunction(name, t,
1461 ExprManager::VAR_FLAG_DEFINED);
1462 cmd->reset(new DefineFunctionCommand(name, func, terms, e));
1465 | DEFINE_CONST_TOK { PARSER_STATE->checkThatLogicIsSet(); }
1466 symbol[name,CHECK_UNDECLARED,SYM_VARIABLE]
1467 { PARSER_STATE->checkUserSymbol(name); }
1468 sortSymbol[t,CHECK_DECLARED]
1469 { /* add variables to parser state before parsing term */
1470 Debug("parser") << "define const: '" << name << "'" << std::endl;
1471 PARSER_STATE->pushScope(true);
1472 for(std::vector<std::pair<std::string, CVC4::Type> >::const_iterator i =
1473 sortedVarNames.begin(), iend = sortedVarNames.end(); i != iend;
1475 terms.push_back(PARSER_STATE->mkBoundVar((*i).first, (*i).second));
1479 { PARSER_STATE->popScope();
1480 // declare the name down here (while parsing term, signature
1481 // must not be extended with the name itself; no recursion
1483 Expr func = PARSER_STATE->mkFunction(name, t,
1484 ExprManager::VAR_FLAG_DEFINED);
1485 cmd->reset(new DefineFunctionCommand(name, func, terms, e));
1488 | SIMPLIFY_TOK { PARSER_STATE->checkThatLogicIsSet(); }
1490 { cmd->reset(new SimplifyCommand(e)); }
1491 | GET_QE_TOK { PARSER_STATE->checkThatLogicIsSet(); }
1493 { cmd->reset(new GetQuantifierEliminationCommand(e, true)); }
1494 | GET_QE_DISJUNCT_TOK { PARSER_STATE->checkThatLogicIsSet(); }
1496 { cmd->reset(new GetQuantifierEliminationCommand(e, false)); }
1500 datatypes_2_5_DefCommand[bool isCo, CVC4::PtrCloser<CVC4::Command>* cmd]
1502 std::vector<CVC4::Datatype> dts;
1504 std::vector<Type> sorts;
1506 : { PARSER_STATE->checkThatLogicIsSet();
1507 /* open a scope to keep the UnresolvedTypes contained */
1508 PARSER_STATE->pushScope(true); }
1509 LPAREN_TOK /* parametric sorts */
1510 ( symbol[name,CHECK_UNDECLARED,SYM_SORT]
1511 { sorts.push_back( PARSER_STATE->mkSort(name) ); }
1514 LPAREN_TOK ( LPAREN_TOK datatypeDef[isCo, dts, sorts] RPAREN_TOK )+ RPAREN_TOK
1515 { PARSER_STATE->popScope();
1516 cmd->reset(new DatatypeDeclarationCommand(PARSER_STATE->mkMutualDatatypeTypes(dts)));
1520 datatypeDefCommand[bool isCo, CVC4::PtrCloser<CVC4::Command>* cmd]
1522 std::vector<CVC4::Datatype> dts;
1525 : { PARSER_STATE->checkThatLogicIsSet(); }
1526 symbol[name,CHECK_UNDECLARED,SYM_SORT] LPAREN_TOK
1527 { std::vector<Type> params;
1528 dts.push_back(Datatype(name,params,isCo));
1530 ( LPAREN_TOK constructorDef[dts.back()] RPAREN_TOK )+
1532 { cmd->reset(new DatatypeDeclarationCommand(PARSER_STATE->mkMutualDatatypeTypes(dts))); }
1535 datatypesDefCommand[bool isCo, CVC4::PtrCloser<CVC4::Command>* cmd]
1537 std::vector<CVC4::Datatype> dts;
1539 std::vector<std::string> dnames;
1540 std::vector<unsigned> arities;
1541 std::vector<Type> params;
1543 : { PARSER_STATE->checkThatLogicIsSet(); PARSER_STATE->pushScope(true); }
1544 LPAREN_TOK /* sorts */
1545 ( LPAREN_TOK symbol[name,CHECK_UNDECLARED,SYM_SORT] n=INTEGER_LITERAL RPAREN_TOK
1546 { unsigned arity = AntlrInput::tokenToUnsigned(n);
1549 // type = PARSER_STATE->mkSort(name);
1551 // type = PARSER_STATE->mkSortConstructor(name, arity);
1553 //types.push_back(type);
1554 Debug("parser-dt") << "Datatype : " << name << ", arity = " << arity << std::endl;
1555 dnames.push_back(name);
1556 arities.push_back( arity );
1563 Debug("parser-dt") << "Processing datatype #" << dts.size() << std::endl;
1564 if( dts.size()>=dnames.size() ){
1565 PARSER_STATE->parseError("Too many datatypes defined in this block.");
1568 ( PAR_TOK { PARSER_STATE->pushScope(true); } LPAREN_TOK
1569 ( symbol[name,CHECK_UNDECLARED,SYM_SORT]
1570 { params.push_back( PARSER_STATE->mkSort(name) ); }
1573 if( params.size()!=arities[dts.size()] ){
1574 PARSER_STATE->parseError("Wrong number of parameters for datatype.");
1576 Debug("parser-dt") << params.size() << " parameters for " << dnames[dts.size()] << std::endl;
1577 dts.push_back(Datatype(dnames[dts.size()],params,isCo));
1580 ( LPAREN_TOK constructorDef[dts.back()] RPAREN_TOK )+
1581 RPAREN_TOK { PARSER_STATE->popScope(); }
1582 | { if( 0!=arities[dts.size()] ){
1583 PARSER_STATE->parseError("No parameters given for datatype.");
1585 Debug("parser-dt") << params.size() << " parameters for " << dnames[dts.size()] << std::endl;
1586 dts.push_back(Datatype(dnames[dts.size()],params,isCo));
1588 ( LPAREN_TOK constructorDef[dts.back()] RPAREN_TOK )+
1593 { PARSER_STATE->popScope();
1594 cmd->reset(new DatatypeDeclarationCommand(PARSER_STATE->mkMutualDatatypeTypes(dts)));
1598 rewriterulesCommand[CVC4::PtrCloser<CVC4::Command>* cmd]
1600 std::vector<std::pair<std::string, Type> > sortedVarNames;
1601 std::vector<Expr> args, guards, heads, triggers;
1602 Expr head, body, expr, expr2, bvl;
1605 : /* rewrite rules */
1607 LPAREN_TOK sortedVarList[sortedVarNames] RPAREN_TOK
1609 kind = CVC4::kind::RR_REWRITE;
1610 PARSER_STATE->pushScope(true);
1611 for(std::vector<std::pair<std::string, CVC4::Type> >::const_iterator i =
1612 sortedVarNames.begin(), iend = sortedVarNames.end();
1615 args.push_back(PARSER_STATE->mkBoundVar((*i).first, (*i).second));
1617 bvl = MK_EXPR(kind::BOUND_VAR_LIST, args);
1619 LPAREN_TOK ( pattern[expr] { triggers.push_back( expr ); } )* RPAREN_TOK
1620 LPAREN_TOK (termList[guards,expr])? RPAREN_TOK
1621 term[head, expr2] term[body, expr2]
1624 args.push_back(head);
1625 args.push_back(body);
1627 if( !triggers.empty() ){
1628 expr2 = MK_EXPR(kind::INST_PATTERN_LIST, triggers);
1629 args.push_back(expr2);
1631 expr = MK_EXPR(kind, args);
1633 args.push_back(bvl);
1635 switch( guards.size() ){
1637 args.push_back(MK_CONST(bool(true))); break;
1639 args.push_back(guards[0]); break;
1641 expr2 = MK_EXPR(kind::AND, guards);
1642 args.push_back(expr2); break;
1644 args.push_back(expr);
1645 expr = MK_EXPR(CVC4::kind::REWRITE_RULE, args);
1646 cmd->reset(new AssertCommand(expr, false)); }
1647 /* propagation rule */
1648 | rewritePropaKind[kind]
1649 LPAREN_TOK sortedVarList[sortedVarNames] RPAREN_TOK
1651 PARSER_STATE->pushScope(true);
1652 for(std::vector<std::pair<std::string, CVC4::Type> >::const_iterator i =
1653 sortedVarNames.begin(), iend = sortedVarNames.end();
1656 args.push_back(PARSER_STATE->mkBoundVar((*i).first, (*i).second));
1658 bvl = MK_EXPR(kind::BOUND_VAR_LIST, args);
1660 LPAREN_TOK ( pattern[expr] { triggers.push_back( expr ); } )* RPAREN_TOK
1661 LPAREN_TOK (termList[guards,expr])? RPAREN_TOK
1662 LPAREN_TOK (termList[heads,expr])? RPAREN_TOK
1667 switch( heads.size() ){
1669 args.push_back(MK_CONST(bool(true))); break;
1671 args.push_back(heads[0]); break;
1673 expr2 = MK_EXPR(kind::AND, heads);
1674 args.push_back(expr2); break;
1676 args.push_back(body);
1678 if( !triggers.empty() ){
1679 expr2 = MK_EXPR(kind::INST_PATTERN_LIST, triggers);
1680 args.push_back(expr2);
1682 expr = MK_EXPR(kind, args);
1684 args.push_back(bvl);
1686 switch( guards.size() ){
1688 args.push_back(MK_CONST(bool(true))); break;
1690 args.push_back(guards[0]); break;
1692 expr2 = MK_EXPR(kind::AND, guards);
1693 args.push_back(expr2); break;
1695 args.push_back(expr);
1696 expr = MK_EXPR(CVC4::kind::REWRITE_RULE, args);
1697 cmd->reset(new AssertCommand(expr, false));
1701 rewritePropaKind[CVC4::Kind& kind]
1702 : REDUCTION_RULE_TOK { $kind = CVC4::kind::RR_REDUCTION; }
1703 | PROPAGATION_RULE_TOK { $kind = CVC4::kind::RR_DEDUCTION; }
1706 pattern[CVC4::Expr& expr]
1708 std::vector<Expr> patexpr;
1710 : LPAREN_TOK termList[patexpr,expr] RPAREN_TOK
1712 expr = MK_EXPR(kind::INST_PATTERN, patexpr);
1716 simpleSymbolicExprNoKeyword[CVC4::SExpr& sexpr]
1720 std::vector<unsigned int> s_vec;
1723 { sexpr = SExpr(Integer(AntlrInput::tokenText($INTEGER_LITERAL))); }
1725 { sexpr = SExpr(AntlrInput::tokenToRational($DECIMAL_LITERAL)); }
1727 { assert( AntlrInput::tokenText($HEX_LITERAL).find("#x") == 0 );
1728 std::string hexString = AntlrInput::tokenTextSubstr($HEX_LITERAL, 2);
1729 sexpr = SExpr(Integer(hexString, 16));
1732 { assert( AntlrInput::tokenText($BINARY_LITERAL).find("#b") == 0 );
1733 std::string binString = AntlrInput::tokenTextSubstr($BINARY_LITERAL, 2);
1734 sexpr = SExpr(Integer(binString, 2));
1737 { sexpr = SExpr(s); }
1738 // | LPAREN_TOK STRCST_TOK
1739 // ( INTEGER_LITERAL {
1740 // s_vec.push_back( atoi( AntlrInput::tokenText($INTEGER_LITERAL) ) + 65 );
1743 // sexpr = SExpr( MK_CONST( ::CVC4::String(s_vec) ) );
1745 | symbol[s,CHECK_NONE,SYM_SORT]
1746 { sexpr = SExpr(SExpr::Keyword(s)); }
1747 | tok=(ASSERT_TOK | CHECKSAT_TOK | DECLARE_FUN_TOK | DECLARE_SORT_TOK
1748 | DEFINE_FUN_TOK | DEFINE_FUN_REC_TOK | DEFINE_FUNS_REC_TOK
1749 | DEFINE_SORT_TOK | GET_VALUE_TOK | GET_ASSIGNMENT_TOK
1750 | GET_ASSERTIONS_TOK | GET_PROOF_TOK | GET_UNSAT_CORE_TOK | EXIT_TOK
1751 | RESET_TOK | RESET_ASSERTIONS_TOK | SET_LOGIC_TOK | SET_INFO_TOK
1752 | GET_INFO_TOK | SET_OPTION_TOK | GET_OPTION_TOK | PUSH_TOK | POP_TOK
1753 | DECLARE_DATATYPES_TOK | GET_MODEL_TOK | ECHO_TOK | REWRITE_RULE_TOK
1754 | REDUCTION_RULE_TOK | PROPAGATION_RULE_TOK | SIMPLIFY_TOK)
1755 { sexpr = SExpr(SExpr::Keyword(AntlrInput::tokenText($tok))); }
1757 { std::stringstream ss;
1758 ss << language::SetLanguage(CVC4::language::output::LANG_SMTLIB_V2_5)
1759 << EXPR_MANAGER->mkConst(k);
1760 sexpr = SExpr(ss.str());
1764 keyword[std::string& s]
1766 { s = AntlrInput::tokenText($KEYWORD); }
1769 simpleSymbolicExpr[CVC4::SExpr& sexpr]
1770 : simpleSymbolicExprNoKeyword[sexpr]
1772 { sexpr = SExpr(AntlrInput::tokenText($KEYWORD)); }
1775 symbolicExpr[CVC4::SExpr& sexpr]
1777 std::vector<SExpr> children;
1779 : simpleSymbolicExpr[sexpr]
1781 ( symbolicExpr[sexpr] { children.push_back(sexpr); } )* RPAREN_TOK
1782 { sexpr = SExpr(children); }
1787 * @return the expression representing the formula
1789 term[CVC4::Expr& expr, CVC4::Expr& expr2]
1791 Debug("parser") << "term: " << AntlrInput::tokenText(LT(1)) << std::endl;
1792 Kind kind = kind::NULL_EXPR;
1794 std::string name, name2;
1795 std::vector<Expr> args;
1796 std::vector< std::pair<std::string, Type> > sortedVarNames;
1800 std::vector<Expr> patexprs;
1801 std::vector<Expr> patconds;
1802 std::hash_set<std::string, StringHashFunction> names;
1803 std::vector< std::pair<std::string, Expr> > binders;
1806 bool isBuiltinOperator = false;
1807 bool readLetSort = false;
1808 int match_vindex = -1;
1809 std::vector<Type> match_ptypes;
1811 : /* a built-in operator application */
1812 LPAREN_TOK builtinOp[kind] termList[args,expr] RPAREN_TOK
1814 if( !PARSER_STATE->strictModeEnabled() &&
1815 (kind == CVC4::kind::AND || kind == CVC4::kind::OR) &&
1817 /* Unary AND/OR can be replaced with the argument.
1818 * It just so happens expr should already be the only argument. */
1819 assert( expr == args[0] );
1820 } else if( CVC4::kind::isAssociative(kind) &&
1821 args.size() > EXPR_MANAGER->maxArity(kind) ) {
1822 /* Special treatment for associative operators with lots of children */
1823 expr = EXPR_MANAGER->mkAssociative(kind, args);
1824 } else if( kind == CVC4::kind::MINUS && args.size() == 1 ) {
1825 expr = MK_EXPR(CVC4::kind::UMINUS, args[0]);
1826 } else if( ( kind == CVC4::kind::XOR || kind == CVC4::kind::MINUS ) &&
1828 /* left-associative, but CVC4 internally only supports 2 args */
1830 for(size_t i = 1; i < args.size(); ++i) {
1831 expr = MK_EXPR(kind, expr, args[i]);
1833 } else if( kind == CVC4::kind::IMPLIES && args.size() > 2 ) {
1834 /* right-associative, but CVC4 internally only supports 2 args */
1835 expr = args[args.size() - 1];
1836 for(size_t i = args.size() - 1; i > 0;) {
1837 expr = MK_EXPR(kind, args[--i], expr);
1839 } else if( ( kind == CVC4::kind::EQUAL ||
1840 kind == CVC4::kind::LT || kind == CVC4::kind::GT ||
1841 kind == CVC4::kind::LEQ || kind == CVC4::kind::GEQ ) &&
1843 /* "chainable", but CVC4 internally only supports 2 args */
1844 expr = MK_EXPR(MK_CONST(Chain(kind)), args);
1845 } else if( PARSER_STATE->strictModeEnabled() && kind == CVC4::kind::ABS &&
1846 args.size() == 1 && !args[0].getType().isInteger() ) {
1847 /* first, check that ABS is even defined in this logic */
1848 PARSER_STATE->checkOperator(kind, args.size());
1849 PARSER_STATE->parseError("abs can only be applied to Int, not Real, "
1850 "while in strict SMT-LIB compliance mode");
1852 PARSER_STATE->checkOperator(kind, args.size());
1853 expr = MK_EXPR(kind, args);
1856 | LPAREN_TOK AS_TOK term[f, f2] sortSymbol[type, CHECK_DECLARED] RPAREN_TOK
1858 if(f.getKind() == CVC4::kind::APPLY_CONSTRUCTOR && type.isDatatype()) {
1859 std::vector<CVC4::Expr> v;
1860 Expr e = f.getOperator();
1861 const DatatypeConstructor& dtc =
1862 Datatype::datatypeOf(e)[Datatype::indexOf(e)];
1863 v.push_back(MK_EXPR( CVC4::kind::APPLY_TYPE_ASCRIPTION,
1864 MK_CONST(AscriptionType(dtc.getSpecializedConstructorType(type))), f.getOperator() ));
1865 v.insert(v.end(), f.begin(), f.end());
1866 expr = MK_EXPR(CVC4::kind::APPLY_CONSTRUCTOR, v);
1867 } else if(f.getKind() == CVC4::kind::EMPTYSET) {
1868 Debug("parser") << "Empty set encountered: " << f << " "
1869 << f2 << " " << type << std::endl;
1870 expr = MK_CONST( ::CVC4::EmptySet(type) );
1871 } else if(f.getKind() == CVC4::kind::UNIVERSE_SET) {
1872 expr = EXPR_MANAGER->mkNullaryOperator(type, kind::UNIVERSE_SET);
1873 } else if(f.getKind() == CVC4::kind::SEP_NIL) {
1874 //We don't want the nil reference to be a constant: for instance, it
1875 //could be of type Int but is not a const rational. However, the
1876 //expression has 0 children. So we convert to a SEP_NIL variable.
1877 expr = EXPR_MANAGER->mkNullaryOperator(type, kind::SEP_NIL);
1879 if(f.getType() != type) {
1880 PARSER_STATE->parseError("Type ascription not satisfied.");
1884 | LPAREN_TOK quantOp[kind]
1885 LPAREN_TOK sortedVarList[sortedVarNames] RPAREN_TOK
1887 PARSER_STATE->pushScope(true);
1888 for(std::vector<std::pair<std::string, CVC4::Type> >::const_iterator i =
1889 sortedVarNames.begin(), iend = sortedVarNames.end();
1892 args.push_back(PARSER_STATE->mkBoundVar((*i).first, (*i).second));
1894 Expr bvl = MK_EXPR(kind::BOUND_VAR_LIST, args);
1896 args.push_back(bvl);
1898 term[f, f2] RPAREN_TOK
1900 PARSER_STATE->popScope();
1901 switch(f.getKind()) {
1902 case CVC4::kind::RR_REWRITE:
1903 case CVC4::kind::RR_REDUCTION:
1904 case CVC4::kind::RR_DEDUCTION:
1905 if(kind == CVC4::kind::EXISTS) {
1906 PARSER_STATE->parseError("Use Exists instead of Forall for a rewrite "
1909 args.push_back(f2); // guards
1910 args.push_back(f); // rule
1911 expr = MK_EXPR(CVC4::kind::REWRITE_RULE, args);
1918 expr = MK_EXPR(kind, args);
1921 | LPAREN_TOK functionName[name, CHECK_NONE]
1922 { isBuiltinOperator = PARSER_STATE->isOperatorEnabled(name);
1923 if(isBuiltinOperator) {
1924 /* A built-in operator not already handled by the lexer */
1925 kind = PARSER_STATE->getOperatorKind(name);
1927 /* A non-built-in function application */
1928 PARSER_STATE->checkDeclaration(name, CHECK_DECLARED, SYM_VARIABLE);
1929 //hack to allow constants with parentheses (disabled for now)
1930 //if( PARSER_STATE->sygus() && !PARSER_STATE->isFunctionLike(name) ){
1931 // op = PARSER_STATE->getVariable(name);
1933 PARSER_STATE->checkFunctionLike(name);
1934 const bool isDefinedFunction =
1935 PARSER_STATE->isDefinedFunction(name);
1936 if(isDefinedFunction) {
1937 expr = PARSER_STATE->getFunction(name);
1938 kind = CVC4::kind::APPLY;
1940 expr = PARSER_STATE->getVariable(name);
1941 Type t = expr.getType();
1942 if(t.isConstructor()) {
1943 kind = CVC4::kind::APPLY_CONSTRUCTOR;
1944 } else if(t.isSelector()) {
1945 kind = CVC4::kind::APPLY_SELECTOR;
1946 } else if(t.isTester()) {
1947 kind = CVC4::kind::APPLY_TESTER;
1949 kind = CVC4::kind::APPLY_UF;
1952 args.push_back(expr);
1955 //(termList[args,expr])? RPAREN_TOK
1956 termList[args,expr] RPAREN_TOK
1957 { Debug("parser") << "args has size " << args.size() << std::endl
1958 << "expr is " << expr << std::endl;
1959 for(std::vector<Expr>::iterator i = args.begin(); i != args.end(); ++i) {
1960 Debug("parser") << "++ " << *i << std::endl;
1962 if(isBuiltinOperator) {
1963 PARSER_STATE->checkOperator(kind, args.size());
1965 expr = MK_EXPR(kind, args);
1969 ( /* An indexed function application */
1970 indexedFunctionName[op, kind] termList[args,expr] RPAREN_TOK
1972 if( kind!=kind::NULL_EXPR ){
1973 expr = MK_EXPR( kind, op, args );
1975 expr = MK_EXPR(op, args);
1977 PARSER_STATE->checkOperator(expr.getKind(), args.size());
1979 | /* Array constant (in Z3 syntax) */
1980 LPAREN_TOK AS_TOK CONST_TOK sortSymbol[type, CHECK_DECLARED]
1981 RPAREN_TOK term[f, f2] RPAREN_TOK
1983 if(!type.isArray()) {
1984 std::stringstream ss;
1985 ss << "expected array constant term, but cast is not of array type"
1987 << "cast type: " << type;
1988 PARSER_STATE->parseError(ss.str());
1991 std::stringstream ss;
1992 ss << "expected constant term inside array constant, but found "
1993 << "nonconstant term:" << std::endl
1994 << "the term: " << f;
1995 PARSER_STATE->parseError(ss.str());
1997 if(!ArrayType(type).getConstituentType().isComparableTo(f.getType())) {
1998 std::stringstream ss;
1999 ss << "type mismatch inside array constant term:" << std::endl
2000 << "array type: " << type << std::endl
2001 << "expected const type: " << ArrayType(type).getConstituentType()
2003 << "computed const type: " << f.getType();
2004 PARSER_STATE->parseError(ss.str());
2006 expr = MK_CONST( ::CVC4::ArrayStoreAll(type, f) );
2009 | /* a let binding */
2010 LPAREN_TOK LET_TOK LPAREN_TOK
2011 { PARSER_STATE->pushScope(true); }
2012 ( LPAREN_TOK symbol[name,CHECK_NONE,SYM_VARIABLE]
2013 (term[expr, f2] | sortSymbol[type,CHECK_DECLARED]
2014 { readLetSort = true; } term[expr, f2]
2017 // this is a parallel let, so we have to save up all the contributions
2018 // of the let and define them only later on
2019 { if( !PARSER_STATE->sygus() && readLetSort ){
2020 PARSER_STATE->parseError("Bad syntax for let term.");
2021 }else if(names.count(name) == 1) {
2022 std::stringstream ss;
2023 ss << "warning: symbol `" << name << "' bound multiple times by let;"
2024 << " the last binding will be used, shadowing earlier ones";
2025 PARSER_STATE->warning(ss.str());
2029 binders.push_back(std::make_pair(name, expr)); } )+
2030 { // now implement these bindings
2031 for(std::vector< std::pair<std::string, Expr> >::iterator
2032 i = binders.begin(); i != binders.end(); ++i) {
2033 PARSER_STATE->defineVar((*i).first, (*i).second);
2039 { PARSER_STATE->popScope(); }
2040 | /* match expression */
2041 LPAREN_TOK MATCH_TOK term[expr, f2] {
2042 if( !expr.getType().isDatatype() ){
2043 PARSER_STATE->parseError("Cannot match on non-datatype term.");
2049 LPAREN_TOK INDEX_TOK term[f, f2] {
2050 if( match_vindex==-1 ){
2051 match_vindex = (int)patexprs.size();
2053 patexprs.push_back( f );
2054 patconds.push_back(MK_CONST(bool(true)));
2057 | LPAREN_TOK LPAREN_TOK term[f, f2] {
2059 PARSER_STATE->pushScope(true);
2060 //f should be a constructor
2062 Debug("parser-dt") << "Pattern head : " << f << " " << f.getType() << std::endl;
2063 if( !type.isConstructor() ){
2064 PARSER_STATE->parseError("Pattern must be application of a constructor or a variable.");
2066 if( Datatype::datatypeOf(f).isParametric() ){
2067 type = Datatype::datatypeOf(f)[Datatype::indexOf(f)].getSpecializedConstructorType(expr.getType());
2069 match_ptypes = ((ConstructorType)type).getArgTypes();
2072 ( symbol[name,CHECK_NONE,SYM_VARIABLE] {
2073 if( args.size()>=match_ptypes.size() ){
2074 PARSER_STATE->parseError("Too many arguments for pattern.");
2076 //make of proper type
2077 Expr arg = PARSER_STATE->mkBoundVar(name, match_ptypes[args.size()]);
2078 args.push_back( arg );
2083 const DatatypeConstructor& dtc = Datatype::datatypeOf(f)[Datatype::indexOf(f)];
2084 if( args.size()!=dtc.getNumArgs() ){
2085 PARSER_STATE->parseError("Bad number of arguments for application of constructor in pattern.");
2088 std::vector<Expr> largs;
2089 largs.push_back( MK_EXPR( CVC4::kind::BOUND_VAR_LIST, args ) );
2090 largs.push_back( f3 );
2091 std::vector< Expr > aargs;
2092 aargs.push_back( MK_EXPR( CVC4::kind::LAMBDA, largs ) );
2093 for( unsigned i=0; i<dtc.getNumArgs(); i++ ){
2094 //can apply total version since we will be guarded by ITE condition
2095 aargs.push_back( MK_EXPR( CVC4::kind::APPLY_SELECTOR_TOTAL, dtc[i].getSelector(), expr ) );
2097 patexprs.push_back( MK_EXPR( CVC4::kind::APPLY, aargs ) );
2098 patconds.push_back( MK_EXPR( CVC4::kind::APPLY_TESTER, dtc.getTester(), expr ) );
2101 { PARSER_STATE->popScope(); }
2102 | LPAREN_TOK symbol[name,CHECK_DECLARED,SYM_VARIABLE] {
2103 f = PARSER_STATE->getVariable(name);
2105 if( !type.isConstructor() || !((ConstructorType)type).getArgTypes().empty() ){
2106 PARSER_STATE->parseError("Must apply constructors of arity greater than 0 to arguments in pattern.");
2110 const DatatypeConstructor& dtc = Datatype::datatypeOf(f)[Datatype::indexOf(f)];
2111 patexprs.push_back( f3 );
2112 patconds.push_back( MK_EXPR( CVC4::kind::APPLY_TESTER, dtc.getTester(), expr ) );
2116 RPAREN_TOK RPAREN_TOK {
2117 if( match_vindex==-1 ){
2118 const Datatype& dt = ((DatatypeType)expr.getType()).getDatatype();
2119 std::map< unsigned, bool > processed;
2121 //ensure that all datatype constructors are matched (to ensure exhaustiveness)
2122 for( unsigned i=0; i<patconds.size(); i++ ){
2123 unsigned curr_index = Datatype::indexOf(patconds[i].getOperator());
2124 if( curr_index<0 && curr_index>=dt.getNumConstructors() ){
2125 PARSER_STATE->parseError("Pattern is not legal for the head of a match.");
2127 if( processed.find( curr_index )==processed.end() ){
2128 processed[curr_index] = true;
2132 if( count!=dt.getNumConstructors() ){
2133 PARSER_STATE->parseError("Patterns are not exhaustive in a match construct.");
2137 int end_index = match_vindex==-1 ? patexprs.size()-1 : match_vindex;
2138 bool first_time = true;
2139 for( int index = end_index; index>=0; index-- ){
2141 expr = patexprs[index];
2144 expr = MK_EXPR( CVC4::kind::ITE, patconds[index], patexprs[index], expr );
2148 | symbol[name,CHECK_NONE,SYM_VARIABLE] SYGUS_ENUM_CONS_TOK
2149 symbol[name2,CHECK_NONE,SYM_VARIABLE]
2150 { std::string cname = name + "__Enum__" + name2;
2151 Debug("parser-sygus") << "Check for enum const " << cname << std::endl;
2152 expr = PARSER_STATE->getVariable(cname);
2153 // expr.getType().isConstructor() &&
2154 // ConstructorType(expr.getType()).getArity()==0;
2155 expr = MK_EXPR(CVC4::kind::APPLY_CONSTRUCTOR, expr);
2158 | symbol[name,CHECK_DECLARED,SYM_VARIABLE]
2159 { if( PARSER_STATE->sygus() && name[0]=='-' &&
2160 name.find_first_not_of("0123456789", 1) == std::string::npos ){
2161 //allow unary minus in sygus
2162 expr = MK_CONST(Rational(name));
2164 const bool isDefinedFunction =
2165 PARSER_STATE->isDefinedFunction(name);
2166 if(PARSER_STATE->isAbstractValue(name)) {
2167 expr = PARSER_STATE->mkAbstractValue(name);
2168 } else if(isDefinedFunction) {
2169 expr = MK_EXPR(CVC4::kind::APPLY,
2170 PARSER_STATE->getFunction(name));
2172 expr = PARSER_STATE->getVariable(name);
2173 Type t = PARSER_STATE->getType(name);
2174 if(t.isConstructor() && ConstructorType(t).getArity() == 0) {
2175 // don't require parentheses, immediately turn it into an apply
2176 expr = MK_EXPR(CVC4::kind::APPLY_CONSTRUCTOR, expr);
2182 /* attributed expressions */
2183 | LPAREN_TOK ATTRIBUTE_TOK term[expr, f2]
2184 ( attribute[expr, attexpr, attr]
2185 { if( ! attexpr.isNull()) {
2186 patexprs.push_back( attexpr );
2191 if(attr == ":rewrite-rule") {
2194 if(expr[1].getKind() == kind::IMPLIES ||
2195 expr[1].getKind() == kind::EQUAL) {
2199 guard = MK_CONST(bool(true));
2203 args.push_back(body[0]);
2204 args.push_back(body[1]);
2209 if( body.getKind()==kind::IMPLIES ){
2210 kind = kind::RR_DEDUCTION;
2211 }else if( body.getKind()==kind::EQUAL ){
2212 kind = body[0].getType().isBoolean() ? kind::RR_REDUCTION : kind::RR_REWRITE;
2214 PARSER_STATE->parseError("Error parsing rewrite rule.");
2216 expr = MK_EXPR( kind, args );
2217 } else if(! patexprs.empty()) {
2218 if( !f2.isNull() && f2.getKind()==kind::INST_PATTERN_LIST ){
2219 for( size_t i=0; i<f2.getNumChildren(); i++ ){
2220 if( f2[i].getKind()==kind::INST_PATTERN ){
2221 patexprs.push_back( f2[i] );
2223 std::stringstream ss;
2224 ss << "warning: rewrite rules do not support " << f2[i]
2225 << " within instantiation pattern list";
2226 PARSER_STATE->warning(ss.str());
2230 expr2 = MK_EXPR(kind::INST_PATTERN_LIST, patexprs);
2237 { expr = MK_CONST( AntlrInput::tokenToInteger($INTEGER_LITERAL) ); }
2240 { // FIXME: This doesn't work because an SMT rational is not a
2241 // valid GMP rational string
2242 expr = MK_CONST( AntlrInput::tokenToRational($DECIMAL_LITERAL) ); }
2244 | LPAREN_TOK INDEX_TOK
2245 ( bvLit=SIMPLE_SYMBOL size=INTEGER_LITERAL
2246 { if(AntlrInput::tokenText($bvLit).find("bv") == 0) {
2247 expr = MK_CONST( AntlrInput::tokenToBitvector($bvLit, $size) );
2249 PARSER_STATE->parseError("Unexpected symbol `" +
2250 AntlrInput::tokenText($bvLit) + "'");
2253 | FP_PINF_TOK eb=INTEGER_LITERAL sb=INTEGER_LITERAL
2254 { expr = MK_CONST(FloatingPoint(AntlrInput::tokenToUnsigned($eb),
2255 AntlrInput::tokenToUnsigned($sb),
2257 | FP_NINF_TOK eb=INTEGER_LITERAL sb=INTEGER_LITERAL
2258 { expr = MK_CONST(FloatingPoint(AntlrInput::tokenToUnsigned($eb),
2259 AntlrInput::tokenToUnsigned($sb),
2261 | FP_NAN_TOK eb=INTEGER_LITERAL sb=INTEGER_LITERAL
2262 { expr = MK_CONST(FloatingPoint(AntlrInput::tokenToUnsigned($eb),
2263 AntlrInput::tokenToUnsigned($sb),
2265 // NOTE: Theory parametric constants go here
2271 { assert( AntlrInput::tokenText($HEX_LITERAL).find("#x") == 0 );
2272 std::string hexString = AntlrInput::tokenTextSubstr($HEX_LITERAL, 2);
2273 expr = MK_CONST( BitVector(hexString, 16) ); }
2276 { assert( AntlrInput::tokenText($BINARY_LITERAL).find("#b") == 0 );
2277 std::string binString = AntlrInput::tokenTextSubstr($BINARY_LITERAL, 2);
2278 expr = MK_CONST( BitVector(binString, 2) ); }
2281 { expr = MK_CONST( ::CVC4::String(s) ); }
2282 | FP_RNE_TOK { expr = MK_CONST(roundNearestTiesToEven); }
2283 | FP_RNA_TOK { expr = MK_CONST(roundNearestTiesToAway); }
2284 | FP_RTP_TOK { expr = MK_CONST(roundTowardPositive); }
2285 | FP_RTN_TOK { expr = MK_CONST(roundTowardNegative); }
2286 | FP_RTZ_TOK { expr = MK_CONST(roundTowardZero); }
2287 | FP_RNE_FULL_TOK { expr = MK_CONST(roundNearestTiesToEven); }
2288 | FP_RNA_FULL_TOK { expr = MK_CONST(roundNearestTiesToAway); }
2289 | FP_RTP_FULL_TOK { expr = MK_CONST(roundTowardPositive); }
2290 | FP_RTN_FULL_TOK { expr = MK_CONST(roundTowardNegative); }
2291 | FP_RTZ_FULL_TOK { expr = MK_CONST(roundTowardZero); }
2294 { std::vector< Expr > nvec;
2295 expr = MK_EXPR( CVC4::kind::REGEXP_EMPTY, nvec );
2299 { std::vector< Expr > nvec;
2300 expr = MK_EXPR( CVC4::kind::REGEXP_SIGMA, nvec );
2304 { expr = MK_CONST( ::CVC4::EmptySet(Type())); }
2307 { //booleanType is placeholder here since we don't have type info without type annotation
2308 expr = EXPR_MANAGER->mkNullaryOperator(EXPR_MANAGER->booleanType(), kind::UNIVERSE_SET); }
2311 { //booleanType is placeholder here since we don't have type info without type annotation
2312 expr = EXPR_MANAGER->mkNullaryOperator(EXPR_MANAGER->booleanType(), kind::SEP_NIL); }
2313 // NOTE: Theory constants go here
2319 attribute[CVC4::Expr& expr, CVC4::Expr& retExpr, std::string& attr]
2323 std::vector<Expr> patexprs;
2325 bool hasValue = false;
2327 : KEYWORD ( simpleSymbolicExprNoKeyword[sexpr] { hasValue = true; } )?
2329 attr = AntlrInput::tokenText($KEYWORD);
2330 // EXPR_MANAGER->setNamedAttribute( expr, attr );
2331 if(attr == ":rewrite-rule") {
2333 std::stringstream ss;
2334 ss << "warning: Attribute " << attr
2335 << " does not take a value (ignoring)";
2336 PARSER_STATE->warning(ss.str());
2339 } else if(attr==":axiom" || attr==":conjecture" || attr==":fun-def" ||
2340 attr==":sygus" || attr==":synthesis") {
2342 std::stringstream ss;
2343 ss << "warning: Attribute " << attr
2344 << " does not take a value (ignoring)";
2345 PARSER_STATE->warning(ss.str());
2348 bool success = true;
2349 std::string attr_name = attr;
2350 attr_name.erase( attr_name.begin() );
2351 if( attr==":fun-def" ){
2352 if( expr.getKind()!=kind::EQUAL || expr[0].getKind()!=kind::APPLY_UF ){
2355 FunctionType t = (FunctionType)expr[0].getOperator().getType();
2356 for( unsigned i=0; i<expr[0].getNumChildren(); i++ ){
2357 if( expr[0][i].getKind() != kind::BOUND_VARIABLE ||
2358 expr[0][i].getType() != t.getArgTypes()[i] ){
2362 for( unsigned j=0; j<i; j++ ){
2363 if( expr[0][j]==expr[0][i] ){
2372 std::stringstream ss;
2373 ss << "warning: Function definition should be an equality whose LHS "
2374 << "is an uninterpreted function applied to unique variables.";
2375 PARSER_STATE->warning(ss.str());
2380 Type t = EXPR_MANAGER->booleanType();
2381 avar = PARSER_STATE->mkVar(attr_name, t);
2384 //Will set the attribute on auxiliary var (preserves attribute on
2385 //formula through rewriting).
2386 retExpr = MK_EXPR(kind::INST_ATTRIBUTE, avar);
2387 Command* c = new SetUserAttributeCommand( attr_name, avar );
2389 PARSER_STATE->preemptCommand(c);
2392 PARSER_STATE->attributeNotSupported(attr);
2395 | ATTRIBUTE_PATTERN_TOK LPAREN_TOK
2397 { patexprs.push_back( patexpr ); }
2400 attr = std::string(":pattern");
2401 retExpr = MK_EXPR(kind::INST_PATTERN, patexprs);
2403 | ATTRIBUTE_NO_PATTERN_TOK term[patexpr, e2]
2405 attr = std::string(":no-pattern");
2406 retExpr = MK_EXPR(kind::INST_NO_PATTERN, patexpr);
2408 | tok=( ATTRIBUTE_INST_LEVEL | ATTRIBUTE_RR_PRIORITY ) INTEGER_LITERAL
2410 Expr n = MK_CONST( AntlrInput::tokenToInteger($INTEGER_LITERAL) );
2411 std::vector<Expr> values;
2412 values.push_back( n );
2413 std::string attr_name(AntlrInput::tokenText($tok));
2414 attr_name.erase( attr_name.begin() );
2415 Type t = EXPR_MANAGER->booleanType();
2416 Expr avar = PARSER_STATE->mkVar(attr_name, t);
2417 retExpr = MK_EXPR(kind::INST_ATTRIBUTE, avar);
2418 Command* c = new SetUserAttributeCommand( attr_name, avar, values );
2420 PARSER_STATE->preemptCommand(c);
2422 | ATTRIBUTE_NAMED_TOK symbolicExpr[sexpr]
2424 attr = std::string(":named");
2425 if(!sexpr.isKeyword()) {
2426 PARSER_STATE->parseError("improperly formed :named annotation");
2428 std::string name = sexpr.getValue();
2429 PARSER_STATE->checkUserSymbol(name);
2430 // ensure expr is a closed subterm
2431 std::set<Expr> freeVars;
2432 if(!isClosed(expr, freeVars)) {
2433 assert(!freeVars.empty());
2434 std::stringstream ss;
2435 ss << ":named annotations can only name terms that are closed; this "
2436 << "one contains free variables:";
2437 for(std::set<Expr>::const_iterator i = freeVars.begin();
2438 i != freeVars.end(); ++i) {
2441 PARSER_STATE->parseError(ss.str());
2443 // check that sexpr is a fresh function symbol, and reserve it
2444 PARSER_STATE->reserveSymbolAtAssertionLevel(name);
2446 Expr func = PARSER_STATE->mkFunction(name, expr.getType());
2447 // remember the last term to have been given a :named attribute
2448 PARSER_STATE->setLastNamedTerm(expr, name);
2449 // bind name to expr with define-fun
2451 new DefineNamedFunctionCommand(name, func, std::vector<Expr>(), expr);
2453 PARSER_STATE->preemptCommand(c);
2458 * Matches a bit-vector operator (the ones parametrized by numbers)
2460 indexedFunctionName[CVC4::Expr& op, CVC4::Kind& kind]
2465 : LPAREN_TOK INDEX_TOK
2466 ( 'extract' n1=INTEGER_LITERAL n2=INTEGER_LITERAL
2467 { op = MK_CONST(BitVectorExtract(AntlrInput::tokenToUnsigned($n1),
2468 AntlrInput::tokenToUnsigned($n2))); }
2469 | 'repeat' n=INTEGER_LITERAL
2470 { op = MK_CONST(BitVectorRepeat(AntlrInput::tokenToUnsigned($n))); }
2471 | 'zero_extend' n=INTEGER_LITERAL
2472 { op = MK_CONST(BitVectorZeroExtend(AntlrInput::tokenToUnsigned($n))); }
2473 | 'sign_extend' n=INTEGER_LITERAL
2474 { op = MK_CONST(BitVectorSignExtend(AntlrInput::tokenToUnsigned($n))); }
2475 | 'rotate_left' n=INTEGER_LITERAL
2476 { op = MK_CONST(BitVectorRotateLeft(AntlrInput::tokenToUnsigned($n))); }
2477 | 'rotate_right' n=INTEGER_LITERAL
2478 { op = MK_CONST(BitVectorRotateRight(AntlrInput::tokenToUnsigned($n))); }
2479 | DIVISIBLE_TOK n=INTEGER_LITERAL
2480 { op = MK_CONST(Divisible(AntlrInput::tokenToUnsigned($n))); }
2481 | INT2BV_TOK n=INTEGER_LITERAL
2482 { op = MK_CONST(IntToBitVector(AntlrInput::tokenToUnsigned($n)));
2483 if(PARSER_STATE->strictModeEnabled()) {
2484 PARSER_STATE->parseError(
2485 "bv2nat and int2bv are not part of SMT-LIB, and aren't available "
2486 "in SMT-LIB strict compliance mode");
2488 | FP_PINF_TOK eb=INTEGER_LITERAL sb=INTEGER_LITERAL
2489 { op = MK_CONST(FloatingPoint(AntlrInput::tokenToUnsigned($eb),
2490 AntlrInput::tokenToUnsigned($sb),
2492 | FP_NINF_TOK eb=INTEGER_LITERAL sb=INTEGER_LITERAL
2493 { op = MK_CONST(FloatingPoint(AntlrInput::tokenToUnsigned($eb),
2494 AntlrInput::tokenToUnsigned($sb),
2496 | FP_NAN_TOK eb=INTEGER_LITERAL sb=INTEGER_LITERAL
2497 { op = MK_CONST(FloatingPoint(AntlrInput::tokenToUnsigned($eb),
2498 AntlrInput::tokenToUnsigned($sb),
2500 | FP_PZERO_TOK eb=INTEGER_LITERAL sb=INTEGER_LITERAL
2501 { op = MK_CONST(FloatingPoint(AntlrInput::tokenToUnsigned($eb),
2502 AntlrInput::tokenToUnsigned($sb),
2504 | FP_NZERO_TOK eb=INTEGER_LITERAL sb=INTEGER_LITERAL
2505 { op = MK_CONST(FloatingPoint(AntlrInput::tokenToUnsigned($eb),
2506 AntlrInput::tokenToUnsigned($sb),
2508 | FP_TO_FP_TOK eb=INTEGER_LITERAL sb=INTEGER_LITERAL
2509 { op = MK_CONST(FloatingPointToFPGeneric(
2510 AntlrInput::tokenToUnsigned($eb),
2511 AntlrInput::tokenToUnsigned($sb)));
2513 | FP_TO_FPBV_TOK eb=INTEGER_LITERAL sb=INTEGER_LITERAL
2514 { op = MK_CONST(FloatingPointToFPIEEEBitVector(
2515 AntlrInput::tokenToUnsigned($eb),
2516 AntlrInput::tokenToUnsigned($sb)));
2518 | FP_TO_FPFP_TOK eb=INTEGER_LITERAL sb=INTEGER_LITERAL
2519 { op = MK_CONST(FloatingPointToFPFloatingPoint(
2520 AntlrInput::tokenToUnsigned($eb),
2521 AntlrInput::tokenToUnsigned($sb)));
2523 | FP_TO_FPR_TOK eb=INTEGER_LITERAL sb=INTEGER_LITERAL
2524 { op = MK_CONST(FloatingPointToFPReal(AntlrInput::tokenToUnsigned($eb),
2525 AntlrInput::tokenToUnsigned($sb)));
2527 | FP_TO_FPS_TOK eb=INTEGER_LITERAL sb=INTEGER_LITERAL
2528 { op = MK_CONST(FloatingPointToFPSignedBitVector(
2529 AntlrInput::tokenToUnsigned($eb),
2530 AntlrInput::tokenToUnsigned($sb)));
2532 | FP_TO_FPU_TOK eb=INTEGER_LITERAL sb=INTEGER_LITERAL
2533 { op = MK_CONST(FloatingPointToFPUnsignedBitVector(
2534 AntlrInput::tokenToUnsigned($eb),
2535 AntlrInput::tokenToUnsigned($sb)));
2537 | FP_TO_UBV_TOK m=INTEGER_LITERAL
2538 { op = MK_CONST(FloatingPointToUBV(AntlrInput::tokenToUnsigned($m))); }
2539 | FP_TO_SBV_TOK m=INTEGER_LITERAL
2540 { op = MK_CONST(FloatingPointToSBV(AntlrInput::tokenToUnsigned($m))); }
2541 | TESTER_TOK term[expr, expr2] {
2542 if( expr.getKind()==kind::APPLY_CONSTRUCTOR && expr.getNumChildren()==0 ){
2543 //for nullary constructors, must get the operator
2544 expr = expr.getOperator();
2546 if( !expr.getType().isConstructor() ){
2547 PARSER_STATE->parseError("Bad syntax for test (_ is X), X must be a constructor.");
2549 op = Datatype::datatypeOf(expr)[Datatype::indexOf(expr)].getTester();
2550 kind = CVC4::kind::APPLY_TESTER;
2552 | badIndexedFunctionName
2558 * Matches an erroneous indexed function name (and args) for better
2561 badIndexedFunctionName
2565 : id=(SIMPLE_SYMBOL | QUOTED_SYMBOL | UNTERMINATED_QUOTED_SYMBOL)
2566 { PARSER_STATE->parseError(std::string("Unknown indexed function `") +
2567 AntlrInput::tokenText($id) + "'");
2572 * Matches a sequence of terms and puts them into the formulas
2574 * @param formulas the vector to fill with terms
2575 * @param expr an Expr reference for the elements of the sequence
2577 /* NOTE: We pass an Expr in here just to avoid allocating a fresh Expr every
2578 * time through this rule. */
2579 termList[std::vector<CVC4::Expr>& formulas, CVC4::Expr& expr]
2583 : ( term[expr, expr2] { formulas.push_back(expr); } )+
2587 * Matches a string, and strips off the quotes.
2589 str[std::string& s, bool fsmtlib]
2590 : STRING_LITERAL_2_0
2591 { s = AntlrInput::tokenText($STRING_LITERAL_2_0);
2592 /* strip off the quotes */
2593 s = s.substr(1, s.size() - 2);
2594 for(size_t i=0; i<s.size(); i++) {
2595 if((unsigned)s[i] > 127 && !isprint(s[i])) {
2596 PARSER_STATE->parseError("Extended/unprintable characters are not "
2597 "part of SMT-LIB, and they must be encoded "
2598 "as escape sequences");
2602 /* handle SMT-LIB standard escapes '\\' and '\"' */
2603 char* p_orig = strdup(s.c_str());
2604 char *p = p_orig, *q = p_orig;
2608 if(*q == '\\' || *q == '"') {
2624 | STRING_LITERAL_2_5
2625 { s = AntlrInput::tokenText($STRING_LITERAL_2_5);
2626 /* strip off the quotes */
2627 s = s.substr(1, s.size() - 2);
2628 for(size_t i=0; i<s.size(); i++) {
2629 if((unsigned)s[i] > 127 && !isprint(s[i])) {
2630 PARSER_STATE->parseError("Extended/unprintable characters are not "
2631 "part of SMT-LIB, and they must be encoded "
2632 "as escape sequences");
2635 // In the 2.5 version, always handle escapes (regardless of fsmtlib flag).
2636 char* p_orig = strdup(s.c_str());
2637 char *p = p_orig, *q = p_orig;
2652 * Matches a builtin operator symbol and sets kind to its associated Expr kind.
2654 builtinOp[CVC4::Kind& kind]
2656 Debug("parser") << "builtin: " << AntlrInput::tokenText(LT(1)) << std::endl;
2658 : NOT_TOK { $kind = CVC4::kind::NOT; }
2659 | IMPLIES_TOK { $kind = CVC4::kind::IMPLIES; }
2660 | AND_TOK { $kind = CVC4::kind::AND; }
2661 | OR_TOK { $kind = CVC4::kind::OR; }
2662 | XOR_TOK { $kind = CVC4::kind::XOR; }
2663 | EQUAL_TOK { $kind = CVC4::kind::EQUAL; }
2664 | DISTINCT_TOK { $kind = CVC4::kind::DISTINCT; }
2665 | ITE_TOK { $kind = CVC4::kind::ITE; }
2667 { $kind = CVC4::kind::GT; }
2668 | GREATER_THAN_EQUAL_TOK
2669 { $kind = CVC4::kind::GEQ; }
2670 | LESS_THAN_EQUAL_TOK
2671 { $kind = CVC4::kind::LEQ; }
2673 { $kind = CVC4::kind::LT; }
2674 | PLUS_TOK { $kind = CVC4::kind::PLUS; }
2675 | MINUS_TOK { $kind = CVC4::kind::MINUS; }
2676 | STAR_TOK { $kind = CVC4::kind::MULT; }
2677 | DIV_TOK { $kind = CVC4::kind::DIVISION; }
2680 { $kind = CVC4::kind::BITVECTOR_TO_NAT;
2681 if(PARSER_STATE->strictModeEnabled()) {
2682 PARSER_STATE->parseError("bv2nat and int2bv are not part of SMT-LIB, "
2683 "and aren't available in SMT-LIB strict "
2688 | DTSIZE_TOK { $kind = CVC4::kind::DT_SIZE; }
2689 | FMFCARD_TOK { $kind = CVC4::kind::CARDINALITY_CONSTRAINT; }
2690 | FMFCARDVAL_TOK { $kind = CVC4::kind::CARDINALITY_VALUE; }
2691 | INST_CLOSURE_TOK { $kind = CVC4::kind::INST_CLOSURE; }
2693 // NOTE: Theory operators no longer go here, add to smt2.cpp. Only
2694 // special cases may go here. When this comment was written (2015
2695 // Apr), the special cases were: core theory operators, arith
2696 // operators which start with symbols like * / + >= etc, quantifier
2697 // theory operators, and operators which depended on parser's state
2698 // to accept or reject.
2701 quantOp[CVC4::Kind& kind]
2703 Debug("parser") << "quant: " << AntlrInput::tokenText(LT(1)) << std::endl;
2705 : EXISTS_TOK { $kind = CVC4::kind::EXISTS; }
2706 | FORALL_TOK { $kind = CVC4::kind::FORALL; }
2710 * Matches a (possibly undeclared) function symbol (returning the string)
2711 * @param check what kind of check to do with the symbol
2713 functionName[std::string& name, CVC4::parser::DeclarationCheck check]
2714 : symbol[name,check,SYM_VARIABLE]
2718 * Matches a sequence of sort symbols and fills them into the given
2721 sortList[std::vector<CVC4::Type>& sorts]
2725 : ( sortSymbol[t,CHECK_DECLARED] { sorts.push_back(t); } )*
2728 nonemptySortList[std::vector<CVC4::Type>& sorts]
2732 : ( sortSymbol[t,CHECK_DECLARED] { sorts.push_back(t); } )+
2736 * Matches a sequence of (variable,sort) symbol pairs and fills them
2737 * into the given vector.
2739 sortedVarList[std::vector<std::pair<std::string, CVC4::Type> >& sortedVars]
2744 : ( LPAREN_TOK symbol[name,CHECK_NONE,SYM_VARIABLE]
2745 sortSymbol[t,CHECK_DECLARED] RPAREN_TOK
2746 { sortedVars.push_back(make_pair(name, t)); }
2751 * Matches the sort symbol, which can be an arbitrary symbol.
2752 * @param check the check to perform on the name
2754 sortName[std::string& name, CVC4::parser::DeclarationCheck check]
2755 : symbol[name,check,SYM_SORT]
2758 sortSymbol[CVC4::Type& t, CVC4::parser::DeclarationCheck check]
2761 std::vector<CVC4::Type> args;
2762 std::vector<uint64_t> numerals;
2763 bool indexed = false;
2765 : sortName[name,CHECK_NONE]
2767 if(check == CHECK_DECLARED || PARSER_STATE->isDeclared(name, SYM_SORT)) {
2768 t = PARSER_STATE->getSort(name);
2770 t = PARSER_STATE->mkUnresolvedType(name);
2773 | LPAREN_TOK (INDEX_TOK {indexed = true;} | {indexed = false;})
2774 symbol[name,CHECK_NONE,SYM_SORT]
2775 ( nonemptyNumeralList[numerals]
2776 { // allow sygus inputs to elide the `_'
2777 if( !indexed && !PARSER_STATE->sygus() ) {
2778 std::stringstream ss;
2779 ss << "SMT-LIB requires use of an indexed sort here, e.g. (_ " << name
2781 PARSER_STATE->parseError(ss.str());
2783 if( name == "BitVec" ) {
2784 if( numerals.size() != 1 ) {
2785 PARSER_STATE->parseError("Illegal bitvector type.");
2787 if(numerals.front() == 0) {
2788 PARSER_STATE->parseError("Illegal bitvector size: 0");
2790 t = EXPR_MANAGER->mkBitVectorType(numerals.front());
2791 } else if ( name == "FloatingPoint" ) {
2792 if( numerals.size() != 2 ) {
2793 PARSER_STATE->parseError("Illegal floating-point type.");
2795 if(!validExponentSize(numerals[0])) {
2796 PARSER_STATE->parseError("Illegal floating-point exponent size");
2798 if(!validSignificandSize(numerals[1])) {
2799 PARSER_STATE->parseError("Illegal floating-point significand size");
2801 t = EXPR_MANAGER->mkFloatingPointType(numerals[0],numerals[1]);
2803 std::stringstream ss;
2804 ss << "unknown indexed sort symbol `" << name << "'";
2805 PARSER_STATE->parseError(ss.str());
2810 std::stringstream ss;
2811 ss << "Unexpected use of indexing operator `_' before `" << name
2812 << "', try leaving it out";
2813 PARSER_STATE->parseError(ss.str());
2816 PARSER_STATE->parseError("Extra parentheses around sort name not "
2817 "permitted in SMT-LIB");
2818 } else if(name == "Array" &&
2819 PARSER_STATE->isTheoryEnabled(Smt2::THEORY_ARRAYS) ) {
2820 if(args.size() != 2) {
2821 PARSER_STATE->parseError("Illegal array type.");
2823 t = EXPR_MANAGER->mkArrayType( args[0], args[1] );
2824 } else if(name == "Set" &&
2825 PARSER_STATE->isTheoryEnabled(Smt2::THEORY_SETS) ) {
2826 if(args.size() != 1) {
2827 PARSER_STATE->parseError("Illegal set type.");
2829 t = EXPR_MANAGER->mkSetType( args[0] );
2830 } else if(check == CHECK_DECLARED ||
2831 PARSER_STATE->isDeclared(name, SYM_SORT)) {
2832 t = PARSER_STATE->getSort(name, args);
2834 // make unresolved type
2836 t = PARSER_STATE->mkUnresolvedType(name);
2837 Debug("parser-param") << "param: make unres type " << name
2840 t = PARSER_STATE->mkUnresolvedTypeConstructor(name,args);
2841 t = SortConstructorType(t).instantiate( args );
2842 Debug("parser-param")
2843 << "param: make unres param type " << name << " " << args.size()
2844 << " " << PARSER_STATE->getArity( name ) << std::endl;
2852 * Matches a list of symbols, with check and type arguments as for the
2853 * symbol[] rule below.
2855 symbolList[std::vector<std::string>& names,
2856 CVC4::parser::DeclarationCheck check,
2857 CVC4::parser::SymbolType type]
2861 : ( symbol[id,check,type] { names.push_back(id); } )*
2865 * Matches an symbol and sets the string reference parameter id.
2866 * @param id string to hold the symbol
2867 * @param check what kinds of check to do on the symbol
2868 * @param type the intended namespace for the symbol
2870 symbol[std::string& id,
2871 CVC4::parser::DeclarationCheck check,
2872 CVC4::parser::SymbolType type]
2874 { id = AntlrInput::tokenText($SIMPLE_SYMBOL);
2875 if(!PARSER_STATE->isAbstractValue(id)) {
2876 // if an abstract value, SmtEngine handles declaration
2877 PARSER_STATE->checkDeclaration(id, check, type);
2880 | ( 'repeat' { id = "repeat"; }
2881 /* these are keywords in SyGuS but we don't want to inhibit their
2882 * use as symbols in SMT-LIB */
2883 | SET_OPTIONS_TOK { id = "set-options"; }
2884 | DECLARE_VAR_TOK { id = "declare-var"; }
2885 | DECLARE_PRIMED_VAR_TOK { id = "declare-primed-var"; }
2886 | SYNTH_FUN_TOK { id = "synth-fun"; }
2887 | SYNTH_INV_TOK { id = "synth-inv"; }
2888 | CONSTRAINT_TOK { id = "constraint"; }
2889 | INV_CONSTRAINT_TOK { id = "inv-constraint"; }
2890 | CHECK_SYNTH_TOK { id = "check-synth"; }
2892 { PARSER_STATE->checkDeclaration(id, check, type); }
2894 { id = AntlrInput::tokenText($QUOTED_SYMBOL);
2895 /* strip off the quotes */
2896 id = id.substr(1, id.size() - 2);
2897 if(!PARSER_STATE->isAbstractValue(id)) {
2898 // if an abstract value, SmtEngine handles declaration
2899 PARSER_STATE->checkDeclaration(id, check, type);
2902 | UNTERMINATED_QUOTED_SYMBOL
2904 { PARSER_STATE->unexpectedEOF("unterminated |quoted| symbol"); }
2906 { PARSER_STATE->unexpectedEOF("backslash not permitted in |quoted| "
2912 * Matches a nonempty list of numerals.
2913 * @param numerals the (empty) vector to house the numerals.
2915 nonemptyNumeralList[std::vector<uint64_t>& numerals]
2917 { numerals.push_back(AntlrInput::tokenToUnsigned($INTEGER_LITERAL)); }
2922 * Parses a datatype definition
2924 datatypeDef[bool isCo, std::vector<CVC4::Datatype>& datatypes,
2925 std::vector< CVC4::Type >& params]
2929 /* This really needs to be CHECK_NONE, or mutually-recursive
2930 * datatypes won't work, because this type will already be
2931 * "defined" as an unresolved type; don't worry, we check
2933 : symbol[id,CHECK_NONE,SYM_SORT] { PARSER_STATE->pushScope(true); }
2934 /* ( '[' symbol[id2,CHECK_UNDECLARED,SYM_SORT] {
2935 t = PARSER_STATE->mkSort(id2);
2936 params.push_back( t );
2938 ( symbol[id2,CHECK_UNDECLARED,SYM_SORT] {
2939 t = PARSER_STATE->mkSort(id2);
2940 params.push_back( t ); }
2942 )?*/ //AJR: this isn't necessary if we use z3's style
2943 { datatypes.push_back(Datatype(id,params,isCo));
2944 if(!PARSER_STATE->isUnresolvedType(id)) {
2945 // if not unresolved, must be undeclared
2946 PARSER_STATE->checkDeclaration(id, CHECK_UNDECLARED, SYM_SORT);
2949 ( LPAREN_TOK constructorDef[datatypes.back()] RPAREN_TOK )+
2950 { PARSER_STATE->popScope(); }
2954 * Parses a constructor defintion for type
2956 constructorDef[CVC4::Datatype& type]
2959 CVC4::DatatypeConstructor* ctor = NULL;
2961 : symbol[id,CHECK_UNDECLARED,SYM_VARIABLE]
2962 { // make the tester
2963 std::string testerId("is-");
2964 testerId.append(id);
2965 PARSER_STATE->checkDeclaration(testerId, CHECK_UNDECLARED, SYM_VARIABLE);
2966 ctor = new CVC4::DatatypeConstructor(id, testerId);
2968 ( LPAREN_TOK selector[*ctor] RPAREN_TOK )*
2969 { // make the constructor
2970 type.addConstructor(*ctor);
2971 Debug("parser-idt") << "constructor: " << id.c_str() << std::endl;
2976 selector[CVC4::DatatypeConstructor& ctor]
2981 : symbol[id,CHECK_UNDECLARED,SYM_SORT] sortSymbol[t,CHECK_NONE]
2982 { ctor.addArg(id, t);
2983 Debug("parser-idt") << "selector: " << id.c_str()
2984 << " of type " << t << std::endl;
2988 // Base SMT-LIB tokens
2989 ASSERT_TOK : 'assert';
2990 CHECKSAT_TOK : 'check-sat';
2991 DECLARE_FUN_TOK : 'declare-fun';
2992 DECLARE_SORT_TOK : 'declare-sort';
2993 DEFINE_FUN_TOK : 'define-fun';
2994 DEFINE_FUN_REC_TOK : 'define-fun-rec';
2995 DEFINE_FUNS_REC_TOK : 'define-funs-rec';
2996 DEFINE_SORT_TOK : 'define-sort';
2997 GET_VALUE_TOK : 'get-value';
2998 GET_ASSIGNMENT_TOK : 'get-assignment';
2999 GET_ASSERTIONS_TOK : 'get-assertions';
3000 GET_PROOF_TOK : 'get-proof';
3001 GET_UNSAT_CORE_TOK : 'get-unsat-core';
3003 RESET_TOK : { PARSER_STATE->v2_5(false) }? 'reset';
3004 RESET_ASSERTIONS_TOK : 'reset-assertions';
3007 ATTRIBUTE_TOK : '!';
3011 SET_LOGIC_TOK : 'set-logic';
3012 SET_INFO_TOK : 'set-info';
3013 META_INFO_TOK : 'meta-info';
3014 GET_INFO_TOK : 'get-info';
3015 SET_OPTION_TOK : 'set-option';
3016 GET_OPTION_TOK : 'get-option';
3020 CONST_TOK : 'const';
3022 // extended commands
3023 DECLARE_CODATATYPE_TOK : { PARSER_STATE->v2_6() }? 'declare-codatatype';
3024 DECLARE_DATATYPE_TOK : { PARSER_STATE->v2_6() }? 'declare-datatype';
3025 DECLARE_DATATYPES_2_5_TOK : { !PARSER_STATE->v2_6() }?'declare-datatypes';
3026 DECLARE_DATATYPES_TOK : { PARSER_STATE->v2_6() }?'declare-datatypes';
3027 DECLARE_CODATATYPES_2_5_TOK : { !PARSER_STATE->v2_6() }?'declare-codatatypes';
3028 DECLARE_CODATATYPES_TOK : { PARSER_STATE->v2_6() }?'declare-codatatypes';
3029 PAR_TOK : { PARSER_STATE->v2_6() }?'par';
3030 TESTER_TOK : { PARSER_STATE->v2_6() && PARSER_STATE->isTheoryEnabled(Smt2::THEORY_DATATYPES) }?'is';
3031 MATCH_TOK : { PARSER_STATE->v2_6() && PARSER_STATE->isTheoryEnabled(Smt2::THEORY_DATATYPES) }?'match';
3032 GET_MODEL_TOK : 'get-model';
3034 REWRITE_RULE_TOK : 'assert-rewrite';
3035 REDUCTION_RULE_TOK : 'assert-reduction';
3036 PROPAGATION_RULE_TOK : 'assert-propagation';
3037 DECLARE_SORTS_TOK : 'declare-sorts';
3038 DECLARE_FUNS_TOK : 'declare-funs';
3039 DECLARE_PREDS_TOK : 'declare-preds';
3040 DEFINE_TOK : 'define';
3041 DECLARE_CONST_TOK : 'declare-const';
3042 DEFINE_CONST_TOK : 'define-const';
3043 SIMPLIFY_TOK : 'simplify';
3044 INCLUDE_TOK : 'include';
3045 GET_QE_TOK : 'get-qe';
3046 GET_QE_DISJUNCT_TOK : 'get-qe-disjunct';
3049 SYNTH_FUN_TOK : 'synth-fun';
3050 SYNTH_INV_TOK : 'synth-inv';
3051 CHECK_SYNTH_TOK : 'check-synth';
3052 DECLARE_VAR_TOK : 'declare-var';
3053 DECLARE_PRIMED_VAR_TOK : 'declare-primed-var';
3054 CONSTRAINT_TOK : 'constraint';
3055 INV_CONSTRAINT_TOK : 'inv-constraint';
3056 SET_OPTIONS_TOK : 'set-options';
3057 SYGUS_ENUM_TOK : { PARSER_STATE->sygus() }? 'Enum';
3058 SYGUS_ENUM_CONS_TOK : { PARSER_STATE->sygus() }? '::';
3059 SYGUS_CONSTANT_TOK : { PARSER_STATE->sygus() }? 'Constant';
3060 SYGUS_VARIABLE_TOK : { PARSER_STATE->sygus() }? 'Variable';
3061 SYGUS_INPUT_VARIABLE_TOK : { PARSER_STATE->sygus() }? 'InputVariable';
3062 SYGUS_LOCAL_VARIABLE_TOK : { PARSER_STATE->sygus() }? 'LocalVariable';
3065 ATTRIBUTE_PATTERN_TOK : ':pattern';
3066 ATTRIBUTE_NO_PATTERN_TOK : ':no-pattern';
3067 ATTRIBUTE_NAMED_TOK : ':named';
3068 ATTRIBUTE_INST_LEVEL : ':quant-inst-max-level';
3069 ATTRIBUTE_RR_PRIORITY : ':rr-priority';
3071 // operators (NOTE: theory symbols go here)
3072 AMPERSAND_TOK : '&';
3075 DISTINCT_TOK : 'distinct';
3078 EXISTS_TOK : 'exists';
3079 FORALL_TOK : 'forall';
3080 GREATER_THAN_TOK : '>';
3081 GREATER_THAN_EQUAL_TOK : '>=';
3083 LESS_THAN_TOK : '<';
3084 LESS_THAN_EQUAL_TOK : '<=';
3088 // PERCENT_TOK : '%';
3096 DIVISIBLE_TOK : 'divisible';
3098 BV2NAT_TOK : 'bv2nat';
3099 INT2BV_TOK : 'int2bv';
3101 RENOSTR_TOK : 're.nostr';
3102 REALLCHAR_TOK : 're.allchar';
3104 DTSIZE_TOK : 'dt.size';
3106 FMFCARD_TOK : 'fmf.card';
3107 FMFCARDVAL_TOK : 'fmf.card.val';
3109 INST_CLOSURE_TOK : 'inst-closure';
3111 EMPTYSET_TOK: { PARSER_STATE->isTheoryEnabled(Smt2::THEORY_SETS) }? 'emptyset';
3112 UNIVSET_TOK: { PARSER_STATE->isTheoryEnabled(Smt2::THEORY_SETS) }? 'univset';
3113 NILREF_TOK: { PARSER_STATE->isTheoryEnabled(Smt2::THEORY_SEP) }? 'sep.nil';
3114 // Other set theory operators are not
3115 // tokenized and handled directly when
3116 // processing a term
3118 FP_PINF_TOK : '+oo';
3119 FP_NINF_TOK : '-oo';
3120 FP_PZERO_TOK : '+zero';
3121 FP_NZERO_TOK : '-zero';
3122 FP_NAN_TOK : { PARSER_STATE->isTheoryEnabled(Smt2::THEORY_FP) }? 'NaN';
3124 FP_TO_FP_TOK : { PARSER_STATE->isTheoryEnabled(Smt2::THEORY_FP) }? 'to_fp';
3125 FP_TO_FPBV_TOK : { PARSER_STATE->isTheoryEnabled(Smt2::THEORY_FP) }? 'to_fp_bv';
3126 FP_TO_FPFP_TOK : { PARSER_STATE->isTheoryEnabled(Smt2::THEORY_FP) }? 'to_fp_fp';
3127 FP_TO_FPR_TOK : { PARSER_STATE->isTheoryEnabled(Smt2::THEORY_FP) }? 'to_fp_real';
3128 FP_TO_FPS_TOK : { PARSER_STATE->isTheoryEnabled(Smt2::THEORY_FP) }? 'to_fp_signed';
3129 FP_TO_FPU_TOK : { PARSER_STATE->isTheoryEnabled(Smt2::THEORY_FP) }? 'to_fp_unsigned';
3130 FP_TO_UBV_TOK : { PARSER_STATE->isTheoryEnabled(Smt2::THEORY_FP) }? 'fp.to_ubv';
3131 FP_TO_SBV_TOK : { PARSER_STATE->isTheoryEnabled(Smt2::THEORY_FP) }? 'fp.to_sbv';
3132 FP_RNE_TOK : { PARSER_STATE->isTheoryEnabled(Smt2::THEORY_FP) }? 'RNE';
3133 FP_RNA_TOK : { PARSER_STATE->isTheoryEnabled(Smt2::THEORY_FP) }? 'RNA';
3134 FP_RTP_TOK : { PARSER_STATE->isTheoryEnabled(Smt2::THEORY_FP) }? 'RTP';
3135 FP_RTN_TOK : { PARSER_STATE->isTheoryEnabled(Smt2::THEORY_FP) }? 'RTN';
3136 FP_RTZ_TOK : { PARSER_STATE->isTheoryEnabled(Smt2::THEORY_FP) }? 'RTZ';
3137 FP_RNE_FULL_TOK : { PARSER_STATE->isTheoryEnabled(Smt2::THEORY_FP) }? 'roundNearestTiesToEven';
3138 FP_RNA_FULL_TOK : { PARSER_STATE->isTheoryEnabled(Smt2::THEORY_FP) }? 'roundNearestTiesToAway';
3139 FP_RTP_FULL_TOK : { PARSER_STATE->isTheoryEnabled(Smt2::THEORY_FP) }? 'roundTowardPositive';
3140 FP_RTN_FULL_TOK : { PARSER_STATE->isTheoryEnabled(Smt2::THEORY_FP) }? 'roundTowardNegative';
3141 FP_RTZ_FULL_TOK : { PARSER_STATE->isTheoryEnabled(Smt2::THEORY_FP) }? 'roundTowardZero';
3144 * A sequence of printable ASCII characters (except backslash) that starts
3145 * and ends with | and does not otherwise contain |.
3147 * You shouldn't generally use this in parser rules, as the |quoting|
3148 * will be part of the token text. Use the symbol[] parser rule instead.
3151 : '|' ~('|' | '\\')* '|'
3153 UNTERMINATED_QUOTED_SYMBOL
3154 : '|' ~('|' | '\\')*
3158 * Matches a keyword from the input. A keyword is a simple symbol prefixed
3162 : ':' (ALPHA | DIGIT | SYMBOL_CHAR)+
3166 * Matches a "simple" symbol: a non-empty sequence of letters, digits and
3167 * the characters + - / * = % ? ! . $ ~ & ^ < > @ that does not start with a
3168 * digit, and is not the special reserved symbols '!' or '_'.
3171 : (ALPHA | SYMBOL_CHAR) (ALPHA | DIGIT | SYMBOL_CHAR)+
3173 | SYMBOL_CHAR_NOUNDERSCORE_NOATTRIBUTE
3177 * Matches and skips whitespace in the input.
3180 : (' ' | '\t' | '\f' | '\r' | '\n')+ { SKIP(); }
3184 * Matches an integer constant from the input (non-empty sequence of
3185 * digits, with no leading zeroes).
3192 * Match an integer constant. In non-strict mode, this is any sequence
3193 * of digits. In strict mode, non-zero integers can't have leading
3198 char *start = (char*) GETCHARINDEX();
3201 { Debug("parser-extra") << "NUMERAL: "
3202 << (uintptr_t)start << ".." << GETCHARINDEX()
3203 << " strict? " << (bool)(PARSER_STATE->strictModeEnabled())
3204 << " ^0? " << (bool)(*start == '0')
3205 << " len>1? " << (bool)(start < (char*)(GETCHARINDEX() - 1))
3207 { !PARSER_STATE->strictModeEnabled() ||
3209 start == (char*)(GETCHARINDEX() - 1) }?
3213 * Matches a decimal constant from the input.
3216 : NUMERAL '.' DIGIT+
3220 * Matches a hexadecimal constant.
3227 * Matches a binary constant.
3234 * Matches a double-quoted string literal from SMT-LIB 2.0.
3235 * Escaping is supported, and * escape character '\' has to be escaped.
3237 * You shouldn't generally use this in parser rules, as the quotes
3238 * will be part of the token text. Use the str[] parser rule instead.
3241 : { PARSER_STATE->v2_0() }?=>
3242 '"' ('\\' . | ~('\\' | '"'))* '"'
3246 * Matches a double-quoted string literal from SMT-LIB 2.5.
3247 * You escape a double-quote inside the string with "", e.g.,
3248 * "This is a string literal with "" a single, embedded double quote."
3250 * You shouldn't generally use this in parser rules, as the quotes
3251 * will be part of the token text. Use the str[] parser rule instead.
3254 : { PARSER_STATE->v2_5(false) || PARSER_STATE->sygus() }?=>
3255 '"' (~('"') | '""')* '"'
3259 * Matches sygus quoted literal
3261 SYGUS_QUOTED_LITERAL
3262 : { PARSER_STATE->sygus() }?=>
3263 '"' (ALPHA|DIGIT)* '"'
3267 * Matches the comments and ignores them
3270 : ';' (~('\n' | '\r'))* { SKIP(); }
3274 * Matches any letter ('a'-'z' and 'A'-'Z').
3283 * Matches the digits (0-9)
3285 fragment DIGIT : '0'..'9';
3287 fragment HEX_DIGIT : DIGIT | 'a'..'f' | 'A'..'F';
3290 * Matches the characters that may appear as a one-character "symbol"
3291 * (which excludes _ and !, which are reserved words in SMT-LIB).
3293 fragment SYMBOL_CHAR_NOUNDERSCORE_NOATTRIBUTE
3294 : '+' | '-' | '/' | '*' | '=' | '%' | '?' | '.' | '$' | '~'
3295 | '&' | '^' | '<' | '>' | '@'
3299 * Matches the characters that may appear in a "symbol" (i.e., an identifier)
3301 fragment SYMBOL_CHAR
3302 : SYMBOL_CHAR_NOUNDERSCORE_NOATTRIBUTE | '_' | '!'