summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/theory/bv/slicer.cpp73
-rw-r--r--src/theory/bv/slicer.h5
-rw-r--r--src/theory/bv/theory_bv.cpp7
3 files changed, 32 insertions, 53 deletions
diff --git a/src/theory/bv/slicer.cpp b/src/theory/bv/slicer.cpp
index 51775f72a..e49976572 100644
--- a/src/theory/bv/slicer.cpp
+++ b/src/theory/bv/slicer.cpp
@@ -29,6 +29,7 @@ using namespace std;
void Base::decomposeNode(TNode node, std::vector<Node>& decomp) {
Debug("bv-slicer") << "Base::decomposeNode " << node << "\n with base" << debugPrint() << endl;
+
Index low = 0;
Index high = utils::getSize(node) - 1;
if (node.getKind() == kind::BITVECTOR_EXTRACT) {
@@ -237,7 +238,7 @@ void Slicer::splitEqualities(TNode node, std::vector<Node>& equalities) {
if (base1 != Base(width)) {
// we split the equalities according to the base
int last = 0;
- for (unsigned i = 1; i < utils::getSize(t1); ++i) {
+ for (unsigned i = 0; i < utils::getSize(t1); ++i) {
if (base1.isCutPoint(i)) {
Node extract1 = Rewriter::rewrite(utils::mkExtract(t1, i, last));
Node extract2 = Rewriter::rewrite(utils::mkExtract(t2, i, last));
@@ -255,13 +256,13 @@ void Slicer::splitEqualities(TNode node, std::vector<Node>& equalities) {
void Slicer::processEquality(TNode node) {
Assert (node.getKind() == kind::EQUAL);
Debug("bv-slicer") << "theory::bv::Slicer::processEquality " << node << endl;
- std::vector<Node> equalities;
- splitEqualities(node, equalities);
- for (unsigned i = 0; i < equalities.size(); ++i) {
- Debug("bv-slicer") << " splitEqualities " << node << endl;
- registerSimpleEquality(equalities[i]);
- d_simpleEqualities.push_back(equalities[i]);
- }
+ // std::vector<Node> equalities;
+ // splitEqualities(node, equalities);
+ // for (unsigned i = 0; i < equalities.size(); ++i) {
+ // Debug("bv-slicer") << " splitEqualities " << node << endl;
+ registerSimpleEquality(node);
+ d_simpleEqualities.push_back(node);
+ // }
}
void Slicer::registerSimpleEquality(TNode eq) {
@@ -269,7 +270,10 @@ void Slicer::registerSimpleEquality(TNode eq) {
Debug("bv-slicer") << "theory::bv::Slicer::registerSimpleEquality " << eq << endl;
TNode a = eq[0];
TNode b = eq[1];
-
+
+ if (a == b)
+ return;
+
RootId id_a = registerTerm(a);
RootId id_b = registerTerm(b);
@@ -284,7 +288,7 @@ void Slicer::registerSimpleEquality(TNode eq) {
low_b = utils::getExtractLow(b);
}
- if (id_a == id_b) {
+ if (id_a == id_b ) {
// we are in the special case a[i0:j0] = a[i1:j1]
Index high_a = utils::getExtractHigh(a);
Index high_b = utils::getExtractHigh(b);
@@ -446,50 +450,17 @@ void Slicer::computeCoarsestBase() {
debugCheckBase();
}
-void Slicer::getExtractOverBase(TNode node, std::vector<Node>& decomp) {
+// void Slicer::getExtractOverBase(TNode node, std::vector<Node>& decomp) {
-}
+// }
+
void Slicer::getBaseDecomposition(TNode node, std::vector<Node>& decomp) {
- if (node.getKind() == kind::BITVECTOR_CONCAT) {
- for (unsigned i = 0; i < node.getNumChildren(); ++i) {
- TNode root = node[i].getKind() == kind::BITVECTOR_EXTRACT ? node[i][0] : node[i];
- Assert (isRootTerm(root));
- Base base = getSliceBlock(getRootId(root))->getBase();
- std::vector<Node> decomp_i;
- base.decomposeNode(node[i], decomp_i);
- // TODO: add check for extract and finish this code here
-
- if (node[i].getKind() == kind::BITVECTOR_EXTRACT) {
- unsigned low = utils::getExtractLow(node[i]);
- unsigned high = utils::getExtractHigh(node[i]);
- unsigned size = 0;
- bool add = false;
- for (int i = decomp_i.size() - 1; i >= 0; --i) {
- int size_i = utils::getSize(decomp_i[i]);
- if (low > size + size_i - 1 && !add) {
- add = true;
- Node first = utils::mkExtract(decomp_i[i], size + size_i -1, low - size);
- decomp.push_back(first);
- }
- if (high < size + size_i - 1 && add) {
- add = false;
- Node last = utils::mkExtract(decomp_i[i], size + size_i - 1, high - size);
- decomp.push_back(last);
- }
- if(add) {
- decomp.push_back(decomp_i[i]);
- }
- size += size_i;
- }
- }
- }
- } else {
- TNode root = node.getKind() == kind::BITVECTOR_EXTRACT ? node[0] : node;
- Assert (isRootTerm(root));
- Base base = getSliceBlock(getRootId(root))->getBase();
- base.decomposeNode(node, decomp);
- }
+ Assert (node.getKind() != kind::BITVECTOR_CONCAT);
+ TNode root = node.getKind() == kind::BITVECTOR_EXTRACT ? node[0] : node;
+ Assert (isRootTerm(root));
+ Base base = getSliceBlock(getRootId(root))->getBase();
+ base.decomposeNode(node, decomp);
}
void Slicer::debugCheckBase() {
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);
diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index d537b8e60..bb16e00ce 100644
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -210,6 +210,13 @@ Node TheoryBV::ppRewrite(TNode t)
Node result = RewriteRule<BitwiseEq>::run<false>(t);
return Rewriter::rewrite(result);
}
+
+ if (t.getKind() == kind::EQUAL) {
+ std::vector<Node> equalities;
+ Slicer::splitEqualities(t, equalities);
+ return utils::mkAnd(equalities);
+ }
+
return t;
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback