/** Backtrackable number of nodes that have been inserted */
context::CDO<unsigned> 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();
*/
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;
}
*/
reference_type max(reference_type set) const {
Assert(set != null);
+ Assert(isValid(set));
while (d_memory[set].hasRight()) {
set = d_memory[set].getRight();
}
*/
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)
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);
void insert(reference_type& root, const value_type& value) {
backtrack();
+ Assert(isValid(root));
if (root == null) {
root = newSet(value);
return;
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;
}
}
*/
const_value_reference maxElement(reference_type set) const {
Assert(set != null);
+ Assert(isValid(set));
backtrack();
return d_memory[max(set)].getValue();
}
*/
const_value_reference minElement(reference_type set) const {
Assert(set != null);
+ Assert(isValid(set));
backtrack();
return d_memory[min(set)].getValue();
}
*/
const_value_reference prev(reference_type set, const_value_reference value) {
backtrack();
+ Assert(isValid(set));
const_value_reference candidate_value;
bool candidate_found = false;
const_value_reference next(reference_type set, const_value_reference value) {
backtrack();
+ Assert(isValid(set));
const_value_reference candidate_value;
bool candidate_found = false;
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;
*/
bool contains(reference_type set, const_value_reference value) const {
backtrack();
+ Assert(isValid(set));
return count(set, value, value) > 0;
}
void getElements(reference_type set, const_value_reference lowerBound, const_value_reference upperBound, std::vector<value_type>& output) const {
Assert(lowerBound <= upperBound);
backtrack();
+ Assert(isValid(set));
Debug("set_collection") << "BacktrackableSetCollection::getElements(" << toString(set) << "," << lowerBound << "," << upperBound << ")" << std::endl;
*/
void print(std::ostream& out, reference_type set) const {
backtrack();
+ Assert(isValid(set));
+
if (set == null) {
return;
}
* 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();
typedef context::BacktrackableSetCollection<std::vector<slice_point>, slice_point, set_reference> set_collection;
/** The map type from nodes to their references */
- typedef std::map<Node, set_reference> slicing_map;
+ typedef context::CDMap<Node, set_reference, NodeHashFunction> slicing_map;
/** The equality engine theory of bit-vectors is using */
typedef typename TheoryBitvector::BvEqualityEngine EqualityEngine;
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)
+ {
}
/**
inline bool addSlice(Node term, unsigned slicePoint);
};
-
-template <class TheoryBitvector>
-bool SliceManager<TheoryBitvector>::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<TNode> assumptions;
- std::vector<TNode> 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 <class TheoryBitvector>
bool SliceManager<TheoryBitvector>::solveEquality(TNode lhs, TNode rhs) {
std::set<TNode> assumptions;
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);
}
}
return result;
}
+template <class TheoryBitvector>
+bool SliceManager<TheoryBitvector>::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<TNode> assumptions;
+ std::vector<TNode> 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 <class TheoryBitvector>
inline bool SliceManager<TheoryBitvector>::slice(TNode node, std::vector<Node>& sliced) {
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<size_t> slicePoints;
if (low + 1 < high) {
assumptions.insert(assertion);
d_out->conflict(mkConjunction(assumptions));
return;
+ } else {
+ d_disequalities.push_back(assertion);
}
break;
}
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<TNode> 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) {
/** The asserted stuff */
context::CDSet<TNode, TNodeHashFunction> d_assertions;
+ /** Asserted dis-equalities */
+ context::CDList<TNode> 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() {
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"
--- /dev/null
+(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)))))))))
+)
--- /dev/null
+(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 ))))
+)
+))
+)
projects / cvc5.git / commitdiff