From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Mon, 12 Oct 2020 16:14:08 +0000 (-0500)
Subject: Eliminate uses of Expr in SmtEngine interface (#5240)
X-Git-Tag: cvc5-1.0.0~2723
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=3ce6e00068c02286704143d82d5f044fdb356516;p=cvc5.git

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.
---

diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp
index 4dda6098e..0384b573e 100644
--- a/src/api/cvc4cpp.cpp
+++ b/src/api/cvc4cpp.cpp
@@ -4556,7 +4556,7 @@ Result Solver::checkEntailed(Term term) const
   CVC4_API_ARG_CHECK_NOT_NULL(term);
   CVC4_API_SOLVER_CHECK_TERM(term);
 
-  CVC4::Result r = d_smtEngine->checkEntailed(term.d_node->toExpr());
+  CVC4::Result r = d_smtEngine->checkEntailed(*term.d_node);
   return Result(r);
 
   CVC4_API_SOLVER_TRY_CATCH_END;
@@ -4576,7 +4576,7 @@ Result Solver::checkEntailed(const std::vector<Term>& terms) const
     CVC4_API_ARG_CHECK_NOT_NULL(term);
   }
 
-  std::vector<Expr> exprs = termVectorToExprs(terms);
+  std::vector<Node> exprs = termVectorToNodes(terms);
   CVC4::Result r = d_smtEngine->checkEntailed(exprs);
   return Result(r);
 
@@ -4626,7 +4626,7 @@ Result Solver::checkSatAssuming(Term assumption) const
       << "Cannot make multiple queries unless incremental solving is enabled "
          "(try --incremental)";
   CVC4_API_SOLVER_CHECK_TERM(assumption);
-  CVC4::Result r = d_smtEngine->checkSat(assumption.d_node->toExpr());
+  CVC4::Result r = d_smtEngine->checkSat(*assumption.d_node);
   return Result(r);
   CVC4_API_SOLVER_TRY_CATCH_END;
 }
@@ -4647,7 +4647,7 @@ Result Solver::checkSatAssuming(const std::vector<Term>& assumptions) const
     CVC4_API_SOLVER_CHECK_TERM(term);
     CVC4_API_ARG_CHECK_NOT_NULL(term);
   }
-  std::vector<Expr> eassumptions = termVectorToExprs(assumptions);
+  std::vector<Node> eassumptions = termVectorToNodes(assumptions);
   CVC4::Result r = d_smtEngine->checkSat(eassumptions);
   return Result(r);
   CVC4_API_SOLVER_TRY_CATCH_END;
@@ -4731,7 +4731,7 @@ Term Solver::defineFun(const std::string& symbol,
   CVC4_API_SOLVER_TRY_CATCH_BEGIN;
   CVC4_API_ARG_CHECK_EXPECTED(sort.isFirstClass(), sort)
       << "first-class sort as codomain sort for function sort";
-  std::vector<Type> domain_types;
+  std::vector<TypeNode> domain_types;
   for (size_t i = 0, size = bound_vars.size(); i < size; ++i)
   {
     CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
@@ -4747,20 +4747,21 @@ Term Solver::defineFun(const std::string& symbol,
     CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
         t.isFirstClass(), "sort of parameter", bound_vars[i], i)
         << "first-class sort of parameter of defined function";
-    domain_types.push_back(t);
+    domain_types.push_back(TypeNode::fromType(t));
   }
   CVC4_API_SOLVER_CHECK_SORT(sort);
   CVC4_API_CHECK(sort == term.getSort())
       << "Invalid sort of function body '" << term << "', expected '" << sort
       << "'";
-  Type type = *sort.d_type;
+  NodeManager* nm = getNodeManager();
+  TypeNode type = TypeNode::fromType(*sort.d_type);
   if (!domain_types.empty())
   {
-    type = d_exprMgr->mkFunctionType(domain_types, type);
+    type = nm->mkFunctionType(domain_types, type);
   }
-  Expr fun = d_exprMgr->mkVar(symbol, type);
-  std::vector<Expr> ebound_vars = termVectorToExprs(bound_vars);
-  d_smtEngine->defineFunction(fun, ebound_vars, term.d_node->toExpr(), global);
+  Node fun = Node::fromExpr(d_exprMgr->mkVar(symbol, type.toType()));
+  std::vector<Node> ebound_vars = termVectorToNodes(bound_vars);
+  d_smtEngine->defineFunction(fun, ebound_vars, *term.d_node, global);
   return Term(this, fun);
   CVC4_API_SOLVER_TRY_CATCH_END;
 }
@@ -4809,9 +4810,8 @@ Term Solver::defineFun(Term fun,
 
   CVC4_API_SOLVER_CHECK_TERM(term);
 
-  std::vector<Expr> ebound_vars = termVectorToExprs(bound_vars);
-  d_smtEngine->defineFunction(
-      fun.d_node->toExpr(), ebound_vars, term.d_node->toExpr(), global);
+  std::vector<Node> ebound_vars = termVectorToNodes(bound_vars);
+  d_smtEngine->defineFunction(*fun.d_node, ebound_vars, *term.d_node, global);
   return fun;
   CVC4_API_SOLVER_TRY_CATCH_END;
 }
