Includes iterators and notification callbacks. These classes will be highly relevant for planned extensions to the core theory engine infrastructure.
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
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
#include "cvc4_private.h"
-#pragma once
+#ifndef CVC4__THEORY__UF__EQUALITY_ENGINE_H
+#define CVC4__THEORY__UF__EQUALITY_ENGINE_H
#include <deque>
#include <queue>
#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"
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.
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
--- /dev/null
+/********************* */
+/*! \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
--- /dev/null
+/********************* */
+/*! \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
--- /dev/null
+/********************* */
+/*! \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
projects / cvc5.git / commitdiff