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.

6 files changed, 368 insertions, 250 deletions

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 6bbc2d29b..d8b778efa 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -811,6 +811,9 @@ libcvc4_add_sources(
   theory/uf/cardinality_extension.h
   theory/uf/equality_engine.cpp
   theory/uf/equality_engine.h
+  theory/uf/equality_engine_iterator.cpp
+  theory/uf/equality_engine_iterator.h
+  theory/uf/equality_engine_notify.h
   theory/uf/equality_engine_types.h
   theory/uf/eq_proof.cpp
   theory/uf/eq_proof.h
diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp
index 171140d89..3abc56553 100644
--- a/src/theory/uf/equality_engine.cpp
+++ b/src/theory/uf/equality_engine.cpp
@@ -2358,109 +2358,6 @@ bool EqualityEngine::propagateTriggerTermDisequalities(Theory::Set tags, Trigger
   return !d_done;
 }
 
-EqClassesIterator::EqClassesIterator() :
-    d_ee(NULL), d_it(0) {
-}
-
-EqClassesIterator::EqClassesIterator(const eq::EqualityEngine* ee)
-: d_ee(ee)
-{
-  Assert(d_ee->consistent());
-  d_it = 0;
-  // Go to the first non-internal node that is it's own representative
-  if(d_it < d_ee->d_nodesCount && (d_ee->d_isInternal[d_it] || d_ee->getEqualityNode(d_it).getFind() != d_it)) {
-    ++d_it;
-  }
-}
-
-Node EqClassesIterator::operator*() const {
-  return d_ee->d_nodes[d_it];
-}
-
-bool EqClassesIterator::operator==(const EqClassesIterator& i) const {
-  return d_ee == i.d_ee && d_it == i.d_it;
-}
-
-bool EqClassesIterator::operator!=(const EqClassesIterator& i) const {
-  return !(*this == i);
-}
-
-EqClassesIterator& EqClassesIterator::operator++() {
-  ++d_it;
-  while(d_it < d_ee->d_nodesCount && (d_ee->d_isInternal[d_it] || d_ee->getEqualityNode(d_it).getFind() != d_it)) {
-    ++d_it;
-  }
-  return *this;
-}
-
-EqClassesIterator EqClassesIterator::operator++(int) {
-  EqClassesIterator i = *this;
-  ++*this;
-  return i;
-}
-
-bool EqClassesIterator::isFinished() const {
-  return d_it >= d_ee->d_nodesCount;
-}
-
-EqClassIterator::EqClassIterator()
-: d_ee(NULL)
-, d_start(null_id)
-, d_current(null_id)
-{}
-
-EqClassIterator::EqClassIterator(Node eqc, const eq::EqualityEngine* ee)
-: d_ee(ee)
-{
-  Assert(d_ee->consistent());
-  d_current = d_start = d_ee->getNodeId(eqc);
-  Assert(d_start == d_ee->getEqualityNode(d_start).getFind());
-  Assert(!d_ee->d_isInternal[d_start]);
-}
-
-Node EqClassIterator::operator*() const {
-  return d_ee->d_nodes[d_current];
-}
-
-bool EqClassIterator::operator==(const EqClassIterator& i) const {
-  return d_ee == i.d_ee && d_current == i.d_current;
-}
-
-bool EqClassIterator::operator!=(const EqClassIterator& i) const {
-  return !(*this == i);
-}
-
-EqClassIterator& EqClassIterator::operator++() {
-  Assert(!isFinished());
-
-  Assert(d_start == d_ee->getEqualityNode(d_current).getFind());
-  Assert(!d_ee->d_isInternal[d_current]);
-
-  // Find the next one
-  do {
-    d_current = d_ee->getEqualityNode(d_current).getNext();
-  } while(d_ee->d_isInternal[d_current]);
-
-  Assert(d_start == d_ee->getEqualityNode(d_current).getFind());
-  Assert(!d_ee->d_isInternal[d_current]);
-
-  if(d_current == d_start) {
-    // we end when we have cycled back to the original representative
-    d_current = null_id;
-  }
-  return *this;
-}
-
-EqClassIterator EqClassIterator::operator++(int) {
-  EqClassIterator i = *this;
-  ++*this;
-  return i;
-}
-
-bool EqClassIterator::isFinished() const {
-  return d_current == null_id;
-}
-
 } // Namespace uf
 } // Namespace theory
 } // Namespace CVC4
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
diff --git a/src/theory/uf/equality_engine_iterator.cpp b/src/theory/uf/equality_engine_iterator.cpp
new file mode 100644
index 000000000..2ed86499c
--- /dev/null
+++ b/src/theory/uf/equality_engine_iterator.cpp
@@ -0,0 +1,135 @@
+/*********************                                                        */
+/*! \file equality_engine_iterator.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Dejan Jovanovic, Andrew Reynolds, Guy Katz
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Implementation of iterator class for equality engine
+ **/
+
+#include "theory/uf/equality_engine_iterator.h"
+
+#include "theory/uf/equality_engine.h"
+
+namespace CVC4 {
+namespace theory {
+namespace eq {
+
+EqClassesIterator::EqClassesIterator() : d_ee(nullptr), d_it(0) {}
+
+EqClassesIterator::EqClassesIterator(const eq::EqualityEngine* ee) : d_ee(ee)
+{
+  Assert(d_ee->consistent());
+  d_it = 0;
+  // Go to the first non-internal node that is it's own representative
+  if (d_it < d_ee->d_nodesCount
+      && (d_ee->d_isInternal[d_it]
+          || d_ee->getEqualityNode(d_it).getFind() != d_it))
+  {
+    ++d_it;
+  }
+}
+
+Node EqClassesIterator::operator*() const { return d_ee->d_nodes[d_it]; }
+
+bool EqClassesIterator::operator==(const EqClassesIterator& i) const
+{
+  return d_ee == i.d_ee && d_it == i.d_it;
+}
+
+bool EqClassesIterator::operator!=(const EqClassesIterator& i) const
+{
+  return !(*this == i);
+}
+
+EqClassesIterator& EqClassesIterator::operator++()
+{
+  ++d_it;
+  while (d_it < d_ee->d_nodesCount
+         && (d_ee->d_isInternal[d_it]
+             || d_ee->getEqualityNode(d_it).getFind() != d_it))
+  {
+    ++d_it;
+  }
+  return *this;
+}
+
+EqClassesIterator EqClassesIterator::operator++(int)
+{
+  EqClassesIterator i = *this;
+  ++*this;
+  return i;
+}
+
+bool EqClassesIterator::isFinished() const
+{
+  return d_it >= d_ee->d_nodesCount;
+}
+
+EqClassIterator::EqClassIterator()
+    : d_ee(nullptr), d_start(null_id), d_current(null_id)
+{
+}
+
+EqClassIterator::EqClassIterator(Node eqc, const eq::EqualityEngine* ee)
+    : d_ee(ee)
+{
+  Assert(d_ee->consistent());
+  d_current = d_start = d_ee->getNodeId(eqc);
+  Assert(d_start == d_ee->getEqualityNode(d_start).getFind());
+  Assert(!d_ee->d_isInternal[d_start]);
+}
+
+Node EqClassIterator::operator*() const { return d_ee->d_nodes[d_current]; }
+
+bool EqClassIterator::operator==(const EqClassIterator& i) const
+{
+  return d_ee == i.d_ee && d_current == i.d_current;
+}
+
+bool EqClassIterator::operator!=(const EqClassIterator& i) const
+{
+  return !(*this == i);
+}
+
+EqClassIterator& EqClassIterator::operator++()
+{
+  Assert(!isFinished());
+
+  Assert(d_start == d_ee->getEqualityNode(d_current).getFind());
+  Assert(!d_ee->d_isInternal[d_current]);
+
+  // Find the next one
+  do
+  {
+    d_current = d_ee->getEqualityNode(d_current).getNext();
+  } while (d_ee->d_isInternal[d_current]);
+
+  Assert(d_start == d_ee->getEqualityNode(d_current).getFind());
+  Assert(!d_ee->d_isInternal[d_current]);
+
+  if (d_current == d_start)
+  {
+    // we end when we have cycled back to the original representative
+    d_current = null_id;
+  }
+  return *this;
+}
+
+EqClassIterator EqClassIterator::operator++(int)
+{
+  EqClassIterator i = *this;
+  ++*this;
+  return i;
+}
+
+bool EqClassIterator::isFinished() const { return d_current == null_id; }
+
+}  // namespace eq
+}  // Namespace theory
+}  // Namespace CVC4
diff --git a/src/theory/uf/equality_engine_iterator.h b/src/theory/uf/equality_engine_iterator.h
new file mode 100644
index 000000000..212474d4c
--- /dev/null
+++ b/src/theory/uf/equality_engine_iterator.h
@@ -0,0 +1,84 @@
+/*********************                                                        */
+/*! \file equality_engine_iterator.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Dejan Jovanovic, Andrew Reynolds, Morgan Deters
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Iterator class for equality engine
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__THEORY__UF__EQUALITY_ENGINE_ITERATOR_H
+#define CVC4__THEORY__UF__EQUALITY_ENGINE_ITERATOR_H
+
+#include "expr/node.h"
+#include "theory/uf/equality_engine_types.h"
+
+namespace CVC4 {
+namespace theory {
+namespace eq {
+
+class EqualityEngine;
+
+/**
+ * Iterator to iterate over all the equivalence classes in an equality engine.
+ */
+class EqClassesIterator
+{
+ 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;
+
+ private:
+  /** Pointer to the equality engine we are iterating over */
+  const eq::EqualityEngine* d_ee;
+  /** The iterator value */
+  size_t d_it;
+};
+
+/**
+ * Iterator to iterate over the equivalence class members in a particular
+ * equivalence class.
+ */
+class EqClassIterator
+{
+ public:
+  EqClassIterator();
+  /**
+   * Iterate over equivalence class eqc, where eqc must be a representative of
+   * argument ee.
+   */
+  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;
+
+ private:
+  /** Pointer to the equality engine we are iterating over */
+  const eq::EqualityEngine* d_ee;
+  /** Starting node */
+  EqualityNodeId d_start;
+  /** Current node */
+  EqualityNodeId d_current;
+};
+
+}  // Namespace eq
+}  // Namespace theory
+}  // Namespace CVC4
+
+#endif
diff --git a/src/theory/uf/equality_engine_notify.h b/src/theory/uf/equality_engine_notify.h
new file mode 100644
index 000000000..2fd839115
--- /dev/null
+++ b/src/theory/uf/equality_engine_notify.h
@@ -0,0 +1,140 @@
+/*********************                                                        */
+/*! \file equality_engine_notify.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Dejan Jovanovic, Andrew Reynolds, Morgan Deters
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief The virtual class for notifications from the equality engine.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__THEORY__UF__EQUALITY_ENGINE_NOTIFY_H
+#define CVC4__THEORY__UF__EQUALITY_ENGINE_NOTIFY_H
+
+#include "expr/node.h"
+
+namespace CVC4 {
+namespace theory {
+namespace eq {
+
+/**
+ * Interface for equality engine notifications. All the notifications
+ * are safe as TNodes, but not necessarily for negations.
+ */
+class EqualityEngineNotify
+{
+ 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 */
+
+}  // Namespace eq
+}  // Namespace theory
+}  // Namespace CVC4
+
+#endif