Apart from { quantifiers, bool, builtin }, each Theory now has an official equality engine. This PR elaborates on the standard recommended template that Theory should follow, which applies to all theories, regardless of whether they have an equality engine.
This includes:
A standard check method. The Theory is now expected to implement 4 callbacks (preCheck, postCheck, preNotifyFact, notifyFact).
A standard collectModelInfo method. The Theory is now expected to implement 2 callbacks (computeRelevantTerms, collectModelValues).
Additionally, 2 more methods have an obvious default:
(1) getEqualityStatus, which returns information based on an equality engine if it exists,
(2) addSharedTerm, which adds the term as a trigger term to the equality engine of the theory if it exists. Notice that for the sake of more consistent naming, theories now implement notifySharedTerm (previously TheoryEngine called theory-independent addSharedTermInternal which called addSharedTerm, this is updated now to addSharedTerm/notifySharedTerm).
Other methods will not be standardized yet e.g. preRegisterTerm, since they vary per theory.
FYI @barrettcw
Each theory on the branch https://github.com/ajreynol/CVC4/tree/centralEe conforms to this template (e.g. they do not override check or collectModelInfo). The next step will be to pull the new implementation of each Theory from that branch.
return d_internal->expandDefinition(node);
}
-void TheoryArith::addSharedTerm(TNode n){
- d_internal->addSharedTerm(n);
-}
+void TheoryArith::notifySharedTerm(TNode n) { d_internal->addSharedTerm(n); }
TrustNode TheoryArith::ppRewrite(TNode atom)
{
EqualityStatus getEqualityStatus(TNode a, TNode b) override;
- void addSharedTerm(TNode n) override;
+ void notifySharedTerm(TNode n) override;
Node getModelValue(TNode var) override;
// SHARING
/////////////////////////////////////////////////////////////////////////////
-
-void TheoryArrays::addSharedTerm(TNode t) {
- Debug("arrays::sharing") << spaces(getSatContext()->getLevel()) << "TheoryArrays::addSharedTerm(" << t << ")" << std::endl;
+void TheoryArrays::notifySharedTerm(TNode t)
+{
+ Debug("arrays::sharing") << spaces(getSatContext()->getLevel())
+ << "TheoryArrays::notifySharedTerm(" << t << ")"
+ << std::endl;
d_equalityEngine->addTriggerTerm(t, THEORY_ARRAYS);
if (t.getType().isArray()) {
d_sharedArrays.insert(t);
void checkPair(TNode r1, TNode r2);
public:
- void addSharedTerm(TNode t) override;
+ void notifySharedTerm(TNode t) override;
EqualityStatus getEqualityStatus(TNode a, TNode b) override;
void computeCareGraph() override;
bool isShared(TNode t)
return TrustNode::mkTrustPropExp(node, explanation, nullptr);
}
-
-void TheoryBV::addSharedTerm(TNode t) {
- Debug("bitvector::sharing") << indent() << "TheoryBV::addSharedTerm(" << t << ")" << std::endl;
+void TheoryBV::notifySharedTerm(TNode t)
+{
+ Debug("bitvector::sharing")
+ << indent() << "TheoryBV::notifySharedTerm(" << t << ")" << std::endl;
d_sharedTermsSet.insert(t);
if (options::bitvectorEqualitySolver()) {
for (unsigned i = 0; i < d_subtheories.size(); ++i) {
*/
void explain(TNode literal, std::vector<TNode>& assumptions);
- void addSharedTerm(TNode t) override;
+ void notifySharedTerm(TNode t) override;
bool isSharedTerm(TNode t) { return d_sharedTermsSet.contains(t); }
return TrustNode::null();
}
-void TheoryDatatypes::addSharedTerm(TNode t) {
- Debug("datatypes") << "TheoryDatatypes::addSharedTerm(): "
- << t << " " << t.getType().isBoolean() << endl;
+void TheoryDatatypes::notifySharedTerm(TNode t)
+{
+ Debug("datatypes") << "TheoryDatatypes::notifySharedTerm(): " << t << " "
+ << t.getType().isBoolean() << endl;
d_equalityEngine->addTriggerTerm(t, THEORY_DATATYPES);
- Debug("datatypes") << "TheoryDatatypes::addSharedTerm() finished" << std::endl;
+ Debug("datatypes") << "TheoryDatatypes::notifySharedTerm() finished"
+ << std::endl;
}
bool TheoryDatatypes::propagateLit(TNode literal)
void preRegisterTerm(TNode n) override;
TrustNode expandDefinition(Node n) override;
TrustNode ppRewrite(TNode n) override;
- void addSharedTerm(TNode t) override;
+ void notifySharedTerm(TNode t) override;
EqualityStatus getEqualityStatus(TNode a, TNode b) override;
bool collectModelInfo(TheoryModel* m) override;
void shutdown() override {}
return;
}
-void TheoryFp::addSharedTerm(TNode node) {
+void TheoryFp::notifySharedTerm(TNode node)
+{
Trace("fp-addSharedTerm")
- << "TheoryFp::addSharedTerm(): " << node << std::endl;
+ << "TheoryFp::notifySharedTerm(): " << node << std::endl;
// A system-wide invariant; terms must be registered before they are shared
Assert(isRegistered(node));
return;
}
// Resolve the abstractions for the conversion lemmas
- // if (level == EFFORT_COMBINATION) {
if (level == EFFORT_LAST_CALL)
{
Trace("fp") << "TheoryFp::check(): checking abstractions" << std::endl;
TrustNode expandDefinition(Node node) override;
void preRegisterTerm(TNode node) override;
- void addSharedTerm(TNode node) override;
+ void notifySharedTerm(TNode node) override;
TrustNode ppRewrite(TNode node) override;
// SHARING
/////////////////////////////////////////////////////////////////////////////
-
-void TheorySep::addSharedTerm(TNode t) {
- Debug("sep") << "TheorySep::addSharedTerm(" << t << ")" << std::endl;
+void TheorySep::notifySharedTerm(TNode t)
+{
+ Debug("sep") << "TheorySep::notifySharedTerm(" << t << ")" << std::endl;
d_equalityEngine->addTriggerTerm(t, THEORY_SEP);
}
TrustNode explain(TNode n) override;
public:
- void addSharedTerm(TNode t) override;
+ void notifySharedTerm(TNode t) override;
EqualityStatus getEqualityStatus(TNode a, TNode b) override;
void computeCareGraph() override;
d_internal->finishInit();
}
-void TheorySets::addSharedTerm(TNode n) {
- d_internal->addSharedTerm(n);
-}
+void TheorySets::notifySharedTerm(TNode n) { d_internal->addSharedTerm(n); }
void TheorySets::check(Effort e) {
if (done() && e < Theory::EFFORT_FULL) {
void finishInit() override;
//--------------------------------- end initialization
- void addSharedTerm(TNode) override;
+ void notifySharedTerm(TNode) override;
void check(Effort) override;
bool collectModelInfo(TheoryModel* m) override;
void computeCareGraph() override;
return false;
}
-void TheoryStrings::addSharedTerm(TNode t) {
- Debug("strings") << "TheoryStrings::addSharedTerm(): "
- << t << " " << t.getType().isBoolean() << endl;
+void TheoryStrings::notifySharedTerm(TNode t)
+{
+ Debug("strings") << "TheoryStrings::notifySharedTerm(): " << t << " "
+ << t.getType().isBoolean() << endl;
d_equalityEngine->addTriggerTerm(t, THEORY_STRINGS);
if (options::stringExp())
{
d_esolver.addSharedTerm(t);
}
- Debug("strings") << "TheoryStrings::addSharedTerm() finished" << std::endl;
+ Debug("strings") << "TheoryStrings::notifySharedTerm() finished" << std::endl;
}
EqualityStatus TheoryStrings::getEqualityStatus(TNode a, TNode b) {
/** shutdown */
void shutdown() override {}
/** add shared term */
- void addSharedTerm(TNode n) override;
+ void notifySharedTerm(TNode n) override;
/** get equality status */
EqualityStatus getEqualityStatus(TNode a, TNode b) override;
/** preregister term */
os << "EFFORT_STANDARD"; break;
case Theory::EFFORT_FULL:
os << "EFFORT_FULL"; break;
- case Theory::EFFORT_COMBINATION:
- os << "EFFORT_COMBINATION"; break;
case Theory::EFFORT_LAST_CALL:
os << "EFFORT_LAST_CALL"; break;
default:
d_theoryState->setEqualityEngine(ee);
}
}
+
void Theory::setQuantifiersEngine(QuantifiersEngine* qe)
{
Assert(d_quantEngine == nullptr);
+ // quantifiers engine may be null if not in quantified logic
d_quantEngine = qe;
}
return tid;
}
-void Theory::addSharedTermInternal(TNode n) {
- Debug("sharing") << "Theory::addSharedTerm<" << getId() << ">(" << n << ")" << endl;
- Debug("theory::assertions") << "Theory::addSharedTerm<" << getId() << ">(" << n << ")" << endl;
- d_sharedTerms.push_back(n);
- addSharedTerm(n);
+void Theory::notifySharedTerm(TNode n)
+{
+ // TODO (project #39): this will move to addSharedTerm, as every theory with
+ // an equality does this in their notifySharedTerm method.
+ // if we have an equality engine, add the trigger term
+ if (d_equalityEngine != nullptr)
+ {
+ d_equalityEngine->addTriggerTerm(n, d_id);
+ }
}
void Theory::computeCareGraph() {
// Collect all terms appearing in assertions
irrKinds.insert(kind::EQUAL);
irrKinds.insert(kind::NOT);
- context::CDList<Assertion>::const_iterator assert_it = facts_begin(), assert_it_end = facts_end();
- for (; assert_it != assert_it_end; ++assert_it) {
+ context::CDList<Assertion>::const_iterator assert_it = facts_begin(),
+ assert_it_end = facts_end();
+ for (; assert_it != assert_it_end; ++assert_it)
+ {
collectTerms(*assert_it, irrKinds, termSet);
}
- if (!includeShared) return;
-
+ if (!includeShared)
+ {
+ return;
+ }
// Add terms that are shared terms
- set<Kind> kempty;
- context::CDList<TNode>::const_iterator shared_it = shared_terms_begin(), shared_it_end = shared_terms_end();
- for (; shared_it != shared_it_end; ++shared_it) {
+ std::set<Kind> kempty;
+ context::CDList<TNode>::const_iterator shared_it = shared_terms_begin(),
+ shared_it_end = shared_terms_end();
+ for (; shared_it != shared_it_end; ++shared_it)
+ {
collectTerms(*shared_it, kempty, termSet);
}
}
d_careGraph = NULL;
}
+EqualityStatus Theory::getEqualityStatus(TNode a, TNode b)
+{
+ // if not using an equality engine, then by default we don't know the status
+ if (d_equalityEngine == nullptr)
+ {
+ return EQUALITY_UNKNOWN;
+ }
+ Assert(d_equalityEngine->hasTerm(a) && d_equalityEngine->hasTerm(b));
+
+ // Check for equality (simplest)
+ if (d_equalityEngine->areEqual(a, b))
+ {
+ // The terms are implied to be equal
+ return EQUALITY_TRUE;
+ }
+
+ // Check for disequality
+ if (d_equalityEngine->areDisequal(a, b, false))
+ {
+ // The terms are implied to be dis-equal
+ return EQUALITY_FALSE;
+ }
+
+ // All other terms are unknown, which is conservative. A theory may override
+ // this method if it knows more information.
+ return EQUALITY_UNKNOWN;
+}
+
+void Theory::check(Effort level)
+{
+ // see if we are already done (as an optimization)
+ if (done() && level < EFFORT_FULL)
+ {
+ return;
+ }
+ Assert(d_theoryState!=nullptr);
+ // standard calls for resource, stats
+ d_out->spendResource(ResourceManager::Resource::TheoryCheckStep);
+ TimerStat::CodeTimer checkTimer(d_checkTime);
+ // pre-check at level
+ if (preCheck(level))
+ {
+ // check aborted for a theory-specific reason
+ return;
+ }
+ // process the pending fact queue
+ while (!done() && !d_theoryState->isInConflict())
+ {
+ // Get the next assertion from the fact queue
+ Assertion assertion = get();
+ TNode fact = assertion.d_assertion;
+ bool polarity = fact.getKind() != kind::NOT;
+ TNode atom = polarity ? fact : fact[0];
+ // call the pre-notify method
+ if (preNotifyFact(atom, polarity, fact, assertion.d_isPreregistered))
+ {
+ // handled in theory-specific way that doesn't involve equality engine
+ continue;
+ }
+ // Theories that don't have an equality engine should always return true
+ // for preNotifyFact
+ Assert(d_equalityEngine != nullptr);
+ // assert to the equality engine
+ if (atom.getKind() == kind::EQUAL)
+ {
+ d_equalityEngine->assertEquality(atom, polarity, fact);
+ }
+ else
+ {
+ d_equalityEngine->assertPredicate(atom, polarity, fact);
+ }
+ // notify the theory of the new fact, which is not internal
+ notifyFact(atom, polarity, fact, false);
+ }
+ // post-check at level
+ postCheck(level);
+}
+
+bool Theory::preCheck(Effort level) { return false; }
+
+void Theory::postCheck(Effort level) {}
+
+bool Theory::preNotifyFact(TNode atom, bool polarity, TNode fact, bool isPrereg)
+{
+ return false;
+}
+
+void Theory::notifyFact(TNode atom, bool polarity, TNode fact, bool isInternal)
+{
+}
+
+void Theory::preRegisterTerm(TNode node) {}
+
+void Theory::addSharedTerm(TNode n)
+{
+ Debug("sharing") << "Theory::addSharedTerm<" << getId() << ">(" << n << ")"
+ << std::endl;
+ Debug("theory::assertions")
+ << "Theory::addSharedTerm<" << getId() << ">(" << n << ")" << std::endl;
+ d_sharedTerms.push_back(n);
+ // now call theory-specific method notifySharedTerm
+ notifySharedTerm(n);
+}
+
eq::EqualityEngine* Theory::getEqualityEngine()
{
// get the assigned equality engine, which is a pointer stored in this class
/** Index into the head of the facts list */
context::CDO<unsigned> d_factsHead;
- /** Add shared term to the theory. */
- void addSharedTermInternal(TNode node);
-
/** Indices for splitting on the shared terms. */
context::CDO<unsigned> d_sharedTermsIndex;
*/
context::CDList<TNode> d_sharedTerms;
- //---------------------------------- collect model info
+ //---------------------------------- private collect model info
/**
* Scans the current set of assertions and shared terms top-down
* until a theory-leaf is reached, and adds all terms found to
void collectTerms(TNode n,
std::set<Kind>& irrKinds,
std::set<Node>& termSet) const;
- /**
- * Same as above, but with empty irrKinds. This version can be overridden
- * by the theory, e.g. by restricting or extending the set of terms returned
- * by computeRelevantTermsInternal, which is called by default with no
- * irrKinds.
- */
- virtual void computeRelevantTerms(std::set<Node>& termSet,
- bool includeShared = true);
- /**
- * Collect model values, after equality information is added to the model.
- * The argument termSet is the set of relevant terms returned by
- * computeRelevantTerms.
- */
- virtual bool collectModelValues(TheoryModel* m, std::set<Node>& termSet);
- //---------------------------------- end collect model info
+ //---------------------------------- end private collect model info
/**
* Construct a Theory.
virtual void finishInit() {}
//--------------------------------- end private initialization
+ /**
+ * This method is called to notify a theory that the node n should
+ * be considered a "shared term" by this theory. This does anything
+ * theory-specific concerning the fact that n is now marked as a shared
+ * term, which is done in addition to explicitly storing n as a shared
+ * term and adding it as a trigger term in the equality engine of this
+ * class (see addSharedTerm).
+ */
+ virtual void notifySharedTerm(TNode n);
+
public:
//--------------------------------- initialization
/**
* Normally we call QUICK_CHECK or STANDARD; at the leaves we call
* with FULL_EFFORT.
*/
- enum Effort {
+ enum Effort
+ {
/**
* Standard effort where theory need not do anything
*/
EFFORT_STANDARD = 50,
/**
- * Full effort requires the theory make sure its assertions are satisfiable or not
+ * Full effort requires the theory make sure its assertions are satisfiable
+ * or not
*/
EFFORT_FULL = 100,
/**
- * Combination effort means that the individual theories are already satisfied, and
- * it is time to put some effort into propagation of shared term equalities
- */
- EFFORT_COMBINATION = 150,
- /**
- * Last call effort, reserved for quantifiers.
+ * Last call effort, called after theory combination has completed with
+ * no lemmas and a model is available.
*/
EFFORT_LAST_CALL = 200
- };/* enum Effort */
+ }; /* enum Effort */
static inline bool standardEffortOrMore(Effort e) CVC4_CONST_FUNCTION
{ return e >= EFFORT_STANDARD; }
{ return e >= EFFORT_STANDARD && e < EFFORT_FULL; }
static inline bool fullEffort(Effort e) CVC4_CONST_FUNCTION
{ return e == EFFORT_FULL; }
- static inline bool combination(Effort e) CVC4_CONST_FUNCTION
- { return e == EFFORT_COMBINATION; }
/**
* Get the id for this Theory.
return d_valuation;
}
+ /** Get the equality engine being used by this theory. */
+ eq::EqualityEngine* getEqualityEngine();
+
/**
* Get the quantifiers engine associated to this theory.
*/
return d_quantEngine;
}
- /**
- * Get the quantifiers engine associated to this theory (const version).
- */
- const QuantifiersEngine* getQuantifiersEngine() const {
- return d_quantEngine;
- }
-
/** Get the decision manager associated to this theory. */
DecisionManager* getDecisionManager() { return d_decManager; }
/**
* Pre-register a term. Done one time for a Node per SAT context level.
*/
- virtual void preRegisterTerm(TNode) { }
+ virtual void preRegisterTerm(TNode);
/**
* Assert a fact in the current context.
d_facts.push_back(Assertion(assertion, isPreregistered));
}
- /**
- * This method is called to notify a theory that the node n should
- * be considered a "shared term" by this theory
- */
- virtual void addSharedTerm(TNode n) { }
-
- /**
- * Get the official equality engine of this theory.
- */
- eq::EqualityEngine* getEqualityEngine();
+ /** Add shared term to the theory. */
+ void addSharedTerm(TNode node);
/**
* Return the current theory care graph. Theories should overload
* Return the status of two terms in the current context. Should be
* implemented in sub-theories to enable more efficient theory-combination.
*/
- virtual EqualityStatus getEqualityStatus(TNode a, TNode b) {
- return EQUALITY_UNKNOWN;
- }
+ virtual EqualityStatus getEqualityStatus(TNode a, TNode b);
/**
* Return the model value of the give shared term (or null if not available).
- */
- virtual Node getModelValue(TNode var) { return Node::null(); }
-
- /**
- * Check the current assignment's consistency.
*
- * An implementation of check() is required to either:
- * - return a conflict on the output channel,
- * - be interrupted,
- * - throw an exception
- * - or call get() until done() is true.
+ * TODO (project #39): this method is likely to become deprecated.
*/
- virtual void check(Effort level = EFFORT_FULL) { }
-
- /** Needs last effort check? */
- virtual bool needsCheckLastEffort() { return false; }
+ virtual Node getModelValue(TNode var) { return Node::null(); }
/** T-propagate new literal assignments in the current context. */
- virtual void propagate(Effort level = EFFORT_FULL) { }
+ virtual void propagate(Effort level = EFFORT_FULL) {}
/**
* Return an explanation for the literal represented by parameter n
"Theory::explain() interface!";
}
+ //--------------------------------- check
+ /**
+ * Does this theory wish to be called to check at last call effort? This is
+ * the case for any theory that wishes to run when a model is available.
+ */
+ virtual bool needsCheckLastEffort() { return false; }
+ /**
+ * Check the current assignment's consistency.
+ *
+ * An implementation of check() is required to either:
+ * - return a conflict on the output channel,
+ * - be interrupted,
+ * - throw an exception
+ * - or call get() until done() is true.
+ *
+ * The standard method for check consists of a loop that processes the entire
+ * fact queue when preCheck returns false. It makes four theory-specific
+ * callbacks, (preCheck, postCheck, preNotifyFact, notifyFact) as described
+ * below. It asserts each fact to the official equality engine when
+ * preNotifyFact returns false.
+ *
+ * Theories that use this check method must use an official theory
+ * state object (d_theoryState).
+ *
+ * TODO (project #39): this method should be non-virtual, once all theories
+ * conform to the new standard
+ */
+ virtual void check(Effort level = EFFORT_FULL);
+ /**
+ * Pre-check, called before the fact queue of the theory is processed.
+ * If this method returns false, then the theory will process its fact
+ * queue. If this method returns true, then the theory has indicated
+ * its check method should finish immediately.
+ */
+ virtual bool preCheck(Effort level = EFFORT_FULL);
+ /**
+ * Post-check, called after the fact queue of the theory is processed.
+ */
+ virtual void postCheck(Effort level = EFFORT_FULL);
+ /**
+ * Pre-notify fact, return true if the theory processed it. If this
+ * method returns false, then the atom will be added to the equality engine
+ * of the theory and notifyFact will be called with isInternal=false.
+ *
+ * Theories that implement check but do not use official equality
+ * engines should always return true for this method.
+ *
+ * @param atom The atom
+ * @param polarity Its polarity
+ * @param fact The original literal that was asserted
+ * @param isPrereg Whether the assertion is preregistered
+ * @return true if the theory completely processed this fact, i.e. it does
+ * not need to assert the fact to its equality engine.
+ */
+ virtual bool preNotifyFact(TNode atom, bool pol, TNode fact, bool isPrereg);
+ /**
+ * Notify fact, called immediately after the fact was pushed into the
+ * equality engine.
+ *
+ * @param atom The atom
+ * @param polarity Its polarity
+ * @param fact The original literal that was asserted
+ * @param isInternal Whether the origin of the fact was internal
+ */
+ virtual void notifyFact(TNode atom, bool pol, TNode fact, bool isInternal);
+ //--------------------------------- end check
+
+ //--------------------------------- collect model info
/**
* Get all relevant information in this theory regarding the current
* model. This should be called after a call to check( FULL_EFFORT )
*
* This method returns true if and only if the equality engine of m is
* consistent as a result of this call.
+ *
+ * The standard method for collectModelInfo computes the relevant terms,
+ * asserts the theory's equality engine to the model (if necessary) and
+ * then calls computeModelValues.
+ *
+ * TODO (project #39): this method should be non-virtual, once all theories
+ * conform to the new standard
*/
virtual bool collectModelInfo(TheoryModel* m);
+ /**
+ * Same as above, but with empty irrKinds. This version can be overridden
+ * by the theory, e.g. by restricting or extending the set of terms returned
+ * by computeRelevantTermsInternal, which is called by default with no
+ * irrKinds.
+ */
+ virtual void computeRelevantTerms(std::set<Node>& termSet,
+ bool includeShared = true);
+ /**
+ * Collect model values, after equality information is added to the model.
+ * The argument termSet is the set of relevant terms returned by
+ * computeRelevantTerms.
+ */
+ virtual bool collectModelValues(TheoryModel* m, std::set<Node>& termSet);
/** if theories want to do something with model after building, do it here */
virtual void postProcessModel( TheoryModel* m ){ }
+ //--------------------------------- end collect model info
+
+ //--------------------------------- preprocessing
/**
* Statically learn from assertion "in," which has been asserted
* true at the top level. The theory should only add (via
* preprocessing before they are asserted to theory engine.
*/
virtual void ppNotifyAssertions(const std::vector<Node>& assertions) {}
+ //--------------------------------- end preprocessing
/**
* A Theory is called with presolve exactly one time per user
/** Turn on proof-production mode. */
void produceProofs() { d_proofsEnabled = true; }
-
};/* class Theory */
std::ostream& operator<<(std::ostream& os, theory::Theory::Effort level);
Theory::Set theories = d_sharedTerms.getTheoriesToNotify(atom, term);
for (TheoryId id = THEORY_FIRST; id != THEORY_LAST; ++ id) {
if (Theory::setContains(id, theories)) {
- theoryOf(id)->addSharedTermInternal(term);
+ theoryOf(id)->addSharedTerm(term);
}
}
d_sharedTerms.markNotified(term, theories);
return EQUALITY_FALSE_IN_MODEL;
}
-void TheoryUF::addSharedTerm(TNode t) {
+void TheoryUF::notifySharedTerm(TNode t)
+{
Debug("uf::sharing") << "TheoryUF::addSharedTerm(" << t << ")" << std::endl;
d_equalityEngine->addTriggerTerm(t, THEORY_UF);
}
void ppStaticLearn(TNode in, NodeBuilder<>& learned) override;
void presolve() override;
- void addSharedTerm(TNode n) override;
+ void notifySharedTerm(TNode n) override;
void computeCareGraph() override;
EqualityStatus getEqualityStatus(TNode a, TNode b) override;
projects / cvc5.git / commitdiff