summaryrefslogtreecommitdiff
path: root/src/theory
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory')
-rw-r--r--src/theory/arith/theory_arith.cpp4
-rw-r--r--src/theory/arith/theory_arith.h2
-rw-r--r--src/theory/arrays/theory_arrays.cpp8
-rw-r--r--src/theory/arrays/theory_arrays.h2
-rw-r--r--src/theory/bv/theory_bv.cpp7
-rw-r--r--src/theory/bv/theory_bv.h2
-rw-r--r--src/theory/datatypes/theory_datatypes.cpp10
-rw-r--r--src/theory/datatypes/theory_datatypes.h2
-rw-r--r--src/theory/fp/theory_fp.cpp6
-rw-r--r--src/theory/fp/theory_fp.h2
-rw-r--r--src/theory/sep/theory_sep.cpp6
-rw-r--r--src/theory/sep/theory_sep.h2
-rw-r--r--src/theory/sets/theory_sets.cpp4
-rw-r--r--src/theory/sets/theory_sets.h2
-rw-r--r--src/theory/strings/theory_strings.cpp9
-rw-r--r--src/theory/strings/theory_strings.h2
-rw-r--r--src/theory/theory.cpp142
-rw-r--r--src/theory/theory.h189
-rw-r--r--src/theory/theory_engine.cpp2
-rw-r--r--src/theory/uf/theory_uf.cpp3
-rw-r--r--src/theory/uf/theory_uf.h2
21 files changed, 290 insertions, 118 deletions
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index 4e0582f50..ea751ca74 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -87,9 +87,7 @@ TrustNode TheoryArith::expandDefinition(Node node)
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)
{
diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h
index d0147fe9f..bfe30db61 100644
--- a/src/theory/arith/theory_arith.h
+++ b/src/theory/arith/theory_arith.h
@@ -104,7 +104,7 @@ class TheoryArith : public Theory {
EqualityStatus getEqualityStatus(TNode a, TNode b) override;
- void addSharedTerm(TNode n) override;
+ void notifySharedTerm(TNode n) override;
Node getModelValue(TNode var) override;
diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index 34c4fd156..b4a234748 100644
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -883,9 +883,11 @@ Node TheoryArrays::explain(TNode literal, eq::EqProof* proof) {
// 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);
diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h
index a1fa19631..8cbf826c1 100644
--- a/src/theory/arrays/theory_arrays.h
+++ b/src/theory/arrays/theory_arrays.h
@@ -251,7 +251,7 @@ class TheoryArrays : public Theory {
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)
diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index d03d81a3d..1696d6185 100644
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -880,9 +880,10 @@ TrustNode TheoryBV::explain(TNode node)
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) {
diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h
index 65100f98f..c6e9282f4 100644
--- a/src/theory/bv/theory_bv.h
+++ b/src/theory/bv/theory_bv.h
@@ -244,7 +244,7 @@ class TheoryBV : public Theory {
*/
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); }
diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index 65264bb3f..f85b79c53 100644
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -727,11 +727,13 @@ TrustNode TheoryDatatypes::ppRewrite(TNode in)
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)
diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h
index 137aae469..6dd990b30 100644
--- a/src/theory/datatypes/theory_datatypes.h
+++ b/src/theory/datatypes/theory_datatypes.h
@@ -290,7 +290,7 @@ private:
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 {}
diff --git a/src/theory/fp/theory_fp.cpp b/src/theory/fp/theory_fp.cpp
index 82086aafe..0c5a92572 100644
--- a/src/theory/fp/theory_fp.cpp
+++ b/src/theory/fp/theory_fp.cpp
@@ -908,9 +908,10 @@ void TheoryFp::preRegisterTerm(TNode node)
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;
@@ -998,7 +999,6 @@ void TheoryFp::check(Effort level) {
}
// Resolve the abstractions for the conversion lemmas
- // if (level == EFFORT_COMBINATION) {
if (level == EFFORT_LAST_CALL)
{
Trace("fp") << "TheoryFp::check(): checking abstractions" << std::endl;
diff --git a/src/theory/fp/theory_fp.h b/src/theory/fp/theory_fp.h
index ad052f92a..79ece7bce 100644
--- a/src/theory/fp/theory_fp.h
+++ b/src/theory/fp/theory_fp.h
@@ -58,7 +58,7 @@ class TheoryFp : public Theory {
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;
diff --git a/src/theory/sep/theory_sep.cpp b/src/theory/sep/theory_sep.cpp
index cf3cf2f9a..0059d9f3a 100644
--- a/src/theory/sep/theory_sep.cpp
+++ b/src/theory/sep/theory_sep.cpp
@@ -160,9 +160,9 @@ TrustNode TheorySep::explain(TNode literal)
// 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);
}
diff --git a/src/theory/sep/theory_sep.h b/src/theory/sep/theory_sep.h
index bbb37a3a2..af411c64a 100644
--- a/src/theory/sep/theory_sep.h
+++ b/src/theory/sep/theory_sep.h
@@ -114,7 +114,7 @@ class TheorySep : public Theory {
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;
diff --git a/src/theory/sets/theory_sets.cpp b/src/theory/sets/theory_sets.cpp
index 647a7bb47..63ebacc23 100644
--- a/src/theory/sets/theory_sets.cpp
+++ b/src/theory/sets/theory_sets.cpp
@@ -88,9 +88,7 @@ void TheorySets::finishInit()
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) {
diff --git a/src/theory/sets/theory_sets.h b/src/theory/sets/theory_sets.h
index 9e04b89a7..a7fb31dab 100644
--- a/src/theory/sets/theory_sets.h
+++ b/src/theory/sets/theory_sets.h
@@ -58,7 +58,7 @@ class TheorySets : public Theory
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;
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index e42796354..0de0cc33c 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -153,15 +153,16 @@ bool TheoryStrings::areCareDisequal( TNode x, TNode y ) {
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) {
diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h
index 8a1afe6b3..f4aa0675c 100644
--- a/src/theory/strings/theory_strings.h
+++ b/src/theory/strings/theory_strings.h
@@ -96,7 +96,7 @@ class TheoryStrings : public Theory {
/** 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 */
diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp
index 7220e2e1c..f65a7c45c 100644
--- a/src/theory/theory.cpp
+++ b/src/theory/theory.cpp
@@ -44,8 +44,6 @@ std::ostream& operator<<(std::ostream& os, Theory::Effort level){
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:
@@ -109,9 +107,11 @@ void Theory::setEqualityEngine(eq::EqualityEngine* ee)
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;
}
@@ -266,11 +266,15 @@ TheoryId Theory::theoryOf(options::TheoryOfMode mode, TNode node)
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() {
@@ -394,17 +398,23 @@ void Theory::computeRelevantTermsInternal(std::set<Node>& termSet,
// 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);
}
}
@@ -474,6 +484,110 @@ void Theory::getCareGraph(CareGraph* careGraph) {
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
diff --git a/src/theory/theory.h b/src/theory/theory.h
index 349f36a57..8ea64e724 100644
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -138,9 +138,6 @@ class Theory {
/** 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;
@@ -184,7 +181,7 @@ class Theory {
*/
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
@@ -207,21 +204,7 @@ class Theory {
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.
@@ -334,6 +317,16 @@ class 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
/**
@@ -435,25 +428,23 @@ class Theory {
* 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; }
@@ -461,8 +452,6 @@ class Theory {
{ 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.
@@ -506,6 +495,9 @@ class Theory {
return d_valuation;
}
+ /** Get the equality engine being used by this theory. */
+ eq::EqualityEngine* getEqualityEngine();
+
/**
* Get the quantifiers engine associated to this theory.
*/
@@ -513,13 +505,6 @@ class 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; }
@@ -559,7 +544,7 @@ class Theory {
/**
* 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.
@@ -571,16 +556,8 @@ class Theory {
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
@@ -593,31 +570,17 @@ class Theory {
* 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
@@ -630,6 +593,74 @@ class Theory {
"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 )
@@ -637,10 +668,34 @@ class Theory {
*
* 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
@@ -681,6 +736,7 @@ class Theory {
* 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
@@ -941,7 +997,6 @@ class Theory {
/** Turn on proof-production mode. */
void produceProofs() { d_proofsEnabled = true; }
-
};/* class Theory */
std::ostream& operator<<(std::ostream& os, theory::Theory::Effort level);
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index b88b6158e..cf29039ff 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -1219,7 +1219,7 @@ void TheoryEngine::assertFact(TNode literal)
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);
diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
index 29014d33f..7d554c613 100644
--- a/src/theory/uf/theory_uf.cpp
+++ b/src/theory/uf/theory_uf.cpp
@@ -503,7 +503,8 @@ EqualityStatus TheoryUF::getEqualityStatus(TNode a, TNode b) {
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);
}
diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h
index 8efaf79e3..916c6ef6b 100644
--- a/src/theory/uf/theory_uf.h
+++ b/src/theory/uf/theory_uf.h
@@ -184,7 +184,7 @@ private:
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;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback