Created
November 11, 2019 16:10
-
-
Save corwin-of-amber/03566e0dd7c06f558b9dc4b5620e5c7c to your computer and use it in GitHub Desktop.
SuSLik pure synthesis mini-benchmarks
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
; 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) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
; 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) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
; 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) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
; 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) |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment