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.

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)