Eliminate uses of Expr in SmtEngine interface (#5240)

This eliminates all use of Expr in the SmtEngine except in a few interfaces (setUserAttribute, getAssignment) whose signature is currently in question.

The next steps will be to (1) eliminate Expr from the smt/model.h interface, (2) replace Type by TypeNode in Sort.

4 files changed, 13 insertions, 14 deletions

diff --git a/src/preprocessing/passes/bv_to_int.cpp b/src/preprocessing/passes/bv_to_int.cpp
index 06a5714d3..eaae7d71d 100644
--- a/src/preprocessing/passes/bv_to_int.cpp
+++ b/src/preprocessing/passes/bv_to_int.cpp
@@ -815,7 +815,7 @@ void BVToInt::defineBVUFAsIntUF(Node bvUF, Node intUF)
   // The type of the resulting term
   TypeNode resultType;
   // symbolic arguments of original function
-  vector<Expr> args;
+  vector<Node> args;
   if (!bvUF.getType().isFunction()) {
     // bvUF is a variable.
     // in this case, the result is just the original term
@@ -837,7 +837,7 @@ void BVToInt::defineBVUFAsIntUF(Node bvUF, Node intUF)
       // Each bit-vector argument is casted to a natural number
       // Other arguments are left intact.
       Node fresh_bound_var = d_nm->mkBoundVar(d);
-      args.push_back(fresh_bound_var.toExpr());
+      args.push_back(fresh_bound_var);
       Node castedArg = args[i];
       if (d.isBitVector())
       {
@@ -851,8 +851,7 @@ void BVToInt::defineBVUFAsIntUF(Node bvUF, Node intUF)
   // If the result is BV, it needs to be casted back.
   result = castToType(result, resultType);
   // add the function definition to the smt engine.
-  smt::currentSmtEngine()->defineFunction(
-      bvUF.toExpr(), args, result.toExpr(), true);
+  d_preprocContext->getSmt()->defineFunction(bvUF, args, result, true);
 }
 
 bool BVToInt::childrenTypesChanged(Node n)
diff --git a/src/preprocessing/passes/quantifier_macros.cpp b/src/preprocessing/passes/quantifier_macros.cpp
index 8fea4cbac..604f8719c 100644
--- a/src/preprocessing/passes/quantifier_macros.cpp
+++ b/src/preprocessing/passes/quantifier_macros.cpp
@@ -504,20 +504,21 @@ void QuantifierMacros::finalizeDefinitions() {
   if( options::incrementalSolving() || options::produceModels() || doDefs ){
     Trace("macros") << "Store as defined functions..." << std::endl;
     //also store as defined functions
+    SmtEngine* smt = d_preprocContext->getSmt();
     for( std::map< Node, Node >::iterator it = d_macro_defs.begin(); it != d_macro_defs.end(); ++it ){
       Trace("macros-def") << "Macro definition for " << it->first << " : " << it->second << std::endl;
       Trace("macros-def") << "  basis is : ";
       std::vector< Node > nargs;
-      std::vector< Expr > args;
+      std::vector<Node> args;
       for( unsigned i=0; i<d_macro_basis[it->first].size(); i++ ){
         Node bv = NodeManager::currentNM()->mkBoundVar( d_macro_basis[it->first][i].getType() );
         Trace("macros-def") << d_macro_basis[it->first][i] << " ";
         nargs.push_back( bv );
-        args.push_back( bv.toExpr() );
+        args.push_back(bv);
       }
       Trace("macros-def") << std::endl;
       Node sbody = it->second.substitute( d_macro_basis[it->first].begin(), d_macro_basis[it->first].end(), nargs.begin(), nargs.end() );
-      smt::currentSmtEngine()->defineFunction( it->first.toExpr(), args, sbody.toExpr() );
+      smt->defineFunction(it->first, args, sbody);
 
       if( Trace.isOn("macros-warn") ){
         debugMacroDefinition( it->first, sbody );
diff --git a/src/preprocessing/passes/real_to_int.cpp b/src/preprocessing/passes/real_to_int.cpp
index 046a1c990..672e281d7 100644
--- a/src/preprocessing/passes/real_to_int.cpp
+++ b/src/preprocessing/passes/real_to_int.cpp
@@ -181,9 +181,8 @@ Node RealToInt::realToIntInternal(TNode n, NodeMap& cache, std::vector<Node>& va
           var_eq.push_back(n.eqNode(ret));
           // ensure that the original variable is defined to be the returned
           // one, which is important for models and for incremental solving.
-          std::vector<Expr> args;
-          smt::currentSmtEngine()->defineFunction(
-              n.toExpr(), args, ret.toExpr());
+          std::vector<Node> args;
+          d_preprocContext->getSmt()->defineFunction(n, args, ret);
         }
       }
     }
diff --git a/src/preprocessing/passes/sygus_inference.cpp b/src/preprocessing/passes/sygus_inference.cpp
index cdacd740a..ea767e771 100644
--- a/src/preprocessing/passes/sygus_inference.cpp
+++ b/src/preprocessing/passes/sygus_inference.cpp
@@ -44,21 +44,21 @@ PreprocessingPassResult SygusInference::applyInternal(
   {
     Assert(funs.size() == sols.size());
     // if so, sygus gives us function definitions
-    SmtEngine* master_smte = smt::currentSmtEngine();
+    SmtEngine* master_smte = d_preprocContext->getSmt();
     for (unsigned i = 0, size = funs.size(); i < size; i++)
     {
-      std::vector<Expr> args;
+      std::vector<Node> args;
       Node sol = sols[i];
       // if it is a non-constant function
       if (sol.getKind() == LAMBDA)
       {
         for (const Node& v : sol[0])
         {
-          args.push_back(v.toExpr());
+          args.push_back(v);
         }
         sol = sol[1];
       }
-      master_smte->defineFunction(funs[i].toExpr(), args, sol.toExpr());
+      master_smte->defineFunction(funs[i], args, sol);
     }
 
     // apply substitution to everything, should result in SAT