diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-08-03 16:35:19 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-08-03 16:35:19 -0500 |
commit | f332d9eb50796d0dde8302d463ed830fc6770133 (patch) | |
tree | d07f21eef23d9e10ac9863eded4c899ec403a8be /src/parser/cvc/Cvc.g | |
parent | a9b0e87897b95871916368d0dae780f53efcadd8 (diff) |
Update datatypes in cvc parser to the new API (#4826)
This is leftover from the parser conversion. This is towards eliminating all remaining Expr-level calls in the parser.
Notice that 2 parser-level checks for records are eliminated in this PR, since we do not export record objects in the new API.
Diffstat (limited to 'src/parser/cvc/Cvc.g')
-rw-r--r-- | src/parser/cvc/Cvc.g | 46 |
1 files changed, 18 insertions, 28 deletions
diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g index fe5f5e636..091b5a22b 100644 --- a/src/parser/cvc/Cvc.g +++ b/src/parser/cvc/Cvc.g @@ -1646,9 +1646,9 @@ tupleStore[CVC4::api::Term& f] ss << "tuple is of length " << length << "; cannot update index " << k; PARSER_STATE->parseError(ss.str()); } - const Datatype & dt = ((DatatypeType)t.getType()).getDatatype(); + const api::Datatype& dt = t.getDatatype(); f2 = SOLVER->mkTerm( - api::APPLY_SELECTOR, api::Term(SOLVER, dt[0][k].getSelector()), f); + api::APPLY_SELECTOR, dt[0][k].getSelectorTerm(), f); } ( ( arrayStore[f2] | DOT ( tupleStore[f2] @@ -1675,13 +1675,9 @@ recordStore[CVC4::api::Term& f] << "its type: " << t; PARSER_STATE->parseError(ss.str()); } - const Record& rec = ((DatatypeType)t.getType()).getRecord(); - if(! rec.contains(id)) { - PARSER_STATE->parseError(std::string("no such field `") + id + "' in record"); - } - const Datatype & dt = ((DatatypeType)t.getType()).getDatatype(); + const api::Datatype& dt = t.getDatatype(); f2 = SOLVER->mkTerm( - api::APPLY_SELECTOR, api::Term(SOLVER, dt[0][id].getSelector()), f); + api::APPLY_SELECTOR, dt[0][id].getSelectorTerm(), f); } ( ( arrayStore[f2] | DOT ( tupleStore[f2] @@ -1820,13 +1816,9 @@ postfixTerm[CVC4::api::Term& f] if(! type.isRecord()) { PARSER_STATE->parseError("record-select applied to non-record"); } - const Record& rec = ((DatatypeType)type.getType()).getRecord(); - if(!rec.contains(id)){ - PARSER_STATE->parseError(std::string("no such field `") + id + "' in record"); - } - const Datatype & dt = ((DatatypeType)type.getType()).getDatatype(); + const api::Datatype& dt = type.getDatatype(); f = SOLVER->mkTerm(api::APPLY_SELECTOR, - api::Term(SOLVER, dt[0][id].getSelector()), + dt[0][id].getSelectorTerm(), f); } | k=numeral @@ -1841,9 +1833,9 @@ postfixTerm[CVC4::api::Term& f] ss << "tuple is of length " << length << "; cannot access index " << k; PARSER_STATE->parseError(ss.str()); } - const Datatype & dt = ((DatatypeType)type.getType()).getDatatype(); + const api::Datatype& dt = type.getDatatype(); f = SOLVER->mkTerm(api::APPLY_SELECTOR, - api::Term(SOLVER, dt[0][k].getSelector()), + dt[0][k].getSelectorTerm(), f); } ) @@ -1883,8 +1875,8 @@ relationTerm[CVC4::api::Term& f] args.push_back(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(SOLVER, dt[0].getConstructor())); + const api::Datatype& dt = t.getDatatype(); + args.insert(args.begin(), dt[0].getConstructorTerm()); f = MK_TERM(api::APPLY_CONSTRUCTOR, args); } | IDEN_TOK LPAREN formula[f] RPAREN @@ -2135,8 +2127,8 @@ simpleTerm[CVC4::api::Term& f] types.push_back((*i).getSort()); } api::Sort dtype = SOLVER->mkTupleSort(types); - const Datatype& dt = ((DatatypeType)dtype.getType()).getDatatype(); - args.insert(args.begin(), api::Term(SOLVER, dt[0].getConstructor())); + const api::Datatype& dt = dtype.getDatatype(); + args.insert(args.begin(), dt[0].getConstructorTerm()); f = MK_TERM(api::APPLY_CONSTRUCTOR, args); } } @@ -2145,9 +2137,8 @@ simpleTerm[CVC4::api::Term& f] | LPAREN RPAREN { 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(SOLVER, dt[0].getConstructor())); + const api::Datatype& dt = dtype.getDatatype(); + f = MK_TERM(api::APPLY_CONSTRUCTOR, dt[0].getConstructorTerm()); } /* empty record literal */ @@ -2155,9 +2146,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(SOLVER, dt[0].getConstructor())); + const api::Datatype& dt = dtype.getDatatype(); + f = MK_TERM(api::APPLY_CONSTRUCTOR, dt[0].getConstructorTerm()); } /* empty set literal */ | LBRACE RBRACE @@ -2254,8 +2244,8 @@ simpleTerm[CVC4::api::Term& f] typeIds.push_back(std::make_pair(names[i], args[i].getSort())); } api::Sort dtype = SOLVER->mkRecordSort(typeIds); - const Datatype& dt = ((DatatypeType)dtype.getType()).getDatatype(); - args.insert(args.begin(), api::Term(SOLVER, dt[0].getConstructor())); + const api::Datatype& dt = dtype.getDatatype(); + args.insert(args.begin(), dt[0].getConstructorTerm()); f = MK_TERM(api::APPLY_CONSTRUCTOR, args); } |