Revert "Merging proof branch"

This reverts commit 89ba584531115b7f6d47088d7614368ea05ab9d8.

1 files changed, 176 insertions, 176 deletions

diff --git a/src/theory/bv/abstraction.cpp b/src/theory/bv/abstraction.cpp
index dc5520411..fdc36ce72 100644
--- a/src/theory/bv/abstraction.cpp
+++ b/src/theory/bv/abstraction.cpp
@@ -41,7 +41,7 @@ bool AbstractionModule::applyAbstraction(const std::vector<Node>& assertions, st
           continue;
         }
         Node signature = computeSignature(assertions[i][j]);
-        storeSignature(signature, assertions[i][j]);
+        storeSignature(signature, assertions[i][j]); 
         Debug("bv-abstraction") << "   assertion: " << assertions[i][j] <<"\n";
         Debug("bv-abstraction") << "   signature: " << signature <<"\n";
       }
@@ -52,7 +52,7 @@ bool AbstractionModule::applyAbstraction(const std::vector<Node>& assertions, st
   for (unsigned i = 0; i < assertions.size(); ++i) {
     if (assertions[i].getKind() == kind::OR &&
         assertions[i][0].getKind() == kind::AND) {
-      std::vector<Node> new_children;
+      std::vector<Node> new_children; 
       for (unsigned j = 0; j < assertions[i].getNumChildren(); ++j) {
         if (hasSignature(assertions[i][j])) {
           new_children.push_back(abstractSignatures(assertions[i][j]));
@@ -60,10 +60,10 @@ bool AbstractionModule::applyAbstraction(const std::vector<Node>& assertions, st
           new_children.push_back(assertions[i][j]);
         }
       }
-      new_assertions.push_back(utils::mkNode(kind::OR, new_children));
+      new_assertions.push_back(utils::mkNode(kind::OR, new_children)); 
     } else {
       // assertions that are not changed
-      new_assertions.push_back(assertions[i]);
+      new_assertions.push_back(assertions[i]); 
     }
   }
 
@@ -71,21 +71,21 @@ bool AbstractionModule::applyAbstraction(const std::vector<Node>& assertions, st
     skolemizeArguments(new_assertions);
   }
 
-
+  
   // if we are using the eager solver reverse the abstraction
   if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) {
     if (d_funcToSignature.size() == 0) {
       // we did not change anything
       return false;
     }
-    NodeNodeMap seen;
+    NodeNodeMap seen; 
     for (unsigned i = 0; i < new_assertions.size(); ++i) {
-      new_assertions[i] = reverseAbstraction(new_assertions[i], seen);
+      new_assertions[i] = reverseAbstraction(new_assertions[i], seen); 
     }
     // we undo the abstraction functions so the logic is QF_BV still
-    return true;
+    return true; 
   }
-
+  
   // return true if we have created new function symbols for the problem
   return d_funcToSignature.size() != 0;
 }
