This PR changes the front end of prop engine to distinguish input formulas from skolem definitions, which is required by the decision engine. This PR breaks the dependency of PropEngine on the AssertionsPipeline, as now the determining of whether an input formula is a skolem definition is handled externally, in SmtSolver.
With this PR, we should not be required to satisfy skolem definitions that are not relevant based on the techniques already implemented in the decision engine. Currently, we are not distinguishing input formulas from skolem definitions properly, meaning we assert more literals than we need to.
This also simplifies related interfaces within decision engine.
We should test this PR with --decision=justification on SMT-LIB.
DecisionEngine::DecisionEngine(context::Context* sc,
context::UserContext* uc,
ResourceManager* rm)
- : d_enabledITEStrategy(nullptr),
- d_needIteSkolemMap(),
- d_relevancyStrategy(nullptr),
- d_assertions(uc),
- d_cnfStream(nullptr),
+ : d_cnfStream(nullptr),
d_satSolver(nullptr),
d_satContext(sc),
d_userContext(uc),
d_result(sc, SAT_VALUE_UNKNOWN),
d_engineState(0),
- d_resourceManager(rm)
+ d_resourceManager(rm),
+ d_enabledITEStrategy(nullptr)
{
Trace("decision") << "Creating decision engine" << std::endl;
}
{
d_enabledITEStrategy.reset(new decision::JustificationHeuristic(
this, d_userContext, d_satContext));
- d_needIteSkolemMap.push_back(d_enabledITEStrategy.get());
}
}
Assert(d_engineState == 1);
d_engineState = 2;
d_enabledITEStrategy.reset(nullptr);
- d_needIteSkolemMap.clear();
}
SatLiteral DecisionEngine::getNext(bool& stopSearch)
: d_enabledITEStrategy->getNext(stopSearch);
}
-bool DecisionEngine::isRelevant(SatVariable var)
+void DecisionEngine::addAssertion(TNode assertion)
{
- Debug("decision") << "isRelevant(" << var <<")" << std::endl;
- if (d_relevancyStrategy != nullptr)
- {
- //Assert(d_cnfStream->hasNode(var));
- return d_relevancyStrategy->isRelevant( d_cnfStream->getNode(SatLiteral(var)) );
- }
- else
- {
- return true;
- }
-}
-
-SatValue DecisionEngine::getPolarity(SatVariable var)
-{
- Debug("decision") << "getPolarity(" << var <<")" << std::endl;
- if (d_relevancyStrategy != nullptr)
- {
- Assert(isRelevant(var));
- return d_relevancyStrategy->getPolarity( d_cnfStream->getNode(SatLiteral(var)) );
- }
- else
+ // new assertions, reset whatever result we knew
+ d_result = SAT_VALUE_UNKNOWN;
+ if (d_enabledITEStrategy != nullptr)
{
- return SAT_VALUE_UNKNOWN;
+ d_enabledITEStrategy->addAssertion(assertion);
}
}
-void DecisionEngine::addAssertions(const std::vector<Node>& assertions,
- const std::vector<Node>& ppLemmas,
- const std::vector<Node>& ppSkolems)
+void DecisionEngine::addSkolemDefinition(TNode lem, TNode skolem)
{
// new assertions, reset whatever result we knew
d_result = SAT_VALUE_UNKNOWN;
-
- for (const Node& assertion : assertions)
- {
- d_assertions.push_back(assertion);
- }
-
- for(unsigned i = 0; i < d_needIteSkolemMap.size(); ++i)
+ if (d_enabledITEStrategy != nullptr)
{
- d_needIteSkolemMap[i]->addAssertions(assertions, ppLemmas, ppSkolems);
+ d_enabledITEStrategy->addSkolemDefinition(lem, skolem);
}
}
namespace CVC4 {
class DecisionEngine {
- std::unique_ptr<ITEDecisionStrategy> d_enabledITEStrategy;
- vector <ITEDecisionStrategy* > d_needIteSkolemMap;
- RelevancyStrategy* d_relevancyStrategy;
-
- typedef context::CDList<Node> AssertionsList;
- AssertionsList d_assertions;
// PropEngine* d_propEngine;
CnfStream* d_cnfStream;
/** Gets the next decision based on strategies that are enabled */
SatLiteral getNext(bool& stopSearch);
- /** Is a sat variable relevant */
- bool isRelevant(SatVariable var);
-
- /**
- * Try to get tell SAT solver what polarity to try for a
- * decision. Return SAT_VALUE_UNKNOWN if it can't help
- */
- SatValue getPolarity(SatVariable var);
-
/** Is the DecisionEngine in a state where it has solved everything? */
bool isDone() {
Trace("decision") << "DecisionEngine::isDone() returning "
// External World helping us help the Strategies
/**
- * Add a list of assertions, as well as lemmas coming from preprocessing
- * (ppLemmas) and pairwise the skolems they constrain (ppSkolems).
+ * Notify this class that assertion is an (input) assertion, not corresponding
+ * to a skolem definition.
*/
- 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)
-
+ void addAssertion(TNode assertion);
/**
- * Get the assertions. Strategies are notified when these are available.
+ * Notify this class that lem is the skolem definition for skolem, which is
+ * a part of the current assertions.
*/
- AssertionsList& getAssertions() {
- return d_assertions;
- }
+ void addSkolemDefinition(TNode lem, TNode skolem);
+ // Interface for Strategies to use stuff stored in Decision Engine
+ // (which was possibly requested by them on initialization)
// Interface for Strategies to get information about External World
Node getNode(SatLiteral l) {
return d_cnfStream->getNode(l);
}
+
+ private:
+ /** The ITE decision strategy we have allocated */
+ std::unique_ptr<ITEDecisionStrategy> d_enabledITEStrategy;
};/* DecisionEngine class */
}/* CVC4 namespace */
virtual ~DecisionStrategy() { }
virtual prop::SatLiteral getNext(bool&) = 0;
-
- virtual bool needIteSkolemMap() { return false; }
-
- virtual void notifyAssertionsAvailable() { return; }
};/* class DecisionStrategy */
class ITEDecisionStrategy : public DecisionStrategy {
ITEDecisionStrategy(DecisionEngine* de, context::Context *c) :
DecisionStrategy(de, c) {
}
-
- bool needIteSkolemMap() override { return true; }
-
/**
- * Add a list of assertions, as well as lemmas coming from preprocessing
- * (ppLemmas) and pairwise the skolems they constrain (ppSkolems).
+ * Add that assertion is an (input) assertion, not corresponding to a
+ * skolem definition.
+ */
+ virtual void addAssertion(TNode assertion) = 0;
+ /**
+ * Add that lem is the skolem definition for skolem, which is a part of
+ * the current assertions.
*/
- virtual void addAssertions(const std::vector<Node>& assertions,
- const std::vector<Node>& ppLemmas,
- const std::vector<Node>& ppSkolems) = 0;
+ virtual void addSkolemDefinition(TNode lem, TNode skolem) = 0;
};/* class ITEDecisionStrategy */
-class RelevancyStrategy : public ITEDecisionStrategy {
-public:
- RelevancyStrategy(DecisionEngine* de, context::Context *c) :
- ITEDecisionStrategy(de, c) {
- }
-
- virtual bool isRelevant(TNode n) = 0;
- virtual prop::SatValue getPolarity(TNode n) = 0;
-};/* class RelevancyStrategy */
-
}/* CVC4::decision namespace */
}/* CVC4 namespace */
}
}
-void JustificationHeuristic::addAssertions(const std::vector<Node>& assertions,
- const std::vector<Node>& ppLemmas,
- const std::vector<Node>& ppSkolems)
+void JustificationHeuristic::addAssertion(TNode assertion)
{
- Assert(ppSkolems.size() == ppLemmas.size());
- Trace("decision")
- << "JustificationHeuristic::addAssertions()"
- << " size = " << assertions.size()
- << std::endl;
-
// Save all assertions locally, including the assertions generated by term
// removal. We have to make sure that we assign a value to all the Boolean
// term variables. To illustrate why this is, consider the case where we have
// assertion to be satisifed. However, we also have to make sure that we pick
// a value for `b` that is not in conflict with the other assignments (we can
// only choose `b` to be `true` otherwise the model is incorrect).
- for (const Node& assertion : assertions)
- {
- d_assertions.push_back(assertion);
- }
-
- // Save mapping between ite skolems and ite assertions
- for (size_t i = 0, nlemmas = ppLemmas.size(); i < nlemmas; i++)
- {
- Trace("decision::jh::ite") << " jh-ite: " << ppSkolems[i] << " maps to "
- << ppLemmas[i] << std::endl;
- d_skolemAssertions[ppSkolems[i]] = ppLemmas[i];
- }
+ d_assertions.push_back(assertion);
+}
- // Automatic weight computation
+void JustificationHeuristic::addSkolemDefinition(TNode lem, TNode skolem)
+{
+ Trace("decision::jh::ite")
+ << " jh-ite: " << skolem << " maps to " << lem << std::endl;
+ d_skolemAssertions[skolem] = lem;
}
SatLiteral JustificationHeuristic::findSplitter(TNode node,
prop::SatLiteral getNext(bool &stopSearch) override;
- void addAssertions(const std::vector<Node>& assertions,
- const std::vector<Node>& ppLemmas,
- const std::vector<Node>& ppSkolems) override;
+ /**
+ * Notify this class that assertion is an (input) assertion, not corresponding
+ * to a skolem definition.
+ */
+ void addAssertion(TNode assertion) override;
+ /**
+ * Notify this class that lem is the skolem definition for skolem, which is
+ * a part of the current assertions.
+ */
+ void addSkolemDefinition(TNode lem, TNode skolem) override;
private:
/* getNext with an option to specify threshold */
namespace CVC4 {
namespace preprocessing {
+using IteSkolemMap = std::unordered_map<size_t, Node>;
+
/**
* Assertion Pipeline stores a list of assertions modified by preprocessing
* passes. It is assumed that all assertions after d_realAssertionsEnd were
Assert(newSkolems.size() == newAsserts.size());
for (unsigned j = 0, nnasserts = newAsserts.size(); j < nnasserts; j++)
{
- imap[newSkolems[j]] = assertions->size();
+ imap[assertions->size()] = newSkolems[j];
assertions->pushBackTrusted(newAsserts[j]);
// new assertions have a dependence on the node (old pf architecture)
if (options::unsatCores() && !options::proofNew())
Assert(newSkolems.size() == newAsserts.size());
for (unsigned j = 0, nnasserts = newAsserts.size(); j < nnasserts; j++)
{
- imap[newSkolems[j]] = assertions->size();
+ imap[assertions->size()] = newSkolems[j];
assertions->pushBackTrusted(newAsserts[j]);
// new assertions have a dependence on the node (old pf architecture)
if (options::unsatCores())
}
void PropEngine::notifyPreprocessedAssertions(
- const preprocessing::AssertionPipeline& ap)
+ const std::vector<Node>& assertions)
{
// 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);
+ d_theoryEngine->notifyPreprocessedAssertions(assertions);
}
void PropEngine::assertFormula(TNode node) {
Assert(!d_inCheckSat) << "Sat solver in solve()!";
Debug("prop") << "assertFormula(" << node << ")" << endl;
- if (isProofEnabled())
- {
- d_pfCnfStream->convertAndAssert(node, false, false, nullptr);
- // register in proof manager
- d_ppm->registerAssertion(node);
- }
- else
- {
- d_cnfStream->convertAndAssert(node, false, false, true);
- }
+ d_decisionEngine->addAssertion(node);
+ assertInternal(node, false, false, true);
+}
+
+void PropEngine::assertSkolemDefinition(TNode node, TNode skolem)
+{
+ Assert(!d_inCheckSat) << "Sat solver in solve()!";
+ Debug("prop") << "assertFormula(" << node << ")" << endl;
+ d_decisionEngine->addSkolemDefinition(node, skolem);
+ assertInternal(node, false, false, true);
}
void PropEngine::assertLemma(theory::TrustNode tlemma, theory::LemmaProperty p)
}
// now, assert the lemmas
- assertLemmaInternal(tplemma, removable);
- for (size_t i = 0, lsize = ppLemmas.size(); i < lsize; ++i)
- {
- assertLemmaInternal(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(tplemma.getProven());
- std::vector<Node> ppLemmasF;
- for (const theory::TrustNode& tnl : ppLemmas)
- {
- ppLemmasF.push_back(tnl.getProven());
- }
- d_decisionEngine->addAssertions(assertions, ppLemmasF, ppSkolems);
- }
+ assertLemmasInternal(tplemma, ppLemmas, ppSkolems, removable);
}
-void PropEngine::assertLemmaInternal(theory::TrustNode trn, bool removable)
+void PropEngine::assertTrustedLemmaInternal(theory::TrustNode trn,
+ bool removable)
{
Node node = trn.getNode();
- bool negated = trn.getKind() == theory::TrustNodeKind::CONFLICT;
Debug("prop::lemmas") << "assertLemma(" << node << ")" << endl;
+ bool negated = trn.getKind() == theory::TrustNodeKind::CONFLICT;
+ Assert(!isProofEnabled() || trn.getGenerator() != nullptr);
+ assertInternal(trn.getNode(), negated, removable, false, trn.getGenerator());
+}
+
+void PropEngine::assertInternal(
+ TNode node, bool negated, bool removable, bool input, ProofGenerator* pg)
+{
// Assert as (possibly) removable
if (isProofEnabled())
{
- Assert(trn.getGenerator());
- d_pfCnfStream->convertAndAssert(
- node, negated, removable, trn.getGenerator());
+ d_pfCnfStream->convertAndAssert(node, negated, removable, pg);
+ // if input, register the assertion
+ if (input)
+ {
+ d_ppm->registerAssertion(node);
+ }
}
else
{
- d_cnfStream->convertAndAssert(node, removable, negated);
+ d_cnfStream->convertAndAssert(node, removable, negated, input);
+ }
+}
+void PropEngine::assertLemmasInternal(
+ theory::TrustNode trn,
+ const std::vector<theory::TrustNode>& ppLemmas,
+ const std::vector<Node>& ppSkolems,
+ bool removable)
+{
+ if (!trn.isNull())
+ {
+ assertTrustedLemmaInternal(trn, removable);
+ }
+ for (const theory::TrustNode& tnl : ppLemmas)
+ {
+ assertTrustedLemmaInternal(tnl, removable);
+ }
+ // assert to decision engine
+ if (!removable)
+ {
+ // also add to the decision engine, where notice we don't need proofs
+ if (!trn.isNull())
+ {
+ // notify the theory proxy of the lemma
+ d_decisionEngine->addAssertion(trn.getProven());
+ }
+ Assert(ppSkolems.size() == ppLemmas.size());
+ for (size_t i = 0, lsize = ppLemmas.size(); i < lsize; ++i)
+ {
+ Node lem = ppLemmas[i].getProven();
+ d_decisionEngine->addSkolemDefinition(lem, ppSkolems[i]);
+ }
}
}
std::vector<Node> newSkolems;
theory::TrustNode tpn = d_theoryProxy->preprocess(n, newLemmas, newSkolems);
// send lemmas corresponding to the skolems introduced by preprocessing n
- for (const theory::TrustNode& tnl : newLemmas)
- {
- assertLemma(tnl, theory::LemmaProperty::NONE);
- }
+ theory::TrustNode trnNull;
+ assertLemmasInternal(trnNull, newLemmas, newSkolems, false);
return tpn.isNull() ? Node(n) : tpn.getNode();
}
#include "base/modal_exception.h"
#include "expr/node.h"
#include "options/options.h"
-#include "preprocessing/assertion_pipeline.h"
#include "proof/proof_manager.h"
#include "prop/minisat/core/Solver.h"
#include "prop/minisat/minisat.h"
/**
* 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.
+ * theory engine of the given assertions. Notice this vector includes
+ * both the input formulas and the skolem definitions.
*/
- void notifyPreprocessedAssertions(const preprocessing::AssertionPipeline& ap);
+ void notifyPreprocessedAssertions(const std::vector<Node>& assertions);
/**
* 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 is asserted permanently for the current context. Note the
+ * formula should correspond to an input formula and not a lemma introduced
+ * by term formula removal (which instead should use the interface below).
* @param node the formula to assert
*/
void assertFormula(TNode node);
+ /**
+ * Same as above, but node corresponds to the skolem definition of the given
+ * skolem.
+ * @param node the formula to assert
+ * @param skolem the skolem that this lemma defines.
+ *
+ * For example, if k is introduced by ITE removal of (ite C x y), then node
+ * is the formula (ite C (= k x) (= k y)). It is important to distinguish
+ * these kinds of lemmas from input assertions, as the justification decision
+ * heuristic treates them specially.
+ */
+ void assertSkolemDefinition(TNode node, TNode skolem);
/**
* Converts the given formula to CNF and assert the CNF to the SAT solver.
* @param removable whether this lemma can be quietly removed based
* on an activity heuristic
*/
- void assertLemmaInternal(theory::TrustNode trn, bool removable);
+ void assertTrustedLemmaInternal(theory::TrustNode trn, bool removable);
+ /**
+ * Assert node as a formula to the CNF stream
+ * @param node The formula to assert
+ * @param negated Whether to assert the negation of node
+ * @param removable Whether the formula is removable
+ * @param input Whether the formula came from the input
+ * @param pg Pointer to a proof generator that can provide a proof of node
+ * (or its negation if negated is true).
+ */
+ void assertInternal(TNode node,
+ bool negated,
+ bool removable,
+ bool input,
+ ProofGenerator* pg = nullptr);
+ /**
+ * Assert lemmas internal, where trn is a trust node corresponding to a
+ * formula to assert to the CNF stream, ppLemmas and ppSkolems are the
+ * skolem definitions and skolems obtained from preprocessing it, and
+ * removable is whether the lemma is removable.
+ */
+ void assertLemmasInternal(theory::TrustNode trn,
+ const std::vector<theory::TrustNode>& ppLemmas,
+ const std::vector<Node>& ppSkolems,
+ bool removable);
/**
* Indicates that the SAT solver is currently solving something and we should
d_theoryEngine->spendResource(r);
}
-bool TheoryProxy::isDecisionRelevant(SatVariable var) {
- return d_decisionEngine->isRelevant(var);
-}
+bool TheoryProxy::isDecisionRelevant(SatVariable var) { return true; }
bool TheoryProxy::isDecisionEngineDone() {
return d_decisionEngine->isDone();
}
SatValue TheoryProxy::getDecisionPolarity(SatVariable var) {
- return d_decisionEngine->getPolarity(var);
+ return SAT_VALUE_UNKNOWN;
}
CnfStream* TheoryProxy::getCnfStream() { return d_cnfStream; }
// process the assertions with the preprocessor
bool noConflict = d_pp.process(as);
- // Push the formula to decision engine
+ // Notify the input formulas to theory engine
if (noConflict)
{
- Chat() << "notifying theory engine and decision engine..." << std::endl;
- d_propEngine->notifyPreprocessedAssertions(ap);
+ Chat() << "notifying theory engine..." << std::endl;
+ d_propEngine->notifyPreprocessedAssertions(ap.ref());
}
// end: INVARIANT to maintain: no reordering of assertions or
{
Chat() << "converting to CNF..." << endl;
TimerStat::CodeTimer codeTimer(d_stats.d_cnfConversionTime);
- for (const Node& assertion : ap.ref())
+ const std::vector<Node>& assertions = ap.ref();
+ // It is important to distinguish the input assertions from the skolem
+ // definitions, as the decision justification heuristic treates the latter
+ // specially.
+ preprocessing::IteSkolemMap& ism = ap.getIteSkolemMap();
+ preprocessing::IteSkolemMap::iterator it;
+ for (size_t i = 0, asize = assertions.size(); i < asize; i++)
{
- Chat() << "+ " << assertion << std::endl;
- d_propEngine->assertFormula(assertion);
+ // is the assertion a skolem definition?
+ it = ism.find(i);
+ if (it == ism.end())
+ {
+ Chat() << "+ input " << assertions[i] << std::endl;
+ d_propEngine->assertFormula(assertions[i]);
+ }
+ else
+ {
+ Chat() << "+ skolem definition " << assertions[i] << " (from "
+ << it->second << ")" << std::endl;
+ d_propEngine->assertSkolemDefinition(assertions[i], it->second);
+ }
}
}
namespace CVC4 {
-typedef std::unordered_map<Node, unsigned, NodeHashFunction> IteSkolemMap;
-
class RemoveTermFormulas {
public:
RemoveTermFormulas(context::UserContext* u, ProofNodeManager* pnm = nullptr);
projects / cvc5.git / commitdiff