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/cvc | |
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/cvc')
-rw-r--r-- | src/parser/cvc/Cvc.g | 43 |
1 files changed, 30 insertions, 13 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); } |