diff options
| -rw-r--r-- | src/theory/bv/slicer.cpp | 11 | ||||
| -rw-r--r-- | 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; }; |