diff options
Diffstat (limited to 'src/theory/arrays/theory_arrays.cpp')
-rw-r--r-- | src/theory/arrays/theory_arrays.cpp | 16 |
1 files changed, 9 insertions, 7 deletions
diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp index a17f506de..b43ba5591 100644 --- a/src/theory/arrays/theory_arrays.cpp +++ b/src/theory/arrays/theory_arrays.cpp @@ -17,6 +17,7 @@ #include "theory/arrays/theory_arrays.h" #include <map> +#include <memory> #include "expr/kind.h" #include "options/arrays_options.h" @@ -395,7 +396,8 @@ bool TheoryArrays::propagate(TNode literal) }/* TheoryArrays::propagate(TNode) */ -void TheoryArrays::explain(TNode literal, std::vector<TNode>& assumptions, eq::EqProof *proof) { +void TheoryArrays::explain(TNode literal, std::vector<TNode>& assumptions, + eq::EqProof* proof) { // Do the work bool polarity = literal.getKind() != kind::NOT; TNode atom = polarity ? literal : literal[0]; @@ -831,16 +833,15 @@ Node TheoryArrays::explain(TNode literal) { return explanation; } -Node TheoryArrays::explain(TNode literal, eq::EqProof *proof) -{ +Node TheoryArrays::explain(TNode literal, eq::EqProof* proof) { ++d_numExplain; - Debug("arrays") << spaces(getSatContext()->getLevel()) << "TheoryArrays::explain(" << literal << ")" << std::endl; + Debug("arrays") << spaces(getSatContext()->getLevel()) + << "TheoryArrays::explain(" << literal << ")" << std::endl; std::vector<TNode> assumptions; explain(literal, assumptions, proof); return mkAnd(assumptions); } - ///////////////////////////////////////////////////////////////////////////// // SHARING ///////////////////////////////////////////////////////////////////////////// @@ -2238,9 +2239,10 @@ bool TheoryArrays::dischargeLemmas() void TheoryArrays::conflict(TNode a, TNode b) { Debug("pf::array") << "TheoryArrays::Conflict called" << std::endl; - eq::EqProof* proof = d_proofsEnabled ? new eq::EqProof() : NULL; + std::shared_ptr<eq::EqProof> proof = d_proofsEnabled ? + std::make_shared<eq::EqProof>() : nullptr; - d_conflictNode = explain(a.eqNode(b), proof); + d_conflictNode = explain(a.eqNode(b), proof.get()); if (!d_inCheckModel) { ProofArray* proof_array = NULL; |