@@ -4838,7 +4838,7 @@ Term Solver::defineFunRec(const std::string& symbol,
   CVC4_API_ARG_CHECK_EXPECTED(sort.isFirstClass(), sort)
       << "first-class sort as function codomain sort";
   Assert(!sort.isFunction()); /* A function sort is not first-class. */
-  std::vector<Type> domain_types;
+  std::vector<TypeNode> domain_types;
   for (size_t i = 0, size = bound_vars.size(); i < size; ++i)
   {
     CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
@@ -4850,7 +4850,7 @@ Term Solver::defineFunRec(const std::string& symbol,
         bound_vars[i],
         i)
         << "a bound variable";
-    CVC4::Type t = bound_vars[i].d_node->getType().toType();
+    CVC4::TypeNode t = bound_vars[i].d_node->getType();
     CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
         t.isFirstClass(), "sort of parameter", bound_vars[i], i)
         << "first-class sort of parameter of defined function";
@@ -4861,13 +4861,14 @@ Term Solver::defineFunRec(const std::string& symbol,
       << "Invalid sort of function body '" << term << "', expected '" << sort
       << "'";
   CVC4_API_SOLVER_CHECK_TERM(term);
-  Type type = *sort.d_type;
+  NodeManager* nm = getNodeManager();
+  TypeNode type = TypeNode::fromType(*sort.d_type);
   if (!domain_types.empty())
   {
-    type = d_exprMgr->mkFunctionType(domain_types, type);
+    type = nm->mkFunctionType(domain_types, type);
   }
-  Expr fun = d_exprMgr->mkVar(symbol, type);
-  std::vector<Expr> ebound_vars = termVectorToExprs(bound_vars);
+  Node fun = Node::fromExpr(d_exprMgr->mkVar(symbol, type.toType()));
+  std::vector<Node> ebound_vars = termVectorToNodes(bound_vars);
   d_smtEngine->defineFunctionRec(
       fun, ebound_vars, term.d_node->toExpr(), global);
   return Term(this, fun);
@@ -4925,9 +4926,9 @@ Term Solver::defineFunRec(Term fun,
   }
 
   CVC4_API_SOLVER_CHECK_TERM(term);
-  std::vector<Expr> ebound_vars = termVectorToExprs(bound_vars);
+  std::vector<Node> ebound_vars = termVectorToNodes(bound_vars);
   d_smtEngine->defineFunctionRec(
-      fun.d_node->toExpr(), ebound_vars, term.d_node->toExpr(), global);
+      *fun.d_node, ebound_vars, *term.d_node, global);
   return fun;
   CVC4_API_SOLVER_TRY_CATCH_END;
 }
@@ -5003,13 +5004,13 @@ void Solver::defineFunsRec(const std::vector<Term>& funs,
           << "function or nullary symbol";
     }
   }
-  std::vector<Expr> efuns = termVectorToExprs(funs);
-  std::vector<std::vector<Expr>> ebound_vars;
+  std::vector<Node> efuns = termVectorToNodes(funs);
+  std::vector<std::vector<Node>> ebound_vars;
   for (const auto& v : bound_vars)
   {
-    ebound_vars.push_back(termVectorToExprs(v));
+    ebound_vars.push_back(termVectorToNodes(v));
   }
-  std::vector<Expr> exprs = termVectorToExprs(terms);
+  std::vector<Node> exprs = termVectorToNodes(terms);
   d_smtEngine->defineFunctionsRec(efuns, ebound_vars, exprs, global);
   CVC4_API_SOLVER_TRY_CATCH_END;
 }
@@ -5028,12 +5029,12 @@ void Solver::echo(std::ostream& out, const std::string& str) const
 std::vector<Term> Solver::getAssertions(void) const
 {
   CVC4_API_SOLVER_TRY_CATCH_BEGIN;
-  std::vector<Expr> assertions = d_smtEngine->getAssertions();
+  std::vector<Node> assertions = d_smtEngine->getAssertions();
   /* Can not use
    *   return std::vector<Term>(assertions.begin(), assertions.end());
    * here since constructor is private */
   std::vector<Term> res;
-  for (const Expr& e : assertions)
+  for (const Node& e : assertions)
   {
     res.push_back(Term(this, e));
   }
@@ -5359,7 +5360,7 @@ void Solver::blockModelValues(const std::vector<Term>& terms) const
       << "Cannot get value when in unsat mode.";
   CVC4_API_ARG_SIZE_CHECK_EXPECTED(!terms.empty(), terms)
       << "a non-empty set of terms";
-  for (int i = 0; i < terms.size(); ++i)
+  for (size_t i = 0, tsize = terms.size(); i < tsize; ++i)
   {
     CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
         !terms[i].isNull(), "term", terms[i], i)
@@ -5369,7 +5370,7 @@ void Solver::blockModelValues(const std::vector<Term>& terms) const
         << "a term associated to this solver object";
   }
   CVC4::ExprManagerScope exmgrs(*(d_exprMgr.get()));
