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.

10 files changed, 178 insertions, 249 deletions

diff --git a/src/smt/abduction_solver.cpp b/src/smt/abduction_solver.cpp
index 1de044fd4..3f03c00e2 100644
--- a/src/smt/abduction_solver.cpp
+++ b/src/smt/abduction_solver.cpp
@@ -39,12 +39,7 @@ bool AbductionSolver::getAbduct(const Node& goal,
     throw ModalException(msg);
   }
   Trace("sygus-abduct") << "SmtEngine::getAbduct: goal " << goal << 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();
   std::vector<Node> asserts(axioms.begin(), axioms.end());
   // must expand definitions
   Node conjn = d_parent->expandDefinitions(goal);
@@ -139,8 +134,8 @@ void AbductionSolver::checkAbduct(Node a)
   Trace("check-abduct") << "SmtEngine::checkAbduct: get expanded assertions"
                         << std::endl;
 
-  std::vector<Expr> asserts = d_parent->getExpandedAssertions();
-  asserts.push_back(a.toExpr());
+  std::vector<Node> asserts = d_parent->getExpandedAssertions();
+  asserts.push_back(a);
 
   // two checks: first, consistent with assertions, second, implies negated goal
   // is unsatisfiable.
@@ -153,7 +148,7 @@ void AbductionSolver::checkAbduct(Node a)
     initializeSubsolver(abdChecker);
     Trace("check-abduct") << "SmtEngine::checkAbduct: phase " << j
                           << ": asserting formulas" << std::endl;
-    for (const Expr& e : asserts)
+    for (const Node& e : asserts)
     {
       abdChecker->assertFormula(e);
     }
@@ -177,7 +172,7 @@ void AbductionSolver::checkAbduct(Node a)
           << "SmtEngine::checkAbduct: goal is " << d_abdConj << std::endl;
       // add the goal to the set of assertions
       Assert(!d_abdConj.isNull());
