Bugfix. Fix the semantics of BVSMOD to always give the remainder rounding towards...

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1343 e59a4935-1847-0410-ae03-e826735625c1

diff --git a/src/AST/ArrayTransformer.cpp b/src/AST/ArrayTransformer.cpp
index 5f71254623e188c01974406ba7600a376d700cef..af1853c9a28861ddb44dd7c259c8c35a5345f5f6 100644 (file)
--- a/src/AST/ArrayTransformer.cpp
+++ b/src/AST/ArrayTransformer.cpp
@@ -51,7 +51,7 @@ namespace BEEV
 
     runTimes->stop(RunTimes::Transforming);
 
-    return result;
+   return result;
   }
 
   //Translates signed BVDIV,BVMOD and BVREM into unsigned variety
@@ -106,19 +106,26 @@ namespace BEEV
       }
 
     // This is the modulus of dividing rounding to -infinity.
-    // Except if the signs are different, and it perfectly divides
-    // the modulus is the divisor (not zero).
     else if (SBVMOD == in.GetKind())
       {
-        // (let (?msb_s (extract[|m-1|:|m-1|] s))
-        // (let (?msb_t (extract[|m-1|:|m-1|] t))
-        // (ite (and (= ?msb_s bit0) (= ?msb_t bit0))
-        //      (bvurem s t)
-        // (ite (and (= ?msb_s bit1) (= ?msb_t bit0))
-        //      (bvadd (bvneg (bvurem (bvneg s) t)) t)
-        // (ite (and (= ?msb_s bit0) (= ?msb_t bit1))
-        //      (bvadd (bvurem s (bvneg t)) t)
-        //      (bvneg (bvurem (bvneg s) (bvneg t)))))))
+
+       /*
+                       (bvsmod s t) abbreviates
+                                 (let ((?msb_s ((_ extract |m-1| |m-1|) s))
+                                               (?msb_t ((_ extract |m-1| |m-1|) t)))
+                                       (let ((abs_s (ite (= ?msb_s #b0) s (bvneg s)))
+                                                 (abs_t (ite (= ?msb_t #b0) t (bvneg t))))
+                                         (let ((u (bvurem abs_s abs_t)))
+                                               (ite (= u (_ bv0 m))
+                                                        u
+                                               (ite (and (= ?msb_s #b0) (= ?msb_t #b0))
+                                                        u
+                                               (ite (and (= ?msb_s #b1) (= ?msb_t #b0))
+                                                        (bvadd (bvneg u) t)
+                                               (ite (and (= ?msb_s #b0) (= ?msb_t #b1))
+                                                        (bvadd u t)
+                                                        (bvneg u))))))))
+        */
 
         //Take absolute value.
         ASTNode pos_dividend = 
@@ -143,12 +150,14 @@ namespace BEEV
                          nf->CreateTerm(BVUMINUS, len, urem_node),
                          urem_node);
 
-        // if It's XOR <0 then add t (not its absolute value).
+        // if It's XOR <0, and it doesn't perfectly divide, then add t (not its absolute value).
         ASTNode xor_node = 
           nf->CreateNode(XOR, cond_dividend, cond_divisor);
+        ASTNode neZ = nf->CreateNode(NOT, nf->CreateNode(EQ, rev_node, bm->CreateZeroConst(divisor.GetValueWidth())));
+        ASTNode cond = nf->CreateNode(AND,xor_node ,neZ);
         ASTNode n = 
           nf->CreateTerm(ITE, len,
-                         xor_node, 
+                         cond,
                          nf->CreateTerm(BVPLUS, len, rev_node, divisor),
                          rev_node);
 

