diff options
Diffstat (limited to 'src/theory/uf')
-rw-r--r-- | src/theory/uf/equality_engine.cpp | 70 | ||||
-rw-r--r-- | src/theory/uf/equality_engine.h | 18 | ||||
-rw-r--r-- | src/theory/uf/theory_uf.cpp | 7 |
3 files changed, 58 insertions, 37 deletions
diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp index 1378b4edf..a9142c4ef 100644 --- a/src/theory/uf/equality_engine.cpp +++ b/src/theory/uf/equality_engine.cpp @@ -926,8 +926,12 @@ std::string EqualityEngine::edgesToString(EqualityEdgeId edgeId) const { return out.str(); } -void EqualityEngine::explainEquality(TNode t1, TNode t2, bool polarity, std::vector<TNode>& equalities, EqProof * eqp) const { - Debug("equality") << d_name << "::eq::explainEquality(" << t1 << ", " << t2 << ", " << (polarity ? "true" : "false") << ")" << ", proof = " << (eqp ? "ON" : "OFF") << std::endl; +void EqualityEngine::explainEquality(TNode t1, TNode t2, bool polarity, + std::vector<TNode>& equalities, + EqProof* eqp) const { + Debug("equality") << d_name << "::eq::explainEquality(" << t1 << ", " << t2 + << ", " << (polarity ? "true" : "false") << ")" + << ", proof = " << (eqp ? "ON" : "OFF") << std::endl; // The terms must be there already Assert(hasTerm(t1) && hasTerm(t2));; @@ -953,21 +957,21 @@ void EqualityEngine::explainEquality(TNode t1, TNode t2, bool polarity, std::vec for (unsigned i = reasonRef.mergesStart; i < reasonRef.mergesEnd; ++ i) { EqualityPair toExplain = d_deducedDisequalityReasons[i]; - EqProof* eqpc = NULL; + std::shared_ptr<EqProof> eqpc; // If we're constructing a (transitivity) proof, we don't need to include an explanation for x=x. if (eqp && toExplain.first != toExplain.second) { - eqpc = new EqProof; + eqpc = std::make_shared<EqProof>(); } - getExplanation(toExplain.first, toExplain.second, equalities, eqpc); + getExplanation(toExplain.first, toExplain.second, equalities, eqpc.get()); if (eqpc) { Debug("pf::ee") << "Child proof is:" << std::endl; eqpc->debug_print("pf::ee", 1); if (eqpc->d_id == eq::MERGED_THROUGH_TRANS) { - std::vector<EqProof *> orderedChildren; + std::vector<std::shared_ptr<EqProof>> orderedChildren; bool nullCongruenceFound = false; for (unsigned i = 0; i < eqpc->d_children.size(); ++i) { if (eqpc->d_children[i]->d_id==eq::MERGED_THROUGH_CONGRUENCE && @@ -1002,10 +1006,9 @@ void EqualityEngine::explainEquality(TNode t1, TNode t2, bool polarity, std::vec eqp->d_id = MERGED_THROUGH_CONSTANTS; } else if (eqp->d_children.size() == 1) { // The transitivity proof has just one child. Simplify. - EqProof* temp = eqp->d_children[0]; + std::shared_ptr<EqProof> temp = eqp->d_children[0]; eqp->d_children.clear(); *eqp = *temp; - delete temp; } Debug("pf::ee") << "Disequality explanation final proof: " << std::endl; @@ -1014,16 +1017,21 @@ void EqualityEngine::explainEquality(TNode t1, TNode t2, bool polarity, std::vec } } -void EqualityEngine::explainPredicate(TNode p, bool polarity, std::vector<TNode>& assertions, EqProof * eqp) const { - Debug("equality") << d_name << "::eq::explainPredicate(" << p << ")" << std::endl; +void EqualityEngine::explainPredicate(TNode p, bool polarity, + std::vector<TNode>& assertions, + EqProof* eqp) const { + Debug("equality") << d_name << "::eq::explainPredicate(" << p << ")" + << std::endl; // Must have the term Assert(hasTerm(p)); // Get the explanation - getExplanation(getNodeId(p), polarity ? d_trueId : d_falseId, assertions, eqp); + getExplanation(getNodeId(p), polarity ? d_trueId : d_falseId, assertions, + eqp); } -void EqualityEngine::getExplanation(EqualityNodeId t1Id, EqualityNodeId t2Id, std::vector<TNode>& equalities, EqProof * eqp) const { - +void EqualityEngine::getExplanation(EqualityNodeId t1Id, EqualityNodeId t2Id, + std::vector<TNode>& equalities, + EqProof* eqp) const { Debug("equality") << d_name << "::eq::getExplanation(" << d_nodes[t1Id] << "," << d_nodes[t2Id] << ")" << std::endl; // We can only explain the nodes that got merged @@ -1094,7 +1102,7 @@ void EqualityEngine::getExplanation(EqualityNodeId t1Id, EqualityNodeId t2Id, st Debug("equality") << d_name << "::eq::getExplanation(): path found: " << std::endl; - std::vector<EqProof *> eqp_trans; + std::vector<std::shared_ptr<EqProof>> eqp_trans; // Reconstruct the path do { @@ -1109,10 +1117,10 @@ void EqualityEngine::getExplanation(EqualityNodeId t1Id, EqualityNodeId t2Id, st Debug("equality") << d_name << " in currentEdge = (" << d_nodes[currentNode] << "," << d_nodes[edge.getNodeId()] << ")" << std::endl; Debug("equality") << d_name << " reason type = " << reasonType << std::endl; - EqProof* eqpc = NULL; + std::shared_ptr<EqProof> eqpc;; // Make child proof if a proof is being constructed if (eqp) { - eqpc = new EqProof; + eqpc = std::make_shared<EqProof>(); eqpc->d_id = reasonType; } @@ -1126,11 +1134,13 @@ void EqualityEngine::getExplanation(EqualityNodeId t1Id, EqualityNodeId t2Id, st Debug("equality") << push; Debug("equality") << "Explaining left hand side equalities" << std::endl; - EqProof * eqpc1 = eqpc ? new EqProof : NULL; - getExplanation(f1.a, f2.a, equalities, eqpc1); + std::shared_ptr<EqProof> eqpc1 = + eqpc ? std::make_shared<EqProof>() : nullptr; + getExplanation(f1.a, f2.a, equalities, eqpc1.get()); Debug("equality") << "Explaining right hand side equalities" << std::endl; - EqProof * eqpc2 = eqpc ? new EqProof : NULL; - getExplanation(f1.b, f2.b, equalities, eqpc2); + std::shared_ptr<EqProof> eqpc2 = + eqpc ? std::make_shared<EqProof>() : nullptr; + getExplanation(f1.b, f2.b, equalities, eqpc2.get()); if( eqpc ){ eqpc->d_children.push_back( eqpc1 ); eqpc->d_children.push_back( eqpc2 ); @@ -1173,8 +1183,9 @@ void EqualityEngine::getExplanation(EqualityNodeId t1Id, EqualityNodeId t2Id, st // Explain why a = b constant Debug("equality") << push; - EqProof * eqpc1 = eqpc ? new EqProof : NULL; - getExplanation(eq.a, eq.b, equalities, eqpc1); + std::shared_ptr<EqProof> eqpc1 = + eqpc ? std::make_shared<EqProof>() : nullptr; + getExplanation(eq.a, eq.b, equalities, eqpc1.get()); if( eqpc ){ eqpc->d_children.push_back( eqpc1 ); } @@ -1198,8 +1209,10 @@ void EqualityEngine::getExplanation(EqualityNodeId t1Id, EqualityNodeId t2Id, st for (unsigned i = 0; i < interpreted.getNumChildren(); ++ i) { EqualityNodeId childId = getNodeId(interpreted[i]); Assert(isConstant(childId)); - EqProof * eqpcc = eqpc ? new EqProof : NULL; - getExplanation(childId, getEqualityNode(childId).getFind(), equalities, eqpcc); + std::shared_ptr<EqProof> eqpcc = + eqpc ? std::make_shared<EqProof>() : nullptr; + getExplanation(childId, getEqualityNode(childId).getFind(), + equalities, eqpcc.get()); if( eqpc ) { eqpc->d_children.push_back( eqpcc ); @@ -1223,8 +1236,9 @@ void EqualityEngine::getExplanation(EqualityNodeId t1Id, EqualityNodeId t2Id, st if (eqpc) { //apply proof reconstruction processing (when eqpc is non-null) if (d_pathReconstructionTriggers.find(reasonType) != d_pathReconstructionTriggers.end()) { - d_pathReconstructionTriggers.find(reasonType)->second->notify(reasonType, reason, a, b, - equalities, eqpc); + d_pathReconstructionTriggers.find(reasonType) + ->second->notify(reasonType, reason, a, b, equalities, + eqpc.get()); } if (reasonType == MERGED_THROUGH_EQUALITY) { eqpc->d_node = reason; @@ -1255,9 +1269,8 @@ void EqualityEngine::getExplanation(EqualityNodeId t1Id, EqualityNodeId t2Id, st if (eqpc != NULL && eqpc->d_id == MERGED_THROUGH_REFLEXIVITY) { if(eqpc->d_node.isNull()) { Assert(eqpc->d_children.size() == 1); - EqProof *p = eqpc; + std::shared_ptr<EqProof> p = eqpc; eqpc = p->d_children[0]; - delete p; } else { Assert(eqpc->d_children.empty()); } @@ -1270,7 +1283,6 @@ void EqualityEngine::getExplanation(EqualityNodeId t1Id, EqualityNodeId t2Id, st if (eqp) { if(eqp_trans.size() == 1) { *eqp = *eqp_trans[0]; - delete eqp_trans[0]; } else { eqp->d_id = MERGED_THROUGH_TRANS; eqp->d_children.insert( eqp->d_children.end(), eqp_trans.begin(), eqp_trans.end() ); 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 diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp index e8cc3b385..170621603 100644 --- a/src/theory/uf/theory_uf.cpp +++ b/src/theory/uf/theory_uf.cpp @@ -17,6 +17,8 @@ #include "theory/uf/theory_uf.h" +#include <memory> + #include "options/quantifiers_options.h" #include "options/smt_options.h" #include "options/uf_options.h" @@ -629,8 +631,9 @@ void TheoryUF::computeCareGraph() { }/* TheoryUF::computeCareGraph() */ void TheoryUF::conflict(TNode a, TNode b) { - eq::EqProof* pf = d_proofsEnabled ? new eq::EqProof() : NULL; - d_conflictNode = explain(a.eqNode(b),pf); + std::shared_ptr<eq::EqProof> pf = + d_proofsEnabled ? std::make_shared<eq::EqProof>() : nullptr; + d_conflictNode = explain(a.eqNode(b), pf.get()); ProofUF* puf = d_proofsEnabled ? new ProofUF( pf ) : NULL; d_out->conflict(d_conflictNode, puf); d_conflict = true; |