-      asserts.push_back(d_abdConj.toExpr());
+      asserts.push_back(d_abdConj);
     }
     else
     {
diff --git a/src/smt/defined_function.h b/src/smt/defined_function.h
index 0a4fc181f..c2e594fe7 100644
--- a/src/smt/defined_function.h
+++ b/src/smt/defined_function.h
@@ -34,7 +34,7 @@ class DefinedFunction
 {
  public:
   DefinedFunction() {}
-  DefinedFunction(Node func, std::vector<Node>& formals, Node formula)
+  DefinedFunction(Node func, const std::vector<Node>& formals, Node formula)
       : d_func(func), d_formals(formals), d_formula(formula)
   {
   }
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;
diff --git a/src/smt/interpolation_solver.h b/src/smt/interpolation_solver.h
index 8e6d2cd14..096cf8983 100644
--- a/src/smt/interpolation_solver.h
+++ b/src/smt/interpolation_solver.h
@@ -71,8 +71,8 @@ class InterpolationSolver
    * the interpolation problem (interpol), and the solution implies the goal
    * (conj). If these criteria are not met, an internal error is thrown.
    */
-  void checkInterpol(Expr interpol,
-                     const std::vector<Expr>& easserts,
+  void checkInterpol(Node interpol,
+                     const std::vector<Node>& easserts,
                      const Node& conj);
 
  private:
diff --git a/src/smt/model_blocker.cpp b/src/smt/model_blocker.cpp
index 8d232ed9e..9d15b5690 100644
--- a/src/smt/model_blocker.cpp
+++ b/src/smt/model_blocker.cpp
@@ -23,24 +23,15 @@ using namespace CVC4::kind;
 
 namespace CVC4 {
 
-Expr ModelBlocker::getModelBlocker(const std::vector<Expr>& assertions,
+Node ModelBlocker::getModelBlocker(const std::vector<Node>& assertions,
                                    theory::TheoryModel* m,
                                    options::BlockModelsMode mode,
-                                   const std::vector<Expr>& exprToBlock)
+                                   const std::vector<Node>& exprToBlock)
 {
   NodeManager* nm = NodeManager::currentNM();
   // convert to nodes
-  std::vector<Node> tlAsserts;
-  for (const Expr& a : assertions)
-  {
-    Node an = Node::fromExpr(a);
-    tlAsserts.push_back(an);
-  }
-  std::vector<Node> nodesToBlock;
-  for (const Expr& eb : exprToBlock)
-  {
-    nodesToBlock.push_back(Node::fromExpr(eb));
-  }
+  std::vector<Node> tlAsserts = assertions;
+  std::vector<Node> nodesToBlock = exprToBlock;
   Trace("model-blocker") << "Compute model blocker, assertions:" << std::endl;
   Node blocker;
   if (mode == options::BlockModelsMode::LITERALS)
@@ -117,7 +108,7 @@ Expr ModelBlocker::getModelBlocker(const std::vector<Expr>& assertions,
               // rewrite, this ensures that e.g. the propositional value of
               // quantified formulas can be queried
               n = theory::Rewriter::rewrite(n);
-              Node vn = Node::fromExpr(m->getValue(n.toExpr()));
+              Node vn = m->getValue(n);
               Assert(vn.isConst());
               if (vn.getConst<bool>() == cpol)
               {
@@ -139,7 +130,7 @@ Expr ModelBlocker::getModelBlocker(const std::vector<Expr>& assertions,
         }
         else if (catom.getKind() == ITE)
         {
-          Node vcond = Node::fromExpr(m->getValue(cur[0].toExpr()));
+          Node vcond = m->getValue(cur[0]);
           Assert(vcond.isConst());
           Node cond = cur[0];
           Node branch;
@@ -282,7 +273,7 @@ Expr ModelBlocker::getModelBlocker(const std::vector<Expr>& assertions,
     }
   }
   Trace("model-blocker") << "...model blocker is " << blocker << std::endl;
-  return blocker.toExpr();
+  return blocker;
 }
 
 } /* namespace CVC4 */
diff --git a/src/smt/model_blocker.h b/src/smt/model_blocker.h
index 0ee40a88a..92d200d40 100644
--- a/src/smt/model_blocker.h
+++ b/src/smt/model_blocker.h
@@ -59,11 +59,11 @@ class ModelBlocker
    * our input. In other words, we do not return ~(x < 0) V ~(w < 0) since the
    * left disjunct is always false.
    */
-  static Expr getModelBlocker(
-      const std::vector<Expr>& assertions,
+  static Node getModelBlocker(
+      const std::vector<Node>& assertions,
       theory::TheoryModel* m,
       options::BlockModelsMode mode,
-      const std::vector<Expr>& exprToBlock = std::vector<Expr>());
+      const std::vector<Node>& exprToBlock = std::vector<Node>());
 }; /* class TheoryModelCoreBuilder */
 
 }  // namespace CVC4
diff --git a/src/smt/model_core_builder.cpp b/src/smt/model_core_builder.cpp
index c6a73df75..59dac63e8 100644
--- a/src/smt/model_core_builder.cpp
+++ b/src/smt/model_core_builder.cpp
@@ -20,7 +20,7 @@ using namespace CVC4::kind;
 
 namespace CVC4 {
 
-bool ModelCoreBuilder::setModelCore(const std::vector<Expr>& assertions,
+bool ModelCoreBuilder::setModelCore(const std::vector<Node>& assertions,
                                     Model* m,
                                     options::ModelCoresMode mode)
 {
@@ -34,14 +34,9 @@ bool ModelCoreBuilder::setModelCore(const std::vector<Expr>& assertions,
   }
 
   // convert to nodes
-  std::vector<Node> asserts;
-  for (unsigned i = 0, size = assertions.size(); i < size; i++)
-  {
-    asserts.push_back(Node::fromExpr(assertions[i]));
-  }
   NodeManager* nm = NodeManager::currentNM();
 
-  Node formula = asserts.size() > 1? nm->mkNode(AND, asserts) : asserts[0];
+  Node formula = nm->mkAnd(assertions);
   std::vector<Node> vars;
   std::vector<Node> subs;
   Trace("model-core") << "Assignments: " << std::endl;
diff --git a/src/smt/model_core_builder.h b/src/smt/model_core_builder.h
index d4d2a8441..984c61d04 100644
--- a/src/smt/model_core_builder.h
+++ b/src/smt/model_core_builder.h
@@ -54,7 +54,7 @@ class ModelCoreBuilder
    * If m is not a model for assertions, this method returns false and m is
    * left unchanged.
    */
-  static bool setModelCore(const std::vector<Expr>& assertions,
+  static bool setModelCore(const std::vector<Node>& assertions,
                            Model* m,
                            options::ModelCoresMode mode);
 }; /* class TheoryModelCoreBuilder */
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index ff45ce0ce..205865e16 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -71,7 +71,6 @@
 #include "smt/abduction_solver.h"
 #include "smt/abstract_values.h"
 #include "smt/assertions.h"
-#include "smt/node_command.h"
 #include "smt/defined_function.h"
 #include "smt/dump_manager.h"
 #include "smt/expr_names.h"
@@ -80,6 +79,7 @@
 #include "smt/logic_request.h"
 #include "smt/model_blocker.h"
 #include "smt/model_core_builder.h"
+#include "smt/node_command.h"
 #include "smt/options_manager.h"
 #include "smt/preprocessor.h"
 #include "smt/proof_manager.h"
@@ -94,6 +94,7 @@
 #include "smt_util/boolean_simplification.h"
 #include "smt_util/nary_builder.h"
 #include "theory/logic_info.h"
+#include "theory/quantifiers/quantifiers_attributes.h"
 #include "theory/rewriter.h"
 #include "theory/sort_inference.h"
 #include "theory/substitutions.h"
@@ -114,20 +115,6 @@ using namespace CVC4::theory;
 
 namespace CVC4 {
 
-// !!! Temporary until commands are migrated to the new API !!!
-std::vector<Node> exprVectorToNodes(const std::vector<Expr>& exprs)
-{
-  std::vector<Node> nodes;
-  nodes.reserve(exprs.size());
-
-  for (Expr e : exprs)
-  {
-    nodes.push_back(Node::fromExpr(e));
-  }
-
-  return nodes;
-}
-
 SmtEngine::SmtEngine(ExprManager* em, Options* optr)
     : d_state(new SmtEngineState(*this)),
       d_exprManager(em),
@@ -650,33 +637,36 @@ CVC4::SExpr SmtEngine::getInfo(const std::string& key) const
   return SExpr::parseListOfListOfAtoms(current_options);
 }
 
-void SmtEngine::debugCheckFormals(const std::vector<Expr>& formals, Expr func)
+void SmtEngine::debugCheckFormals(const std::vector<Node>& formals, Node func)
 {
-  for(std::vector<Expr>::const_iterator i = formals.begin(); i != formals.end(); ++i) {
+  for (std::vector<Node>::const_iterator i = formals.begin();
+       i != formals.end();
+       ++i)
+  {
     if((*i).getKind() != kind::BOUND_VARIABLE) {
       stringstream ss;
       ss << "All formal arguments to defined functions must be BOUND_VARIABLEs, but in the\n"
          << "definition of function " << func << ", formal\n"
          << "  " << *i << "\n"
          << "has kind " << (*i).getKind();
-      throw TypeCheckingException(func, ss.str());
+      throw TypeCheckingException(func.toExpr(), ss.str());
     }
   }
 }
 
-void SmtEngine::debugCheckFunctionBody(Expr formula,
-                                       const std::vector<Expr>& formals,
-                                       Expr func)
+void SmtEngine::debugCheckFunctionBody(Node formula,
+                                       const std::vector<Node>& formals,
+                                       Node func)
 {
-  Type formulaType = formula.getType(options::typeChecking());
-  Type funcType = func.getType();
+  TypeNode formulaType = formula.getType(options::typeChecking());
+  TypeNode funcType = func.getType();
   // We distinguish here between definitions of constants and functions,
   // because the type checking for them is subtly different.  Perhaps we
   // should instead have SmtEngine::defineFunction() and
   // SmtEngine::defineConstant() for better clarity, although then that
   // doesn't match the SMT-LIBv2 standard...
   if(formals.size() > 0) {
-    Type rangeType = FunctionType(funcType).getRangeType();
+    TypeNode rangeType = funcType.getRangeType();
     if(! formulaType.isComparableTo(rangeType)) {
       stringstream ss;
       ss << "Type of defined function does not match its declaration\n"
@@ -684,24 +674,24 @@ void SmtEngine::debugCheckFunctionBody(Expr formula,
          << "Declared type : " << rangeType << "\n"
          << "The body      : " << formula << "\n"
          << "Body type     : " << formulaType;
-      throw TypeCheckingException(func, ss.str());
+      throw TypeCheckingException(func.toExpr(), ss.str());
     }
   } else {
     if(! formulaType.isComparableTo(funcType)) {
       stringstream ss;
       ss << "Declared type of defined constant does not match its definition\n"
          << "The constant   : " << func << "\n"
-         << "Declared type  : " << funcType << " " << Type::getTypeNode(funcType)->getId() << "\n"
+         << "Declared type  : " << funcType << "\n"
          << "The definition : " << formula << "\n"
-         << "Definition type: " << formulaType << " " << Type::getTypeNode(formulaType)->getId();
-      throw TypeCheckingException(func, ss.str());
+         << "Definition type: " << formulaType;
+      throw TypeCheckingException(func.toExpr(), ss.str());
     }
   }
 }
 
-void SmtEngine::defineFunction(Expr func,
-                               const std::vector<Expr>& formals,
-                               Expr formula,
+void SmtEngine::defineFunction(Node func,
+                               const std::vector<Node>& formals,
+                               Node formula,
                                bool global)
 {
   SmtScope smts(this);
@@ -717,13 +707,12 @@ void SmtEngine::defineFunction(Expr func,
   std::vector<Node> nFormals;
   nFormals.reserve(formals.size());
 
-  for (const Expr& formal : formals)
+  for (const Node& formal : formals)
   {
-    nFormals.push_back(formal.getNode());
+    nFormals.push_back(formal);
   }
 
-  DefineFunctionNodeCommand nc(
-      ss.str(), func.getNode(), nFormals, formula.getNode());
+  DefineFunctionNodeCommand nc(ss.str(), func, nFormals, formula);
   d_dumpm->addToModelCommandAndDump(
       nc, ExprManager::VAR_FLAG_DEFINED, true, "declarations");
 
@@ -731,36 +720,27 @@ void SmtEngine::defineFunction(Expr func,
   debugCheckFunctionBody(formula, formals, func);
 
   // Substitute out any abstract values in formula
-  Node formNode = d_absValues->substituteAbstractValues(Node::fromExpr(formula));
-
-  TNode funcNode = func.getTNode();
-  vector<Node> formalsNodes;
-  for(vector<Expr>::const_iterator i = formals.begin(),
-        iend = formals.end();
-      i != iend;
-      ++i) {
-    formalsNodes.push_back((*i).getNode());
-  }
-  DefinedFunction def(funcNode, formalsNodes, formNode);
+  Node formNode = d_absValues->substituteAbstractValues(formula);
+  DefinedFunction def(func, formals, formNode);
   // Permit (check-sat) (define-fun ...) (get-value ...) sequences.
   // Otherwise, (check-sat) (get-value ((! foo :named bar))) breaks
   // d_haveAdditions = true;
-  Debug("smt") << "definedFunctions insert " << funcNode << " " << formNode << endl;
+  Debug("smt") << "definedFunctions insert " << func << " " << formNode << endl;
 
   if (global)
   {
-    d_definedFunctions->insertAtContextLevelZero(funcNode, def);
+    d_definedFunctions->insertAtContextLevelZero(func, def);
   }
   else
   {
-    d_definedFunctions->insert(funcNode, def);
+    d_definedFunctions->insert(func, def);
   }
 }
 
 void SmtEngine::defineFunctionsRec(
-    const std::vector<Expr>& funcs,
-    const std::vector<std::vector<Expr>>& formals,
-    const std::vector<Expr>& formulas,
+    const std::vector<Node>& funcs,
+    const std::vector<std::vector<Node>>& formals,
+    const std::vector<Node>& formulas,
     bool global)
 {
   SmtScope smts(this);
@@ -789,22 +769,15 @@ void SmtEngine::defineFunctionsRec(
 
   if (Dump.isOn("raw-benchmark"))
   {
-    std::vector<Node> nFuncs = exprVectorToNodes(funcs);
-    std::vector<std::vector<Node>> nFormals;
-    for (const std::vector<Expr>& formal : formals)
-    {
-      nFormals.emplace_back(exprVectorToNodes(formal));
-    }
-    std::vector<Node> nFormulas = exprVectorToNodes(formulas);
     getOutputManager().getPrinter().toStreamCmdDefineFunctionRec(
-        getOutputManager().getDumpOut(), nFuncs, nFormals, nFormulas);
+        getOutputManager().getDumpOut(), funcs, formals, formulas);
   }
 
-  ExprManager* em = getExprManager();
+  NodeManager* nm = getNodeManager();
   for (unsigned i = 0, size = funcs.size(); i < size; i++)
   {
     // we assert a quantified formula
-    Expr func_app;
+    Node func_app;
     // make the function application
     if (formals[i].empty())
     {
@@ -813,52 +786,49 @@ void SmtEngine::defineFunctionsRec(
     }
     else
     {
-      std::vector<Expr> children;
+      std::vector<Node> children;
       children.push_back(funcs[i]);
       children.insert(children.end(), formals[i].begin(), formals[i].end());
-      func_app = em->mkExpr(kind::APPLY_UF, children);
+      func_app = nm->mkNode(kind::APPLY_UF, children);
     }
-    Expr lem = em->mkExpr(kind::EQUAL, func_app, formulas[i]);
+    Node lem = nm->mkNode(kind::EQUAL, func_app, formulas[i]);
     if (!formals[i].empty())
     {
       // set the attribute to denote this is a function definition
-      std::string attr_name("fun-def");
-      Expr aexpr = em->mkExpr(kind::INST_ATTRIBUTE, func_app);
-      aexpr = em->mkExpr(kind::INST_PATTERN_LIST, aexpr);
-      std::vector<Expr> expr_values;
-      std::string str_value;
-      setUserAttribute(attr_name, func_app, expr_values, str_value);
+      Node aexpr = nm->mkNode(kind::INST_ATTRIBUTE, func_app);
+      aexpr = nm->mkNode(kind::INST_PATTERN_LIST, aexpr);
+      FunDefAttribute fda;
+      func_app.setAttribute(fda, true);
       // make the quantified formula
-      Expr boundVars = em->mkExpr(kind::BOUND_VAR_LIST, formals[i]);
-      lem = em->mkExpr(kind::FORALL, boundVars, lem, aexpr);
+      Node boundVars = nm->mkNode(kind::BOUND_VAR_LIST, formals[i]);
+      lem = nm->mkNode(kind::FORALL, boundVars, lem, aexpr);
     }
     // assert the quantified formula
     //   notice we don't call assertFormula directly, since this would
     //   duplicate the output on raw-benchmark.
-    Node lemn = Node::fromExpr(lem);
     // add define recursive definition to the assertions
-    d_asserts->addDefineFunRecDefinition(lemn, global);
+    d_asserts->addDefineFunRecDefinition(lem, global);
   }
 }
 
-void SmtEngine::defineFunctionRec(Expr func,
-                                  const std::vector<Expr>& formals,
-                                  Expr formula,
+void SmtEngine::defineFunctionRec(Node func,
+                                  const std::vector<Node>& formals,
+                                  Node formula,
                                   bool global)
 {
-  std::vector<Expr> funcs;
+  std::vector<Node> funcs;
   funcs.push_back(func);
-  std::vector<std::vector<Expr> > formals_multi;
+  std::vector<std::vector<Node>> formals_multi;
   formals_multi.push_back(formals);
-  std::vector<Expr> formulas;
+  std::vector<Node> formulas;
   formulas.push_back(formula);
   defineFunctionsRec(funcs, formals_multi, formulas, global);
 }
 
-bool SmtEngine::isDefinedFunction( Expr func ){
-  Node nf = Node::fromExpr( func );
-  Debug("smt") << "isDefined function " << nf << "?" << std::endl;
-  return d_definedFunctions->find(nf) != d_definedFunctions->end();
+bool SmtEngine::isDefinedFunction(Node func)
+{
+  Debug("smt") << "isDefined function " << func << "?" << std::endl;
+  return d_definedFunctions->find(func) != d_definedFunctions->end();
 }
 
 Result SmtEngine::quickCheck() {
@@ -942,7 +912,13 @@ void SmtEngine::notifyPostSolvePost()
   te->postsolve();
 }
 
-Result SmtEngine::checkSat(const Expr& assumption, bool inUnsatCore)
+Result SmtEngine::checkSat()
+{
+  Node nullNode;
+  return checkSat(nullNode);
+}
+
+Result SmtEngine::checkSat(const Node& assumption, bool inUnsatCore)
 {
   if (Dump.isOn("benchmark"))
   {
@@ -952,12 +928,13 @@ Result SmtEngine::checkSat(const Expr& assumption, bool inUnsatCore)
   std::vector<Node> assump;
   if (!assumption.isNull())
   {
-    assump.push_back(Node::fromExpr(assumption));
+    assump.push_back(assumption);
   }
   return checkSatInternal(assump, inUnsatCore, false);
 }
 
-Result SmtEngine::checkSat(const vector<Expr>& assumptions, bool inUnsatCore)
+Result SmtEngine::checkSat(const std::vector<Node>& assumptions,
+                           bool inUnsatCore)
 {
   if (Dump.isOn("benchmark"))
   {
@@ -969,43 +946,33 @@ Result SmtEngine::checkSat(const vector<Expr>& assumptions, bool inUnsatCore)
     else
     {
       getOutputManager().getPrinter().toStreamCmdCheckSatAssuming(
-          getOutputManager().getDumpOut(), exprVectorToNodes(assumptions));
+          getOutputManager().getDumpOut(), assumptions);
     }
   }
-  std::vector<Node> assumps;
-  for (const Expr& e : assumptions)
-  {
-    assumps.push_back(Node::fromExpr(e));
-  }
-  return checkSatInternal(assumps, inUnsatCore, false);
+  return checkSatInternal(assumptions, inUnsatCore, false);
 }
 
-Result SmtEngine::checkEntailed(const Expr& node, bool inUnsatCore)
+Result SmtEngine::checkEntailed(const Node& node, bool inUnsatCore)
 {
   if (Dump.isOn("benchmark"))
   {
     getOutputManager().getPrinter().toStreamCmdQuery(
-        getOutputManager().getDumpOut(), node.getNode());
+        getOutputManager().getDumpOut(), node);
   }
-  return checkSatInternal(node.isNull()
-                              ? std::vector<Node>()
-                              : std::vector<Node>{Node::fromExpr(node)},
-                          inUnsatCore,
-                          true)
+  return checkSatInternal(
+             node.isNull() ? std::vector<Node>() : std::vector<Node>{node},
+             inUnsatCore,
+             true)
       .asEntailmentResult();
 }
 
-Result SmtEngine::checkEntailed(const vector<Expr>& nodes, bool inUnsatCore)
+Result SmtEngine::checkEntailed(const std::vector<Node>& nodes,
+                                bool inUnsatCore)
 {
-  std::vector<Node> ns;
-  for (const Expr& e : nodes)
-  {
-    ns.push_back(Node::fromExpr(e));
-  }
-  return checkSatInternal(ns, inUnsatCore, true).asEntailmentResult();
+  return checkSatInternal(nodes, inUnsatCore, true).asEntailmentResult();
 }
 
-Result SmtEngine::checkSatInternal(const vector<Node>& assumptions,
+Result SmtEngine::checkSatInternal(const std::vector<Node>& assumptions,
                                    bool inUnsatCore,
                                    bool isEntailmentCheck)
 {
@@ -1272,12 +1239,12 @@ Node SmtEngine::getValue(const Node& ex) const
   return resultNode;
 }
 
-vector<Expr> SmtEngine::getValues(const vector<Expr>& exprs)
+std::vector<Node> SmtEngine::getValues(const std::vector<Node>& exprs)
 {
-  vector<Expr> result;
-  for (const Expr& e : exprs)
+  std::vector<Node> result;
+  for (const Node& e : exprs)
   {
-    result.push_back(getValue(e).toExpr());
+    result.push_back(getValue(e));
   }
   return result;
 }
@@ -1400,7 +1367,7 @@ Model* SmtEngine::getModel() {
   {
     // If we enabled model cores, we compute a model core for m based on our
     // (expanded) assertions using the model core builder utility
-    std::vector<Expr> eassertsProc = getExpandedAssertions();
+    std::vector<Node> eassertsProc = getExpandedAssertions();
     ModelCoreBuilder::setModelCore(eassertsProc, m, options::modelCoresMode());
   }
   m->d_inputName = d_state->getFilename();
@@ -1431,13 +1398,13 @@ Result SmtEngine::blockModel()
   }
 
   // get expanded assertions
-  std::vector<Expr> eassertsProc = getExpandedAssertions();
-  Expr eblocker = ModelBlocker::getModelBlocker(
+  std::vector<Node> eassertsProc = getExpandedAssertions();
+  Node eblocker = ModelBlocker::getModelBlocker(
       eassertsProc, m, options::blockModelsMode());
-  return assertFormula(Node::fromExpr(eblocker));
+  return assertFormula(eblocker);
 }
 
-Result SmtEngine::blockModelValues(const std::vector<Expr>& exprs)
+Result SmtEngine::blockModelValues(const std::vector<Node>& exprs)
 {
   Trace("smt") << "SMT blockModelValues()" << endl;
   SmtScope smts(this);
@@ -1447,20 +1414,20 @@ Result SmtEngine::blockModelValues(const std::vector<Expr>& exprs)
   if (Dump.isOn("benchmark"))
   {
     getOutputManager().getPrinter().toStreamCmdBlockModelValues(
-        getOutputManager().getDumpOut(), exprVectorToNodes(exprs));
+        getOutputManager().getDumpOut(), exprs);
   }
 
   TheoryModel* m = getAvailableModel("block model values");
 
   // get expanded assertions
-  std::vector<Expr> eassertsProc = getExpandedAssertions();
+  std::vector<Node> eassertsProc = getExpandedAssertions();
   // we always do block model values mode here
-  Expr eblocker = ModelBlocker::getModelBlocker(
+  Node eblocker = ModelBlocker::getModelBlocker(
       eassertsProc, m, options::BlockModelsMode::VALUES, exprs);
-  return assertFormula(Node::fromExpr(eblocker));
+  return assertFormula(eblocker);
 }
 
-std::pair<Expr, Expr> SmtEngine::getSepHeapAndNilExpr(void)
+std::pair<Node, Node> SmtEngine::getSepHeapAndNilExpr(void)
 {
   if (!d_logic.isTheoryEnabled(THEORY_SEP))
   {
@@ -1479,27 +1446,26 @@ std::pair<Expr, Expr> SmtEngine::getSepHeapAndNilExpr(void)
         << "SmtEngine::getSepHeapAndNilExpr(): failed to obtain heap/nil "
            "expressions from theory model.";
   }
-  return std::make_pair(heap, nil);
+  return std::make_pair(Node::fromExpr(heap), Node::fromExpr(nil));
 }
 
-std::vector<Expr> SmtEngine::getExpandedAssertions()
+std::vector<Node> SmtEngine::getExpandedAssertions()
 {
-  std::vector<Expr> easserts = getAssertions();
+  std::vector<Node> easserts = getAssertions();
   // must expand definitions
-  std::vector<Expr> eassertsProc;
+  std::vector<Node> eassertsProc;
   std::unordered_map<Node, Node, NodeHashFunction> cache;
-  for (const Expr& e : easserts)
+  for (const Node& e : easserts)
   {
-    Node ea = Node::fromExpr(e);
-    Node eae = d_pp->expandDefinitions(ea, cache);
-    eassertsProc.push_back(eae.toExpr());
+    Node eae = d_pp->expandDefinitions(e, cache);
+    eassertsProc.push_back(eae);
   }
   return eassertsProc;
 }
 
-Expr SmtEngine::getSepHeapExpr() { return getSepHeapAndNilExpr().first; }
+Node SmtEngine::getSepHeapExpr() { return getSepHeapAndNilExpr().first; }
 
-Expr SmtEngine::getSepNilExpr() { return getSepHeapAndNilExpr().second; }
+Node SmtEngine::getSepNilExpr() { return getSepHeapAndNilExpr().second; }
 
 UnsatCore SmtEngine::getUnsatCoreInternal()
 {
@@ -1618,7 +1584,7 @@ void SmtEngine::checkModel(bool hardFailure) {
       // We'll first do some checks, then add to our substitution map
       // the mapping: function symbol |-> value
 
-      Expr func = c->getFunction().toExpr();
+      Node func = c->getFunction();
       Node val = m->getValue(func);
 
       Notice() << "SmtEngine::checkModel(): adding substitution: " << func << " |-> " << val << endl;
@@ -1634,7 +1600,8 @@ void SmtEngine::checkModel(bool hardFailure) {
         // [func->func2] and checking equality of the Nodes.
         // (this just a way to check if func is in n.)
         SubstitutionMap subs(&fakeContext);
-        Node func2 = NodeManager::currentNM()->mkSkolem("", TypeNode::fromType(func.getType()), "", NodeManager::SKOLEM_NO_NOTIFY);
+        Node func2 = NodeManager::currentNM()->mkSkolem(
+            "", func.getType(), "", NodeManager::SKOLEM_NO_NOTIFY);
         subs.addSubstitution(func, func2);
         if(subs.apply(n) != n) {
           Notice() << "SmtEngine::checkModel(): *** PROBLEM: MODEL VALUE DEFINED IN TERMS OF ITSELF ***" << endl;
@@ -1853,6 +1820,7 @@ bool SmtEngine::getInterpol(const Node& conj,
                             const TypeNode& grammarType,
                             Node& interpol)
 {
+  SmtScope smts(this);
   bool success = d_interpolSolver->getInterpol(conj, grammarType, interpol);
   // notify the state of whether the get-interpol call was successfuly, which
   // impacts the SMT mode.
@@ -1870,6 +1838,7 @@ bool SmtEngine::getAbduct(const Node& conj,
                           const TypeNode& grammarType,
                           Node& abd)
 {
+  SmtScope smts(this);
   bool success = d_abductSolver->getAbduct(conj, grammarType, abd);
   // notify the state of whether the get-abduct call was successfuly, which
   // impacts the SMT mode.
@@ -1883,49 +1852,33 @@ bool SmtEngine::getAbduct(const Node& conj, Node& abd)
   return getAbduct(conj, grammarType, abd);
 }
 
-void SmtEngine::getInstantiatedQuantifiedFormulas( std::vector< Expr >& qs ) {
+void SmtEngine::getInstantiatedQuantifiedFormulas(std::vector<Node>& qs)
+{
   SmtScope smts(this);
   TheoryEngine* te = getTheoryEngine();
   Assert(te != nullptr);
-  std::vector<Node> qs_n;
-  te->getInstantiatedQuantifiedFormulas(qs_n);
-  for (std::size_t i = 0, n = qs_n.size(); i < n; i++)
-  {
-    qs.push_back(qs_n[i].toExpr());
-  }
+  te->getInstantiatedQuantifiedFormulas(qs);
 }
 
-void SmtEngine::getInstantiations( Expr q, std::vector< Expr >& insts ) {
+void SmtEngine::getInstantiations(Node q, std::vector<Node>& insts)
+{
   SmtScope smts(this);
   TheoryEngine* te = getTheoryEngine();
   Assert(te != nullptr);
-  std::vector<Node> insts_n;
-  te->getInstantiations(Node::fromExpr(q), insts_n);
-  for (std::size_t i = 0, n = insts_n.size(); i < n; i++)
-  {
-    insts.push_back(insts_n[i].toExpr());
-  }
+  te->getInstantiations(q, insts);
 }
 
-void SmtEngine::getInstantiationTermVectors( Expr q, std::vector< std::vector< Expr > >& tvecs ) {
+void SmtEngine::getInstantiationTermVectors(
+    Node q, std::vector<std::vector<Node>>& tvecs)
+{
   SmtScope smts(this);
   Assert(options::trackInstLemmas());
   TheoryEngine* te = getTheoryEngine();
   Assert(te != nullptr);
-  std::vector<std::vector<Node>> tvecs_n;
-  te->getInstantiationTermVectors(Node::fromExpr(q), tvecs_n);
-  for (std::size_t i = 0, n = tvecs_n.size(); i < n; i++)
-  {
-    std::vector<Expr> tvec;
-    for (std::size_t j = 0, m = tvecs_n[i].size(); j < m; j++)
-    {
-      tvec.push_back(tvecs_n[i][j].toExpr());
-    }
-    tvecs.push_back(tvec);
-  }
+  te->getInstantiationTermVectors(q, tvecs);
 }
 
-std::vector<Expr> SmtEngine::getAssertions()
+std::vector<Node> SmtEngine::getAssertions()
 {
   SmtScope smts(this);
   finishInit();
@@ -1942,10 +1895,10 @@ std::vector<Expr> SmtEngine::getAssertions()
   }
   context::CDList<Node>* al = d_asserts->getAssertionList();
   Assert(al != nullptr);
-  std::vector<Expr> res;
+  std::vector<Node> res;
   for (const Node& n : *al)
   {
-    res.emplace_back(n.toExpr());
+    res.emplace_back(n);
   }
   // copy the result out
   return res;
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 1b8789513..62e54a0c1 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -306,13 +306,13 @@ class CVC4_PUBLIC SmtEngine
    *
    * The return value has the same meaning as that of assertFormula.
    */
-  Result blockModelValues(const std::vector<Expr>& exprs);
+  Result blockModelValues(const std::vector<Node>& exprs);
 
   /** When using separation logic, obtain the expression for the heap.  */
-  Expr getSepHeapExpr();
+  Node getSepHeapExpr();
 
   /** When using separation logic, obtain the expression for nil.  */
-  Expr getSepNilExpr();
+  Node getSepNilExpr();
 
   /**
    * Get an aspect of the current SMT execution environment.
@@ -333,13 +333,13 @@ class CVC4_PUBLIC SmtEngine
    * @param global True if this definition is global (i.e. should persist when
    *               popping the user context)
    */
-  void defineFunction(Expr func,
-                      const std::vector<Expr>& formals,
-                      Expr formula,
+  void defineFunction(Node func,
+                      const std::vector<Node>& formals,
+                      Node formula,
                       bool global = false);
 
   /** Return true if given expression is a defined function. */
-  bool isDefinedFunction(Expr func);
+  bool isDefinedFunction(Node func);
 
   /**
    * Define functions recursive
@@ -359,17 +359,17 @@ class CVC4_PUBLIC SmtEngine
    * @param global True if this definition is global (i.e. should persist when
    *               popping the user context)
    */
-  void defineFunctionsRec(const std::vector<Expr>& funcs,
-                          const std::vector<std::vector<Expr>>& formals,
-                          const std::vector<Expr>& formulas,
+  void defineFunctionsRec(const std::vector<Node>& funcs,
+                          const std::vector<std::vector<Node>>& formals,
+                          const std::vector<Node>& formulas,
                           bool global = false);
   /**
    * Define function recursive
    * Same as above, but for a single function.
    */
-  void defineFunctionRec(Expr func,
-                         const std::vector<Expr>& formals,
-                         Expr formula,
+  void defineFunctionRec(Node func,
+                         const std::vector<Node>& formals,
+                         Node formula,
                          bool global = false);
   /**
    * Add a formula to the current context: preprocess, do per-theory
@@ -391,9 +391,8 @@ class CVC4_PUBLIC SmtEngine
    *
    * @throw Exception
    */
-  Result checkEntailed(const Expr& assumption = Expr(),
-                       bool inUnsatCore = true);
-  Result checkEntailed(const std::vector<Expr>& assumptions,
+  Result checkEntailed(const Node& assumption, bool inUnsatCore = true);
+  Result checkEntailed(const std::vector<Node>& assumptions,
                        bool inUnsatCore = true);
 
   /**
@@ -402,8 +401,9 @@ class CVC4_PUBLIC SmtEngine
    *
    * @throw Exception
    */
-  Result checkSat(const Expr& assumption = Expr(), bool inUnsatCore = true);
-  Result checkSat(const std::vector<Expr>& assumptions,
+  Result checkSat();
+  Result checkSat(const Node& assumption, bool inUnsatCore = true);
+  Result checkSat(const std::vector<Node>& assumptions,
                   bool inUnsatCore = true);
 
   /**
@@ -528,7 +528,7 @@ class CVC4_PUBLIC SmtEngine
   /**
    * Same as getValue but for a vector of expressions
    */
-  std::vector<Expr> getValues(const std::vector<Expr>& exprs);
+  std::vector<Node> getValues(const std::vector<Node>& exprs);
 
   /**
    * Add a function to the set of expressions whose value is to be
@@ -666,7 +666,7 @@ class CVC4_PUBLIC SmtEngine
    * Get list of quantified formulas that were instantiated on the last call
    * to check-sat.
    */
-  void getInstantiatedQuantifiedFormulas(std::vector<Expr>& qs);
+  void getInstantiatedQuantifiedFormulas(std::vector<Node>& qs);
 
   /**
    * Get instantiations for quantified formula q.
@@ -679,7 +679,7 @@ class CVC4_PUBLIC SmtEngine
    * In particular, if q is of the form forall x. P(x), then insts is a list
    * of formulas of the form P(t1), ..., P(tn).
    */
-  void getInstantiations(Expr q, std::vector<Expr>& insts);
+  void getInstantiations(Node q, std::vector<Node>& insts);
   /**
    * Get instantiation term vectors for quantified formula q.
    *
@@ -689,8 +689,8 @@ class CVC4_PUBLIC SmtEngine
    * Notice that these are not guaranteed to come in the same order as the
    * instantiation lemmas above.
    */
-  void getInstantiationTermVectors(Expr q,
-                                   std::vector<std::vector<Expr> >& tvecs);
+  void getInstantiationTermVectors(Node q,
+                                   std::vector<std::vector<Node>>& tvecs);
 
   /**
    * Get an unsatisfiable core (only if immediately preceded by an UNSAT or
@@ -703,7 +703,7 @@ class CVC4_PUBLIC SmtEngine
    * Get the current set of assertions.  Only permitted if the
    * SmtEngine is set to operate interactively.
    */
-  std::vector<Expr> getAssertions();
+  std::vector<Node> getAssertions();
 
   /**
    * Push a user-level context.
@@ -879,7 +879,7 @@ class CVC4_PUBLIC SmtEngine
    *
    * Return the set of assertions, after expanding definitions.
    */
-  std::vector<Expr> getExpandedAssertions();
+  std::vector<Node> getExpandedAssertions();
   /* .......................................................................  */
  private:
   /* .......................................................................  */
@@ -949,8 +949,8 @@ class CVC4_PUBLIC SmtEngine
    * the interpolation problem (interpol), and the solution implies the goal
    * (conj). If these criteria are not met, an internal error is thrown.
    */
-  void checkInterpol(Expr interpol,
-                     const std::vector<Expr>& easserts,
+  void checkInterpol(Node interpol,
+                     const std::vector<Node>& easserts,
                      const Node& conj);
 
   /**
@@ -1037,23 +1037,23 @@ class CVC4_PUBLIC SmtEngine
    * the function that the formal argument list is for. This method is used
    * as a helper function when defining (recursive) functions.
    */
-  void debugCheckFormals(const std::vector<Expr>& formals, Expr func);
+  void debugCheckFormals(const std::vector<Node>& formals, Node func);
 
   /**
    * Checks whether formula is a valid function body for func whose formal
    * argument list is stored in formals. This method is
    * used as a helper function when defining (recursive) functions.
    */
-  void debugCheckFunctionBody(Expr formula,
-                              const std::vector<Expr>& formals,
-                              Expr func);
+  void debugCheckFunctionBody(Node formula,
+                              const std::vector<Node>& formals,
+                              Node func);
 
   /**
    * Helper method to obtain both the heap and nil from the solver. Returns a
    * std::pair where the first element is the heap expression and the second
    * element is the nil expression.
    */
-  std::pair<Expr, Expr> getSepHeapAndNilExpr();
+  std::pair<Node, Node> getSepHeapAndNilExpr();
 
   /* Members -------------------------------------------------------------- */