diff options
author | Aina Niemetz <aina.niemetz@gmail.com> | 2020-06-03 20:56:24 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-06-03 20:56:24 -0700 |
commit | 5938faaf034a761f3462d8e03b86b1726a332f68 (patch) | |
tree | 864fcd067ac024689b2fb3ee782ce7edd99e0a3a /src/parser/cvc | |
parent | 418b0281e62a6b657da32f6504965269ad90c18b (diff) |
New C++ Api: First batch of API guards. (#4557)
This is the first batch of API guards, mainly extending existing guards
in the Solver object with checks that Ops, Terms, Sorts, and datatype objects
are associated to this solver object.
This further changes how DatatypeConstructorDecl objects are created. Previously,
they were not created via the Solver object (while DatatypeDecl was). Now, they are
created via Solver::mkDatatypeConstructorDecl, consistent with how DatatypeDecl
objects are created.
Diffstat (limited to 'src/parser/cvc')
-rw-r--r-- | src/parser/cvc/Cvc.g | 43 |
1 files changed, 17 insertions, 26 deletions
diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g index fdb6a081c..e604c7769 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, - api::Sort(PARSER_STATE->getSolver(), t.getType()), + api::Sort(SOLVER, t.getType()), ExprManager::VAR_FLAG_GLOBAL | ExprManager::VAR_FLAG_DEFINED); PARSER_STATE->defineVar(*i, f); Command* decl = @@ -1654,9 +1654,7 @@ tupleStore[CVC4::api::Term& f] } const Datatype & dt = ((DatatypeType)t.getType()).getDatatype(); f2 = SOLVER->mkTerm( - api::APPLY_SELECTOR, - api::Term(PARSER_STATE->getSolver(), dt[0][k].getSelector()), - f); + api::APPLY_SELECTOR, api::Term(SOLVER, dt[0][k].getSelector()), f); } ( ( arrayStore[f2] | DOT ( tupleStore[f2] @@ -1689,9 +1687,7 @@ recordStore[CVC4::api::Term& f] } const Datatype & dt = ((DatatypeType)t.getType()).getDatatype(); f2 = SOLVER->mkTerm( - api::APPLY_SELECTOR, - api::Term(PARSER_STATE->getSolver(), dt[0][id].getSelector()), - f); + api::APPLY_SELECTOR, api::Term(SOLVER, dt[0][id].getSelector()), f); } ( ( arrayStore[f2] | DOT ( tupleStore[f2] @@ -1835,10 +1831,9 @@ 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(PARSER_STATE->getSolver(), dt[0][id].getSelector()), - f); + f = SOLVER->mkTerm(api::APPLY_SELECTOR, + api::Term(SOLVER, dt[0][id].getSelector()), + f); } | k=numeral { @@ -1853,10 +1848,9 @@ 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(PARSER_STATE->getSolver(), dt[0][k].getSelector()), - f); + f = SOLVER->mkTerm(api::APPLY_SELECTOR, + api::Term(SOLVER, dt[0][k].getSelector()), + f); } ) )* @@ -1896,8 +1890,7 @@ relationTerm[CVC4::api::Term& f] types.push_back(f.getSort()); api::Sort t = SOLVER->mkTupleSort(types); const Datatype& dt = Datatype(((DatatypeType)t.getType()).getDatatype()); - args.insert(args.begin(), - api::Term(PARSER_STATE->getSolver(), dt[0].getConstructor())); + args.insert(args.begin(), api::Term(SOLVER, dt[0].getConstructor())); f = MK_TERM(api::APPLY_CONSTRUCTOR, args); } | IDEN_TOK LPAREN formula[f] RPAREN @@ -2147,9 +2140,7 @@ simpleTerm[CVC4::api::Term& f] } api::Sort dtype = SOLVER->mkTupleSort(types); const Datatype& dt = ((DatatypeType)dtype.getType()).getDatatype(); - args.insert( - args.begin(), - api::Term(PARSER_STATE->getSolver(), dt[0].getConstructor())); + args.insert(args.begin(), api::Term(SOLVER, dt[0].getConstructor())); f = MK_TERM(api::APPLY_CONSTRUCTOR, args); } } @@ -2160,7 +2151,7 @@ simpleTerm[CVC4::api::Term& f] api::Sort dtype = SOLVER->mkTupleSort(types); const Datatype& dt = ((DatatypeType)dtype.getType()).getDatatype(); f = MK_TERM(api::APPLY_CONSTRUCTOR, - api::Term(PARSER_STATE->getSolver(), dt[0].getConstructor())); + api::Term(SOLVER, dt[0].getConstructor())); } /* empty record literal */ @@ -2170,7 +2161,7 @@ simpleTerm[CVC4::api::Term& f] std::vector<std::pair<std::string, api::Sort>>()); const Datatype& dt = ((DatatypeType)dtype.getType()).getDatatype(); f = MK_TERM(api::APPLY_CONSTRUCTOR, - api::Term(PARSER_STATE->getSolver(), dt[0].getConstructor())); + api::Term(SOLVER, dt[0].getConstructor())); } /* empty set literal */ | LBRACE RBRACE @@ -2268,8 +2259,7 @@ simpleTerm[CVC4::api::Term& f] } api::Sort dtype = SOLVER->mkRecordSort(typeIds); const Datatype& dt = ((DatatypeType)dtype.getType()).getDatatype(); - args.insert(args.begin(), - api::Term(PARSER_STATE->getSolver(), dt[0].getConstructor())); + args.insert(args.begin(), api::Term(SOLVER, dt[0].getConstructor())); f = MK_TERM(api::APPLY_CONSTRUCTOR, args); } @@ -2377,8 +2367,9 @@ constructorDef[CVC4::api::DatatypeDecl& type] std::unique_ptr<CVC4::api::DatatypeConstructorDecl> ctor; } : identifier[id,CHECK_UNDECLARED,SYM_SORT] - { - ctor.reset(new CVC4::api::DatatypeConstructorDecl(id)); + { + ctor.reset(new CVC4::api::DatatypeConstructorDecl( + SOLVER->mkDatatypeConstructorDecl(id))); } ( LPAREN selector[&ctor] |