diff options
author | Aina Niemetz <aina.niemetz@gmail.com> | 2020-06-02 09:09:15 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-06-02 09:09:15 -0700 |
commit | 50edf184492d20f4acb7b8d82f3843f3146f77d5 (patch) | |
tree | 2a1bbdbd59dc7aefca114b108c646eb6f2dd933e /src/parser | |
parent | b826fc8ae95fc13c4e2be45e39961199392a4dda (diff) |
New C++ API: Keep reference to solver object in non-solver objects. (#4549)
This is in preparation for adding guards to ensure that sort and term
arguments belong to the same solver.
Diffstat (limited to 'src/parser')
-rw-r--r-- | src/parser/cvc/Cvc.g | 43 | ||||
-rw-r--r-- | src/parser/parser.cpp | 55 | ||||
-rw-r--r-- | src/parser/parser.h | 12 | ||||
-rw-r--r-- | src/parser/smt2/Smt2.g | 18 | ||||
-rw-r--r-- | src/parser/smt2/smt2.cpp | 13 | ||||
-rw-r--r-- | src/parser/tptp/Tptp.g | 4 |
6 files changed, 84 insertions, 61 deletions
diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g index 8e4152e2e..fdb6a081c 100644 --- a/src/parser/cvc/Cvc.g +++ b/src/parser/cvc/Cvc.g @@ -1159,7 +1159,7 @@ declareVariables[std::unique_ptr<CVC4::Command>* cmd, CVC4::api::Sort& t, PARSER_STATE->checkDeclaration(*i, CHECK_UNDECLARED, SYM_VARIABLE); api::Term func = PARSER_STATE->mkVar( *i, - t.getType(), + api::Sort(PARSER_STATE->getSolver(), t.getType()), ExprManager::VAR_FLAG_GLOBAL | ExprManager::VAR_FLAG_DEFINED); PARSER_STATE->defineVar(*i, f); Command* decl = @@ -1654,7 +1654,9 @@ tupleStore[CVC4::api::Term& f] } const Datatype & dt = ((DatatypeType)t.getType()).getDatatype(); f2 = SOLVER->mkTerm( - api::APPLY_SELECTOR, api::Term(dt[0][k].getSelector()), f); + api::APPLY_SELECTOR, + api::Term(PARSER_STATE->getSolver(), dt[0][k].getSelector()), + f); } ( ( arrayStore[f2] | DOT ( tupleStore[f2] @@ -1687,7 +1689,9 @@ recordStore[CVC4::api::Term& f] } const Datatype & dt = ((DatatypeType)t.getType()).getDatatype(); f2 = SOLVER->mkTerm( - api::APPLY_SELECTOR, api::Term(dt[0][id].getSelector()), f); + api::APPLY_SELECTOR, + api::Term(PARSER_STATE->getSolver(), dt[0][id].getSelector()), + f); } ( ( arrayStore[f2] | DOT ( tupleStore[f2] @@ -1831,7 +1835,10 @@ postfixTerm[CVC4::api::Term& f] PARSER_STATE->parseError(std::string("no such field `") + id + "' in record"); } const Datatype & dt = ((DatatypeType)type.getType()).getDatatype(); - f = SOLVER->mkTerm(api::APPLY_SELECTOR,api::Term(dt[0][id].getSelector()), f); + f = SOLVER->mkTerm( + api::APPLY_SELECTOR, + api::Term(PARSER_STATE->getSolver(), dt[0][id].getSelector()), + f); } | k=numeral { @@ -1846,7 +1853,10 @@ postfixTerm[CVC4::api::Term& f] PARSER_STATE->parseError(ss.str()); } const Datatype & dt = ((DatatypeType)type.getType()).getDatatype(); - f = SOLVER->mkTerm(api::APPLY_SELECTOR,api::Term(dt[0][k].getSelector()), f); + f = SOLVER->mkTerm( + api::APPLY_SELECTOR, + api::Term(PARSER_STATE->getSolver(), dt[0][k].getSelector()), + f); } ) )* @@ -1857,7 +1867,7 @@ postfixTerm[CVC4::api::Term& f] | ABS_TOK LPAREN formula[f] RPAREN { f = MK_TERM(CVC4::api::ABS, f); } | DIVISIBLE_TOK LPAREN formula[f] COMMA n=numeral RPAREN - { f = MK_TERM(SOLVER->mkOp(CVC4::api::DIVISIBLE,n), f); } + { f = MK_TERM(SOLVER->mkOp(CVC4::api::DIVISIBLE, n), f); } | DISTINCT_TOK LPAREN formula[f] { args.push_back(f); } ( COMMA formula[f] { args.push_back(f); } )* RPAREN @@ -1868,7 +1878,7 @@ postfixTerm[CVC4::api::Term& f] ) ( typeAscription[f, t] { - f = PARSER_STATE->applyTypeAscription(f,t).getExpr(); + f = PARSER_STATE->applyTypeAscription(f,t); } )? ; @@ -1885,8 +1895,9 @@ relationTerm[CVC4::api::Term& f] args.push_back(f); types.push_back(f.getSort()); api::Sort t = SOLVER->mkTupleSort(types); - const Datatype& dt = ((DatatypeType)t.getType()).getDatatype(); - args.insert( args.begin(), api::Term(dt[0].getConstructor()) ); + const Datatype& dt = Datatype(((DatatypeType)t.getType()).getDatatype()); + args.insert(args.begin(), + api::Term(PARSER_STATE->getSolver(), dt[0].getConstructor())); f = MK_TERM(api::APPLY_CONSTRUCTOR, args); } | IDEN_TOK LPAREN formula[f] RPAREN @@ -2136,7 +2147,9 @@ simpleTerm[CVC4::api::Term& f] } api::Sort dtype = SOLVER->mkTupleSort(types); const Datatype& dt = ((DatatypeType)dtype.getType()).getDatatype(); - args.insert( args.begin(), dt[0].getConstructor() ); + args.insert( + args.begin(), + api::Term(PARSER_STATE->getSolver(), dt[0].getConstructor())); f = MK_TERM(api::APPLY_CONSTRUCTOR, args); } } @@ -2146,7 +2159,9 @@ simpleTerm[CVC4::api::Term& f] { std::vector<api::Sort> types; api::Sort dtype = SOLVER->mkTupleSort(types); const Datatype& dt = ((DatatypeType)dtype.getType()).getDatatype(); - f = MK_TERM(api::APPLY_CONSTRUCTOR, api::Term(dt[0].getConstructor())); } + f = MK_TERM(api::APPLY_CONSTRUCTOR, + api::Term(PARSER_STATE->getSolver(), dt[0].getConstructor())); + } /* empty record literal */ | PARENHASH HASHPAREN @@ -2154,7 +2169,8 @@ simpleTerm[CVC4::api::Term& f] api::Sort dtype = SOLVER->mkRecordSort( std::vector<std::pair<std::string, api::Sort>>()); const Datatype& dt = ((DatatypeType)dtype.getType()).getDatatype(); - f = MK_TERM(api::APPLY_CONSTRUCTOR, api::Term(dt[0].getConstructor())); + f = MK_TERM(api::APPLY_CONSTRUCTOR, + api::Term(PARSER_STATE->getSolver(), dt[0].getConstructor())); } /* empty set literal */ | LBRACE RBRACE @@ -2252,7 +2268,8 @@ simpleTerm[CVC4::api::Term& f] } api::Sort dtype = SOLVER->mkRecordSort(typeIds); const Datatype& dt = ((DatatypeType)dtype.getType()).getDatatype(); - args.insert( args.begin(), dt[0].getConstructor() ); + args.insert(args.begin(), + api::Term(PARSER_STATE->getSolver(), dt[0].getConstructor())); f = MK_TERM(api::APPLY_CONSTRUCTOR, args); } diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp index c860d14c7..b24f9ae9d 100644 --- a/src/parser/parser.cpp +++ b/src/parser/parser.cpp @@ -82,14 +82,9 @@ api::Term Parser::getSymbol(const std::string& name, SymbolType type) { checkDeclaration(name, CHECK_DECLARED, type); assert(isDeclared(name, type)); - - if (type == SYM_VARIABLE) { - // Functions share var namespace - return d_symtab->lookup(name); - } - - assert(false); // Unhandled(type); - return Expr(); + assert(type == SYM_VARIABLE); + // Functions share var namespace + return api::Term(d_solver, d_symtab->lookup(name)); } api::Term Parser::getVariable(const std::string& name) @@ -166,7 +161,7 @@ api::Sort Parser::getSort(const std::string& name) { checkDeclaration(name, CHECK_DECLARED, SYM_SORT); assert(isDeclared(name, SYM_SORT)); - api::Sort t = api::Sort(d_symtab->lookupType(name)); + api::Sort t = api::Sort(d_solver, d_symtab->lookupType(name)); return t; } @@ -175,8 +170,8 @@ api::Sort Parser::getSort(const std::string& name, { checkDeclaration(name, CHECK_DECLARED, SYM_SORT); assert(isDeclared(name, SYM_SORT)); - api::Sort t = - api::Sort(d_symtab->lookupType(name, api::sortVectorToTypes(params))); + api::Sort t = api::Sort( + d_solver, d_symtab->lookupType(name, api::sortVectorToTypes(params))); return t; } @@ -237,7 +232,8 @@ std::vector<api::Term> Parser::bindBoundVars( std::vector<api::Term> vars; for (std::pair<std::string, api::Sort>& i : sortedVarNames) { - vars.push_back(bindBoundVar(i.first, i.second.getType())); + vars.push_back( + bindBoundVar(i.first, api::Sort(d_solver, i.second.getType()))); } return vars; } @@ -251,7 +247,7 @@ api::Term Parser::mkAnonymousFunction(const std::string& prefix, } stringstream name; name << prefix << "_anon_" << ++d_anonymousFunctionCount; - return mkVar(name.str(), type.getType(), flags); + return mkVar(name.str(), api::Sort(d_solver, type.getType()), flags); } std::vector<api::Term> Parser::bindVars(const std::vector<std::string> names, @@ -334,7 +330,8 @@ void Parser::defineParameterizedType(const std::string& name, api::Sort Parser::mkSort(const std::string& name, uint32_t flags) { Debug("parser") << "newSort(" << name << ")" << std::endl; - api::Sort type = d_solver->getExprManager()->mkSort(name, flags); + api::Sort type = + api::Sort(d_solver, d_solver->getExprManager()->mkSort(name, flags)); defineType( name, type, @@ -348,8 +345,9 @@ api::Sort Parser::mkSortConstructor(const std::string& name, { Debug("parser") << "newSortConstructor(" << name << ", " << arity << ")" << std::endl; - api::Sort type = - d_solver->getExprManager()->mkSortConstructor(name, arity, flags); + api::Sort type = api::Sort( + d_solver, + d_solver->getExprManager()->mkSortConstructor(name, arity, flags)); defineType( name, vector<api::Sort>(arity), @@ -379,8 +377,10 @@ api::Sort Parser::mkUnresolvedTypeConstructor( { Debug("parser") << "newSortConstructor(P)(" << name << ", " << params.size() << ")" << std::endl; - api::Sort unresolved = d_solver->getExprManager()->mkSortConstructor( - name, params.size(), ExprManager::SORT_FLAG_PLACEHOLDER); + api::Sort unresolved = + api::Sort(d_solver, + d_solver->getExprManager()->mkSortConstructor( + name, params.size(), ExprManager::SORT_FLAG_PLACEHOLDER)); defineType(name, params, unresolved); api::Sort t = getSort(name, params); d_unresolved.insert(unresolved); @@ -588,11 +588,12 @@ api::Term Parser::applyTypeAscription(api::Term t, api::Sort s) Expr e = t.getExpr(); const DatatypeConstructor& dtc = Datatype::datatypeOf(e)[Datatype::indexOf(e)]; - t = api::Term(em->mkExpr( - kind::APPLY_TYPE_ASCRIPTION, - em->mkConst( - AscriptionType(dtc.getSpecializedConstructorType(s.getType()))), - e)); + t = api::Term( + d_solver, + em->mkExpr(kind::APPLY_TYPE_ASCRIPTION, + em->mkConst(AscriptionType( + dtc.getSpecializedConstructorType(s.getType()))), + e)); } // the type of t does not match the sort s by design (constructor type // vs datatype type), thus we use an alternative check here. @@ -624,7 +625,7 @@ api::Term Parser::mkVar(const std::string& name, uint32_t flags) { return api::Term( - d_solver->getExprManager()->mkVar(name, type.getType(), flags)); + d_solver, d_solver->getExprManager()->mkVar(name, type.getType(), flags)); } //!!!!!!!!!!! temporary @@ -892,16 +893,16 @@ std::vector<unsigned> Parser::processAdHocStringEsc(const std::string& s) return str; } -Expr Parser::mkStringConstant(const std::string& s) +api::Term Parser::mkStringConstant(const std::string& s) { ExprManager* em = d_solver->getExprManager(); if (language::isInputLang_smt2_6(em->getOptions().getInputLanguage())) { - return d_solver->mkString(s, true).getExpr(); + return api::Term(d_solver, d_solver->mkString(s, true).getExpr()); } // otherwise, we must process ad-hoc escape sequences std::vector<unsigned> str = processAdHocStringEsc(s); - return d_solver->mkString(str).getExpr(); + return api::Term(d_solver, d_solver->mkString(str).getExpr()); } } /* CVC4::parser namespace */ diff --git a/src/parser/parser.h b/src/parser/parser.h index 7941cfdd5..b5dc83902 100644 --- a/src/parser/parser.h +++ b/src/parser/parser.h @@ -808,7 +808,7 @@ public: inline SymbolTable* getSymbolTable() const { return d_symtab; } - + //------------------------ operator overloading /** is this function overloaded? */ bool isOverloadedFunction(api::Term fun) @@ -822,7 +822,8 @@ public: */ api::Term getOverloadedConstantForType(const std::string& name, api::Sort t) { - return d_symtab->getOverloadedConstantForType(name, t.getType()); + return api::Term(d_solver, + d_symtab->getOverloadedConstantForType(name, t.getType())); } /** @@ -833,8 +834,9 @@ public: api::Term getOverloadedFunctionForTypes(const std::string& name, std::vector<api::Sort>& argTypes) { - return d_symtab->getOverloadedFunctionForTypes( - name, api::sortVectorToTypes(argTypes)); + return api::Term(d_solver, + d_symtab->getOverloadedFunctionForTypes( + name, api::sortVectorToTypes(argTypes))); } //------------------------ end operator overloading /** @@ -845,7 +847,7 @@ public: * SMT-LIB 2.6 or higher), or otherwise calling the solver to construct * the string. */ - Expr mkStringConstant(const std::string& s); + api::Term mkStringConstant(const std::string& s); private: /** ad-hoc string escaping diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 95f4b1a67..081990a45 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -101,7 +101,7 @@ namespace CVC4 { 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 Expr& e) : CVC4::api::Term(d_solver, e) {} myExpr(const myExpr& e) : CVC4::api::Term(e) {} };/* struct myExpr */ }/* CVC4::parser::smt2 namespace */ @@ -286,7 +286,7 @@ 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.getType()); + PARSER_STATE->defineParameterizedType(name, sorts, t); cmd->reset(new DefineTypeCommand( name, api::sortVectorToTypes(sorts), t.getType())); } @@ -800,7 +800,7 @@ sygusGrammarV1[CVC4::api::Sort & ret, PARSER_STATE->getUnresolvedSorts().clear(); - ret = datatypeTypes[0]; + ret = api::Sort(PARSER_STATE->getSolver(), datatypeTypes[0]); }; // SyGuS grammar term. @@ -893,7 +893,7 @@ sygusGTerm[CVC4::SygusGTerm& sgt, const std::string& fun] << "expression " << atomTerm << std::endl; std::stringstream ss; ss << atomTerm; - sgt.d_op.d_expr = atomTerm.getExpr(); + sgt.d_op.d_expr = atomTerm; sgt.d_name = ss.str(); sgt.d_gterm_type = SygusGTerm::gterm_op; } @@ -1791,8 +1791,10 @@ termNonVariable[CVC4::api::Term& expr, CVC4::api::Term& expr2] Expr ef = f.getExpr(); if (Datatype::datatypeOf(ef).isParametric()) { - type = Datatype::datatypeOf(ef)[Datatype::indexOf(ef)] - .getSpecializedConstructorType(expr.getSort().getType()); + type = api::Sort( + PARSER_STATE->getSolver(), + Datatype::datatypeOf(ef)[Datatype::indexOf(ef)] + .getSpecializedConstructorType(expr.getSort().getType())); } argTypes = type.getConstructorDomainSorts(); } @@ -1914,10 +1916,10 @@ termNonVariable[CVC4::api::Term& expr, CVC4::api::Term& expr2] sorts.emplace_back(arg.getSort()); terms.emplace_back(arg); } - expr = SOLVER->mkTuple(sorts, terms).getExpr(); + expr = SOLVER->mkTuple(sorts, terms); } | /* an atomic term (a term with no subterms) */ - termAtomic[atomTerm] { expr = atomTerm.getExpr(); } + termAtomic[atomTerm] { expr = atomTerm; } ; diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index 9ca2194f4..608e47a6b 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -1377,7 +1377,7 @@ void Smt2::mkSygusDatatype(api::DatatypeDecl& dt, if( std::find( types.begin(), types.end(), t )==types.end() ){ types.push_back( t ); //identity element - api::Sort bt = dt.getDatatype().getSygusType(); + api::Sort bt = api::Sort(d_solver, dt.getDatatype().getSygusType()); Debug("parser-sygus") << ": make identity function for " << bt << ", argument type " << t << std::endl; std::stringstream ss; @@ -1481,7 +1481,7 @@ api::Term Smt2::purifySygusGTerm(api::Term term, api::Term ret = d_solver->mkVar(term.getSort()); Trace("parser-sygus2-debug") << "...unresolved non-terminal, intro " << ret << std::endl; - args.push_back(ret.getExpr()); + args.push_back(api::Term(d_solver, ret.getExpr())); cargs.push_back(itn->second); return ret; } @@ -1571,8 +1571,7 @@ void Smt2::parseOpApplyTypeAscription(ParseOp& p, api::Sort type) 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(); + p.d_expr = applyTypeAscription(p.d_expr, type); } api::Term Smt2::parseOpToExpr(ParseOp& p) @@ -1776,8 +1775,10 @@ api::Term Smt2::applyParseOp(ParseOp& p, std::vector<api::Term>& args) parseError(ss.str()); } const Datatype& dt = ((DatatypeType)t.getType()).getDatatype(); - api::Term ret = d_solver->mkTerm( - api::APPLY_SELECTOR, api::Term(dt[0][n].getSelector()), args[0]); + api::Term ret = + d_solver->mkTerm(api::APPLY_SELECTOR, + api::Term(d_solver, dt[0][n].getSelector()), + args[0]); Debug("parser") << "applyParseOp: return selector " << ret << std::endl; return ret; } diff --git a/src/parser/tptp/Tptp.g b/src/parser/tptp/Tptp.g index c2f4675b1..c1d60ca31 100644 --- a/src/parser/tptp/Tptp.g +++ b/src/parser/tptp/Tptp.g @@ -1441,7 +1441,7 @@ tffLetTermBinding[std::vector<CVC4::api::Term> & bvlist, PARSER_STATE->checkLetBinding(bvlist, lhs, rhs, false); std::vector<api::Term> lchildren(++lhs.begin(), lhs.end()); rhs = MK_TERM(api::LAMBDA, MK_TERM(api::BOUND_VAR_LIST, lchildren), rhs); - lhs = api::Term(lhs.getExpr().getOperator()); + lhs = api::Term(PARSER_STATE->getSolver(), lhs.getExpr().getOperator()); } | LPAREN_TOK tffLetTermBinding[bvlist, lhs, rhs] RPAREN_TOK ; @@ -1463,7 +1463,7 @@ tffLetFormulaBinding[std::vector<CVC4::api::Term> & bvlist, PARSER_STATE->checkLetBinding(bvlist, lhs, rhs, true); std::vector<api::Term> lchildren(++lhs.begin(), lhs.end()); rhs = MK_TERM(api::LAMBDA, MK_TERM(api::BOUND_VAR_LIST, lchildren), rhs); - lhs = api::Term(lhs.getExpr().getOperator()); + lhs = api::Term(PARSER_STATE->getSolver(), lhs.getExpr().getOperator()); } | LPAREN_TOK tffLetFormulaBinding[bvlist, lhs, rhs] RPAREN_TOK ; |