diff options
| author | Tim King <taking@cs.nyu.edu> | 2017-10-25 14:28:07 -0700 |
|---|---|---|
| committer | Aina Niemetz <aina.niemetz@gmail.com> | 2017-10-25 14:28:07 -0700 |
| commit | 0e3f99d90a5fcafd04b04adf0d3e7e71ccfa65b0 (patch) | |
| tree | d0a60841c95046ab9b19923d393f663805e962da /src/theory/uf/equality_engine.h | |
| parent | c49ef48588c708bfef3c7a0f9db8219415301a94 (diff) | |
Switching EqProof to use shared_ptr everywhere. (#1217)
This clarifies the memory ownership of EqProofs.
Diffstat (limited to 'src/theory/uf/equality_engine.h')
| -rw-r--r-- | src/theory/uf/equality_engine.h | 18 |
1 files changed, 12 insertions, 6 deletions
diff --git a/src/theory/uf/equality_engine.h b/src/theory/uf/equality_engine.h index 9638b9f09..a89e55312 100644 --- a/src/theory/uf/equality_engine.h +++ b/src/theory/uf/equality_engine.h @@ -21,6 +21,7 @@ #include <deque> #include <queue> +#include <memory> #include <unordered_map> #include <vector> @@ -150,7 +151,8 @@ public: virtual ~PathReconstructionNotify() {} virtual void notify(unsigned reasonType, Node reason, Node a, Node b, - std::vector<TNode>& equalities, EqProof* proof) const = 0; + std::vector<TNode>& equalities, + EqProof* proof) const = 0; }; /** @@ -506,7 +508,7 @@ private: * imply t1 = t2. Returns TNodes as the assertion equalities should be hashed somewhere * else. */ - void getExplanation(EqualityEdgeId t1Id, EqualityNodeId t2Id, std::vector<TNode>& equalities, EqProof * eqp) const; + void getExplanation(EqualityEdgeId t1Id, EqualityNodeId t2Id, std::vector<TNode>& equalities, EqProof* eqp) const; /** * Print the equality graph. @@ -794,14 +796,17 @@ public: * Returns the reasons (added when asserting) that imply it * in the assertions vector. */ - void explainEquality(TNode t1, TNode t2, bool polarity, std::vector<TNode>& assertions, EqProof * eqp = NULL) const; + void explainEquality(TNode t1, TNode t2, bool polarity, + std::vector<TNode>& assertions, + EqProof* eqp = nullptr) const; /** * Get an explanation of the predicate being true or false. * Returns the reasons (added when asserting) that imply imply it * in the assertions vector. */ - void explainPredicate(TNode p, bool polarity, std::vector<TNode>& assertions, EqProof * eqp = NULL) const; + void explainPredicate(TNode p, bool polarity, std::vector<TNode>& assertions, + EqProof* eqp = nullptr) const; /** * Add term to the set of trigger terms with a corresponding tag. The notify class will get @@ -925,8 +930,9 @@ public: EqProof() : d_id(MERGED_THROUGH_REFLEXIVITY){} unsigned d_id; Node d_node; - std::vector< EqProof * > d_children; - void debug_print(const char * c, unsigned tb = 0, PrettyPrinter* prettyPrinter = NULL) const; + std::vector<std::shared_ptr<EqProof>> d_children; + void debug_print(const char* c, unsigned tb = 0, + PrettyPrinter* prettyPrinter = nullptr) const; };/* class EqProof */ } // Namespace eq |