diff options
author | Mathias Preiner <mathias.preiner@gmail.com> | 2018-09-05 14:31:11 -0700 |
---|---|---|
committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-09-05 16:31:11 -0500 |
commit | 90b90bdfad8c5fbf0f3208e7282fee6dd58aafc0 (patch) | |
tree | 2382e87cacab179b7d74225c9a71e7043502911f /src/theory/arith | |
parent | 1c6b193a3a843b37e5248505f9004f6d1bb0dca7 (diff) |
Use std::uniqe_ptr for d_eq_infer to make Coverity happy. (#2432)
Diffstat (limited to 'src/theory/arith')
-rw-r--r-- | src/theory/arith/congruence_manager.cpp | 39 | ||||
-rw-r--r-- | src/theory/arith/congruence_manager.h | 9 |
2 files changed, 25 insertions, 23 deletions
diff --git a/src/theory/arith/congruence_manager.cpp b/src/theory/arith/congruence_manager.cpp index d4a59b4b0..bf251660d 100644 --- a/src/theory/arith/congruence_manager.cpp +++ b/src/theory/arith/congruence_manager.cpp @@ -28,35 +28,36 @@ namespace CVC4 { namespace theory { namespace arith { -ArithCongruenceManager::ArithCongruenceManager(context::Context* c, ConstraintDatabase& cd, SetupLiteralCallBack setup, const ArithVariables& avars, RaiseEqualityEngineConflict raiseConflict) - : d_inConflict(c), - d_raiseConflict(raiseConflict), - d_notify(*this), - d_eq_infer(NULL), - d_eqi_counter(0,c), - d_keepAlive(c), - d_propagatations(c), - d_explanationMap(c), - d_constraintDatabase(cd), - d_setupLiteral(setup), - d_avariables(avars), - d_ee(d_notify, c, "theory::arith::ArithCongruenceManager", true) +ArithCongruenceManager::ArithCongruenceManager( + context::Context* c, + ConstraintDatabase& cd, + SetupLiteralCallBack setup, + const ArithVariables& avars, + RaiseEqualityEngineConflict raiseConflict) + : d_inConflict(c), + d_raiseConflict(raiseConflict), + d_notify(*this), + d_eq_infer(), + d_eqi_counter(0, c), + d_keepAlive(c), + d_propagatations(c), + d_explanationMap(c), + d_constraintDatabase(cd), + d_setupLiteral(setup), + d_avariables(avars), + d_ee(d_notify, c, "theory::arith::ArithCongruenceManager", true) { d_ee.addFunctionKind(kind::NONLINEAR_MULT); d_ee.addFunctionKind(kind::EXPONENTIAL); d_ee.addFunctionKind(kind::SINE); //module to infer additional equalities based on normalization if( options::sNormInferEq() ){ - d_eq_infer = new quantifiers::EqualityInference(c, true); + d_eq_infer.reset(new quantifiers::EqualityInference(c, true)); d_true = NodeManager::currentNM()->mkConst( true ); } } -ArithCongruenceManager::~ArithCongruenceManager() { - if( d_eq_infer ){ - delete d_eq_infer; - } -} +ArithCongruenceManager::~ArithCongruenceManager() {} ArithCongruenceManager::Statistics::Statistics(): d_watchedVariables("theory::arith::congruence::watchedVariables", 0), diff --git a/src/theory/arith/congruence_manager.h b/src/theory/arith/congruence_manager.h index 278c79a2f..11c229399 100644 --- a/src/theory/arith/congruence_manager.h +++ b/src/theory/arith/congruence_manager.h @@ -77,10 +77,11 @@ private: void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) override; }; ArithCongruenceNotify d_notify; - - /** module for shostak normalization, d_eqi_counter is how many pending merges in d_eq_infer we have processed */ - quantifiers::EqualityInference * d_eq_infer; - context::CDO< unsigned > d_eqi_counter; + + /** module for shostak normalization, d_eqi_counter is how many pending merges + * in d_eq_infer we have processed */ + std::unique_ptr<quantifiers::EqualityInference> d_eq_infer; + context::CDO<unsigned> d_eqi_counter; Node d_true; context::CDList<Node> d_keepAlive; |