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/smt2 | |
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/smt2')
-rw-r--r-- | src/parser/smt2/Smt2.g | 18 | ||||
-rw-r--r-- | src/parser/smt2/smt2.cpp | 13 |
2 files changed, 17 insertions, 14 deletions
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; } |