blob: 37ed848efbf93ddb886622840b8daa5b4a06ac01 (
plain)
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
|
; EXPECT: unsat
; COMMAND-LINE: --cegqi-si=all --sygus-out=status
(set-logic LIA)
(synth-fun max ((x Int) (y Int)) Int
((Start Int (0 1 x y
(+ Start Start)
(- Start Start)
(ite StartBool Start Start)))
(StartBool Bool ((and StartBool StartBool)
(not StartBool)
(<= Start Start)))))
;(synth-fun min ((x Int) (y Int)) Int
; ((Start Int ((Constant Int) (Variable Int)
; (+ Start Start)
; (- Start Start)
; (ite StartBool Start Start)))
; (StartBool Bool ((and StartBool StartBool)
; (not StartBool)
; (<= Start Start)))))
(declare-var x Int)
(declare-var y Int)
(constraint (>= (max x y) x))
(constraint (>= (max x y) y))
(constraint (or (= x (max x y))
(= y (max x y))))
;(constraint (= (+ (max x y) (min x y))
; (+ x y)))
(check-synth)
|
