summaryrefslogtreecommitdiff
path: root/src/decision
diff options
context:
space:
mode:
Diffstat (limited to 'src/decision')
-rw-r--r--src/decision/decision_engine.cpp28
-rw-r--r--src/decision/decision_engine.h18
-rw-r--r--src/decision/decision_strategy.h6
-rw-r--r--src/decision/justification_heuristic.cpp28
-rw-r--r--src/decision/justification_heuristic.h6
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 */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback