diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-09-02 16:02:41 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-09-02 16:02:41 -0500 |
commit | 2d6d62b7bc0c15a44b38641a52ba389591ecc7f6 (patch) | |
tree | e11ae0a24c157cf01dbcf287727240b4e75b7b8a /src/theory/uf/equality_engine.h | |
parent | dba70e10ef8ae0a991969cb7ca0cba2d0e9d9d4d (diff) | |
parent | 0f9fb31069d51e003a39b0e93f506324dec2bdac (diff) |
Merge branch 'master' into fixCMSBuildPRfixCMSBuildPR
Diffstat (limited to 'src/theory/uf/equality_engine.h')
-rw-r--r-- | src/theory/uf/equality_engine.h | 32 |
1 files changed, 0 insertions, 32 deletions
diff --git a/src/theory/uf/equality_engine.h b/src/theory/uf/equality_engine.h index 19a10eba8..f8444965f 100644 --- a/src/theory/uf/equality_engine.h +++ b/src/theory/uf/equality_engine.h @@ -43,26 +43,10 @@ namespace CVC4 { namespace theory { namespace eq { - -class EqProof; class EqClassesIterator; class EqClassIterator; /** - * An interface for equality engine notifications during equality path reconstruction. - * Can be used to add theory-specific logic for, e.g., proof construction. - */ -class PathReconstructionNotify { -public: - - virtual ~PathReconstructionNotify() {} - - virtual void notify(unsigned reasonType, Node reason, Node a, Node b, - std::vector<TNode>& equalities, - EqProof* proof) const = 0; -}; - -/** * Class for keeping an incremental congruence closure over a set of terms. It provides * notifications via an EqualityEngineNotify object. */ @@ -152,9 +136,6 @@ private: /** The map of kinds with operators to be considered external (for higher-order) */ KindMap d_congruenceKindsExtOperators; - /** Objects that need to be notified during equality path reconstruction */ - std::map<unsigned, const PathReconstructionNotify*> d_pathReconstructionTriggers; - /** Map from nodes to their ids */ std::unordered_map<TNode, EqualityNodeId, TNodeHashFunction> d_nodeIds; @@ -196,9 +177,6 @@ private: /** Memory for the use-list nodes */ std::vector<UseListNode> d_useListNodes; - /** A fresh merge reason type to return upon request */ - unsigned d_freshMergeReasonType; - /** * We keep a list of asserted equalities. Not among original terms, but * among the class representatives. @@ -861,16 +839,6 @@ private: */ bool consistent() const { return !d_done; } - /** - * Marks an object for merge type based notification during equality path reconstruction. - */ - void addPathReconstructionTrigger(unsigned trigger, const PathReconstructionNotify* notify); - - /** - * Returns a fresh merge reason type tag for the client to use. - */ - unsigned getFreshMergeReasonType(); - /** Identify this equality engine (for debugging, etc..) */ std::string identify() const; }; |