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.

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