From f0988a89ecc0e5f2995dc8d390b5e9df2fa5421f Mon Sep 17 00:00:00 2001
From: lianah <lianahady@gmail.com>
Date: Fri, 1 Feb 2013 19:27:45 -0500
Subject: [PATCH] minor changes.

---
 src/theory/bv/slicer.cpp | 11 ++++++++---
 src/theory/bv/slicer.h   | 10 +++++++---
 2 files changed, 15 insertions(+), 6 deletions(-)

diff --git a/src/theory/bv/slicer.cpp b/src/theory/bv/slicer.cpp
index e750070ef..55402251d 100644
--- a/src/theory/bv/slicer.cpp
+++ b/src/theory/bv/slicer.cpp
@@ -512,6 +512,7 @@ bool Slicer::isCoreTerm(TNode node) {
   }
   return d_coreTermCache[node]; 
 }
+unsigned Slicer::d_numAddedEqualities = 0; 
 
 void Slicer::splitEqualities(TNode node, std::vector<Node>& equalities) {
   Assert (node.getKind() == kind::EQUAL);
@@ -545,8 +546,8 @@ void Slicer::splitEqualities(TNode node, std::vector<Node>& equalities) {
     int last = 0; 
     for (unsigned i = 1; i <= utils::getSize(t1); ++i) {
       if (base1.isCutPoint(i)) {
-        Node extract1 = Rewriter::rewrite(utils::mkExtract(t1, i-1, last));
-        Node extract2 = Rewriter::rewrite(utils::mkExtract(t2, i-1, last));
+        Node extract1 = utils::mkExtract(t1, i-1, last);
+        Node extract2 = utils::mkExtract(t2, i-1, last);
         last = i;
         Assert (utils::getSize(extract1) == utils::getSize(extract2)); 
         equalities.push_back(utils::mkNode(kind::EQUAL, extract1, extract2)); 
@@ -556,6 +557,7 @@ void Slicer::splitEqualities(TNode node, std::vector<Node>& equalities) {
     // just return same equality
     equalities.push_back(node);
   }
+  d_numAddedEqualities += equalities.size() - 1; 
 } 
 
 std::string UnionFind::debugPrint(TermId id) {
@@ -580,12 +582,14 @@ UnionFind::Statistics::Statistics():
   d_numRepresentatives("theory::bv::slicer::NumberOfRepresentatives", 0),
   d_numSplits("theory::bv::slicer::NumberOfSplits", 0),
   d_numMerges("theory::bv::slicer::NumberOfMerges", 0),
-  d_avgFindDepth("theory::bv::slicer::AverageFindDepth")
+  d_avgFindDepth("theory::bv::slicer::AverageFindDepth"),
+  d_numAddedEqualities("theory::bv::slicer::NumberOfEqualitiesAdded", Slicer::d_numAddedEqualities)
 {
   StatisticsRegistry::registerStat(&d_numRepresentatives);
   StatisticsRegistry::registerStat(&d_numSplits);
   StatisticsRegistry::registerStat(&d_numMerges);
   StatisticsRegistry::registerStat(&d_avgFindDepth);
+  StatisticsRegistry::registerStat(&d_numAddedEqualities);
 }
 
 UnionFind::Statistics::~Statistics() {
@@ -593,4 +597,5 @@ UnionFind::Statistics::~Statistics() {
   StatisticsRegistry::unregisterStat(&d_numSplits);
   StatisticsRegistry::unregisterStat(&d_numMerges);
   StatisticsRegistry::unregisterStat(&d_avgFindDepth);
+  StatisticsRegistry::unregisterStat(&d_numAddedEqualities);
 }
diff --git a/src/theory/bv/slicer.h b/src/theory/bv/slicer.h
index c3e893239..f3b16e3d7 100644
--- a/src/theory/bv/slicer.h
+++ b/src/theory/bv/slicer.h
@@ -193,7 +193,9 @@ class UnionFind {
     IntStat d_numRepresentatives;
     IntStat d_numSplits;
     IntStat d_numMerges;
-    AverageStat d_avgFindDepth; 
+    AverageStat d_avgFindDepth;
+    ReferenceStat<unsigned> d_numAddedEqualities; 
+    //IntStat d_numAddedEqualities; 
     Statistics();
     ~Statistics();
   };
@@ -220,7 +222,8 @@ public:
     Assert (id < d_nodes.size());
     return d_nodes[id].getBitwidth(); 
   }
-  std::string debugPrint(TermId id); 
+  std::string debugPrint(TermId id);
+  friend class Slicer; 
 };
 
 class Slicer {
@@ -240,7 +243,8 @@ public:
   void getBaseDecomposition(TNode node, std::vector<Node>& decomp);
   void processEquality(TNode eq);
   bool isCoreTerm (TNode node);
-  static void splitEqualities(TNode node, std::vector<Node>& equalities); 
+  static void splitEqualities(TNode node, std::vector<Node>& equalities);
+  static unsigned d_numAddedEqualities; 
 }; 
 
 
-- 
2.30.2