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

diff --git a/src/simplifier/simplifier.cpp b/src/simplifier/simplifier.cpp
index 7bd69487761d543619e5bdc0db8a81832bdc53d3..9a997873264c265c18699757c3636a2549e86a9f 100644 (file)
--- 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 (file)
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)
+