test/regress/regress0/sygus/sygus-uf.sy


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20

(set-logic LIA)

(declare-fun uf (Int) Int)

(synth-fun f ((x Int) (y Int)) Bool
  ((Start Bool (true false
                (<= IntExpr IntExpr)
                (= IntExpr IntExpr)
                (and Start Start)
                (or Start Start)
                (not Start)))
   (IntExpr Int (0 1 x y
                 (+ IntExpr IntExpr)
                 (- IntExpr IntExpr)))))

(declare-var x Int)

(constraint (f (uf x) (uf x)))

(check-synth)