diff options
Diffstat (limited to 'src/decision')
-rw-r--r-- | src/decision/decision_engine.cpp | 28 | ||||
-rw-r--r-- | src/decision/decision_engine.h | 18 | ||||
-rw-r--r-- | src/decision/decision_strategy.h | 6 | ||||
-rw-r--r-- | src/decision/justification_heuristic.cpp | 28 | ||||
-rw-r--r-- | src/decision/justification_heuristic.h | 6 |
5 files changed, 32 insertions, 54 deletions
diff --git a/src/decision/decision_engine.cpp b/src/decision/decision_engine.cpp index 8e419e768..01f78f2d6 100644 --- a/src/decision/decision_engine.cpp +++ b/src/decision/decision_engine.cpp @@ -98,31 +98,21 @@ SatValue DecisionEngine::getPolarity(SatVariable var) } } -void DecisionEngine::addAssertions(const vector<Node> &assertions) -{ - Assert(false); // doing this so that we revisit what to do - // here. Currently not being used. - - // d_result = SAT_VALUE_UNKNOWN; - // d_assertions.reserve(assertions.size()); - // for(unsigned i = 0; i < assertions.size(); ++i) - // d_assertions.push_back(assertions[i]); -} - -void DecisionEngine::addAssertions(const vector<Node> &assertions, - unsigned assertionsEnd, - IteSkolemMap iteSkolemMap) +void DecisionEngine::addAssertions( + const preprocessing::AssertionPipeline& assertions) { // new assertions, reset whatever result we knew d_result = SAT_VALUE_UNKNOWN; - // d_assertions.reserve(assertions.size()); - for(unsigned i = 0; i < assertions.size(); ++i) - d_assertions.push_back(assertions[i]); + for (const Node& assertion : assertions) + { + d_assertions.push_back(assertion); + } for(unsigned i = 0; i < d_needIteSkolemMap.size(); ++i) - d_needIteSkolemMap[i]-> - addAssertions(assertions, assertionsEnd, iteSkolemMap); + { + d_needIteSkolemMap[i]->addAssertions(assertions); + } } }/* CVC4 namespace */ diff --git a/src/decision/decision_engine.h b/src/decision/decision_engine.h index 838e53b5a..c5325bc9a 100644 --- a/src/decision/decision_engine.h +++ b/src/decision/decision_engine.h @@ -24,11 +24,12 @@ #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" -#include "smt/term_formula_removal.h" #include "smt/smt_engine_scope.h" +#include "smt/term_formula_removal.h" using namespace std; using namespace CVC4::prop; @@ -173,21 +174,10 @@ public: /* return d_needIteSkolemMap.size() > 0; */ /* } */ - /* add a set of assertions */ - void addAssertions(const vector<Node> &assertions); - /** - * add a set of assertions, while providing a mapping between skolem - * variables and corresponding assertions. It is assumed that all - * assertions after assertionEnd were generated by ite - * removal. Hence, iteSkolemMap maps into only these. + * Add a list of assertions from an AssertionPipeline. */ - void addAssertions(const vector<Node> &assertions, - unsigned assertionsEnd, - IteSkolemMap iteSkolemMap); - - /* add a single assertion */ - void addAssertion(Node n); + void addAssertions(const preprocessing::AssertionPipeline& assertions); // 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 bad80d4ef..d26b28eeb 100644 --- a/src/decision/decision_strategy.h +++ b/src/decision/decision_strategy.h @@ -19,6 +19,7 @@ #ifndef __CVC4__DECISION__DECISION_STRATEGY_H #define __CVC4__DECISION__DECISION_STRATEGY_H +#include "preprocessing/assertion_pipeline.h" #include "prop/sat_solver_types.h" #include "smt/term_formula_removal.h" @@ -57,9 +58,8 @@ public: bool needIteSkolemMap() override { return true; } - virtual void addAssertions(const std::vector<Node> &assertions, - unsigned assertionsEnd, - IteSkolemMap iteSkolemMap) = 0; + virtual void addAssertions( + const preprocessing::AssertionPipeline& assertions) = 0; };/* class ITEDecisionStrategy */ class RelevancyStrategy : public ITEDecisionStrategy { diff --git a/src/decision/justification_heuristic.cpp b/src/decision/justification_heuristic.cpp index 7d19d3363..b4fbe1cbd 100644 --- a/src/decision/justification_heuristic.cpp +++ b/src/decision/justification_heuristic.cpp @@ -163,12 +163,10 @@ inline void computeXorIffDesiredValues } } - - -void JustificationHeuristic::addAssertions -(const std::vector<Node> &assertions, - unsigned assertionsEnd, - IteSkolemMap iteSkolemMap) { +void JustificationHeuristic::addAssertions( + const preprocessing::AssertionPipeline &assertions) +{ + size_t assertionsEnd = assertions.getRealAssertionsEnd(); Trace("decision") << "JustificationHeuristic::addAssertions()" @@ -177,19 +175,19 @@ void JustificationHeuristic::addAssertions << std::endl; // Save the 'real' assertions locally - for(unsigned i = 0; i < assertionsEnd; ++i) + for (size_t i = 0; i < assertionsEnd; i++) + { d_assertions.push_back(assertions[i]); + } // Save mapping between ite skolems and ite assertions - for(IteSkolemMap::iterator i = iteSkolemMap.begin(); - i != iteSkolemMap.end(); ++i) { - - Trace("decision::jh::ite") - << " jh-ite: " << (i->first) << " maps to " - << assertions[(i->second)] << std::endl; - Assert(i->second >= assertionsEnd && i->second < assertions.size()); + for (const std::pair<const Node, unsigned> &i : assertions.getIteSkolemMap()) + { + Trace("decision::jh::ite") << " jh-ite: " << (i.first) << " maps to " + << assertions[(i.second)] << std::endl; + Assert(i.second >= assertionsEnd && i.second < assertions.size()); - d_iteAssertions[i->first] = assertions[i->second]; + d_iteAssertions[i.first] = assertions[i.second]; } // Automatic weight computation diff --git a/src/decision/justification_heuristic.h b/src/decision/justification_heuristic.h index a70bee02c..0cd45ada7 100644 --- a/src/decision/justification_heuristic.h +++ b/src/decision/justification_heuristic.h @@ -32,6 +32,7 @@ #include "decision/decision_engine.h" #include "decision/decision_strategy.h" #include "expr/node.h" +#include "preprocessing/assertion_pipeline.h" #include "prop/sat_solver_types.h" namespace CVC4 { @@ -119,9 +120,8 @@ public: prop::SatLiteral getNext(bool &stopSearch) override; - void addAssertions(const std::vector<Node> &assertions, - unsigned assertionsEnd, - IteSkolemMap iteSkolemMap) override; + void addAssertions( + const preprocessing::AssertionPipeline &assertions) override; private: /* getNext with an option to specify threshold */ |