From b1f4694c582a315feccb4c0c7e1a683583ff29e8 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 9 Dec 2020 12:44:03 -0600 Subject: Make decision engine independent of AssertionsPipeline (#5626) This PR makes decision engine independent of AssertionsPipeline, which consequently allows some of the key PropEngine interfaces to be consolidated. It also modifies PropEngine to take TrustNode for assertLemma, which is the first step for making PropEngine manage proofs from TheoryEngine. This is in preparation for modifying the interplay between PropEngine, TheoryEngine, TheoryPreprocessor, and new proposed SAT relevancy heuristic. There are no intended behavior changes in this PR. Marking "major" since this impacts several current directions (including proof-new integration, lazy theory preprocessing, SAT relevancy). --- src/decision/decision_engine.cpp | 7 ++++--- src/decision/decision_engine.h | 8 +++++--- src/decision/decision_strategy.h | 13 ++++++++++--- src/decision/justification_heuristic.cpp | 19 ++++++++----------- src/decision/justification_heuristic.h | 5 +++-- 5 files changed, 30 insertions(+), 22 deletions(-) (limited to 'src/decision') diff --git a/src/decision/decision_engine.cpp b/src/decision/decision_engine.cpp index 6ebd73a5f..ec8943f4a 100644 --- a/src/decision/decision_engine.cpp +++ b/src/decision/decision_engine.cpp @@ -113,8 +113,9 @@ SatValue DecisionEngine::getPolarity(SatVariable var) } } -void DecisionEngine::addAssertions( - const preprocessing::AssertionPipeline& assertions) +void DecisionEngine::addAssertions(const std::vector& assertions, + const std::vector& ppLemmas, + const std::vector& ppSkolems) { // new assertions, reset whatever result we knew d_result = SAT_VALUE_UNKNOWN; @@ -126,7 +127,7 @@ void DecisionEngine::addAssertions( for(unsigned i = 0; i < d_needIteSkolemMap.size(); ++i) { - d_needIteSkolemMap[i]->addAssertions(assertions); + d_needIteSkolemMap[i]->addAssertions(assertions, ppLemmas, ppSkolems); } } diff --git a/src/decision/decision_engine.h b/src/decision/decision_engine.h index 52e1e2d1a..afa16397d 100644 --- a/src/decision/decision_engine.h +++ b/src/decision/decision_engine.h @@ -24,7 +24,6 @@ #include "base/output.h" #include "decision/decision_strategy.h" #include "expr/node.h" -#include "preprocessing/assertion_pipeline.h" #include "prop/cnf_stream.h" #include "prop/prop_engine.h" #include "prop/sat_solver_types.h" @@ -142,9 +141,12 @@ class DecisionEngine { // External World helping us help the Strategies /** - * Add a list of assertions from an AssertionPipeline. + * Add a list of assertions, as well as lemmas coming from preprocessing + * (ppLemmas) and pairwise the skolems they constrain (ppSkolems). */ - void addAssertions(const preprocessing::AssertionPipeline& assertions); + void addAssertions(const std::vector& assertions, + const std::vector& ppLemmas, + const std::vector& ppSkolems); // Interface for Strategies to use stuff stored in Decision Engine // (which was possibly requested by them on initialization) diff --git a/src/decision/decision_strategy.h b/src/decision/decision_strategy.h index f7c28299d..ebddc659d 100644 --- a/src/decision/decision_strategy.h +++ b/src/decision/decision_strategy.h @@ -19,7 +19,9 @@ #ifndef CVC4__DECISION__DECISION_STRATEGY_H #define CVC4__DECISION__DECISION_STRATEGY_H -#include "preprocessing/assertion_pipeline.h" +#include + +#include "expr/node.h" #include "prop/sat_solver_types.h" #include "smt/term_formula_removal.h" @@ -58,8 +60,13 @@ public: bool needIteSkolemMap() override { return true; } - virtual void addAssertions( - const preprocessing::AssertionPipeline& assertions) = 0; + /** + * Add a list of assertions, as well as lemmas coming from preprocessing + * (ppLemmas) and pairwise the skolems they constrain (ppSkolems). + */ + virtual void addAssertions(const std::vector& assertions, + const std::vector& ppLemmas, + const std::vector& ppSkolems) = 0; };/* class ITEDecisionStrategy */ class RelevancyStrategy : public ITEDecisionStrategy { diff --git a/src/decision/justification_heuristic.cpp b/src/decision/justification_heuristic.cpp index baf0056e9..afbff18c1 100644 --- a/src/decision/justification_heuristic.cpp +++ b/src/decision/justification_heuristic.cpp @@ -164,15 +164,14 @@ inline void computeXorIffDesiredValues } } -void JustificationHeuristic::addAssertions( - const preprocessing::AssertionPipeline &assertions) +void JustificationHeuristic::addAssertions(const std::vector& assertions, + const std::vector& ppLemmas, + const std::vector& ppSkolems) { - size_t assertionsEnd = assertions.getRealAssertionsEnd(); - + Assert(ppSkolems.size() == ppLemmas.size()); Trace("decision") << "JustificationHeuristic::addAssertions()" << " size = " << assertions.size() - << " assertionsEnd = " << assertionsEnd << std::endl; // Save all assertions locally, including the assertions generated by term @@ -198,13 +197,11 @@ void JustificationHeuristic::addAssertions( } // Save mapping between ite skolems and ite assertions - for (const std::pair &i : assertions.getIteSkolemMap()) + for (size_t i = 0, nlemmas = ppLemmas.size(); i < nlemmas; i++) { - Trace("decision::jh::ite") << " jh-ite: " << (i.first) << " maps to " - << assertions[(i.second)] << std::endl; - Assert(i.second >= assertionsEnd && i.second < assertions.size()); - - d_skolemAssertions[i.first] = assertions[i.second]; + Trace("decision::jh::ite") << " jh-ite: " << ppSkolems[i] << " maps to " + << ppLemmas[i] << std::endl; + d_skolemAssertions[ppSkolems[i]] = ppLemmas[i]; } // Automatic weight computation diff --git a/src/decision/justification_heuristic.h b/src/decision/justification_heuristic.h index 5ecb5eb08..81b08f1a6 100644 --- a/src/decision/justification_heuristic.h +++ b/src/decision/justification_heuristic.h @@ -121,8 +121,9 @@ public: prop::SatLiteral getNext(bool &stopSearch) override; - void addAssertions( - const preprocessing::AssertionPipeline &assertions) override; + void addAssertions(const std::vector& assertions, + const std::vector& ppLemmas, + const std::vector& ppSkolems) override; private: /* getNext with an option to specify threshold */ -- cgit v1.2.3