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).
}
}
-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;
for(unsigned i = 0; i < d_needIteSkolemMap.size(); ++i)
{
- d_needIteSkolemMap[i]->addAssertions(assertions);
+ d_needIteSkolemMap[i]->addAssertions(assertions, ppLemmas, ppSkolems);
}
}
#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"
// 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)
#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"
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 {
}
}
-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
}
// 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
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 */
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;
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) {
*/
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.
* 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
// 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
#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"
}
}
- // 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
}
}
- // 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());
}
(assert (! (or (distinct v4 (= v0 v4 v3 v3 v4)) (not v4) v3) :named IP_146))
(check-sat-assuming (IP_107 IP_133))
(get-unsat-core)
-(exit)
\ No newline at end of file
+(exit)
projects / cvc5.git / commitdiff