From c2cf8201afa6b44a5d3103cf8938eccb69cec590 Mon Sep 17 00:00:00 2001
From: lianah <lianahady@gmail.com>
Date: Thu, 25 Apr 2013 18:43:12 -0400
Subject: added bvule, bvsle operator elimination rulesl; added bvurem lemma
 generation

---
 src/theory/bv/theory_bv.cpp | 29 +++++++++++++++++++++++++++++
 1 file changed, 29 insertions(+)

(limited to 'src/theory/bv/theory_bv.cpp')

diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index 7cb06ca15..bd7d4c70b 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),
@@ -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); 
     }
-- 
cgit v1.2.3