diff --git a/src/simplifier/consteval.cpp b/src/simplifier/consteval.cpp
index e9acd557fe04036063dbbcc129edfa9ee72a5212..412f100d5d4d5541f7997002c2761066dc81a1c9 100644 (file)
--- a/src/simplifier/consteval.cpp
+++ b/src/simplifier/consteval.cpp
@@ -346,18 +346,23 @@ namespace BEEV
       case SBVMOD:
         {
           assert(2==number_of_children);
-          /* Definition taken from the SMTLIB website
-             (bvsmod s t) abbreviates
-             (let (?msb_s (extract[|m-1|:|m-1|] s))
-             (let (?msb_t (extract[|m-1|:|m-1|] t))
-             (ite (and (= ?msb_s bit0) (= ?msb_t bit0))
-             (bvurem s t)
-             (ite (and (= ?msb_s bit1) (= ?msb_t bit0))
-             (bvadd (bvneg (bvurem (bvneg s) t)) t)
-             (ite (and (= ?msb_s bit0) (= ?msb_t bit1))
-             (bvadd (bvurem s (bvneg t)) t)
-             (bvneg (bvurem (bvneg s) (bvneg t)))))))
-          */
+/*
+          (bvsmod s t) abbreviates
+              (let ((?msb_s ((_ extract |m-1| |m-1|) s))
+                    (?msb_t ((_ extract |m-1| |m-1|) t)))
+                (let ((abs_s (ite (= ?msb_s #b0) s (bvneg s)))
+                      (abs_t (ite (= ?msb_t #b0) t (bvneg t))))
+                  (let ((u (bvurem abs_s abs_t)))
+                    (ite (= u (_ bv0 m))
+                         u
+                    (ite (and (= ?msb_s #b0) (= ?msb_t #b0))
+                         u
+                    (ite (and (= ?msb_s #b1) (= ?msb_t #b0))
+                         (bvadd (bvneg u) t)
+                    (ite (and (= ?msb_s #b0) (= ?msb_t #b1))
+                         (bvadd u t)
+                         (bvneg u))))))))
+*/
 
           assert(input_children[0].GetValueWidth() == input_children[1].GetValueWidth());
 
@@ -396,20 +401,25 @@ namespace BEEV
                   CONSTANTBV::BitVector_Negate(tmp0b, tmp0);
 
                   CONSTANTBV::ErrCode e = CONSTANTBV::BitVector_Div_Pos(quotient, tmp0b, tmp1, remainder);
-
                   assert(e == CONSTANTBV::ErrCode_Ok);
 
                   CBV remb = CONSTANTBV::BitVector_Create(inputwidth, true);
                   CONSTANTBV::BitVector_Negate(remb, remainder);
 
-                  bool carry = false;
-                  CBV res = CONSTANTBV::BitVector_Create(inputwidth, true);
-                  CONSTANTBV::BitVector_add(res, remb, tmp1, &carry);
-
-                  OutputNode = _bm->CreateBVConst(res, outputwidth);
+                  if (CONSTANTBV::BitVector_is_empty(remb))
+                  {
+                                       OutputNode = _bm->CreateZeroConst(outputwidth);
+                  }
+                  else
+                  {
+                       CBV res = CONSTANTBV::BitVector_Create(inputwidth, true);
+                       bool carry = false;
+                       CONSTANTBV::BitVector_add(res, remb, tmp1, &carry);
+                                       OutputNode = _bm->CreateBVConst(res, outputwidth);
+                  }
 
-                  CONSTANTBV::BitVector_Destroy(tmp0b);
                   CONSTANTBV::BitVector_Destroy(remb);
+                  CONSTANTBV::BitVector_Destroy(tmp0b);
                   CONSTANTBV::BitVector_Destroy(remainder);
                 }
               else if (!isNegativeS && isNegativeT)
@@ -422,11 +432,17 @@ namespace BEEV
 
                   assert(e == CONSTANTBV::ErrCode_Ok);
 
-                  bool carry = false;
-                  CBV res = CONSTANTBV::BitVector_Create(inputwidth, true);
-                  CONSTANTBV::BitVector_add(res, remainder, tmp1, &carry);
-
-                  OutputNode = _bm->CreateBVConst(res, outputwidth);
+                  if (CONSTANTBV::BitVector_is_empty(remainder))
+                  {
+                                       OutputNode = _bm->CreateZeroConst(outputwidth);
+                                 }
+                                       else
+                                 {
+                                       CBV res = CONSTANTBV::BitVector_Create(inputwidth, true);
+                       bool carry = false;
+                                       CONSTANTBV::BitVector_add(res, remainder, tmp1, &carry);
+                                       OutputNode = _bm->CreateBVConst(res, outputwidth);
+                                 }
 
                   CONSTANTBV::BitVector_Destroy(tmp1b);
                   CONSTANTBV::BitVector_Destroy(remainder);