Skip to content

Instantly share code, notes, and snippets.

@Rufflewind
Last active July 4, 2021 21:13
Show Gist options
  • Save Rufflewind/a880e03fb0d13644a1e8 to your computer and use it in GitHub Desktop.
Save Rufflewind/a880e03fb0d13644a1e8 to your computer and use it in GitHub Desktop.
Truncated integer division in Z3
(declare-fun a () Int)
(declare-fun b () Int)
(declare-fun c () Int)
;; (assert (= a (div -7 -3)))
;; (assert (= b (div 7 -3)))
;; (assert (= c (div -7 3)))
;; (assert (= a (mod -7 -3)))
;; (assert (= b (mod 7 -3)))
;; (assert (= c (mod -7 3)))
;; C-style truncated division/modulus
(define-fun truncdiv ((x Int) (y Int)) Int
(ite (or (= (mod x y) 0) (>= x 0))
(div x y)
(ite (>= y 0)
(+ (div x y) 1)
(- (div x y) 1))))
(define-fun truncmod ((x Int) (y Int)) Int
(- x (* (truncdiv x y) y)))
;; (assert (= a (truncdiv -7 -3)))
;; (assert (= b (truncdiv 7 -3)))
;; (assert (= c (truncdiv -7 3)))
(assert (= a (truncmod -7 -3)))
(assert (= b (truncmod 7 -3)))
(assert (= c (truncmod -7 3)))
(check-sat)
(get-model)
(exit)
(declare-fun MIN () Int)
(declare-fun MAX () Int)
(assert
(and
;; signed integer
(= MAX 2147483647)
(or
;; 2s complement
(= (+ MIN 1) (- MAX))
;; 1s complement / signed zero
(= MIN (- MAX))
)
;; unsigned integer
;; (= MAX 4294967295)
;; (= MIN 0)
))
(define-fun truncdiv ((x Int) (y Int)) Int
(ite (or (= (mod x y) 0) (>= x 0))
(div x y)
(ite (>= y 0)
(+ (div x y) 1)
(- (div x y) 1))))
(define-fun truncmod ((x Int) (y Int)) Int
(- x (* (truncdiv x y) y)))
(declare-fun x () Int)
(declare-fun y () Int)
(declare-fun q () Int)
(declare-fun r () Int)
(assert
(and
(>= x MIN) (<= x MAX)
(>= y MIN) (<= y MAX)
;; search for integer overflow
(not (and
(>= q MIN) (<= q MAX)
(>= r MIN) (<= r MAX)
))
;; preconditions
(not (= y 0))
(not (and (not (= (- MAX) MIN)) (= x MIN) (= y -1)))
;; perform division
(= q (truncdiv x y))
(= r (truncmod x y))
)
)
(check-sat)
(get-model)
(exit)
(declare-fun MIN () Int)
(declare-fun MAX () Int)
(assert (= MAX 2147483647))
(assert (or
;; 2s complement
(= (+ MIN 1) (- MAX))
;; 1s complement / signed zero
(= MIN (- MAX))
))
(define-fun truncdiv ((x Int) (y Int)) Int
(ite (or (= (mod x y) 0) (>= x 0))
(div x y)
(ite (>= y 0)
(+ (div x y) 1)
(- (div x y) 1))))
(define-fun truncmod ((x Int) (y Int)) Int
(- x (* (truncdiv x y) y)))
(declare-fun x () Int)
(declare-fun y () Int)
(declare-fun q () Int)
(declare-fun r () Int)
(declare-fun q2 () Int)
(declare-fun r2 () Int)
(assert
(and
(>= x MIN) (<= x MAX)
(>= y MIN) (<= y MAX)
(>= q MIN) (<= q MAX)
(>= r MIN) (<= r MAX)
;; search for integer overflow
(not (and
(>= q2 MIN) (<= q2 MAX)
(>= r2 MIN) (<= r2 MAX)
))
;; preconditions
(not (= y 0)) (not (and (not (= (- MAX) MIN)) (= x MIN) (= y -1)))
;; perform division
(= q (truncdiv x y))
(= r (truncmod x y))
;; sub-precondition: r && (x < 0) != (y < 0)
(not (= r 0)) (not (= (< x 0) (< y 0)))
(= q2 (- q 1))
(= r2 (+ r y))
)
)
(check-sat)
(get-model)
(exit)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment