diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2020-07-15 16:42:00 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-07-15 18:42:00 -0500 |
commit | 3b87ce3ab67fd463a733ad11402e32f94eb1017e (patch) | |
tree | f58e422e35ca61ca61045f09643d61d2e500a77c /src/theory/quantifiers | |
parent | f1351ca7462d3d601e0dec78b71f54e0c7ee381f (diff) |
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.
Diffstat (limited to 'src/theory/quantifiers')
4 files changed, 5 insertions, 5 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; |