Fix more simple coverity warnings (#2372)

14 files changed, 135 insertions, 145 deletions

diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index 65df3a642..283c70ada 100644
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -41,24 +41,26 @@ namespace CVC4 {
 namespace theory {
 namespace datatypes {
 
-TheoryDatatypes::TheoryDatatypes(Context* c, UserContext* u, OutputChannel& out,
-                                 Valuation valuation, const LogicInfo& logicInfo)
+TheoryDatatypes::TheoryDatatypes(Context* c,
+                                 UserContext* u,
+                                 OutputChannel& out,
+                                 Valuation valuation,
+                                 const LogicInfo& logicInfo)
     : Theory(THEORY_DATATYPES, c, u, out, valuation, logicInfo),
-      //d_cycle_check(c),
-      d_hasSeenCycle(c, false),
       d_infer(c),
       d_infer_exp(c),
-      d_term_sk( u ),
-      d_notify( *this ),
+      d_term_sk(u),
+      d_notify(*this),
       d_equalityEngine(d_notify, c, "theory::datatypes", true),
-      d_labels( c ),
-      d_selector_apps( c ),
-      //d_consEqc( c ),
-      d_conflict( c, false ),
-      d_collectTermsCache( c ),
-      d_functionTerms( c ),
-      d_singleton_eq( u ),
-      d_lemmas_produced_c( u )
+      d_labels(c),
+      d_selector_apps(c),
+      d_conflict(c, false),
+      d_addedLemma(false),
+      d_addedFact(false),
+      d_collectTermsCache(c),
+      d_functionTerms(c),
+      d_singleton_eq(u),
+      d_lemmas_produced_c(u)
 {
   // The kinds we are treating as function application in congruence
   d_equalityEngine.addFunctionKind(kind::APPLY_CONSTRUCTOR);
@@ -765,25 +767,6 @@ void TheoryDatatypes::conflict(TNode a, TNode b){
 void TheoryDatatypes::eqNotifyNewClass(TNode t){
   if( t.getKind()==APPLY_CONSTRUCTOR ){
     getOrMakeEqcInfo( t, true );
-    //look at all equivalence classes with constructor terms
-/*
-    for( BoolMap::const_iterator it = d_consEqc.begin(); it != d_consEqc.end(); ++it ){
-      if( (*it).second ){
-        TNode r = (*it).first;
-        if( r.getType()==t.getType() ){
-          EqcInfo * ei = getOrMakeEqcInfo( r, false );
-          if( ei && !ei->d_constructor.get().isNull() && ei->d_constructor.get().getOperator()!=t.getOperator() ){
-            Node deq = ei->d_constructor.get().eqNode( t ).negate();
-            d_pending.push_back( deq );
-            d_pending_exp[ deq ] = d_true;
-            Trace("datatypes-infer") << "DtInfer : diff constructor : " << deq << std::endl;
-            d_infer.push_back( deq );
-          }
-        }
-      }
-    }
-*/
-    //d_consEqc[t] = true;
   }
 }
 
@@ -865,14 +848,7 @@ void TheoryDatatypes::merge( Node t1, Node t2 ){
             if( d_conflict ){
               return;
             }
-            //d_consEqc[t1] = true;
           }
-          //AJR: do this?
-          //else if( cons2.isConst() ){
-          //  //prefer the constant
-          //  eqc1->d_constructor = cons2;
-          //}
-          //d_consEqc[t2] = false;
         }
       }else{
         Trace("datatypes-debug") << "  no eqc info for " << t1 << ", must create" << std::endl;
@@ -1998,9 +1974,6 @@ Node TheoryDatatypes::searchForCycle( TNode n, TNode on,
       for( unsigned i=0; i<ncons.getNumChildren(); i++ ) {
         TNode cn = searchForCycle( ncons[i], on, visited, proc, explanation, false );
         if( cn==on ) {
-          //if( Debug.isOn("datatypes-cycles") && !d_cycle_check.isConnectedNode( n, ncons[i] ) ){
-          //  Debug("datatypes-cycles") << "Cycle subterm: " << n << " is not -> " << ncons[i] << "!!!!" << std::endl;
-          //}
           //add explanation for why the constructor is connected
           if( n != ncons ) {
             explainEquality( n, ncons, true, explanation );
diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h
index e06bb7408..233ebd052 100644
--- a/src/theory/datatypes/theory_datatypes.h
+++ b/src/theory/datatypes/theory_datatypes.h
@@ -46,10 +46,6 @@ class TheoryDatatypes : public Theory {
   typedef context::CDHashMap<Node, bool, NodeHashFunction> BoolMap;
   typedef context::CDHashMap<Node, Node, NodeHashFunction> NodeMap;
 
-  /** transitive closure to record equivalence/subterm relation.  */
-  // TransitiveClosureNode d_cycle_check;
-  /** has seen cycle */
-  context::CDO<bool> d_hasSeenCycle;
   /** inferences */
   NodeList d_infer;
   NodeList d_infer_exp;
@@ -179,12 +175,19 @@ private:
   /** selector apps for eqch equivalence class */
   NodeIntMap d_selector_apps;
   std::map< Node, std::vector< Node > > d_selector_apps_data;
-  /** constructor terms */
-  //BoolMap d_consEqc;
   /** Are we in conflict */
   context::CDO<bool> d_conflict;
-  /** Added lemma ? */
+  /** added lemma
+   *
+   * This flag is set to true during a full effort check if this theory
+   * called d_out->lemma(...).
+   */
   bool d_addedLemma;
+  /** 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;
   /** The conflict node */
   Node d_conflictNode;
diff --git a/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp
index 83098e3ba..3cf605238 100644
--- a/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp
+++ b/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp
@@ -57,7 +57,7 @@ class CegInstantiatorBvInverterQuery : public BvInverterQuery
 };
 
 BvInstantiator::BvInstantiator(QuantifiersEngine* qe, TypeNode tn)
-    : Instantiator(qe, tn)
+    : Instantiator(qe, tn), d_inst_id_counter(0)
 {
   // get the global inverter utility
   // this must be global since we need to:
diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cbqi.cpp b/src/theory/quantifiers/cegqi/inst_strategy_cbqi.cpp
index c281e81ca..ac76ee31f 100644
--- a/src/theory/quantifiers/cegqi/inst_strategy_cbqi.cpp
+++ b/src/theory/quantifiers/cegqi/inst_strategy_cbqi.cpp
@@ -38,11 +38,14 @@ using namespace CVC4::theory::arith;
 
 #define ARITH_INSTANTIATOR_USE_MINUS_DELTA
 
-InstStrategyCbqi::InstStrategyCbqi( QuantifiersEngine * qe )
-  : QuantifiersModule( qe ), d_added_cbqi_lemma( qe->getUserContext() ), 
-d_elim_quants( qe->getSatContext() ),
-d_nested_qe_waitlist_size( qe->getUserContext() ),
-d_nested_qe_waitlist_proc( qe->getUserContext() )
+InstStrategyCbqi::InstStrategyCbqi(QuantifiersEngine* qe)
+    : QuantifiersModule(qe),
+      d_cbqi_set_quant_inactive(false),
+      d_incomplete_check(false),
+      d_added_cbqi_lemma(qe->getUserContext()),
+      d_elim_quants(qe->getSatContext()),
+      d_nested_qe_waitlist_size(qe->getUserContext()),
+      d_nested_qe_waitlist_proc(qe->getUserContext())
 //, d_added_inst( qe->getUserContext() )
 {
   d_qid_count = 0;
diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cbqi.h b/src/theory/quantifiers/cegqi/inst_strategy_cbqi.h
index 236904ef2..4334652da 100644
--- a/src/theory/quantifiers/cegqi/inst_strategy_cbqi.h
+++ b/src/theory/quantifiers/cegqi/inst_strategy_cbqi.h
@@ -37,7 +37,18 @@ class InstStrategyCbqi : public QuantifiersModule {
   typedef context::CDHashMap< Node, int, NodeHashFunction> NodeIntMap;
 
  protected:
+  /** set quantified formula inactive
+   *
+   * This flag is set to true during a full effort check if at least one
+   * quantified formula is set "inactive", that is, its negation is
+   * unsatisfiable in the current context.
+   */
   bool d_cbqi_set_quant_inactive;
+  /** incomplete check
+   *
+   * This is set to true during a full effort check if this strategy could
+   * not find an instantiation for at least one asserted quantified formula.
+   */
   bool d_incomplete_check;
   /** whether we have added cbqi lemma */
   NodeSet d_added_cbqi_lemma;
diff --git a/src/theory/quantifiers/conjecture_generator.cpp b/src/theory/quantifiers/conjecture_generator.cpp
index e82ab617a..a1c132fda 100644
--- a/src/theory/quantifiers/conjecture_generator.cpp
+++ b/src/theory/quantifiers/conjecture_generator.cpp
@@ -80,16 +80,18 @@ void OpArgIndex::getGroundTerms( ConjectureGenerator * s, std::vector< TNode >&
   }
 }
 
-
-
-ConjectureGenerator::ConjectureGenerator( QuantifiersEngine * qe, context::Context* c ) : QuantifiersModule( qe ),
-d_notify( *this ),
-d_uequalityEngine(d_notify, c, "ConjectureGenerator::ee", false),
-d_ee_conjectures( c ){
-  d_fullEffortCount = 0;
-  d_conj_count = 0;
-  d_subs_confirmCount = 0;
-  d_subs_unkCount = 0;
+ConjectureGenerator::ConjectureGenerator(QuantifiersEngine* qe,
+                                         context::Context* c)
+    : QuantifiersModule(qe),
+      d_notify(*this),
+      d_uequalityEngine(d_notify, c, "ConjectureGenerator::ee", false),
+      d_ee_conjectures(c),
+      d_conj_count(0),
+      d_subs_confirmCount(0),
+      d_subs_unkCount(0),
+      d_fullEffortCount(0),
+      d_hasAddedLemma(false)
+{
   d_uequalityEngine.addFunctionKind( kind::APPLY_UF );
   d_uequalityEngine.addFunctionKind( kind::APPLY_CONSTRUCTOR );
 
diff --git a/src/theory/quantifiers/conjecture_generator.h b/src/theory/quantifiers/conjecture_generator.h
index 6d626038d..a3a0b8795 100644
--- a/src/theory/quantifiers/conjecture_generator.h
+++ b/src/theory/quantifiers/conjecture_generator.h
@@ -70,10 +70,19 @@ class TermGenEnv;
 
 class TermGenerator
 {
-private:
+ private:
   unsigned calculateGeneralizationDepth( TermGenEnv * s, std::map< TypeNode, std::vector< int > >& fvs );
-public:
-  TermGenerator(){}
+
+ public:
+  TermGenerator()
+      : d_id(0),
+        d_status(0),
+        d_status_num(0),
+        d_match_status(0),
+        d_match_status_child_num(0),
+        d_match_mode(0)
+  {
+  }
   TypeNode d_typ;
   unsigned d_id;
   //1 : consider as unique variable
diff --git a/src/theory/quantifiers/ematching/candidate_generator.cpp b/src/theory/quantifiers/ematching/candidate_generator.cpp
index 4208b11ae..6ea6e50b3 100644
--- a/src/theory/quantifiers/ematching/candidate_generator.cpp
+++ b/src/theory/quantifiers/ematching/candidate_generator.cpp
@@ -33,8 +33,9 @@ bool CandidateGenerator::isLegalCandidate( Node n ){
   return d_qe->getTermDatabase()->isTermActive( n ) && ( !options::cbqi() || !quantifiers::TermUtil::hasInstConstAttr(n) );
 }
 
-CandidateGeneratorQE::CandidateGeneratorQE( QuantifiersEngine* qe, Node pat ) :
-CandidateGenerator( qe ), d_term_iter( -1 ){
+CandidateGeneratorQE::CandidateGeneratorQE(QuantifiersEngine* qe, Node pat)
+    : CandidateGenerator(qe), d_term_iter(-1), d_term_iter_limit(0)
+{
   d_op = qe->getTermDatabase()->getMatchOperator( pat );
   Assert( !d_op.isNull() );
 }
diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp
index a8079f775..1e3116f43 100644
--- a/src/theory/quantifiers/first_order_model.cpp
+++ b/src/theory/quantifiers/first_order_model.cpp
@@ -572,10 +572,6 @@ void FirstOrderModelIG::resetEvaluate(){
   d_eval_uf_use_default.clear();
   d_eval_uf_model.clear();
   d_eval_term_index_order.clear();
-  d_eval_formulas = 0;
-  d_eval_uf_terms = 0;
-  d_eval_lits = 0;
-  d_eval_lits_unknown = 0;
 }
 
 //if evaluate( n ) = eVal,
@@ -585,7 +581,6 @@ void FirstOrderModelIG::resetEvaluate(){
 // if eVal is not 0, then
 //   each n{ri->d_index[0]/x_0...ri->d_index[depIndex]/x_depIndex, */x_(depIndex+1) ... */x_n } is equivalent in the current model
 int FirstOrderModelIG::evaluate( Node n, int& depIndex, RepSetIterator* ri ){
-  ++d_eval_formulas;
   Debug("fmf-eval-debug2") << "Evaluate " << n << std::endl;
   //Notice() << "Eval " << n << std::endl;
   if( n.getKind()==NOT ){
@@ -661,7 +656,6 @@ int FirstOrderModelIG::evaluate( Node n, int& depIndex, RepSetIterator* ri ){
   }else if( n.getKind()==FORALL ){
     return 0;
   }else{
-    ++d_eval_lits;
     //Debug("fmf-eval-debug") << "Evaluate literal " << n << std::endl;
     int retVal = 0;
     depIndex = ri->getNumTerms()-1;
@@ -684,7 +678,6 @@ int FirstOrderModelIG::evaluate( Node n, int& depIndex, RepSetIterator* ri ){
     if( retVal!=0 ){
       Debug("fmf-eval-debug") << "Evaluate literal: return " << retVal << ", depIndex = " << depIndex << std::endl;
     }else{
-      ++d_eval_lits_unknown;
       Trace("fmf-eval-amb") << "Neither true nor false : " << n << std::endl;
       Trace("fmf-eval-amb") << "   value : " << val << std::endl;
     }
@@ -731,7 +724,6 @@ Node FirstOrderModelIG::evaluateTerm( Node n, int& depIndex, RepSetIterator* ri
         //Debug("fmf-eval-debug") << "Evaluate term " << n << " (" << gn << ")" << std::endl;
         //if it is a defined UF, then consult the interpretation
         if( d_uf_model_tree.find( op )!=d_uf_model_tree.end() ){
-          ++d_eval_uf_terms;
           int argDepIndex = 0;
           //make the term model specifically for n
           makeEvalUfModel( n );
diff --git a/src/theory/quantifiers/first_order_model.h b/src/theory/quantifiers/first_order_model.h
index 059250f8d..7da5b2088 100644
--- a/src/theory/quantifiers/first_order_model.h
+++ b/src/theory/quantifiers/first_order_model.h
@@ -266,12 +266,6 @@ public:
   /** evaluate functions */
   int evaluate( Node n, int& depIndex, RepSetIterator* ri  );
   Node evaluateTerm( Node n, int& depIndex, RepSetIterator* ri  );
-public:
-  //statistics
-  int d_eval_formulas;
-  int d_eval_uf_terms;
-  int d_eval_lits;
-  int d_eval_lits_unknown;
 private:
   //default evaluate term function
   Node evaluateTermDefault( Node n, int& depIndex, std::vector< int >& childDepIndex, RepSetIterator* ri  );
diff --git a/src/theory/quantifiers/fmf/model_builder.cpp b/src/theory/quantifiers/fmf/model_builder.cpp
index d1b7eebb8..c03fc7a32 100644
--- a/src/theory/quantifiers/fmf/model_builder.cpp
+++ b/src/theory/quantifiers/fmf/model_builder.cpp
@@ -457,24 +457,17 @@ bool QModelBuilderIG::hasConstantDefinition( Node n ){
   return false;
 }
 
-QModelBuilderIG::Statistics::Statistics():
-  d_num_quants_init("QModelBuilderIG::Number_Quantifiers", 0),
-  d_num_partial_quants_init("QModelBuilderIG::Number_Partial_Quantifiers", 0),
-  d_init_inst_gen_lemmas("QModelBuilderIG::Initialize_Inst_Gen_Lemmas", 0 ),
-  d_inst_gen_lemmas("QModelBuilderIG::Inst_Gen_Lemmas", 0 ),
-  d_eval_formulas("QModelBuilderIG::Eval_Formulas", 0 ),
-  d_eval_uf_terms("QModelBuilderIG::Eval_Uf_Terms", 0 ),
-  d_eval_lits("QModelBuilderIG::Eval_Lits", 0 ),
-  d_eval_lits_unknown("QModelBuilderIG::Eval_Lits_Unknown", 0 )
+QModelBuilderIG::Statistics::Statistics()
+    : d_num_quants_init("QModelBuilderIG::Number_Quantifiers", 0),
+      d_num_partial_quants_init("QModelBuilderIG::Number_Partial_Quantifiers",
+                                0),
+      d_init_inst_gen_lemmas("QModelBuilderIG::Initialize_Inst_Gen_Lemmas", 0),
+      d_inst_gen_lemmas("QModelBuilderIG::Inst_Gen_Lemmas", 0)
 {
   smtStatisticsRegistry()->registerStat(&d_num_quants_init);
   smtStatisticsRegistry()->registerStat(&d_num_partial_quants_init);
   smtStatisticsRegistry()->registerStat(&d_init_inst_gen_lemmas);
   smtStatisticsRegistry()->registerStat(&d_inst_gen_lemmas);
-  smtStatisticsRegistry()->registerStat(&d_eval_formulas);
-  smtStatisticsRegistry()->registerStat(&d_eval_uf_terms);
-  smtStatisticsRegistry()->registerStat(&d_eval_lits);
-  smtStatisticsRegistry()->registerStat(&d_eval_lits_unknown);
 }
 
 QModelBuilderIG::Statistics::~Statistics(){
@@ -482,10 +475,6 @@ QModelBuilderIG::Statistics::~Statistics(){
   smtStatisticsRegistry()->unregisterStat(&d_num_partial_quants_init);
   smtStatisticsRegistry()->unregisterStat(&d_init_inst_gen_lemmas);
   smtStatisticsRegistry()->unregisterStat(&d_inst_gen_lemmas);
-  smtStatisticsRegistry()->unregisterStat(&d_eval_formulas);
-  smtStatisticsRegistry()->unregisterStat(&d_eval_uf_terms);
-  smtStatisticsRegistry()->unregisterStat(&d_eval_lits);
-  smtStatisticsRegistry()->unregisterStat(&d_eval_lits_unknown);
 }
 
 //do exhaustive instantiation
@@ -558,12 +547,6 @@ int QModelBuilderIG::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, in
         }
       }
       //print debugging information
-      if( fmig ){
-        d_statistics.d_eval_formulas += fmig->d_eval_formulas;
-        d_statistics.d_eval_uf_terms += fmig->d_eval_uf_terms;
-        d_statistics.d_eval_lits += fmig->d_eval_lits;
-        d_statistics.d_eval_lits_unknown += fmig->d_eval_lits_unknown;
-      }
       Trace("inst-fmf-ei") << "For " << f << ", finished: " << std::endl;
       Trace("inst-fmf-ei") << "   Inst Tried: " << d_triedLemmas << std::endl;
       Trace("inst-fmf-ei") << "   Inst Added: " << d_addedLemmas << std::endl;
diff --git a/src/theory/quantifiers/fmf/model_builder.h b/src/theory/quantifiers/fmf/model_builder.h
index 353883a20..b34f1e580 100644
--- a/src/theory/quantifiers/fmf/model_builder.h
+++ b/src/theory/quantifiers/fmf/model_builder.h
@@ -148,10 +148,6 @@ class QModelBuilderIG : public QModelBuilder
     IntStat d_num_partial_quants_init;
     IntStat d_init_inst_gen_lemmas;
     IntStat d_inst_gen_lemmas;
-    IntStat d_eval_formulas;
-    IntStat d_eval_uf_terms;
-    IntStat d_eval_lits;
-    IntStat d_eval_lits_unknown;
     Statistics();
     ~Statistics();
   };
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 */