diff options
Diffstat (limited to 'src/decision')
-rw-r--r-- | src/decision/decision_engine.cpp | 7 | ||||
-rw-r--r-- | src/decision/decision_engine.h | 8 | ||||
-rw-r--r-- | src/decision/decision_strategy.h | 13 | ||||
-rw-r--r-- | src/decision/justification_heuristic.cpp | 19 | ||||
-rw-r--r-- | src/decision/justification_heuristic.h | 5 |
5 files changed, 30 insertions, 22 deletions
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<Node>& assertions, + const std::vector<Node>& ppLemmas, + const std::vector<Node>& 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<Node>& assertions, + const std::vector<Node>& ppLemmas, + const std::vector<Node>& 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 <vector> + +#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<Node>& assertions, + const std::vector<Node>& ppLemmas, + const std::vector<Node>& 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<Node>& assertions, + const std::vector<Node>& ppLemmas, + const std::vector<Node>& 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<const Node, unsigned> &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<Node>& assertions, + const std::vector<Node>& ppLemmas, + const std::vector<Node>& ppSkolems) override; private: /* getNext with an option to specify threshold */ |