SatLiteral CnfStream::getLiteral(TNode node) {
TranslationCache::iterator find = d_translationCache.find(node);
- Assert(find != d_translationCache.end(), "Literal not in the CNF Cache");
+ Assert(find != d_translationCache.end(), "Literal not in the CNF Cache: ", node.toString().c_str());
SatLiteral literal = find->second.literal;
Debug("cnf") << "CnfStream::getLiteral(" << node << ") => " << literal << std::endl;
return literal;
#include "util/output.h"
#include "util/stats.h"
#include "theory/rewriter.h"
+#include "theory/bv/theory_bv_utils.h"
namespace CVC4 {
namespace theory {
// Check for constants
if (d_nodes[t1classId].getMetaKind() == kind::metakind::CONSTANT &&
d_nodes[t2classId].getMetaKind() == kind::metakind::CONSTANT) {
- d_notify.conflict(reason);
+ std::vector<TNode> reasons;
+ getExplanation(t1, d_nodes[t1classId], reasons);
+ getExplanation(t2, d_nodes[t2classId], reasons);
+ reasons.push_back(reason);
+ d_notify.conflict(utils::mkAnd(reasons));
return false;
}
template <typename OwnerClass, typename NotifyClass, typename UnionFindPreferences>
void EqualityEngine<OwnerClass, NotifyClass, UnionFindPreferences>::getExplanation(TNode t1, TNode t2, std::vector<TNode>& equalities) const {
- Assert(equalities.empty());
- Assert(t1 != t2);
Assert(getRepresentative(t1) == getRepresentative(t2));
Debug("equality") << "EqualityEngine::getExplanation(" << t1 << "," << t2 << ")" << std::endl;
+ // If the nodes are the same, we're done
+ if (t1 == t2) return;
+
const_cast<EqualityEngine*>(this)->backtrack();
// Queue for the BFS containing nodes
theory THEORY_BV ::CVC4::theory::bv::TheoryBV "theory/bv/theory_bv.h"
-properties finite check
+properties finite check propagate
rewriter ::CVC4::theory::bv::TheoryBVRewriter "theory/bv/theory_bv_rewriter.h"
// If we have a negation asserted, we have a confict
if (d_assertions.contains(equality.notNode())) {
- vector<TNode> assertions;
- d_eqEngine.getExplanation(equality[0], equality[1], assertions);
- assertions.push_back(equality.notNode());
- d_out->conflict(mkAnd(assertions));
+ std::vector<TNode> explanation;
+ d_eqEngine.getExplanation(equality[0], equality[1], explanation);
+ std::set<TNode> assumptions;
+ assumptions.insert(equality.notNode());
+ utils::getConjuncts(explanation, assumptions);
+ d_out->conflict(utils::mkConjunction(assumptions));
return false;
}
Unhandled(n.getKind());
}
}
+
+void TheoryBV::explain(TNode node) {
+ Debug("bitvector") << "TheoryBV::explain(" << node << ")" << std::endl;
+ if(node.getKind() == kind::EQUAL) {
+ std::vector<TNode> reasons;
+ d_eqEngine.getExplanation(node[0], node[1], reasons);
+ std::set<TNode> simpleReasons;
+ utils::getConjuncts(reasons, simpleReasons);
+ d_out->explanation(utils::mkConjunction(simpleReasons));
+ return;
+ }
+ Unreachable();
+}
return d_theoryBV.triggerEquality(triggerId);
}
void conflict(Node explanation) {
- d_theoryBV.d_out->conflict(explanation);
+ std::set<TNode> assumptions;
+ utils::getConjuncts(explanation, assumptions);
+ d_theoryBV.d_out->conflict(utils::mkConjunction(assumptions));
}
};
void propagate(Effort e) { }
- void explain(TNode n) { }
+ void explain(TNode n);
Node getValue(TNode n, Valuation* valuation);
}
inline Node mkAnd(std::vector<TNode>& children) {
- return NodeManager::currentNM()->mkNode(kind::AND, children);
+ if (children.size() > 1) {
+ return NodeManager::currentNM()->mkNode(kind::AND, children);
+ } else {
+ return children[0];
+ }
}
inline Node mkAnd(std::vector<Node>& children) {
}
}
+inline void getConjuncts(std::vector<TNode>& nodes, std::set<TNode>& conjuncts) {
+ for (unsigned i = 0, i_end = nodes.size(); i < i_end; ++ i) {
+ getConjuncts(nodes[i], conjuncts);
+ }
+}
+
+
inline Node mkConjunction(const std::set<TNode> nodes) {
std::set<TNode> expandedNodes;
slice-19.smt \
slice-20.smt \
ext_con_004_001_1024.smt \
- a78test0002.smt
+ a78test0002.smt \
+ a95test0002.smt \
+ bitvec0.smt \
+ bitvec2.smt \
+ bitvec3.smt \
+ bitvec5.smt
EXTRA_DIST = $(TESTS)
--- /dev/null
+(benchmark a95test0002.smt
+ :source {
+Bit-vector benchmarks from Dawson Engler's tool contributed by Vijay Ganesh
+(vganesh@stanford.edu). Translated into SMT-LIB format by Clark Barrett using
+CVC3.
+
+}
+ :status sat
+ :difficulty { 0 }
+ :category { industrial }
+ :logic QF_BV
+ :extrafuns ((a BitVec[32]))
+ :assumption
+(not (not (= (concat bv0[16] (extract[15:0] a)) a)))
+ :formula
+(not false)
+)
--- /dev/null
+(benchmark bitvec1.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 ((b BitVec[32]))
+ :extrafuns ((c BitVec[32]))
+ :extrafuns ((res BitVec[32]))
+ :formula
+(flet ($cvc_1 (= (extract[0:0] a) bv1[1])) (flet ($cvc_2 (= (extract[0:0] b) bv1[1])) (let (?cvc_0 (extract[0:0] c)) (flet ($cvc_6 (= ?cvc_0 bv1[1])) (let (?cvc_3 (extract[0:0] res)) (flet ($cvc_4 (= (extract[1:1] a) bv1[1])) (flet ($cvc_5 (= (extract[1:1] b) bv1[1])) (flet ($cvc_8 (if_then_else $cvc_4 (not $cvc_5) $cvc_5)) (let (?cvc_7 (extract[1:1] c)) (let (?cvc_9 (extract[1:1] res)) (not (implies (and (and (and (= (extract[1:0] a) bv1[2]) (= (extract[1:0] b) bv1[2])) (and (if_then_else (and $cvc_1 $cvc_2) $cvc_6 (= ?cvc_0 bv0[1])) (if_then_else (if_then_else $cvc_1 (not $cvc_2) $cvc_2) (= ?cvc_3 bv1[1]) (= ?cvc_3 bv0[1])))) (and (if_then_else (or (and $cvc_4 $cvc_5) (and $cvc_8 $cvc_6) ) (= ?cvc_7 bv1[1]) (= ?cvc_7 bv0[1])) (if_then_else (if_then_else $cvc_6 (not $cvc_8) $cvc_8) (= ?cvc_9 bv1[1]) (= ?cvc_9 bv0[1])))) (and (= (extract[1:0] res) bv2[2]) (= (extract[1:0] c) bv1[2]))))))))))))))
+)
--- /dev/null
+(benchmark bitvec2.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
+ :extrapreds ((a))
+ :formula
+(not (= (concat bv1[1] (ite a bv0[1] bv1[1])) (ite a bv2[2] bv3[2])))
+)
--- /dev/null
+(benchmark bitvec3.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 ((b BitVec[32]))
+ :extrafuns ((c1 BitVec[32]))
+ :extrafuns ((c2 BitVec[32]))
+ :extrafuns ((out BitVec[32]))
+ :extrafuns ((carry BitVec[32]))
+ :formula
+(let (?cvc_0 (extract[1:0] b)) (let (?cvc_1 (extract[2:0] c1)) (let (?cvc_3 (concat bv0[1] bv0[2])) (let (?cvc_2 (extract[2:0] c2)) (flet ($cvc_4 (= (extract[0:0] c1) bv1[1])) (flet ($cvc_5 (= (extract[0:0] c2) bv1[1])) (let (?cvc_6 (extract[0:0] carry)) (let (?cvc_7 (extract[1:1] c1)) (flet ($cvc_11 (= ?cvc_7 bv1[1])) (let (?cvc_8 (extract[1:1] c2)) (flet ($cvc_10 (= ?cvc_8 bv0[1])) (flet ($cvc_9 (= ?cvc_7 bv0[1])) (flet ($cvc_12 (= ?cvc_8 bv1[1])) (flet ($cvc_14 (or (and $cvc_11 $cvc_10) (and $cvc_9 $cvc_12) )) (flet ($cvc_13 (= ?cvc_6 bv1[1])) (let (?cvc_15 (extract[1:1] carry)) (let (?cvc_16 (extract[2:2] c1)) (flet ($cvc_20 (= ?cvc_16 bv1[1])) (let (?cvc_17 (extract[2:2] c2)) (flet ($cvc_19 (= ?cvc_17 bv0[1])) (flet ($cvc_18 (= ?cvc_16 bv0[1])) (flet ($cvc_21 (= ?cvc_17 bv1[1])) (flet ($cvc_22 (= ?cvc_15 bv1[1])) (not (implies (and (= (extract[1:0] a) bv3[2]) (= ?cvc_0 bv3[2])) (implies (and (and (and (and (and (and (and (if_then_else (= (extract[0:0] a) bv1[1]) (= ?cvc_1 (concat bv0[1] ?cvc_0)) (= ?cvc_1 ?cvc_3)) (if_then_else (= (extract[1:1] a) bv1[1]) (= ?cvc_2 (concat ?cvc_0 bv0[1])) (= ?cvc_2 ?cvc_3))) (= (extract[0:0] out) (ite (or $cvc_4 $cvc_5 ) bv1[1] bv0[1]))) (= ?cvc_6 (ite (and $cvc_4 $cvc_5) bv1[1] bv0[1]))) (= (extract[1:1] out) (ite (or (and (= ?cvc_6 bv0[1]) $cvc_14) (and $cvc_13 (and $cvc_9 $cvc_10)) ) bv1[1] bv0[1]))) (= ?cvc_15 (ite (or (and $cvc_11 $cvc_12) (and $cvc_13 $cvc_14) ) bv1[1] bv0[1]))) (= (extract[2:2] out) (ite (or (and (= ?cvc_15 bv0[1]) (or (and $cvc_20 $cvc_19) (and $cvc_18 $cvc_21) )) (and $cvc_22 (and $cvc_18 $cvc_19)) ) bv1[1] bv0[1]))) (= (extract[2:2] carry) (ite (or (and $cvc_20 $cvc_21) (and $cvc_22 (or $cvc_20 $cvc_21 )) ) bv1[1] bv0[1]))) (and (= (extract[2:0] out) bv1[3]) (= (extract[2:0] carry) bv6[3]))))))))))))))))))))))))))))
+)
--- /dev/null
+(benchmark bitvec5.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 ((b BitVec[32]))
+ :extrafuns ((c BitVec[32]))
+ :extrafuns ((d BitVec[32]))
+ :extrafuns ((e BitVec[32]))
+ :formula
+(not (and (implies (and (and (= (extract[31:0] a) (extract[31:0] b)) (= (extract[31:16] a) (extract[15:0] c))) (= (extract[31:8] b) (extract[23:0] d))) (= (extract[11:8] c) (extract[19:16] d))) (implies (= (extract[30:0] e) (extract[31:1] e)) (= (extract[0:0] e) (extract[31:31] e)))))
+)
projects / cvc5.git / commitdiff