summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/prop/bvminisat/bvminisat.cpp1
-rw-r--r--src/theory/bv/bv_to_bool.cpp19
-rw-r--r--src/theory/bv/theory_bv.cpp29
-rw-r--r--src/theory/bv/theory_bv.h8
-rw-r--r--src/theory/bv/theory_bv_rewrite_rules.h5
-rw-r--r--src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h16
-rw-r--r--src/theory/bv/theory_bv_rewriter.cpp18
7 files changed, 79 insertions, 17 deletions
diff --git a/src/prop/bvminisat/bvminisat.cpp b/src/prop/bvminisat/bvminisat.cpp
index 6bbe4bb3e..ab25fa6cb 100644
--- a/src/prop/bvminisat/bvminisat.cpp
+++ b/src/prop/bvminisat/bvminisat.cpp
@@ -106,6 +106,7 @@ SatValue BVMinisatSatSolver::solve(){
SatValue BVMinisatSatSolver::solve(long unsigned int& resource){
Trace("limit") << "MinisatSatSolver::solve(): have limit of " << resource << " conflicts" << std::endl;
+ ++d_statistics.d_statCallsToSolve;
if(resource == 0) {
d_minisat->budgetOff();
} else {
diff --git a/src/theory/bv/bv_to_bool.cpp b/src/theory/bv/bv_to_bool.cpp
index 8084a7282..7bec805ef 100644
--- a/src/theory/bv/bv_to_bool.cpp
+++ b/src/theory/bv/bv_to_bool.cpp
@@ -44,8 +44,11 @@ void BvToBoolVisitor::start(TNode node) {}
void BvToBoolVisitor::storeBvToBool(TNode bv_term, TNode bool_term) {
Assert (bv_term.getType().isBitVector() &&
- bv_term.getType().getBitVectorSize() == 1);
- Assert (bool_term.getType().isBoolean() && d_bvToBoolMap.find(bv_term) == d_bvToBoolMap.end());
+ bv_term.getType().getBitVectorSize() == 1 &&
+ bool_term.getType().isBoolean() && bv_term != Node() && bool_term != Node());
+ if (d_bvToBoolMap.find(bv_term) != d_bvToBoolMap.end()) {
+ Assert (d_bvToBoolMap[bv_term] == bool_term);
+ }
d_bvToBoolMap[bv_term] = bool_term;
}
@@ -75,9 +78,10 @@ bool BvToBoolVisitor::isConvertibleBvTerm(TNode node) {
return true;
}
- Kind kind = node.getKind();
if (!node.getType().isBitVector() || node.getType().getBitVectorSize() != 1)
return false;
+
+ Kind kind = node.getKind();
if (kind == kind::CONST_BITVECTOR) {
return true;
@@ -95,6 +99,10 @@ bool BvToBoolVisitor::isConvertibleBvTerm(TNode node) {
}
return true;
}
+ if (kind == kind::VARIABLE) {
+ storeBvToBool(node, utils::mkNode(kind::EQUAL, node, utils::mkConst(BitVector(1, 1u))));
+ return true;
+ }
return false;
}
@@ -226,7 +234,8 @@ void BvToBoolVisitor::visit(TNode current, TNode parent) {
check(current, parent);
if (isConvertibleBvAtom(current)) {
- result = convertBvAtom(current);
+ result = convertBvAtom(current);
+ addToCache(current, result);
} else if (isConvertibleBvTerm(current)) {
result = convertBvTerm(current);
} else {
@@ -244,10 +253,10 @@ void BvToBoolVisitor::visit(TNode current, TNode parent) {
}
result = builder;
}
+ addToCache(current, result);
}
Assert (result != Node());
Debug("bv-to-bool") << " =>" << result <<"\n";
- addToCache(current, result);
}
diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index 326eab36a..953f9b3e5 100644
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -43,6 +43,7 @@ TheoryBV::TheoryBV(context::Context* c, context::UserContext* u, OutputChannel&
d_subtheories(),
d_subtheoryMap(),
d_statistics(),
+ d_lemmasAdded(c, false),
d_conflict(c, false),
d_literalsToPropagate(c),
d_literalsToPropagateIndex(c, 0),
@@ -125,6 +126,28 @@ void TheoryBV::sendConflict() {
}
}
+void TheoryBV::checkForLemma(TNode fact) {
+ if (fact.getKind() == kind::EQUAL) {
+ if (fact[0].getKind() == kind::BITVECTOR_UREM_TOTAL) {
+ TNode urem = fact[0];
+ TNode result = fact[1];
+ TNode divisor = urem[1];
+ Node result_ult_div = utils::mkNode(kind::BITVECTOR_ULT, result, divisor);
+ Node split = utils::mkNode(kind::OR, utils::mkNode(kind::NOT, fact), result_ult_div);
+ lemma(split);
+ }
+ if (fact[1].getKind() == kind::BITVECTOR_UREM_TOTAL) {
+ TNode urem = fact[1];
+ TNode result = fact[0];
+ TNode divisor = urem[1];
+ Node result_ult_div = utils::mkNode(kind::BITVECTOR_ULT, result, divisor);
+ Node split = utils::mkNode(kind::OR, utils::mkNode(kind::NOT, fact), result_ult_div);
+ lemma(split);
+ }
+ }
+}
+
+
void TheoryBV::check(Effort e)
{
Trace("bitvector") <<"TheoryBV::check (" << e << ")\n";
@@ -144,8 +167,14 @@ void TheoryBV::check(Effort e)
return;
}
+ if (Theory::fullEffort(e)) {
+ Trace("bitvector-fulleffort") << "TheoryBV::fullEffort \n";
+ printFacts( Trace("bitvector-fulleffort") );
+ }
+
while (!done()) {
TNode fact = get().assertion;
+ checkForLemma(fact);
for (unsigned i = 0; i < d_subtheories.size(); ++i) {
d_subtheories[i]->assertFact(fact);
}
diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h
index 481493e13..22e3d0507 100644
--- a/src/theory/bv/theory_bv.h
+++ b/src/theory/bv/theory_bv.h
@@ -85,6 +85,8 @@ private:
Statistics d_statistics;
+ context::CDO<bool> d_lemmasAdded;
+
// Are we in conflict?
context::CDO<bool> d_conflict;
@@ -97,6 +99,8 @@ private:
/** Index of the next literal to propagate */
context::CDO<unsigned> d_literalsToPropagateIndex;
+
+
/**
* Keeps a map from nodes to the subtheory that propagated it so that we can explain it
* properly.
@@ -147,7 +151,9 @@ private:
void sendConflict();
- void lemma(TNode node) { d_out->lemma(node); }
+ void lemma(TNode node) { d_out->lemma(node); d_lemmasAdded = true; }
+
+ void checkForLemma(TNode node);
friend class Bitblaster;
friend class BitblastSolver;
diff --git a/src/theory/bv/theory_bv_rewrite_rules.h b/src/theory/bv/theory_bv_rewrite_rules.h
index cff85b92b..d362fa603 100644
--- a/src/theory/bv/theory_bv_rewrite_rules.h
+++ b/src/theory/bv/theory_bv_rewrite_rules.h
@@ -152,7 +152,7 @@ enum RewriteRuleId {
AndSimplify,
OrSimplify,
XorSimplify,
-
+ UleEliminate,
// rules to simplify bitblasting
BBPlusNeg
};
@@ -269,7 +269,8 @@ inline std::ostream& operator << (std::ostream& out, RewriteRuleId ruleId) {
case BBPlusNeg : out << "BBPlusNeg"; return out;
case UltOne : out << "UltOne"; return out;
case SltZero : out << "SltZero"; return out;
- case ZeroUlt : out << "ZeroUlt"; return out;
+ case ZeroUlt : out << "ZeroUlt"; return out;
+ case UleEliminate : out << "UleEliminate"; return out;
default:
Unreachable();
}
diff --git a/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h b/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h
index b466aceae..a63721de1 100644
--- a/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h
+++ b/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h
@@ -85,6 +85,7 @@ Node RewriteRule<SgeEliminate>::apply(TNode node) {
return result;
}
+
template <>
bool RewriteRule<SltEliminate>::applies(TNode node) {
return (node.getKind() == kind::BITVECTOR_SLT);
@@ -136,6 +137,21 @@ Node RewriteRule<SleEliminate>::apply(TNode node) {
return utils::mkNode(kind::NOT, b_slt_a);
}
+template <>
+bool RewriteRule<UleEliminate>::applies(TNode node) {
+ return (node.getKind() == kind::BITVECTOR_ULE);
+}
+
+template <>
+Node RewriteRule<UleEliminate>::apply(TNode node) {
+ Debug("bv-rewrite") << "RewriteRule<UleEliminate>(" << node << ")" << std::endl;
+
+ TNode a = node[0];
+ TNode b = node[1];
+ Node b_ult_a = utils::mkNode(kind::BITVECTOR_ULT, b, a);
+ return utils::mkNode(kind::NOT, b_ult_a);
+}
+
template <>
bool RewriteRule<CompEliminate>::applies(TNode node) {
diff --git a/src/theory/bv/theory_bv_rewriter.cpp b/src/theory/bv/theory_bv_rewriter.cpp
index 07499d01a..f6d138f5d 100644
--- a/src/theory/bv/theory_bv_rewriter.cpp
+++ b/src/theory/bv/theory_bv_rewriter.cpp
@@ -75,10 +75,10 @@ RewriteResponse TheoryBVRewriter::RewriteUlt(TNode node, bool preregister) {
Node resultNode = LinearRewriteStrategy
< RewriteRule<EvalUlt>,
// if both arguments are constants evaluates
- RewriteRule<UltZero>,
+ RewriteRule<UltZero>
// a < 0 rewrites to false
- RewriteRule<UltOne>,
- RewriteRule<ZeroUlt>
+ // RewriteRule<UltOne>,
+ // RewriteRule<ZeroUlt>
>::apply(node);
return RewriteResponse(REWRITE_DONE, resultNode);
@@ -86,8 +86,8 @@ RewriteResponse TheoryBVRewriter::RewriteUlt(TNode node, bool preregister) {
RewriteResponse TheoryBVRewriter::RewriteSlt(TNode node, bool preregister){
Node resultNode = LinearRewriteStrategy
- < RewriteRule < EvalSlt >,
- RewriteRule < SltZero >
+ < RewriteRule < EvalSlt >
+ // RewriteRule < SltZero >
>::apply(node);
return RewriteResponse(REWRITE_DONE, resultNode);
@@ -106,18 +106,18 @@ RewriteResponse TheoryBVRewriter::RewriteUle(TNode node, bool preregister){
RewriteRule<UleMax>,
RewriteRule<ZeroUle>,
RewriteRule<UleZero>,
- RewriteRule<UleSelf>
+ RewriteRule<UleSelf>,
+ RewriteRule<UleEliminate>
>::apply(node);
return RewriteResponse(resultNode == node ? REWRITE_DONE : REWRITE_AGAIN, resultNode);
}
RewriteResponse TheoryBVRewriter::RewriteSle(TNode node, bool preregister){
Node resultNode = LinearRewriteStrategy
- < RewriteRule <EvalSle>,
+ < RewriteRule <EvalSle>,
RewriteRule <SleEliminate>
>::apply(node);
-
- return RewriteResponse(REWRITE_DONE, resultNode);
+ return RewriteResponse(resultNode == node? REWRITE_DONE : REWRITE_AGAIN, resultNode);
}
RewriteResponse TheoryBVRewriter::RewriteUgt(TNode node, bool preregister){
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback