From 73b8b6c6ea8004225e99225f1e1f7666a5a49593 Mon Sep 17 00:00:00 2001 From: =?utf8?q?Dejan=20Jovanovi=C4=87?= Date: Sun, 20 Mar 2011 19:50:48 +0000 Subject: [PATCH] more bugfixes for bitvectors --- src/theory/bv/cd_set_collection.h | 94 ++++++++++- src/theory/bv/slice_manager.h | 147 +++++++++--------- src/theory/bv/theory_bv.cpp | 28 ++++ src/theory/bv/theory_bv.h | 5 +- test/regress/regress0/bv/core/Makefile.am | 5 +- test/regress/regress0/bv/core/bitvec0.smt | 24 +++ .../regress0/bv/core/ext_con_004_001_1024.smt | 26 ++++ 7 files changed, 251 insertions(+), 78 deletions(-) create mode 100644 test/regress/regress0/bv/core/bitvec0.smt create mode 100644 test/regress/regress0/bv/core/ext_con_004_001_1024.smt diff --git a/src/theory/bv/cd_set_collection.h b/src/theory/bv/cd_set_collection.h index aeb28ab7b..d020ef362 100644 --- a/src/theory/bv/cd_set_collection.h +++ b/src/theory/bv/cd_set_collection.h @@ -40,10 +40,19 @@ class BacktrackableSetCollection { /** Backtrackable number of nodes that have been inserted */ context::CDO d_nodesInserted; + /** Check if the reference is valid in the current context */ + inline bool isValid(reference_type set) const { + return d_nodesInserted == d_memory.size() && (set == null || set < d_memory.size()); + } + /** Backtrack */ void backtrack() { while (d_nodesInserted < d_memory.size()) { const tree_entry_type& node = d_memory.back(); + + Debug("cd_set_collection") << "BacktrackableSetCollection::backtrack(): removing " << node.getValue() + << " from " << internalToString(getRoot(d_memory.size()-1)) << std::endl; + if (node.hasParent()) { if (node.isLeft()) { d_memory[node.getParent()].removeLeft(); @@ -64,7 +73,7 @@ class BacktrackableSetCollection { */ reference_type newElement(const value_type& value, reference_type left, reference_type right, reference_type parent, bool isLeft) { reference_type index = d_memory.size(); - d_memory.push_back(tree_entry_type(value, left, right, value, isLeft)); + d_memory.push_back(tree_entry_type(value, left, right, parent, isLeft)); d_nodesInserted = d_nodesInserted + 1; return index; } @@ -91,6 +100,7 @@ class BacktrackableSetCollection { */ reference_type max(reference_type set) const { Assert(set != null); + Assert(isValid(set)); while (d_memory[set].hasRight()) { set = d_memory[set].getRight(); } @@ -102,12 +112,54 @@ class BacktrackableSetCollection { */ reference_type min(reference_type set) const { Assert(set != null); + Assert(isValid(set)); while (d_memory[set].hasLeft()) { set = d_memory[set].getLeft(); } return set; } + /** + * REturns the root of the tree + */ + reference_type getRoot(reference_type set) const { + // We don't check validity as this is used in backtracking + while (set != null && d_memory[set].hasParent()) { + Assert(set > d_memory[set].getParent()); + set = d_memory[set].getParent(); + } + return set; + } + + /** + * Print the list of elements to the output. + */ + void internalPrint(std::ostream& out, reference_type set) const { + if (set == null) { + return; + } + const tree_entry_type& current = d_memory[set]; + if (current.hasLeft()) { + internalPrint(out, current.getLeft()); + out << ","; + } + out << current.getValue(); + if (current.hasRight()) { + out << ","; + internalPrint(out, current.getRight()); + } + } + + /** + * String representation of a set. + */ + std::string internalToString(reference_type set) const { + std::stringstream out; + internalPrint(out, set); + return out.str(); + } + + public: BacktrackableSetCollection(context::Context* context) @@ -118,6 +170,20 @@ public: return d_memory.size(); } + size_t size(reference_type set) const { + backtrack(); + Assert(isValid(set)); + if (set == null) return 0; + size_t n = 1; + if (d_memory[set].hasLeft()) { + n += size(d_memory[set].getLeft()); + } + if (d_memory[set].hasRight()) { + n += size(d_memory[set].getRight()); + } + return n; + } + reference_type newSet(const value_type& value) { backtrack(); return newElement(value, null, null, null, false); @@ -125,6 +191,7 @@ public: void insert(reference_type& root, const value_type& value) { backtrack(); + Assert(isValid(root)); if (root == null) { root = newSet(value); return; @@ -133,20 +200,24 @@ public: reference_type parent = null; reference_type current = root; while (true) { - parent = current; + Assert(isValid(current)); if (value < d_memory[current].getValue()) { if (d_memory[current].hasLeft()) { + parent = current; current = d_memory[current].getLeft(); } else { - d_memory[current].setLeft(newElement(value, null, null, parent, true)); + d_memory[current].setLeft(newElement(value, null, null, current, true)); + Assert(d_memory[current].hasLeft()); return; } } else { - Assert(value != d_memory[root].getValue()); + Assert(value != d_memory[current].getValue()); if (d_memory[current].hasRight()) { + parent = current; current = d_memory[current].getRight(); } else { - d_memory[parent].setRight(newElement(value, null, null, parent, false)); + d_memory[current].setRight(newElement(value, null, null, current, false)); + Assert(d_memory[current].hasRight()); return; } } @@ -158,6 +229,7 @@ public: */ const_value_reference maxElement(reference_type set) const { Assert(set != null); + Assert(isValid(set)); backtrack(); return d_memory[max(set)].getValue(); } @@ -167,6 +239,7 @@ public: */ const_value_reference minElement(reference_type set) const { Assert(set != null); + Assert(isValid(set)); backtrack(); return d_memory[min(set)].getValue(); } @@ -176,6 +249,7 @@ public: */ const_value_reference prev(reference_type set, const_value_reference value) { backtrack(); + Assert(isValid(set)); const_value_reference candidate_value; bool candidate_found = false; @@ -202,6 +276,7 @@ public: const_value_reference next(reference_type set, const_value_reference value) { backtrack(); + Assert(isValid(set)); const_value_reference candidate_value; bool candidate_found = false; @@ -232,6 +307,8 @@ public: unsigned count(reference_type set, const_value_reference lowerBound, const_value_reference upperBound) const { Assert(lowerBound <= upperBound); backtrack(); + Assert(isValid(set)); + // Empty set no elements if (set == null) { return 0; @@ -260,6 +337,7 @@ public: */ bool contains(reference_type set, const_value_reference value) const { backtrack(); + Assert(isValid(set)); return count(set, value, value) > 0; } @@ -270,6 +348,7 @@ public: void getElements(reference_type set, const_value_reference lowerBound, const_value_reference upperBound, std::vector& output) const { Assert(lowerBound <= upperBound); backtrack(); + Assert(isValid(set)); Debug("set_collection") << "BacktrackableSetCollection::getElements(" << toString(set) << "," << lowerBound << "," << upperBound << ")" << std::endl; @@ -298,6 +377,8 @@ public: */ void print(std::ostream& out, reference_type set) const { backtrack(); + Assert(isValid(set)); + if (set == null) { return; } @@ -317,6 +398,9 @@ public: * String representation of a set. */ std::string toString(reference_type set) const { + backtrack(); + Assert(isValid(set)); + std::stringstream out; print(out, set); return out.str(); diff --git a/src/theory/bv/slice_manager.h b/src/theory/bv/slice_manager.h index 96a0067dc..ed516fa31 100644 --- a/src/theory/bv/slice_manager.h +++ b/src/theory/bv/slice_manager.h @@ -122,7 +122,7 @@ public: typedef context::BacktrackableSetCollection, slice_point, set_reference> set_collection; /** The map type from nodes to their references */ - typedef std::map slicing_map; + typedef context::CDMap slicing_map; /** The equality engine theory of bit-vectors is using */ typedef typename TheoryBitvector::BvEqualityEngine EqualityEngine; @@ -150,7 +150,11 @@ private: public: SliceManager(TheoryBitvector& theoryBitvector, context::Context* context) - : d_theoryBitvector(theoryBitvector), d_equalityEngine(theoryBitvector.getEqualityEngine()), d_setCollection(context) { + : d_theoryBitvector(theoryBitvector), + d_equalityEngine(theoryBitvector.getEqualityEngine()), + d_setCollection(context), + d_nodeSlicing(context) + { } /** @@ -207,68 +211,6 @@ private: inline bool addSlice(Node term, unsigned slicePoint); }; - -template -bool SliceManager::addSlice(Node node, unsigned slicePoint) { - Debug("slicing") << "SliceMagager::addSlice(" << node << "," << slicePoint << ")" << std::endl; - - bool ok = true; - - int low = node.getKind() == kind::BITVECTOR_EXTRACT ? utils::getExtractLow(node) : 0; - int high = node.getKind() == kind::BITVECTOR_EXTRACT ? utils::getExtractHigh(node) + 1: utils::getSize(node); - slicePoint += low; - - TNode nodeBase = baseTerm(node); - - set_reference sliceSet; - slicing_map::iterator find = d_nodeSlicing.find(nodeBase); - if (find == d_nodeSlicing.end()) { - sliceSet = d_nodeSlicing[nodeBase] = d_setCollection.newSet(slicePoint); - d_setCollection.insert(sliceSet, low); - d_setCollection.insert(sliceSet, high); - } else { - sliceSet = find->second; - } - - // What are the points surrounding the new slice point - int prev = d_setCollection.prev(sliceSet, slicePoint); - int next = d_setCollection.next(sliceSet, slicePoint); - - // Add the slice to the set - d_setCollection.insert(sliceSet, slicePoint); - Debug("slicing") << "SliceMagager::addSlice(" << node << "," << slicePoint << "): current set " << d_setCollection.toString(sliceSet) << std::endl; - - // Add the terms and the equality to the equality engine - Node t1 = utils::mkExtract(nodeBase, next - 1, slicePoint); - Node t2 = utils::mkExtract(nodeBase, slicePoint - 1, prev); - Node nodeSlice = (next == high && prev == low) ? node : utils::mkExtract(nodeBase, next - 1, prev); - Node concat = utils::mkConcat(t1, t2); - - d_equalityEngine.addTerm(t1); - d_equalityEngine.addTerm(t2); - d_equalityEngine.addTerm(nodeSlice); - d_equalityEngine.addTerm(concat); - - // We are free to add this slice, unless the slice has a representative that's already a concat - TNode nodeSliceRepresentative = d_equalityEngine.getRepresentative(nodeSlice); - if (nodeSliceRepresentative.getKind() != kind::BITVECTOR_CONCAT) { - // Add the slice to the equality engine - ok = d_equalityEngine.addEquality(nodeSlice, concat, utils::mkTrue()); - } else { - // If the representative is a concat, we must solve it - // There is no need do add nodeSlice = concat as we will solve the representative of nodeSlice - std::set assumptions; - std::vector equalities; - d_equalityEngine.getExplanation(nodeSlice, nodeSliceRepresentative, equalities); - assumptions.insert(equalities.begin(), equalities.end()); - ok = solveEquality(nodeSliceRepresentative, concat, assumptions); - } - - Debug("slicing") << "SliceMagager::addSlice(" << node << "," << slicePoint << ") => " << d_setCollection.toString(d_nodeSlicing[nodeBase]) << std::endl; - - return ok; -} - template bool SliceManager::solveEquality(TNode lhs, TNode rhs) { std::set assumptions; @@ -541,11 +483,13 @@ bool SliceManager::isSliced(TNode node) const { if (find == d_nodeSlicing.end()) { result = nodeKind != kind::BITVECTOR_EXTRACT; } else { + set_reference sliceSet = (*find).second; + Assert(d_setCollection.size(sliceSet) >= 2); // The term is not sliced if one of the borders is not in the slice set or // there is a point between the borders result = - d_setCollection.contains(find->second, low) && d_setCollection.contains(find->second, high + 1) && - (low == high || d_setCollection.count(find->second, low + 1, high) == 0); + d_setCollection.contains(sliceSet, low) && d_setCollection.contains(sliceSet, high + 1) && + (low == high || d_setCollection.count(sliceSet, low + 1, high) == 0); } } @@ -553,6 +497,68 @@ bool SliceManager::isSliced(TNode node) const { return result; } +template +bool SliceManager::addSlice(Node node, unsigned slicePoint) { + Debug("slicing") << "SliceMagager::addSlice(" << node << "," << slicePoint << ")" << std::endl; + + bool ok = true; + + int low = node.getKind() == kind::BITVECTOR_EXTRACT ? utils::getExtractLow(node) : 0; + int high = node.getKind() == kind::BITVECTOR_EXTRACT ? utils::getExtractHigh(node) + 1: utils::getSize(node); + slicePoint += low; + + TNode nodeBase = baseTerm(node); + + set_reference sliceSet; + slicing_map::iterator find = d_nodeSlicing.find(nodeBase); + if (find == d_nodeSlicing.end()) { + d_nodeSlicing[nodeBase] = sliceSet = d_setCollection.newSet(0); + d_setCollection.insert(sliceSet, utils::getSize(nodeBase)); + } else { + sliceSet = (*find).second; + } + + Assert(d_setCollection.size(sliceSet) >= 2); + + // What are the points surrounding the new slice point + int prev = d_setCollection.prev(sliceSet, slicePoint); + int next = d_setCollection.next(sliceSet, slicePoint); + + // Add the slice to the set + d_setCollection.insert(sliceSet, slicePoint); + Debug("slicing") << "SliceMagager::addSlice(" << node << "," << slicePoint << "): current set " << d_setCollection.toString(sliceSet) << std::endl; + + // Add the terms and the equality to the equality engine + Node t1 = utils::mkExtract(nodeBase, next - 1, slicePoint); + Node t2 = utils::mkExtract(nodeBase, slicePoint - 1, prev); + Node nodeSlice = (next == high && prev == low) ? node : utils::mkExtract(nodeBase, next - 1, prev); + Node concat = utils::mkConcat(t1, t2); + + d_equalityEngine.addTerm(t1); + d_equalityEngine.addTerm(t2); + d_equalityEngine.addTerm(nodeSlice); + d_equalityEngine.addTerm(concat); + + // We are free to add this slice, unless the slice has a representative that's already a concat + TNode nodeSliceRepresentative = d_equalityEngine.getRepresentative(nodeSlice); + if (nodeSliceRepresentative.getKind() != kind::BITVECTOR_CONCAT) { + // Add the slice to the equality engine + ok = d_equalityEngine.addEquality(nodeSlice, concat, utils::mkTrue()); + } else { + // If the representative is a concat, we must solve it + // There is no need do add nodeSlice = concat as we will solve the representative of nodeSlice + std::set assumptions; + std::vector equalities; + d_equalityEngine.getExplanation(nodeSlice, nodeSliceRepresentative, equalities); + assumptions.insert(equalities.begin(), equalities.end()); + ok = solveEquality(nodeSliceRepresentative, concat, assumptions); + } + + Debug("slicing") << "SliceMagager::addSlice(" << node << "," << slicePoint << ") => " << d_setCollection.toString(d_nodeSlicing[nodeBase]) << std::endl; + + return ok; +} + template inline bool SliceManager::slice(TNode node, std::vector& sliced) { @@ -572,18 +578,19 @@ inline bool SliceManager::slice(TNode node, std::vector& Assert(nodeBase.getKind() != kind::CONST_BITVECTOR); // The nodes slice set - set_collection::reference_type nodeSliceSet; + set_reference nodeSliceSet; // Find the current one or construct it slicing_map::iterator findSliceSet = d_nodeSlicing.find(nodeBase); if (findSliceSet == d_nodeSlicing.end()) { - nodeSliceSet = d_setCollection.newSet(utils::getSize(nodeBase)); - d_setCollection.insert(nodeSliceSet, 0); - d_nodeSlicing[nodeBase] = nodeSliceSet; + d_nodeSlicing[nodeBase] = nodeSliceSet = d_setCollection.newSet(0); + d_setCollection.insert(nodeSliceSet, utils::getSize(nodeBase)); } else { nodeSliceSet = d_nodeSlicing[nodeBase]; } + Assert(d_setCollection.size(nodeSliceSet) >= 2); + Debug("slicing") << "SliceManager::slice(" << node << "): current: " << d_setCollection.toString(nodeSliceSet) << std::endl; std::vector slicePoints; if (low + 1 < high) { diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index 2d823383c..2d989a563 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -89,6 +89,8 @@ void TheoryBV::check(Effort e) { assumptions.insert(assertion); d_out->conflict(mkConjunction(assumptions)); return; + } else { + d_disequalities.push_back(assertion); } break; } @@ -96,6 +98,32 @@ void TheoryBV::check(Effort e) { Unhandled(); } } + + if (fullEffort(e)) { + + Debug("bitvector") << "TheoryBV::check(" << e << "): checking dis-equalities" << std::endl; + + for (unsigned i = 0, i_end = d_disequalities.size(); i < i_end; ++ i) { + + Debug("bitvector") << "TheoryBV::check(" << e << "): checking " << d_disequalities[i] << std::endl; + + TNode equality = d_disequalities[i][0]; + // Assumptions + std::set assumptions; + Node lhsNormalized = d_eqEngine.normalize(equality[0], assumptions); + Node rhsNormalized = d_eqEngine.normalize(equality[1], assumptions); + + Debug("bitvector") << "TheoryBV::check(" << e << "): normalizes to " << lhsNormalized << " = " << rhsNormalized << std::endl; + + // No need to slice the equality, the whole thing *should* be deduced + if (lhsNormalized == rhsNormalized) { + Debug("bitvector") << "TheoryBV::check(" << e << "): conflict with " << utils::setToString(assumptions) << std::endl; + assumptions.insert(d_disequalities[i]); + d_out->conflict(mkConjunction(assumptions)); + return; + } + } + } } bool TheoryBV::triggerEquality(size_t triggerId) { diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h index 8eaa332eb..474c4d0cd 100644 --- a/src/theory/bv/theory_bv.h +++ b/src/theory/bv/theory_bv.h @@ -93,13 +93,16 @@ private: /** The asserted stuff */ context::CDSet d_assertions; + /** Asserted dis-equalities */ + context::CDList d_disequalities; + /** Called by the equality managere on triggers */ bool triggerEquality(size_t triggerId); public: TheoryBV(context::Context* c, OutputChannel& out) : - Theory(THEORY_BV, c, out), d_eqEngine(*this, c, "theory::bv::EqualityEngine"), d_sliceManager(*this, c), d_assertions(c) { + Theory(THEORY_BV, c, out), d_eqEngine(*this, c, "theory::bv::EqualityEngine"), d_sliceManager(*this, c), d_assertions(c), d_disequalities(c) { } BvEqualityEngine& getEqualityEngine() { diff --git a/test/regress/regress0/bv/core/Makefile.am b/test/regress/regress0/bv/core/Makefile.am index 0e559f6f2..25f977f3b 100644 --- a/test/regress/regress0/bv/core/Makefile.am +++ b/test/regress/regress0/bv/core/Makefile.am @@ -62,8 +62,9 @@ TESTS = \ slice-17.smt \ slice-18.smt \ slice-19.smt \ - slice-20.smt - + slice-20.smt \ + ext_con_004_001_1024.smt + EXTRA_DIST = $(TESTS) # synonyms for "check" diff --git a/test/regress/regress0/bv/core/bitvec0.smt b/test/regress/regress0/bv/core/bitvec0.smt new file mode 100644 index 000000000..12766375f --- /dev/null +++ b/test/regress/regress0/bv/core/bitvec0.smt @@ -0,0 +1,24 @@ +(benchmark bitvec0.smt + :source { +Hand-crafted bit-vector benchmarks. Some are from the SVC benchmark suite. +Contributed by Vijay Ganesh (vganesh@stanford.edu). Translated into SMT-LIB +format by Clark Barrett using CVC3. + +} + :status unsat + :difficulty { 0 } + :category { crafted } + :logic QF_BV + :extrafuns ((a BitVec[32])) + :extrafuns ((t BitVec[32])) + :extrafuns ((b BitVec[32])) + :extrafuns ((aa BitVec[32])) + :extrafuns ((c BitVec[32])) + :extrafuns ((d BitVec[32])) + :extrafuns ((aaaa BitVec[32])) + :extrafuns ((bbb BitVec[32])) + :extrafuns ((aaa BitVec[32])) + :extrafuns ((z BitVec[32])) + :formula +(let (?cvc_0 (extract[6:2] a)) (let (?cvc_1 (extract[2:2] t)) (let (?cvc_2 (extract[6:6] t)) (let (?cvc_3 (extract[2:0] b)) (let (?cvc_4 (extract[2:0] c)) (not (and (and (and (if_then_else (= (concat (concat bv0[1] (extract[3:2] a)) (extract[6:5] a)) ?cvc_0) (= ?cvc_0 bv0[5]) (if_then_else (or (or (= bv2[3] bv6[3]) (= bv0[3] bv6[3]) ) (= bv7[3] bv6[3]) ) false true)) (and (if_then_else (= (concat (extract[3:2] t) (extract[6:5] t)) (extract[5:2] t)) (= ?cvc_1 ?cvc_2) true) (if_then_else (= (extract[4:0] t) (extract[6:2] t)) (and (and (= ?cvc_1 (extract[4:4] t)) (= (extract[0:0] t) ?cvc_2)) (= (extract[1:1] t) (extract[5:5] t))) true))) (implies (and (and (= ?cvc_3 (extract[2:0] aa)) (= ?cvc_4 ?cvc_3)) (= ?cvc_4 (extract[2:0] d))) (= (extract[1:1] d) (extract[1:1] aa)))) (and (and (and (if_then_else (= bv7[3] (extract[2:0] aaaa)) (= bv1[1] (extract[1:1] aaaa)) true) (if_then_else (= (extract[2:0] bbb) (extract[2:0] aaa)) (= (extract[1:1] bbb) (extract[1:1] aaa)) true)) (= (concat (concat (concat bv4[3] bv1[1]) bv1[1]) bv2[2]) (concat (concat bv1[1] bv7[5]) bv0[1]))) (if_then_else (= bv3[2] (extract[1:0] z)) (= bv1[1] (extract[0:0] z)) true))))))))) +) diff --git a/test/regress/regress0/bv/core/ext_con_004_001_1024.smt b/test/regress/regress0/bv/core/ext_con_004_001_1024.smt new file mode 100644 index 000000000..95d1aa0fd --- /dev/null +++ b/test/regress/regress0/bv/core/ext_con_004_001_1024.smt @@ -0,0 +1,26 @@ +(benchmark ext_con_004_001_1024.smt +:source { Generated by Roberto Bruttomesso } +:status unsat +:category { crafted } +:logic QF_BV +:extrafuns ((a BitVec[1024])) +:extrafuns ((dummy BitVec[256])) +:extrafuns ((v1 BitVec[1024])) +:extrafuns ((v2 BitVec[1024])) +:extrafuns ((v3 BitVec[1024])) +:extrafuns ((v4 BitVec[1024])) +:formula +(let (?shared a) +(and +(not (= (extract[767:512] v1) (extract[511:256] v1))) +(not (= (extract[767:512] v2) (extract[511:256] v2))) +(not (= (extract[767:512] v3) (extract[511:256] v3))) +(not (= (extract[767:512] v4) (extract[511:256] v4))) +(or +(and (= (extract[1023:256] ?shared) (concat (extract[1023:512] v1 ) dummy)) (= (extract[767:0] ?shared) (concat dummy (extract[511:0] v1 )))) +(and (= (extract[1023:256] ?shared) (concat (extract[1023:512] v2 ) dummy)) (= (extract[767:0] ?shared) (concat dummy (extract[511:0] v2 )))) +(and (= (extract[1023:256] ?shared) (concat (extract[1023:512] v3 ) dummy)) (= (extract[767:0] ?shared) (concat dummy (extract[511:0] v3 )))) +(and (= (extract[1023:256] ?shared) (concat (extract[1023:512] v4 ) dummy)) (= (extract[767:0] ?shared) (concat dummy (extract[511:0] v4 )))) +) +)) +) -- 2.30.2