summaryrefslogtreecommitdiff
path: root/src/theory/bv
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/bv')
-rw-r--r--src/theory/bv/theory_bv.cpp24
-rw-r--r--src/theory/bv/theory_bv.h7
-rw-r--r--src/theory/bv/theory_bv_rewrite_rules_normalization.h9
-rw-r--r--src/theory/bv/theory_bv_rewrite_rules_simplification.h17
-rw-r--r--src/theory/bv/theory_bv_rewriter.h3
5 files changed, 26 insertions, 34 deletions
diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index a3f4364ba..b6f12793d 100644
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -36,13 +36,13 @@ const bool d_useEqualityEngine = true;
const bool d_useSatPropagation = true;
-TheoryBV::TheoryBV(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation)
- : Theory(THEORY_BV, c, u, out, valuation),
+TheoryBV::TheoryBV(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo)
+ : Theory(THEORY_BV, c, u, out, valuation, logicInfo),
d_context(c),
d_assertions(c),
d_bitblaster(new Bitblaster(c) ),
- d_statistics(),
d_alreadyPropagatedSet(c),
+ d_statistics(),
d_notify(*this),
d_equalityEngine(d_notify, c, "theory::bv::TheoryBV"),
d_conflict(c, false),
@@ -204,7 +204,7 @@ void TheoryBV::check(Effort e)
// If in conflict, output the conflict
if (d_conflict) {
- Debug("bitvector") << spaces(getContext()->getLevel()) << "TheoryBV::check(): conflict " << d_conflictNode << std::endl;
+ Debug("bitvector") << spaces(getSatContext()->getLevel()) << "TheoryBV::check(): conflict " << d_conflictNode << std::endl;
d_out->conflict(d_conflictNode);
return;
}
@@ -247,7 +247,7 @@ Node TheoryBV::getValue(TNode n) {
void TheoryBV::propagate(Effort e) {
- BVDebug("bitvector") << spaces(getContext()->getLevel()) << "TheoryBV::propagate()" << std::endl;
+ BVDebug("bitvector") << spaces(getSatContext()->getLevel()) << "TheoryBV::propagate()" << std::endl;
if (d_conflict) {
return;
@@ -256,13 +256,13 @@ void TheoryBV::propagate(Effort e) {
// get new propagations from the equality engine
for (; d_literalsToPropagateIndex < d_literalsToPropagate.size(); d_literalsToPropagateIndex = d_literalsToPropagateIndex + 1) {
TNode literal = d_literalsToPropagate[d_literalsToPropagateIndex];
- BVDebug("bitvector") << spaces(getContext()->getLevel()) << "TheoryBV::propagate(): propagating from equality engine: " << literal << std::endl;
+ BVDebug("bitvector") << spaces(getSatContext()->getLevel()) << "TheoryBV::propagate(): propagating from equality engine: " << literal << std::endl;
bool satValue;
Node normalized = Rewriter::rewrite(literal);
if (!d_valuation.hasSatValue(normalized, satValue) || satValue) {
d_out->propagate(literal);
} else {
- Debug("bitvector") << spaces(getContext()->getLevel()) << "TheoryBV::propagate(): in conflict, normalized = " << normalized << std::endl;
+ Debug("bitvector") << spaces(getSatContext()->getLevel()) << "TheoryBV::propagate(): in conflict, normalized = " << normalized << std::endl;
Node negatedLiteral;
std::vector<TNode> assumptions;
if (normalized != d_false) {
@@ -353,11 +353,11 @@ Theory::PPAssertStatus TheoryBV::ppAssert(TNode in, SubstitutionMap& outSubstitu
bool TheoryBV::propagate(TNode literal)
{
- Debug("bitvector") << spaces(getContext()->getLevel()) << "TheoryBV::propagate(" << literal << ")" << std::endl;
+ Debug("bitvector") << spaces(getSatContext()->getLevel()) << "TheoryBV::propagate(" << literal << ")" << std::endl;
// If already in conflict, no more propagation
if (d_conflict) {
- Debug("bitvector") << spaces(getContext()->getLevel()) << "TheoryBV::propagate(" << literal << "): already in conflict" << std::endl;
+ Debug("bitvector") << spaces(getSatContext()->getLevel()) << "TheoryBV::propagate(" << literal << "): already in conflict" << std::endl;
return false;
}
@@ -369,7 +369,7 @@ bool TheoryBV::propagate(TNode literal)
// If asserted, we might be in conflict
if (isAsserted) {
if (!satValue) {
- Debug("bitvector") << spaces(getContext()->getLevel()) << "TheoryBV::propagate(" << literal << ", normalized = " << normalized << ") => conflict" << std::endl;
+ Debug("bitvector") << spaces(getSatContext()->getLevel()) << "TheoryBV::propagate(" << literal << ", normalized = " << normalized << ") => conflict" << std::endl;
std::vector<TNode> assumptions;
Node negatedLiteral;
if (normalized != d_false) {
@@ -386,7 +386,7 @@ bool TheoryBV::propagate(TNode literal)
}
// Nothing, just enqueue it for propagation and mark it as asserted already
- Debug("bitvector") << spaces(getContext()->getLevel()) << "TheoryBV::propagate(" << literal << ") => enqueuing for propagation" << std::endl;
+ Debug("bitvector") << spaces(getSatContext()->getLevel()) << "TheoryBV::propagate(" << literal << ") => enqueuing for propagation" << std::endl;
d_literalsToPropagate.push_back(literal);
return true;
@@ -432,7 +432,7 @@ Node TheoryBV::explain(TNode node) {
void TheoryBV::addSharedTerm(TNode t) {
- Debug("bitvector::sharing") << spaces(getContext()->getLevel()) << "TheoryBV::addSharedTerm(" << t << ")" << std::endl;
+ Debug("bitvector::sharing") << spaces(getSatContext()->getLevel()) << "TheoryBV::addSharedTerm(" << t << ")" << std::endl;
if (d_useEqualityEngine) {
d_equalityEngine.addTriggerTerm(t);
}
diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h
index 940eaef56..c4953213d 100644
--- a/src/theory/bv/theory_bv.h
+++ b/src/theory/bv/theory_bv.h
@@ -69,7 +69,7 @@ private:
public:
- TheoryBV(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation);
+ TheoryBV(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo);
~TheoryBV();
void preRegisterTerm(TNode n);
@@ -86,6 +86,7 @@ public:
//Node preprocessTerm(TNode term);
PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions);
+
private:
class Statistics {
@@ -107,13 +108,13 @@ private:
NotifyClass(TheoryBV& uf): d_bv(uf) {}
bool notify(TNode propagation) {
- Debug("bitvector") << spaces(d_bv.getContext()->getLevel()) << "NotifyClass::notify(" << propagation << ")" << std::endl;
+ Debug("bitvector") << spaces(d_bv.getSatContext()->getLevel()) << "NotifyClass::notify(" << propagation << ")" << std::endl;
// Just forward to bv
return d_bv.propagate(propagation);
}
void notify(TNode t1, TNode t2) {
- Debug("arrays") << spaces(d_bv.getContext()->getLevel()) << "NotifyClass::notify(" << t1 << ", " << t2 << ")" << std::endl;
+ Debug("arrays") << spaces(d_bv.getSatContext()->getLevel()) << "NotifyClass::notify(" << t1 << ", " << t2 << ")" << std::endl;
// Propagate equality between shared terms
Node equality = Rewriter::rewriteEquality(theory::THEORY_UF, t1.eqNode(t2));
d_bv.propagate(t1.eqNode(t2));
diff --git a/src/theory/bv/theory_bv_rewrite_rules_normalization.h b/src/theory/bv/theory_bv_rewrite_rules_normalization.h
index 5587e25eb..da3fb6554 100644
--- a/src/theory/bv/theory_bv_rewrite_rules_normalization.h
+++ b/src/theory/bv/theory_bv_rewrite_rules_normalization.h
@@ -384,18 +384,15 @@ Node RewriteRule<NegMult>::apply(Node node) {
BVDebug("bv-rewrite") << "RewriteRule<NegMult>(" << node << ")" << std::endl;
TNode mult = node[0];
std::vector<Node> children;
- bool has_const = false;
+ BitVector bv(utils::getSize(node), (unsigned)1);
for(unsigned i = 0; i < mult.getNumChildren(); ++i) {
if(mult[i].getKind() == kind::CONST_BITVECTOR) {
- Assert(has_const == false);
- has_const = true;
- BitVector bv = mult[i].getConst<BitVector>();
- children.push_back(utils::mkConst(-bv));
+ bv = bv * mult[i].getConst<BitVector>();
} else {
children.push_back(mult[i]);
}
}
- Assert (has_const);
+ children.push_back(utils::mkConst(-bv));
return utils::mkSortedNode(kind::BITVECTOR_MULT, children);
}
diff --git a/src/theory/bv/theory_bv_rewrite_rules_simplification.h b/src/theory/bv/theory_bv_rewrite_rules_simplification.h
index 530949de2..490b413db 100644
--- a/src/theory/bv/theory_bv_rewrite_rules_simplification.h
+++ b/src/theory/bv/theory_bv_rewrite_rules_simplification.h
@@ -308,15 +308,17 @@ Node RewriteRule<XorOne>::apply(Node node) {
for(unsigned i = 0; i < node.getNumChildren(); ++i) {
if (node[i] == ones) {
// make sure only ones occurs only once
- Assert(!found_ones);
- found_ones = true;
+ found_ones = !found_ones;
} else {
children.push_back(node[i]);
}
}
- children[0] = utils::mkNode(kind::BITVECTOR_NOT, children[0]);
- return utils::mkSortedNode(kind::BITVECTOR_XOR, children);
+ Node result = utils::mkNode(kind::BITVECTOR_XOR, children);
+ if (found_ones) {
+ result = utils::mkNode(kind::BITVECTOR_NOT, result);
+ }
+ return result;
}
@@ -344,16 +346,11 @@ template<> inline
Node RewriteRule<XorZero>::apply(Node node) {
BVDebug("bv-rewrite") << "RewriteRule<XorZero>(" << node << ")" << std::endl;
std::vector<Node> children;
- bool found_zero = false;
Node zero = utils::mkConst(utils::getSize(node), 0);
// XorSimplify should have been called before
for(unsigned i = 0; i < node.getNumChildren(); ++i) {
- if (node[i] == zero) {
- // make sure zero occurs only once
- Assert(!found_zero);
- found_zero = true;
- } else {
+ if (node[i] != zero) {
children.push_back(node[i]);
}
}
diff --git a/src/theory/bv/theory_bv_rewriter.h b/src/theory/bv/theory_bv_rewriter.h
index 0ce3fa303..60715ee60 100644
--- a/src/theory/bv/theory_bv_rewriter.h
+++ b/src/theory/bv/theory_bv_rewriter.h
@@ -33,10 +33,7 @@ struct AllRewriteRules;
typedef RewriteResponse (*RewriteFunction) (TNode, bool);
class TheoryBVRewriter {
- // static CVC4_THREADLOCAL(AllRewriteRules*) s_allRules;
- // static CVC4_THREADLOCAL(TimerStat*) d_rewriteTimer;
-#warning "TODO: Double check thread safety and make sure the fix compiles on mac."
static RewriteFunction d_rewriteTable[kind::LAST_KIND];
static RewriteResponse IdentityRewrite(TNode node, bool prerewrite = false);
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback