Use Nodes for SmtEngine assertions (#4752)

This commit changes SmtEngine::assertFormula() to use Nodes rather
than Exprs and changes AssertionList to be Node-based. This is
work towards removing the Expr layer.

5 files changed, 7 insertions, 7 deletions

diff --git a/src/theory/quantifiers/expr_miner.cpp b/src/theory/quantifiers/expr_miner.cpp
index 00a627adf..72e47fac8 100644
--- a/src/theory/quantifiers/expr_miner.cpp
+++ b/src/theory/quantifiers/expr_miner.cpp
@@ -80,7 +80,7 @@ void ExprMiner::initializeChecker(std::unique_ptr<SmtEngine>& checker,
   // Convert bound variables to skolems. This ensures the satisfiability
   // check is ground.
   Node squery = convertToSkolem(query);
-  checker->assertFormula(squery.toExpr());
+  checker->assertFormula(squery);
 }
 
 Result ExprMiner::doCheck(Node query)
diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp
index 0612c85f8..cd9bbeb1f 100644
--- a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp
+++ b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp
@@ -377,7 +377,7 @@ bool CegSingleInv::solve()
   // solve the single invocation conjecture using a fresh copy of SMT engine
   std::unique_ptr<SmtEngine> siSmt;
   initializeSubsolver(siSmt);
-  siSmt->assertFormula(siq.toExpr());
+  siSmt->assertFormula(siq);
   Result r = siSmt->checkSat();
   Trace("sygus-si") << "Result: " << r << std::endl;
   if (r.asSatisfiabilityResult().isSat() != Result::UNSAT)
diff --git a/src/theory/quantifiers/sygus/cegis_core_connective.cpp b/src/theory/quantifiers/sygus/cegis_core_connective.cpp
index dcdd89c1b..a7f32155c 100644
--- a/src/theory/quantifiers/sygus/cegis_core_connective.cpp
+++ b/src/theory/quantifiers/sygus/cegis_core_connective.cpp
@@ -744,7 +744,7 @@ Node CegisCoreConnective::constructSolutionFromPool(Component& ccheck,
     Node query = rasserts.size() == 1 ? rasserts[0] : nm->mkNode(AND, rasserts);
     for (const Node& a : rasserts)
     {
-      checkSol->assertFormula(a.toExpr());
+      checkSol->assertFormula(a);
     }
     Result r = checkSol->checkSat();
     Trace("sygus-ccore") << "----- check-sat returned " << r << std::endl;
@@ -782,7 +782,7 @@ Node CegisCoreConnective::constructSolutionFromPool(Component& ccheck,
           std::shuffle(scasserts.begin(), scasserts.end(), Random::getRandom());
           for (const Node& sca : scasserts)
           {
-            checkSc->assertFormula(sca.toExpr());
+            checkSc->assertFormula(sca);
           }
           Result rsc = checkSc->checkSat();
           Trace("sygus-ccore")
diff --git a/src/theory/quantifiers/sygus/sygus_repair_const.cpp b/src/theory/quantifiers/sygus/sygus_repair_const.cpp
index 3e632fc56..2514b05e2 100644
--- a/src/theory/quantifiers/sygus/sygus_repair_const.cpp
+++ b/src/theory/quantifiers/sygus/sygus_repair_const.cpp
@@ -235,7 +235,7 @@ bool SygusRepairConst::repairSolution(Node sygusBody,
   repcChecker->setOption("miniscope-quant", true);
   repcChecker->setOption("miniscope-quant-fv", true);
   repcChecker->setOption("quant-split", true);
-  repcChecker->assertFormula(fo_body.toExpr());
+  repcChecker->assertFormula(fo_body);
   // check satisfiability
   Result r = repcChecker->checkSat();
   Trace("sygus-repair-const") << "...got : " << r << std::endl;
diff --git a/src/theory/smt_engine_subsolver.cpp b/src/theory/smt_engine_subsolver.cpp
index 863d1ab86..41526c30d 100644
--- a/src/theory/smt_engine_subsolver.cpp
+++ b/src/theory/smt_engine_subsolver.cpp
@@ -70,7 +70,7 @@ Result checkWithSubsolver(std::unique_ptr<SmtEngine>& smte,
     return r;
   }
   initializeSubsolver(smte, needsTimeout, timeout);
-  smte->assertFormula(query.toExpr());
+  smte->assertFormula(query);
   return smte->checkSat();
 }
 
@@ -106,7 +106,7 @@ Result checkWithSubsolver(Node query,
   }
   std::unique_ptr<SmtEngine> smte;
   initializeSubsolver(smte, needsTimeout, timeout);
-  smte->assertFormula(query.toExpr());
+  smte->assertFormula(query);
   r = smte->checkSat();
   if (r.asSatisfiabilityResult().isSat() == Result::SAT)
   {