File size: 896 Bytes
32cdebd |
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 |
; max3.sl
; Synthesize the maximum of 3 integers, from a purely declarative spec
(set-logic LIA)
(synth-fun max3 ((x Int) (y Int) (z Int)) Int
((Start Int (x
y
z
0
1
(+ Start Start)
(- Start Start)
(ite StartBool Start Start)))
(StartBool Bool ((and StartBool StartBool)
(or StartBool StartBool)
(not StartBool)
(<= Start Start)
(= Start Start)
(>= Start Start)))))
(declare-var x Int)
(declare-var y Int)
(declare-var z Int)
(constraint (>= (max3 x y z) x))
(constraint (>= (max3 x y z) y))
(constraint (>= (max3 x y z) z))
(constraint (or (= x (max3 x y z))
(or (= y (max3 x y z))
(= z (max3 x y z)))))
(check-synth)
|