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.

1 files changed, 7 insertions, 12 deletions

diff --git a/src/smt/interpolation_solver.cpp b/src/smt/interpolation_solver.cpp
index d2193d226..ffcb09a23 100644
--- a/src/smt/interpolation_solver.cpp
+++ b/src/smt/interpolation_solver.cpp
@@ -44,12 +44,7 @@ bool InterpolationSolver::getInterpol(const Node& conj,
   }
   Trace("sygus-interpol") << "SmtEngine::getInterpol: conjecture " << conj
                           << std::endl;
-  std::vector<Expr> easserts = d_parent->getExpandedAssertions();
-  std::vector<Node> axioms;
-  for (unsigned i = 0, size = easserts.size(); i < size; i++)
-  {
-    axioms.push_back(Node::fromExpr(easserts[i]));
-  }
+  std::vector<Node> axioms = d_parent->getExpandedAssertions();
   // must expand definitions
   Node conjn = d_parent->expandDefinitions(conj);
   std::string name("A");
@@ -60,7 +55,7 @@ bool InterpolationSolver::getInterpol(const Node& conj,
   {
     if (options::checkInterpols())
     {
-      checkInterpol(interpol.toExpr(), easserts, conj);
+      checkInterpol(interpol.toExpr(), axioms, conj);
     }
     return true;
   }
@@ -73,8 +68,8 @@ bool InterpolationSolver::getInterpol(const Node& conj, Node& interpol)
   return getInterpol(conj, grammarType, interpol);
 }
 
-void InterpolationSolver::checkInterpol(Expr interpol,
-                                        const std::vector<Expr>& easserts,
+void InterpolationSolver::checkInterpol(Node interpol,
+                                        const std::vector<Node>& easserts,
                                         const Node& conj)
 {
   Assert(interpol.getType().isBoolean());
@@ -98,18 +93,18 @@ void InterpolationSolver::checkInterpol(Expr interpol,
                             << ": asserting formulas" << std::endl;
     if (j == 0)
     {
-      for (const Expr& e : easserts)
+      for (const Node& e : easserts)
       {
         itpChecker->assertFormula(e);
       }
-      Expr negitp = interpol.notExpr();
+      Node negitp = interpol.notNode();
       itpChecker->assertFormula(negitp);
     }
     else
     {
       itpChecker->assertFormula(interpol);
       Assert(!conj.isNull());
-      itpChecker->assertFormula(conj.toExpr().notExpr());
+      itpChecker->assertFormula(conj.notNode());
     }
     Trace("check-interpol") << "SmtEngine::checkInterpol: phase " << j
                             << ": check the assertions" << std::endl;