added bvule, bvsle operator elimination rulesl; added bvurem lemma generation

diff --git a/src/prop/bvminisat/bvminisat.cpp b/src/prop/bvminisat/bvminisat.cpp
index 6bbe4bb3edf895c4d07c2523ca38fb7817bd9673..ab25fa6cbec8ccfbc12c83a8fee52bddba0c7f68 100644 (file)
--- 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 8084a728228937eadbcc01f5266cd7e8d54a320c..7bec805ef4dcd1b8726e2bac0d527b39a50adcbd 100644 (file)
--- 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 7cb06ca1564b7a67c9341bac5d9415c482ed796c..bd7d4c70b6a7614954f107c3c094395ab1bb8a45 100644 (file)
--- 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),
@@ -122,6 +123,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"; 
@@ -141,8 +164,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 8b184f9722e823cc25af91abb598705ddca90f20..827b6e878408006c2b534aaa3ec1adfcb049c5e3 100644 (file)
--- a/src/theory/bv/theory_bv.h
+++ b/src/theory/bv/theory_bv.h
@@ -84,6 +84,8 @@ private:
 
   Statistics d_statistics;
 
+  context::CDO<bool> d_lemmasAdded;
+  
   // Are we in conflict?
   context::CDO<bool> d_conflict;
 
@@ -96,6 +98,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.
@@ -146,7 +150,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 cff85b92b816484143b3f269737cac66470d1e8a..d362fa603509072ecd94e8b77b2dcc4eb734dc20 100644 (file)
--- 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 b466aceae5e9039dabd9ce641a2792f477e2d9c3..a63721de12196a30cfe55a764f2a8eb575835eec 100644 (file)
--- 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 07499d01a06c82b35a5cb51e8397ffed70a35593..f6d138f5d541b8d7a0367dd721503eaeb4c640ce 100644 (file)
--- 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){