From 500f85f9c664001b84a90f4836bbb9577b871e29 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 5 Mar 2020 16:16:15 -0600 Subject: Migrate a majority of the functionality in parsers to the new API (#3838) This PR migrates a majority of the functionality of the parsers (cvc, tptp, smt2/sygus) to the new API. The main omitted functionality not addressed in this PR is the datatypes. Largely, the Expr-level Datatype is still used throughout. Remaining tasks: Migrate the Datatypes to the new API in cvc/smt2. Eliminate the use of ExprManager::mkVar (with flags for DEFINED/GLOBAL). For the latter, I have made a utility function in Parser::mkVar that captures all calls to this function. Notice that the existing mkVar/mkBoundVar/mkDefinedFun have been renamed to the more fitting names bindVar/bindBoundVar/bindDefinedFun etc. Note: this PR contains no major code changes, each line of code should roughly correspond one-to-one with the changed version. This fixes CVC4/cvc4-projects#77, fixes CVC4/cvc4-projects#78, fixes CVC4/cvc4-projects#80, fixes CVC4/cvc4-projects#85. --- test/unit/parser/parser_black.h | 24 ++++++++++++------------ 1 file changed, 12 insertions(+), 12 deletions(-) (limited to 'test/unit/parser') diff --git a/test/unit/parser/parser_black.h b/test/unit/parser/parser_black.h index e00016f45..85b379ac0 100644 --- a/test/unit/parser/parser_black.h +++ b/test/unit/parser/parser_black.h @@ -45,21 +45,21 @@ class ParserBlack /* Set up declaration context for expr inputs */ virtual void setupContext(Parser& parser) { /* a, b, c: BOOLEAN */ - parser.mkVar("a", d_solver->getExprManager()->booleanType()); - parser.mkVar("b", d_solver->getExprManager()->booleanType()); - parser.mkVar("c", d_solver->getExprManager()->booleanType()); + parser.bindVar("a", d_solver->getBooleanSort()); + parser.bindVar("b", d_solver->getBooleanSort()); + parser.bindVar("c", d_solver->getBooleanSort()); /* t, u, v: TYPE */ - Type t = parser.mkSort("t"); - Type u = parser.mkSort("u"); - Type v = parser.mkSort("v"); + api::Sort t = parser.mkSort("t"); + api::Sort u = parser.mkSort("u"); + api::Sort v = parser.mkSort("v"); /* f : t->u; g: u->v; h: v->t; */ - parser.mkVar("f", d_solver->getExprManager()->mkFunctionType(t, u)); - parser.mkVar("g", d_solver->getExprManager()->mkFunctionType(u, v)); - parser.mkVar("h", d_solver->getExprManager()->mkFunctionType(v, t)); + parser.bindVar("f", d_solver->mkFunctionSort(t, u)); + parser.bindVar("g", d_solver->mkFunctionSort(u, v)); + parser.bindVar("h", d_solver->mkFunctionSort(v, t)); /* x:t; y:u; z:v; */ - parser.mkVar("x",t); - parser.mkVar("y",u); - parser.mkVar("z",v); + parser.bindVar("x", t); + parser.bindVar("y", u); + parser.bindVar("z", v); } void tryGoodInput(const string goodInput) -- cgit v1.2.3