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.

4 files changed, 4 insertions, 4 deletions

diff --git a/examples/nra-translate/smt2toisat.cpp b/examples/nra-translate/smt2toisat.cpp
index 34745ad03..cf6377d98 100644
--- a/examples/nra-translate/smt2toisat.cpp
+++ b/examples/nra-translate/smt2toisat.cpp
@@ -73,7 +73,7 @@ int main(int argc, char* argv[])
     DeclareFunctionCommand* declare = dynamic_cast<DeclareFunctionCommand*>(cmd);
     if (declare) {
       string name = declare->getSymbol();
-      Expr var = parser->getVariable(name);
+      Expr var = parser->getVariable(name).getExpr();
       unsigned n = variables.size();
       variables[var] = n;
       delete cmd;
diff --git a/examples/nra-translate/smt2tomathematica.cpp b/examples/nra-translate/smt2tomathematica.cpp
index c5c2f3af4..916ada0d9 100644
--- a/examples/nra-translate/smt2tomathematica.cpp
+++ b/examples/nra-translate/smt2tomathematica.cpp
@@ -72,7 +72,7 @@ int main(int argc, char* argv[])
     DeclareFunctionCommand* declare = dynamic_cast<DeclareFunctionCommand*>(cmd);
     if (declare) {
       string name = declare->getSymbol();
-      Expr var = parser->getVariable(name);
+      Expr var = parser->getVariable(name).getExpr();
       unsigned n = variables.size();
       variables[var] = n;
       delete cmd;
diff --git a/examples/nra-translate/smt2toqepcad.cpp b/examples/nra-translate/smt2toqepcad.cpp
index cdc2e0878..2750ee191 100644
--- a/examples/nra-translate/smt2toqepcad.cpp
+++ b/examples/nra-translate/smt2toqepcad.cpp
@@ -74,7 +74,7 @@ int main(int argc, char* argv[])
         dynamic_cast<DeclareFunctionCommand*>(cmd);
     if (declare) {
       string name = declare->getSymbol();
-      Expr var = parser->getVariable(name);
+      Expr var = parser->getVariable(name).getExpr();
       unsigned n = variables.size();
       variables[var] = n;
       delete cmd;
diff --git a/examples/nra-translate/smt2toredlog.cpp b/examples/nra-translate/smt2toredlog.cpp
index 654a6a038..638f7c452 100644
--- a/examples/nra-translate/smt2toredlog.cpp
+++ b/examples/nra-translate/smt2toredlog.cpp
@@ -76,7 +76,7 @@ int main(int argc, char* argv[])
     DeclareFunctionCommand* declare = dynamic_cast<DeclareFunctionCommand*>(cmd);
     if (declare) {
       string name = declare->getSymbol();
-      Expr var = parser->getVariable(name);
+      Expr var = parser->getVariable(name).getExpr();
       unsigned n = variables.size();
       variables[var] = n;
       delete cmd;