From 3b87ce3ab67fd463a733ad11402e32f94eb1017e Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Wed, 15 Jul 2020 16:42:00 -0700 Subject: 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. --- src/theory/quantifiers/expr_miner.cpp | 2 +- src/theory/quantifiers/sygus/ce_guided_single_inv.cpp | 2 +- src/theory/quantifiers/sygus/cegis_core_connective.cpp | 4 ++-- src/theory/quantifiers/sygus/sygus_repair_const.cpp | 2 +- 4 files changed, 5 insertions(+), 5 deletions(-) (limited to 'src/theory/quantifiers') 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& 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 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; -- cgit v1.2.3