From cc701a49102275f42aecdcd994ab78366d14c5da Mon Sep 17 00:00:00 2001
From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Mon, 7 Mar 2011 02:48:14 +0000
Subject: [PATCH] Improvement. Add an extra simplification rule for BVDIV/
 BVMOD.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1192 e59a4935-1847-0410-ae03-e826735625c1
---
 src/simplifier/simplifier.cpp | 42 ++++++++++++++++++-----------
 unit_test/mod2.smt2           | 50 +++++++++++++++++++++++++++++++++++
 2 files changed, 77 insertions(+), 15 deletions(-)
 create mode 100644 unit_test/mod2.smt2

diff --git a/src/simplifier/simplifier.cpp b/src/simplifier/simplifier.cpp
index 7bd6948..9a99787 100644
--- a/src/simplifier/simplifier.cpp
+++ b/src/simplifier/simplifier.cpp
@@ -2740,26 +2740,38 @@ namespace BEEV
         break;
 
       case BVDIV:
-      if (inputterm[0] == inputterm[1])
         {
-          output = _bm->CreateOneConst(inputValueWidth);
-          break;
+        if (inputterm[0] == inputterm[1])
+          {
+            output = _bm->CreateOneConst(inputValueWidth);
+            break;
+          }
+        if (inputterm[1] == _bm->CreateOneConst(inputValueWidth))
+        {
+            output = inputterm[0];
+            break;
         }
-      if (inputterm[1] == _bm->CreateOneConst(inputValueWidth))
-      {
-    	  	 output = inputterm[0];
-    	  	 break;
+        ASTNode lessThan = SimplifyFormula(nf->CreateNode(BVLT, inputterm[0], inputterm[1]),false, NULL);
+        if (lessThan == ASTTrue)
+           output = _bm->CreateZeroConst(inputValueWidth);
+        else
+            output = inputterm;
       }
-      output = inputterm;
-      break;
-
-    case BVMOD:
-      if (inputterm[0] == inputterm[1])
+        break;
+      case BVMOD:
         {
-          output = _bm->CreateZeroConst(inputValueWidth);
-          break;
+          if (inputterm[0] == inputterm[1])
+          {
+            output = _bm->CreateZeroConst(inputValueWidth);
+            break;
+          }
+          ASTNode lessThan = SimplifyFormula(nf->CreateNode(BVLT, inputterm[0], inputterm[1]),false, NULL);
+
+          if (lessThan == ASTTrue)
+              output=  inputterm[0];
+           else
+              output = inputterm;
         }
-      output = inputterm;
       break;
 
     case BVXOR:
diff --git a/unit_test/mod2.smt2 b/unit_test/mod2.smt2
new file mode 100644
index 0000000..25893ce
--- /dev/null
+++ b/unit_test/mod2.smt2
@@ -0,0 +1,50 @@
+(set-logic QF_BV)
+(set-info :smt-lib-version 2.0)
+(set-info :category "check")
+(set-info :status sat)
+(declare-fun x () (_ BitVec 15))
+(declare-fun y () (_ BitVec 15))
+
+; This should be simplified down.
+;2758:(BVEXTRACT 
+;   2598:(BVMOD 
+;    188:(BVCONCAT 
+;      78:0b00000000000000
+;      34:(ITE 
+;        28:(BVSGT 
+;          26:(BVSX 
+;            12:v25374
+;            24:0x0000000E)
+;          16:v25376)
+;        30:0b1
+;        32:0b0))
+;    2594:0b011000111111101)
+;  198:0x0000000C
+;  200:0x00000005)
+
+
+
+; This is always true. 
+(assert 
+	(=  (concat (_ bv0 5) ((_ extract 9 0) x))
+		(bvurem (concat (_ bv0 5) ((_ extract 9 0) x)) (_ bv12000 15) ) 
+	)
+)
+
+; This is always true. 
+(assert 
+	(=  (_ bv0 15) 
+		(bvudiv (concat (_ bv0 5) ((_ extract 9 0) y)) (_ bv12000 15) ) 
+	)
+)
+
+
+
+; So unconstrained variables don't eliminate immediately.
+(assert (not (= x y)))
+
+
+
+(check-sat)
+(exit)
+
-- 
2.47.3