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 | |
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')
-rw-r--r-- | src/theory/quantifiers/expr_miner.cpp | 2 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/ce_guided_single_inv.cpp | 2 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/cegis_core_connective.cpp | 4 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/sygus_repair_const.cpp | 2 | ||||
-rw-r--r-- | src/theory/smt_engine_subsolver.cpp | 4 |
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) { |