(self, left, right)
return self.Ite(self.Or(cond1, cond2), u,
                        self.Ite(cond3, case3, self.Ite(cond4, case4, case5)))
Returns the SIGNED MODULUS of left divided by right.
Returns the SIGNED MODULUS of left divided by right.
Returns the SIGNED MODULUS of left divided by right .
def BVSMod(self, left, right):
        """Returns the SIGNED MODULUS of left divided by right."""
        # According to SMT-LIB standard (2015-06-23) BVSMod is defined as follows
        # http://smtlib.cs.uiowa.edu/logics-all.shtml#QF_BV
        #
        # For all terms s,t of sort (_ BitVec m), where 0 < m,
        # (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))))))))
        m = left.bv_width()
        s = left
        t = right
        zero_1 = self.BV("#b0")
        one_1 = self.BV("#b1")

        msb_s = self.BVExtract(s, m-1, m-1)
        msb_t = self.BVExtract(t, m-1, m-1)
        abs_s = self.Ite(self.Equals(msb_s, zero_1), s, self.BVNeg(s))
        abs_t = self.Ite(self.Equals(msb_t, zero_1), t, self.BVNeg(t))
        u = self.BVURem(abs_s, abs_t)

        cond1 = self.Equals(u, self.BV(0, m))
        cond2 = self.And(self.Equals(msb_s, zero_1), self.Equals(msb_t, zero_1))
        cond3 = self.And(self.Equals(msb_s, one_1), self.Equals(msb_t, zero_1))
        cond4 = self.And(self.Equals(msb_s, zero_1), self.Equals(msb_t, one_1))

        case3 = self.BVAdd(self.BVNeg(u), t)
        case4 = self.BVAdd(u, t)
        case5 = self.BVNeg(u)

        return self.Ite(self.Or(cond1, cond2), u,
                        self.Ite(cond3, case3, self.Ite(cond4, case4, case5)))
def BVSMod ( self , left , right ) : # According to SMT-LIB standard (2015-06-23) BVSMod is defined as follows # http://smtlib.cs.uiowa.edu/logics-all.shtml#QF_BV # # For all terms s,t of sort (_ BitVec m), where 0 < m, # (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)))))))) m = left . bv_width ( ) s = left t = right zero_1 = self . BV ( "#b0" ) one_1 = self . BV ( "#b1" ) msb_s = self . BVExtract ( s , m - 1 , m - 1 ) msb_t = self . BVExtract ( t , m - 1 , m - 1 ) abs_s = self . Ite ( self . Equals ( msb_s , zero_1 ) , s , self . BVNeg ( s ) ) abs_t = self . Ite ( self . Equals ( msb_t , zero_1 ) , t , self . BVNeg ( t ) ) u = self . BVURem ( abs_s , abs_t ) cond1 = self . Equals ( u , self . BV ( 0 , m ) ) cond2 = self . And ( self . Equals ( msb_s , zero_1 ) , self . Equals ( msb_t , zero_1 ) ) cond3 = self . And ( self . Equals ( msb_s , one_1 ) , self . Equals ( msb_t , zero_1 ) ) cond4 = self . And ( self . Equals ( msb_s , zero_1 ) , self . Equals ( msb_t , one_1 ) ) case3 = self . BVAdd ( self . BVNeg ( u ) , t ) case4 = self . BVAdd ( u , t ) case5 = self . BVNeg ( u ) return self . Ite ( self . Or ( cond1 , cond2 ) , u , self . Ite ( cond3 , case3 , self . Ite ( cond4 , case4 , case5 ) ) )