diff options
Diffstat (limited to 'src/theory/uf/equality_engine.h')
-rw-r--r-- | src/theory/uf/equality_engine.h | 71 |
1 files changed, 69 insertions, 2 deletions
diff --git a/src/theory/uf/equality_engine.h b/src/theory/uf/equality_engine.h index 18a525f2d..13b8898d5 100644 --- a/src/theory/uf/equality_engine.h +++ b/src/theory/uf/equality_engine.h @@ -141,7 +141,11 @@ public: * Creates a new node, which is in a list of it's own. */ EqualityNode(EqualityNodeId nodeId = null_id) - : d_size(1), d_findId(nodeId), d_nextId(nodeId), d_useList(null_uselist_id) {} + : d_size(1), + d_findId(nodeId), + d_nextId(nodeId), + d_useList(null_uselist_id) + {} /** * Retuerns the uselist. @@ -266,6 +270,12 @@ public: private: + /** The context we are using */ + context::Context* d_context; + + /** Whether to notify or not (temporarily disabled on equality checks) */ + bool d_performNotify; + /** The class to notify when a representative changes for a term */ NotifyClass d_notify; @@ -455,6 +465,21 @@ private: std::vector<TriggerId> d_nodeTriggers; /** + * List of terms that are marked as individual triggers. + */ + std::vector<EqualityNodeId> d_individualTriggers; + + /** + * Size of the individual triggers list. + */ + context::CDO<unsigned> d_individualTriggersSize; + + /** + * Map from ids to the individual trigger id representative. + */ + std::vector<EqualityNodeId> d_nodeIndividualTrigger; + + /** * Adds the trigger with triggerId to the beginning of the trigger list of the node with id nodeId. */ void addTriggerToList(EqualityNodeId nodeId, TriggerId triggerId); @@ -503,6 +528,11 @@ private: */ void debugPrintGraph() const; + /** The true node */ + Node d_true; + /** The false node */ + Node d_false; + public: /** @@ -511,15 +541,20 @@ public: */ EqualityEngine(NotifyClass& notify, context::Context* context, std::string name) : ContextNotifyObj(context), + d_context(context), + d_performNotify(true), d_notify(notify), d_nodesCount(context, 0), d_assertedEqualitiesCount(context, 0), d_equalityTriggersCount(context, 0), + d_individualTriggersSize(context, 0), d_stats(name) { Debug("equality") << "EqualityEdge::EqualityEngine(): id_null = " << +null_id << std::endl; Debug("equality") << "EqualityEdge::EqualityEngine(): edge_null = " << +null_edge << std::endl; Debug("equality") << "EqualityEdge::EqualityEngine(): trigger_null = " << +null_trigger << std::endl; + d_true = NodeManager::currentNM()->mkConst<bool>(true); + d_false = NodeManager::currentNM()->mkConst<bool>(false); } /** @@ -561,6 +596,11 @@ public: void addEquality(TNode t1, TNode t2, TNode reason); /** + * Adds an dis-equality t1 != t2 to the database. + */ + void addDisequality(TNode t1, TNode t2, TNode reason); + + /** * Returns the representative of the term t. */ TNode getRepresentative(TNode t) const; @@ -578,11 +618,38 @@ public: void getExplanation(TNode t1, TNode t2, std::vector<TNode>& equalities) const; /** + * Add term to the trigger terms. The notify class will get notified when two + * trigger terms become equal. Thihs will only happen on trigger term + * representatives. + */ + void addTriggerTerm(TNode t); + + /** + * Returns true if t is a trigger term or equal to some other trigger term. + */ + bool isTriggerTerm(TNode t) const; + + /** * Adds a notify trigger for equality t1 = t2, i.e. when t1 = t2 the notify will be called with - * (t1 = t2). + * trigger. */ void addTriggerEquality(TNode t1, TNode t2, TNode trigger); + /** + * Adds a notify trigger for dis-equality t1 != t2, i.e. when t1 != t2 the notify will be called with + * trigger. + */ + void addTriggerDisequality(TNode t1, TNode t2, TNode trigger); + + /** + * Check whether the two terms are equal. + */ + bool areEqual(TNode t1, TNode t2); + + /** + * Check whether the two term are dis-equal. + */ + bool areDisequal(TNode t1, TNode t2); }; } // Namespace uf |