diff options
| author | Liana Hadarean <lianahady@gmail.com> | 2013-01-10 14:30:23 -0500 |
|---|---|---|
| committer | Liana Hadarean <lianahady@gmail.com> | 2013-01-10 14:30:23 -0500 |
| commit | 590e7f438dacbee1c349f431316e918de43e5a8e (patch) | |
| tree | a929137ade5daf8bee54882ca9800801f7ebd66c /src/theory/bv/slicer.h | |
| parent | 9d4f5a26492a377e9b818cdfbbeb8fb5ef5b310b (diff) | |
minor bug fixes
Diffstat (limited to 'src/theory/bv/slicer.h')
| -rw-r--r-- | src/theory/bv/slicer.h | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/src/theory/bv/slicer.h b/src/theory/bv/slicer.h index cb4636fef..fa9b65ce1 100644 --- a/src/theory/bv/slicer.h +++ b/src/theory/bv/slicer.h @@ -303,7 +303,7 @@ typedef std::vector<Splinter*> Splinters; typedef std::vector<SliceBlock*> SliceBlocks; class Slicer { - std::vector<TNode> d_simpleEqualities; /**< equalities of the form a[i0:j0] = b[i1:j1] */ + std::vector<Node> d_simpleEqualities; /**< equalities of the form a[i0:j0] = b[i1:j1] */ Roots d_roots; uint32_t d_numRoots; NodeRootIdMap d_nodeRootMap; @@ -323,9 +323,10 @@ public: */ void processEquality(TNode node); bool isCoreTerm(TNode node); + static void splitEqualities(TNode node, std::vector<Node>& equalities); private: void registerSimpleEquality(TNode node); - void splitEqualities(TNode node, std::vector<Node>& equalities); + TNode addSimpleTerm(TNode t); bool isRootTerm(TNode node); |