diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-08-09 16:50:09 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-08-09 14:50:09 -0700 |
commit | 28f5438df1e5ba87aab60552658aa09b79c35ba2 (patch) | |
tree | a6220b7a3efdaaac55f161b2133a8235e7f40c97 /src/theory/uf/equality_engine.h | |
parent | 43ae3483320d7964166407f84d04339ece944bbf (diff) |
Splitting a few utility classes from EqualityEngine to their own file (#4862)
Includes iterators and notification callbacks. These classes will be highly relevant for planned extensions to the core theory engine infrastructure.
Diffstat (limited to 'src/theory/uf/equality_engine.h')
-rw-r--r-- | src/theory/uf/equality_engine.h | 153 |
1 files changed, 6 insertions, 147 deletions
diff --git a/src/theory/uf/equality_engine.h b/src/theory/uf/equality_engine.h index 6b1f3b6aa..42ae3437d 100644 --- a/src/theory/uf/equality_engine.h +++ b/src/theory/uf/equality_engine.h @@ -17,7 +17,8 @@ #include "cvc4_private.h" -#pragma once +#ifndef CVC4__THEORY__UF__EQUALITY_ENGINE_H +#define CVC4__THEORY__UF__EQUALITY_ENGINE_H #include <deque> #include <queue> @@ -33,6 +34,8 @@ #include "theory/rewriter.h" #include "theory/theory.h" #include "theory/uf/eq_proof.h" +#include "theory/uf/equality_engine_iterator.h" +#include "theory/uf/equality_engine_notify.h" #include "theory/uf/equality_engine_types.h" #include "util/statistics_registry.h" @@ -46,115 +49,6 @@ class EqClassesIterator; class EqClassIterator; /** - * Interface for equality engine notifications. All the notifications - * are safe as TNodes, but not necessarily for negations. - */ -class EqualityEngineNotify { - - friend class EqualityEngine; - -public: - - virtual ~EqualityEngineNotify() {}; - - /** - * Notifies about a trigger equality that became true or false. - * - * @param equality the equality that became true or false - * @param value the value of the equality - */ - virtual bool eqNotifyTriggerEquality(TNode equality, bool value) = 0; - - /** - * Notifies about a trigger predicate that became true or false. - * - * @param predicate the trigger predicate that became true or false - * @param value the value of the predicate - */ - virtual bool eqNotifyTriggerPredicate(TNode predicate, bool value) = 0; - - /** - * Notifies about the merge of two trigger terms. - * - * @param tag the theory that both triggers were tagged with - * @param t1 a term marked as trigger - * @param t2 a term marked as trigger - * @param value true if equal, false if dis-equal - */ - virtual bool eqNotifyTriggerTermEquality(TheoryId tag, TNode t1, TNode t2, bool value) = 0; - - /** - * Notifies about the merge of two constant terms. After this, all work is suspended and all you - * can do is ask for explanations. - * - * @param t1 a constant term - * @param t2 a constant term - */ - virtual void eqNotifyConstantTermMerge(TNode t1, TNode t2) = 0; - - /** - * Notifies about the creation of a new equality class. - * - * @param t the term forming the new class - */ - virtual void eqNotifyNewClass(TNode t) = 0; - - /** - * Notifies about the merge of two classes (just before the merge). - * - * @param t1 a term - * @param t2 a term - */ - virtual void eqNotifyPreMerge(TNode t1, TNode t2) = 0; - - /** - * Notifies about the merge of two classes (just after the merge). - * - * @param t1 a term - * @param t2 a term - */ - virtual void eqNotifyPostMerge(TNode t1, TNode t2) = 0; - - /** - * Notifies about the disequality of two terms. - * - * @param t1 a term - * @param t2 a term - * @param reason the reason - */ - virtual void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) = 0; - -};/* class EqualityEngineNotify */ - -/** - * Implementation of the notification interface that ignores all the - * notifications. - */ -class EqualityEngineNotifyNone : public EqualityEngineNotify { -public: - bool eqNotifyTriggerEquality(TNode equality, bool value) override - { - return true; - } - bool eqNotifyTriggerPredicate(TNode predicate, bool value) override - { - return true; - } - bool eqNotifyTriggerTermEquality(TheoryId tag, - TNode t1, - TNode t2, - bool value) override - { - return true; - } - void eqNotifyConstantTermMerge(TNode t1, TNode t2) override {} - void eqNotifyNewClass(TNode t) override {} - void eqNotifyPreMerge(TNode t1, TNode t2) override {} - void eqNotifyPostMerge(TNode t1, TNode t2) override {} - void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) override {} -};/* class EqualityEngineNotifyNone */ - -/** * An interface for equality engine notifications during equality path reconstruction. * Can be used to add theory-specific logic for, e.g., proof construction. */ @@ -915,43 +809,8 @@ public: unsigned getFreshMergeReasonType(); }; -/** - * Iterator to iterate over the equivalence classes. - */ -class EqClassesIterator { - const eq::EqualityEngine* d_ee; - size_t d_it; -public: - EqClassesIterator(); - EqClassesIterator(const eq::EqualityEngine* ee); - Node operator*() const; - bool operator==(const EqClassesIterator& i) const; - bool operator!=(const EqClassesIterator& i) const; - EqClassesIterator& operator++(); - EqClassesIterator operator++(int); - bool isFinished() const; -};/* class EqClassesIterator */ - -/** - * Iterator to iterate over the equivalence class members. - */ -class EqClassIterator { - const eq::EqualityEngine* d_ee; - /** Starting node */ - EqualityNodeId d_start; - /** Current node */ - EqualityNodeId d_current; -public: - EqClassIterator(); - EqClassIterator(Node eqc, const eq::EqualityEngine* ee); - Node operator*() const; - bool operator==(const EqClassIterator& i) const; - bool operator!=(const EqClassIterator& i) const; - EqClassIterator& operator++(); - EqClassIterator operator++(int); - bool isFinished() const; -};/* class EqClassIterator */ - } // Namespace eq } // Namespace theory } // Namespace CVC4 + +#endif |