-  d_smtEngine->blockModelValues(termVectorToExprs(terms));
+  d_smtEngine->blockModelValues(termVectorToNodes(terms));
   CVC4_API_SOLVER_TRY_CATCH_END;
 }
 
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
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 -------------------------------------------------------------- */
 
diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp
index 4ab92f6a7..4b45072f7 100644
--- a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp
+++ b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp
@@ -386,7 +386,7 @@ bool CegSingleInv::solve()
     return false;
   }
   // now, get the instantiations
-  std::vector<Expr> qs;
+  std::vector<Node> qs;
   siSmt->getInstantiatedQuantifiedFormulas(qs);
   Assert(qs.size() <= 1);
   // track the instantiations, as solution construction is based on this
@@ -394,15 +394,13 @@ bool CegSingleInv::solve()
                     << std::endl;
   d_inst.clear();
   d_instConds.clear();
-  for (const Expr& q : qs)
+  for (const Node& q : qs)
   {
-    TNode qn = Node::fromExpr(q);
-    Assert(qn.getKind() == FORALL);
-    std::vector<std::vector<Expr> > tvecs;
-    siSmt->getInstantiationTermVectors(q, tvecs);
-    Trace("sygus-si") << "#instantiations of " << q << "=" << tvecs.size()
+    Assert(q.getKind() == FORALL);
+    siSmt->getInstantiationTermVectors(q, d_inst);
+    Trace("sygus-si") << "#instantiations of " << q << "=" << d_inst.size()
                       << std::endl;
-    // We use the original synthesis conjecture siq, since qn may contain
+    // We use the original synthesis conjecture siq, since q may contain
     // internal symbols e.g. termITE skolem after preprocessing.
     std::vector<Node> vars;
     for (const Node& v : siq[0])
@@ -410,16 +408,10 @@ bool CegSingleInv::solve()
       vars.push_back(v);
     }
     Node body = siq[1];
-    for (unsigned i = 0, ninsts = tvecs.size(); i < ninsts; i++)
+    for (unsigned i = 0, ninsts = d_inst.size(); i < ninsts; i++)
     {
-      std::vector<Expr>& tvi = tvecs[i];
-      std::vector<Node> inst;
-      for (const Expr& t : tvi)
-      {
-        inst.push_back(Node::fromExpr(t));
-      }
+      std::vector<Node>& inst = d_inst[i];
       Trace("sygus-si") << "  Instantiation: " << inst << std::endl;
-      d_inst.push_back(inst);
       // instantiation should have same arity since we are not allowed to
       // eliminate variables from quantifiers marked with QuantElimAttribute.
       Assert(inst.size() == vars.size());
diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp
index 2d0a80599..b8cbdf6b3 100644
--- a/src/theory/theory_model.cpp
+++ b/src/theory/theory_model.cpp
@@ -98,6 +98,17 @@ void TheoryModel::setHeapModel( Node h, Node neq ) {
   d_sep_nil_eq = neq;
 }
 
+bool TheoryModel::getHeapModel(Node& h, Node& neq) const
+{
+  if (d_sep_heap.isNull() || d_sep_nil_eq.isNull())
+  {
+    return false;
+  }
+  h = d_sep_heap;
+  neq = d_sep_nil_eq;
+  return true;
+}
+
 bool TheoryModel::getHeapModel( Expr& h, Expr& neq ) const {
   if( d_sep_heap.isNull() || d_sep_nil_eq.isNull() ){
     return false;
diff --git a/src/theory/theory_model.h b/src/theory/theory_model.h
index b1401c074..9f330ff6c 100644
--- a/src/theory/theory_model.h
+++ b/src/theory/theory_model.h
@@ -301,6 +301,8 @@ public:
   /** set the heap and value sep.nil is equal to */
   void setHeapModel(Node h, Node neq);
   /** get the heap and value sep.nil is equal to */
+  bool getHeapModel(Node& h, Node& neq) const;
+  /** get the heap and value sep.nil is equal to */
   bool getHeapModel(Expr& h, Expr& neq) const override;
   //---------------------------- end separation logic
 
diff --git a/test/unit/expr/type_node_white.h b/test/unit/expr/type_node_white.h
index 4d268fbf6..22d3f0d84 100644
--- a/test/unit/expr/type_node_white.h
+++ b/test/unit/expr/type_node_white.h
@@ -64,9 +64,9 @@ class TypeNodeWhite : public CxxTest::TestSuite {
     Node xPos = d_nm->mkNode(GT, x, d_nm->mkConst(Rational(0)));
     TypeNode funtype = d_nm->mkFunctionType(integerType, booleanType);
     Node lambda = d_nm->mkVar("lambda", funtype);
-    vector<Expr> formals;
-    formals.push_back(x.toExpr());
-    d_smt->defineFunction(lambda.toExpr(), formals, xPos.toExpr());
+    vector<Node> formals;
+    formals.push_back(x);
+    d_smt->defineFunction(lambda, formals, xPos);
 
     TS_ASSERT( not realType.isComparableTo(booleanType) );
     TS_ASSERT( realType.isComparableTo(integerType) );