diff options
author | lianah <lianahady@gmail.com> | 2013-01-10 20:44:58 -0500 |
---|---|---|
committer | lianah <lianahady@gmail.com> | 2013-01-10 20:44:58 -0500 |
commit | f8c88fa4b7b9b2d59f48d0e33f1344196a06f5da (patch) | |
tree | 97ea6b2a2304d867cceebec6c9494ec1fcbd749e /src/theory/bv/slicer.h | |
parent | 590e7f438dacbee1c349f431316e918de43e5a8e (diff) |
fixed most bugs and added paranoid assertions
Diffstat (limited to 'src/theory/bv/slicer.h')
-rw-r--r-- | src/theory/bv/slicer.h | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/src/theory/bv/slicer.h b/src/theory/bv/slicer.h index fa9b65ce1..4d430258d 100644 --- a/src/theory/bv/slicer.h +++ b/src/theory/bv/slicer.h @@ -70,7 +70,7 @@ public: void decomposeNode(TNode node, std::vector<Node>& decomp); - bool isCutPoint(Index index) { + bool isCutPoint (Index index) { Assert (index < d_size); // the last cut point is implicit if (index == d_size - 1) @@ -223,7 +223,8 @@ public: std::map<Index, Splinter*>::const_iterator end() { return d_splinters.end(); } - std::string debugPrint(); + std::string debugPrint(); + bool isConsistent(); }; class Slicer; @@ -341,7 +342,7 @@ private: RootId makeRoot(TNode n); Slice* makeSlice(TNode node); - void debugCheckBase(); + bool debugCheckBase(); public: Slice* getSlice(const SplinterPointer& sp) { Assert (sp != Undefined); |