diff options
Diffstat (limited to 'src/parser/smt2')
-rw-r--r-- | src/parser/smt2/Smt2.g | 588 | ||||
-rw-r--r-- | src/parser/smt2/smt2.cpp | 980 | ||||
-rw-r--r-- | src/parser/smt2/smt2.h | 166 | ||||
-rw-r--r-- | src/parser/smt2/smt2_input.cpp | 2 | ||||
-rw-r--r-- | src/parser/smt2/sygus_input.cpp | 2 |
5 files changed, 892 insertions, 846 deletions
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 9ae9f7261..cd661364d 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -87,24 +87,26 @@ using namespace CVC4::parser; namespace CVC4 { class Expr; + namespace api { + class Term; + class Sort; + } + namespace parser { namespace smt2 { /** * Just exists to provide the uintptr_t constructor that ANTLR * requires. */ - struct myExpr : public CVC4::Expr { - myExpr() : CVC4::Expr() {} - myExpr(void*) : CVC4::Expr() {} - myExpr(const Expr& e) : CVC4::Expr(e) {} - myExpr(const myExpr& e) : CVC4::Expr(e) {} + struct myExpr : public CVC4::api::Term { + myExpr() : CVC4::api::Term() {} + myExpr(void*) : CVC4::api::Term() {} + myExpr(const Expr& e) : CVC4::api::Term(e) {} + myExpr(const myExpr& e) : CVC4::api::Term(e) {} };/* struct myExpr */ }/* CVC4::parser::smt2 namespace */ }/* CVC4::parser namespace */ - namespace api { - class Term; - } }/* CVC4 namespace */ }/* @parser::includes */ @@ -141,14 +143,10 @@ using namespace CVC4::parser; * PARSER would be undefined.) */ #undef PARSER_STATE #define PARSER_STATE ((Smt2*)PARSER->super) -#undef EXPR_MANAGER -#define EXPR_MANAGER PARSER_STATE->getExprManager() -#undef MK_EXPR -#define MK_EXPR EXPR_MANAGER->mkExpr -#undef MK_CONST -#define MK_CONST EXPR_MANAGER->mkConst #undef SOLVER #define SOLVER PARSER_STATE->getSolver() +#undef MK_TERM +#define MK_TERM SOLVER->mkTerm #define UNSUPPORTED PARSER_STATE->unimplementedFeature }/* parser::postinclude */ @@ -160,7 +158,7 @@ using namespace CVC4::parser; */ parseExpr returns [CVC4::parser::smt2::myExpr expr] @declarations { - Expr expr2; + CVC4::api::Term expr2; } : term[expr, expr2] | EOF @@ -225,12 +223,12 @@ command [std::unique_ptr<CVC4::Command>* cmd] @declarations { std::string name; std::vector<std::string> names; - Expr expr, expr2; - Type t; - std::vector<Expr> terms; - std::vector<Type> sorts; - std::vector<std::pair<std::string, Type> > sortedVarNames; - std::vector<Expr> flattenVars; + CVC4::api::Term expr, expr2; + CVC4::api::Sort t; + std::vector<CVC4::api::Term> terms; + std::vector<api::Sort> sorts; + std::vector<std::pair<std::string, CVC4::api::Sort> > sortedVarNames; + std::vector<CVC4::api::Term> flattenVars; } : /* set the logic */ SET_LOGIC_TOK symbol[name,CHECK_NONE,SYM_SORT] @@ -267,11 +265,11 @@ command [std::unique_ptr<CVC4::Command>* cmd] << "' arity=" << n << std::endl; unsigned arity = AntlrInput::tokenToUnsigned(n); if(arity == 0) { - Type type = PARSER_STATE->mkSort(name); - cmd->reset(new DeclareTypeCommand(name, 0, type)); + api::Sort type = PARSER_STATE->mkSort(name); + cmd->reset(new DeclareTypeCommand(name, 0, type.getType())); } else { - Type type = PARSER_STATE->mkSortConstructor(name, arity); - cmd->reset(new DeclareTypeCommand(name, arity, type)); + api::Sort type = PARSER_STATE->mkSortConstructor(name, arity); + cmd->reset(new DeclareTypeCommand(name, arity, type.getType())); } } | /* sort definition */ @@ -291,8 +289,9 @@ command [std::unique_ptr<CVC4::Command>* cmd] { PARSER_STATE->popScope(); // Do NOT call mkSort, since that creates a new sort! // This name is not its own distinct sort, it's an alias. - PARSER_STATE->defineParameterizedType(name, sorts, t); - cmd->reset(new DefineTypeCommand(name, sorts, t)); + PARSER_STATE->defineParameterizedType(name, sorts, t.getType()); + cmd->reset(new DefineTypeCommand( + name, api::sortVectorToTypes(sorts), t.getType())); } | /* function declaration */ DECLARE_FUN_TOK { PARSER_STATE->checkThatLogicIsSet(); } @@ -315,8 +314,9 @@ command [std::unique_ptr<CVC4::Command>* cmd] if (PARSER_STATE->sygus_v1()) { // it is a higher-order universal variable - Expr func = PARSER_STATE->mkBoundVar(name, t); - cmd->reset(new DeclareSygusFunctionCommand(name, func, t)); + api::Term func = PARSER_STATE->bindBoundVar(name, t); + cmd->reset( + new DeclareSygusFunctionCommand(name, func.getExpr(), t.getType())); } else if( PARSER_STATE->sygus() ) { @@ -325,8 +325,10 @@ command [std::unique_ptr<CVC4::Command>* cmd] } else { - Expr func = PARSER_STATE->mkVar(name, t, ExprManager::VAR_FLAG_NONE, true); - cmd->reset(new DeclareFunctionCommand(name, func, t)); + api::Term func = + PARSER_STATE->bindVar(name, t, ExprManager::VAR_FLAG_NONE, true); + cmd->reset( + new DeclareFunctionCommand(name, func.getExpr(), t.getType())); } } | /* function definition */ @@ -339,7 +341,7 @@ command [std::unique_ptr<CVC4::Command>* cmd] Debug("parser") << "define fun: '" << name << "'" << std::endl; if( sortedVarNames.size() > 0 ) { sorts.reserve(sortedVarNames.size()); - for(std::vector<std::pair<std::string, CVC4::Type> >::const_iterator i = + for(std::vector<std::pair<std::string, api::Sort> >::const_iterator i = sortedVarNames.begin(), iend = sortedVarNames.end(); i != iend; ++i) { @@ -348,7 +350,7 @@ command [std::unique_ptr<CVC4::Command>* cmd] t = PARSER_STATE->mkFlatFunctionType(sorts, t, flattenVars); } PARSER_STATE->pushScope(true); - terms = PARSER_STATE->mkBoundVars(sortedVarNames); + terms = PARSER_STATE->bindBoundVars(sortedVarNames); } term[expr, expr2] { @@ -363,16 +365,17 @@ command [std::unique_ptr<CVC4::Command>* cmd] // must not be extended with the name itself; no recursion // permitted) // we allow overloading for function definitions - Expr func = PARSER_STATE->mkVar(name, t, + api::Term func = PARSER_STATE->bindVar(name, t, ExprManager::VAR_FLAG_DEFINED, true); - cmd->reset(new DefineFunctionCommand(name, func, terms, expr)); + cmd->reset(new DefineFunctionCommand( + name, func.getExpr(), api::termVectorToExprs(terms), expr.getExpr())); } | DECLARE_DATATYPE_TOK datatypeDefCommand[false, cmd] | DECLARE_DATATYPES_TOK datatypesDefCommand[false, cmd] | /* value query */ GET_VALUE_TOK { PARSER_STATE->checkThatLogicIsSet(); } ( LPAREN_TOK termList[terms,expr] RPAREN_TOK - { cmd->reset(new GetValueCommand(terms)); } + { cmd->reset(new GetValueCommand(api::termVectorToExprs(terms))); } | ~LPAREN_TOK { PARSER_STATE->parseError("The get-value command expects a list of " "terms. Perhaps you forgot a pair of " @@ -387,11 +390,13 @@ command [std::unique_ptr<CVC4::Command>* cmd] { PARSER_STATE->clearLastNamedTerm(); } term[expr, expr2] { bool inUnsatCore = PARSER_STATE->lastNamedTerm().first == expr; - cmd->reset(new AssertCommand(expr, inUnsatCore)); + cmd->reset(new AssertCommand(expr.getExpr(), inUnsatCore)); if(inUnsatCore) { // set the expression name, if there was a named term - std::pair<Expr, std::string> namedTerm = PARSER_STATE->lastNamedTerm(); - Command* csen = new SetExpressionNameCommand(namedTerm.first, namedTerm.second); + std::pair<api::Term, std::string> namedTerm = + PARSER_STATE->lastNamedTerm(); + Command* csen = new SetExpressionNameCommand(namedTerm.first.getExpr(), + namedTerm.second); csen->setMuted(true); PARSER_STATE->preemptCommand(csen); } @@ -409,13 +414,15 @@ command [std::unique_ptr<CVC4::Command>* cmd] "permitted while operating in strict compliance mode."); } } - | { expr = Expr(); } + | { expr = api::Term(); } ) - { cmd->reset(new CheckSatCommand(expr)); } + { cmd->reset(new CheckSatCommand(expr.getExpr())); } | /* check-sat-assuming */ CHECK_SAT_ASSUMING_TOK { PARSER_STATE->checkThatLogicIsSet(); } ( LPAREN_TOK termList[terms,expr] RPAREN_TOK - { cmd->reset(new CheckSatAssumingCommand(terms)); } + { + cmd->reset(new CheckSatAssumingCommand(api::termVectorToExprs(terms))); + } | ~LPAREN_TOK { PARSER_STATE->parseError("The check-sat-assuming command expects a " "list of terms. Perhaps you forgot a pair of " @@ -544,14 +551,14 @@ command [std::unique_ptr<CVC4::Command>* cmd] sygusCommand returns [std::unique_ptr<CVC4::Command> cmd] @declarations { - Expr expr, expr2; - Type t, range; + CVC4::api::Term expr, expr2; + CVC4::api::Sort t, range; std::vector<std::string> names; - std::vector<std::pair<std::string, Type> > sortedVarNames; + std::vector<std::pair<std::string, CVC4::api::Sort> > sortedVarNames; std::unique_ptr<Smt2::SynthFunFactory> synthFunFactory; std::string name, fun; bool isInv; - Type grammar; + CVC4::api::Sort grammar; } : /* declare-var */ DECLARE_VAR_TOK { PARSER_STATE->checkThatLogicIsSet(); } @@ -559,8 +566,8 @@ sygusCommand returns [std::unique_ptr<CVC4::Command> cmd] { PARSER_STATE->checkUserSymbol(name); } sortSymbol[t,CHECK_DECLARED] { - Expr var = PARSER_STATE->mkBoundVar(name, t); - cmd.reset(new DeclareSygusVarCommand(name, var, t)); + api::Term var = PARSER_STATE->bindBoundVar(name, t); + cmd.reset(new DeclareSygusVarCommand(name, var.getExpr(), t.getType())); } | /* declare-primed-var */ DECLARE_PRIMED_VAR_TOK { PARSER_STATE->checkThatLogicIsSet(); } @@ -570,12 +577,12 @@ sygusCommand returns [std::unique_ptr<CVC4::Command> cmd] { // spurious command, we do not need to create a variable. We only keep // track of the command for sanity checking / dumping - cmd.reset(new DeclareSygusPrimedVarCommand(name, t)); + cmd.reset(new DeclareSygusPrimedVarCommand(name, t.getType())); } | /* synth-fun */ ( SYNTH_FUN_V1_TOK { isInv = false; } - | SYNTH_INV_V1_TOK { isInv = true; range = EXPR_MANAGER->booleanType(); } + | SYNTH_INV_V1_TOK { isInv = true; range = SOLVER->getBooleanSort(); } ) { PARSER_STATE->checkThatLogicIsSet(); } symbol[fun,CHECK_UNDECLARED,SYM_VARIABLE] @@ -597,7 +604,7 @@ sygusCommand returns [std::unique_ptr<CVC4::Command> cmd] } | /* synth-fun */ ( SYNTH_FUN_TOK { isInv = false; } - | SYNTH_INV_TOK { isInv = true; range = EXPR_MANAGER->booleanType(); } + | SYNTH_INV_TOK { isInv = true; range = SOLVER->getBooleanSort(); } ) { PARSER_STATE->checkThatLogicIsSet(); } symbol[fun,CHECK_UNDECLARED,SYM_VARIABLE] @@ -625,7 +632,7 @@ sygusCommand returns [std::unique_ptr<CVC4::Command> cmd] } term[expr, expr2] { Debug("parser-sygus") << "...read constraint " << expr << std::endl; - cmd.reset(new SygusConstraintCommand(expr)); + cmd.reset(new SygusConstraintCommand(expr.getExpr())); } | /* inv-constraint */ INV_CONSTRAINT_TOK @@ -651,24 +658,24 @@ sygusCommand returns [std::unique_ptr<CVC4::Command> cmd] * The argument fun is a unique identifier to avoid naming clashes for the * datatypes constructed by this call. */ -sygusGrammarV1[CVC4::Type & ret, - const std::vector<CVC4::Expr>& sygus_vars, +sygusGrammarV1[CVC4::api::Sort & ret, + const std::vector<CVC4::api::Term>& sygus_vars, const std::string& fun] @declarations { - Type t; + CVC4::api::Sort t; std::string name; unsigned startIndex = 0; std::vector<std::vector<CVC4::SygusGTerm>> sgts; std::vector<CVC4::Datatype> datatypes; - std::vector<Type> sorts; + std::vector<api::Sort> sorts; std::vector<std::vector<ParseOp>> ops; std::vector<std::vector<std::string>> cnames; - std::vector<std::vector<std::vector<CVC4::Type>>> cargs; + std::vector<std::vector<std::vector<CVC4::api::Sort>>> cargs; std::vector<bool> allow_const; std::vector<std::vector<std::string>> unresolved_gterm_sym; - std::map<CVC4::Type, CVC4::Type> sygus_to_builtin; - std::map<CVC4::Type, CVC4::Expr> sygus_to_builtin_expr; + std::map<CVC4::api::Sort, CVC4::api::Sort> sygus_to_builtin; + std::map<CVC4::api::Sort, CVC4::api::Term> sygus_to_builtin_expr; } : LPAREN_TOK { PARSER_STATE->pushScope(); } (LPAREN_TOK @@ -688,7 +695,7 @@ sygusGrammarV1[CVC4::Type & ret, cargs, allow_const, unresolved_gterm_sym); - Type unres_t; + api::Sort unres_t; if (!PARSER_STATE->isUnresolvedType(name)) { // if not unresolved, must be undeclared @@ -724,7 +731,7 @@ sygusGrammarV1[CVC4::Type & ret, { for (unsigned j = 0, size = sgts[i].size(); j < size; j++) { - Type sub_ret; + api::Sort sub_ret; PARSER_STATE->processSygusGTerm(sgts[i][j], i, datatypes, @@ -748,10 +755,10 @@ sygusGrammarV1[CVC4::Type & ret, Debug("parser-sygus") << "..." << datatypes[i].getName() << " has builtin sort " << sorts[i] << std::endl; } - Expr bvl; + api::Term bvl; if (!sygus_vars.empty()) { - bvl = MK_EXPR(kind::BOUND_VAR_LIST, sygus_vars); + bvl = MK_TERM(api::BOUND_VAR_LIST, sygus_vars); } for (unsigned i = 0; i < ndatatypes; i++) { @@ -763,7 +770,8 @@ sygusGrammarV1[CVC4::Type & ret, "Internal error : could not infer " "builtin sort for nested gterm."); } - datatypes[i].setSygus(sorts[i], bvl, allow_const[i], false); + datatypes[i].setSygus( + sorts[i].getType(), bvl.getExpr(), allow_const[i], false); PARSER_STATE->mkSygusDatatype(datatypes[i], ops[i], cnames[i], @@ -796,10 +804,10 @@ sygusGrammarV1[CVC4::Type & ret, sygusGTerm[CVC4::SygusGTerm& sgt, const std::string& fun] @declarations { std::string name, name2; - Kind k; - Type t; + CVC4::api::Kind k; + CVC4::api::Sort t; std::string sname; - std::vector< Expr > let_vars; + std::vector< CVC4::api::Term > let_vars; std::string s; CVC4::api::Term atomTerm; } @@ -833,7 +841,7 @@ sygusGTerm[CVC4::SygusGTerm& sgt, const std::string& fun] Debug("parser-sygus") << "Sygus grammar " << fun << " : builtin op : " << name << std::endl; k = PARSER_STATE->getOperatorKind(name); - sgt.d_name = kind::kindToString(k); + sgt.d_name = api::kindToString(k); sgt.d_gterm_type = SygusGTerm::gterm_op; sgt.d_op.d_kind = k; }else{ @@ -886,7 +894,7 @@ sygusGTerm[CVC4::SygusGTerm& sgt, const std::string& fun] Debug("parser-sygus") << "Sygus grammar " << fun << " : unary minus integer literal " << name << std::endl; - sgt.d_op.d_expr = MK_CONST(Rational(name)); + sgt.d_op.d_expr = SOLVER->mkReal(name); sgt.d_name = name; sgt.d_gterm_type = SygusGTerm::gterm_op; }else if( PARSER_STATE->isDeclared(name,SYM_VARIABLE) ){ @@ -922,21 +930,21 @@ sygusGTerm[CVC4::SygusGTerm& sgt, const std::string& fun] * The argument fun is a unique identifier to avoid naming clashes for the * datatypes constructed by this call. */ -sygusGrammar[CVC4::Type & ret, - const std::vector<CVC4::Expr>& sygusVars, +sygusGrammar[CVC4::api::Sort & ret, + const std::vector<CVC4::api::Term>& sygusVars, const std::string& fun] @declarations { // the pre-declaration - std::vector<std::pair<std::string, Type> > sortedVarNames; + std::vector<std::pair<std::string, CVC4::api::Sort> > sortedVarNames; // non-terminal symbols of the grammar - std::vector<Expr> ntSyms; - Type t; + std::vector<CVC4::api::Term> ntSyms; + CVC4::api::Sort t; std::string name; - Expr e, e2; + CVC4::api::Term e, e2; std::vector<CVC4::Datatype> datatypes; - std::vector<Type> unresTypes; - std::map<Expr, CVC4::Type> ntsToUnres; + std::vector<api::Sort> unresTypes; + std::map<CVC4::api::Term, CVC4::api::Sort> ntsToUnres; unsigned dtProcessed = 0; std::unordered_set<unsigned> allowConst; } @@ -946,20 +954,20 @@ sygusGrammar[CVC4::Type & ret, { // non-terminal symbols in the pre-declaration are locally scoped PARSER_STATE->pushScope(true); - for (std::pair<std::string, CVC4::Type>& i : sortedVarNames) + for (std::pair<std::string, api::Sort>& i : sortedVarNames) { Trace("parser-sygus2") << "Declare datatype " << i.first << std::endl; // make the datatype, which encodes terms generated by this non-terminal std::string dname = i.first; - datatypes.push_back(Datatype(EXPR_MANAGER, dname)); + datatypes.push_back(Datatype(PARSER_STATE->getExprManager(), dname)); // make its unresolved type, used for referencing the final version of // the datatype PARSER_STATE->checkDeclaration(dname, CHECK_UNDECLARED, SYM_SORT); - Type urt = PARSER_STATE->mkUnresolvedType(dname); + api::Sort urt = PARSER_STATE->mkUnresolvedType(dname); unresTypes.push_back(urt); // make the non-terminal symbol, which will be parsed as an ordinary // free variable. - Expr nts = PARSER_STATE->mkBoundVar(i.first, i.second); + api::Term nts = PARSER_STATE->bindBoundVar(i.first, i.second); ntSyms.push_back(nts); ntsToUnres[nts] = urt; } @@ -1019,17 +1027,17 @@ sygusGrammar[CVC4::Type & ret, "Number of grouped rule listings does not match " "number of symbols in predeclaration."); } - Expr bvl; + api::Term bvl; if (!sygusVars.empty()) { - bvl = MK_EXPR(kind::BOUND_VAR_LIST, sygusVars); + bvl = MK_TERM(api::BOUND_VAR_LIST, sygusVars); } Trace("parser-sygus2") << "Process " << dtProcessed << " sygus datatypes..." << std::endl; for (unsigned i = 0; i < dtProcessed; i++) { bool aci = allowConst.find(i)!=allowConst.end(); - Type btt = sortedVarNames[i].second; - datatypes[i].setSygus(btt, bvl, aci, false); + api::Sort btt = sortedVarNames[i].second; + datatypes[i].setSygus(btt.getType(), bvl.getExpr(), aci, false); Trace("parser-sygus2") << "- " << datatypes[i].getName() << ", #cons= " << datatypes[i].getNumConstructors() << ", aci= " << aci << std::endl; @@ -1089,21 +1097,22 @@ smt25Command[std::unique_ptr<CVC4::Command>* cmd] @declarations { std::string name; std::string fname; - Expr expr, expr2; - std::vector<std::pair<std::string, Type> > sortedVarNames; + CVC4::api::Term expr, expr2; + std::vector<std::pair<std::string, CVC4::api::Sort> > sortedVarNames; SExpr sexpr; - Type t; - Expr func; - std::vector<Expr> bvs; - std::vector< std::vector<std::pair<std::string, Type> > > sortedVarNamesList; - std::vector<std::vector<Expr>> flattenVarsList; - std::vector<std::vector<Expr>> formals; - std::vector<Expr> funcs; - std::vector<Expr> func_defs; - Expr aexpr; + CVC4::api::Sort t; + CVC4::api::Term func; + std::vector<CVC4::api::Term> bvs; + std::vector<std::vector<std::pair<std::string, CVC4::api::Sort>>> + sortedVarNamesList; + std::vector<std::vector<CVC4::api::Term>> flattenVarsList; + std::vector<std::vector<CVC4::api::Term>> formals; + std::vector<CVC4::api::Term> funcs; + std::vector<CVC4::api::Term> func_defs; + CVC4::api::Term aexpr; std::unique_ptr<CVC4::CommandSequence> seq; - std::vector<Type> sorts; - std::vector<Expr> flattenVars; + std::vector<api::Sort> sorts; + std::vector<CVC4::api::Term> flattenVars; } /* declare-const */ : DECLARE_CONST_TOK { PARSER_STATE->checkThatLogicIsSet(); } @@ -1111,8 +1120,9 @@ smt25Command[std::unique_ptr<CVC4::Command>* cmd] { PARSER_STATE->checkUserSymbol(name); } sortSymbol[t,CHECK_DECLARED] { // allow overloading here - Expr c = PARSER_STATE->mkVar(name, t, ExprManager::VAR_FLAG_NONE, true); - cmd->reset(new DeclareFunctionCommand(name, c, t)); } + api::Term c = + PARSER_STATE->bindVar(name, t, ExprManager::VAR_FLAG_NONE, true); + cmd->reset(new DeclareFunctionCommand(name, c.getExpr(), t.getType())); } /* get model */ | GET_MODEL_TOK { PARSER_STATE->checkThatLogicIsSet(); } @@ -1144,15 +1154,18 @@ smt25Command[std::unique_ptr<CVC4::Command>* cmd] LPAREN_TOK sortedVarList[sortedVarNames] RPAREN_TOK sortSymbol[t,CHECK_DECLARED] { - func = PARSER_STATE->mkDefineFunRec(fname, sortedVarNames, t, flattenVars); - PARSER_STATE->pushDefineFunRecScope(sortedVarNames, func, flattenVars, bvs, true ); + func = + PARSER_STATE->bindDefineFunRec(fname, sortedVarNames, t, flattenVars); + PARSER_STATE->pushDefineFunRecScope( + sortedVarNames, func, flattenVars, bvs, true); } term[expr, expr2] { PARSER_STATE->popScope(); if( !flattenVars.empty() ){ expr = PARSER_STATE->mkHoApply( expr, flattenVars ); } - cmd->reset(new DefineFunctionRecCommand(func,bvs,expr)); + cmd->reset(new DefineFunctionRecCommand( + func.getExpr(), api::termVectorToExprs(bvs), expr.getExpr())); } | DEFINE_FUNS_REC_TOK { PARSER_STATE->checkThatLogicIsSet();} @@ -1164,7 +1177,8 @@ smt25Command[std::unique_ptr<CVC4::Command>* cmd] sortSymbol[t,CHECK_DECLARED] { flattenVars.clear(); - func = PARSER_STATE->mkDefineFunRec( fname, sortedVarNames, t, flattenVars ); + func = PARSER_STATE->bindDefineFunRec( + fname, sortedVarNames, t, flattenVars); funcs.push_back( func ); // add to lists (need to remember for when parsing the bodies) @@ -1214,20 +1228,28 @@ smt25Command[std::unique_ptr<CVC4::Command>* cmd] "Number of functions defined does not match number listed in " "define-funs-rec")); } - cmd->reset( new DefineFunctionRecCommand(funcs,formals,func_defs)); + std::vector<std::vector<Expr>> eformals; + for (unsigned i=0, fsize = formals.size(); i<fsize; i++) + { + eformals.push_back(api::termVectorToExprs(formals[i])); + } + cmd->reset( + new DefineFunctionRecCommand(api::termVectorToExprs(funcs), + eformals, + api::termVectorToExprs(func_defs))); } ; extendedCommand[std::unique_ptr<CVC4::Command>* cmd] @declarations { std::vector<CVC4::Datatype> dts; - Expr e, e2; - Type t; + CVC4::api::Term e, e2; + CVC4::api::Sort t; std::string name; std::vector<std::string> names; - std::vector<Expr> terms; - std::vector<Type> sorts; - std::vector<std::pair<std::string, Type> > sortedVarNames; + std::vector<CVC4::api::Term> terms; + std::vector<api::Sort> sorts; + std::vector<std::pair<std::string, CVC4::api::Sort> > sortedVarNames; std::unique_ptr<CVC4::CommandSequence> seq; } /* Extended SMT-LIB set of commands syntax, not permitted in @@ -1236,6 +1258,7 @@ extendedCommand[std::unique_ptr<CVC4::Command>* cmd] | DECLARE_CODATATYPES_2_5_TOK datatypes_2_5_DefCommand[true, cmd] | DECLARE_CODATATYPE_TOK datatypeDefCommand[true, cmd] | DECLARE_CODATATYPES_TOK datatypesDefCommand[true, cmd] + /* Support some of Z3's extended SMT-LIB commands */ | DECLARE_SORTS_TOK { PARSER_STATE->checkThatLogicIsSet(); } @@ -1250,8 +1273,8 @@ extendedCommand[std::unique_ptr<CVC4::Command>* cmd] LPAREN_TOK ( symbol[name,CHECK_UNDECLARED,SYM_SORT] { PARSER_STATE->checkUserSymbol(name); - Type type = PARSER_STATE->mkSort(name); - seq->addCommand(new DeclareTypeCommand(name, 0, type)); + api::Sort type = PARSER_STATE->mkSort(name); + seq->addCommand(new DeclareTypeCommand(name, 0, type.getType())); } )+ RPAREN_TOK @@ -1263,7 +1286,7 @@ extendedCommand[std::unique_ptr<CVC4::Command>* cmd] ( LPAREN_TOK symbol[name,CHECK_UNDECLARED,SYM_VARIABLE] { PARSER_STATE->checkUserSymbol(name); } nonemptySortList[sorts] RPAREN_TOK - { Type tt; + { api::Sort tt; if(sorts.size() > 1) { if(!PARSER_STATE->isTheoryEnabled(Smt2::THEORY_UF)) { PARSER_STATE->parseError( @@ -1273,15 +1296,17 @@ extendedCommand[std::unique_ptr<CVC4::Command>* cmd] + " unless option --uf-ho is used"); } // must flatten - Type range = sorts.back(); + api::Sort range = sorts.back(); sorts.pop_back(); tt = PARSER_STATE->mkFlatFunctionType(sorts, range); } else { tt = sorts[0]; } // allow overloading - Expr func = PARSER_STATE->mkVar(name, tt, ExprManager::VAR_FLAG_NONE, true); - seq->addCommand(new DeclareFunctionCommand(name, func, tt)); + api::Term func = + PARSER_STATE->bindVar(name, tt, ExprManager::VAR_FLAG_NONE, true); + seq->addCommand( + new DeclareFunctionCommand(name, func.getExpr(), tt.getType())); sorts.clear(); } )+ @@ -1293,7 +1318,7 @@ extendedCommand[std::unique_ptr<CVC4::Command>* cmd] ( LPAREN_TOK symbol[name,CHECK_UNDECLARED,SYM_VARIABLE] { PARSER_STATE->checkUserSymbol(name); } sortList[sorts] RPAREN_TOK - { Type boolType = EXPR_MANAGER->booleanType(); + { t = SOLVER->getBooleanSort(); if(sorts.size() > 0) { if(!PARSER_STATE->isTheoryEnabled(Smt2::THEORY_UF)) { PARSER_STATE->parseError( @@ -1302,11 +1327,13 @@ extendedCommand[std::unique_ptr<CVC4::Command>* cmd] + PARSER_STATE->getLogic().getLogicString() + " unless option --uf-ho is used"); } - boolType = EXPR_MANAGER->mkFunctionType(sorts, boolType); + t = SOLVER->mkFunctionSort(sorts, t); } // allow overloading - Expr func = PARSER_STATE->mkVar(name, boolType, ExprManager::VAR_FLAG_NONE, true); - seq->addCommand(new DeclareFunctionCommand(name, func, boolType)); + api::Term func = + PARSER_STATE->bindVar(name, t, ExprManager::VAR_FLAG_NONE, true); + seq->addCommand( + new DeclareFunctionCommand(name, func.getExpr(), t.getType())); sorts.clear(); } )+ @@ -1317,9 +1344,9 @@ extendedCommand[std::unique_ptr<CVC4::Command>* cmd] ( symbol[name,CHECK_UNDECLARED,SYM_VARIABLE] { PARSER_STATE->checkUserSymbol(name); } term[e,e2] - { Expr func = PARSER_STATE->mkVar(name, e.getType(), + { api::Term func = PARSER_STATE->bindVar(name, e.getSort(), ExprManager::VAR_FLAG_DEFINED); - cmd->reset(new DefineFunctionCommand(name, func, e)); + cmd->reset(new DefineFunctionCommand(name, func.getExpr(), e.getExpr())); } | LPAREN_TOK symbol[name,CHECK_UNDECLARED,SYM_VARIABLE] @@ -1328,27 +1355,27 @@ extendedCommand[std::unique_ptr<CVC4::Command>* cmd] { /* add variables to parser state before parsing term */ Debug("parser") << "define fun: '" << name << "'" << std::endl; PARSER_STATE->pushScope(true); - terms = PARSER_STATE->mkBoundVars(sortedVarNames); + terms = PARSER_STATE->bindBoundVars(sortedVarNames); } term[e,e2] { PARSER_STATE->popScope(); // declare the name down here (while parsing term, signature // must not be extended with the name itself; no recursion // permitted) - Type tt = e.getType(); + api::Sort tt = e.getSort(); if( sortedVarNames.size() > 0 ) { - std::vector<CVC4::Type> types; - types.reserve(sortedVarNames.size()); - for(std::vector<std::pair<std::string, CVC4::Type> >::const_iterator + sorts.reserve(sortedVarNames.size()); + for(std::vector<std::pair<std::string, api::Sort> >::const_iterator i = sortedVarNames.begin(), iend = sortedVarNames.end(); i != iend; ++i) { - types.push_back((*i).second); + sorts.push_back((*i).second); } - tt = EXPR_MANAGER->mkFunctionType(types, tt); + tt = SOLVER->mkFunctionSort(sorts, tt); } - Expr func = PARSER_STATE->mkVar(name, tt, + api::Term func = PARSER_STATE->bindVar(name, tt, ExprManager::VAR_FLAG_DEFINED); - cmd->reset(new DefineFunctionCommand(name, func, terms, e)); + cmd->reset(new DefineFunctionCommand( + name, func.getExpr(), api::termVectorToExprs(terms), e.getExpr())); } ) | DEFINE_CONST_TOK { PARSER_STATE->checkThatLogicIsSet(); } @@ -1358,37 +1385,38 @@ extendedCommand[std::unique_ptr<CVC4::Command>* cmd] { /* add variables to parser state before parsing term */ Debug("parser") << "define const: '" << name << "'" << std::endl; PARSER_STATE->pushScope(true); - terms = PARSER_STATE->mkBoundVars(sortedVarNames); + terms = PARSER_STATE->bindBoundVars(sortedVarNames); } term[e, e2] { PARSER_STATE->popScope(); // declare the name down here (while parsing term, signature // must not be extended with the name itself; no recursion // permitted) - Expr func = PARSER_STATE->mkVar(name, t, + api::Term func = PARSER_STATE->bindVar(name, t, ExprManager::VAR_FLAG_DEFINED); - cmd->reset(new DefineFunctionCommand(name, func, terms, e)); + cmd->reset(new DefineFunctionCommand( + name, func.getExpr(), api::termVectorToExprs(terms), e.getExpr())); } | SIMPLIFY_TOK { PARSER_STATE->checkThatLogicIsSet(); } term[e,e2] - { cmd->reset(new SimplifyCommand(e)); } + { cmd->reset(new SimplifyCommand(e.getExpr())); } | GET_QE_TOK { PARSER_STATE->checkThatLogicIsSet(); } term[e,e2] - { cmd->reset(new GetQuantifierEliminationCommand(e, true)); } + { cmd->reset(new GetQuantifierEliminationCommand(e.getExpr(), true)); } | GET_QE_DISJUNCT_TOK { PARSER_STATE->checkThatLogicIsSet(); } term[e,e2] - { cmd->reset(new GetQuantifierEliminationCommand(e, false)); } - | GET_ABDUCT_TOK { + { cmd->reset(new GetQuantifierEliminationCommand(e.getExpr(), false)); } + | GET_ABDUCT_TOK { PARSER_STATE->checkThatLogicIsSet(); } symbol[name,CHECK_UNDECLARED,SYM_VARIABLE] term[e,e2] ( sygusGrammar[t, terms, name] - )? + )? { - cmd->reset(new GetAbductCommand(name,e, t)); + cmd->reset(new GetAbductCommand(name,e.getExpr(), t.getType())); } | DECLARE_HEAP LPAREN_TOK sortSymbol[t, CHECK_DECLARED] @@ -1401,7 +1429,7 @@ extendedCommand[std::unique_ptr<CVC4::Command>* cmd] | BLOCK_MODEL_VALUES_TOK { PARSER_STATE->checkThatLogicIsSet(); } ( LPAREN_TOK termList[terms,e] RPAREN_TOK - { cmd->reset(new BlockModelValuesCommand(terms)); } + { cmd->reset(new BlockModelValuesCommand(api::termVectorToExprs(terms))); } | ~LPAREN_TOK { PARSER_STATE->parseError("The block-model-value command expects a list " "of terms. Perhaps you forgot a pair of " @@ -1415,7 +1443,7 @@ datatypes_2_5_DefCommand[bool isCo, std::unique_ptr<CVC4::Command>* cmd] @declarations { std::vector<CVC4::Datatype> dts; std::string name; - std::vector<Type> sorts; + std::vector<api::Sort> sorts; std::vector<std::string> dnames; std::vector<unsigned> arities; } @@ -1424,7 +1452,9 @@ datatypes_2_5_DefCommand[bool isCo, std::unique_ptr<CVC4::Command>* cmd] PARSER_STATE->pushScope(true); } LPAREN_TOK /* parametric sorts */ ( symbol[name,CHECK_UNDECLARED,SYM_SORT] - { sorts.push_back( PARSER_STATE->mkSort(name, ExprManager::SORT_FLAG_PLACEHOLDER) ); } + { + sorts.push_back(PARSER_STATE->mkSort(name, ExprManager::SORT_FLAG_PLACEHOLDER)); + } )* RPAREN_TOK LPAREN_TOK ( LPAREN_TOK datatypeDef[isCo, dts, sorts] RPAREN_TOK )+ RPAREN_TOK @@ -1483,7 +1513,7 @@ datatypesDef[bool isCo, @declarations { std::vector<CVC4::Datatype> dts; std::string name; - std::vector<Type> params; + std::vector<api::Sort> params; } : { PARSER_STATE->pushScope(true); } ( LPAREN_TOK { @@ -1495,7 +1525,8 @@ datatypesDef[bool isCo, } ( PAR_TOK { PARSER_STATE->pushScope(true); } LPAREN_TOK ( symbol[name,CHECK_UNDECLARED,SYM_SORT] - { params.push_back( PARSER_STATE->mkSort(name, ExprManager::SORT_FLAG_PLACEHOLDER) ); } + { + params.push_back( PARSER_STATE->mkSort(name, ExprManager::SORT_FLAG_PLACEHOLDER)); } )* RPAREN_TOK { // if the arity was fixed by prelude and is not equal to the number of parameters @@ -1503,7 +1534,7 @@ datatypesDef[bool isCo, PARSER_STATE->parseError("Wrong number of parameters for datatype."); } Debug("parser-dt") << params.size() << " parameters for " << dnames[dts.size()] << std::endl; - dts.push_back(Datatype(EXPR_MANAGER, dnames[dts.size()],params,isCo)); + dts.push_back(Datatype(PARSER_STATE->getExprManager(), dnames[dts.size()],api::sortVectorToTypes(params),isCo)); } LPAREN_TOK ( LPAREN_TOK constructorDef[dts.back()] RPAREN_TOK )+ @@ -1513,7 +1544,10 @@ datatypesDef[bool isCo, PARSER_STATE->parseError("No parameters given for datatype."); } Debug("parser-dt") << params.size() << " parameters for " << dnames[dts.size()] << std::endl; - dts.push_back(Datatype(EXPR_MANAGER, dnames[dts.size()],params,isCo)); + dts.push_back(Datatype(PARSER_STATE->getExprManager(), + dnames[dts.size()], + api::sortVectorToTypes(params), + isCo)); } ( LPAREN_TOK constructorDef[dts.back()] RPAREN_TOK )+ ) @@ -1586,12 +1620,12 @@ symbolicExpr[CVC4::SExpr& sexpr] * Matches a term. * @return the expression representing the term. */ -term[CVC4::Expr& expr, CVC4::Expr& expr2] +term[CVC4::api::Term& expr, CVC4::api::Term& expr2] @init { - Kind kind = kind::NULL_EXPR; - Expr f; + api::Kind kind = api::NULL_EXPR; + CVC4::api::Term f; std::string name; - Type type; + CVC4::api::Sort type; ParseOp p; } : termNonVariable[expr, expr2] @@ -1609,26 +1643,26 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2] * @return the expression expr representing the term or formula, and expr2, an * optional annotation for expr (for instance, for attributed expressions). */ -termNonVariable[CVC4::Expr& expr, CVC4::Expr& expr2] +termNonVariable[CVC4::api::Term& expr, CVC4::api::Term& expr2] @init { Debug("parser") << "term: " << AntlrInput::tokenText(LT(1)) << std::endl; - Kind kind = kind::NULL_EXPR; + api::Kind kind = api::NULL_EXPR; std::string name; - std::vector<Expr> args; - std::vector< std::pair<std::string, Type> > sortedVarNames; - Expr bvl; - Expr f, f2, f3; + std::vector<CVC4::api::Term> args; + std::vector< std::pair<std::string, CVC4::api::Sort> > sortedVarNames; + CVC4::api::Term bvl; + CVC4::api::Term f, f2, f3; std::string attr; - Expr attexpr; - std::vector<Expr> patexprs; - std::vector<Expr> matchcases; + CVC4::api::Term attexpr; + std::vector<CVC4::api::Term> patexprs; + std::vector<CVC4::api::Term> matchcases; std::unordered_set<std::string> names; - std::vector< std::pair<std::string, Expr> > binders; - Type type; - Type type2; + std::vector< std::pair<std::string, CVC4::api::Term> > binders; + CVC4::api::Sort type; + CVC4::api::Sort type2; api::Term atomTerm; ParseOp p; - std::vector<Type> argTypes; + std::vector<api::Sort> argTypes; } : LPAREN_TOK quantOp[kind] { PARSER_STATE->pushScope(true); } @@ -1642,7 +1676,7 @@ termNonVariable[CVC4::Expr& expr, CVC4::Expr& expr2] if(! f2.isNull()){ args.push_back(f2); } - expr = MK_EXPR(kind, args); + expr = MK_TERM(kind, args); } | LPAREN_TOK COMPREHENSION_TOK { PARSER_STATE->pushScope(true); } @@ -1651,9 +1685,9 @@ termNonVariable[CVC4::Expr& expr, CVC4::Expr& expr2] args.push_back(bvl); } term[f, f2] { args.push_back(f); } - term[f, f2] { - args.push_back(f); - expr = MK_EXPR(CVC4::kind::COMPREHENSION, args); + term[f, f2] { + args.push_back(f); + expr = MK_TERM(api::COMPREHENSION, args); } RPAREN_TOK | LPAREN_TOK qualIdentifier[p] @@ -1697,7 +1731,7 @@ termNonVariable[CVC4::Expr& expr, CVC4::Expr& expr2] } binders.push_back(std::make_pair(name, expr)); } )+ ) { // now implement these bindings - for (const std::pair<std::string, Expr>& binder : binders) + for (const std::pair<std::string, api::Term>& binder : binders) { { PARSER_STATE->defineVar(binder.first, binder.second); @@ -1710,7 +1744,7 @@ termNonVariable[CVC4::Expr& expr, CVC4::Expr& expr2] { PARSER_STATE->popScope(); } | /* match expression */ LPAREN_TOK MATCH_TOK term[expr, f2] { - if( !expr.getType().isDatatype() ){ + if( !expr.getSort().isDatatype() ){ PARSER_STATE->parseError("Cannot match on non-datatype term."); } } @@ -1721,17 +1755,19 @@ termNonVariable[CVC4::Expr& expr, CVC4::Expr& expr2] args.clear(); PARSER_STATE->pushScope(true); // f should be a constructor - type = f.getType(); + type = f.getSort(); Debug("parser-dt") << "Pattern head : " << f << " " << type << std::endl; if (!type.isConstructor()) { PARSER_STATE->parseError("Pattern must be application of a constructor or a variable."); } - if (Datatype::datatypeOf(f).isParametric()) + Expr ef = f.getExpr(); + if (Datatype::datatypeOf(ef).isParametric()) { - type = Datatype::datatypeOf(f)[Datatype::indexOf(f)].getSpecializedConstructorType(expr.getType()); + type = Datatype::datatypeOf(ef)[Datatype::indexOf(ef)] + .getSpecializedConstructorType(expr.getSort().getType()); } - argTypes = static_cast<ConstructorType>(type).getArgTypes(); + argTypes = type.getConstructorDomainSorts(); } // arguments of the pattern ( symbol[name,CHECK_NONE,SYM_VARIABLE] { @@ -1740,18 +1776,18 @@ termNonVariable[CVC4::Expr& expr, CVC4::Expr& expr2] PARSER_STATE->parseError("Too many arguments for pattern."); } //make of proper type - Expr arg = PARSER_STATE->mkBoundVar(name, argTypes[args.size()]); + api::Term arg = PARSER_STATE->bindBoundVar(name, argTypes[args.size()]); args.push_back( arg ); } )* RPAREN_TOK term[f3, f2] { // make the match case - std::vector<Expr> cargs; + std::vector<CVC4::api::Term> cargs; cargs.push_back(f); cargs.insert(cargs.end(),args.begin(),args.end()); - Expr c = MK_EXPR(kind::APPLY_CONSTRUCTOR,cargs); - Expr bvla = MK_EXPR(kind::BOUND_VAR_LIST,args); - Expr mc = MK_EXPR(kind::MATCH_BIND_CASE, bvla, c, f3); + api::Term c = MK_TERM(api::APPLY_CONSTRUCTOR,cargs); + api::Term bvla = MK_TERM(api::BOUND_VAR_LIST,args); + api::Term mc = MK_TERM(api::MATCH_BIND_CASE, bvla, c, f3); matchcases.push_back(mc); // now, pop the scope PARSER_STATE->popScope(); @@ -1762,31 +1798,31 @@ termNonVariable[CVC4::Expr& expr, CVC4::Expr& expr2] if (PARSER_STATE->isDeclared(name,SYM_VARIABLE)) { f = PARSER_STATE->getVariable(name); - type = f.getType(); - if (!type.isConstructor() || - !((ConstructorType)type).getArgTypes().empty()) + type = f.getSort(); + if (!type.isConstructor() || + !type.getConstructorDomainSorts().empty()) { PARSER_STATE->parseError("Must apply constructors of arity greater than 0 to arguments in pattern."); } // make nullary constructor application - f = MK_EXPR(kind::APPLY_CONSTRUCTOR, f); + f = MK_TERM(api::APPLY_CONSTRUCTOR, f); } else { // it has the type of the head expr - f = PARSER_STATE->mkBoundVar(name, expr.getType()); + f = PARSER_STATE->bindBoundVar(name, expr.getSort()); } } term[f3, f2] { - Expr mc; - if (f.getKind() == kind::BOUND_VARIABLE) + api::Term mc; + if (f.getKind() == api::VARIABLE) { - Expr bvlf = MK_EXPR(kind::BOUND_VAR_LIST, f); - mc = MK_EXPR(kind::MATCH_BIND_CASE, bvlf, f, f3); + api::Term bvlf = MK_TERM(api::BOUND_VAR_LIST, f); + mc = MK_TERM(api::MATCH_BIND_CASE, bvlf, f, f3); } else { - mc = MK_EXPR(kind::MATCH_CASE, f, f3); + mc = MK_TERM(api::MATCH_CASE, f, f3); } matchcases.push_back(mc); } @@ -1798,10 +1834,10 @@ termNonVariable[CVC4::Expr& expr, CVC4::Expr& expr2] { PARSER_STATE->parseError("Must have at least one case in match."); } - std::vector<Expr> mchildren; + std::vector<api::Term> mchildren; mchildren.push_back(expr); mchildren.insert(mchildren.end(), matchcases.begin(), matchcases.end()); - expr = MK_EXPR(kind::MATCH, mchildren); + expr = MK_TERM(api::MATCH, mchildren); } /* attributed expressions */ @@ -1814,9 +1850,9 @@ termNonVariable[CVC4::Expr& expr, CVC4::Expr& expr2] )+ RPAREN_TOK { if(! patexprs.empty()) { - if( !f2.isNull() && f2.getKind()==kind::INST_PATTERN_LIST ){ + if( !f2.isNull() && f2.getKind()==api::INST_PATTERN_LIST ){ for( size_t i=0; i<f2.getNumChildren(); i++ ){ - if( f2[i].getKind()==kind::INST_PATTERN ){ + if( f2[i].getKind()==api::INST_PATTERN ){ patexprs.push_back( f2[i] ); }else{ std::stringstream ss; @@ -1826,7 +1862,7 @@ termNonVariable[CVC4::Expr& expr, CVC4::Expr& expr2] } } } - expr2 = MK_EXPR(kind::INST_PATTERN_LIST, patexprs); + expr2 = MK_TERM(api::INST_PATTERN_LIST, patexprs); } else { expr2 = f2; } @@ -1840,15 +1876,15 @@ termNonVariable[CVC4::Expr& expr, CVC4::Expr& expr2] args.push_back(bvl); args.push_back(f); PARSER_STATE->popScope(); - expr = MK_EXPR(CVC4::kind::LAMBDA, args); + expr = MK_TERM(api::LAMBDA, args); } | LPAREN_TOK TUPLE_CONST_TOK termList[args,expr] RPAREN_TOK { std::vector<api::Sort> sorts; std::vector<api::Term> terms; - for (const Expr& arg : args) + for (const api::Term& arg : args) { - sorts.emplace_back(arg.getType()); + sorts.emplace_back(arg.getSort()); terms.emplace_back(arg); } expr = SOLVER->mkTuple(sorts, terms).getExpr(); @@ -1881,7 +1917,7 @@ termNonVariable[CVC4::Expr& expr, CVC4::Expr& expr2] * - For declared functions f, we return (2). * - For indexed functions like testers (_ is C) and bitvector extract * (_ extract n m), we return (3) for the appropriate operator. - * - For tuple selectors (_ tupSel n), we return (1) and (3). Kind is set to + * - For tuple selectors (_ tupSel n), we return (1) and (3). api::Kind is set to * APPLY_SELECTOR, and expr is set to n, which is to be interpreted by the * caller as the n^th generic tuple selector. We do this since there is no * AST expression representing generic tuple select, and we do not have enough @@ -1910,16 +1946,16 @@ termNonVariable[CVC4::Expr& expr, CVC4::Expr& expr2] */ qualIdentifier[CVC4::ParseOp& p] @init { - Kind k; + api::Kind k; std::string baseName; - Expr f; - Type type; + CVC4::api::Term f; + CVC4::api::Sort type; } : identifier[p] | LPAREN_TOK AS_TOK ( CONST_TOK sortSymbol[type, CHECK_DECLARED] { - p.d_kind = kind::STORE_ALL; + p.d_kind = api::STORE_ALL; PARSER_STATE->parseOpApplyTypeAscription(p, type); } | identifier[p] @@ -1941,8 +1977,8 @@ qualIdentifier[CVC4::ParseOp& p] */ identifier[CVC4::ParseOp& p] @init { - Expr f; - Expr f2; + CVC4::api::Term f; + CVC4::api::Term f2; std::vector<uint64_t> numerals; } : functionName[p.d_name, CHECK_NONE] @@ -1952,24 +1988,29 @@ identifier[CVC4::ParseOp& p] | LPAREN_TOK INDEX_TOK ( TESTER_TOK term[f, f2] { - if (f.getKind() == kind::APPLY_CONSTRUCTOR && f.getNumChildren() == 0) + if (f.getKind() == api::APPLY_CONSTRUCTOR && f.getNumChildren() == 1) { // for nullary constructors, must get the operator - f = f.getOperator(); + f = f[0]; } - if (!f.getType().isConstructor()) + if (!f.getSort().isConstructor()) { PARSER_STATE->parseError( "Bad syntax for test (_ is X), X must be a constructor."); } - p.d_expr = Datatype::datatypeOf(f)[Datatype::indexOf(f)].getTester(); + // get the datatype that f belongs to + api::Sort sf = f.getSort().getConstructorCodomainSort(); + api::Datatype d = sf.getDatatype(); + // lookup by name + api::DatatypeConstructor dc = d.getConstructor(f.toString()); + p.d_expr = dc.getTesterTerm(); } | TUPLE_SEL_TOK m=INTEGER_LITERAL { // we adopt a special syntax (_ tupSel n) - p.d_kind = CVC4::kind::APPLY_SELECTOR; + p.d_kind = api::APPLY_SELECTOR; // put m in expr so that the caller can deal with this case - p.d_expr = MK_CONST(Rational(AntlrInput::tokenToUnsigned($m))); + p.d_expr = SOLVER->mkReal(AntlrInput::tokenToUnsigned($m)); } | sym=SIMPLE_SYMBOL nonemptyNumeralList[numerals] { @@ -1985,8 +2026,8 @@ identifier[CVC4::ParseOp& p] */ termAtomic[CVC4::api::Term& atomTerm] @init { - Type type; - Type type2; + CVC4::api::Sort type; + CVC4::api::Sort type2; std::string s; std::vector<uint64_t> numerals; } @@ -2054,18 +2095,17 @@ termAtomic[CVC4::api::Term& atomTerm] /** * Read attribute */ -attribute[CVC4::Expr& expr, CVC4::Expr& retExpr, std::string& attr] +attribute[CVC4::api::Term& expr, CVC4::api::Term& retExpr, std::string& attr] @init { SExpr sexpr; - Expr patexpr; - std::vector<Expr> patexprs; - Expr e2; + CVC4::api::Term patexpr; + std::vector<CVC4::api::Term> patexprs; + CVC4::api::Term e2; bool hasValue = false; } : KEYWORD ( simpleSymbolicExprNoKeyword[sexpr] { hasValue = true; } )? { attr = AntlrInput::tokenText($KEYWORD); - // EXPR_MANAGER->setNamedAttribute( expr, attr ); if(attr == ":rewrite-rule") { if(hasValue) { std::stringstream ss; @@ -2083,18 +2123,18 @@ attribute[CVC4::Expr& expr, CVC4::Expr& retExpr, std::string& attr] << " does not take a value (ignoring)"; PARSER_STATE->warning(ss.str()); } - Expr avar; + api::Term avar; bool success = true; std::string attr_name = attr; attr_name.erase( attr_name.begin() ); if( attr==":fun-def" ){ - if( expr.getKind()!=kind::EQUAL || expr[0].getKind()!=kind::APPLY_UF ){ + if( expr.getKind()!=api::EQUAL || expr[0].getKind()!=api::APPLY_UF ){ success = false; }else{ - FunctionType t = (FunctionType)expr[0].getOperator().getType(); + api::Sort t = expr[0].getOp().getSort(); for( unsigned i=0; i<expr[0].getNumChildren(); i++ ){ - if( expr[0][i].getKind() != kind::BOUND_VARIABLE || - expr[0][i].getType() != t.getArgTypes()[i] ){ + if( expr[0][i].getKind() != api::VARIABLE || + expr[0][i].getSort() != t.getFunctionDomainSorts()[i] ){ success = false; break; }else{ @@ -2116,14 +2156,14 @@ attribute[CVC4::Expr& expr, CVC4::Expr& retExpr, std::string& attr] avar = expr[0]; } }else{ - Type boolType = EXPR_MANAGER->booleanType(); - avar = PARSER_STATE->mkVar(attr_name, boolType); + api::Sort boolType = SOLVER->getBooleanSort(); + avar = PARSER_STATE->bindVar(attr_name, boolType); } if( success ){ //Will set the attribute on auxiliary var (preserves attribute on //formula through rewriting). - retExpr = MK_EXPR(kind::INST_ATTRIBUTE, avar); - Command* c = new SetUserAttributeCommand( attr_name, avar ); + retExpr = MK_TERM(api::INST_ATTRIBUTE, avar); + Command* c = new SetUserAttributeCommand( attr_name, avar.getExpr() ); c->setMuted(true); PARSER_STATE->preemptCommand(c); } @@ -2137,35 +2177,38 @@ attribute[CVC4::Expr& expr, CVC4::Expr& retExpr, std::string& attr] )+ RPAREN_TOK { attr = std::string(":pattern"); - retExpr = MK_EXPR(kind::INST_PATTERN, patexprs); + retExpr = MK_TERM(api::INST_PATTERN, patexprs); } | ATTRIBUTE_NO_PATTERN_TOK term[patexpr, e2] { attr = std::string(":no-pattern"); - retExpr = MK_EXPR(kind::INST_NO_PATTERN, patexpr); + retExpr = MK_TERM(api::INST_NO_PATTERN, patexpr); } - | tok=( ATTRIBUTE_INST_LEVEL | ATTRIBUTE_RR_PRIORITY ) INTEGER_LITERAL + | tok=( ATTRIBUTE_INST_LEVEL ) INTEGER_LITERAL { - Expr n = MK_CONST( AntlrInput::tokenToInteger($INTEGER_LITERAL) ); - std::vector<Expr> values; + std::stringstream sIntLit; + sIntLit << $INTEGER_LITERAL; + api::Term n = SOLVER->mkReal(sIntLit.str()); + std::vector<api::Term> values; values.push_back( n ); std::string attr_name(AntlrInput::tokenText($tok)); attr_name.erase( attr_name.begin() ); - Type boolType = EXPR_MANAGER->booleanType(); - Expr avar = PARSER_STATE->mkVar(attr_name, boolType); - retExpr = MK_EXPR(kind::INST_ATTRIBUTE, avar); - Command* c = new SetUserAttributeCommand( attr_name, avar, values ); + api::Sort boolType = SOLVER->getBooleanSort(); + api::Term avar = PARSER_STATE->bindVar(attr_name, boolType); + retExpr = MK_TERM(api::INST_ATTRIBUTE, avar); + Command* c = new SetUserAttributeCommand( + attr_name, avar.getExpr(), api::termVectorToExprs(values)); c->setMuted(true); PARSER_STATE->preemptCommand(c); } | ATTRIBUTE_NAMED_TOK symbolicExpr[sexpr] { attr = std::string(":named"); - Expr func = PARSER_STATE->setNamedAttribute(expr, sexpr); + api::Term func = PARSER_STATE->setNamedAttribute(expr, sexpr); std::string name = sexpr.getValue(); // bind name to expr with define-fun - Command* c = - new DefineNamedFunctionCommand(name, func, std::vector<Expr>(), expr); + Command* c = new DefineNamedFunctionCommand( + name, func.getExpr(), std::vector<Expr>(), expr.getExpr()); c->setMuted(true); PARSER_STATE->preemptCommand(c); } @@ -2175,13 +2218,13 @@ attribute[CVC4::Expr& expr, CVC4::Expr& retExpr, std::string& attr] * Matches a sequence of terms and puts them into the formulas * vector. * @param formulas the vector to fill with terms - * @param expr an Expr reference for the elements of the sequence + * @param expr an CVC4::api::Term reference for the elements of the sequence */ -/* NOTE: We pass an Expr in here just to avoid allocating a fresh Expr every +/* NOTE: We pass an CVC4::api::Term in here just to avoid allocating a fresh CVC4::api::Term every * time through this rule. */ -termList[std::vector<CVC4::Expr>& formulas, CVC4::Expr& expr] +termList[std::vector<CVC4::api::Term>& formulas, CVC4::api::Term& expr] @declarations { - Expr expr2; + CVC4::api::Term expr2; } : ( term[expr, expr2] { formulas.push_back(expr); } )+ ; @@ -2236,12 +2279,12 @@ str[std::string& s, bool fsmtlib] } ; -quantOp[CVC4::Kind& kind] +quantOp[CVC4::api::Kind& kind] @init { Debug("parser") << "quant: " << AntlrInput::tokenText(LT(1)) << std::endl; } - : EXISTS_TOK { $kind = CVC4::kind::EXISTS; } - | FORALL_TOK { $kind = CVC4::kind::FORALL; } + : EXISTS_TOK { $kind = api::EXISTS; } + | FORALL_TOK { $kind = api::FORALL; } ; /** @@ -2256,16 +2299,16 @@ functionName[std::string& name, CVC4::parser::DeclarationCheck check] * Matches a sequence of sort symbols and fills them into the given * vector. */ -sortList[std::vector<CVC4::Type>& sorts] +sortList[std::vector<CVC4::api::Sort>& sorts] @declarations { - Type t; + CVC4::api::Sort t; } : ( sortSymbol[t,CHECK_DECLARED] { sorts.push_back(t); } )* ; -nonemptySortList[std::vector<CVC4::Type>& sorts] +nonemptySortList[std::vector<CVC4::api::Sort>& sorts] @declarations { - Type t; + CVC4::api::Sort t; } : ( sortSymbol[t,CHECK_DECLARED] { sorts.push_back(t); } )+ ; @@ -2274,10 +2317,10 @@ nonemptySortList[std::vector<CVC4::Type>& sorts] * Matches a sequence of (variable,sort) symbol pairs and fills them * into the given vector. */ -sortedVarList[std::vector<std::pair<std::string, CVC4::Type> >& sortedVars] +sortedVarList[std::vector<std::pair<std::string, CVC4::api::Sort> >& sortedVars] @declarations { std::string name; - Type t; + CVC4::api::Sort t; } : ( LPAREN_TOK symbol[name,CHECK_NONE,SYM_VARIABLE] sortSymbol[t,CHECK_DECLARED] RPAREN_TOK @@ -2289,14 +2332,15 @@ sortedVarList[std::vector<std::pair<std::string, CVC4::Type> >& sortedVars] * Matches a sequence of (variable, sort) symbol pairs, registers them as bound * variables, and returns a term corresponding to the list of pairs. */ -boundVarList[CVC4::Expr& expr] +boundVarList[CVC4::api::Term& expr] @declarations { - std::vector<std::pair<std::string, CVC4::Type>> sortedVarNames; + std::vector<std::pair<std::string, CVC4::api::Sort>> sortedVarNames; } : LPAREN_TOK sortedVarList[sortedVarNames] RPAREN_TOK { - std::vector<CVC4::Expr> args = PARSER_STATE->mkBoundVars(sortedVarNames); - expr = MK_EXPR(kind::BOUND_VAR_LIST, args); + std::vector<CVC4::api::Term> args = + PARSER_STATE->bindBoundVars(sortedVarNames); + expr = MK_TERM(api::BOUND_VAR_LIST, args); } ; @@ -2308,10 +2352,10 @@ sortName[std::string& name, CVC4::parser::DeclarationCheck check] : symbol[name,check,SYM_SORT] ; -sortSymbol[CVC4::Type& t, CVC4::parser::DeclarationCheck check] +sortSymbol[CVC4::api::Sort& t, CVC4::parser::DeclarationCheck check] @declarations { std::string name; - std::vector<CVC4::Type> args; + std::vector<CVC4::api::Sort> args; std::vector<uint64_t> numerals; bool indexed = false; } @@ -2340,7 +2384,7 @@ sortSymbol[CVC4::Type& t, CVC4::parser::DeclarationCheck check] if(numerals.front() == 0) { PARSER_STATE->parseError("Illegal bitvector size: 0"); } - t = EXPR_MANAGER->mkBitVectorType(numerals.front()); + t = SOLVER->mkBitVectorSort(numerals.front()); } else if ( name == "FloatingPoint" ) { if( numerals.size() != 2 ) { PARSER_STATE->parseError("Illegal floating-point type."); @@ -2351,7 +2395,7 @@ sortSymbol[CVC4::Type& t, CVC4::parser::DeclarationCheck check] if(!validSignificandSize(numerals[1])) { PARSER_STATE->parseError("Illegal floating-point significand size"); } - t = EXPR_MANAGER->mkFloatingPointType(numerals[0],numerals[1]); + t = SOLVER->mkFloatingPointSort(numerals[0],numerals[1]); } else { std::stringstream ss; ss << "unknown indexed sort symbol `" << name << "'"; @@ -2373,15 +2417,15 @@ sortSymbol[CVC4::Type& t, CVC4::parser::DeclarationCheck check] if(args.size() != 2) { PARSER_STATE->parseError("Illegal array type."); } - t = EXPR_MANAGER->mkArrayType( args[0], args[1] ); + t = SOLVER->mkArraySort( args[0], args[1] ); } else if(name == "Set" && PARSER_STATE->isTheoryEnabled(Smt2::THEORY_SETS) ) { if(args.size() != 1) { PARSER_STATE->parseError("Illegal set type."); } - t = EXPR_MANAGER->mkSetType( args[0] ); + t = SOLVER->mkSetSort( args[0] ); } else if(name == "Tuple") { - t = EXPR_MANAGER->mkTupleType(args); + t = SOLVER->mkTupleSort(args); } else if(check == CHECK_DECLARED || PARSER_STATE->isDeclared(name, SYM_SORT)) { t = PARSER_STATE->getSort(name, args); @@ -2393,7 +2437,7 @@ sortSymbol[CVC4::Type& t, CVC4::parser::DeclarationCheck check] << std::endl; } else { t = PARSER_STATE->mkUnresolvedTypeConstructor(name,args); - t = SortConstructorType(t).instantiate( args ); + t = t.instantiate( args ); Debug("parser-param") << "param: make unres param type " << name << " " << args.size() << " " << PARSER_STATE->getArity( name ) << std::endl; @@ -2407,7 +2451,7 @@ sortSymbol[CVC4::Type& t, CVC4::parser::DeclarationCheck check] PARSER_STATE->parseError("Arrow types must have at least 2 arguments"); } //flatten the type - Type rangeType = args.back(); + api::Sort rangeType = args.back(); args.pop_back(); t = PARSER_STATE->mkFlatFunctionType( args, rangeType ); } @@ -2474,7 +2518,7 @@ nonemptyNumeralList[std::vector<uint64_t>& numerals] * Parses a datatype definition */ datatypeDef[bool isCo, std::vector<CVC4::Datatype>& datatypes, - std::vector< CVC4::Type >& params] + std::vector< CVC4::api::Sort >& params] @init { std::string id; } @@ -2483,11 +2527,11 @@ datatypeDef[bool isCo, std::vector<CVC4::Datatype>& datatypes, * "defined" as an unresolved type; don't worry, we check * below. */ : symbol[id,CHECK_NONE,SYM_SORT] { PARSER_STATE->pushScope(true); } - { datatypes.push_back(Datatype(EXPR_MANAGER, id, params, isCo)); - if(!PARSER_STATE->isUnresolvedType(id)) { - // if not unresolved, must be undeclared - PARSER_STATE->checkDeclaration(id, CHECK_UNDECLARED, SYM_SORT); - } + { + datatypes.push_back(Datatype(PARSER_STATE->getExprManager(), + id, + api::sortVectorToTypes(params), + isCo)); } ( LPAREN_TOK constructorDef[datatypes.back()] RPAREN_TOK )+ { PARSER_STATE->popScope(); } @@ -2518,10 +2562,10 @@ constructorDef[CVC4::Datatype& type] selector[CVC4::DatatypeConstructor& ctor] @init { std::string id; - Type t, t2; + CVC4::api::Sort t, t2; } : symbol[id,CHECK_NONE,SYM_SORT] sortSymbol[t,CHECK_NONE] - { ctor.addArg(id, t); + { ctor.addArg(id, t.getType()); Debug("parser-idt") << "selector: " << id.c_str() << " of type " << t << std::endl; } diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index 15fdd8461..73be8910f 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -45,242 +45,236 @@ Smt2::Smt2(api::Solver* solver, Input* input, bool strictMode, bool parseOnly) } void Smt2::addArithmeticOperators() { - addOperator(kind::PLUS, "+"); - addOperator(kind::MINUS, "-"); - // kind::MINUS is converted to kind::UMINUS if there is only a single operand - Parser::addOperator(kind::UMINUS); - addOperator(kind::MULT, "*"); - addOperator(kind::LT, "<"); - addOperator(kind::LEQ, "<="); - addOperator(kind::GT, ">"); - addOperator(kind::GEQ, ">="); + addOperator(api::PLUS, "+"); + addOperator(api::MINUS, "-"); + // api::MINUS is converted to api::UMINUS if there is only a single operand + Parser::addOperator(api::UMINUS); + addOperator(api::MULT, "*"); + addOperator(api::LT, "<"); + addOperator(api::LEQ, "<="); + addOperator(api::GT, ">"); + addOperator(api::GEQ, ">="); if (!strictModeEnabled()) { // NOTE: this operator is non-standard - addOperator(kind::POW, "^"); + addOperator(api::POW, "^"); } } void Smt2::addTranscendentalOperators() { - addOperator(kind::EXPONENTIAL, "exp"); - addOperator(kind::SINE, "sin"); - addOperator(kind::COSINE, "cos"); - addOperator(kind::TANGENT, "tan"); - addOperator(kind::COSECANT, "csc"); - addOperator(kind::SECANT, "sec"); - addOperator(kind::COTANGENT, "cot"); - addOperator(kind::ARCSINE, "arcsin"); - addOperator(kind::ARCCOSINE, "arccos"); - addOperator(kind::ARCTANGENT, "arctan"); - addOperator(kind::ARCCOSECANT, "arccsc"); - addOperator(kind::ARCSECANT, "arcsec"); - addOperator(kind::ARCCOTANGENT, "arccot"); - addOperator(kind::SQRT, "sqrt"); + addOperator(api::EXPONENTIAL, "exp"); + addOperator(api::SINE, "sin"); + addOperator(api::COSINE, "cos"); + addOperator(api::TANGENT, "tan"); + addOperator(api::COSECANT, "csc"); + addOperator(api::SECANT, "sec"); + addOperator(api::COTANGENT, "cot"); + addOperator(api::ARCSINE, "arcsin"); + addOperator(api::ARCCOSINE, "arccos"); + addOperator(api::ARCTANGENT, "arctan"); + addOperator(api::ARCCOSECANT, "arccsc"); + addOperator(api::ARCSECANT, "arcsec"); + addOperator(api::ARCCOTANGENT, "arccot"); + addOperator(api::SQRT, "sqrt"); } void Smt2::addQuantifiersOperators() { if (!strictModeEnabled()) { - addOperator(kind::INST_CLOSURE, "inst-closure"); + addOperator(api::INST_CLOSURE, "inst-closure"); } } void Smt2::addBitvectorOperators() { - addOperator(kind::BITVECTOR_CONCAT, "concat"); - addOperator(kind::BITVECTOR_NOT, "bvnot"); - addOperator(kind::BITVECTOR_AND, "bvand"); - addOperator(kind::BITVECTOR_OR, "bvor"); - addOperator(kind::BITVECTOR_NEG, "bvneg"); - addOperator(kind::BITVECTOR_PLUS, "bvadd"); - addOperator(kind::BITVECTOR_MULT, "bvmul"); - addOperator(kind::BITVECTOR_UDIV, "bvudiv"); - addOperator(kind::BITVECTOR_UREM, "bvurem"); - addOperator(kind::BITVECTOR_SHL, "bvshl"); - addOperator(kind::BITVECTOR_LSHR, "bvlshr"); - addOperator(kind::BITVECTOR_ULT, "bvult"); - addOperator(kind::BITVECTOR_NAND, "bvnand"); - addOperator(kind::BITVECTOR_NOR, "bvnor"); - addOperator(kind::BITVECTOR_XOR, "bvxor"); - addOperator(kind::BITVECTOR_XNOR, "bvxnor"); - addOperator(kind::BITVECTOR_COMP, "bvcomp"); - addOperator(kind::BITVECTOR_SUB, "bvsub"); - addOperator(kind::BITVECTOR_SDIV, "bvsdiv"); - addOperator(kind::BITVECTOR_SREM, "bvsrem"); - addOperator(kind::BITVECTOR_SMOD, "bvsmod"); - addOperator(kind::BITVECTOR_ASHR, "bvashr"); - addOperator(kind::BITVECTOR_ULE, "bvule"); - addOperator(kind::BITVECTOR_UGT, "bvugt"); - addOperator(kind::BITVECTOR_UGE, "bvuge"); - addOperator(kind::BITVECTOR_SLT, "bvslt"); - addOperator(kind::BITVECTOR_SLE, "bvsle"); - addOperator(kind::BITVECTOR_SGT, "bvsgt"); - addOperator(kind::BITVECTOR_SGE, "bvsge"); - addOperator(kind::BITVECTOR_REDOR, "bvredor"); - addOperator(kind::BITVECTOR_REDAND, "bvredand"); - addOperator(kind::BITVECTOR_TO_NAT, "bv2nat"); - + addOperator(api::BITVECTOR_CONCAT, "concat"); + addOperator(api::BITVECTOR_NOT, "bvnot"); + addOperator(api::BITVECTOR_AND, "bvand"); + addOperator(api::BITVECTOR_OR, "bvor"); + addOperator(api::BITVECTOR_NEG, "bvneg"); + addOperator(api::BITVECTOR_PLUS, "bvadd"); + addOperator(api::BITVECTOR_MULT, "bvmul"); + addOperator(api::BITVECTOR_UDIV, "bvudiv"); + addOperator(api::BITVECTOR_UREM, "bvurem"); + addOperator(api::BITVECTOR_SHL, "bvshl"); + addOperator(api::BITVECTOR_LSHR, "bvlshr"); + addOperator(api::BITVECTOR_ULT, "bvult"); + addOperator(api::BITVECTOR_NAND, "bvnand"); + addOperator(api::BITVECTOR_NOR, "bvnor"); + addOperator(api::BITVECTOR_XOR, "bvxor"); + addOperator(api::BITVECTOR_XNOR, "bvxnor"); + addOperator(api::BITVECTOR_COMP, "bvcomp"); + addOperator(api::BITVECTOR_SUB, "bvsub"); + addOperator(api::BITVECTOR_SDIV, "bvsdiv"); + addOperator(api::BITVECTOR_SREM, "bvsrem"); + addOperator(api::BITVECTOR_SMOD, "bvsmod"); + addOperator(api::BITVECTOR_ASHR, "bvashr"); + addOperator(api::BITVECTOR_ULE, "bvule"); + addOperator(api::BITVECTOR_UGT, "bvugt"); + addOperator(api::BITVECTOR_UGE, "bvuge"); + addOperator(api::BITVECTOR_SLT, "bvslt"); + addOperator(api::BITVECTOR_SLE, "bvsle"); + addOperator(api::BITVECTOR_SGT, "bvsgt"); + addOperator(api::BITVECTOR_SGE, "bvsge"); + addOperator(api::BITVECTOR_REDOR, "bvredor"); + addOperator(api::BITVECTOR_REDAND, "bvredand"); + addOperator(api::BITVECTOR_TO_NAT, "bv2nat"); + + addIndexedOperator(api::BITVECTOR_EXTRACT, api::BITVECTOR_EXTRACT, "extract"); + addIndexedOperator(api::BITVECTOR_REPEAT, api::BITVECTOR_REPEAT, "repeat"); addIndexedOperator( - kind::BITVECTOR_EXTRACT, api::BITVECTOR_EXTRACT, "extract"); - addIndexedOperator(kind::BITVECTOR_REPEAT, api::BITVECTOR_REPEAT, "repeat"); + api::BITVECTOR_ZERO_EXTEND, api::BITVECTOR_ZERO_EXTEND, "zero_extend"); addIndexedOperator( - kind::BITVECTOR_ZERO_EXTEND, api::BITVECTOR_ZERO_EXTEND, "zero_extend"); + api::BITVECTOR_SIGN_EXTEND, api::BITVECTOR_SIGN_EXTEND, "sign_extend"); addIndexedOperator( - kind::BITVECTOR_SIGN_EXTEND, api::BITVECTOR_SIGN_EXTEND, "sign_extend"); + api::BITVECTOR_ROTATE_LEFT, api::BITVECTOR_ROTATE_LEFT, "rotate_left"); addIndexedOperator( - kind::BITVECTOR_ROTATE_LEFT, api::BITVECTOR_ROTATE_LEFT, "rotate_left"); - addIndexedOperator(kind::BITVECTOR_ROTATE_RIGHT, - api::BITVECTOR_ROTATE_RIGHT, - "rotate_right"); - addIndexedOperator(kind::INT_TO_BITVECTOR, api::INT_TO_BITVECTOR, "int2bv"); + api::BITVECTOR_ROTATE_RIGHT, api::BITVECTOR_ROTATE_RIGHT, "rotate_right"); + addIndexedOperator(api::INT_TO_BITVECTOR, api::INT_TO_BITVECTOR, "int2bv"); } void Smt2::addDatatypesOperators() { - Parser::addOperator(kind::APPLY_CONSTRUCTOR); - Parser::addOperator(kind::APPLY_TESTER); - Parser::addOperator(kind::APPLY_SELECTOR); - Parser::addOperator(kind::APPLY_SELECTOR_TOTAL); + Parser::addOperator(api::APPLY_CONSTRUCTOR); + Parser::addOperator(api::APPLY_TESTER); + Parser::addOperator(api::APPLY_SELECTOR); if (!strictModeEnabled()) { - addOperator(kind::DT_SIZE, "dt.size"); + addOperator(api::DT_SIZE, "dt.size"); } } void Smt2::addStringOperators() { - defineVar("re.all", - getSolver() - ->mkTerm(api::REGEXP_STAR, getSolver()->mkRegexpSigma()) - .getExpr()); - - addOperator(kind::STRING_CONCAT, "str.++"); - addOperator(kind::STRING_LENGTH, "str.len"); - addOperator(kind::STRING_SUBSTR, "str.substr" ); - addOperator(kind::STRING_STRCTN, "str.contains" ); - addOperator(kind::STRING_CHARAT, "str.at" ); - addOperator(kind::STRING_STRIDOF, "str.indexof" ); - addOperator(kind::STRING_STRREPL, "str.replace" ); + defineVar( + "re.all", + getSolver()->mkTerm(api::REGEXP_STAR, getSolver()->mkRegexpSigma())); + addOperator(api::STRING_CONCAT, "str.++"); + addOperator(api::STRING_LENGTH, "str.len"); + addOperator(api::STRING_SUBSTR, "str.substr"); + addOperator(api::STRING_STRCTN, "str.contains"); + addOperator(api::STRING_CHARAT, "str.at"); + addOperator(api::STRING_STRIDOF, "str.indexof"); + addOperator(api::STRING_STRREPL, "str.replace"); if (!strictModeEnabled()) { - addOperator(kind::STRING_TOLOWER, "str.tolower"); - addOperator(kind::STRING_TOUPPER, "str.toupper"); - addOperator(kind::STRING_REV, "str.rev"); - } - addOperator(kind::STRING_PREFIX, "str.prefixof" ); - addOperator(kind::STRING_SUFFIX, "str.suffixof" ); - addOperator(kind::STRING_FROM_CODE, "str.from_code"); - addOperator(kind::STRING_IS_DIGIT, "str.is_digit" ); - + addOperator(api::STRING_TOLOWER, "str.tolower"); + addOperator(api::STRING_TOUPPER, "str.toupper"); + addOperator(api::STRING_REV, "str.rev"); + } + addOperator(api::STRING_PREFIX, "str.prefixof"); + addOperator(api::STRING_SUFFIX, "str.suffixof"); + addOperator(api::STRING_FROM_CODE, "str.from_code"); + addOperator(api::STRING_IS_DIGIT, "str.is_digit"); // at the moment, we only use this syntax for smt2.6.1 if (getLanguage() == language::input::LANG_SMTLIB_V2_6_1 || getLanguage() == language::input::LANG_SYGUS_V2) { - addOperator(kind::STRING_ITOS, "str.from_int"); - addOperator(kind::STRING_STOI, "str.to_int"); - addOperator(kind::STRING_IN_REGEXP, "str.in_re"); - addOperator(kind::STRING_TO_REGEXP, "str.to_re"); - addOperator(kind::STRING_TO_CODE, "str.to_code"); - addOperator(kind::STRING_STRREPLALL, "str.replace_all"); + addOperator(api::STRING_ITOS, "str.from_int"); + addOperator(api::STRING_STOI, "str.to_int"); + addOperator(api::STRING_IN_REGEXP, "str.in_re"); + addOperator(api::STRING_TO_REGEXP, "str.to_re"); + addOperator(api::STRING_TO_CODE, "str.to_code"); + addOperator(api::STRING_STRREPLALL, "str.replace_all"); } else { - addOperator(kind::STRING_ITOS, "int.to.str"); - addOperator(kind::STRING_STOI, "str.to.int"); - addOperator(kind::STRING_IN_REGEXP, "str.in.re"); - addOperator(kind::STRING_TO_REGEXP, "str.to.re"); - addOperator(kind::STRING_TO_CODE, "str.code"); - addOperator(kind::STRING_STRREPLALL, "str.replaceall"); - } - - addOperator(kind::REGEXP_CONCAT, "re.++"); - addOperator(kind::REGEXP_UNION, "re.union"); - addOperator(kind::REGEXP_INTER, "re.inter"); - addOperator(kind::REGEXP_STAR, "re.*"); - addOperator(kind::REGEXP_PLUS, "re.+"); - addOperator(kind::REGEXP_OPT, "re.opt"); - addOperator(kind::REGEXP_RANGE, "re.range"); - addOperator(kind::REGEXP_LOOP, "re.loop"); - addOperator(kind::REGEXP_COMPLEMENT, "re.comp"); - addOperator(kind::REGEXP_DIFF, "re.diff"); - addOperator(kind::STRING_LT, "str.<"); - addOperator(kind::STRING_LEQ, "str.<="); + addOperator(api::STRING_ITOS, "int.to.str"); + addOperator(api::STRING_STOI, "str.to.int"); + addOperator(api::STRING_IN_REGEXP, "str.in.re"); + addOperator(api::STRING_TO_REGEXP, "str.to.re"); + addOperator(api::STRING_TO_CODE, "str.code"); + addOperator(api::STRING_STRREPLALL, "str.replaceall"); + } + + addOperator(api::REGEXP_CONCAT, "re.++"); + addOperator(api::REGEXP_UNION, "re.union"); + addOperator(api::REGEXP_INTER, "re.inter"); + addOperator(api::REGEXP_STAR, "re.*"); + addOperator(api::REGEXP_PLUS, "re.+"); + addOperator(api::REGEXP_OPT, "re.opt"); + addOperator(api::REGEXP_RANGE, "re.range"); + addOperator(api::REGEXP_LOOP, "re.loop"); + addOperator(api::REGEXP_COMPLEMENT, "re.comp"); + addOperator(api::REGEXP_DIFF, "re.diff"); + addOperator(api::STRING_LT, "str.<"); + addOperator(api::STRING_LEQ, "str.<="); } void Smt2::addFloatingPointOperators() { - addOperator(kind::FLOATINGPOINT_FP, "fp"); - addOperator(kind::FLOATINGPOINT_EQ, "fp.eq"); - addOperator(kind::FLOATINGPOINT_ABS, "fp.abs"); - addOperator(kind::FLOATINGPOINT_NEG, "fp.neg"); - addOperator(kind::FLOATINGPOINT_PLUS, "fp.add"); - addOperator(kind::FLOATINGPOINT_SUB, "fp.sub"); - addOperator(kind::FLOATINGPOINT_MULT, "fp.mul"); - addOperator(kind::FLOATINGPOINT_DIV, "fp.div"); - addOperator(kind::FLOATINGPOINT_FMA, "fp.fma"); - addOperator(kind::FLOATINGPOINT_SQRT, "fp.sqrt"); - addOperator(kind::FLOATINGPOINT_REM, "fp.rem"); - addOperator(kind::FLOATINGPOINT_RTI, "fp.roundToIntegral"); - addOperator(kind::FLOATINGPOINT_MIN, "fp.min"); - addOperator(kind::FLOATINGPOINT_MAX, "fp.max"); - addOperator(kind::FLOATINGPOINT_LEQ, "fp.leq"); - addOperator(kind::FLOATINGPOINT_LT, "fp.lt"); - addOperator(kind::FLOATINGPOINT_GEQ, "fp.geq"); - addOperator(kind::FLOATINGPOINT_GT, "fp.gt"); - addOperator(kind::FLOATINGPOINT_ISN, "fp.isNormal"); - addOperator(kind::FLOATINGPOINT_ISSN, "fp.isSubnormal"); - addOperator(kind::FLOATINGPOINT_ISZ, "fp.isZero"); - addOperator(kind::FLOATINGPOINT_ISINF, "fp.isInfinite"); - addOperator(kind::FLOATINGPOINT_ISNAN, "fp.isNaN"); - addOperator(kind::FLOATINGPOINT_ISNEG, "fp.isNegative"); - addOperator(kind::FLOATINGPOINT_ISPOS, "fp.isPositive"); - addOperator(kind::FLOATINGPOINT_TO_REAL, "fp.to_real"); - - addIndexedOperator(kind::FLOATINGPOINT_TO_FP_GENERIC, + addOperator(api::FLOATINGPOINT_FP, "fp"); + addOperator(api::FLOATINGPOINT_EQ, "fp.eq"); + addOperator(api::FLOATINGPOINT_ABS, "fp.abs"); + addOperator(api::FLOATINGPOINT_NEG, "fp.neg"); + addOperator(api::FLOATINGPOINT_PLUS, "fp.add"); + addOperator(api::FLOATINGPOINT_SUB, "fp.sub"); + addOperator(api::FLOATINGPOINT_MULT, "fp.mul"); + addOperator(api::FLOATINGPOINT_DIV, "fp.div"); + addOperator(api::FLOATINGPOINT_FMA, "fp.fma"); + addOperator(api::FLOATINGPOINT_SQRT, "fp.sqrt"); + addOperator(api::FLOATINGPOINT_REM, "fp.rem"); + addOperator(api::FLOATINGPOINT_RTI, "fp.roundToIntegral"); + addOperator(api::FLOATINGPOINT_MIN, "fp.min"); + addOperator(api::FLOATINGPOINT_MAX, "fp.max"); + addOperator(api::FLOATINGPOINT_LEQ, "fp.leq"); + addOperator(api::FLOATINGPOINT_LT, "fp.lt"); + addOperator(api::FLOATINGPOINT_GEQ, "fp.geq"); + addOperator(api::FLOATINGPOINT_GT, "fp.gt"); + addOperator(api::FLOATINGPOINT_ISN, "fp.isNormal"); + addOperator(api::FLOATINGPOINT_ISSN, "fp.isSubnormal"); + addOperator(api::FLOATINGPOINT_ISZ, "fp.isZero"); + addOperator(api::FLOATINGPOINT_ISINF, "fp.isInfinite"); + addOperator(api::FLOATINGPOINT_ISNAN, "fp.isNaN"); + addOperator(api::FLOATINGPOINT_ISNEG, "fp.isNegative"); + addOperator(api::FLOATINGPOINT_ISPOS, "fp.isPositive"); + addOperator(api::FLOATINGPOINT_TO_REAL, "fp.to_real"); + + addIndexedOperator(api::FLOATINGPOINT_TO_FP_GENERIC, api::FLOATINGPOINT_TO_FP_GENERIC, "to_fp"); - addIndexedOperator(kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR, + addIndexedOperator(api::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR, api::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR, "to_fp_unsigned"); addIndexedOperator( - kind::FLOATINGPOINT_TO_UBV, api::FLOATINGPOINT_TO_UBV, "fp.to_ubv"); + api::FLOATINGPOINT_TO_UBV, api::FLOATINGPOINT_TO_UBV, "fp.to_ubv"); addIndexedOperator( - kind::FLOATINGPOINT_TO_SBV, api::FLOATINGPOINT_TO_SBV, "fp.to_sbv"); + api::FLOATINGPOINT_TO_SBV, api::FLOATINGPOINT_TO_SBV, "fp.to_sbv"); if (!strictModeEnabled()) { - addIndexedOperator(kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR, + addIndexedOperator(api::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR, api::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR, "to_fp_bv"); - addIndexedOperator(kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT, + addIndexedOperator(api::FLOATINGPOINT_TO_FP_FLOATINGPOINT, api::FLOATINGPOINT_TO_FP_FLOATINGPOINT, "to_fp_fp"); - addIndexedOperator(kind::FLOATINGPOINT_TO_FP_REAL, + addIndexedOperator(api::FLOATINGPOINT_TO_FP_REAL, api::FLOATINGPOINT_TO_FP_REAL, "to_fp_real"); - addIndexedOperator(kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR, + addIndexedOperator(api::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR, api::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR, "to_fp_signed"); } } void Smt2::addSepOperators() { - addOperator(kind::SEP_STAR, "sep"); - addOperator(kind::SEP_PTO, "pto"); - addOperator(kind::SEP_WAND, "wand"); - addOperator(kind::SEP_EMP, "emp"); - Parser::addOperator(kind::SEP_STAR); - Parser::addOperator(kind::SEP_PTO); - Parser::addOperator(kind::SEP_WAND); - Parser::addOperator(kind::SEP_EMP); + addOperator(api::SEP_STAR, "sep"); + addOperator(api::SEP_PTO, "pto"); + addOperator(api::SEP_WAND, "wand"); + addOperator(api::SEP_EMP, "emp"); + Parser::addOperator(api::SEP_STAR); + Parser::addOperator(api::SEP_PTO); + Parser::addOperator(api::SEP_WAND); + Parser::addOperator(api::SEP_EMP); } void Smt2::addTheory(Theory theory) { switch(theory) { case THEORY_ARRAYS: - addOperator(kind::SELECT, "select"); - addOperator(kind::STORE, "store"); + addOperator(api::SELECT, "select"); + addOperator(api::STORE, "store"); break; case THEORY_BITVECTORS: @@ -288,145 +282,132 @@ void Smt2::addTheory(Theory theory) { break; case THEORY_CORE: - defineType("Bool", getExprManager()->booleanType()); - defineVar("true", getExprManager()->mkConst(true)); - defineVar("false", getExprManager()->mkConst(false)); - addOperator(kind::AND, "and"); - addOperator(kind::DISTINCT, "distinct"); - addOperator(kind::EQUAL, "="); - addOperator(kind::IMPLIES, "=>"); - addOperator(kind::ITE, "ite"); - addOperator(kind::NOT, "not"); - addOperator(kind::OR, "or"); - addOperator(kind::XOR, "xor"); + defineType("Bool", d_solver->getBooleanSort()); + defineVar("true", d_solver->mkTrue()); + defineVar("false", d_solver->mkFalse()); + addOperator(api::AND, "and"); + addOperator(api::DISTINCT, "distinct"); + addOperator(api::EQUAL, "="); + addOperator(api::IMPLIES, "=>"); + addOperator(api::ITE, "ite"); + addOperator(api::NOT, "not"); + addOperator(api::OR, "or"); + addOperator(api::XOR, "xor"); break; case THEORY_REALS_INTS: - defineType("Real", getExprManager()->realType()); - addOperator(kind::DIVISION, "/"); - addOperator(kind::TO_INTEGER, "to_int"); - addOperator(kind::IS_INTEGER, "is_int"); - addOperator(kind::TO_REAL, "to_real"); + defineType("Real", d_solver->getRealSort()); + addOperator(api::DIVISION, "/"); + addOperator(api::TO_INTEGER, "to_int"); + addOperator(api::IS_INTEGER, "is_int"); + addOperator(api::TO_REAL, "to_real"); // falling through on purpose, to add Ints part of Reals_Ints CVC4_FALLTHROUGH; case THEORY_INTS: - defineType("Int", getExprManager()->integerType()); + defineType("Int", d_solver->getIntegerSort()); addArithmeticOperators(); - addOperator(kind::INTS_DIVISION, "div"); - addOperator(kind::INTS_MODULUS, "mod"); - addOperator(kind::ABS, "abs"); - addIndexedOperator(kind::DIVISIBLE, api::DIVISIBLE, "divisible"); + addOperator(api::INTS_DIVISION, "div"); + addOperator(api::INTS_MODULUS, "mod"); + addOperator(api::ABS, "abs"); + addIndexedOperator(api::DIVISIBLE, api::DIVISIBLE, "divisible"); break; case THEORY_REALS: - defineType("Real", getExprManager()->realType()); + defineType("Real", d_solver->getRealSort()); addArithmeticOperators(); - addOperator(kind::DIVISION, "/"); + addOperator(api::DIVISION, "/"); if (!strictModeEnabled()) { - addOperator(kind::ABS, "abs"); + addOperator(api::ABS, "abs"); } break; case THEORY_TRANSCENDENTALS: - defineVar("real.pi", - getExprManager()->mkNullaryOperator(getExprManager()->realType(), - CVC4::kind::PI)); + defineVar("real.pi", d_solver->mkTerm(api::PI)); addTranscendentalOperators(); break; case THEORY_QUANTIFIERS: addQuantifiersOperators(); break; case THEORY_SETS: - defineVar("emptyset", - d_solver->mkEmptySet(d_solver->getNullSort()).getExpr()); + defineVar("emptyset", d_solver->mkEmptySet(d_solver->getNullSort())); // the Boolean sort is a placeholder here since we don't have type info // without type annotation - defineVar("univset", - d_solver->mkUniverseSet(d_solver->getBooleanSort()).getExpr()); - - addOperator(kind::UNION, "union"); - addOperator(kind::INTERSECTION, "intersection"); - addOperator(kind::SETMINUS, "setminus"); - addOperator(kind::SUBSET, "subset"); - addOperator(kind::MEMBER, "member"); - addOperator(kind::SINGLETON, "singleton"); - addOperator(kind::INSERT, "insert"); - addOperator(kind::CARD, "card"); - addOperator(kind::COMPLEMENT, "complement"); - addOperator(kind::JOIN, "join"); - addOperator(kind::PRODUCT, "product"); - addOperator(kind::TRANSPOSE, "transpose"); - addOperator(kind::TCLOSURE, "tclosure"); + defineVar("univset", d_solver->mkUniverseSet(d_solver->getBooleanSort())); + + addOperator(api::UNION, "union"); + addOperator(api::INTERSECTION, "intersection"); + addOperator(api::SETMINUS, "setminus"); + addOperator(api::SUBSET, "subset"); + addOperator(api::MEMBER, "member"); + addOperator(api::SINGLETON, "singleton"); + addOperator(api::INSERT, "insert"); + addOperator(api::CARD, "card"); + addOperator(api::COMPLEMENT, "complement"); + addOperator(api::JOIN, "join"); + addOperator(api::PRODUCT, "product"); + addOperator(api::TRANSPOSE, "transpose"); + addOperator(api::TCLOSURE, "tclosure"); break; case THEORY_DATATYPES: { - const std::vector<Type> types; - defineType("Tuple", getExprManager()->mkTupleType(types)); + const std::vector<api::Sort> types; + defineType("Tuple", d_solver->mkTupleSort(types)); addDatatypesOperators(); break; } case THEORY_STRINGS: - defineType("String", getExprManager()->stringType()); - defineType("RegLan", getExprManager()->regExpType()); - defineType("Int", getExprManager()->integerType()); + defineType("String", d_solver->getStringSort()); + defineType("RegLan", d_solver->getRegExpSort()); + defineType("Int", d_solver->getIntegerSort()); if (getLanguage() == language::input::LANG_SMTLIB_V2_6_1) { - defineVar("re.none", d_solver->mkRegexpEmpty().getExpr()); + defineVar("re.none", d_solver->mkRegexpEmpty()); } else { - defineVar("re.nostr", d_solver->mkRegexpEmpty().getExpr()); + defineVar("re.nostr", d_solver->mkRegexpEmpty()); } - defineVar("re.allchar", d_solver->mkRegexpSigma().getExpr()); + defineVar("re.allchar", d_solver->mkRegexpSigma()); addStringOperators(); break; case THEORY_UF: - Parser::addOperator(kind::APPLY_UF); + Parser::addOperator(api::APPLY_UF); if (!strictModeEnabled() && d_logic.hasCardinalityConstraints()) { - addOperator(kind::CARDINALITY_CONSTRAINT, "fmf.card"); - addOperator(kind::CARDINALITY_VALUE, "fmf.card.val"); + addOperator(api::CARDINALITY_CONSTRAINT, "fmf.card"); + addOperator(api::CARDINALITY_VALUE, "fmf.card.val"); } break; case THEORY_FP: - defineType("RoundingMode", getExprManager()->roundingModeType()); - defineType("Float16", getExprManager()->mkFloatingPointType(5, 11)); - defineType("Float32", getExprManager()->mkFloatingPointType(8, 24)); - defineType("Float64", getExprManager()->mkFloatingPointType(11, 53)); - defineType("Float128", getExprManager()->mkFloatingPointType(15, 113)); - - defineVar( - "RNE", - d_solver->mkRoundingMode(api::ROUND_NEAREST_TIES_TO_EVEN).getExpr()); - defineVar( - "roundNearestTiesToEven", - d_solver->mkRoundingMode(api::ROUND_NEAREST_TIES_TO_EVEN).getExpr()); - defineVar( - "RNA", - d_solver->mkRoundingMode(api::ROUND_NEAREST_TIES_TO_AWAY).getExpr()); - defineVar( - "roundNearestTiesToAway", - d_solver->mkRoundingMode(api::ROUND_NEAREST_TIES_TO_AWAY).getExpr()); - defineVar("RTP", - d_solver->mkRoundingMode(api::ROUND_TOWARD_POSITIVE).getExpr()); + defineType("RoundingMode", d_solver->getRoundingmodeSort()); + defineType("Float16", d_solver->mkFloatingPointSort(5, 11)); + defineType("Float32", d_solver->mkFloatingPointSort(8, 24)); + defineType("Float64", d_solver->mkFloatingPointSort(11, 53)); + defineType("Float128", d_solver->mkFloatingPointSort(15, 113)); + + defineVar("RNE", d_solver->mkRoundingMode(api::ROUND_NEAREST_TIES_TO_EVEN)); + defineVar("roundNearestTiesToEven", + d_solver->mkRoundingMode(api::ROUND_NEAREST_TIES_TO_EVEN)); + defineVar("RNA", d_solver->mkRoundingMode(api::ROUND_NEAREST_TIES_TO_AWAY)); + defineVar("roundNearestTiesToAway", + d_solver->mkRoundingMode(api::ROUND_NEAREST_TIES_TO_AWAY)); + defineVar("RTP", d_solver->mkRoundingMode(api::ROUND_TOWARD_POSITIVE)); defineVar("roundTowardPositive", - d_solver->mkRoundingMode(api::ROUND_TOWARD_POSITIVE).getExpr()); - defineVar("RTN", - d_solver->mkRoundingMode(api::ROUND_TOWARD_NEGATIVE).getExpr()); + d_solver->mkRoundingMode(api::ROUND_TOWARD_POSITIVE)); + defineVar("RTN", d_solver->mkRoundingMode(api::ROUND_TOWARD_NEGATIVE)); defineVar("roundTowardNegative", - d_solver->mkRoundingMode(api::ROUND_TOWARD_NEGATIVE).getExpr()); - defineVar("RTZ", - d_solver->mkRoundingMode(api::ROUND_TOWARD_ZERO).getExpr()); + d_solver->mkRoundingMode(api::ROUND_TOWARD_NEGATIVE)); + defineVar("RTZ", d_solver->mkRoundingMode(api::ROUND_TOWARD_ZERO)); defineVar("roundTowardZero", - d_solver->mkRoundingMode(api::ROUND_TOWARD_ZERO).getExpr()); + d_solver->mkRoundingMode(api::ROUND_TOWARD_ZERO)); addFloatingPointOperators(); break; @@ -434,8 +415,7 @@ void Smt2::addTheory(Theory theory) { case THEORY_SEP: // the Boolean sort is a placeholder here since we don't have type info // without type annotation - defineVar("sep.nil", - d_solver->mkSepNil(d_solver->getBooleanSort()).getExpr()); + defineVar("sep.nil", d_solver->mkSepNil(d_solver->getBooleanSort())); addSepOperators(); break; @@ -447,14 +427,15 @@ void Smt2::addTheory(Theory theory) { } } -void Smt2::addOperator(Kind kind, const std::string& name) { +void Smt2::addOperator(api::Kind kind, const std::string& name) +{ Debug("parser") << "Smt2::addOperator( " << kind << ", " << name << " )" << std::endl; Parser::addOperator(kind); operatorKindMap[name] = kind; } -void Smt2::addIndexedOperator(Kind tKind, +void Smt2::addIndexedOperator(api::Kind tKind, api::Kind opKind, const std::string& name) { @@ -462,7 +443,8 @@ void Smt2::addIndexedOperator(Kind tKind, d_indexedOpKindMap[name] = opKind; } -Kind Smt2::getOperatorKind(const std::string& name) const { +api::Kind Smt2::getOperatorKind(const std::string& name) const +{ // precondition: isOperatorEnabled(name) return operatorKindMap.find(name)->second; } @@ -513,7 +495,9 @@ bool Smt2::logicIsSet() { return d_logicSet; } -Expr Smt2::getExpressionForNameAndType(const std::string& name, Type t) { +api::Term Smt2::getExpressionForNameAndType(const std::string& name, + api::Sort t) +{ if (isAbstractValue(name)) { return mkAbstractValue(name); @@ -581,40 +565,40 @@ api::Op Smt2::mkIndexedOp(const std::string& name, return api::Op(); } -Expr Smt2::mkDefineFunRec( +api::Term Smt2::bindDefineFunRec( const std::string& fname, - const std::vector<std::pair<std::string, Type> >& sortedVarNames, - Type t, - std::vector<Expr>& flattenVars) + const std::vector<std::pair<std::string, api::Sort>>& sortedVarNames, + api::Sort t, + std::vector<api::Term>& flattenVars) { - std::vector<Type> sorts; - for (const std::pair<std::string, CVC4::Type>& svn : sortedVarNames) + std::vector<api::Sort> sorts; + for (const std::pair<std::string, api::Sort>& svn : sortedVarNames) { sorts.push_back(svn.second); } // make the flattened function type, add bound variables // to flattenVars if the defined function was given a function return type. - Type ft = mkFlatFunctionType(sorts, t, flattenVars); + api::Sort ft = mkFlatFunctionType(sorts, t, flattenVars); // allow overloading - return mkVar(fname, ft, ExprManager::VAR_FLAG_NONE, true); + return bindVar(fname, ft, ExprManager::VAR_FLAG_NONE, true); } void Smt2::pushDefineFunRecScope( - const std::vector<std::pair<std::string, Type> >& sortedVarNames, - Expr func, - const std::vector<Expr>& flattenVars, - std::vector<Expr>& bvs, + const std::vector<std::pair<std::string, api::Sort>>& sortedVarNames, + api::Term func, + const std::vector<api::Term>& flattenVars, + std::vector<api::Term>& bvs, bool bindingLevel) { pushScope(bindingLevel); // bound variables are those that are explicitly named in the preamble // of the define-fun(s)-rec command, we define them here - for (const std::pair<std::string, CVC4::Type>& svn : sortedVarNames) + for (const std::pair<std::string, api::Sort>& svn : sortedVarNames) { - Expr v = mkBoundVar(svn.first, svn.second); + api::Term v = bindBoundVar(svn.first, svn.second); bvs.push_back(v); } @@ -626,7 +610,7 @@ void Smt2::reset() { d_seenSetLogic = false; d_logic = LogicInfo(); operatorKindMap.clear(); - d_lastNamedTerm = std::pair<Expr, std::string>(); + d_lastNamedTerm = std::pair<api::Term, std::string>(); this->Parser::reset(); if( !strictModeEnabled() ) { @@ -645,8 +629,8 @@ Smt2::SynthFunFactory::SynthFunFactory( Smt2* smt2, const std::string& fun, bool isInv, - Type range, - std::vector<std::pair<std::string, CVC4::Type>>& sortedVarNames) + api::Sort range, + std::vector<std::pair<std::string, api::Sort>>& sortedVarNames) : d_smt2(smt2), d_fun(fun), d_isInv(isInv) { if (range.isNull()) @@ -657,38 +641,37 @@ Smt2::SynthFunFactory::SynthFunFactory( { smt2->parseError("Cannot use synth-fun with function return type."); } - std::vector<Type> varSorts; - for (const std::pair<std::string, CVC4::Type>& p : sortedVarNames) + std::vector<api::Sort> varSorts; + for (const std::pair<std::string, api::Sort>& p : sortedVarNames) { varSorts.push_back(p.second); } Debug("parser-sygus") << "Define synth fun : " << fun << std::endl; - Type synthFunType = - varSorts.size() > 0 - ? d_smt2->getExprManager()->mkFunctionType(varSorts, range) - : range; + api::Sort synthFunType = + varSorts.size() > 0 ? d_smt2->getSolver()->mkFunctionSort(varSorts, range) + : range; // we do not allow overloading for synth fun - d_synthFun = d_smt2->mkBoundVar(fun, synthFunType); + d_synthFun = d_smt2->bindBoundVar(fun, synthFunType); // set the sygus type to be range by default, which is overwritten below // if a grammar is provided d_sygusType = range; d_smt2->pushScope(true); - d_sygusVars = d_smt2->mkBoundVars(sortedVarNames); + d_sygusVars = d_smt2->bindBoundVars(sortedVarNames); } Smt2::SynthFunFactory::~SynthFunFactory() { d_smt2->popScope(); } -std::unique_ptr<Command> Smt2::SynthFunFactory::mkCommand(Type grammar) +std::unique_ptr<Command> Smt2::SynthFunFactory::mkCommand(api::Sort grammar) { Debug("parser-sygus") << "...read synth fun " << d_fun << std::endl; - return std::unique_ptr<Command>( - new SynthFunCommand(d_fun, - d_synthFun, - grammar.isNull() ? d_sygusType : grammar, - d_isInv, - d_sygusVars)); + return std::unique_ptr<Command>(new SynthFunCommand( + d_fun, + d_synthFun.getExpr(), + grammar.isNull() ? d_sygusType.getType() : grammar.getType(), + d_isInv, + api::termVectorToExprs(d_sygusVars))); } std::unique_ptr<Command> Smt2::invConstraint( @@ -705,7 +688,7 @@ std::unique_ptr<Command> Smt2::invConstraint( "arguments."); } - std::vector<Expr> terms; + std::vector<api::Term> terms; for (const std::string& name : names) { if (!isDeclared(name)) @@ -718,7 +701,8 @@ std::unique_ptr<Command> Smt2::invConstraint( terms.push_back(getVariable(name)); } - return std::unique_ptr<Command>(new SygusInvConstraintCommand(terms)); + return std::unique_ptr<Command>( + new SygusInvConstraintCommand(api::termVectorToExprs(terms))); } Command* Smt2::setLogic(std::string name, bool fromCommand) @@ -932,33 +916,32 @@ void Smt2::includeFile(const std::string& filename) { parseError("Couldn't open include file `" + path + "'"); } } - bool Smt2::isAbstractValue(const std::string& name) { return name.length() >= 2 && name[0] == '@' && name[1] != '0' && name.find_first_not_of("0123456789", 1) == std::string::npos; } -Expr Smt2::mkAbstractValue(const std::string& name) +api::Term Smt2::mkAbstractValue(const std::string& name) { assert(isAbstractValue(name)); // remove the '@' - return getExprManager()->mkConst(AbstractValue(Integer(name.substr(1)))); + return d_solver->mkAbstractValue(name.substr(1)); } -void Smt2::mkSygusConstantsForType( const Type& type, std::vector<CVC4::Expr>& ops ) { +void Smt2::mkSygusConstantsForType(const api::Sort& type, + std::vector<api::Term>& ops) +{ if( type.isInteger() ){ - ops.push_back(getExprManager()->mkConst(Rational(0))); - ops.push_back(getExprManager()->mkConst(Rational(1))); + ops.push_back(d_solver->mkReal(0)); + ops.push_back(d_solver->mkReal(1)); }else if( type.isBitVector() ){ - unsigned sz = ((BitVectorType)type).getSize(); - BitVector bval0(sz, (unsigned int)0); - ops.push_back( getExprManager()->mkConst(bval0) ); - BitVector bval1(sz, (unsigned int)1); - ops.push_back( getExprManager()->mkConst(bval1) ); + uint32_t sz = type.getBVSize(); + ops.push_back(d_solver->mkBitVector(sz, 0)); + ops.push_back(d_solver->mkBitVector(sz, 1)); }else if( type.isBoolean() ){ - ops.push_back(getExprManager()->mkConst(true)); - ops.push_back(getExprManager()->mkConst(false)); + ops.push_back(d_solver->mkTrue()); + ops.push_back(d_solver->mkFalse()); } //TODO : others? } @@ -969,36 +952,37 @@ void Smt2::processSygusGTerm( CVC4::SygusGTerm& sgt, int index, std::vector<CVC4::Datatype>& datatypes, - std::vector<CVC4::Type>& sorts, + std::vector<api::Sort>& sorts, std::vector<std::vector<ParseOp>>& ops, std::vector<std::vector<std::string>>& cnames, - std::vector<std::vector<std::vector<CVC4::Type>>>& cargs, + std::vector<std::vector<std::vector<api::Sort>>>& cargs, std::vector<bool>& allow_const, std::vector<std::vector<std::string>>& unresolved_gterm_sym, - const std::vector<CVC4::Expr>& sygus_vars, - std::map<CVC4::Type, CVC4::Type>& sygus_to_builtin, - std::map<CVC4::Type, CVC4::Expr>& sygus_to_builtin_expr, - CVC4::Type& ret, + const std::vector<api::Term>& sygus_vars, + std::map<api::Sort, api::Sort>& sygus_to_builtin, + std::map<api::Sort, api::Term>& sygus_to_builtin_expr, + api::Sort& ret, bool isNested) { if (sgt.d_gterm_type == SygusGTerm::gterm_op) { Debug("parser-sygus") << "Add " << sgt.d_op << " to datatype " << index << std::endl; - Kind oldKind; - Kind newKind = kind::UNDEFINED_KIND; + api::Kind oldKind; + api::Kind newKind = api::UNDEFINED_KIND; //convert to UMINUS if one child of MINUS - if (sgt.d_children.size() == 1 && sgt.d_op.d_kind == kind::MINUS) + if (sgt.d_children.size() == 1 && sgt.d_op.d_kind == api::MINUS) { - oldKind = kind::MINUS; - newKind = kind::UMINUS; + oldKind = api::MINUS; + newKind = api::UMINUS; } - if( newKind!=kind::UNDEFINED_KIND ){ + if (newKind != api::UNDEFINED_KIND) + { Debug("parser-sygus") << "Replace " << sgt.d_op.d_kind << " with " << newKind << std::endl; sgt.d_op.d_kind = newKind; - std::string oldName = kind::kindToString(oldKind); - std::string newName = kind::kindToString(newKind); + std::string oldName = api::kindToString(oldKind); + std::string newName = api::kindToString(newKind); size_t pos = 0; if((pos = sgt.d_name.find(oldName, pos)) != std::string::npos){ sgt.d_name.replace(pos, oldName.length(), newName); @@ -1006,22 +990,32 @@ void Smt2::processSygusGTerm( } ops[index].push_back(sgt.d_op); cnames[index].push_back( sgt.d_name ); - cargs[index].push_back( std::vector< CVC4::Type >() ); + cargs[index].push_back(std::vector<api::Sort>()); for( unsigned i=0; i<sgt.d_children.size(); i++ ){ std::stringstream ss; ss << datatypes[index].getName() << "_" << ops[index].size() << "_arg_" << i; std::string sub_dname = ss.str(); //add datatype for child - Type null_type; + api::Sort null_type; pushSygusDatatypeDef( null_type, sub_dname, datatypes, sorts, ops, cnames, cargs, allow_const, unresolved_gterm_sym ); int sub_dt_index = datatypes.size()-1; //process child - Type sub_ret; + api::Sort sub_ret; processSygusGTerm( sgt.d_children[i], sub_dt_index, datatypes, sorts, ops, cnames, cargs, allow_const, unresolved_gterm_sym, sygus_vars, sygus_to_builtin, sygus_to_builtin_expr, sub_ret, true ); //process the nested gterm (either pop the last datatype, or flatten the argument) - Type tt = processSygusNestedGTerm( sub_dt_index, sub_dname, datatypes, sorts, ops, cnames, cargs, allow_const, unresolved_gterm_sym, - sygus_to_builtin, sygus_to_builtin_expr, sub_ret ); + api::Sort tt = processSygusNestedGTerm(sub_dt_index, + sub_dname, + datatypes, + sorts, + ops, + cnames, + cargs, + allow_const, + unresolved_gterm_sym, + sygus_to_builtin, + sygus_to_builtin_expr, + sub_ret); cargs[index].back().push_back(tt); } } @@ -1030,7 +1024,7 @@ void Smt2::processSygusGTerm( if( sgt.getNumChildren()!=0 ){ parseError("Bad syntax for Sygus Constant."); } - std::vector< Expr > consts; + std::vector<api::Term> consts; mkSygusConstantsForType( sgt.d_type, consts ); Debug("parser-sygus") << "...made " << consts.size() << " constants." << std::endl; for( unsigned i=0; i<consts.size(); i++ ){ @@ -1041,7 +1035,7 @@ void Smt2::processSygusGTerm( constOp.d_expr = consts[i]; ops[index].push_back(constOp); cnames[index].push_back( ss.str() ); - cargs[index].push_back( std::vector< CVC4::Type >() ); + cargs[index].push_back(std::vector<api::Sort>()); } allow_const[index] = true; } @@ -1053,7 +1047,8 @@ void Smt2::processSygusGTerm( } Debug("parser-sygus") << "...process " << sygus_vars.size() << " variables." << std::endl; for( unsigned i=0; i<sygus_vars.size(); i++ ){ - if( sygus_vars[i].getType()==sgt.d_type ){ + if (sygus_vars[i].getSort() == sgt.d_type) + { std::stringstream ss; ss << sygus_vars[i]; Debug("parser-sygus") << "...add for variable " << ss.str() << std::endl; @@ -1061,7 +1056,7 @@ void Smt2::processSygusGTerm( varOp.d_expr = sygus_vars[i]; ops[index].push_back(varOp); cnames[index].push_back( ss.str() ); - cargs[index].push_back( std::vector< CVC4::Type >() ); + cargs[index].push_back(std::vector<api::Sort>()); } } } @@ -1092,13 +1087,13 @@ void Smt2::processSygusGTerm( } bool Smt2::pushSygusDatatypeDef( - Type t, + api::Sort t, std::string& dname, std::vector<CVC4::Datatype>& datatypes, - std::vector<CVC4::Type>& sorts, + std::vector<api::Sort>& sorts, std::vector<std::vector<ParseOp>>& ops, std::vector<std::vector<std::string>>& cnames, - std::vector<std::vector<std::vector<CVC4::Type>>>& cargs, + std::vector<std::vector<std::vector<api::Sort>>>& cargs, std::vector<bool>& allow_const, std::vector<std::vector<std::string>>& unresolved_gterm_sym) { @@ -1106,7 +1101,7 @@ bool Smt2::pushSygusDatatypeDef( datatypes.push_back(Datatype(getExprManager(), dname)); ops.push_back(std::vector<ParseOp>()); cnames.push_back(std::vector<std::string>()); - cargs.push_back(std::vector<std::vector<CVC4::Type> >()); + cargs.push_back(std::vector<std::vector<api::Sort>>()); allow_const.push_back(false); unresolved_gterm_sym.push_back(std::vector< std::string >()); return true; @@ -1114,10 +1109,10 @@ bool Smt2::pushSygusDatatypeDef( bool Smt2::popSygusDatatypeDef( std::vector<CVC4::Datatype>& datatypes, - std::vector<CVC4::Type>& sorts, + std::vector<api::Sort>& sorts, std::vector<std::vector<ParseOp>>& ops, std::vector<std::vector<std::string>>& cnames, - std::vector<std::vector<std::vector<CVC4::Type>>>& cargs, + std::vector<std::vector<std::vector<api::Sort>>>& cargs, std::vector<bool>& allow_const, std::vector<std::vector<std::string>>& unresolved_gterm_sym) { @@ -1131,21 +1126,21 @@ bool Smt2::popSygusDatatypeDef( return true; } -Type Smt2::processSygusNestedGTerm( +api::Sort Smt2::processSygusNestedGTerm( int sub_dt_index, std::string& sub_dname, std::vector<CVC4::Datatype>& datatypes, - std::vector<CVC4::Type>& sorts, + std::vector<api::Sort>& sorts, std::vector<std::vector<ParseOp>>& ops, std::vector<std::vector<std::string>>& cnames, - std::vector<std::vector<std::vector<CVC4::Type>>>& cargs, + std::vector<std::vector<std::vector<api::Sort>>>& cargs, std::vector<bool>& allow_const, std::vector<std::vector<std::string>>& unresolved_gterm_sym, - std::map<CVC4::Type, CVC4::Type>& sygus_to_builtin, - std::map<CVC4::Type, CVC4::Expr>& sygus_to_builtin_expr, - Type sub_ret) + std::map<api::Sort, api::Sort>& sygus_to_builtin, + std::map<api::Sort, CVC4::api::Term>& sygus_to_builtin_expr, + api::Sort sub_ret) { - Type t = sub_ret; + api::Sort t = sub_ret; Debug("parser-sygus") << "Argument is "; if( t.isNull() ){ //then, it is the datatype we constructed, which should have a single constructor @@ -1156,13 +1151,16 @@ Type Smt2::processSygusNestedGTerm( parseError(std::string("Internal error : datatype for nested gterm does not have a constructor.")); } ParseOp op = ops[sub_dt_index][0]; - Type curr_t; + api::Sort curr_t; if (!op.d_expr.isNull() && (op.d_expr.isConst() || cargs[sub_dt_index][0].empty())) { - Expr sop = op.d_expr; - curr_t = sop.getType(); - Debug("parser-sygus") << ": it is constant/0-arg cons " << sop << " with type " << sop.getType() << ", debug=" << sop.isConst() << " " << cargs[sub_dt_index][0].size() << std::endl; + api::Term sop = op.d_expr; + curr_t = sop.getSort(); + Debug("parser-sygus") + << ": it is constant/0-arg cons " << sop << " with type " + << sop.getSort() << ", debug=" << sop.isConst() << " " + << cargs[sub_dt_index][0].size() << std::endl; // only cache if it is a singleton datatype (has unique expr) if (ops[sub_dt_index].size() == 1) { @@ -1176,24 +1174,29 @@ Type Smt2::processSygusNestedGTerm( } else { - std::vector< Expr > children; + std::vector<api::Term> children; for( unsigned i=0; i<cargs[sub_dt_index][0].size(); i++ ){ - std::map< CVC4::Type, CVC4::Expr >::iterator it = sygus_to_builtin_expr.find( cargs[sub_dt_index][0][i] ); + std::map<api::Sort, CVC4::api::Term>::iterator it = + sygus_to_builtin_expr.find(cargs[sub_dt_index][0][i]); if( it==sygus_to_builtin_expr.end() ){ if( sygus_to_builtin.find( cargs[sub_dt_index][0][i] )==sygus_to_builtin.end() ){ std::stringstream ss; ss << "Missing builtin type for type " << cargs[sub_dt_index][0][i] << "!" << std::endl; ss << "Builtin types are currently : " << std::endl; - for( std::map< CVC4::Type, CVC4::Type >::iterator itb = sygus_to_builtin.begin(); itb != sygus_to_builtin.end(); ++itb ){ + for (std::map<api::Sort, api::Sort>::iterator itb = + sygus_to_builtin.begin(); + itb != sygus_to_builtin.end(); + ++itb) + { ss << " " << itb->first << " -> " << itb->second << std::endl; } parseError(ss.str()); } - Type bt = sygus_to_builtin[cargs[sub_dt_index][0][i]]; + api::Sort bt = sygus_to_builtin[cargs[sub_dt_index][0][i]]; Debug("parser-sygus") << ": child " << i << " introduce type elem for " << cargs[sub_dt_index][0][i] << " " << bt << std::endl; std::stringstream ss; ss << t << "_x_" << i; - Expr bv = mkBoundVar(ss.str(), bt); + api::Term bv = bindBoundVar(ss.str(), bt); children.push_back( bv ); d_sygus_bound_var_type[bv] = cargs[sub_dt_index][0][i]; }else{ @@ -1201,9 +1204,10 @@ Type Smt2::processSygusNestedGTerm( children.push_back( it->second ); } } - Expr e = applyParseOp(op, children); - Debug("parser-sygus") << ": constructed " << e << ", which has type " << e.getType() << std::endl; - curr_t = e.getType(); + api::Term e = applyParseOp(op, children); + Debug("parser-sygus") << ": constructed " << e << ", which has type " + << e.getSort() << std::endl; + curr_t = e.getSort(); sygus_to_builtin_expr[t] = e; } sorts[sub_dt_index] = curr_t; @@ -1221,12 +1225,12 @@ Type Smt2::processSygusNestedGTerm( void Smt2::setSygusStartIndex(const std::string& fun, int startIndex, std::vector<CVC4::Datatype>& datatypes, - std::vector<CVC4::Type>& sorts, + std::vector<api::Sort>& sorts, std::vector<std::vector<ParseOp>>& ops) { if( startIndex>0 ){ CVC4::Datatype tmp_dt = datatypes[0]; - Type tmp_sort = sorts[0]; + api::Sort tmp_sort = sorts[0]; std::vector<ParseOp> tmp_ops; tmp_ops.insert( tmp_ops.end(), ops[0].begin(), ops[0].end() ); datatypes[0] = datatypes[startIndex]; @@ -1247,9 +1251,9 @@ void Smt2::setSygusStartIndex(const std::string& fun, void Smt2::mkSygusDatatype(CVC4::Datatype& dt, std::vector<ParseOp>& ops, std::vector<std::string>& cnames, - std::vector<std::vector<CVC4::Type>>& cargs, + std::vector<std::vector<api::Sort>>& cargs, std::vector<std::string>& unresolved_gterm_sym, - std::map<CVC4::Type, CVC4::Type>& sygus_to_builtin) + std::map<api::Sort, api::Sort>& sygus_to_builtin) { Debug("parser-sygus") << "Making sygus datatype " << dt.getName() << std::endl; Debug("parser-sygus") << " add constructors..." << std::endl; @@ -1295,28 +1299,29 @@ void Smt2::mkSygusDatatype(CVC4::Datatype& dt, Debug("parser-sygus") << "--> Duplicate gterm operator : " << ops[i] << std::endl; // make into define-fun - std::vector<Type> ltypes; + std::vector<api::Sort> ltypes; for (unsigned j = 0, size = cargs[i].size(); j < size; j++) { ltypes.push_back(sygus_to_builtin[cargs[i][j]]); } - std::vector<Expr> largs; - Expr lbvl = makeSygusBoundVarList(dt, i, ltypes, largs); + std::vector<api::Term> largs; + api::Term lbvl = makeSygusBoundVarList(dt, i, ltypes, largs); // make the let_body - Expr body = applyParseOp(ops[i], largs); + api::Term body = applyParseOp(ops[i], largs); // replace by lambda ParseOp pLam; - pLam.d_expr = getExprManager()->mkExpr(kind::LAMBDA, lbvl, body); + pLam.d_expr = d_solver->mkTerm(api::LAMBDA, lbvl, body); ops[i] = pLam; Debug("parser-sygus") << " ...replace op : " << ops[i] << std::endl; // callback prints as the expression - spc = std::make_shared<printer::SygusExprPrintCallback>(body, largs); + spc = std::make_shared<printer::SygusExprPrintCallback>( + body.getExpr(), api::termVectorToExprs(largs)); } else { - Expr sop = ops[i].d_expr; - if (!sop.isNull() && sop.getType().isBitVector() && sop.isConst()) + api::Term sop = ops[i].d_expr; + if (!sop.isNull() && sop.getSort().isBitVector() && sop.isConst()) { Debug("parser-sygus") << "--> Bit-vector constant " << sop << " (" << cnames[i] << ")" << std::endl; @@ -1326,22 +1331,22 @@ void Smt2::mkSygusDatatype(CVC4::Datatype& dt, // the given name. spc = std::make_shared<printer::SygusNamedPrintCallback>(cnames[i]); } - else if (!sop.isNull() && sop.getKind() == kind::VARIABLE) + else if (!sop.isNull() && sop.getKind() == api::VARIABLE) { Debug("parser-sygus") << "--> Defined function " << ops[i] << std::endl; // turn f into (lammbda (x) (f x)) // in a degenerate case, ops[i] may be a defined constant, // in which case we do not replace by a lambda. - if (sop.getType().isFunction()) + if (sop.getSort().isFunction()) { - std::vector<Type> ftypes = - static_cast<FunctionType>(sop.getType()).getArgTypes(); - std::vector<Expr> largs; - Expr lbvl = makeSygusBoundVarList(dt, i, ftypes, largs); + std::vector<api::Sort> ftypes = + sop.getSort().getFunctionDomainSorts(); + std::vector<api::Term> largs; + api::Term lbvl = makeSygusBoundVarList(dt, i, ftypes, largs); largs.insert(largs.begin(), sop); - Expr body = getExprManager()->mkExpr(kind::APPLY_UF, largs); - ops[i].d_expr = getExprManager()->mkExpr(kind::LAMBDA, lbvl, body); + api::Term body = d_solver->mkTerm(api::APPLY_UF, largs); + ops[i].d_expr = d_solver->mkTerm(api::LAMBDA, lbvl, body); Debug("parser-sygus") << " ...replace op : " << ops[i] << std::endl; } @@ -1364,15 +1369,22 @@ void Smt2::mkSygusDatatype(CVC4::Datatype& dt, cnames[i] = ss.str(); Debug("parser-sygus") << " construct the datatype " << cnames[i] << "..." << std::endl; + // Add the sygus constructor, either using the expression operator of // ops[i], or the kind. if (!ops[i].d_expr.isNull()) { - dt.addSygusConstructor(ops[i].d_expr, cnames[i], cargs[i], spc); + dt.addSygusConstructor(ops[i].d_expr.getExpr(), + cnames[i], + api::sortVectorToTypes(cargs[i]), + spc); } - else if (ops[i].d_kind != kind::NULL_EXPR) + else if (ops[i].d_kind != api::NULL_EXPR) { - dt.addSygusConstructor(ops[i].d_kind, cnames[i], cargs[i], spc); + dt.addSygusConstructor(extToIntKind(ops[i].d_kind), + cnames[i], + api::sortVectorToTypes(cargs[i]), + spc); } else { @@ -1387,36 +1399,38 @@ void Smt2::mkSygusDatatype(CVC4::Datatype& dt, Debug("parser-sygus") << " add constructors for unresolved symbols..." << std::endl; if( !unresolved_gterm_sym.empty() ){ - std::vector< Type > types; + std::vector<api::Sort> types; Debug("parser-sygus") << "...resolve " << unresolved_gterm_sym.size() << " symbols..." << std::endl; for( unsigned i=0; i<unresolved_gterm_sym.size(); i++ ){ Debug("parser-sygus") << " resolve : " << unresolved_gterm_sym[i] << std::endl; if( isUnresolvedType(unresolved_gterm_sym[i]) ){ Debug("parser-sygus") << " it is an unresolved type." << std::endl; - Type t = getSort(unresolved_gterm_sym[i]); + api::Sort t = getSort(unresolved_gterm_sym[i]); if( std::find( types.begin(), types.end(), t )==types.end() ){ types.push_back( t ); //identity element - Type bt = dt.getSygusType(); + api::Sort bt = dt.getSygusType(); Debug("parser-sygus") << ": make identity function for " << bt << ", argument type " << t << std::endl; std::stringstream ss; ss << t << "_x"; - Expr var = mkBoundVar(ss.str(), bt); - std::vector<Expr> lchildren; - lchildren.push_back( - getExprManager()->mkExpr(kind::BOUND_VAR_LIST, var)); + api::Term var = bindBoundVar(ss.str(), bt); + std::vector<api::Term> lchildren; + lchildren.push_back(d_solver->mkTerm(api::BOUND_VAR_LIST, var)); lchildren.push_back(var); - Expr id_op = getExprManager()->mkExpr(kind::LAMBDA, lchildren); + api::Term id_op = d_solver->mkTerm(api::LAMBDA, lchildren); // empty sygus callback (should not be printed) std::shared_ptr<SygusPrintCallback> sepc = std::make_shared<printer::SygusEmptyPrintCallback>(); //make the sygus argument list - std::vector< Type > id_carg; + std::vector<api::Sort> id_carg; id_carg.push_back( t ); - dt.addSygusConstructor(id_op, unresolved_gterm_sym[i], id_carg, sepc); + dt.addSygusConstructor(id_op.getExpr(), + unresolved_gterm_sym[i], + api::sortVectorToTypes(id_carg), + sepc); //add to operators ParseOp idOp; @@ -1432,31 +1446,30 @@ void Smt2::mkSygusDatatype(CVC4::Datatype& dt, } } -Expr Smt2::makeSygusBoundVarList(Datatype& dt, - unsigned i, - const std::vector<Type>& ltypes, - std::vector<Expr>& lvars) +api::Term Smt2::makeSygusBoundVarList(CVC4::Datatype& dt, + unsigned i, + const std::vector<api::Sort>& ltypes, + std::vector<api::Term>& lvars) { for (unsigned j = 0, size = ltypes.size(); j < size; j++) { std::stringstream ss; ss << dt.getName() << "_x_" << i << "_" << j; - Expr v = mkBoundVar(ss.str(), ltypes[j]); + api::Term v = bindBoundVar(ss.str(), ltypes[j]); lvars.push_back(v); } - return getExprManager()->mkExpr(kind::BOUND_VAR_LIST, lvars); + return d_solver->mkTerm(api::BOUND_VAR_LIST, lvars); } -void Smt2::addSygusConstructorTerm(Datatype& dt, - Expr term, - std::map<Expr, Type>& ntsToUnres) const +void Smt2::addSygusConstructorTerm( + Datatype& dt, + api::Term term, + std::map<api::Term, api::Sort>& ntsToUnres) const { Trace("parser-sygus2") << "Add sygus cons term " << term << std::endl; - // Ensure that we do type checking here to catch sygus constructors with - // malformed builtin operators. The argument "true" to getType here forces - // a recursive well-typedness check. - term.getType(true); - // purify each occurrence of a non-terminal symbol in term, replace by + // At this point, we should know that dt is well founded, and that its + // builtin sygus operators are well-typed. + // Now, purify each occurrence of a non-terminal symbol in term, replace by // free variables. These become arguments to constructors. Notice we must do // a tree traversal in this function, since unique paths to the same term // should be treated as distinct terms. @@ -1464,7 +1477,7 @@ void Smt2::addSygusConstructorTerm(Datatype& dt, // this does not lead to exponential behavior with respect to input size. std::vector<api::Term> args; std::vector<api::Sort> cargs; - api::Term op = purifySygusGTerm(api::Term(term), ntsToUnres, args, cargs); + api::Term op = purifySygusGTerm(term, ntsToUnres, args, cargs); std::stringstream ssCName; ssCName << op.getKind(); Trace("parser-sygus2") << "Purified operator " << op @@ -1487,14 +1500,14 @@ void Smt2::addSygusConstructorTerm(Datatype& dt, } api::Term Smt2::purifySygusGTerm(api::Term term, - std::map<Expr, Type>& ntsToUnres, + std::map<api::Term, api::Sort>& ntsToUnres, std::vector<api::Term>& args, std::vector<api::Sort>& cargs) const { Trace("parser-sygus2-debug") << "purifySygusGTerm: " << term << " #nchild=" << term.getExpr().getNumChildren() << std::endl; - std::map<Expr, Type>::iterator itn = ntsToUnres.find(term.getExpr()); + std::map<api::Term, api::Sort>::iterator itn = ntsToUnres.find(term); if (itn != ntsToUnres.end()) { api::Term ret = d_solver->mkVar(term.getSort()); @@ -1526,35 +1539,35 @@ api::Term Smt2::purifySygusGTerm(api::Term term, } void Smt2::addSygusConstructorVariables(Datatype& dt, - const std::vector<Expr>& sygusVars, - Type type) const + const std::vector<api::Term>& sygusVars, + api::Sort type) const { // each variable of appropriate type becomes a sygus constructor in dt. for (unsigned i = 0, size = sygusVars.size(); i < size; i++) { - Expr v = sygusVars[i]; - if (v.getType() == type) + api::Term v = sygusVars[i]; + if (v.getSort() == type) { std::stringstream ss; ss << v; - std::vector<CVC4::Type> cargs; - dt.addSygusConstructor(v, ss.str(), cargs); + std::vector<api::Sort> cargs; + dt.addSygusConstructor( + v.getExpr(), ss.str(), api::sortVectorToTypes(cargs)); } } } InputLanguage Smt2::getLanguage() const { - ExprManager* em = getExprManager(); - return em->getOptions().getInputLanguage(); + return getExprManager()->getOptions().getInputLanguage(); } -void Smt2::parseOpApplyTypeAscription(ParseOp& p, Type type) +void Smt2::parseOpApplyTypeAscription(ParseOp& p, api::Sort type) { Debug("parser") << "parseOpApplyTypeAscription : " << p << " " << type << std::endl; // (as const (Array T1 T2)) - if (p.d_kind == kind::STORE_ALL) + if (p.d_kind == api::STORE_ALL) { if (!type.isArray()) { @@ -1576,6 +1589,7 @@ void Smt2::parseOpApplyTypeAscription(ParseOp& p, Type type) if (isDeclared(p.d_name, SYM_VARIABLE)) { p.d_expr = getExpressionForNameAndType(p.d_name, type); + p.d_name = std::string(""); } if (p.d_expr.isNull()) { @@ -1586,17 +1600,18 @@ void Smt2::parseOpApplyTypeAscription(ParseOp& p, Type type) } } Trace("parser-qid") << "Resolve ascription " << type << " on " << p.d_expr; - Trace("parser-qid") << " " << p.d_expr.getKind() << " " << p.d_expr.getType(); + Trace("parser-qid") << " " << p.d_expr.getKind() << " " << p.d_expr.getSort(); Trace("parser-qid") << std::endl; // otherwise, we process the type ascription p.d_expr = applyTypeAscription(api::Term(p.d_expr), api::Sort(type)).getExpr(); } -Expr Smt2::parseOpToExpr(ParseOp& p) +api::Term Smt2::parseOpToExpr(ParseOp& p) { - Expr expr; - if (p.d_kind != kind::NULL_EXPR || !p.d_type.isNull()) + Debug("parser") << "parseOpToExpr: " << p << std::endl; + api::Term expr; + if (p.d_kind != api::NULL_EXPR || !p.d_type.isNull()) { parseError( "Bad syntax for qualified identifier operator in term position."); @@ -1611,7 +1626,7 @@ Expr Smt2::parseOpToExpr(ParseOp& p) && p.d_name.find_first_not_of("0123456789", 1) == std::string::npos) { // allow unary minus in sygus version 1 - expr = getExprManager()->mkConst(Rational(p.d_name)); + expr = d_solver->mkReal(p.d_name); } else { @@ -1628,38 +1643,41 @@ Expr Smt2::parseOpToExpr(ParseOp& p) return expr; } -Expr Smt2::applyParseOp(ParseOp& p, std::vector<Expr>& args) +api::Term Smt2::applyParseOp(ParseOp& p, std::vector<api::Term>& args) { bool isBuiltinOperator = false; // the builtin kind of the overall return expression - Kind kind = kind::NULL_EXPR; + api::Kind kind = api::NULL_EXPR; // First phase: process the operator if (Debug.isOn("parser")) { Debug("parser") << "applyParseOp: " << p << " to:" << std::endl; - for (std::vector<Expr>::iterator i = args.begin(); i != args.end(); ++i) + for (std::vector<api::Term>::iterator i = args.begin(); i != args.end(); + ++i) { Debug("parser") << "++ " << *i << std::endl; } } api::Op op; - if (p.d_kind != kind::NULL_EXPR) + if (p.d_kind != api::NULL_EXPR) { // It is a special case, e.g. tupSel or array constant specification. // We have to wait until the arguments are parsed to resolve it. } else if (!p.d_expr.isNull()) { - // An explicit operator, e.g. an indexed symbol. - args.insert(args.begin(), p.d_expr); - Kind fkind = getKindForFunction(p.d_expr); - if (fkind != kind::UNDEFINED_KIND) + // An explicit operator, e.g. an apply function + api::Kind fkind = getKindForFunction(p.d_expr); + if (fkind != api::UNDEFINED_KIND) { // Some operators may require a specific kind. // Testers are handled differently than other indexed operators, // since they require a kind. kind = fkind; + Debug("parser") << "Got function kind " << kind << " for expression " + << std::endl; } + args.insert(args.begin(), p.d_expr); } else if (!p.d_op.isNull()) { @@ -1678,7 +1696,7 @@ Expr Smt2::applyParseOp(ParseOp& p, std::vector<Expr>& args) { // A non-built-in function application, get the expression checkDeclaration(p.d_name, CHECK_DECLARED, SYM_VARIABLE); - Expr v = getVariable(p.d_name); + api::Term v = getVariable(p.d_name); if (!v.isNull()) { checkFunctionLike(v); @@ -1691,12 +1709,13 @@ Expr Smt2::applyParseOp(ParseOp& p, std::vector<Expr>& args) // Could not find the expression. It may be an overloaded symbol, // in which case we may find it after knowing the types of its // arguments. - std::vector<Type> argTypes; - for (std::vector<Expr>::iterator i = args.begin(); i != args.end(); ++i) + std::vector<api::Sort> argTypes; + for (std::vector<api::Term>::iterator i = args.begin(); i != args.end(); + ++i) { - argTypes.push_back((*i).getType()); + argTypes.push_back((*i).getSort()); } - Expr fop = getOverloadedFunctionForTypes(p.d_name, argTypes); + api::Term fop = getOverloadedFunctionForTypes(p.d_name, argTypes); if (!fop.isNull()) { checkFunctionLike(fop); @@ -1715,13 +1734,13 @@ Expr Smt2::applyParseOp(ParseOp& p, std::vector<Expr>& args) // Second phase: apply the arguments to the parse op ExprManager* em = getExprManager(); // handle special cases - if (p.d_kind == kind::STORE_ALL && !p.d_type.isNull()) + if (p.d_kind == api::STORE_ALL && !p.d_type.isNull()) { if (args.size() != 1) { parseError("Too many arguments to array constant."); } - Expr constVal = args[0]; + api::Term constVal = args[0]; if (!constVal.isConst()) { // To parse array constants taking reals whose values are specified by @@ -1732,12 +1751,13 @@ Expr Smt2::applyParseOp(ParseOp& p, std::vector<Expr>& args) // like 5.0 which are converted to (/ 5 1) to distinguish them from // integer constants. We must ensure numerator and denominator are // constant and the denominator is non-zero. - if (constVal.getKind() == kind::DIVISION && constVal[0].isConst() + if (constVal.getKind() == api::DIVISION && constVal[0].isConst() && constVal[1].isConst() - && !constVal[1].getConst<Rational>().isZero()) + && !constVal[1].getExpr().getConst<Rational>().isZero()) { - constVal = em->mkConst(constVal[0].getConst<Rational>() - / constVal[1].getConst<Rational>()); + std::stringstream sdiv; + sdiv << constVal[0] << "/" << constVal[1]; + constVal = d_solver->mkReal(sdiv.str()); } if (!constVal.isConst()) { @@ -1748,47 +1768,52 @@ Expr Smt2::applyParseOp(ParseOp& p, std::vector<Expr>& args) parseError(ss.str()); } } - ArrayType aqtype = static_cast<ArrayType>(p.d_type); - if (!aqtype.getConstituentType().isComparableTo(constVal.getType())) + if (!p.d_type.getArrayElementSort().isComparableTo(constVal.getSort())) { std::stringstream ss; ss << "type mismatch inside array constant term:" << std::endl << "array type: " << p.d_type << std::endl - << "expected const type: " << aqtype.getConstituentType() << std::endl - << "computed const type: " << constVal.getType(); + << "expected const type: " << p.d_type.getArrayElementSort() + << std::endl + << "computed const type: " << constVal.getSort(); parseError(ss.str()); } - return em->mkConst(ArrayStoreAll(p.d_type, constVal)); + api::Term ret = d_solver->mkConstArray(p.d_type, constVal); + Debug("parser") << "applyParseOp: return store all " << ret << std::endl; + return ret; } - else if (p.d_kind == kind::APPLY_SELECTOR && !p.d_expr.isNull()) + else if (p.d_kind == api::APPLY_SELECTOR && !p.d_expr.isNull()) { // tuple selector case - Integer x = p.d_expr.getConst<Rational>().getNumerator(); + Integer x = p.d_expr.getExpr().getConst<Rational>().getNumerator(); if (!x.fitsUnsignedInt()) { parseError("index of tupSel is larger than size of unsigned int"); } unsigned int n = x.toUnsignedInt(); - if (args.size() > 1) + if (args.size() != 1) { - parseError("tupSel applied to more than one tuple argument"); + parseError("tupSel should only be applied to one tuple argument"); } - Type t = args[0].getType(); + api::Sort t = args[0].getSort(); if (!t.isTuple()) { parseError("tupSel applied to non-tuple"); } - size_t length = ((DatatypeType)t).getTupleLength(); + size_t length = t.getTupleLength(); if (n >= length) { std::stringstream ss; ss << "tuple is of length " << length << "; cannot access index " << n; parseError(ss.str()); } - const Datatype& dt = ((DatatypeType)t).getDatatype(); - return em->mkExpr(kind::APPLY_SELECTOR, dt[0][n].getSelector(), args); + const Datatype& dt = ((DatatypeType)t.getType()).getDatatype(); + api::Term ret = d_solver->mkTerm( + api::APPLY_SELECTOR, api::Term(dt[0][n].getSelector()), args[0]); + Debug("parser") << "applyParseOp: return selector " << ret << std::endl; + return ret; } - else if (p.d_kind != kind::NULL_EXPR) + else if (p.d_kind != api::NULL_EXPR) { // it should not have an expression or type specified at this point if (!p.d_expr.isNull() || !p.d_type.isNull()) @@ -1802,43 +1827,47 @@ Expr Smt2::applyParseOp(ParseOp& p, std::vector<Expr>& args) } else if (isBuiltinOperator) { + Trace("ajr-temp") << "mkTerm builtin operator" << std::endl; if (!em->getOptions().getUfHo() - && (kind == kind::EQUAL || kind == kind::DISTINCT)) + && (kind == api::EQUAL || kind == api::DISTINCT)) { // need --uf-ho if these operators are applied over function args - for (std::vector<Expr>::iterator i = args.begin(); i != args.end(); ++i) + for (std::vector<api::Term>::iterator i = args.begin(); i != args.end(); + ++i) { - if ((*i).getType().isFunction()) + if ((*i).getSort().isFunction()) { parseError( "Cannot apply equalty to functions unless --uf-ho is set."); } } } - if (!strictModeEnabled() && (kind == kind::AND || kind == kind::OR) + if (!strictModeEnabled() && (kind == api::AND || kind == api::OR) && args.size() == 1) { // Unary AND/OR can be replaced with the argument. + Debug("parser") << "applyParseOp: return unary " << args[0] << std::endl; return args[0]; } - else if (kind == kind::MINUS && args.size() == 1) + else if (kind == api::MINUS && args.size() == 1) { - return em->mkExpr(kind::UMINUS, args[0]); + api::Term ret = d_solver->mkTerm(api::UMINUS, args[0]); + Debug("parser") << "applyParseOp: return uminus " << ret << std::endl; + return ret; } - api::Term ret = - d_solver->mkTerm(intToExtKind(kind), api::exprVectorToTerms(args)); + api::Term ret = d_solver->mkTerm(kind, args); Debug("parser") << "applyParseOp: return default builtin " << ret << std::endl; - return ret.getExpr(); + return ret; } if (args.size() >= 2) { // may be partially applied function, in this case we use HO_APPLY - Type argt = args[0].getType(); + api::Sort argt = args[0].getSort(); if (argt.isFunction()) { - unsigned arity = static_cast<FunctionType>(argt).getArity(); + unsigned arity = argt.getFunctionArity(); if (args.size() - 1 < arity) { if (!em->getOptions().getUfHo()) @@ -1848,26 +1877,33 @@ Expr Smt2::applyParseOp(ParseOp& p, std::vector<Expr>& args) Debug("parser") << "Partial application of " << args[0]; Debug("parser") << " : #argTypes = " << arity; Debug("parser") << ", #args = " << args.size() - 1 << std::endl; + api::Term ret = d_solver->mkTerm(api::HO_APPLY, args); + Debug("parser") << "applyParseOp: return curry higher order " << ret + << std::endl; // must curry the partial application - return em->mkLeftAssociative(kind::HO_APPLY, args); + return ret; } } } if (!op.isNull()) { - api::Term ret = d_solver->mkTerm(op, api::exprVectorToTerms(args)); + api::Term ret = d_solver->mkTerm(op, args); Debug("parser") << "applyParseOp: return op : " << ret << std::endl; - return ret.getExpr(); + return ret; } - if (kind == kind::NULL_EXPR) + if (kind == api::NULL_EXPR) { - std::vector<Expr> eargs(args.begin() + 1, args.end()); - return em->mkExpr(args[0], eargs); - } - return em->mkExpr(kind, args); + // should never happen in the new API + parseError("do not know how to process parse op"); + } + Debug("parser") << "Try default term construction for kind " << kind + << " #args = " << args.size() << "..." << std::endl; + api::Term ret = d_solver->mkTerm(kind, args); + Debug("parser") << "applyParseOp: return : " << ret << std::endl; + return ret; } -Expr Smt2::setNamedAttribute(Expr& expr, const SExpr& sexpr) +api::Term Smt2::setNamedAttribute(api::Term& expr, const SExpr& sexpr) { if (!sexpr.isKeyword()) { @@ -1876,7 +1912,7 @@ Expr Smt2::setNamedAttribute(Expr& expr, const SExpr& sexpr) std::string name = sexpr.getValue(); checkUserSymbol(name); // ensure expr is a closed subterm - if (expr.hasFreeVariable()) + if (expr.getExpr().hasFreeVariable()) { std::stringstream ss; ss << ":named annotations can only name terms that are closed"; @@ -1885,19 +1921,17 @@ Expr Smt2::setNamedAttribute(Expr& expr, const SExpr& sexpr) // check that sexpr is a fresh function symbol, and reserve it reserveSymbolAtAssertionLevel(name); // define it - Expr func = mkVar(name, expr.getType(), ExprManager::VAR_FLAG_DEFINED); + api::Term func = bindVar(name, expr.getSort(), ExprManager::VAR_FLAG_DEFINED); // remember the last term to have been given a :named attribute setLastNamedTerm(expr, name); return func; } -Expr Smt2::mkAnd(const std::vector<Expr>& es) +api::Term Smt2::mkAnd(const std::vector<api::Term>& es) { - ExprManager* em = getExprManager(); - if (es.size() == 0) { - return em->mkConst(true); + return d_solver->mkTrue(); } else if (es.size() == 1) { @@ -1905,7 +1939,7 @@ Expr Smt2::mkAnd(const std::vector<Expr>& es) } else { - return em->mkExpr(kind::AND, es); + return d_solver->mkTerm(api::AND, es); } } diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h index 53ebf5929..afa60bf2f 100644 --- a/src/parser/smt2/smt2.h +++ b/src/parser/smt2/smt2.h @@ -72,15 +72,15 @@ class Smt2 : public Parser bool d_seenSetLogic; LogicInfo d_logic; - std::unordered_map<std::string, Kind> operatorKindMap; + std::unordered_map<std::string, api::Kind> operatorKindMap; /** * Maps indexed symbols to the kind of the operator (e.g. "extract" to * BITVECTOR_EXTRACT). */ std::unordered_map<std::string, api::Kind> d_indexedOpKindMap; - std::pair<Expr, std::string> d_lastNamedTerm; + std::pair<api::Term, std::string> d_lastNamedTerm; // for sygus - std::vector<Expr> d_sygusVars, d_sygusVarPrimed, d_sygusConstraints, + std::vector<api::Term> d_sygusVars, d_sygusVarPrimed, d_sygusConstraints, d_sygusFunSymbols; protected: @@ -97,7 +97,7 @@ class Smt2 : public Parser */ void addTheory(Theory theory); - void addOperator(Kind k, const std::string& name); + void addOperator(api::Kind k, const std::string& name); /** * Registers an indexed function symbol. @@ -109,11 +109,11 @@ class Smt2 : public Parser * @param opKind The kind of the operator term (e.g. BITVECTOR_EXTRACT) * @param name The name of the symbol (e.g. "extract") */ - void addIndexedOperator(Kind tKind, + void addIndexedOperator(api::Kind tKind, api::Kind opKind, const std::string& name); - Kind getOperatorKind(const std::string& name) const; + api::Kind getOperatorKind(const std::string& name) const; bool isOperatorEnabled(const std::string& name) const; @@ -147,7 +147,8 @@ class Smt2 : public Parser /** * Returns the expression that name should be interpreted as. */ - Expr getExpressionForNameAndType(const std::string& name, Type t) override; + api::Term getExpressionForNameAndType(const std::string& name, + api::Sort t) override; /** Make function defined by a define-fun(s)-rec command. * @@ -163,11 +164,11 @@ class Smt2 : public Parser * added to flattenVars in this function if the function is given a function * range type. */ - Expr mkDefineFunRec( + api::Term bindDefineFunRec( const std::string& fname, - const std::vector<std::pair<std::string, Type> >& sortedVarNames, - Type t, - std::vector<Expr>& flattenVars); + const std::vector<std::pair<std::string, api::Sort>>& sortedVarNames, + api::Sort t, + std::vector<api::Term>& flattenVars); /** Push scope for define-fun-rec * @@ -187,10 +188,10 @@ class Smt2 : public Parser * that defined this definition and stores it in bvs. */ void pushDefineFunRecScope( - const std::vector<std::pair<std::string, Type> >& sortedVarNames, - Expr func, - const std::vector<Expr>& flattenVars, - std::vector<Expr>& bvs, + const std::vector<std::pair<std::string, api::Sort>>& sortedVarNames, + api::Term func, + const std::vector<api::Term>& flattenVars, + std::vector<api::Term>& bvs, bool bindingLevel = false); void reset() override; @@ -218,11 +219,11 @@ class Smt2 : public Parser Smt2* smt2, const std::string& fun, bool isInv, - Type range, - std::vector<std::pair<std::string, CVC4::Type>>& sortedVarNames); + api::Sort range, + std::vector<std::pair<std::string, api::Sort>>& sortedVarNames); ~SynthFunFactory(); - const std::vector<Expr>& getSygusVars() const { return d_sygusVars; } + const std::vector<api::Term>& getSygusVars() const { return d_sygusVars; } /** * Create an instance of `SynthFunCommand`. @@ -230,15 +231,15 @@ class Smt2 : public Parser * @param grammar Optional grammar associated with the synth-fun command * @return The instance of `SynthFunCommand` */ - std::unique_ptr<Command> mkCommand(Type grammar); + std::unique_ptr<Command> mkCommand(api::Sort grammar); private: Smt2* d_smt2; std::string d_fun; - Expr d_synthFun; - Type d_sygusType; + api::Term d_synthFun; + api::Sort d_sygusType; bool d_isInv; - std::vector<Expr> d_sygusVars; + std::vector<api::Term> d_sygusVars; }; /** @@ -321,17 +322,16 @@ class Smt2 : public Parser void includeFile(const std::string& filename); - void setLastNamedTerm(Expr e, std::string name) { + void setLastNamedTerm(api::Term e, std::string name) + { d_lastNamedTerm = std::make_pair(e, name); } void clearLastNamedTerm() { - d_lastNamedTerm = std::make_pair(Expr(), ""); + d_lastNamedTerm = std::make_pair(api::Term(), ""); } - std::pair<Expr, std::string> lastNamedTerm() { - return d_lastNamedTerm; - } + std::pair<api::Term, std::string> lastNamedTerm() { return d_lastNamedTerm; } /** Does name denote an abstract value? (of the form '@n' for numeral n). */ bool isAbstractValue(const std::string& name); @@ -341,58 +341,59 @@ class Smt2 : public Parser * Abstract values are used for processing get-value calls. The argument * name should be such that isAbstractValue(name) is true. */ - Expr mkAbstractValue(const std::string& name); + api::Term mkAbstractValue(const std::string& name); - void mkSygusConstantsForType( const Type& type, std::vector<CVC4::Expr>& ops ); + void mkSygusConstantsForType(const api::Sort& type, + std::vector<api::Term>& ops); void processSygusGTerm( CVC4::SygusGTerm& sgt, int index, std::vector<CVC4::Datatype>& datatypes, - std::vector<CVC4::Type>& sorts, + std::vector<api::Sort>& sorts, std::vector<std::vector<ParseOp>>& ops, std::vector<std::vector<std::string>>& cnames, - std::vector<std::vector<std::vector<CVC4::Type>>>& cargs, + std::vector<std::vector<std::vector<api::Sort>>>& cargs, std::vector<bool>& allow_const, std::vector<std::vector<std::string>>& unresolved_gterm_sym, - const std::vector<CVC4::Expr>& sygus_vars, - std::map<CVC4::Type, CVC4::Type>& sygus_to_builtin, - std::map<CVC4::Type, CVC4::Expr>& sygus_to_builtin_expr, - CVC4::Type& ret, + const std::vector<api::Term>& sygus_vars, + std::map<api::Sort, api::Sort>& sygus_to_builtin, + std::map<api::Sort, api::Term>& sygus_to_builtin_expr, + api::Sort& ret, bool isNested = false); bool pushSygusDatatypeDef( - Type t, + api::Sort t, std::string& dname, std::vector<CVC4::Datatype>& datatypes, - std::vector<CVC4::Type>& sorts, + std::vector<api::Sort>& sorts, std::vector<std::vector<ParseOp>>& ops, std::vector<std::vector<std::string>>& cnames, - std::vector<std::vector<std::vector<CVC4::Type>>>& cargs, + std::vector<std::vector<std::vector<api::Sort>>>& cargs, std::vector<bool>& allow_const, std::vector<std::vector<std::string>>& unresolved_gterm_sym); bool popSygusDatatypeDef( std::vector<CVC4::Datatype>& datatypes, - std::vector<CVC4::Type>& sorts, + std::vector<api::Sort>& sorts, std::vector<std::vector<ParseOp>>& ops, std::vector<std::vector<std::string>>& cnames, - std::vector<std::vector<std::vector<CVC4::Type>>>& cargs, + std::vector<std::vector<std::vector<api::Sort>>>& cargs, std::vector<bool>& allow_const, std::vector<std::vector<std::string>>& unresolved_gterm_sym); void setSygusStartIndex(const std::string& fun, int startIndex, std::vector<CVC4::Datatype>& datatypes, - std::vector<CVC4::Type>& sorts, + std::vector<api::Sort>& sorts, std::vector<std::vector<ParseOp>>& ops); void mkSygusDatatype(CVC4::Datatype& dt, std::vector<ParseOp>& ops, std::vector<std::string>& cnames, - std::vector<std::vector<CVC4::Type>>& cargs, + std::vector<std::vector<api::Sort>>& cargs, std::vector<std::string>& unresolved_gterm_sym, - std::map<CVC4::Type, CVC4::Type>& sygus_to_builtin); + std::map<api::Sort, api::Sort>& sygus_to_builtin); /** * Adds a constructor to sygus datatype dt whose sygus operator is term. @@ -407,17 +408,18 @@ class Smt2 : public Parser * with bound variables via purifySygusGTerm, and binding these variables * via a lambda. */ - void addSygusConstructorTerm(Datatype& dt, - Expr term, - std::map<Expr, Type>& ntsToUnres) const; + void addSygusConstructorTerm( + Datatype& dt, + api::Term term, + std::map<api::Term, api::Sort>& ntsToUnres) const; /** * This adds constructors to dt for sygus variables in sygusVars whose * type is argument type. This method should be called when the sygus grammar * term (Variable type) is encountered. */ void addSygusConstructorVariables(Datatype& dt, - const std::vector<Expr>& sygusVars, - Type type) const; + const std::vector<api::Term>& sygusVars, + api::Sort type) const; /** * Smt2 parser provides its own checkDeclaration, which does the @@ -446,40 +448,6 @@ class Smt2 : public Parser } this->Parser::checkDeclaration(name, check, type, notes); } - - void checkOperator(Kind kind, unsigned numArgs) - { - Parser::checkOperator(kind, numArgs); - // strict SMT-LIB mode enables extra checks for some bitvector operators - // that CVC4 permits as N-ary but the standard requires is binary - if(strictModeEnabled()) { - switch(kind) { - case kind::BITVECTOR_AND: - case kind::BITVECTOR_MULT: - case kind::BITVECTOR_OR: - case kind::BITVECTOR_PLUS: - case kind::BITVECTOR_XOR: - if (numArgs != 2 && !v2_6()) - { - parseError( - "Operator requires exactly 2 arguments in strict SMT-LIB " - "compliance mode (for versions <2.6): " - + kindToString(kind)); - } - break; - case kind::BITVECTOR_CONCAT: - if(numArgs != 2) { - parseError( - "Operator requires exactly 2 arguments in strict SMT-LIB " - "compliance mode: " - + kindToString(kind)); - } - break; - default: - break; /* no problem */ - } - } - } /** Set named attribute * * This is called when expression expr is annotated with a name, i.e. @@ -490,7 +458,7 @@ class Smt2 : public Parser * which is used later for tracking assertions in unsat cores. This * symbol is returned by this method. */ - Expr setNamedAttribute(Expr& expr, const SExpr& sexpr); + api::Term setNamedAttribute(api::Term& expr, const SExpr& sexpr); // Throw a ParserException with msg appended with the current logic. inline void parseErrorLogic(const std::string& msg) @@ -516,7 +484,7 @@ class Smt2 : public Parser * - If p's expression field is set, then we leave p unchanged, check if * that expression has the given type and throw a parse error otherwise. */ - void parseOpApplyTypeAscription(ParseOp& p, Type type); + void parseOpApplyTypeAscription(ParseOp& p, api::Sort type); /** * This converts a ParseOp to expression, assuming it is a standalone term. * @@ -526,7 +494,7 @@ class Smt2 : public Parser * of this class. * In other cases, a parse error is thrown. */ - Expr parseOpToExpr(ParseOp& p); + api::Term parseOpToExpr(ParseOp& p); /** * Apply parse operator to list of arguments, and return the resulting * expression. @@ -559,24 +527,24 @@ class Smt2 : public Parser * - If the overall expression is a partial application, then we process this * as a chain of HO_APPLY terms. */ - Expr applyParseOp(ParseOp& p, std::vector<Expr>& args); + api::Term applyParseOp(ParseOp& p, std::vector<api::Term>& args); //------------------------- end processing parse operators private: - std::map< CVC4::Expr, CVC4::Type > d_sygus_bound_var_type; + std::map<api::Term, api::Sort> d_sygus_bound_var_type; - Type processSygusNestedGTerm( + api::Sort processSygusNestedGTerm( int sub_dt_index, std::string& sub_dname, std::vector<CVC4::Datatype>& datatypes, - std::vector<CVC4::Type>& sorts, + std::vector<api::Sort>& sorts, std::vector<std::vector<ParseOp>>& ops, std::vector<std::vector<std::string>>& cnames, - std::vector<std::vector<std::vector<CVC4::Type>>>& cargs, + std::vector<std::vector<std::vector<api::Sort>>>& cargs, std::vector<bool>& allow_const, std::vector<std::vector<std::string>>& unresolved_gterm_sym, - std::map<CVC4::Type, CVC4::Type>& sygus_to_builtin, - std::map<CVC4::Type, CVC4::Expr>& sygus_to_builtin_expr, - Type sub_ret); + std::map<api::Sort, api::Sort>& sygus_to_builtin, + std::map<api::Sort, api::Term>& sygus_to_builtin_expr, + api::Sort sub_ret); /** make sygus bound var list * @@ -586,10 +554,10 @@ class Smt2 : public Parser * It appends a bound variable to lvars for each type in ltypes, and returns * a bound variable list whose children are lvars. */ - Expr makeSygusBoundVarList(Datatype& dt, - unsigned i, - const std::vector<Type>& ltypes, - std::vector<Expr>& lvars); + api::Term makeSygusBoundVarList(CVC4::Datatype& dt, + unsigned i, + const std::vector<api::Sort>& ltypes, + std::vector<api::Term>& lvars); /** Purify sygus grammar term * @@ -603,7 +571,7 @@ class Smt2 : public Parser * sygus constructor. */ api::Term purifySygusGTerm(api::Term term, - std::map<Expr, Type>& ntsToUnres, + std::map<api::Term, api::Sort>& ntsToUnres, std::vector<api::Term>& args, std::vector<api::Sort>& cargs) const; @@ -632,7 +600,7 @@ class Smt2 : public Parser * @return True if `es` is empty, `e` if `es` consists of a single element * `e`, the conjunction of expressions otherwise. */ - Expr mkAnd(const std::vector<Expr>& es); + api::Term mkAnd(const std::vector<api::Term>& es); }; /* class Smt2 */ }/* CVC4::parser namespace */ diff --git a/src/parser/smt2/smt2_input.cpp b/src/parser/smt2/smt2_input.cpp index 4e74eefb5..c0bece257 100644 --- a/src/parser/smt2/smt2_input.cpp +++ b/src/parser/smt2/smt2_input.cpp @@ -64,7 +64,7 @@ Command* Smt2Input::parseCommand() { api::Term Smt2Input::parseExpr() { - return api::Term(d_pSmt2Parser->parseExpr(d_pSmt2Parser)); + return d_pSmt2Parser->parseExpr(d_pSmt2Parser); } }/* CVC4::parser namespace */ diff --git a/src/parser/smt2/sygus_input.cpp b/src/parser/smt2/sygus_input.cpp index f0bed978e..a908bf4d5 100644 --- a/src/parser/smt2/sygus_input.cpp +++ b/src/parser/smt2/sygus_input.cpp @@ -65,7 +65,7 @@ Command* SygusInput::parseCommand() { api::Term SygusInput::parseExpr() { - return api::Term(d_pSmt2Parser->parseExpr(d_pSmt2Parser)); + return d_pSmt2Parser->parseExpr(d_pSmt2Parser); } }/* CVC4::parser namespace */ |