diff options
Diffstat (limited to 'src/theory/shared_terms_database.h')
| -rw-r--r-- | src/theory/shared_terms_database.h | 20 |
1 files changed, 12 insertions, 8 deletions
diff --git a/src/theory/shared_terms_database.h b/src/theory/shared_terms_database.h index fb972b73f..7b6527517 100644 --- a/src/theory/shared_terms_database.h +++ b/src/theory/shared_terms_database.h @@ -123,14 +123,14 @@ private: bool propagateEquality(TNode equality, bool polarity); /** Theory engine */ - TheoryEngine* d_theoryEngine; + TheoryEngine* d_theoryEngine; /** Are we in conflict */ context::CDO<bool> d_inConflict; - + /** Conflicting terms, if any */ Node d_conflictLHS, d_conflictRHS; - + /** Polarity of the conflict */ bool d_conflictPolarity; @@ -166,7 +166,7 @@ public: */ bool isKnown(TNode literal) const; - /** + /** * Returns an explanation of the propagation that came from the database. */ Node explain(TNode literal) const; @@ -175,10 +175,10 @@ public: * Add an equality to propagate. */ void addEqualityToPropagate(TNode equality); - + /** - * Add a shared term to the database. The shared term is a subterm of the atom and - * should be associated with the given theory. + * Add a shared term to the database. The shared term is a subterm of the atom and + * should be associated with the given theory. */ void addSharedTerm(TNode atom, TNode term, theory::Theory::Set theories); @@ -211,7 +211,7 @@ public: * Get the theories that share the term and have been notified already. */ theory::Theory::Set getNotifiedTheories(TNode term) const; - + /** * Returns true if the term is currently registered as shared with some theory. */ @@ -238,6 +238,10 @@ public: */ bool areDisequal(TNode a, TNode b) const; + /** + * get equality engine + */ + theory::eq::EqualityEngine* getEqualityEngine() { return &d_equalityEngine; } protected: /** |