diff options
author | lianah <lianahady@gmail.com> | 2013-02-01 19:27:45 -0500 |
---|---|---|
committer | lianah <lianahady@gmail.com> | 2013-02-01 19:27:45 -0500 |
commit | f0988a89ecc0e5f2995dc8d390b5e9df2fa5421f (patch) | |
tree | 3b2bc8cfbe0ffc731239447e6d120c6c0f78f71d /src/theory/bv/slicer.h | |
parent | 48b19765d2f3ff6b8a5e24187a87512940d74e56 (diff) |
minor changes.
Diffstat (limited to 'src/theory/bv/slicer.h')
-rw-r--r-- | src/theory/bv/slicer.h | 10 |
1 files changed, 7 insertions, 3 deletions
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; }; |