gcd.smt2

; This example illustrates basic arithmetic and 
; uninterpreted functions

(declare-fun x () Int)
(declare-fun y () Int)
(declare-fun z () Int)
(declare-fun gcd3 (Int Int Int) Int)
(declare-fun gcd2 (Int Int) Int)
(declare-fun result () Int)



(assert (= x 1071))
(assert (= y 462))
(assert (= z 7))

(assert (= result (gcd3 x y z)))
(assert (= (gcd3 x y z) (gcd2 x (gcd2 y z))))


;(assert (forall (a Int) (b Int) (q Int) 
;                (and 
;                  (= a (+ (* b q) (mod a b)))
;                  (= 0 (mod a (gcd a b)))
;                  (= 0 (mod b (gcd a b)))
;                )
;        )
;)
;(assert (= (div a (gcd a b)) 0))
;(assert (= (div b (gcd a b)) 0))

;(assert (= (gcd a b) (gcd b (mod a b)) (gcd (mod a b) (mod b (mod a b))) ))
;(assert (= gcd_a b))
;(assert (= gcd_b (mod a b)))
;(assert (= gcd_b (gcd gcd_a gcd_b)))



;(assert (and (= (mod x (gcd y (mod x y))) 0) (= (mod y (gcd y (mod x y))) 0)))
;(assert (or (not (> a b)) (= x (gcd (- a b) b))))
;(assert (or (not (< a b)) (= x (gcd a (- b a)))))

;(assert (= (gcd a b) (gcd b (mod a b))))
;(assert (= a (*b x)))


;(assert (= x (gcd a b)))

(check-sat)
(get-model)