SuSLik pure synthesis mini-benchmarks

01-sll_init.sy

; EXPECT: unsat
; COMMAND-LINE: --cegqi-si=all --sygus-out=status
(set-logic UF)

(declare-var x Int)
(declare-var v Int)

(synth-fun target ((x Int) (v Int)) Int
  ((Start Int (0 1 x v))))


(declare-var z Int)

(declare-fun s12 (Int) Bool)

; exists v2  [= (target x v)]
(constraint (=> 
    (forall ((z Int)) (=> (s12 z) (= z v)))                           ; s12 <= {v}
    (forall ((z Int)) (=> (or (= z (target x v)) (s12 z)) (= z v)))   ; {v2} + s12 <= v
))

(check-synth)

02-sll_singleton.sy

; EXPECT: unsat
; COMMAND-LINE: --cegqi-si=all --sygus-out=status
(set-logic UF)

(declare-var x Int)
(declare-var y Int)

(synth-fun target ((x Int) (y Int)) Int
  ((Start Int (0 1 x y))))


(declare-var z Int)

; exists v2  [= (target x y)]
(constraint
    (forall ((z Int)) (= (= z (target x y)) (= z x)))   ; {x} = {v}
)

(check-synth)

03-tree_flatten_acc.sy

; EXPECT: unsat
; COMMAND-LINE: --cegqi-si=all --sygus-out=status
(set-logic UF)

(declare-sort Loc 0)

(declare-var t3 Loc)
(declare-var t22 Loc)
(declare-var t12 Loc)
(declare-var r2 Loc)
(declare-var l2 Loc)
(declare-var v2 Int)
(declare-var y2 Loc)
(declare-var x Loc)
(declare-var z Loc)

(synth-fun target ((t2 Loc) (t22 Loc) (t12 Loc) (r2 Loc) (l2 Loc) (v2 Int) (y2 Loc) (x Loc) (z Loc)) Int
  ((Start Int (v2 0 1))))


(declare-fun s (Int) Bool)
(declare-fun s2 (Int) Bool)
(declare-fun s11 (Int) Bool)
(declare-fun s12 (Int) Bool)
(declare-fun s13 (Int) Bool)
(declare-fun acc (Int) Bool)

; exists v1  [= (target t3 t22 t12 r2 l2 v2 y2 x z)]
(constraint (=>
    (and 
      (forall ((q Int)) (= (s q) (or (= q v2) (s11 q) (s2 q))))           ; s = {v2} + s11 + s2
      (forall ((q Int)) (= (s12 q) (or (s11 q) (acc q))))                 ; s12 = s11 + acc
      (forall ((q Int)) (= (s13 q) (or (s2 q) (s12 q)))))                 ; s13 = s2 + s12
    (forall ((q Int)) (= (or (s q) (acc q)) 
           (or (= q (target t3 t22 t12 r2 l2 v2 y2 x z)) (s13 q))))       ; s + acc = {v1} + s13
))

(check-synth)

04-strl_prepend.sy

; EXPECT: unsat
; COMMAND-LINE: --cegqi-si=all --sygus-out=status
(set-logic UF)

(declare-var y2 Int)
(declare-var a2 Int)
(declare-var x Int)
(declare-var k Int)
(declare-var r Int)
(declare-var lo Int)

(synth-fun target ((y2 Int) (a2 Int) (x Int) (k Int) (r Int) (lo Int)) Int
  ((Start Int (0 1 y2 a2 x k r lo))))


; exists v  [= (target y2 a2 x k r lo)]
(constraint (=>
    (and
      (<= 0 k) (<= k 7) (<= k lo))
    (and
      (= k (ite (<= (target y2 a2 x k r lo) lo) (target y2 a2 x k r lo) lo))
      (<= (target y2 a2 x k r lo) lo)
      (<= 0 (target y2 a2 x k r lo)) (<= (target y2 a2 x k r lo) 7))
))

(check-synth)