diff options
Diffstat (limited to 'src/theory/bv/slicer.cpp')
-rw-r--r-- | src/theory/bv/slicer.cpp | 15 |
1 files changed, 14 insertions, 1 deletions
diff --git a/src/theory/bv/slicer.cpp b/src/theory/bv/slicer.cpp index 2334ed2b0..ac668ab20 100644 --- a/src/theory/bv/slicer.cpp +++ b/src/theory/bv/slicer.cpp @@ -48,6 +48,14 @@ void Base::sliceAt(Index index) { d_repr[vector_index] = d_repr[vector_index] | bit_mask; } +void Base::undoSliceAt(Index index) { + Index vector_index = index / 32; + Assert (vector_index < d_size); + Index int_index = index % 32; + uint32_t bit_mask = utils::pow2(int_index); + d_repr[vector_index] = d_repr[vector_index] ^ bit_mask; +} + void Base::sliceWith(const Base& other) { Assert (d_size == other.d_size); for (unsigned i = 0; i < d_repr.size(); ++i) { @@ -245,8 +253,9 @@ void UnionFind::split(TermId id, Index i) { if (i == 0 || i == getBitwidth(id)) { // nothing to do - return; + return; } + Assert (i < getBitwidth(id)); if (!hasChildren(id)) { // first time we split this term @@ -417,6 +426,7 @@ void UnionFind::ensureSlicing(const ExtractTerm& term) { } void UnionFind::backtrack() { + return; int size = d_undoStack.size(); for (int i = size; i > d_undoStackIndex.get(); --i) { Operation op = d_undoStack.back(); @@ -443,6 +453,9 @@ void UnionFind::undoSplit(TermId id) { } void UnionFind::recordOperation(OperationKind op, TermId term) { + if (op == SPLIT) { + d_newSplit = true; + } d_undoStackIndex.set(d_undoStackIndex.get() + 1); d_undoStack.push_back(Operation(op, term)); Assert (d_undoStack.size() == d_undoStackIndex); |