diff options
Diffstat (limited to 'src/parser')
-rw-r--r-- | src/parser/cvc/Cvc.g | 57 | ||||
-rw-r--r-- | src/parser/smt/Smt.g | 13 | ||||
-rw-r--r-- | src/parser/smt/smt.cpp | 62 | ||||
-rw-r--r-- | src/parser/smt/smt.h | 4 | ||||
-rw-r--r-- | src/parser/smt2/Smt2.g | 195 | ||||
-rw-r--r-- | src/parser/smt2/smt2.cpp | 24 | ||||
-rw-r--r-- | src/parser/smt2/smt2.h | 1 |
7 files changed, 292 insertions, 64 deletions
diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g index 1f0e6b890..2988ae4ef 100644 --- a/src/parser/cvc/Cvc.g +++ b/src/parser/cvc/Cvc.g @@ -1066,13 +1066,13 @@ restrictedTypePossiblyFunctionLHS[CVC4::Type& t, PARSER_STATE->isDeclared(id, SYM_SORT)) { Debug("parser-param") << "param: getSort " << id << " " << types.size() << " " << PARSER_STATE->getArity( id ) << " " << PARSER_STATE->isDeclared(id, SYM_SORT) << std::endl; - if( types.size()>0 ){ + if(types.size() > 0) { t = PARSER_STATE->getSort(id, types); }else{ t = PARSER_STATE->getSort(id); } } else { - if( types.empty() ){ + if(types.empty()) { t = PARSER_STATE->mkUnresolvedType(id); Debug("parser-param") << "param: make unres type " << id << std::endl; }else{ @@ -1236,22 +1236,36 @@ prefixFormula[CVC4::Expr& f] std::vector<std::string> ids; std::vector<Expr> terms; std::vector<Type> types; + std::vector<Expr> bvs; Type t; + Kind k; + Expr ipl; } /* quantifiers */ - : FORALL_TOK { PARSER_STATE->pushScope(); } LPAREN - boundVarDecl[ids,t] (COMMA boundVarDecl[ids,t])* RPAREN - COLON instantiationPatterns? formula[f] - { PARSER_STATE->popScope(); - UNSUPPORTED("quantifiers not supported yet"); - f = EXPR_MANAGER->mkVar(EXPR_MANAGER->booleanType()); + : ( FORALL_TOK { k = kind::FORALL; } | EXISTS_TOK { k = kind::EXISTS; } ) + { PARSER_STATE->pushScope(); } LPAREN + boundVarDecl[ids,t] + { for(std::vector<std::string>::const_iterator i = ids.begin(); i != ids.end(); ++i) { + bvs.push_back(PARSER_STATE->mkVar(*i, t)); + } + ids.clear(); } - | EXISTS_TOK { PARSER_STATE->pushScope(); } LPAREN - boundVarDecl[ids,t] (COMMA boundVarDecl[ids,t])* RPAREN - COLON instantiationPatterns? formula[f] + ( COMMA boundVarDecl[ids,t] + { + for(std::vector<std::string>::const_iterator i = ids.begin(); i != ids.end(); ++i) { + bvs.push_back(PARSER_STATE->mkVar(*i, t)); + } + ids.clear(); + } + )* RPAREN { + terms.push_back( EXPR_MANAGER->mkExpr( kind::BOUND_VAR_LIST, bvs ) ); } + COLON instantiationPatterns[ipl]? formula[f] { PARSER_STATE->popScope(); - UNSUPPORTED("quantifiers not supported yet"); - f = EXPR_MANAGER->mkVar(EXPR_MANAGER->booleanType()); + terms.push_back(f); + if(! ipl.isNull()) { + terms.push_back(ipl); + } + f = MK_EXPR(k, terms); } /* lets: letDecl defines the variables and functionss, we just @@ -1283,11 +1297,20 @@ prefixFormula[CVC4::Expr& f] } ; -instantiationPatterns +instantiationPatterns[ CVC4::Expr& expr ] @init { + std::vector<Expr> args; Expr f; + std::vector<Expr> patterns; } - : ( PATTERN_TOK LPAREN formula[f] (COMMA formula[f])* RPAREN COLON )+ + : ( PATTERN_TOK LPAREN formula[f] { args.push_back( f ); } (COMMA formula[f] { args.push_back( f ); } )* RPAREN COLON + { patterns.push_back( EXPR_MANAGER->mkExpr( kind::INST_PATTERN, args ) ); + args.clear(); + } )+ + { if(! patterns.empty()) { + expr = EXPR_MANAGER->mkExpr( kind::INST_PATTERN_LIST, patterns ); + } + } ; /** @@ -1417,7 +1440,7 @@ tupleStore[CVC4::Expr& f] Expr f2; } : k=numeral ASSIGN_TOK uminusTerm[f2] - { + { Type t = f.getType(); if(! t.isDatatype()) { PARSER_STATE->parseError("tuple-update applied to non-tuple"); @@ -1456,7 +1479,7 @@ recordStore[CVC4::Expr& f] Expr f2; } : identifier[id,CHECK_NONE,SYM_VARIABLE] ASSIGN_TOK uminusTerm[f2] - { + { Type t = f.getType(); if(! t.isDatatype()) { PARSER_STATE->parseError("record-update applied to non-record"); diff --git a/src/parser/smt/Smt.g b/src/parser/smt/Smt.g index 6dd4e78f3..568f3bb92 100644 --- a/src/parser/smt/Smt.g +++ b/src/parser/smt/Smt.g @@ -244,6 +244,19 @@ annotatedFormula[CVC4::Expr& expr] } } + | /* A quantifier */ + LPAREN_TOK + ( FORALL_TOK { kind = kind::FORALL; } | EXISTS_TOK { kind = kind::EXISTS; } ) + { PARSER_STATE->pushScope(); } + ( LPAREN_TOK let_identifier[name,CHECK_NONE] t=sortSymbol RPAREN_TOK + { args.push_back(PARSER_STATE->mkVar(name, t)); } + )+ + annotatedFormula[expr] RPAREN_TOK + { args.push_back(expr); + expr = MK_EXPR(kind, args); + PARSER_STATE->popScope(); + } + | /* A non-built-in function application */ // Semantic predicate not necessary if parenthesized subexpressions diff --git a/src/parser/smt/smt.cpp b/src/parser/smt/smt.cpp index c3b81655c..4d3c1d086 100644 --- a/src/parser/smt/smt.cpp +++ b/src/parser/smt/smt.cpp @@ -29,6 +29,10 @@ namespace parser { std::hash_map<const std::string, Smt::Logic, CVC4::StringHashFunction> Smt::newLogicMap() { std::hash_map<const std::string, Smt::Logic, CVC4::StringHashFunction> logicMap; + logicMap["AUFLIA"] = AUFLIA; + logicMap["AUFLIRA"] = AUFLIRA; + logicMap["AUFNIRA"] = AUFNIRA; + logicMap["LRA"] = LRA; logicMap["QF_AX"] = QF_AX; logicMap["QF_BV"] = QF_BV; logicMap["QF_IDL"] = QF_IDL; @@ -54,6 +58,9 @@ std::hash_map<const std::string, Smt::Logic, CVC4::StringHashFunction> Smt::newL logicMap["QF_UFNIRA"] = QF_UFNIRA; logicMap["QF_AUFLIA"] = QF_AUFLIA; logicMap["QF_AUFLIRA"] = QF_AUFLIRA; + logicMap["UFNIA"] = UFNIA; + logicMap["UFNIRA"] = UFNIRA; + logicMap["UFLRA"] = UFLRA; logicMap["QF_ALL_SUPPORTED"] = QF_ALL_SUPPORTED; logicMap["ALL_SUPPORTED"] = ALL_SUPPORTED; return logicMap; @@ -109,6 +116,22 @@ void Smt::addTheory(Theory theory) { break; } + case THEORY_BITVECTOR_ARRAYS_EX: { + Unimplemented("Cannot yet handle SMT-LIBv1 bitvector arrays (i.e., the BitVector_ArraysEx theory)"); + //addOperator(kind::SELECT); + //addOperator(kind::STORE); + break; + } + + case THEORY_INT_INT_REAL_ARRAY_ARRAYS_EX: { + defineType("Array1", getExprManager()->mkArrayType(getSort("Int"), getSort("Real"))); + defineType("Array2", getExprManager()->mkArrayType(getSort("Int"), getSort("Array1"))); + addOperator(kind::SELECT); + addOperator(kind::STORE); + break; + } + + case THEORY_INT_ARRAYS: case THEORY_INT_ARRAYS_EX: { defineType("Array", getExprManager()->mkArrayType(getExprManager()->integerType(), getExprManager()->integerType())); @@ -140,6 +163,9 @@ void Smt::addTheory(Theory theory) { case THEORY_BITVECTORS: break; + case THEORY_QUANTIFIERS: + break; + default: Unhandled(theory); } @@ -244,13 +270,14 @@ void Smt::setLogic(const std::string& name) { break; case QF_AUFLIRA: - addTheory(THEORY_ARRAYS_EX); + addTheory(THEORY_INT_INT_REAL_ARRAY_ARRAYS_EX); addUf(); addTheory(THEORY_INTS); addTheory(THEORY_REALS); break; case ALL_SUPPORTED: + addTheory(THEORY_QUANTIFIERS); /* fall through */ case QF_ALL_SUPPORTED: addTheory(THEORY_ARRAYS_EX); @@ -261,14 +288,41 @@ void Smt::setLogic(const std::string& name) { break; case AUFLIA: + addUf(); + addTheory(THEORY_INTS); + addTheory(THEORY_INT_ARRAYS_EX); + addTheory(THEORY_QUANTIFIERS); + break; + case AUFLIRA: case AUFNIRA: + addUf(); + addTheory(THEORY_INTS); + addTheory(THEORY_REALS); + addTheory(THEORY_INT_INT_REAL_ARRAY_ARRAYS_EX); + addTheory(THEORY_QUANTIFIERS); + break; + case LRA: - case UFLRA: case UFNIA: - Unhandled(name); + addUf(); + addTheory(THEORY_INTS); + addTheory(THEORY_QUANTIFIERS); + break; + case UFNIRA: + addUf(); + addTheory(THEORY_INTS); + addTheory(THEORY_REALS); + addTheory(THEORY_QUANTIFIERS); + break; + + case UFLRA: + addUf(); + addTheory(THEORY_REALS); + addTheory(THEORY_QUANTIFIERS); + break; } -} +}/* Smt::setLogic() */ }/* CVC4::parser namespace */ }/* CVC4 namespace */ diff --git a/src/parser/smt/smt.h b/src/parser/smt/smt.h index d77808930..7b1dfc345 100644 --- a/src/parser/smt/smt.h +++ b/src/parser/smt/smt.h @@ -65,6 +65,7 @@ public: QF_UFNIRA, // nonstandard QF_UFNRA, UFLRA, + UFNIRA, // nonstandard UFNIA, QF_ALL_SUPPORTED, // nonstandard ALL_SUPPORTED // nonstandard @@ -75,7 +76,7 @@ public: THEORY_ARRAYS_EX, THEORY_BITVECTORS, THEORY_BITVECTORS_32, - THEORY_BITVECTORS_ARRAYS_EX, + THEORY_BITVECTOR_ARRAYS_EX, THEORY_EMPTY, THEORY_INTS, THEORY_INT_ARRAYS, @@ -83,6 +84,7 @@ public: THEORY_INT_INT_REAL_ARRAY_ARRAYS_EX, THEORY_REALS, THEORY_REALS_INTS, + THEORY_QUANTIFIERS }; private: diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 7a7c7df62..59b6715b9 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -136,7 +136,10 @@ using namespace CVC4::parser; * @return the parsed expression, or the Null Expr if we've reached the end of the input */ parseExpr returns [CVC4::parser::smt2::myExpr expr] - : term[expr] +@declarations { + Expr expr2; +} + : term[expr, expr2] | EOF ; @@ -156,7 +159,7 @@ command returns [CVC4::Command* cmd = NULL] @declarations { std::string name; std::vector<std::string> names; - Expr expr; + Expr expr, expr2; Type t; std::vector<Expr> terms; std::vector<Type> sorts; @@ -258,7 +261,7 @@ command returns [CVC4::Command* cmd = NULL] terms.push_back(PARSER_STATE->mkVar((*i).first, (*i).second)); } } - term[expr] + term[expr, expr2] { PARSER_STATE->popScope(); // declare the name down here (while parsing term, signature // must not be extended with the name itself; no recursion @@ -287,7 +290,7 @@ command returns [CVC4::Command* cmd = NULL] { cmd = new GetAssignmentCommand; } | /* assertion */ ASSERT_TOK { PARSER_STATE->checkThatLogicIsSet(); } - term[expr] + term[expr, expr2] { cmd = new AssertCommand(expr); } | /* checksat */ CHECKSAT_TOK { PARSER_STATE->checkThatLogicIsSet(); } @@ -359,7 +362,7 @@ extendedCommand[CVC4::Command*& cmd] @declarations { std::vector<CVC4::Datatype> dts; Type t; - Expr e; + Expr e, e2; SExpr sexpr; std::string name; std::vector<std::string> names; @@ -420,7 +423,7 @@ symbolicExpr[CVC4::SExpr& sexpr] * Matches a term. * @return the expression representing the formula */ -term[CVC4::Expr& expr] +term[CVC4::Expr& expr, CVC4::Expr& expr2] @init { Debug("parser") << "term: " << AntlrInput::tokenText(LT(1)) << std::endl; Kind kind; @@ -428,6 +431,11 @@ term[CVC4::Expr& expr] std::string name; std::vector<Expr> args; SExpr sexpr; + std::vector< std::pair<std::string, Type> > sortedVarNames; + Expr f, f2; + std::string attr; + Expr attexpr; + std::vector<Expr> attexprs; } : /* a built-in operator application */ LPAREN_TOK builtinOp[kind] termList[args,expr] RPAREN_TOK @@ -456,10 +464,45 @@ term[CVC4::Expr& expr] expr = MK_EXPR(kind, args); } } - + | LPAREN_TOK quantOp[kind] + LPAREN_TOK sortedVarList[sortedVarNames] RPAREN_TOK + { + PARSER_STATE->pushScope(); + for(std::vector<std::pair<std::string, CVC4::Type> >::const_iterator i = + sortedVarNames.begin(), iend = sortedVarNames.end(); + i != iend; + ++i) { + args.push_back(PARSER_STATE->mkVar((*i).first, (*i).second)); + } + Expr bvl = MK_EXPR(kind::BOUND_VAR_LIST, args); + args.clear(); + args.push_back(bvl); + } + term[f, f2] RPAREN_TOK + { + PARSER_STATE->popScope(); + switch(f.getKind()) { + case CVC4::kind::RR_REWRITE: + case CVC4::kind::RR_REDUCTION: + case CVC4::kind::RR_DEDUCTION: + if(kind == CVC4::kind::EXISTS) { + PARSER_STATE->parseError("Use Exists instead of Forall for a rewrite rule."); + } + args.push_back(f2); // guards + args.push_back(f); // rule + expr = MK_EXPR(CVC4::kind::REWRITE_RULE, args); + break; + default: + args.push_back(f); + if(! f2.isNull()){ + args.push_back(f2); + } + expr = MK_EXPR(kind, args); + } + } | /* A non-built-in function application */ LPAREN_TOK - functionName[name,CHECK_DECLARED] + functionName[name, CHECK_DECLARED] { PARSER_STATE->checkFunctionLike(name); const bool isDefinedFunction = PARSER_STATE->isDefinedFunction(name); @@ -469,13 +512,13 @@ term[CVC4::Expr& expr] } else { expr = PARSER_STATE->getVariable(name); Type t = expr.getType(); - if( t.isConstructor() ){ + if(t.isConstructor()) { kind = CVC4::kind::APPLY_CONSTRUCTOR; - }else if( t.isSelector() ){ + } else if(t.isSelector()) { kind = CVC4::kind::APPLY_SELECTOR; - }else if( t.isTester() ){ + } else if(t.isTester()) { kind = CVC4::kind::APPLY_TESTER; - }else{ + } else { kind = CVC4::kind::APPLY_UF; } } @@ -494,10 +537,10 @@ term[CVC4::Expr& expr] | /* a let binding */ LPAREN_TOK LET_TOK LPAREN_TOK { PARSER_STATE->pushScope(); } - ( LPAREN_TOK symbol[name,CHECK_UNDECLARED,SYM_VARIABLE] term[expr] RPAREN_TOK + ( LPAREN_TOK symbol[name,CHECK_UNDECLARED,SYM_VARIABLE] term[expr, f2] RPAREN_TOK { PARSER_STATE->defineVar(name,expr); } )+ RPAREN_TOK - term[expr] + term[expr, f2] RPAREN_TOK { PARSER_STATE->popScope(); } @@ -519,26 +562,45 @@ term[CVC4::Expr& expr] } /* attributed expressions */ - | LPAREN_TOK ATTRIBUTE_TOK term[expr] KEYWORD symbolicExpr[sexpr] RPAREN_TOK - { std::string attr = AntlrInput::tokenText($KEYWORD); - if(attr == ":named") { - name = sexpr.getValue(); - // FIXME ensure expr is a closed subterm - // check that sexpr is a fresh function symbol - PARSER_STATE->checkDeclaration(name, CHECK_UNDECLARED, SYM_VARIABLE); - // define it - Expr func = PARSER_STATE->mkFunction(name, expr.getType()); - // bind name to expr with define-fun - Command* c = - new DefineNamedFunctionCommand(name, func, std::vector<Expr>(), expr); - PARSER_STATE->preemptCommand(c); - } else { - std::stringstream ss; - ss << "Attribute `" << attr << "' not supported"; - PARSER_STATE->parseError(ss.str()); + | LPAREN_TOK ATTRIBUTE_TOK term[expr, f2] + ( attribute[expr, attexpr,attr] + { if(! attexpr.isNull()) { + attexprs.push_back(attexpr); + } } - } + )+ RPAREN_TOK + { + if(attr == ":rewrite-rule") { + Expr guard; + Expr body; + if(expr[1].getKind() == kind::IMPLIES || + expr[1].getKind() == kind::IFF || + expr[1].getKind() == kind::EQUAL) { + guard = expr[0]; + body = expr[1]; + } else { + guard = MK_CONST(bool(true)); + body = expr; + } + expr2 = guard; + args.push_back(body[0]); + args.push_back(body[1]); + if(!f2.isNull()) { + args.push_back(f2); + } + + if ( body.getKind()==kind::IMPLIES ) kind = kind::RR_DEDUCTION; + else if( body.getKind()==kind::IFF ) kind = kind::RR_REDUCTION; + else if( body.getKind()==kind::EQUAL ) kind = kind::RR_REWRITE; + else PARSER_STATE->parseError("Error parsing rewrite rule."); + expr = MK_EXPR( kind, args ); + } else if(! attexprs.empty()) { + if(attexprs[0].getKind() == kind::INST_PATTERN) { + expr2 = MK_EXPR(kind::INST_PATTERN_LIST, attexprs); + } + } + } /* constants */ | INTEGER_LITERAL { expr = MK_CONST( AntlrInput::tokenToInteger($INTEGER_LITERAL) ); } @@ -570,6 +632,46 @@ term[CVC4::Expr& expr] ; /** + * Read attribute + */ +attribute[CVC4::Expr& expr,CVC4::Expr& retExpr, std::string& attr] +@init { + SExpr sexpr; + Expr patexpr; + std::vector<Expr> patexprs; + Expr e2; +} +: KEYWORD + { attr = AntlrInput::tokenText($KEYWORD); } + symbolicExpr[sexpr] + { if(attr == ":named") { + std::string name = sexpr.getValue(); + // FIXME ensure expr is a closed subterm + // check that sexpr is a fresh function symbol + PARSER_STATE->checkDeclaration(name, CHECK_UNDECLARED, SYM_VARIABLE); + // define it + Expr func = PARSER_STATE->mkFunction(name, expr.getType()); + // bind name to expr with define-fun + Command* c = + new DefineNamedFunctionCommand(name, func, std::vector<Expr>(), expr); + PARSER_STATE->preemptCommand(c); + } else { + std::stringstream ss; + ss << "Attribute `" << attr << "' not supported"; + PARSER_STATE->parseError(ss.str()); + } + } + | ATTRIBUTE_PATTERN_TOK LPAREN_TOK ( term[patexpr, e2] { patexprs.push_back( patexpr ); } )+ RPAREN_TOK + { + attr = std::string(":pattern"); + retExpr = MK_EXPR(kind::INST_PATTERN, patexprs); + } + | ATTRIBUTE_REWRITE_RULE { + attr = std::string(":rewrite-rule"); + } + ; + +/** * Matches a bit-vector operator (the ones parametrized by numbers) */ indexedFunctionName[CVC4::Expr& op] @@ -613,7 +715,10 @@ badIndexedFunctionName /* NOTE: We pass an Expr in here just to avoid allocating a fresh Expr every * time through this rule. */ termList[std::vector<CVC4::Expr>& formulas, CVC4::Expr& expr] - : ( term[expr] { formulas.push_back(expr); } )+ +@declarations { + Expr expr2; +} + : ( term[expr, expr2] { formulas.push_back(expr); } )+ ; /** @@ -693,6 +798,14 @@ builtinOp[CVC4::Kind& kind] // NOTE: Theory operators go here ; +quantOp[CVC4::Kind& kind] +@init { + Debug("parser") << "quant: " << AntlrInput::tokenText(LT(1)) << std::endl; +} + : EXISTS_TOK { $kind = CVC4::kind::EXISTS; } + | FORALL_TOK { $kind = CVC4::kind::FORALL; } + ; + /** * Matches a (possibly undeclared) function symbol (returning the string) * @param check what kind of check to do with the symbol @@ -760,12 +873,12 @@ sortSymbol[CVC4::Type& t, CVC4::parser::DeclarationCheck check] std::vector<uint64_t> numerals; } : sortName[name,CHECK_NONE] - { - if( check == CHECK_DECLARED || PARSER_STATE->isDeclared(name, SYM_SORT) ){ - t = PARSER_STATE->getSort(name); - }else{ - t = PARSER_STATE->mkUnresolvedType(name); - } + { + if( check == CHECK_DECLARED || PARSER_STATE->isDeclared(name, SYM_SORT) ){ + t = PARSER_STATE->getSort(name); + }else{ + t = PARSER_STATE->mkUnresolvedType(name); + } } | LPAREN_TOK INDEX_TOK symbol[name,CHECK_NONE,SYM_SORT] nonemptyNumeralList[numerals] RPAREN_TOK { @@ -929,6 +1042,10 @@ POP_TOK : 'pop'; DECLARE_DATATYPES_TOK : 'declare-datatypes'; ECHO_TOK : 'echo'; +// attributes +ATTRIBUTE_PATTERN_TOK : ':pattern'; +ATTRIBUTE_REWRITE_RULE : ':rewrite-rule'; + // operators (NOTE: theory symbols go here) AMPERSAND_TOK : '&'; AND_TOK : 'and'; diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index 709ba087f..549878e46 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -86,6 +86,9 @@ void Smt2::addTheory(Theory theory) { case THEORY_BITVECTORS: break; + case THEORY_QUANTIFIERS: + break; + default: Unhandled(theory); } @@ -195,6 +198,7 @@ void Smt2::setLogic(const std::string& name) { break; case Smt::ALL_SUPPORTED: + addTheory(THEORY_QUANTIFIERS); /* fall through */ case Smt::QF_ALL_SUPPORTED: addTheory(THEORY_ARRAYS); @@ -208,11 +212,25 @@ void Smt2::setLogic(const std::string& name) { case Smt::AUFLIRA: case Smt::AUFNIRA: case Smt::LRA: - case Smt::UFLRA: case Smt::UFNIA: - Unhandled(name); + case Smt::UFNIRA: + case Smt::UFLRA: + if(d_logic != Smt::AUFLIA && d_logic != Smt::UFNIA) { + addTheory(THEORY_REALS); + } + if(d_logic != Smt::LRA) { + addOperator(kind::APPLY_UF); + if(d_logic != Smt::UFLRA) { + addTheory(THEORY_INTS); + if(d_logic != Smt::UFNIA && d_logic != Smt::UFNIRA) { + addTheory(THEORY_ARRAYS); + } + } + } + addTheory(THEORY_QUANTIFIERS); + break; } -} +}/* Smt2::setLogic() */ void Smt2::setInfo(const std::string& flag, const SExpr& sexpr) { // TODO: ??? diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h index b71f63558..9d33e3e62 100644 --- a/src/parser/smt2/smt2.h +++ b/src/parser/smt2/smt2.h @@ -41,6 +41,7 @@ public: THEORY_INTS, THEORY_REALS, THEORY_REALS_INTS, + THEORY_QUANTIFIERS, }; private: |