summaryrefslogtreecommitdiff
path: root/src/theory/bv/slicer.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/bv/slicer.h')
-rw-r--r--src/theory/bv/slicer.h7
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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback