summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/decision/decision_engine.cpp7
-rw-r--r--src/decision/decision_engine.h8
-rw-r--r--src/decision/decision_strategy.h13
-rw-r--r--src/decision/justification_heuristic.cpp19
-rw-r--r--src/decision/justification_heuristic.h5
-rw-r--r--src/prop/prop_engine.cpp54
-rw-r--r--src/prop/prop_engine.h32
-rw-r--r--src/smt/smt_solver.cpp7
-rw-r--r--src/theory/theory_engine.cpp51
9 files changed, 128 insertions, 68 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 */
diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index 26d1e615b..8c1e452e7 100644
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -123,6 +123,28 @@ PropEngine::~PropEngine() {
delete d_theoryProxy;
}
+void PropEngine::notifyPreprocessedAssertions(
+ const preprocessing::AssertionPipeline& ap)
+{
+ // notify the theory engine of preprocessed assertions
+ d_theoryEngine->notifyPreprocessedAssertions(ap.ref());
+
+ // Add assertions to decision engine, which manually extracts what assertions
+ // corresponded to term formula removal. Note that alternatively we could
+ // delay all theory preprocessing and term formula removal to this point, in
+ // which case this method could simply take a vector of Node and not rely on
+ // assertion pipeline or its ITE skolem map.
+ std::vector<Node> ppLemmas;
+ std::vector<Node> ppSkolems;
+ for (const std::pair<const Node, unsigned>& i : ap.getIteSkolemMap())
+ {
+ Assert(i.second >= ap.getRealAssertionsEnd() && i.second < ap.size());
+ ppSkolems.push_back(i.first);
+ ppLemmas.push_back(ap[i.second]);
+ }
+ d_decisionEngine->addAssertions(ap.ref(), ppLemmas, ppSkolems);
+}
+
void PropEngine::assertFormula(TNode node) {
Assert(!d_inCheckSat) << "Sat solver in solve()!";
Debug("prop") << "assertFormula(" << node << ")" << endl;
@@ -130,18 +152,42 @@ void PropEngine::assertFormula(TNode node) {
d_cnfStream->convertAndAssert(node, false, false, true);
}
-void PropEngine::assertLemma(TNode node, bool negated, bool removable)
+void PropEngine::assertLemma(theory::TrustNode trn, bool removable)
{
+ Node node = trn.getNode();
+ bool negated = trn.getKind() == theory::TrustNodeKind::CONFLICT;
Debug("prop::lemmas") << "assertLemma(" << node << ")" << endl;
// Assert as (possibly) removable
d_cnfStream->convertAndAssert(node, removable, negated);
}
-void PropEngine::addAssertionsToDecisionEngine(
- const preprocessing::AssertionPipeline& assertions)
+void PropEngine::assertLemmas(theory::TrustNode lem,
+ std::vector<theory::TrustNode>& ppLemmas,
+ std::vector<Node>& ppSkolems,
+ bool removable)
{
- d_decisionEngine->addAssertions(assertions);
+ Assert(ppSkolems.size() == ppLemmas.size());
+ // assert the lemmas
+ assertLemma(lem, removable);
+ for (size_t i = 0, lsize = ppLemmas.size(); i < lsize; ++i)
+ {
+ assertLemma(ppLemmas[i], removable);
+ }
+
+ // assert to decision engine
+ if (!removable)
+ {
+ // also add to the decision engine, where notice we don't need proofs
+ std::vector<Node> assertions;
+ assertions.push_back(lem.getProven());
+ std::vector<Node> ppLemmasF;
+ for (const theory::TrustNode& tnl : ppLemmas)
+ {
+ ppLemmasF.push_back(tnl.getProven());
+ }
+ d_decisionEngine->addAssertions(assertions, ppLemmasF, ppSkolems);
+ }
}
void PropEngine::requirePhase(TNode n, bool phase) {
diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h
index e4d536c29..061324947 100644
--- a/src/prop/prop_engine.h
+++ b/src/prop/prop_engine.h
@@ -88,6 +88,13 @@ class PropEngine
void shutdown() {}
/**
+ * Notify preprocessed assertions. This method is called just before the
+ * assertions are asserted to this prop engine. This method notifies the
+ * decision engine and the theory engine of the assertions in ap.
+ */
+ void notifyPreprocessedAssertions(const preprocessing::AssertionPipeline& ap);
+
+ /**
* Converts the given formula to CNF and assert the CNF to the SAT solver.
* The formula is asserted permanently for the current context.
* @param node the formula to assert
@@ -99,19 +106,28 @@ class PropEngine
* The formula can be removed by the SAT solver after backtracking lower
* than the (SAT and SMT) level at which it was asserted.
*
- * @param node the formula to assert
- * @param negated whether the node should be considered to be negated
- * at the top level (or not)
+ * @param trn the trust node storing the formula to assert
* @param removable whether this lemma can be quietly removed based
- * on an activity heuristic (or not)
+ * on an activity heuristic
*/
- void assertLemma(TNode node, bool negated, bool removable);
+ void assertLemma(theory::TrustNode trn, bool removable);
/**
- * Pass a list of assertions from an AssertionPipeline to the decision engine.
+ * Assert lemma trn with preprocessing lemmas ppLemmas which correspond
+ * to lemmas for skolems in ppSkolems.
+ *
+ * @param trn the trust node storing the formula to assert
+ * @param ppLemmas the lemmas from preprocessing and term formula removal on
+ * the proven node of trn
+ * @param ppSkolem the skolem that each lemma in ppLemma constrains. It should
+ * be the case that ppLemmas.size()==ppSkolems.size().
+ * @param removable whether this lemma can be quietly removed based
+ * on an activity heuristic
*/
- void addAssertionsToDecisionEngine(
- const preprocessing::AssertionPipeline& assertions);
+ void assertLemmas(theory::TrustNode trn,
+ std::vector<theory::TrustNode>& ppLemmas,
+ std::vector<Node>& ppSkolems,
+ bool removable);
/**
* If ever n is decided upon, it must be in the given phase. This
diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp
index 26a2ff3e1..c18dfe8ac 100644
--- a/src/smt/smt_solver.cpp
+++ b/src/smt/smt_solver.cpp
@@ -224,14 +224,11 @@ void SmtSolver::processAssertions(Assertions& as)
// process the assertions with the preprocessor
bool noConflict = d_pp.process(as);
- // notify theory engine new preprocessed assertions
- d_theoryEngine->notifyPreprocessedAssertions(ap.ref());
-
// Push the formula to decision engine
if (noConflict)
{
- Chat() << "pushing to decision engine..." << endl;
- d_propEngine->addAssertionsToDecisionEngine(ap);
+ Chat() << "notifying theory engine and decision engine..." << std::endl;
+ d_propEngine->notifyPreprocessedAssertions(ap);
}
// end: INVARIANT to maintain: no reordering of assertions or
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 84212fa1b..fa8960446 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -31,7 +31,6 @@
#include "options/options.h"
#include "options/quantifiers_options.h"
#include "options/theory_options.h"
-#include "preprocessing/assertion_pipeline.h"
#include "printer/printer.h"
#include "smt/dump.h"
#include "smt/logic_exception.h"
@@ -1495,26 +1494,18 @@ theory::LemmaStatus TheoryEngine::lemma(theory::TrustNode tlemma,
}
}
- // must use an assertion pipeline due to decision engine below
- AssertionPipeline lemmas;
- // make the assertion pipeline
- lemmas.push_back(lemmap);
- lemmas.updateRealAssertionsEnd();
Assert(newSkolems.size() == newLemmas.size());
- for (size_t i = 0, nsize = newLemmas.size(); i < nsize; i++)
- {
- // store skolem mapping here
- IteSkolemMap& imap = lemmas.getIteSkolemMap();
- imap[newSkolems[i]] = lemmas.size();
- lemmas.push_back(newLemmas[i].getNode());
- }
// If specified, we must add this lemma to the set of those that need to be
// justified, where note we pass all auxiliary lemmas in lemmas, since these
// by extension must be justified as well.
if (d_relManager != nullptr && isLemmaPropertyNeedsJustify(p))
{
- d_relManager->notifyPreprocessedAssertions(lemmas.ref());
+ d_relManager->notifyPreprocessedAssertion(tlemma.getProven());
+ for (const theory::TrustNode& tnl : newLemmas)
+ {
+ d_relManager->notifyPreprocessedAssertion(tnl.getProven());
+ }
}
// do final checks on the lemmas we are about to send
@@ -1531,32 +1522,34 @@ theory::LemmaStatus TheoryEngine::lemma(theory::TrustNode tlemma,
}
}
- // now, send the lemmas to the prop engine
- Trace("te-lemma") << "Lemma, output: " << tlemma.getProven() << std::endl;
- d_propEngine->assertLemma(tlemma.getProven(), false, removable);
- for (size_t i = 0, lsize = newLemmas.size(); i < lsize; ++i)
+ if (Trace.isOn("te-lemma"))
{
- Trace("te-lemma") << "Lemma, new lemma: " << newLemmas[i].getProven()
- << std::endl;
- d_propEngine->assertLemma(newLemmas[i].getProven(), false, removable);
+ Trace("te-lemma") << "Lemma, output: " << tlemma.getProven() << std::endl;
+ for (size_t i = 0, lsize = newLemmas.size(); i < lsize; ++i)
+ {
+ Trace("te-lemma") << "Lemma, new lemma: " << newLemmas[i].getProven()
+ << " (skolem is " << newSkolems[i] << ")" << std::endl;
+ }
}
- // assert to decision engine
- if (!removable)
- {
- d_propEngine->addAssertionsToDecisionEngine(lemmas);
- }
+ // now, send the lemmas to the prop engine
+ d_propEngine->assertLemmas(tlemma, newLemmas, newSkolems, removable);
// Mark that we added some lemmas
d_lemmasAdded = true;
// Lemma analysis isn't online yet; this lemma may only live for this
// user level.
- Node retLemma = lemmas[0];
- if (lemmas.size() > 1)
+ Node retLemma = tlemma.getNode();
+ if (!newLemmas.empty())
{
+ std::vector<Node> lemmas{retLemma};
+ for (const theory::TrustNode& tnl : newLemmas)
+ {
+ lemmas.push_back(tnl.getProven());
+ }
// the returned lemma is the conjunction of all additional lemmas.
- retLemma = NodeManager::currentNM()->mkNode(kind::AND, lemmas.ref());
+ retLemma = NodeManager::currentNM()->mkNode(kind::AND, lemmas);
}
return theory::LemmaStatus(retLemma, d_userContext->getLevel());
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback