Deleting optional members of StrongSolverTheoryUF.

diff --git a/src/theory/uf/theory_uf_strong_solver.cpp b/src/theory/uf/theory_uf_strong_solver.cpp
index cda94e1c49c8ed69b9d02fa59b657ac239fed57f..4713c7dcfd599e15c89d62534e8a65234db322b6 100644 (file)
--- a/src/theory/uf/theory_uf_strong_solver.cpp
+++ b/src/theory/uf/theory_uf_strong_solver.cpp
@@ -1645,34 +1645,37 @@ Node SortModel::getCardinalityLiteral( int c ) {
 
 StrongSolverTheoryUF::StrongSolverTheoryUF(context::Context* c,
                                            context::UserContext* u,
-                                           OutputChannel& out,
-                                           TheoryUF* th)
-  : d_out( &out )
-  , d_th( th )
-  , d_conflict( c, false )
-  , d_rep_model()
-  , d_aloc_com_card( u, 0 )
-  , d_com_card_assertions( c )
-  , d_min_pos_com_card( c, -1 )
-  , d_card_assertions_eqv_lemma( u )
-  , d_min_pos_tn_master_card( c, -1 )
-  , d_rel_eqc( c )
-{
-  if( options::ufssDiseqPropagation() ){
-    d_deq_prop = new DisequalityPropagator( th->getQuantifiersEngine(), this );
-  }else{
-    d_deq_prop = NULL;
+                                           OutputChannel& out, TheoryUF* th)
+    : d_out(&out),
+      d_th(th),
+      d_conflict(c, false),
+      d_rep_model(),
+      d_aloc_com_card(u, 0),
+      d_com_card_assertions(c),
+      d_min_pos_com_card(c, -1),
+      d_card_assertions_eqv_lemma(u),
+      d_min_pos_tn_master_card(c, -1),
+      d_rel_eqc(c),
+      d_deq_prop(NULL),
+      d_sym_break(NULL) {
+  if (options::ufssDiseqPropagation()) {
+    d_deq_prop = new DisequalityPropagator(th->getQuantifiersEngine(), this);
+  }
+  if (options::ufssSymBreak()) {
+    d_sym_break = new SubsortSymmetryBreaker(th->getQuantifiersEngine(), c);
+  }
+}
+
+StrongSolverTheoryUF::~StrongSolverTheoryUF() {
+  for (std::map<TypeNode, SortModel*>::iterator it = d_rep_model.begin();
+       it != d_rep_model.end(); ++it) {
+    delete it->second;
   }
-  if( options::ufssSymBreak() ){
-    d_sym_break = new SubsortSymmetryBreaker( th->getQuantifiersEngine(), c );
-  }else{
-    d_sym_break = NULL;
+  if (d_sym_break) {
+    delete d_sym_break;
   }
-}
-
-StrongSolverTheoryUF::~StrongSolverTheoryUF() { 
-  for( std::map< TypeNode, SortModel* >::iterator it = d_rep_model.begin(); it != d_rep_model.end(); ++it ){
-    delete it->second;
+  if (d_deq_prop) {
+    delete d_deq_prop;
   }
 }
 

diff --git a/src/theory/uf/theory_uf_strong_solver.h b/src/theory/uf/theory_uf_strong_solver.h
index 4e4dbef830e8ebb00a3dc4b2582c410e842c7724..40026522dc687cbb9e401ebefc514202beeadfa1 100644 (file)
--- a/src/theory/uf/theory_uf_strong_solver.h
+++ b/src/theory/uf/theory_uf_strong_solver.h
@@ -365,55 +365,10 @@ public:
     /** get number of regions (for debugging) */
     int getNumRegions();
   }; /** class SortModel */
-private:
-  /** The output channel for the strong solver. */
-  OutputChannel* d_out;
-  /** theory uf pointer */
-  TheoryUF* d_th;
-  /** Are we in conflict */
-  context::CDO<bool> d_conflict;
-  /** rep model structure, one for each type */
-  std::map< TypeNode, SortModel* > d_rep_model;
-  /** get sort model */
-  SortModel* getSortModel( Node n );
-private:
-  /** allocated combined cardinality */
-  context::CDO< int > d_aloc_com_card;
-  /** combined cardinality constraints */
-  std::map< int, Node > d_com_card_literal;
-  /** combined cardinality assertions (indexed by cardinality literals ) */
-  NodeBoolMap d_com_card_assertions;
-  /** minimum positive combined cardinality */
-  context::CDO< int > d_min_pos_com_card;
-  /** cardinality literals for which we have added */
-  NodeBoolMap d_card_assertions_eqv_lemma;
-  /** the master monotone type (if ufssFairnessMonotone enabled) */
-  TypeNode d_tn_mono_master;
-  std::map< TypeNode, bool > d_tn_mono_slave;
-  context::CDO< int > d_min_pos_tn_master_card;  
-  /** initialize */
-  void initializeCombinedCardinality();
-  /** allocateCombinedCardinality */
-  void allocateCombinedCardinality();
-  /** check */
-  void checkCombinedCardinality();
-private:
-  /** relevant eqc */
-  NodeBoolMap d_rel_eqc;
-  /** ensure eqc */
-  void ensureEqc( SortModel* c, Node a );
-  /** ensure eqc for all subterms of n */
-  void ensureEqcRec( Node n );
-public:
-  /** has eqc */
-  bool hasEqc( Node a );
-private:
-  /** disequality propagator */
-  DisequalityPropagator* d_deq_prop;
-  /** symmetry breaking techniques */
-  SubsortSymmetryBreaker* d_sym_break;
+
 public:
-  StrongSolverTheoryUF(context::Context* c, context::UserContext* u, OutputChannel& out, TheoryUF* th);
+  StrongSolverTheoryUF(context::Context* c, context::UserContext* u,
+                       OutputChannel& out, TheoryUF* th);
   ~StrongSolverTheoryUF();
   /** get theory */
   TheoryUF* getTheory() { return d_th; }
@@ -437,7 +392,6 @@ public:
   void assertNode( Node n, bool isDecision );
   /** are disequal */
   bool areDisequal( Node a, Node b );
-public:
   /** check */
   void check( Theory::Effort level );
   /** presolve */
@@ -448,18 +402,14 @@ public:
   Node getNextDecisionRequest();
   /** preregister a term */
   void preRegisterTerm( TNode n );
-  /** preregister a quantifier */
-  //void registerQuantifier( Node f );
   /** notify restart */
   void notifyRestart();
-public:
   /** identify */
   std::string identify() const { return std::string("StrongSolverTheoryUF"); }
   //print debug
   void debugPrint( const char* c );
   /** debug a model */
   bool debugModel( TheoryModel* m );
-public:
   /** get is in conflict */
   bool isConflict() { return d_conflict; }
   /** get cardinality for node */
@@ -468,9 +418,11 @@ public:
   int getCardinality( TypeNode tn );
   /** minimize */
   bool minimize( TheoryModel* m = NULL );
+  /** has eqc */
+  bool hasEqc(Node a);
 
   class Statistics {
-  public:
+   public:
     IntStat d_clique_conflicts;
     IntStat d_clique_lemmas;
     IntStat d_split_lemmas;
@@ -483,7 +435,50 @@ public:
   };
   /** statistics class */
   Statistics d_statistics;
-};/* class StrongSolverTheoryUF */
+
+ private:
+  /** get sort model */
+  SortModel* getSortModel(Node n);
+  /** initialize */
+  void initializeCombinedCardinality();
+  /** allocateCombinedCardinality */
+  void allocateCombinedCardinality();
+  /** check */
+  void checkCombinedCardinality();
+  /** ensure eqc */
+  void ensureEqc(SortModel* c, Node a);
+  /** ensure eqc for all subterms of n */
+  void ensureEqcRec(Node n);
+
+  /** The output channel for the strong solver. */
+  OutputChannel* d_out;
+  /** theory uf pointer */
+  TheoryUF* d_th;
+  /** Are we in conflict */
+  context::CDO<bool> d_conflict;
+  /** rep model structure, one for each type */
+  std::map<TypeNode, SortModel*> d_rep_model;
+  /** allocated combined cardinality */
+  context::CDO<int> d_aloc_com_card;
+  /** combined cardinality constraints */
+  std::map<int, Node> d_com_card_literal;
+  /** combined cardinality assertions (indexed by cardinality literals ) */
+  NodeBoolMap d_com_card_assertions;
+  /** minimum positive combined cardinality */
+  context::CDO<int> d_min_pos_com_card;
+  /** cardinality literals for which we have added */
+  NodeBoolMap d_card_assertions_eqv_lemma;
+  /** the master monotone type (if ufssFairnessMonotone enabled) */
+  TypeNode d_tn_mono_master;
+  std::map<TypeNode, bool> d_tn_mono_slave;
+  context::CDO<int> d_min_pos_tn_master_card;
+  /** relevant eqc */
+  NodeBoolMap d_rel_eqc;
+  /** disequality propagator */
+  DisequalityPropagator* d_deq_prop;
+  /** symmetry breaking techniques */
+  SubsortSymmetryBreaker* d_sym_break;
+}; /* class StrongSolverTheoryUF */
 
 class DisequalityPropagator {
 public: