Skip to content

Instantly share code, notes, and snippets.

@pi8027

pi8027/gist:0431323b827137994ac5

Created May 15, 2014 10:21
Show Gist options
  • Save pi8027/0431323b827137994ac5 to your computer and use it in GitHub Desktop.
Save pi8027/0431323b827137994ac5 to your computer and use it in GitHub Desktop.
Download ZIP
Z3
Raw
gistfile1.txt
(define-fun sub ((x Int) (y Int)) Int
(ite (< x y) 0 (- x y)))
(define-fun minn ((x Int) (y Int)) Int
(sub x (sub x y)))
(define-fun maxn ((x Int) (y Int)) Int
(+ x (sub y x)))
(assert (forall ((x Int) (y Int))
(implies (and (<= 0 x) (<= 0 y))
(= (minn x y) (minn y x)))))
(check-sat)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment