These changes are taken from the SAT relevancy branch. This does not change the behavior of the current code, it breaks the dependency of decision engine on the skolem definition manager and makes the latter solely managed by TheoryProxy.
This is in preparation for virtual clause deletion.
*/
virtual void addSkolemDefinition(TNode lem, TNode skolem) = 0;
/**
- * Notify this class that the literal n has been asserted, possibly
- * propagated by the SAT solver.
+ * Notify this class that the list of lemmas defs are now active in the
+ * current SAT context.
*/
- virtual void notifyAsserted(TNode n) {}
+ virtual void notifyActiveSkolemDefs(std::vector<TNode>& defs) {}
+ /**
+ * Track active skolem defs, whether we need to call the above method
+ * when appropriate.
+ */
+ virtual bool needsActiveSkolemDefs() const { return false; }
protected:
/** Get next internal, the engine-specific implementation of getNext */
namespace cvc5 {
namespace decision {
-JustificationStrategy::JustificationStrategy(Env& env,
- prop::SkolemDefManager* skdm)
+JustificationStrategy::JustificationStrategy(Env& env)
: DecisionEngine(env),
- d_skdm(skdm),
d_assertions(
userContext(),
context(),
insertToAssertionList(toProcess, false);
}
}
+bool JustificationStrategy::needsActiveSkolemDefs() const
+{
+ return d_jhSkRlvMode == options::JutificationSkolemRlvMode::ASSERT;
+}
-void JustificationStrategy::notifyAsserted(TNode n)
+void JustificationStrategy::notifyActiveSkolemDefs(std::vector<TNode>& defs)
{
- if (d_jhSkRlvMode == options::JutificationSkolemRlvMode::ASSERT)
- {
- // assertion processed makes all skolems in assertion active,
- // which triggers their definitions to becoming relevant
- std::vector<TNode> defs;
- d_skdm->notifyAsserted(n, defs, true);
- insertToAssertionList(defs, true);
- }
- // NOTE: can update tracking triggers, pop stack to where a child implied
- // that a node on the current stack is justified.
+ Assert(d_jhSkRlvMode == options::JutificationSkolemRlvMode::ASSERT);
+ // assertion processed makes all skolems in assertion active,
+ // which triggers their definitions to becoming relevant
+ insertToAssertionList(defs, true);
+ // NOTE: if we had a notifyAsserted callback, we could update tracking
+ // triggers, pop stack to where a child implied that a node on the current
+ // stack is justified.
}
void JustificationStrategy::insertToAssertionList(std::vector<TNode>& toProcess,
#include "prop/sat_solver_types.h"
namespace cvc5 {
-
-namespace prop {
-class SkolemDefManager;
-}
-
namespace decision {
/**
{
public:
/** Constructor */
- JustificationStrategy(Env& env, prop::SkolemDefManager* skdm);
+ JustificationStrategy(Env& env);
/** Presolve, called at the beginning of each check-sat call */
void presolve() override;
*/
void addSkolemDefinition(TNode lem, TNode skolem) override;
/**
- * Notify this class that literal n has been asserted. This is triggered when
- * n is sent to TheoryEngine. This activates skolem definitions for skolems
- * k that occur in n.
+ * Notify this class that the list of lemmas defs are now active in the
+ * current SAT context. This is triggered when a literal lit is sent to
+ * TheoryEngine that contains skolems we have yet to see in the current SAT
+ * context, where defs are the skolem definitions for each such skolem.
+ */
+ void notifyActiveSkolemDefs(std::vector<TNode>& defs) override;
+ /**
+ * We need notification of active skolem definitions when our skolem
+ * relevance policy is JutificationSkolemRlvMode::ASSERT.
*/
- void notifyAsserted(TNode n) override;
+ bool needsActiveSkolemDefs() const override;
private:
/**
static bool isTheoryLiteral(TNode n);
/** Is n a theory atom? */
static bool isTheoryAtom(TNode n);
- /** Pointer to the skolem definition manager */
- prop::SkolemDefManager* d_skdm;
/** The assertions, which are user-context dependent. */
AssertionList d_assertions;
/** The skolem assertions */
if (dmode == options::DecisionMode::JUSTIFICATION
|| dmode == options::DecisionMode::STOPONLY)
{
- d_decisionEngine.reset(
- new decision::JustificationStrategy(env, d_skdm.get()));
+ d_decisionEngine.reset(new decision::JustificationStrategy(env));
}
else if (dmode == options::DecisionMode::JUSTIFICATION_OLD
|| dmode == options::DecisionMode::STOPONLY_OLD)
Assert(ppSkolems.size() == ppLemmas.size());
for (size_t i = 0, lsize = ppLemmas.size(); i < lsize; ++i)
{
- Node lem = ppLemmas[i].getProven();
d_theoryProxy->notifyAssertion(ppLemmas[i].getProven(), ppSkolems[i]);
}
}
ScopedBool scopedBool(d_inCheckSat);
d_inCheckSat = true;
- // TODO This currently ignores conflicts (a dangerous practice).
- d_decisionEngine->presolve();
- d_theoryEngine->presolve();
+ // Note this currently ignores conflicts (a dangerous practice).
+ d_theoryProxy->presolve();
if(options::preprocessOnly()) {
return Result(Result::SAT_UNKNOWN, Result::REQUIRES_FULL_CHECK);
: d_propEngine(propEngine),
d_cnfStream(nullptr),
d_decisionEngine(decisionEngine),
+ d_dmNeedsActiveDefs(d_decisionEngine->needsActiveSkolemDefs()),
d_theoryEngine(theoryEngine),
d_queue(env.getContext()),
d_tpp(env, *theoryEngine),
void TheoryProxy::finishInit(CnfStream* cnfStream) { d_cnfStream = cnfStream; }
+void TheoryProxy::presolve()
+{
+ d_decisionEngine->presolve();
+ d_theoryEngine->presolve();
+}
+
void TheoryProxy::notifyAssertion(Node a, TNode skolem)
{
if (skolem.isNull())
while (!d_queue.empty()) {
TNode assertion = d_queue.front();
d_queue.pop();
+ // now, assert to theory engine
d_theoryEngine->assertFact(assertion);
- d_decisionEngine->notifyAsserted(assertion);
+ if (d_dmNeedsActiveDefs)
+ {
+ Assert(d_skdm != nullptr);
+ Trace("sat-rlv-assert")
+ << "Assert to theory engine: " << assertion << std::endl;
+ // Assertion makes all skolems in assertion active,
+ // which triggers their definitions to becoming active.
+ std::vector<TNode> activeSkolemDefs;
+ d_skdm->notifyAsserted(assertion, activeSkolemDefs, true);
+ // notify the decision engine of the skolem definitions that have become
+ // active due to the assertion.
+ d_decisionEngine->notifyActiveSkolemDefs(activeSkolemDefs);
+ }
}
d_theoryEngine->check(effort);
}
/** Finish initialize */
void finishInit(CnfStream* cnfStream);
+ /** Presolve, which calls presolve for the modules managed by this class */
+ void presolve();
+
/** Notify a lemma, possibly corresponding to a skolem definition */
void notifyAssertion(Node lem, TNode skolem = TNode::null());
/** The decision engine we are using. */
decision::DecisionEngine* d_decisionEngine;
+ /**
+ * Whether the decision engine needs notification of active skolem
+ * definitions, see DecisionEngine::needsActiveSkolemDefs.
+ */
+ bool d_dmNeedsActiveDefs;
+
/** The theory engine we are using. */
TheoryEngine* d_theoryEngine;
projects / cvc5.git / commitdiff