diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-03-05 16:16:15 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-03-05 16:16:15 -0600 |
commit | 500f85f9c664001b84a90f4836bbb9577b871e29 (patch) | |
tree | be92a8a20267fe7d381ba1a6cf6c9477825776bf /test/unit/parser | |
parent | 50f82fac417bc5b27ecaeb34d4e8034339c5982f (diff) |
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.
Diffstat (limited to 'test/unit/parser')
-rw-r--r-- | test/unit/parser/parser_black.h | 24 |
1 files changed, 12 insertions, 12 deletions
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) |