blob: ff2be7b227c570211490f5c3915b89fe402ae3d2 (
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
|
; COMMAND-LINE: --sygus-si=all --dag-thresh=0
; EXPECT: (
; EXPECT: (define-fun f1 ((x Bool) (y Bool)) Bool (ite true true false))
; EXPECT: (define-fun f2 ((x Bool) (y Bool)) Bool (ite x (ite y false (not false)) (not (ite false false (not false)))))
; EXPECT: )
; Test ensures that the solution does not contain a random variable
(set-logic UF)
(synth-fun f1 ((x Bool) (y Bool)) Bool
((Start Bool))
((Start Bool (false (ite true true Start)))))
(synth-fun f2 ((x Bool) (y Bool)) Bool
((Start Bool))
((Start Bool (false x y (ite Start Start (not Start))))))
(declare-var x Bool)
(declare-var y Bool)
(constraint (= (f1 x y) true))
(constraint (= (f2 x y) (not (ite x y true))))
(check-synth)
|
