Fix more simple coverity warnings (#2372)

2 files changed, 56 insertions, 33 deletions

diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp
index ab9fa6d54..317080ba6 100644
--- a/src/theory/sets/theory_sets_private.cpp
+++ b/src/theory/sets/theory_sets_private.cpp
@@ -37,25 +37,28 @@ namespace sets {
 
 TheorySetsPrivate::TheorySetsPrivate(TheorySets& external,
                                      context::Context* c,
-                                     context::UserContext* u):
-  d_rels(NULL),
-  d_members(c),
-  d_deq(c),
-  d_deq_processed(u),
-  d_keep(c),
-  d_proxy(u),
-  d_proxy_to_term(u),
-  d_lemmas_produced(u),
-  d_card_processed(u),
-  d_var_elim(u),
-  d_external(external),
-  d_notify(*this),
-  d_equalityEngine(d_notify, c, "theory::sets::ee", true),
-  d_conflict(c)
+                                     context::UserContext* u)
+    : d_members(c),
+      d_deq(c),
+      d_deq_processed(u),
+      d_keep(c),
+      d_sentLemma(false),
+      d_addedFact(false),
+      d_full_check_incomplete(false),
+      d_proxy(u),
+      d_proxy_to_term(u),
+      d_lemmas_produced(u),
+      d_card_enabled(false),
+      d_card_processed(u),
+      d_var_elim(u),
+      d_external(external),
+      d_notify(*this),
+      d_equalityEngine(d_notify, c, "theory::sets::ee", true),
+      d_conflict(c),
+      d_rels(
+          new TheorySetsRels(c, u, &d_equalityEngine, &d_conflict, external)),
+      d_rels_enabled(false)
 {
-
-  d_rels = new TheorySetsRels(c, u, &d_equalityEngine, &d_conflict, external);
-
   d_true = NodeManager::currentNM()->mkConst( true );
   d_false = NodeManager::currentNM()->mkConst( false );
   d_zero = NodeManager::currentNM()->mkConst( Rational(0) );
@@ -68,21 +71,14 @@ TheorySetsPrivate::TheorySetsPrivate(TheorySets& external,
   d_equalityEngine.addFunctionKind(kind::MEMBER);
   d_equalityEngine.addFunctionKind(kind::SUBSET);
 
-  // If cardinality is on.
   d_equalityEngine.addFunctionKind(kind::CARD);
-
-  d_card_enabled = false;
-  d_rels_enabled = false;
-
-}/* TheorySetsPrivate::TheorySetsPrivate() */
+}
 
 TheorySetsPrivate::~TheorySetsPrivate(){
-  delete d_rels;
   for (std::pair<const Node, EqcInfo*>& current_pair : d_eqc_info) {
     delete current_pair.second;
   }
-}/* TheorySetsPrivate::~TheorySetsPrivate() */
-
+}
 
 void TheorySetsPrivate::eqNotifyNewClass(TNode t) {
   if( t.getKind()==kind::SINGLETON || t.getKind()==kind::EMPTYSET ){
diff --git a/src/theory/sets/theory_sets_private.h b/src/theory/sets/theory_sets_private.h
index 31aec85c3..d36e0ddb1 100644
--- a/src/theory/sets/theory_sets_private.h
+++ b/src/theory/sets/theory_sets_private.h
@@ -46,8 +46,6 @@ class TheorySetsPrivate {
   typedef context::CDHashMap< Node, int, NodeHashFunction> NodeIntMap;
   typedef context::CDHashSet<Node, NodeHashFunction> NodeSet;
   typedef context::CDHashMap< Node, Node, NodeHashFunction > NodeMap;
-private:
-  TheorySetsRels * d_rels;
 public:
   void eqNotifyNewClass(TNode t);
   void eqNotifyPreMerge(TNode t1, TNode t2);
@@ -113,9 +111,25 @@ private:
   void addEqualityToExp( Node a, Node b, std::vector< Node >& exp );
   
   void debugPrintSet( Node s, const char * c );
-  
+
+  /** sent lemma
+   *
+   * This flag is set to true during a full effort check if this theory
+   * called d_out->lemma(...).
+   */
   bool d_sentLemma;
+  /** added fact
+   *
+   * This flag is set to true during a full effort check if this theory
+   * added an internal fact to its equality engine.
+   */
   bool d_addedFact;
+  /** full check incomplete
+   *
+   * This flag is set to true during a full effort check if this theory
+   * is incomplete for some reason (for instance, if we combine cardinality
+   * with a relation or extended function kind).
+   */
   bool d_full_check_incomplete;
   NodeMap d_proxy;  
   NodeMap d_proxy_to_term;  
@@ -139,11 +153,15 @@ private:
   std::map< Kind, std::map< Node, std::map< Node, Node > > > d_bop_index;
   std::map< Kind, std::vector< Node > > d_op_list;
   //cardinality
-private:
+ private:
+  /** is cardinality enabled?
+   *
+   * This flag is set to true during a full effort check if any constraint
+   * involving cardinality constraints is asserted to this theory.
+   */
   bool d_card_enabled;
   /** element types of sets for which cardinality is enabled */
   std::map<TypeNode, bool> d_t_card_enabled;
-  bool d_rels_enabled;
   std::map< Node, Node > d_eqc_to_card_term;
   NodeSet d_card_processed;
   std::map< Node, std::vector< Node > > d_card_parent;
@@ -300,7 +318,16 @@ private:
   bool isCareArg( Node n, unsigned a );
 public:
   bool isEntailed( Node n, bool pol );
-  
+
+ private:
+  /** subtheory solver for the theory of relations */
+  std::unique_ptr<TheorySetsRels> d_rels;
+  /** are relations enabled?
+   *
+   * This flag is set to true during a full effort check if any constraint
+   * involving relational constraints is asserted to this theory.
+   */
+  bool d_rels_enabled;
 };/* class TheorySetsPrivate */