Revert "Merging proof branch"

This reverts commit 89ba584531115b7f6d47088d7614368ea05ab9d8.

1 files changed, 15 insertions, 16 deletions

diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h
index ba2a4fc2a..7f0494dc1 100644
--- a/src/theory/bv/theory_bv.h
+++ b/src/theory/bv/theory_bv.h
@@ -56,8 +56,7 @@ class TheoryBV : public Theory {
 public:
 
   TheoryBV(context::Context* c, context::UserContext* u, OutputChannel& out,
-           Valuation valuation, const LogicInfo& logicInfo,
-           std::string name = "");
+           Valuation valuation, const LogicInfo& logicInfo);
 
   ~TheoryBV();
 
@@ -89,8 +88,8 @@ public:
 
   void presolve();
 
-  bool applyAbstraction(const std::vector<Node>& assertions, std::vector<Node>& new_assertions);
-
+  bool applyAbstraction(const std::vector<Node>& assertions, std::vector<Node>& new_assertions); 
+  
   void setProofLog( BitVectorProof * bvp );
 
 private:
@@ -101,10 +100,10 @@ private:
     IntStat     d_solveSubstitutions;
     TimerStat   d_solveTimer;
     IntStat     d_numCallsToCheckFullEffort;
-    IntStat     d_numCallsToCheckStandardEffort;
+    IntStat     d_numCallsToCheckStandardEffort; 
     TimerStat   d_weightComputationTimer;
     IntStat     d_numMultSlice;
-    Statistics(const std::string &name);
+    Statistics();
     ~Statistics();
   };
 
@@ -122,12 +121,12 @@ private:
    */
   Node getBVDivByZero(Kind k, unsigned width);
 
-  typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction> TNodeSet;
+  typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction> TNodeSet; 
   void collectFunctionSymbols(TNode term, TNodeSet& seen);
   void storeFunction(TNode func, TNode term);
   typedef __gnu_cxx::hash_set<Node, NodeHashFunction> NodeSet;
   NodeSet d_staticLearnCache;
-
+  
   /**
    * Maps from bit-vector width to division-by-zero uninterpreted
    * function symbols.
@@ -143,7 +142,7 @@ private:
   CVC4::theory::SubstitutionMap d_funcToSkolem;
 
   context::CDO<bool> d_lemmasAdded;
-
+  
   // Are we in conflict?
   context::CDO<bool> d_conflict;
 
@@ -166,17 +165,17 @@ private:
   typedef context::CDHashMap<Node, SubTheory, NodeHashFunction> PropagatedMap;
   PropagatedMap d_propagatedBy;
 
-  EagerBitblastSolver* d_eagerSolver;
+  EagerBitblastSolver* d_eagerSolver; 
   AbstractionModule* d_abstractionModule;
   bool d_isCoreTheory;
   bool d_calledPreregister;
-
+  
   bool wasPropagatedBySubtheory(TNode literal) const {
-    return d_propagatedBy.find(literal) != d_propagatedBy.end();
+    return d_propagatedBy.find(literal) != d_propagatedBy.end(); 
   }
-
+  
   SubTheory getPropagatingSubtheory(TNode literal) const {
-    Assert(wasPropagatedBySubtheory(literal));
+    Assert(wasPropagatedBySubtheory(literal)); 
     PropagatedMap::const_iterator find = d_propagatedBy.find(literal);
     return (*find).second;
   }
@@ -192,7 +191,7 @@ private:
   void addSharedTerm(TNode t);
 
   bool isSharedTerm(TNode t) { return d_sharedTermsSet.contains(t); }
-
+  
   EqualityStatus getEqualityStatus(TNode a, TNode b);
 
   Node getModelValue(TNode var);
@@ -213,7 +212,7 @@ private:
 
   void lemma(TNode node) { d_out->lemma(node, RULE_CONFLICT); d_lemmasAdded = true; }
 
-  void checkForLemma(TNode node);
+  void checkForLemma(TNode node); 
 
   friend class LazyBitblaster;
   friend class TLazyBitblaster;