diff options
author | lianah <lianahady@gmail.com> | 2013-01-29 16:45:28 -0500 |
---|---|---|
committer | lianah <lianahady@gmail.com> | 2013-01-29 16:45:28 -0500 |
commit | 012f1543af4aa65bf1d9ab9444c36c009fcfeb2b (patch) | |
tree | aa2c7dfafec08ef496e6310a19bf19a52a354e24 /src/theory/bv/slicer.h | |
parent | 5aec0f36fb2e896c24ce122a79bd70678371a249 (diff) |
fixes
Diffstat (limited to 'src/theory/bv/slicer.h')
-rw-r--r-- | src/theory/bv/slicer.h | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/src/theory/bv/slicer.h b/src/theory/bv/slicer.h index 7ab40652d..c4b3b06a1 100644 --- a/src/theory/bv/slicer.h +++ b/src/theory/bv/slicer.h @@ -89,7 +89,8 @@ struct ExtractTerm { { Assert (h >= l && id != UndefinedId); } - Index getBitwidth() const { return high - low + 1; } + Index getBitwidth() const { return high - low + 1; } + std::string debugPrint() const; }; class UnionFind; @@ -109,7 +110,8 @@ struct NormalForm { * * @return */ - TermId getTerm(Index i, const UnionFind& uf) const; + TermId getTerm(Index i, const UnionFind& uf) const; + std::string debugPrint(const UnionFind& uf) const; }; @@ -148,6 +150,7 @@ class UnionFind { d_ch1 = ch1; d_ch2 = ch2; } + std::string debugPrint() const; }; /// map from TermId to the nodes that represent them |