@@ -99,7 +99,7 @@ bool AbstractionModule::isConjunctionOfAtoms(TNode node) {
 bool AbstractionModule::isConjunctionOfAtomsRec(TNode node, TNodeSet& seen) {
   if (seen.find(node)!= seen.end())
     return true;
-
+  
   if (!node.getType().isBitVector()) {
     return (node.getKind() == kind::AND || utils::isBVPredicate(node));
   }
@@ -120,30 +120,30 @@ Node AbstractionModule::reverseAbstraction(Node assertion, NodeNodeMap& seen) {
 
   if (seen.find(assertion) != seen.end())
     return seen[assertion];
-
+  
   if (isAbstraction(assertion)) {
     Node interp =  getInterpretation(assertion);
     seen[assertion] = interp;
-    Assert (interp.getType() == assertion.getType());
+    Assert (interp.getType() == assertion.getType()); 
     return interp;
   }
 
   if (assertion.getNumChildren() == 0) {
     seen[assertion] = assertion;
-    return assertion;
+    return assertion; 
   }
-
+  
   NodeBuilder<> result(assertion.getKind());
   if (assertion.getMetaKind() == kind::metakind::PARAMETERIZED) {
-    result << assertion.getOperator();
+    result << assertion.getOperator(); 
   }
 
   for (unsigned i = 0; i < assertion.getNumChildren(); ++i) {
-    result << reverseAbstraction(assertion[i], seen);
+    result << reverseAbstraction(assertion[i], seen); 
   }
   Node res = result;
   seen[assertion] = res;
-  return res;
+  return res; 
 }
 
 void AbstractionModule::skolemizeArguments(std::vector<Node>& assertions) {
@@ -151,7 +151,7 @@ void AbstractionModule::skolemizeArguments(std::vector<Node>& assertions) {
     TNode assertion = assertions[i];
     if (assertion.getKind() != kind::OR)
       continue;
-
+    
     bool is_skolemizable = true;
     for (unsigned k = 0; k < assertion.getNumChildren(); ++k) {
       if (assertion[k].getKind() != kind::EQUAL ||
@@ -191,54 +191,54 @@ void AbstractionModule::skolemizeArguments(std::vector<Node>& assertions) {
       NodeBuilder<> skolem_func (kind::APPLY_UF);
       skolem_func << func;
       std::vector<Node> skolem_args;
-
+        
       for (unsigned j = 0; j < args.getArity(); ++j) {
         bool all_same = true;
         for (unsigned k = 1; k < args.getNumEntries(); ++k) {
           if ( args.getEntry(k)[j] != args.getEntry(0)[j])
-            all_same = false;
+            all_same = false; 
         }
-        Node new_arg = all_same ? (Node)args.getEntry(0)[j] : utils::mkVar(utils::getSize(args.getEntry(0)[j]));
+        Node new_arg = all_same ? (Node)args.getEntry(0)[j] : utils::mkVar(utils::getSize(args.getEntry(0)[j])); 
         skolem_args.push_back(new_arg);
-        skolem_func << new_arg;
+        skolem_func << new_arg; 
       }
+      
 
-
-      Node skolem_func_eq1 = utils::mkNode(kind::EQUAL, (Node)skolem_func, utils::mkConst(1, 1u));
-
+      Node skolem_func_eq1 = utils::mkNode(kind::EQUAL, (Node)skolem_func, utils::mkConst(1, 1u)); 
+      
       // enumerate arguments assignments
-      std::vector<Node> or_assignments;
+      std::vector<Node> or_assignments; 
       for (ArgsTableEntry::iterator it = args.begin(); it != args.end(); ++it) {
         NodeBuilder<> arg_assignment(kind::AND);
         ArgsVec& args =  *it;
         for (unsigned k = 0; k < args.size(); ++k) {
           Node eq = utils::mkNode(kind::EQUAL, args[k], skolem_args[k]);
-          arg_assignment << eq;
+          arg_assignment << eq; 
         }
         or_assignments.push_back(arg_assignment);
       }
-
+      
       Node new_func_def = utils::mkNode(kind::AND, skolem_func_eq1, utils::mkNode(kind::OR, or_assignments));
-      assertion_builder << new_func_def;
+      assertion_builder << new_func_def; 
     }
     Node new_assertion = assertion_builder;
     Debug("bv-abstraction-dbg") << "AbstractionModule::skolemizeArguments " << assertions[i] << " => \n";
-    Debug("bv-abstraction-dbg") << "    " << new_assertion;
+    Debug("bv-abstraction-dbg") << "    " << new_assertion; 
     assertions[i] = new_assertion;
   }
 }
 
 void AbstractionModule::storeSignature(Node signature, TNode assertion) {
   if(d_signatures.find(signature) == d_signatures.end()) {
-    d_signatures[signature] = 0;
+    d_signatures[signature] = 0; 
   }
-  d_signatures[signature] = d_signatures[signature] + 1;
-  d_assertionToSignature[assertion] = signature;
+  d_signatures[signature] = d_signatures[signature] + 1; 
+  d_assertionToSignature[assertion] = signature; 
 }
 
 Node AbstractionModule::computeSignature(TNode node) {
-  resetSignatureIndex();
-  NodeNodeMap cache;
+  resetSignatureIndex(); 
+  NodeNodeMap cache; 
   Node sig = computeSignatureRec(node, cache);
   return sig;
 }
@@ -247,17 +247,17 @@ Node AbstractionModule::getSignatureSkolem(TNode node) {
   Assert (node.getKind() == kind::VARIABLE);
   unsigned bitwidth = utils::getSize(node);
   if (d_signatureSkolems.find(bitwidth) == d_signatureSkolems.end()) {
-    d_signatureSkolems[bitwidth] = vector<Node>();
+    d_signatureSkolems[bitwidth] = vector<Node>(); 
   }
-
+  
   vector<Node>& skolems = d_signatureSkolems[bitwidth];
   // get the index of bv variables of this size
-  unsigned index = getBitwidthIndex(bitwidth);
+  unsigned index = getBitwidthIndex(bitwidth); 
   Assert (skolems.size() + 1 >= index );
   if (skolems.size() == index) {
     ostringstream os;
     os << "sig_" <<bitwidth <<"_" << index;
-    NodeManager* nm = NodeManager::currentNM();
+    NodeManager* nm = NodeManager::currentNM(); 
     skolems.push_back(nm->mkSkolem(os.str(), nm->mkBitVectorType(bitwidth), "skolem for computing signatures"));
   }
   ++(d_signatureIndices[bitwidth]);
@@ -268,12 +268,12 @@ unsigned AbstractionModule::getBitwidthIndex(unsigned bitwidth) {
   if (d_signatureIndices.find(bitwidth) == d_signatureIndices.end()) {
     d_signatureIndices[bitwidth] = 0;
   }
-  return d_signatureIndices[bitwidth];
+  return d_signatureIndices[bitwidth]; 
 }
 
 void AbstractionModule::resetSignatureIndex() {
   for (IndexMap::iterator it = d_signatureIndices.begin(); it != d_signatureIndices.end(); ++it) {
-    it->second = 0;
+    it->second = 0; 
   }
 }
 
@@ -282,24 +282,24 @@ bool AbstractionModule::hasSignature(Node node) {
 }
 
 Node AbstractionModule::getGeneralizedSignature(Node node) {
-  NodeNodeMap::const_iterator it = d_assertionToSignature.find(node);
+  NodeNodeMap::const_iterator it = d_assertionToSignature.find(node); 
   Assert (it != d_assertionToSignature.end());
-  Node generalized_signature = getGeneralization(it->second);
-  return generalized_signature;
+  Node generalized_signature = getGeneralization(it->second); 
+  return generalized_signature; 
 }
 
 Node AbstractionModule::computeSignatureRec(TNode node, NodeNodeMap& cache) {
   if (cache.find(node) != cache.end()) {
-    return cache.find(node)->second;
+    return cache.find(node)->second; 
   }
-
+  
   if (node.getNumChildren() == 0) {
     if (node.getKind() == kind::CONST_BITVECTOR)
       return node;
 
     Node sig = getSignatureSkolem(node);
-    cache[node] = sig;
-    return sig;
+    cache[node] = sig; 
+    return sig; 
   }
 
   NodeBuilder<> builder(node.getKind());
@@ -308,30 +308,30 @@ Node AbstractionModule::computeSignatureRec(TNode node, NodeNodeMap& cache) {
   }
   for (unsigned i = 0; i < node.getNumChildren(); ++i) {
     Node converted = computeSignatureRec(node[i], cache);
-    builder << converted;
+    builder << converted; 
   }
   Node result = builder;
   cache[node] = result;
-  return result;
+  return result; 
 }
 
-/**
+/** 
  * Returns 0, if the two are equal,
  * 1 if s is a generalization of t
  * 2 if t is a generalization of s
  * -1 if the two cannot be unified
  *
- * @param s
- * @param t
- *
- * @return
+ * @param s 
+ * @param t 
+ * 
+ * @return 
  */
 int AbstractionModule::comparePatterns(TNode s, TNode t) {
   if (s.getKind() == kind::SKOLEM &&
       t.getKind() == kind::SKOLEM) {
     return 0;
   }
-
+  
   if (s.getKind() == kind::CONST_BITVECTOR &&
       t.getKind() == kind::CONST_BITVECTOR) {
     if (s == t) {
@@ -350,7 +350,7 @@ int AbstractionModule::comparePatterns(TNode s, TNode t) {
       t.getKind() == kind::SKOLEM) {
     return 2;
   }
-
+  
   if (s.getNumChildren() != t.getNumChildren() ||
       s.getKind() != t.getKind())
     return -1;
@@ -370,26 +370,26 @@ int AbstractionModule::comparePatterns(TNode s, TNode t) {
 }
 
 TNode AbstractionModule::getGeneralization(TNode term) {
-  NodeNodeMap::iterator it = d_sigToGeneralization.find(term);
+  NodeNodeMap::iterator it = d_sigToGeneralization.find(term); 
   // if not in the map we add it
   if (it == d_sigToGeneralization.end()) {
     d_sigToGeneralization[term] = term;
-    return term;
+    return term; 
   }
-  // doesn't have a generalization
+  // doesn't have a generalization 
   if (it->second == term)
     return term;
-
+  
   TNode generalization = getGeneralization(it->second);
   Assert (generalization != term);
   d_sigToGeneralization[term] = generalization;
-  return generalization;
+  return generalization; 
 }
 
 void AbstractionModule::storeGeneralization(TNode s, TNode t) {
   Assert (s == getGeneralization(s));
   Assert (t == getGeneralization(t));
-  d_sigToGeneralization[s] = t;
+  d_sigToGeneralization[s] = t; 
 }
 
 void AbstractionModule::finalizeSignatures() {
@@ -402,29 +402,29 @@ void AbstractionModule::finalizeSignatures() {
     for (SignatureMap::const_iterator tt = ss; tt != d_signatures.end(); ++tt) {
       TNode t = getGeneralization(tt->first);
       TNode s = getGeneralization(ss->first);
-
+      
       if (t != s) {
         int status = comparePatterns(s, t);
-        Assert (status);
+        Assert (status); 
         if (status < 0)
           continue;
         if (status == 1) {
-          storeGeneralization(t, s);
+          storeGeneralization(t, s); 
         } else {
-          storeGeneralization(s, t);
+          storeGeneralization(s, t); 
         }
       }
     }
   }
   // keep only most general signatures
   for (SignatureMap::iterator it = d_signatures.begin(); it != d_signatures.end(); ) {
-    TNode sig = it->first;
+    TNode sig = it->first; 
     TNode gen = getGeneralization(sig);
     if (sig != gen) {
-      Assert (d_signatures.find(gen) != d_signatures.end());
+      Assert (d_signatures.find(gen) != d_signatures.end()); 
       // update the count
       d_signatures[gen]+= d_signatures[sig];
-      d_signatures.erase(it++);
+      d_signatures.erase(it++); 
     } else {
       ++it;
     }
@@ -434,12 +434,12 @@ void AbstractionModule::finalizeSignatures() {
   // remove signatures that are not frequent enough
   for (SignatureMap::iterator it = d_signatures.begin(); it != d_signatures.end(); ) {
     if (it->second <= 7) {
-      d_signatures.erase(it++);
+      d_signatures.erase(it++); 
     } else {
       ++it;
     }
   }
-
+  
   for (SignatureMap::const_iterator it = d_signatures.begin(); it != d_signatures.end(); ++it) {
     TNode signature = it->first;
     // we already processed this signature
@@ -451,31 +451,31 @@ void AbstractionModule::finalizeSignatures() {
     collectArgumentTypes(signature, arg_types, seen);
     Assert (signature.getType().isBoolean());
     // make function return a bitvector of size 1
-    //Node bv_function = utils::mkNode(kind::ITE, signature, utils::mkConst(1, 1u), utils::mkConst(1, 0u));
+    //Node bv_function = utils::mkNode(kind::ITE, signature, utils::mkConst(1, 1u), utils::mkConst(1, 0u)); 
     TypeNode range = NodeManager::currentNM()->mkBitVectorType(1);
-
+    
     TypeNode abs_type = nm->mkFunctionType(arg_types, range);
     Node abs_func = nm->mkSkolem("abs_$$", abs_type, "abstraction function for bv theory");
     Debug("bv-abstraction") << " abstracted by function " << abs_func << "\n";
 
     // NOTE: signature expression type is BOOLEAN
     d_signatureToFunc[signature] = abs_func;
-    d_funcToSignature[abs_func] = signature;
+    d_funcToSignature[abs_func] = signature; 
   }
 
   d_statistics.d_numFunctionsAbstracted.setData(d_signatureToFunc.size());
-
+  
   Debug("bv-abstraction") << "AbstractionModule::finalizeSignatures abstracted " << d_signatureToFunc.size() << " signatures. \n";
 }
 
 void AbstractionModule::collectArgumentTypes(TNode sig, std::vector<TypeNode>& types, TNodeSet& seen) {
   if (seen.find(sig) != seen.end())
     return;
-
+  
   if (sig.getKind() == kind::SKOLEM) {
     types.push_back(sig.getType());
-    seen.insert(sig);
-    return;
+    seen.insert(sig); 
+    return; 
   }
 
   for (unsigned i = 0; i < sig.getNumChildren(); ++i) {
@@ -487,36 +487,36 @@ void AbstractionModule::collectArgumentTypes(TNode sig, std::vector<TypeNode>& t
 void AbstractionModule::collectArguments(TNode node, TNode signature, std::vector<Node>& args, TNodeSet& seen) {
   if (seen.find(node)!= seen.end())
     return;
-
+  
   if (node.getKind() == kind::VARIABLE ||
       node.getKind() == kind::CONST_BITVECTOR) {
     // a constant in the node can either map to an argument of the abstraction
-    // or can be hard-coded and part of the abstraction
+    // or can be hard-coded and part of the abstraction 
     if (signature.getKind() == kind::SKOLEM) {
       args.push_back(node);
       seen.insert(node);
     } else {
-      Assert (signature.getKind() == kind::CONST_BITVECTOR);
+      Assert (signature.getKind() == kind::CONST_BITVECTOR); 
     }
-    //
-    return;
+    // 
+    return; 
   }
   Assert (node.getKind() == signature.getKind() &&
-          node.getNumChildren() == signature.getNumChildren());
+          node.getNumChildren() == signature.getNumChildren()); 
 
   for (unsigned i = 0; i < node.getNumChildren(); ++i) {
-    collectArguments(node[i], signature[i], args, seen);
-    seen.insert(node);
+    collectArguments(node[i], signature[i], args, seen); 
+    seen.insert(node); 
   }
 }
 
 
 Node AbstractionModule::abstractSignatures(TNode assertion) {
-  Debug("bv-abstraction") << "AbstractionModule::abstractSignatures "<< assertion <<"\n";
+  Debug("bv-abstraction") << "AbstractionModule::abstractSignatures "<< assertion <<"\n"; 
   // assume the assertion has been fully abstracted
   Node signature = getGeneralizedSignature(assertion);
-
-  Debug("bv-abstraction") << "   with sig "<< signature <<"\n";
+  
+  Debug("bv-abstraction") << "   with sig "<< signature <<"\n"; 
   NodeNodeMap::iterator it = d_signatureToFunc.find(signature);
   if (it!= d_signatureToFunc.end()) {
     std::vector<Node> args;
@@ -527,16 +527,16 @@ Node AbstractionModule::abstractSignatures(TNode assertion) {
     collectArguments(assertion, signature, args, seen);
     std::vector<TNode> real_args;
     for (unsigned i = 1; i < args.size(); ++i) {
-      real_args.push_back(args[i]);
+      real_args.push_back(args[i]); 
     }
-    d_argsTable.addEntry(func, real_args);
-    Node result = utils::mkNode(kind::EQUAL, utils::mkNode(kind::APPLY_UF, args),
+    d_argsTable.addEntry(func, real_args); 
+    Node result = utils::mkNode(kind::EQUAL, utils::mkNode(kind::APPLY_UF, args), 
                                 utils::mkConst(1, 1u));
-    Debug("bv-abstraction") << "=>   "<< result << "\n";
-    Assert (result.getType() == assertion.getType());
-    return result;
+    Debug("bv-abstraction") << "=>   "<< result << "\n"; 
+    Assert (result.getType() == assertion.getType()); 
+    return result; 
   }
-  return assertion;
+  return assertion; 
 }
 
 bool AbstractionModule::isAbstraction(TNode node) {
@@ -557,11 +557,11 @@ bool AbstractionModule::isAbstraction(TNode node) {
   if (constant != utils::mkConst(1, 1u))
     return false;
 
-  TNode func_symbol = func.getOperator();
+  TNode func_symbol = func.getOperator(); 
   if (d_funcToSignature.find(func_symbol) == d_funcToSignature.end())
     return false;
 
-  return true;
+  return true; 
 }
 
 Node AbstractionModule::getInterpretation(TNode node) {
@@ -571,51 +571,51 @@ Node AbstractionModule::getInterpretation(TNode node) {
   Assert (constant.getKind() == kind::CONST_BITVECTOR &&
           apply.getKind() == kind::APPLY_UF);
 
-  Node func = apply.getOperator();
+  Node func = apply.getOperator(); 
   Assert (d_funcToSignature.find(func) != d_funcToSignature.end());
-
+  
   Node sig = d_funcToSignature[func];
-
+  
   // substitute arguments in signature
   TNodeTNodeMap seen;
   unsigned index = 0;
   Node result = substituteArguments(sig, apply, index, seen);
-  Assert (result.getType().isBoolean());
+  Assert (result.getType().isBoolean()); 
   Assert (index == apply.getNumChildren());
   // Debug("bv-abstraction") << "AbstractionModule::getInterpretation " << node << "\n";
   // Debug("bv-abstraction") << "    => " << result << "\n";
-  return result;
+  return result; 
 }
 
 Node AbstractionModule::substituteArguments(TNode signature, TNode apply, unsigned& index, TNodeTNodeMap& seen) {
   if (seen.find(signature) != seen.end()) {
-    return seen[signature];
+    return seen[signature]; 
   }
-
+  
   if (signature.getKind() == kind::SKOLEM) {
     // return corresponding argument and increment counter
     seen[signature] = apply[index];
-    return apply[index++];
+    return apply[index++]; 
   }
 
   if (signature.getNumChildren() == 0) {
     Assert (signature.getKind() != kind::VARIABLE &&
-            signature.getKind() != kind::SKOLEM);
+            signature.getKind() != kind::SKOLEM); 
     seen[signature] = signature;
-    return signature;
+    return signature; 
   }
-
+  
   NodeBuilder<> builder(signature.getKind());
   if (signature.getMetaKind() == kind::metakind::PARAMETERIZED) {
     builder << signature.getOperator();
   }
-
+  
   for (unsigned i = 0; i < signature.getNumChildren(); ++i) {
     Node child = substituteArguments(signature[i], apply, index, seen);
-    builder << child;
+    builder << child; 
   }
 
-  Node result = builder;
+  Node result = builder; 
   seen[signature]= result;
 
   return result;
@@ -625,20 +625,20 @@ Node AbstractionModule::simplifyConflict(TNode conflict) {
   if (Dump.isOn("bv-abstraction")) {
     NodeNodeMap seen;
     Node c = reverseAbstraction(conflict, seen);
-    Dump("bv-abstraction") << PushCommand();
+    Dump("bv-abstraction") << PushCommand(); 
     Dump("bv-abstraction") << AssertCommand(c.toExpr());
     Dump("bv-abstraction") << CheckSatCommand();
-    Dump("bv-abstraction") << PopCommand();
+    Dump("bv-abstraction") << PopCommand(); 
   }
 
-  Debug("bv-abstraction-dbg") << "AbstractionModule::simplifyConflict " << conflict << "\n";
+  Debug("bv-abstraction-dbg") << "AbstractionModule::simplifyConflict " << conflict << "\n"; 
   if (conflict.getKind() != kind::AND)
-    return conflict;
+    return conflict; 
 
   std::vector<Node> conjuncts;
   for (unsigned i = 0; i < conflict.getNumChildren(); ++i)
     conjuncts.push_back(conflict[i]);
-
+  
   theory::SubstitutionMap subst(new context::Context());
   for (unsigned i = 0; i < conjuncts.size(); ++i) {
     TNode conjunct = conjuncts[i];
@@ -658,12 +658,12 @@ Node AbstractionModule::simplifyConflict(TNode conflict) {
       } else {
         continue;
       }
-
+      
       Assert (!subst.hasSubstitution(s));
       Assert (!t.isNull() &&
               !s.isNull() &&
               s!= t);
-      subst.addSubstitution(s, t);
+      subst.addSubstitution(s, t); 
 
       for (unsigned k = 0; k < conjuncts.size(); k++) {
         conjuncts[k] = subst.apply(conjuncts[k]);
@@ -671,28 +671,28 @@ Node AbstractionModule::simplifyConflict(TNode conflict) {
     }
   }
   Node new_conflict = Rewriter::rewrite(utils::mkAnd(conjuncts));
-
+  
   Debug("bv-abstraction") << "AbstractionModule::simplifyConflict conflict " << conflict <<"\n";
   Debug("bv-abstraction") << "   => " << new_conflict <<"\n";
 
   if (Dump.isOn("bv-abstraction")) {
-
+    
     NodeNodeMap seen;
     Node nc = reverseAbstraction(new_conflict, seen);
-    Dump("bv-abstraction") << PushCommand();
+    Dump("bv-abstraction") << PushCommand(); 
     Dump("bv-abstraction") << AssertCommand(nc.toExpr());
     Dump("bv-abstraction") << CheckSatCommand();
-    Dump("bv-abstraction") << PopCommand();
+    Dump("bv-abstraction") << PopCommand(); 
   }
-
-  return new_conflict;
+  
+  return new_conflict; 
 }
 
 
 void DebugPrintInstantiations(const std::vector< std::vector<ArgsVec> >& instantiations,
                               const std::vector<TNode> functions) {
   // print header
-  Debug("bv-abstraction-dbg") <<"[ ";
+  Debug("bv-abstraction-dbg") <<"[ "; 
   for (unsigned i = 0; i < functions.size(); ++i) {
     for (unsigned j = 1; j < functions[i].getNumChildren(); ++j) {
       Debug("bv-abstraction-dgb") << functions[i][j] <<" ";
@@ -706,16 +706,16 @@ void DebugPrintInstantiations(const std::vector< std::vector<ArgsVec> >& instant
     const std::vector<ArgsVec>& inst = instantiations[i];
     for (unsigned j = 0; j < inst.size(); ++j) {
       for (unsigned k = 0; k < inst[j].size(); ++k) {
-        Debug("bv-abstraction-dbg") << inst[j][k] << " ";
+        Debug("bv-abstraction-dbg") << inst[j][k] << " "; 
       }
-      Debug("bv-abstraction-dbg") << " || ";
+      Debug("bv-abstraction-dbg") << " || "; 
     }
     Debug("bv-abstraction-dbg") <<"]\n";
   }
 }
 
 void AbstractionModule::generalizeConflict(TNode conflict, std::vector<Node>& lemmas) {
-  Debug("bv-abstraction") << "AbstractionModule::generalizeConflict " << conflict << "\n";
+  Debug("bv-abstraction") << "AbstractionModule::generalizeConflict " << conflict << "\n"; 
   std::vector<TNode> functions;
 
   // collect abstract functions
@@ -737,11 +737,11 @@ void AbstractionModule::generalizeConflict(TNode conflict, std::vector<Node>& le
   // if (functions.size() >= 3) {
   //   // dump conflict
   //   NodeNodeMap seen;
-  //   Node reversed = reverseAbstraction(conflict, seen);
-  //   std::cout << "CONFLICT " << reversed << "\n";
+  //   Node reversed = reverseAbstraction(conflict, seen); 
+  //   std::cout << "CONFLICT " << reversed << "\n"; 
   // }
 
-
+  
   if (functions.size() == 0 || functions.size() > options::bvNumFunc()) {
     return;
   }
@@ -751,31 +751,31 @@ void AbstractionModule::generalizeConflict(TNode conflict, std::vector<Node>& le
   SubstitutionMap skolem_subst(new context::Context());
   SubstitutionMap reverse_skolem(new context::Context());
   makeFreshSkolems(conflict, skolem_subst, reverse_skolem);
-
+  
   Node skolemized_conflict = skolem_subst.apply(conflict);
   for (unsigned i = 0; i < functions.size(); ++i) {
     functions[i] = skolem_subst.apply(functions[i]);
   }
 
-  conflict = skolem_subst.apply(conflict);
+  conflict = skolem_subst.apply(conflict); 
 
   LemmaInstantiatior inst(functions, d_argsTable, conflict);
   std::vector<Node> new_lemmas;
-  inst.generateInstantiations(new_lemmas);
+  inst.generateInstantiations(new_lemmas); 
   for (unsigned i = 0; i < new_lemmas.size(); ++i) {
     TNode lemma = reverse_skolem.apply(new_lemmas[i]);
     if (d_addedLemmas.find(lemma) == d_addedLemmas.end()) {
       lemmas.push_back(lemma);
-      Debug("bv-abstraction-gen") << "adding lemma " << lemma << "\n";
+      Debug("bv-abstraction-gen") << "adding lemma " << lemma << "\n"; 
       storeLemma(lemma);
 
       if (Dump.isOn("bv-abstraction")) {
         NodeNodeMap seen;
         Node l = reverseAbstraction(lemma, seen);
-        Dump("bv-abstraction") << PushCommand();
+        Dump("bv-abstraction") << PushCommand(); 
         Dump("bv-abstraction") << AssertCommand(l.toExpr());
         Dump("bv-abstraction") << CheckSatCommand();
-        Dump("bv-abstraction") << PopCommand();
+        Dump("bv-abstraction") << PopCommand(); 
       }
     }
   }
@@ -787,18 +787,18 @@ int AbstractionModule::LemmaInstantiatior::next(int val, int index) {
   return -1;
 }
 
-/**
+/** 
  * Assumes the stack without top is consistent, and checks that the
  * full stack is consistent
- *
- * @param stack
- *
- * @return
+ * 
+ * @param stack 
+ * 
+ * @return 
  */
 bool AbstractionModule::LemmaInstantiatior::isConsistent(const vector<int>& stack) {
   if (stack.empty())
     return true;
-
+  
   unsigned current = stack.size() - 1;
   TNode func = d_functions[current];
   ArgsTableEntry& matches = d_argsTable.getEntry(func.getOperator());
@@ -807,12 +807,12 @@ bool AbstractionModule::LemmaInstantiatior::isConsistent(const vector<int>& stac
   for (unsigned k = 0; k < args.size(); ++k) {
     TNode s = func[k];
     TNode t = args[k];
-
+      
     TNode s0 = s;
     while (d_subst.hasSubstitution(s0)) {
       s0 = d_subst.getSubstitution(s0);
     }
-
+    
     TNode t0 = t;
     while (d_subst.hasSubstitution(t0)) {
       t0 = d_subst.getSubstitution(t0);
@@ -824,7 +824,7 @@ bool AbstractionModule::LemmaInstantiatior::isConsistent(const vector<int>& stac
       else
         continue;
     }
-
+      
     if(s0.getMetaKind() == kind::metakind::VARIABLE &&
        t0.isConst()) {
       d_subst.addSubstitution(s0, t0);
@@ -839,12 +839,12 @@ bool AbstractionModule::LemmaInstantiatior::isConsistent(const vector<int>& stac
 
     Assert (s0.getMetaKind() == kind::metakind::VARIABLE &&
             t0.getMetaKind() == kind::metakind::VARIABLE);
-
+      
     if (s0 != t0) {
       d_subst.addSubstitution(s0, t0);
     }
   }
-  return true;
+  return true; 
 }
 
 bool AbstractionModule::LemmaInstantiatior::accept(const vector<int>& stack) {
@@ -854,13 +854,13 @@ bool AbstractionModule::LemmaInstantiatior::accept(const vector<int>& stack) {
 void AbstractionModule::LemmaInstantiatior::mkLemma() {
   Node lemma = d_subst.apply(d_conflict);
   // Debug("bv-abstraction-gen") << "AbstractionModule::LemmaInstantiatior::mkLemma " << lemma <<"\n";
-  d_lemmas.push_back(lemma);
+  d_lemmas.push_back(lemma); 
 }
 
 void AbstractionModule::LemmaInstantiatior::backtrack(vector<int>& stack) {
   if (!isConsistent(stack))
     return;
-
+  
   if (accept(stack)) {
     mkLemma();
     return;
@@ -871,7 +871,7 @@ void AbstractionModule::LemmaInstantiatior::backtrack(vector<int>& stack) {
     d_ctx->push();
     stack.push_back(x);
     backtrack(stack);
-
+    
     d_ctx->pop();
     stack.pop_back();
     x = next(x, stack.size());
@@ -880,13 +880,13 @@ void AbstractionModule::LemmaInstantiatior::backtrack(vector<int>& stack) {
 
 
 void AbstractionModule::LemmaInstantiatior::generateInstantiations(std::vector<Node>& lemmas) {
-  Debug("bv-abstraction-gen") << "AbstractionModule::LemmaInstantiatior::generateInstantiations ";
+  Debug("bv-abstraction-gen") << "AbstractionModule::LemmaInstantiatior::generateInstantiations "; 
 
   std::vector<int> stack;
   backtrack(stack);
-  Assert (d_ctx->getLevel() == 0);
-  Debug("bv-abstraction-gen") << "numLemmas=" << d_lemmas.size() <<"\n";
-  lemmas.swap(d_lemmas);
+  Assert (d_ctx->getLevel() == 0); 
+  Debug("bv-abstraction-gen") << "numLemmas=" << d_lemmas.size() <<"\n"; 
+  lemmas.swap(d_lemmas); 
 }
 
 void AbstractionModule::makeFreshSkolems(TNode node, SubstitutionMap& map, SubstitutionMap& reverse_map) {
@@ -910,7 +910,7 @@ void AbstractionModule::makeFreshSkolems(TNode node, SubstitutionMap& map, Subst
 void AbstractionModule::makeFreshArgs(TNode func, std::vector<Node>& fresh_args) {
   Assert (fresh_args.size() == 0);
   Assert (func.getKind() == kind::APPLY_UF);
-  TNodeNodeMap d_map;
+  TNodeNodeMap d_map; 
   for (unsigned i = 0; i < func.getNumChildren(); ++i) {
     TNode arg = func[i];
     if (arg.isConst()) {
@@ -918,9 +918,9 @@ void AbstractionModule::makeFreshArgs(TNode func, std::vector<Node>& fresh_args)
       continue;
     }
     Assert (arg.getMetaKind() == kind::metakind::VARIABLE);
-    TNodeNodeMap::iterator it = d_map.find(arg);
+    TNodeNodeMap::iterator it = d_map.find(arg); 
     if (it != d_map.end()) {
-      fresh_args.push_back(it->second);
+      fresh_args.push_back(it->second); 
     } else {
       Node skolem = utils::mkVar(utils::getSize(arg));
       d_map[arg] = skolem;
@@ -947,7 +947,7 @@ Node AbstractionModule::tryMatching(const std::vector<Node>& ss, const std::vect
     Debug("bv-abstraction-dbg") <<"\n";
   }
 
-
+  
   SubstitutionMap subst(new context::Context());
 
   for (unsigned i = 0; i < ss.size(); ++i) {
@@ -982,10 +982,10 @@ Node AbstractionModule::tryMatching(const std::vector<Node>& ss, const std::vect
     Assert (s0 != t0);
     subst.addSubstitution(s0, t0);
   }
-
+  
   Node res = subst.apply(conflict);
-  Debug("bv-abstraction-dbg") << "  Lemma: " << res <<"\n";
-  return res;
+  Debug("bv-abstraction-dbg") << "  Lemma: " << res <<"\n"; 
+  return res; 
 }
 
 void AbstractionModule::storeLemma(TNode lemma) {
@@ -996,7 +996,7 @@ void AbstractionModule::storeLemma(TNode lemma) {
       atom = atom.getKind() == kind::NOT ? atom[0] : atom;
       Assert (atom.getKind() != kind::NOT);
       Assert (utils::isBVPredicate(atom));
-      d_lemmaAtoms.insert(atom);
+      d_lemmaAtoms.insert(atom); 
     }
   } else {
     lemma = lemma.getKind() == kind::NOT? lemma[0] : lemma;
@@ -1009,9 +1009,9 @@ void AbstractionModule::storeLemma(TNode lemma) {
 bool AbstractionModule::isLemmaAtom(TNode node) const {
   Assert (node.getType().isBoolean());
   node = node.getKind() == kind::NOT? node[0] : node;
-
+  
   return d_inputAtoms.find(node) == d_inputAtoms.end() &&
-    d_lemmaAtoms.find(node) != d_lemmaAtoms.end();
+    d_lemmaAtoms.find(node) != d_lemmaAtoms.end(); 
 }
 
 void AbstractionModule::addInputAtom(TNode atom) {
@@ -1022,31 +1022,31 @@ void AbstractionModule::addInputAtom(TNode atom) {
 
 void AbstractionModule::ArgsTableEntry::addArguments(const ArgsVec& args) {
   Assert (args.size() == d_arity);
-  d_data.push_back(args);
+  d_data.push_back(args); 
 }
 
 void AbstractionModule::ArgsTable::addEntry(TNode signature, const ArgsVec& args) {
   if (d_data.find(signature) == d_data.end()) {
-    d_data[signature] = ArgsTableEntry(args.size());
+    d_data[signature] = ArgsTableEntry(args.size()); 
   }
   ArgsTableEntry& entry = d_data[signature];
-  entry.addArguments(args);
+  entry.addArguments(args); 
 }
 
 
 bool AbstractionModule::ArgsTable::hasEntry(TNode signature) const {
-  return d_data.find(signature) != d_data.end();
+  return d_data.find(signature) != d_data.end(); 
 }
 
 AbstractionModule::ArgsTableEntry& AbstractionModule::ArgsTable::getEntry(TNode signature) {
   Assert (hasEntry(signature));
-  return d_data.find(signature)->second;
+  return d_data.find(signature)->second; 
 }
 
-AbstractionModule::Statistics::Statistics(const std::string& name)
-  : d_numFunctionsAbstracted(name + "theory::bv::AbstractioModule::NumFunctionsAbstracted", 0)
-  , d_numArgsSkolemized(name + "theory::bv::AbstractioModule::NumArgsSkolemized", 0)
-  , d_abstractionTime(name + "theory::bv::AbstractioModule::AbstractionTime")
+AbstractionModule::Statistics::Statistics()
+  : d_numFunctionsAbstracted("theory::bv::AbstractioModule::NumFunctionsAbstracted", 0)
+  , d_numArgsSkolemized("theory::bv::AbstractioModule::NumArgsSkolemized", 0)
+  , d_abstractionTime("theory::bv::AbstractioModule::AbstractionTime")
 {
   smtStatisticsRegistry()->registerStat(&d_numFunctionsAbstracted);
   smtStatisticsRegistry()->registerStat(&d_numArgsSkolemized);