diff options
Diffstat (limited to 'test/regress/regress1/sygus')
54 files changed, 975 insertions, 603 deletions
diff --git a/test/regress/regress1/sygus/Base16_1.sy b/test/regress/regress1/sygus/Base16_1.sy new file mode 100644 index 000000000..b54c7688b --- /dev/null +++ b/test/regress/regress1/sygus/Base16_1.sy @@ -0,0 +1,34 @@ +; EXPECT: unsat +; COMMAND-LINE: --sygus-qe-preproc --cbqi-full --sygus-out=status --cegqi-si=all +(set-logic BV) + +(define-fun B ((h (BitVec 8)) (l (BitVec 8)) (v (BitVec 8))) (BitVec 8) (bvlshr (bvshl v (bvsub #x07 h)) (bvsub #x07 (bvsub h l)))) + +(define-fun E ((x (BitVec 8))) (BitVec 8) (bvadd x #x41)) + +(define-fun f ((x (BitVec 8))) (BitVec 8) (bvsub x #x41)) + +(define-fun d ((x (BitVec 8))) Bool (bvule x #x3f)) + +(synth-fun D ((x (BitVec 8)) (y (BitVec 8)) ) (BitVec 8) + ((Start (BitVec 8) ( + (f Start) x y Const + (bvshl Start Start) (bvnot Start) + (bvand Start Start) + (bvxor Start Start) + (bvor Start Start) + (bvneg Start) + (bvadd Start Start) + (bvlshr Start Start) + (bvsub Start Start) + )) + (Const (BitVec 8) (#x01 #x03 #x06 #x07 #x04 #x05 #x02 #x00)) +)) + +(declare-var x (BitVec 8)) +(constraint (= x (D (E (B #x07 #x04 x) ) (E (B #x03 #x00 x)) )) ) + +; notice we don't have solution reconstruction for this +(check-synth) + + diff --git a/test/regress/regress1/sygus/MPwL_d1s3.sy b/test/regress/regress1/sygus/MPwL_d1s3.sy deleted file mode 100644 index 5178cf86b..000000000 --- a/test/regress/regress1/sygus/MPwL_d1s3.sy +++ /dev/null @@ -1,151 +0,0 @@ -; EXPECT: unsat -; COMMAND-LINE: --sygus-out=status -(set-logic LIA) - -(define-fun get-y ((currPoint Int)) Int -(ite (< currPoint 10) 0 (ite (< currPoint 20) 1 (ite (< currPoint 30) 2 (ite (< currPoint 40) 3 (ite (< currPoint 50) 4 (ite (< currPoint 60) 5 (ite (< currPoint 70) 6 (ite (< currPoint 80) 7 (ite (< currPoint 90) 8 9)))))))))) - -(define-fun get-x ((currPoint Int)) Int - (- currPoint (* (get-y currPoint) 10))) -(define-fun interpret-move (( currPoint Int ) ( move Int)) Int -(ite (= move 0) currPoint -(ite (= move 1) (ite (or (< (+ (get-y currPoint) 1) 0) (>= (+ (get-y currPoint) 1) 10)) currPoint (+ currPoint 10)) -(ite (= move 2) (ite (or (< (+ (get-x currPoint) 1) 0) (>= (+ (get-x currPoint) 1) 10)) currPoint (+ currPoint 1)) -(ite (= move 3) (ite (or (< (+ (get-y currPoint) -1) 0) (>= (+ (get-y currPoint) -1) 10)) currPoint (+ currPoint -10)) -(ite (= move 4) (ite (or (< (+ (get-x currPoint) -1) 0) (>= (+ (get-x currPoint) -1) 10)) currPoint (+ currPoint -1)) -currPoint)))))) - -(define-fun interpret-move-obstacle-0 (( currPoint Int ) ( move Int)) Int -(ite (= move 0) (ite (or (< (+ (get-y currPoint) 1) 0) (>= (+ (get-y currPoint) 1) 10)) currPoint (+ currPoint 10)) -(ite (= move 1) (ite (or (< (+ (get-y currPoint) -1) 0) (>= (+ (get-y currPoint) -1) 10)) currPoint (+ currPoint -10)) -currPoint))) - -(define-fun interpret-move-obstacle-1 (( currPoint Int ) ( move Int)) Int -(ite (= move 0) (ite (or (< (+ (get-y currPoint) 1) 0) (>= (+ (get-y currPoint) 1) 10)) currPoint (+ currPoint 10)) -(ite (= move 1) currPoint -(ite (= move 2) (ite (or (< (+ (get-y currPoint) -1) 0) (>= (+ (get-y currPoint) -1) 10)) currPoint (+ currPoint -10)) -currPoint)))) - -(define-fun allowable-move-obstacle-0 (( start Int ) ( end Int)) Bool - (or (= (interpret-move-obstacle-0 start 0) end) - (or (= (interpret-move-obstacle-0 start 1) end) false))) - -(define-fun allowable-move-obstacle-1 (( start Int ) ( end Int)) Bool - (or (= (interpret-move-obstacle-1 start 0) end) - (or (= (interpret-move-obstacle-1 start 1) end) - (or (= (interpret-move-obstacle-1 start 2) end) false)))) - -(define-fun get-move-obstacle-0 (( start Int ) ( end Int)) Int - (ite (= (interpret-move-obstacle-0 start 0) end) 0 - (ite (= (interpret-move-obstacle-0 start 1) end) 1 -1))) - -(define-fun get-move-obstacle-1 (( start Int ) ( end Int)) Int - (ite (= (interpret-move-obstacle-1 start 0) end) 0 - (ite (= (interpret-move-obstacle-1 start 1) end) 1 - (ite (= (interpret-move-obstacle-1 start 2) end) 2 -1)))) - -(define-fun no-overlap-one-move-combination-2-2 ((p0 Int) (p1 Int) (p2 Int) (p3 Int)) Bool - (and (not (= p0 p2)) (and (not (= p0 p3)) (and (not (= p1 p2)) (and (not (= p1 p3)) true))))) - -(define-fun no-overlaps-0 (( currPoint Int ) ( move Int) (obstacleCurrPoint Int) (obstacleMove Int)) Bool - (= 1 - (ite (= move 0) - (ite (= obstacleMove 0) (ite (no-overlap-one-move-combination-2-2 currPoint (+ (+ currPoint 0) 0) obstacleCurrPoint (+ (+ obstacleCurrPoint 0) 10)) 1 0) - (ite (= obstacleMove 1) (ite (no-overlap-one-move-combination-2-2 currPoint (+ (+ currPoint 0) 0) obstacleCurrPoint (+ (+ obstacleCurrPoint 0) -10)) 1 0) 0)) - (ite (= move 1) - (ite (= obstacleMove 0) (ite (no-overlap-one-move-combination-2-2 currPoint (+ (+ currPoint 0) 10) obstacleCurrPoint (+ (+ obstacleCurrPoint 0) 10)) 1 0) - (ite (= obstacleMove 1) (ite (no-overlap-one-move-combination-2-2 currPoint (+ (+ currPoint 0) 10) obstacleCurrPoint (+ (+ obstacleCurrPoint 0) -10)) 1 0) 0)) - (ite (= move 2) - (ite (= obstacleMove 0) (ite (no-overlap-one-move-combination-2-2 currPoint (+ (+ currPoint 1) 0) obstacleCurrPoint (+ (+ obstacleCurrPoint 0) 10)) 1 0) - (ite (= obstacleMove 1) (ite (no-overlap-one-move-combination-2-2 currPoint (+ (+ currPoint 1) 0) obstacleCurrPoint (+ (+ obstacleCurrPoint 0) -10)) 1 0) 0)) - (ite (= move 3) - (ite (= obstacleMove 0) (ite (no-overlap-one-move-combination-2-2 currPoint (+ (+ currPoint 0) -10) obstacleCurrPoint (+ (+ obstacleCurrPoint 0) 10)) 1 0) - (ite (= obstacleMove 1) (ite (no-overlap-one-move-combination-2-2 currPoint (+ (+ currPoint 0) -10) obstacleCurrPoint (+ (+ obstacleCurrPoint 0) -10)) 1 0) 0)) - (ite (= move 4) - (ite (= obstacleMove 0) (ite (no-overlap-one-move-combination-2-2 currPoint (+ (+ currPoint -1) 0) obstacleCurrPoint (+ (+ obstacleCurrPoint 0) 10)) 1 0) - (ite (= obstacleMove 1) (ite (no-overlap-one-move-combination-2-2 currPoint (+ (+ currPoint -1) 0) obstacleCurrPoint (+ (+ obstacleCurrPoint 0) -10)) 1 0) 0)) 0))))))) - -(define-fun no-overlaps-1 (( currPoint Int ) ( move Int) (obstacleCurrPoint Int) (obstacleMove Int)) Bool - (= 1 - (ite (= move 0) - (ite (= obstacleMove 0) (ite (no-overlap-one-move-combination-2-2 currPoint (+ (+ currPoint 0) 0) obstacleCurrPoint (+ (+ obstacleCurrPoint 0) 10)) 1 0) - (ite (= obstacleMove 1) (ite (no-overlap-one-move-combination-2-2 currPoint (+ (+ currPoint 0) 0) obstacleCurrPoint (+ (+ obstacleCurrPoint 0) 0)) 1 0) - (ite (= obstacleMove 2) (ite (no-overlap-one-move-combination-2-2 currPoint (+ (+ currPoint 0) 0) obstacleCurrPoint (+ (+ obstacleCurrPoint 0) -10)) 1 0) 0))) - (ite (= move 1) - (ite (= obstacleMove 0) (ite (no-overlap-one-move-combination-2-2 currPoint (+ (+ currPoint 0) 10) obstacleCurrPoint (+ (+ obstacleCurrPoint 0) 10)) 1 0) - (ite (= obstacleMove 1) (ite (no-overlap-one-move-combination-2-2 currPoint (+ (+ currPoint 0) 10) obstacleCurrPoint (+ (+ obstacleCurrPoint 0) 0)) 1 0) - (ite (= obstacleMove 2) (ite (no-overlap-one-move-combination-2-2 currPoint (+ (+ currPoint 0) 10) obstacleCurrPoint (+ (+ obstacleCurrPoint 0) -10)) 1 0) 0))) - (ite (= move 2) - (ite (= obstacleMove 0) (ite (no-overlap-one-move-combination-2-2 currPoint (+ (+ currPoint 1) 0) obstacleCurrPoint (+ (+ obstacleCurrPoint 0) 10)) 1 0) - (ite (= obstacleMove 1) (ite (no-overlap-one-move-combination-2-2 currPoint (+ (+ currPoint 1) 0) obstacleCurrPoint (+ (+ obstacleCurrPoint 0) 0)) 1 0) - (ite (= obstacleMove 2) (ite (no-overlap-one-move-combination-2-2 currPoint (+ (+ currPoint 1) 0) obstacleCurrPoint (+ (+ obstacleCurrPoint 0) -10)) 1 0) 0))) - (ite (= move 3) - (ite (= obstacleMove 0) (ite (no-overlap-one-move-combination-2-2 currPoint (+ (+ currPoint 0) -10) obstacleCurrPoint (+ (+ obstacleCurrPoint 0) 10)) 1 0) - (ite (= obstacleMove 1) (ite (no-overlap-one-move-combination-2-2 currPoint (+ (+ currPoint 0) -10) obstacleCurrPoint (+ (+ obstacleCurrPoint 0) 0)) 1 0) - (ite (= obstacleMove 2) (ite (no-overlap-one-move-combination-2-2 currPoint (+ (+ currPoint 0) -10) obstacleCurrPoint (+ (+ obstacleCurrPoint 0) -10)) 1 0) 0))) - (ite (= move 4) - (ite (= obstacleMove 0) (ite (no-overlap-one-move-combination-2-2 currPoint (+ (+ currPoint -1) 0) obstacleCurrPoint (+ (+ obstacleCurrPoint 0) 10)) 1 0) - (ite (= obstacleMove 1) (ite (no-overlap-one-move-combination-2-2 currPoint (+ (+ currPoint -1) 0) obstacleCurrPoint (+ (+ obstacleCurrPoint 0) 0)) 1 0) - (ite (= obstacleMove 2) (ite (no-overlap-one-move-combination-2-2 currPoint (+ (+ currPoint -1) 0) obstacleCurrPoint (+ (+ obstacleCurrPoint 0) -10)) 1 0) 0))) 0))))))) - -(define-fun no-overlaps-one-step-helper ((currPoint Int) (move Int) (o0-t Int) (o0move Int) (o1-t Int) (o1move Int)) Bool - (and (no-overlaps-0 currPoint move o0-t o0move) (and (no-overlaps-1 currPoint move o1-t o1move) true))) - -(define-fun no-overlaps-one-step ((currPoint Int) (move Int) (o0-0 Int) (o0-1 Int) (o1-0 Int) (o1-1 Int)) Bool - (no-overlaps-one-step-helper currPoint move o0-0 (get-move-obstacle-0 o0-0 o0-1) o1-0 (get-move-obstacle-1 o1-0 o1-1))) - - - -(declare-var o0-1 Int) -(declare-var o0-2 Int) -(declare-var o0-3 Int) -(declare-var o1-1 Int) -(declare-var o1-2 Int) -(declare-var o1-3 Int) - -(synth-fun move ((currPoint Int) (o0 Int) (o1 Int)) Int - ((Start Int ( - MoveId - (ite StartBool Start Start))) - (MoveId Int (0 - 1 - 2 - 3 - 4 - )) - (CondInt Int ( - (get-y currPoint) ;y coord - (get-x currPoint) ;x coord - (get-y o0) - (get-x o0) - (get-y o1) - (get-x o1) - (+ CondInt CondInt) - (- CondInt CondInt) - -1 - 0 - 1 - 2 - 3 - 4 - 5 - 6 - 7 - 8 - 9 - )) - (StartBool Bool ((and StartBool StartBool) - (or StartBool StartBool) - (not StartBool) - (<= CondInt CondInt) - (= CondInt CondInt) - (>= CondInt CondInt))))) - - (constraint (let ((pos0 Int 0)) (let ((mov0 Int (move pos0 99 98))) (let ((pos1 Int (interpret-move pos0 mov0))) (let ((mov1 Int (move pos1 o0-1 o1-1))) (let ((pos2 Int (interpret-move pos1 mov1))) (let ((mov2 Int (move pos2 o0-2 o1-2))) (let ((pos3 Int (interpret-move pos2 mov2))) - (or - (and - (= pos3 30) - (and (no-overlaps-one-step pos0 mov0 99 o0-1 98 o1-1) (and (no-overlaps-one-step pos1 mov1 o0-1 o0-2 o1-1 o1-2) (and (no-overlaps-one-step pos2 mov2 o0-2 o0-3 o1-2 o1-3) true)))) - (not (and (allowable-move-obstacle-0 99 o0-1) (and (allowable-move-obstacle-0 o0-1 o0-2) (and (allowable-move-obstacle-0 o0-2 o0-3) (and (allowable-move-obstacle-1 98 o1-1) (and (allowable-move-obstacle-1 o1-1 o1-2) (and (allowable-move-obstacle-1 o1-2 o1-3) true)))))))))))))))) - -(check-synth) diff --git a/test/regress/regress1/sygus/Makefile.am b/test/regress/regress1/sygus/Makefile.am index b2a428bd1..c44c5034d 100644 --- a/test/regress/regress1/sygus/Makefile.am +++ b/test/regress/regress1/sygus/Makefile.am @@ -16,23 +16,61 @@ endif # These are run for all build profiles. # If a test shouldn't be run in e.g. competition mode, # put it below in "TESTS +=" -TESTS = \ +TESTS = \ hd-sdiv.sy \ stopwatch-bt.sy \ - array_sum_dd.sy \ - mpg_guard1-dd.sy \ VC22_a.sy \ - inv_gen_n_c11.sy \ unbdd_inv_gen_ex7.sy \ - icfp_easy_mt_ite.sy \ - three.sy \ - nia-max-square.sy \ - MPwL_d1s3.sy \ - process-arg-invariance.sy \ real-grammar.sy \ - lustre-real.sy + cegar1.sy \ + cggmp.sy \ + clock-inc-tuple.sy \ + dup-op.sy \ + fg_polynomial3.sy \ + hd-01-d1-prog.sy \ + icfp_14.12.sy \ + icfp_14.12-flip-args.sy \ + icfp_28_10.sy \ + icfp_easy-ite.sy \ + inv-example.sy \ + inv-unused.sy \ + multi-fun-polynomial2.sy \ + no-flat-simp.sy \ + process-10-vars.sy \ + tl-type.sy \ + tl-type-4x.sy \ + twolets2-orig.sy \ + unbdd_inv_gen_winf1.sy \ + array_search_2.sy \ + array_sum_2_5.sy \ + commutative.sy \ + constant.sy \ + dt-test-ns.sy \ + hd-19-d1-prog-dup-op.sy \ + list-head-x.sy \ + max.sy \ + nflat-fwd-3.sy \ + nflat-fwd.sy \ + nia-max-square-ns.sy \ + no-mention.sy \ + qe.sy \ + strings-concat-3-args.sy \ + strings-double-rec.sy \ + strings-small.sy \ + strings-template-infer-unused.sy \ + strings-template-infer.sy \ + strings-trivial-simp.sy \ + strings-trivial-two-type.sy \ + strings-trivial.sy \ + sygus-dt.sy \ + tl-type-0.sy \ + triv-type-mismatch-si.sy \ + twolets1.sy -EXTRA_DIST = $(TESTS) +EXTRA_DIST = $(TESTS) \ + enum-test.sy + +# Base16_1.sy # synonyms for "check" in this directory .PHONY: regress regress1 test diff --git a/test/regress/regress1/sygus/array_search_2.sy b/test/regress/regress1/sygus/array_search_2.sy new file mode 100644 index 000000000..41346e655 --- /dev/null +++ b/test/regress/regress1/sygus/array_search_2.sy @@ -0,0 +1,11 @@ +; EXPECT: unsat +; COMMAND-LINE: --cegqi-si=all --sygus-out=status +(set-logic LIA) +(synth-fun findIdx ( (y1 Int) (y2 Int) (k1 Int)) Int ((Start Int ( 0 1 2 y1 y2 k1 (ite BoolExpr Start Start))) (BoolExpr Bool ((< Start Start) (<= Start Start) (> Start Start) (>= Start Start))))) +(declare-var x1 Int) +(declare-var x2 Int) +(declare-var k Int) +(constraint (=> (< x1 x2) (=> (< k x1) (= (findIdx x1 x2 k) 0)))) +(constraint (=> (< x1 x2) (=> (> k x2) (= (findIdx x1 x2 k) 2)))) +(constraint (=> (< x1 x2) (=> (and (> k x1) (< k x2)) (= (findIdx x1 x2 k) 1)))) +(check-synth) diff --git a/test/regress/regress1/sygus/array_sum_2_5.sy b/test/regress/regress1/sygus/array_sum_2_5.sy new file mode 100644 index 000000000..84a75d086 --- /dev/null +++ b/test/regress/regress1/sygus/array_sum_2_5.sy @@ -0,0 +1,9 @@ +; EXPECT: unsat +; COMMAND-LINE: --cegqi-si=all --sygus-out=status +(set-logic LIA) +(synth-fun findSum ( (y1 Int) (y2 Int) )Int ((Start Int ( 0 1 2 y1 y2 (+ Start Start) (ite BoolExpr Start Start))) (BoolExpr Bool ((< Start Start) (<= Start Start) (> Start Start) (>= Start Start))))) +(declare-var x1 Int) +(declare-var x2 Int) +(constraint (=> (> (+ x1 x2) 5) (= (findSum x1 x2 ) (+ x1 x2)))) +(constraint (=> (<= (+ x1 x2) 5) (= (findSum x1 x2 ) 0))) +(check-synth) diff --git a/test/regress/regress1/sygus/array_sum_dd.sy b/test/regress/regress1/sygus/array_sum_dd.sy deleted file mode 100644 index 6d3354d2d..000000000 --- a/test/regress/regress1/sygus/array_sum_dd.sy +++ /dev/null @@ -1,11 +0,0 @@ -; EXPECT: unsat -; COMMAND-LINE: --sygus-out=status -(set-logic LIA) -(synth-fun findSum ( (y1 Int) (y2 Int) )Int ( -(Start Int ( 0 1 y1 y2 (+ Start Start) (ite BoolExpr Start Start))) -(BoolExpr Bool ((< Start Start) (<= Start Start))))) -(declare-var x1 Int) -(declare-var x2 Int) -(constraint (=> (> (+ x1 x2) 0) (= (findSum x1 x2 ) x1))) -(constraint (=> (<= (+ x1 x2) 0) (= (findSum x1 x2 ) x2))) -(check-synth) diff --git a/test/regress/regress1/sygus/cegar1.sy b/test/regress/regress1/sygus/cegar1.sy new file mode 100644 index 000000000..ee85db88a --- /dev/null +++ b/test/regress/regress1/sygus/cegar1.sy @@ -0,0 +1,23 @@ +; EXPECT: unsat +; COMMAND-LINE: --sygus-inv-templ=post --sygus-out=status +(set-logic LIA) + +(synth-inv inv-f ((x Int) (y Int))) + +(declare-primed-var x Int) +(declare-primed-var y Int) + +(define-fun pre-f ((x Int) (y Int)) Bool +(and (and (>= x 0) +(and (<= x 2) +(<= y 2))) (>= y 0))) + +(define-fun trans-f ((x Int) (y Int) (x! Int) (y! Int)) Bool +(and (= x! (+ x 2)) (= y! (+ y 2)))) + +(define-fun post-f ((x Int) (y Int)) Bool +(not (and (= x 4) (= y 0)))) + +(inv-constraint inv-f pre-f trans-f post-f) + +(check-synth) diff --git a/test/regress/regress1/sygus/cggmp.sy b/test/regress/regress1/sygus/cggmp.sy new file mode 100644 index 000000000..a3247e4f4 --- /dev/null +++ b/test/regress/regress1/sygus/cggmp.sy @@ -0,0 +1,23 @@ +; EXPECT: unsat +; COMMAND-LINE: --sygus-inv-templ=pre --sygus-out=status + +(set-logic LIA) + +(synth-inv inv-f ((i Int) (j Int))) + +(declare-primed-var i Int) +(declare-primed-var j Int) + +(define-fun pre-f ((i Int) (j Int)) Bool +(and (= i 1) +(= j 10))) + +(define-fun trans-f ((i Int) (j Int) (i! Int) (j! Int)) Bool +(and (and (>= j i) (= i! (+ i 2))) (= j! (- j 1)))) + +(define-fun post-f ((i Int) (j Int)) Bool +(not (and (< j i) (not (= j 6))))) + +(inv-constraint inv-f pre-f trans-f post-f) + +(check-synth) diff --git a/test/regress/regress1/sygus/clock-inc-tuple.sy b/test/regress/regress1/sygus/clock-inc-tuple.sy new file mode 100644 index 000000000..43fd7c1ac --- /dev/null +++ b/test/regress/regress1/sygus/clock-inc-tuple.sy @@ -0,0 +1,14 @@ +; EXPECT: unsat +; COMMAND-LINE: --cegqi-si=all --sygus-out=status + +(set-logic ALL_SUPPORTED) +(declare-var m Int) +(declare-var s Int) +(declare-var inc Int) +(declare-datatypes ((tuple2 0)) ( ((tuple2 (_m Int) (_s Int))) )) + +(synth-fun x12 ((m Int) (s Int) (inc Int)) tuple2) +(constraint (=> +(and (>= m 0) (>= s 0) (< s 3) (> inc 0)) +(and (>= (_m (x12 m s inc)) 0) (>= (_s (x12 m s inc)) 0) (< (_s (x12 m s inc)) 3) (= (+ (* (_m (x12 m s inc)) 3) (_s (x12 m s inc))) (+ (+ (* m 3) s) inc))))) +(check-synth) diff --git a/test/regress/regress1/sygus/commutative.sy b/test/regress/regress1/sygus/commutative.sy new file mode 100644 index 000000000..24201b453 --- /dev/null +++ b/test/regress/regress1/sygus/commutative.sy @@ -0,0 +1,22 @@ +; EXPECT: unsat +; COMMAND-LINE: --sygus-out=status + +(set-logic LIA) + +(synth-fun comm ((x Int) (y Int)) Int + ((Start Int (x + y + (+ Start Start) + (- Start Start) + )) + )) + +(declare-var x Int) +(declare-var y Int) + +(constraint (= (comm x y) (comm y x))) + + +(check-synth) + +; (+ x y) is a valid solution diff --git a/test/regress/regress1/sygus/constant.sy b/test/regress/regress1/sygus/constant.sy new file mode 100644 index 000000000..1bb3e59fa --- /dev/null +++ b/test/regress/regress1/sygus/constant.sy @@ -0,0 +1,23 @@ +; EXPECT: unsat +; COMMAND-LINE: --sygus-out=status + +(set-logic LIA) + +(synth-fun constant ((x Int)) Int + ((Start Int (x + 0 + 1 + (+ Start Start) + (- Start Start) + )) + )) + +(declare-var x Int) +(declare-var y Int) + +(constraint (= (constant x) (constant y))) + + +(check-synth) + +; 0, 1, (- x x) are valid solutions diff --git a/test/regress/regress1/sygus/dt-test-ns.sy b/test/regress/regress1/sygus/dt-test-ns.sy new file mode 100644 index 000000000..a6e8ac5c2 --- /dev/null +++ b/test/regress/regress1/sygus/dt-test-ns.sy @@ -0,0 +1,14 @@ +; EXPECT: unsat +; COMMAND-LINE: --cegqi-si=all --sygus-out=status +(set-logic LIA) + +(declare-datatypes ((List 0)) (((cons (head Int) (tail List)) (nil)))) + +(synth-fun f ((x Int)) List) + +(declare-var x Int) + +(constraint (is-cons (f x))) +(constraint (and (= (head (f x)) x) (= (head (f x)) (+ 5 (head (tail (f x))))))) +(check-synth) + diff --git a/test/regress/regress1/sygus/dup-op.sy b/test/regress/regress1/sygus/dup-op.sy new file mode 100644 index 000000000..e2c69282e --- /dev/null +++ b/test/regress/regress1/sygus/dup-op.sy @@ -0,0 +1,11 @@ +; EXPECT: unsat +; COMMAND-LINE: --cegqi-si=none --sygus-out=status +(set-logic LIA) +(synth-fun f ((x Int)) Int + ((Start Int ((+ Con Con) (+ Start Start) x)) + (Con Int (0 1)))) + +(declare-var x Int) +(constraint (= (f x) (* 2 x))) +(check-synth) + diff --git a/test/regress/regress1/sygus/enum-test.sy b/test/regress/regress1/sygus/enum-test.sy new file mode 100644 index 000000000..47099eeed --- /dev/null +++ b/test/regress/regress1/sygus/enum-test.sy @@ -0,0 +1,8 @@ +; EXPECT: unsat +; COMMAND-LINE: --cegqi-si=all --sygus-out=status +(set-logic LIA) +(define-sort D (Enum (a b))) +(define-fun f ((x D)) Int (ite (= x D::a) 3 7)) +(synth-fun g () D ((Start D (D::a D::b)))) +(constraint (= (f g) 7)) +(check-synth) diff --git a/test/regress/regress1/sygus/fg_polynomial3.sy b/test/regress/regress1/sygus/fg_polynomial3.sy new file mode 100644 index 000000000..d70516bf1 --- /dev/null +++ b/test/regress/regress1/sygus/fg_polynomial3.sy @@ -0,0 +1,18 @@ +; EXPECT: unsat +; COMMAND-LINE: --sygus-out=status + +(set-logic LIA) + +(synth-fun addExpr1 ((x Int) (y Int)) Int +) + +(synth-fun addExpr2 ((x Int) (y Int)) Int +) + +(declare-var x Int) +(declare-var y Int) + +(constraint (= (+ (addExpr1 x y) (addExpr2 y x)) (- x (+ x y)))) + +(check-synth) + diff --git a/test/regress/regress1/sygus/hd-01-d1-prog.sy b/test/regress/regress1/sygus/hd-01-d1-prog.sy new file mode 100644 index 000000000..1379d4206 --- /dev/null +++ b/test/regress/regress1/sygus/hd-01-d1-prog.sy @@ -0,0 +1,22 @@ +; EXPECT: unsat +; COMMAND-LINE: --cegqi --sygus-out=status + +(set-logic BV) + +(define-fun hd01 ((x (BitVec 32))) (BitVec 32) (bvand x (bvsub x #x00000001))) + +(synth-fun f ((x (BitVec 32))) (BitVec 32) + ((Start (BitVec 32) ((bvand Start Start) + (bvsub Start Start) + (bvor Start Start) + (bvadd Start Start) + (bvxor Start Start) + x + #x00000000 + #xFFFFFFFF + #x00000001)))) + +(declare-var x (BitVec 32)) +(constraint (= (hd01 x) (f x))) +(check-synth) + diff --git a/test/regress/regress1/sygus/hd-19-d1-prog-dup-op.sy b/test/regress/regress1/sygus/hd-19-d1-prog-dup-op.sy new file mode 100644 index 000000000..abcfc2217 --- /dev/null +++ b/test/regress/regress1/sygus/hd-19-d1-prog-dup-op.sy @@ -0,0 +1,32 @@ +; EXPECT: unsat +; COMMAND-LINE: --cegqi-si=all --sygus-out=status + +(set-logic BV) + +(define-fun hd19 ((x (BitVec 32)) (m (BitVec 32)) (k (BitVec 32))) (BitVec 32) + (bvxor x (bvxor (bvshl (bvand (bvxor (bvlshr x k) x) m) k) (bvand (bvxor (bvlshr x k) x) m)))) + +; bvand is a duplicate +(synth-fun f ((x (BitVec 32)) (m (BitVec 32)) (k (BitVec 32))) (BitVec 32) + ((Start (BitVec 32) ((bvand Start Start) + (bvsub Start Start) + (bvxor Start Start) + (bvor Start Start) + (bvand Start Start) + (bvshl Start Start) + (bvlshr Start Start) + (bvashr Start Start) + (bvnot Start) + (bvneg Start) + x + m + k)))) + + +(declare-var x (BitVec 32)) +(declare-var m (BitVec 32)) +(declare-var k (BitVec 32)) + +(constraint (= (hd19 x m k) (f x m k))) +(check-synth) + diff --git a/test/regress/regress1/sygus/icfp_14.12-flip-args.sy b/test/regress/regress1/sygus/icfp_14.12-flip-args.sy new file mode 100644 index 000000000..a1e93cc44 --- /dev/null +++ b/test/regress/regress1/sygus/icfp_14.12-flip-args.sy @@ -0,0 +1,55 @@ +; EXPECT: unsat +; COMMAND-LINE: --sygus-out=status +(set-logic BV) + +(define-fun shr1 ((x (BitVec 64))) (BitVec 64) (bvlshr x #x0000000000000001)) +(define-fun shr4 ((x (BitVec 64))) (BitVec 64) (bvlshr x #x0000000000000004)) +(define-fun shr16 ((x (BitVec 64))) (BitVec 64) (bvlshr x #x0000000000000010)) +(define-fun shl1 ((x (BitVec 64))) (BitVec 64) (bvshl x #x0000000000000001)) +(define-fun if0 ((y (BitVec 64)) (x (BitVec 64)) (z (BitVec 64))) (BitVec 64) (ite (= x #x0000000000000001) y z)) + +(synth-fun f ( (x (BitVec 64))) (BitVec 64) +( + +(Start (BitVec 64) (#x0000000000000000 #x0000000000000001 x (bvnot Start) + (shl1 Start) + (shr1 Start) + (shr4 Start) + (shr16 Start) + (bvand Start Start) + (bvor Start Start) + (bvxor Start Start) + (bvadd Start Start) + (if0 Start Start Start) + )) +) +) +(constraint (= (f #x6E393354DFFAAB51) #xC8E366559002AA57)) +(constraint (= (f #xFDA75AD598A27135) #x812C529533AEC765)) +(constraint (= (f #x58682C0FA4F8DB6D) #xD3CBE9F82D839249)) +(constraint (= (f #x58FDC0941A7E079F) #xD3811FB5F2C0FC30)) +(constraint (= (f #xBDC9B88103ECB0C9) #xA11B23BF7E09A79B)) +(constraint (= (f #x000000000001502F) #xFFFFFFFFFFFF57E8)) +(constraint (= (f #x0000000000010999) #xFFFFFFFFFFFF7B33)) +(constraint (= (f #x0000000000013169) #xFFFFFFFFFFFF674B)) +(constraint (= (f #x000000000001B1A9) #xFFFFFFFFFFFF272B)) +(constraint (= (f #x0000000000016D77) #xFFFFFFFFFFFF4944)) +(constraint (= (f #x0000000000000001) #xFFFFFFFFFFFFFFFF)) +(constraint (= (f #x1ED2E25068744C80) #x0000000000000000)) +(constraint (= (f #x2D2144F9D8CDCBD6) #x0000000000000000)) +(constraint (= (f #xF0F0F0F0F0F0F0F2) #x0000000000000000)) +(constraint (= (f #x83163CFD5DDCCCFB) #xBE74E18151119982)) +(constraint (= (f #xEA31B6A50EF4E399) #x8AE724AD78858E33)) +(constraint (= (f #xE0B1EF549BB6D4B9) #x8FA70855B22495A3)) +(constraint (= (f #x086F9E13A16C363D) #xFBC830F62F49E4E1)) +(constraint (= (f #x2426824D3E67E342) #x0000000000000000)) +(constraint (= (f #xDD518DEFFF18308A) #x0000000000000000)) +(constraint (= (f #x21ECDADB06B3CB03) #xEF0992927CA61A7E)) +(constraint (= (f #x72B1976FBB63A82B) #xC6A73448224E2BEA)) +(constraint (= (f #x16CB47AE0281B27F) #xF49A5C28FEBF26C0)) +(constraint (= (f #x82DE7A1FCA0C0B8F) #xBE90C2F01AF9FA38)) +(constraint (= (f #x0000000000000001) #xFFFFFFFFFFFFFFFF)) +(constraint (= (f #xF0F0F0F0F0F0F0F2) #x0000000000000000)) +(constraint (= (f #x000000000001F0D4) #x0000000000000000)) +(constraint (= (f #x0000000000010067) #xFFFFFFFFFFFF7FCC)) +(check-synth) diff --git a/test/regress/regress1/sygus/icfp_14.12.sy b/test/regress/regress1/sygus/icfp_14.12.sy new file mode 100644 index 000000000..51b86f0f5 --- /dev/null +++ b/test/regress/regress1/sygus/icfp_14.12.sy @@ -0,0 +1,63 @@ +; EXPECT: unsat +; COMMAND-LINE: --sygus-out=status +(set-logic BV) + +(define-fun shr1 ((x (BitVec 64))) (BitVec 64) (bvlshr x #x0000000000000001)) +(define-fun shr4 ((x (BitVec 64))) (BitVec 64) (bvlshr x #x0000000000000004)) +(define-fun shr16 ((x (BitVec 64))) (BitVec 64) (bvlshr x #x0000000000000010)) +(define-fun shl1 ((x (BitVec 64))) (BitVec 64) (bvshl x #x0000000000000001)) +(define-fun if0 ((x (BitVec 64)) (y (BitVec 64)) (z (BitVec 64))) (BitVec 64) (ite (= x #x0000000000000001) y z)) + +(synth-fun f ( (x (BitVec 64))) (BitVec 64) +( + +(Start (BitVec 64) (#x0000000000000000 #x0000000000000001 x (bvnot Start) + (shl1 Start) + (shr1 Start) + (shr4 Start) + (shr16 Start) + (bvand Start Start) + (bvor Start Start) + (bvxor Start Start) + (bvadd Start Start) + (if0 Start Start Start) + )) +) +) +(constraint (= (f #x6E393354DFFAAB51) #xC8E366559002AA57)) +(constraint (= (f #xFDA75AD598A27135) #x812C529533AEC765)) +(constraint (= (f #x58682C0FA4F8DB6D) #xD3CBE9F82D839249)) +(constraint (= (f #x58FDC0941A7E079F) #xD3811FB5F2C0FC30)) +(constraint (= (f #xBDC9B88103ECB0C9) #xA11B23BF7E09A79B)) +(constraint (= (f #x000000000001502F) #xFFFFFFFFFFFF57E8)) +(constraint (= (f #x0000000000010999) #xFFFFFFFFFFFF7B33)) +(constraint (= (f #x0000000000013169) #xFFFFFFFFFFFF674B)) +(constraint (= (f #x000000000001B1A9) #xFFFFFFFFFFFF272B)) +(constraint (= (f #x0000000000016D77) #xFFFFFFFFFFFF4944)) +(constraint (= (f #x0000000000000001) #xFFFFFFFFFFFFFFFF)) +(constraint (= (f #x1ED2E25068744C80) #x0000000000000000)) +(constraint (= (f #x2D2144F9D8CDCBD6) #x0000000000000000)) +(constraint (= (f #xE5D371D100002E8A) #x0000000000000000)) +(constraint (= (f #xADFF6BA34EBDAD72) #x0000000000000000)) +(constraint (= (f #xDA9299B546AAB59A) #x0000000000000000)) +(constraint (= (f #x0000000000015C8A) #x0000000000000000)) +(constraint (= (f #x0000000000017066) #x0000000000000000)) +(constraint (= (f #x000000000001D9D8) #x0000000000000000)) +(constraint (= (f #x00000000000151AE) #x0000000000000000)) +(constraint (= (f #x0000000000017A14) #x0000000000000000)) +(constraint (= (f #xF0F0F0F0F0F0F0F2) #x0000000000000000)) +(constraint (= (f #x83163CFD5DDCCCFB) #xBE74E18151119982)) +(constraint (= (f #xEA31B6A50EF4E399) #x8AE724AD78858E33)) +(constraint (= (f #xE0B1EF549BB6D4B9) #x8FA70855B22495A3)) +(constraint (= (f #x086F9E13A16C363D) #xFBC830F62F49E4E1)) +(constraint (= (f #x2426824D3E67E342) #x0000000000000000)) +(constraint (= (f #xDD518DEFFF18308A) #x0000000000000000)) +(constraint (= (f #x21ECDADB06B3CB03) #xEF0992927CA61A7E)) +(constraint (= (f #x72B1976FBB63A82B) #xC6A73448224E2BEA)) +(constraint (= (f #x16CB47AE0281B27F) #xF49A5C28FEBF26C0)) +(constraint (= (f #x82DE7A1FCA0C0B8F) #xBE90C2F01AF9FA38)) +(constraint (= (f #x0000000000000001) #xFFFFFFFFFFFFFFFF)) +(constraint (= (f #xF0F0F0F0F0F0F0F2) #x0000000000000000)) +(constraint (= (f #x000000000001F0D4) #x0000000000000000)) +(constraint (= (f #x0000000000010067) #xFFFFFFFFFFFF7FCC)) +(check-synth) diff --git a/test/regress/regress1/sygus/icfp_28_10.sy b/test/regress/regress1/sygus/icfp_28_10.sy new file mode 100644 index 000000000..212ae37f5 --- /dev/null +++ b/test/regress/regress1/sygus/icfp_28_10.sy @@ -0,0 +1,40 @@ +; EXPECT: unsat +; COMMAND-LINE: --sygus-out=status + +(set-logic BV) + +(define-fun shr1 ((x (BitVec 64))) (BitVec 64) (bvlshr x #x0000000000000001)) +(define-fun shr4 ((x (BitVec 64))) (BitVec 64) (bvlshr x #x0000000000000004)) +(define-fun shr16 ((x (BitVec 64))) (BitVec 64) (bvlshr x #x0000000000000010)) +(define-fun shl1 ((x (BitVec 64))) (BitVec 64) (bvshl x #x0000000000000001)) +(define-fun if0 ((x (BitVec 64)) (y (BitVec 64)) (z (BitVec 64))) (BitVec 64) (ite (= x #x0000000000000001) y z)) + +(synth-fun f ( (x (BitVec 64))) (BitVec 64) +( + +(Start (BitVec 64) (#x0000000000000000 #x0000000000000001 x (bvnot Start) + (shl1 Start) + (shr1 Start) + (shr4 Start) + (shr16 Start) + (bvand Start Start) + (bvor Start Start) + (bvxor Start Start) + (bvadd Start Start) + (if0 Start Start Start) + )) +) +) + + +(constraint (= (f #xd74594057974e439) #x0000d74594057974)) +(constraint (= (f #x74641ebeee92e8a2) #x000074641ebeee92)) +(constraint (= (f #x91c80141d7ec76b1) #x000091c80141d7ec)) +(constraint (= (f #xe4e55862e5ee4bec) #x0000e4e55862e5ee)) +(constraint (= (f #x367da67ede4260ce) #x0000367da67ede42)) +(constraint (= (f #xa365eb36246b3d8e) #x0000a365eb36246b)) +(constraint (= (f #xcd8a44a6d4c09c29) #x0000cd8a44a6d4c0)) +(constraint (= (f #xa97e9b9b7970433d) #x0000a97e9b9b7970)) +(constraint (= (f #x474dec0dd75d6894) #x0000474dec0dd75d)) +(constraint (= (f #x12430014ed058b24) #x000012430014ed05)) +(check-synth) diff --git a/test/regress/regress1/sygus/icfp_easy_mt_ite.sy b/test/regress/regress1/sygus/icfp_easy-ite.sy index 799633fa3..f0cbbdc53 100644 --- a/test/regress/regress1/sygus/icfp_easy_mt_ite.sy +++ b/test/regress/regress1/sygus/icfp_easy-ite.sy @@ -25,7 +25,9 @@ (StartBool Bool ((= Start #x0000000000000001))) ) ) -(constraint (= (f #x6E393354DFFAAB51) #xC8E366559002AA57)) +(constraint (= (f #x0000000000000001) #x0000000000000001)) + +(constraint (= (f #x0000000000100001) #x0000000000100001)) (constraint (= (f #xE5D371D100002E8A) #x0000000000000000)) diff --git a/test/regress/regress1/sygus/inv-example.sy b/test/regress/regress1/sygus/inv-example.sy new file mode 100644 index 000000000..ff68bc06c --- /dev/null +++ b/test/regress/regress1/sygus/inv-example.sy @@ -0,0 +1,12 @@ +; EXPECT: unsat +; COMMAND-LINE: --sygus-out=status +(set-logic LIA) +(synth-inv inv-f ((x Int) (y Int) (b Bool))) +(declare-primed-var x Int) +(declare-primed-var y Int) +(declare-primed-var b Bool) +(define-fun pre-f ((x Int) (y Int) (b Bool)) Bool (and (and (>= x 5) (<= x 9)) (and (>= y 1) (<= y 3)))) +(define-fun trans-f ((x Int) (y Int) (b Bool) (x! Int) (y! Int) (b! Bool)) Bool (and (and (= b! b) (= y! x)) (ite b (= x! (+ x 10)) (= x! (+ x 12))))) +(define-fun post-f ((x Int) (y Int) (b Bool)) Bool (<= y x)) +(inv-constraint inv-f pre-f trans-f post-f) +(check-synth) diff --git a/test/regress/regress1/sygus/inv-unused.sy b/test/regress/regress1/sygus/inv-unused.sy new file mode 100644 index 000000000..91ba95d39 --- /dev/null +++ b/test/regress/regress1/sygus/inv-unused.sy @@ -0,0 +1,13 @@ +; EXPECT: unsat +; COMMAND-LINE: --sygus-out=status +(set-logic LIA) +(synth-inv inv-f ((x Int) (y Int) (b Bool))) +(declare-primed-var x Int) +(declare-primed-var y Int) +(declare-primed-var b Bool) +(define-fun pre-f ((x Int) (y Int) (b Bool)) Bool (and (>= x 5) (<= x 9))) +(define-fun trans-f ((x Int) (y Int) (b Bool) (x! Int) (y! Int) (b! Bool)) Bool (= x! (+ x 1))) +(define-fun post-f ((x Int) (y Int) (b Bool)) Bool (> x 0)) +(inv-constraint inv-f pre-f trans-f post-f) +; invariant does not depend on arguments y and b +(check-synth) diff --git a/test/regress/regress1/sygus/list-head-x.sy b/test/regress/regress1/sygus/list-head-x.sy new file mode 100644 index 000000000..6c5c1a97b --- /dev/null +++ b/test/regress/regress1/sygus/list-head-x.sy @@ -0,0 +1,13 @@ +; EXPECT: unsat +; COMMAND-LINE: --cegqi-si=all --sygus-out=status +(set-logic ALL_SUPPORTED) + +(declare-datatypes ((List 0)) (((cons (head Int) (tail List)) (nil)))) + +(synth-fun f ((x Int)) List) + +(declare-var x Int) + +(constraint (is-cons (f x))) +(constraint (= (head (f x)) (+ x 7))) +(check-synth) diff --git a/test/regress/regress1/sygus/lustre-real.sy b/test/regress/regress1/sygus/lustre-real.sy deleted file mode 100644 index 2ca010898..000000000 --- a/test/regress/regress1/sygus/lustre-real.sy +++ /dev/null @@ -1,322 +0,0 @@ -; EXPECT: unsat -; COMMAND-LINE: --cegqi-si=none --sygus-out=status -(set-logic LIRA) -(define-fun -__node_init_top_0 ( -(top.usr.onOff@0 Bool) (top.usr.decelSet@0 Bool) (top.usr.accelResume@0 Bool) (top.usr.cancel@0 Bool) (top.usr.brakePedal@0 Bool) (top.usr.carGear@0 Int) (top.usr.carSpeed@0 Real) (top.usr.validInputs@0 Bool) (top.usr.OK@0 Bool) (top.res.init_flag@0 Bool) (top.impl.usr.chart_CruiseController_ModeLogic_mode_logic____wakeup___@0 Bool) (top.impl.usr.chart_CruiseController_ModeLogic_mode_logic_rlt_evtInitStep@0 Bool) (top.impl.usr.chart_CruiseController_ModeLogic_mode_logic_final_state_states___root@0 Int) (top.impl.usr.cruise_controller_CruiseController_ModeLogic_DelayOnsetAccel_Bounded_Count_Out@0 Int) (top.impl.usr.cruise_controller_CruiseController_ModeLogic_DelayOnsetDecel_Bounded_Count_Out@0 Int) ) Bool - -(let ((X1 Int 0)) (let ((X2 Int (ite (not (= X1 1)) 1 X1))) (let ((X3 Bool (or (= X2 1) (and (>= X2 2) (<= X2 8))))) (and (= top.usr.OK@0 X3) (let ((X4 Bool false)) (let ((X5 Bool (and (and (and (and (not top.usr.cancel@0) (not top.usr.brakePedal@0)) (ite (= top.usr.carGear@0 3) true false)) (ite (>= top.usr.carSpeed@0 15.0) true false)) top.usr.validInputs@0))) (let ((X6 Bool false)) (and (= top.impl.usr.cruise_controller_CruiseController_ModeLogic_DelayOnsetDecel_Bounded_Count_Out@0 -(ite (<= (ite (>= 0 (ite top.usr.decelSet@0 1 0)) 0 -(ite top.usr.decelSet@0 1 0)) 20) (ite (>= 0 (ite top.usr.decelSet@0 1 0)) 0 -(ite top.usr.decelSet@0 1 0)) 20)) (= top.impl.usr.cruise_controller_CruiseController_ModeLogic_DelayOnsetAccel_Bounded_Count_Out@0 -(ite (<= (ite (>= 0 (ite top.usr.accelResume@0 1 0)) 0 -(ite top.usr.accelResume@0 1 0)) 20) (ite (>= 0 (ite top.usr.accelResume@0 1 0)) 0 -(ite top.usr.accelResume@0 1 0)) 20)) (= top.impl.usr.chart_CruiseController_ModeLogic_mode_logic_rlt_evtInitStep@0 true) (let ((X7 Int (ite (not top.usr.onOff@0) 0 1))) (let ((X8 Bool (and (and (>= X1 2) (<= X1 8)) (not (ite (not (= X7 0)) true false))))) (let ((X9 Int (ite X8 (ite (and (>= X1 2) (<= X1 8)) 0 X1) X1))) (let ((X10 Int (ite X8 (ite (not (= X9 1)) 1 X9) X9))) (let ((X11 Bool (and (= X10 1) (and (ite (not (= X7 0)) true false) (not X8))))) (let ((X12 Int (ite X11 (ite (= X10 1) 0 X10) X10))) (let ((X13 Int (ite (not (and (>= X12 2) (<= X12 8))) 2 X12))) (let ((X14 Bool (and (not (and (>= X12 2) (<= X12 8))) (and (>= X13 2) (<= X13 8))))) (let ((X15 Int (ite X14 (ite (not (= X13 7)) 7 X13) X13))) (let ((X16 Int (ite X11 X15 X12))) (let ((X17 Bool (or X11 X8))) (let ((X18 Int (ite (not X5) 0 1))) (let ((X19 Bool (and (and (>= X16 3) (<= X16 6)) (not (ite (not (= X18 0)) true false))))) (let ((X20 -Int (ite X19 -(ite (and (>= X16 3) (<= X16 6)) 2 X16) X16))) (let ((X21 Int (ite X19 (ite (not (= X20 8)) 8 X20) X20))) (let ((X22 Int (ite (not X4) 0 1))) (let ((X23 Bool (and (= X21 8) (and (and (ite (not (= (ite (not (= X22 1)) 0 1) 0)) true false) (ite (not (= (ite (not (= X18 1)) 0 1) 0)) true false)) (not X19))))) (let ((X24 Int (ite X23 (ite (= X21 8) 2 X21) X21))) (let ((X25 -Int (ite (not (and (>= X24 3) (<= X24 6))) 3 X24))) (let ((X26 Bool (and (not (and (>= X24 3) (<= X24 6))) (and (>= X25 3) (<= X25 6))))) (let ((X27 -Int (ite X26 -(ite (not (= X25 4)) 4 X25) X25))) (let ((X28 Int (ite X23 X27 X24))) (let ((X29 Bool (or X23 X19))) (let ((X30 Bool (and (= X28 8) (and (and (ite (not -(= (ite (not -(= (ite (not X6) 0 1) 1)) 0 1) 0)) true false) (ite (not -(= (ite (not (= X18 1)) 0 1) 0)) true false)) (not X29))))) (let ((X31 -Int (ite X30 (ite (= X28 8) 2 X28) X28))) (let ((X32 -Int (ite (not (and (>= X31 3) (<= X31 6))) 3 X31))) (let ((X33 Bool (and (not -(and (>= X31 3) (<= X31 6))) (and (>= X32 3) (<= X32 6))))) (let ((X34 -Int (ite X33 -(ite (not (= X32 4)) 4 X32) X32))) (let ((X35 Int (ite X30 X34 X31))) (let ((X36 Bool (or X30 X29))) (let ((X37 Bool (and (= X35 7) (and (and (ite (not -(= (ite (not (= X22 1)) 0 1) 0)) true false) (ite (not -(= (ite (not (= X18 1)) 0 1) 0)) true false)) (not X36))))) (let ((X38 -Int (ite X37 -(ite (= X35 7) 2 X35) X35))) (let ((X39 -Int (ite (not -(and (>= X38 3) (<= X38 6))) 3 X38))) (let ((X40 Bool (and (not -(and (>= X38 3) (<= X38 6))) (and (>= X39 3) (<= X39 6))))) (let ((X41 -Int (ite X40 -(ite (not (= X39 4)) 4 X39) X39))) (let ((X42 Int (ite X37 X41 X38))) (let ((X43 Bool (or X37 X36))) (let ((X44 Bool (and (= X42 4) (= X22 1)))) (let ((X45 -Int (ite X44 -(ite (= X42 4) 3 X42) X42))) (let ((X46 -Int (ite X44 -(ite (not (= X45 4)) 4 X45) X45))) (let ((X47 -Int (ite (not -(ite (= top.impl.usr.cruise_controller_CruiseController_ModeLogic_DelayOnsetAccel_Bounded_Count_Out@0 20) true false)) 0 1))) (let ((X48 Bool (and (= X46 4) (and (= X47 1) (not X44))))) (let ((X49 -Int (ite X48 -(ite (= X46 4) 3 X46) X46))) (let ((X50 -Int (ite X48 -(ite (not (= X49 5)) 5 X49) X49))) (let ((X51 Bool (or X48 X44))) (let ((X52 -Int (ite (not -(ite (= top.impl.usr.cruise_controller_CruiseController_ModeLogic_DelayOnsetDecel_Bounded_Count_Out@0 20) true false)) 0 1))) (let ((X53 Bool (and (= X50 4) (and (= X52 1) (not X51))))) (let ((X54 -Int (ite X53 -(ite (= X50 4) 3 X50) X50))) (let ((X55 -Int (ite X53 -(ite (not -(= X54 6)) 6 X54) X54))) (let ((X56 Bool (or X53 X51))) (let ((X57 Bool (and (= X55 6) (and (= X52 0) (not X56))))) (let ((X58 -Int (ite X57 -(ite (= X55 6) 3 X55) X55))) (let ((X59 -Int (ite X57 -(ite (not -(= X58 4)) 4 X58) X58))) (let ((X60 Bool -(or X57 X56))) (let ((X61 Bool -(and (= X59 5) (and (= X47 0) (not X60))))) (let ((X62 -Int (ite X61 -(ite (= X59 5) 3 X59) X59))) (let ((X63 -Int (ite X61 -(ite (not -(= X62 4)) 4 X62) X62))) (and (= top.impl.usr.chart_CruiseController_ModeLogic_mode_logic____wakeup___@0 true) (= top.impl.usr.chart_CruiseController_ModeLogic_mode_logic_final_state_states___root@0 -(ite top.impl.usr.chart_CruiseController_ModeLogic_mode_logic____wakeup___@0 -(ite top.impl.usr.chart_CruiseController_ModeLogic_mode_logic_rlt_evtInitStep@0 X2 -(ite (and (not X17) (and (>= X16 2) (<= X16 -8))) (ite (and (not X43) (and (>= X42 -3) (<= X42 -6))) X63 X42) X16)) X1)) (<= 0 X47 1) (<= 0 X22 1) (<= 0 X18 1) (<= 0 X7 1) (<= 0 X52 1) top.res.init_flag@0)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ) -(define-fun -__node_trans_top_0 ( -(top.usr.onOff@1 Bool) (top.usr.decelSet@1 Bool) (top.usr.accelResume@1 Bool) (top.usr.cancel@1 Bool) (top.usr.brakePedal@1 Bool) (top.usr.carGear@1 Int) (top.usr.carSpeed@1 Real) (top.usr.validInputs@1 Bool) (top.usr.OK@1 Bool) (top.res.init_flag@1 Bool) (top.impl.usr.chart_CruiseController_ModeLogic_mode_logic____wakeup___@1 Bool) (top.impl.usr.chart_CruiseController_ModeLogic_mode_logic_rlt_evtInitStep@1 Bool) (top.impl.usr.chart_CruiseController_ModeLogic_mode_logic_final_state_states___root@1 Int) (top.impl.usr.cruise_controller_CruiseController_ModeLogic_DelayOnsetAccel_Bounded_Count_Out@1 Int) (top.impl.usr.cruise_controller_CruiseController_ModeLogic_DelayOnsetDecel_Bounded_Count_Out@1 Int) (top.usr.onOff@0 Bool) (top.usr.decelSet@0 Bool) (top.usr.accelResume@0 Bool) (top.usr.cancel@0 Bool) (top.usr.brakePedal@0 Bool) (top.usr.carGear@0 Int) (top.usr.carSpeed@0 Real) (top.usr.validInputs@0 Bool) (top.usr.OK@0 Bool) (top.res.init_flag@0 Bool) (top.impl.usr.chart_CruiseController_ModeLogic_mode_logic____wakeup___@0 Bool) (top.impl.usr.chart_CruiseController_ModeLogic_mode_logic_rlt_evtInitStep@0 Bool) (top.impl.usr.chart_CruiseController_ModeLogic_mode_logic_final_state_states___root@0 Int) (top.impl.usr.cruise_controller_CruiseController_ModeLogic_DelayOnsetAccel_Bounded_Count_Out@0 Int) (top.impl.usr.cruise_controller_CruiseController_ModeLogic_DelayOnsetDecel_Bounded_Count_Out@0 Int) ) Bool - -(let ((X1 -Int top.impl.usr.chart_CruiseController_ModeLogic_mode_logic_final_state_states___root@0)) (let ((X2 Int (ite (not (= X1 1)) 1 X1))) (let ((X3 Bool (or (= X2 1) (and (>= X2 2) (<= X2 8))))) (and (= top.usr.OK@1 X3) (let ((X4 Bool (and (not top.usr.decelSet@0) top.usr.decelSet@1))) (let ((X5 Bool (and (and (and (and (not top.usr.cancel@1) (not top.usr.brakePedal@1)) (ite (= top.usr.carGear@1 3) true false)) (ite (>= top.usr.carSpeed@1 15.0) true false)) top.usr.validInputs@1))) (let ((X6 Bool (and (not top.usr.accelResume@0) top.usr.accelResume@1))) (and (= top.impl.usr.cruise_controller_CruiseController_ModeLogic_DelayOnsetDecel_Bounded_Count_Out@1 -(ite (<= (ite (>= 0 -(ite top.usr.decelSet@1 -(+ top.impl.usr.cruise_controller_CruiseController_ModeLogic_DelayOnsetDecel_Bounded_Count_Out@0 1) 0)) 0 -(ite top.usr.decelSet@1 -(+ top.impl.usr.cruise_controller_CruiseController_ModeLogic_DelayOnsetDecel_Bounded_Count_Out@0 1) 0)) 20) (ite (>= 0 -(ite top.usr.decelSet@1 -(+ top.impl.usr.cruise_controller_CruiseController_ModeLogic_DelayOnsetDecel_Bounded_Count_Out@0 1) 0)) 0 -(ite top.usr.decelSet@1 -(+ top.impl.usr.cruise_controller_CruiseController_ModeLogic_DelayOnsetDecel_Bounded_Count_Out@0 1) 0)) 20)) (= top.impl.usr.cruise_controller_CruiseController_ModeLogic_DelayOnsetAccel_Bounded_Count_Out@1 -(ite (<= (ite (>= 0 -(ite top.usr.accelResume@1 -(+ top.impl.usr.cruise_controller_CruiseController_ModeLogic_DelayOnsetAccel_Bounded_Count_Out@0 1) 0)) 0 -(ite top.usr.accelResume@1 -(+ top.impl.usr.cruise_controller_CruiseController_ModeLogic_DelayOnsetAccel_Bounded_Count_Out@0 1) 0)) 20) (ite (>= 0 -(ite top.usr.accelResume@1 -(+ top.impl.usr.cruise_controller_CruiseController_ModeLogic_DelayOnsetAccel_Bounded_Count_Out@0 1) 0)) 0 -(ite top.usr.accelResume@1 -(+ top.impl.usr.cruise_controller_CruiseController_ModeLogic_DelayOnsetAccel_Bounded_Count_Out@0 1) 0)) 20)) (= top.impl.usr.chart_CruiseController_ModeLogic_mode_logic_rlt_evtInitStep@1 -(ite top.impl.usr.chart_CruiseController_ModeLogic_mode_logic____wakeup___@0 -false top.impl.usr.chart_CruiseController_ModeLogic_mode_logic_rlt_evtInitStep@0)) (let ((X7 Int (ite (not top.usr.onOff@1) 0 1))) (let ((X8 Bool (and (and (>= X1 2) (<= X1 8)) (not (ite (not (= X7 0)) true false))))) (let ((X9 Int (ite X8 (ite (and (>= X1 2) (<= X1 8)) 0 X1) X1))) (let ((X10 Int (ite X8 (ite (not (= X9 1)) 1 X9) X9))) (let ((X11 Bool (and (= X10 1) (and (ite (not (= X7 0)) true false) (not X8))))) (let ((X12 Int (ite X11 (ite (= X10 1) 0 X10) X10))) (let ((X13 Int (ite (not (and (>= X12 2) (<= X12 8))) 2 X12))) (let ((X14 Bool (and (not (and (>= X12 2) (<= X12 8))) (and (>= X13 2) (<= X13 8))))) (let ((X15 Int (ite X14 (ite (not (= X13 7)) 7 X13) X13))) (let ((X16 Int (ite X11 X15 X12))) (let ((X17 Bool (or X11 X8))) (let ((X18 Int (ite (not X5) 0 1))) (let ((X19 Bool (and (and (>= X16 3) (<= X16 6)) (not (ite (not (= X18 0)) true false))))) (let ((X20 -Int (ite X19 -(ite (and (>= X16 3) (<= X16 6)) 2 X16) X16))) (let ((X21 Int (ite X19 (ite (not (= X20 8)) 8 X20) X20))) (let ((X22 Int (ite (not X4) 0 1))) (let ((X23 Bool (and (= X21 8) (and (and (ite (not (= (ite (not (= X22 1)) 0 1) 0)) true false) (ite (not (= (ite (not (= X18 1)) 0 1) 0)) true false)) (not X19))))) (let ((X24 Int (ite X23 (ite (= X21 8) 2 X21) X21))) (let ((X25 -Int (ite (not (and (>= X24 3) (<= X24 6))) 3 X24))) (let ((X26 Bool (and (not (and (>= X24 3) (<= X24 6))) (and (>= X25 3) (<= X25 6))))) (let ((X27 -Int (ite X26 -(ite (not (= X25 4)) 4 X25) X25))) (let ((X28 Int (ite X23 X27 X24))) (let ((X29 Bool (or X23 X19))) (let ((X30 Bool (and (= X28 8) (and (and (ite (not -(= (ite (not -(= (ite (not X6) 0 1) 1)) 0 1) 0)) true false) (ite (not -(= (ite (not (= X18 1)) 0 1) 0)) true false)) (not X29))))) (let ((X31 -Int (ite X30 (ite (= X28 8) 2 X28) X28))) (let ((X32 -Int (ite (not (and (>= X31 3) (<= X31 6))) 3 X31))) (let ((X33 Bool (and (not -(and (>= X31 3) (<= X31 6))) (and (>= X32 3) (<= X32 6))))) (let ((X34 -Int (ite X33 -(ite (not (= X32 4)) 4 X32) X32))) (let ((X35 Int (ite X30 X34 X31))) (let ((X36 Bool (or X30 X29))) (let ((X37 Bool (and (= X35 7) (and (and (ite (not -(= (ite (not (= X22 1)) 0 1) 0)) true false) (ite (not -(= (ite (not (= X18 1)) 0 1) 0)) true false)) (not X36))))) (let ((X38 -Int (ite X37 -(ite (= X35 7) 2 X35) X35))) (let ((X39 -Int (ite (not -(and (>= X38 3) (<= X38 6))) 3 X38))) (let ((X40 Bool (and (not -(and (>= X38 3) (<= X38 6))) (and (>= X39 3) (<= X39 6))))) (let ((X41 -Int (ite X40 -(ite (not (= X39 4)) 4 X39) X39))) (let ((X42 Int (ite X37 X41 X38))) (let ((X43 Bool (or X37 X36))) (let ((X44 Bool (and (= X42 4) (= X22 1)))) (let ((X45 -Int (ite X44 -(ite (= X42 4) 3 X42) X42))) (let ((X46 -Int (ite X44 -(ite (not (= X45 4)) 4 X45) X45))) (let ((X47 -Int (ite (not -(ite (= top.impl.usr.cruise_controller_CruiseController_ModeLogic_DelayOnsetAccel_Bounded_Count_Out@1 20) true false)) 0 1))) (let ((X48 Bool (and (= X46 4) (and (= X47 1) (not X44))))) (let ((X49 -Int (ite X48 -(ite (= X46 4) 3 X46) X46))) (let ((X50 -Int (ite X48 -(ite (not (= X49 5)) 5 X49) X49))) (let ((X51 Bool (or X48 X44))) (let ((X52 -Int (ite (not -(ite (= top.impl.usr.cruise_controller_CruiseController_ModeLogic_DelayOnsetDecel_Bounded_Count_Out@1 20) true false)) 0 1))) (let ((X53 Bool (and (= X50 4) (and (= X52 1) (not X51))))) (let ((X54 -Int (ite X53 -(ite (= X50 4) 3 X50) X50))) (let ((X55 -Int (ite X53 -(ite (not -(= X54 6)) 6 X54) X54))) (let ((X56 Bool (or X53 X51))) (let ((X57 Bool (and (= X55 6) (and (= X52 0) (not X56))))) (let ((X58 -Int (ite X57 -(ite (= X55 6) 3 X55) X55))) (let ((X59 -Int (ite X57 -(ite (not -(= X58 4)) 4 X58) X58))) (let ((X60 Bool -(or X57 X56))) (let ((X61 Bool -(and (= X59 5) (and (= X47 0) (not X60))))) (let ((X62 -Int (ite X61 -(ite (= X59 5) 3 X59) X59))) (let ((X63 -Int (ite X61 -(ite (not -(= X62 4)) 4 X62) X62))) (and (= top.impl.usr.chart_CruiseController_ModeLogic_mode_logic____wakeup___@1 true) (= top.impl.usr.chart_CruiseController_ModeLogic_mode_logic_final_state_states___root@1 -(ite top.impl.usr.chart_CruiseController_ModeLogic_mode_logic____wakeup___@1 -(ite top.impl.usr.chart_CruiseController_ModeLogic_mode_logic_rlt_evtInitStep@1 X2 -(ite (and (not X17) (and (>= X16 2) (<= X16 -8))) (ite (and (not X43) (and (>= X42 -3) (<= X42 -6))) X63 X42) X16)) X1)) (<= 0 X47 1) (<= 0 X22 1) (<= 0 X18 1) (<= 0 X7 1) (<= 0 X52 1) (not top.res.init_flag@1))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ) - - -(synth-inv str_invariant( -(top.usr.onOff Bool) (top.usr.decelSet Bool) (top.usr.accelResume Bool) (top.usr.cancel Bool) (top.usr.brakePedal Bool) (top.usr.carGear Int) (top.usr.carSpeed Real) (top.usr.validInputs Bool) (top.usr.OK Bool) (top.res.init_flag Bool) (top.impl.usr.chart_CruiseController_ModeLogic_mode_logic____wakeup___ Bool) (top.impl.usr.chart_CruiseController_ModeLogic_mode_logic_rlt_evtInitStep Bool) (top.impl.usr.chart_CruiseController_ModeLogic_mode_logic_final_state_states___root Int) (top.impl.usr.cruise_controller_CruiseController_ModeLogic_DelayOnsetAccel_Bounded_Count_Out Int) (top.impl.usr.cruise_controller_CruiseController_ModeLogic_DelayOnsetDecel_Bounded_Count_Out Int) )) - -(declare-primed-var top.usr.onOff Bool) (declare-primed-var top.usr.decelSet Bool) (declare-primed-var top.usr.accelResume Bool) (declare-primed-var top.usr.cancel Bool) (declare-primed-var top.usr.brakePedal Bool) (declare-primed-var top.usr.carGear Int) (declare-primed-var top.usr.carSpeed Real) (declare-primed-var top.usr.validInputs Bool) (declare-primed-var top.usr.OK Bool) (declare-primed-var top.res.init_flag Bool) (declare-primed-var top.impl.usr.chart_CruiseController_ModeLogic_mode_logic____wakeup___ Bool) (declare-primed-var top.impl.usr.chart_CruiseController_ModeLogic_mode_logic_rlt_evtInitStep Bool) (declare-primed-var top.impl.usr.chart_CruiseController_ModeLogic_mode_logic_final_state_states___root Int) (declare-primed-var top.impl.usr.cruise_controller_CruiseController_ModeLogic_DelayOnsetAccel_Bounded_Count_Out Int) (declare-primed-var top.impl.usr.cruise_controller_CruiseController_ModeLogic_DelayOnsetDecel_Bounded_Count_Out Int) -(define-fun -init ( -(top.usr.onOff Bool) (top.usr.decelSet Bool) (top.usr.accelResume Bool) (top.usr.cancel Bool) (top.usr.brakePedal Bool) (top.usr.carGear Int) (top.usr.carSpeed Real) (top.usr.validInputs Bool) (top.usr.OK Bool) (top.res.init_flag Bool) (top.impl.usr.chart_CruiseController_ModeLogic_mode_logic____wakeup___ Bool) (top.impl.usr.chart_CruiseController_ModeLogic_mode_logic_rlt_evtInitStep Bool) (top.impl.usr.chart_CruiseController_ModeLogic_mode_logic_final_state_states___root Int) (top.impl.usr.cruise_controller_CruiseController_ModeLogic_DelayOnsetAccel_Bounded_Count_Out Int) (top.impl.usr.cruise_controller_CruiseController_ModeLogic_DelayOnsetDecel_Bounded_Count_Out Int) ) Bool - -(let ((X1 Int 0)) (let ((X2 Int (ite (not (= X1 1)) 1 X1))) (let ((X3 Bool (or (= X2 1) (and (>= X2 2) (<= X2 8))))) (and (= top.usr.OK X3) (let ((X4 Bool false)) (let ((X5 Bool (and (and (and (and (not top.usr.cancel) (not top.usr.brakePedal)) (ite (= top.usr.carGear 3) true false)) (ite (>= top.usr.carSpeed 15.0) true false)) top.usr.validInputs))) (let ((X6 Bool false)) (and (= top.impl.usr.cruise_controller_CruiseController_ModeLogic_DelayOnsetDecel_Bounded_Count_Out -(ite (<= (ite (>= 0 (ite top.usr.decelSet 1 0)) 0 -(ite top.usr.decelSet 1 0)) 20) (ite (>= 0 (ite top.usr.decelSet 1 0)) 0 -(ite top.usr.decelSet 1 0)) 20)) (= top.impl.usr.cruise_controller_CruiseController_ModeLogic_DelayOnsetAccel_Bounded_Count_Out -(ite (<= (ite (>= 0 (ite top.usr.accelResume 1 0)) 0 -(ite top.usr.accelResume 1 0)) 20) (ite (>= 0 (ite top.usr.accelResume 1 0)) 0 -(ite top.usr.accelResume 1 0)) 20)) (= top.impl.usr.chart_CruiseController_ModeLogic_mode_logic_rlt_evtInitStep true) (let ((X7 Int (ite (not top.usr.onOff) 0 1))) (let ((X8 Bool (and (and (>= X1 2) (<= X1 8)) (not (ite (not (= X7 0)) true false))))) (let ((X9 Int (ite X8 (ite (and (>= X1 2) (<= X1 8)) 0 X1) X1))) (let ((X10 Int (ite X8 (ite (not (= X9 1)) 1 X9) X9))) (let ((X11 Bool (and (= X10 1) (and (ite (not (= X7 0)) true false) (not X8))))) (let ((X12 Int (ite X11 (ite (= X10 1) 0 X10) X10))) (let ((X13 Int (ite (not (and (>= X12 2) (<= X12 8))) 2 X12))) (let ((X14 Bool (and (not (and (>= X12 2) (<= X12 8))) (and (>= X13 2) (<= X13 8))))) (let ((X15 Int (ite X14 (ite (not (= X13 7)) 7 X13) X13))) (let ((X16 Int (ite X11 X15 X12))) (let ((X17 Bool (or X11 X8))) (let ((X18 Int (ite (not X5) 0 1))) (let ((X19 Bool (and (and (>= X16 3) (<= X16 6)) (not (ite (not (= X18 0)) true false))))) (let ((X20 -Int (ite X19 -(ite (and (>= X16 3) (<= X16 6)) 2 X16) X16))) (let ((X21 Int (ite X19 (ite (not (= X20 8)) 8 X20) X20))) (let ((X22 Int (ite (not X4) 0 1))) (let ((X23 Bool (and (= X21 8) (and (and (ite (not (= (ite (not (= X22 1)) 0 1) 0)) true false) (ite (not (= (ite (not (= X18 1)) 0 1) 0)) true false)) (not X19))))) (let ((X24 Int (ite X23 (ite (= X21 8) 2 X21) X21))) (let ((X25 -Int (ite (not (and (>= X24 3) (<= X24 6))) 3 X24))) (let ((X26 Bool (and (not (and (>= X24 3) (<= X24 6))) (and (>= X25 3) (<= X25 6))))) (let ((X27 -Int (ite X26 -(ite (not (= X25 4)) 4 X25) X25))) (let ((X28 Int (ite X23 X27 X24))) (let ((X29 Bool (or X23 X19))) (let ((X30 Bool (and (= X28 8) (and (and (ite (not -(= (ite (not -(= (ite (not X6) 0 1) 1)) 0 1) 0)) true false) (ite (not -(= (ite (not (= X18 1)) 0 1) 0)) true false)) (not X29))))) (let ((X31 -Int (ite X30 (ite (= X28 8) 2 X28) X28))) (let ((X32 -Int (ite (not (and (>= X31 3) (<= X31 6))) 3 X31))) (let ((X33 Bool (and (not -(and (>= X31 3) (<= X31 6))) (and (>= X32 3) (<= X32 6))))) (let ((X34 -Int (ite X33 -(ite (not (= X32 4)) 4 X32) X32))) (let ((X35 Int (ite X30 X34 X31))) (let ((X36 Bool (or X30 X29))) (let ((X37 Bool (and (= X35 7) (and (and (ite (not -(= (ite (not (= X22 1)) 0 1) 0)) true false) (ite (not -(= (ite (not (= X18 1)) 0 1) 0)) true false)) (not X36))))) (let ((X38 -Int (ite X37 -(ite (= X35 7) 2 X35) X35))) (let ((X39 -Int (ite (not -(and (>= X38 3) (<= X38 6))) 3 X38))) (let ((X40 Bool (and (not -(and (>= X38 3) (<= X38 6))) (and (>= X39 3) (<= X39 6))))) (let ((X41 -Int (ite X40 -(ite (not (= X39 4)) 4 X39) X39))) (let ((X42 Int (ite X37 X41 X38))) (let ((X43 Bool (or X37 X36))) (let ((X44 Bool (and (= X42 4) (= X22 1)))) (let ((X45 -Int (ite X44 -(ite (= X42 4) 3 X42) X42))) (let ((X46 -Int (ite X44 -(ite (not (= X45 4)) 4 X45) X45))) (let ((X47 -Int (ite (not -(ite (= top.impl.usr.cruise_controller_CruiseController_ModeLogic_DelayOnsetAccel_Bounded_Count_Out 20) true false)) 0 1))) (let ((X48 Bool (and (= X46 4) (and (= X47 1) (not X44))))) (let ((X49 -Int (ite X48 -(ite (= X46 4) 3 X46) X46))) (let ((X50 -Int (ite X48 -(ite (not (= X49 5)) 5 X49) X49))) (let ((X51 Bool (or X48 X44))) (let ((X52 -Int (ite (not -(ite (= top.impl.usr.cruise_controller_CruiseController_ModeLogic_DelayOnsetDecel_Bounded_Count_Out 20) true false)) 0 1))) (let ((X53 Bool (and (= X50 4) (and (= X52 1) (not X51))))) (let ((X54 -Int (ite X53 -(ite (= X50 4) 3 X50) X50))) (let ((X55 -Int (ite X53 -(ite (not -(= X54 6)) 6 X54) X54))) (let ((X56 Bool (or X53 X51))) (let ((X57 Bool (and (= X55 6) (and (= X52 0) (not X56))))) (let ((X58 -Int (ite X57 -(ite (= X55 6) 3 X55) X55))) (let ((X59 -Int (ite X57 -(ite (not -(= X58 4)) 4 X58) X58))) (let ((X60 Bool -(or X57 X56))) (let ((X61 Bool -(and (= X59 5) (and (= X47 0) (not X60))))) (let ((X62 -Int (ite X61 -(ite (= X59 5) 3 X59) X59))) (let ((X63 -Int (ite X61 -(ite (not -(= X62 4)) 4 X62) X62))) (and (= top.impl.usr.chart_CruiseController_ModeLogic_mode_logic____wakeup___ true) (= top.impl.usr.chart_CruiseController_ModeLogic_mode_logic_final_state_states___root -(ite top.impl.usr.chart_CruiseController_ModeLogic_mode_logic____wakeup___ -(ite top.impl.usr.chart_CruiseController_ModeLogic_mode_logic_rlt_evtInitStep X2 -(ite (and (not X17) (and (>= X16 2) (<= X16 -8))) (ite (and (not X43) (and (>= X42 -3) (<= X42 -6))) X63 X42) X16)) X1)) (<= 0 X47 1) (<= 0 X22 1) (<= 0 X18 1) (<= 0 X7 1) (<= 0 X52 1) top.res.init_flag)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ) -(define-fun trans ( - -;; Current state. -(top.usr.onOff Bool) (top.usr.decelSet Bool) (top.usr.accelResume Bool) (top.usr.cancel Bool) (top.usr.brakePedal Bool) (top.usr.carGear Int) (top.usr.carSpeed Real) (top.usr.validInputs Bool) (top.usr.OK Bool) (top.res.init_flag Bool) (top.impl.usr.chart_CruiseController_ModeLogic_mode_logic____wakeup___ Bool) (top.impl.usr.chart_CruiseController_ModeLogic_mode_logic_rlt_evtInitStep Bool) (top.impl.usr.chart_CruiseController_ModeLogic_mode_logic_final_state_states___root Int) (top.impl.usr.cruise_controller_CruiseController_ModeLogic_DelayOnsetAccel_Bounded_Count_Out Int) (top.impl.usr.cruise_controller_CruiseController_ModeLogic_DelayOnsetDecel_Bounded_Count_Out Int) -;; Next state. -(top.usr.onOff! Bool) (top.usr.decelSet! Bool) (top.usr.accelResume! Bool) (top.usr.cancel! Bool) (top.usr.brakePedal! Bool) (top.usr.carGear! Int) (top.usr.carSpeed! Real) (top.usr.validInputs! Bool) (top.usr.OK! Bool) (top.res.init_flag! Bool) (top.impl.usr.chart_CruiseController_ModeLogic_mode_logic____wakeup___! Bool) (top.impl.usr.chart_CruiseController_ModeLogic_mode_logic_rlt_evtInitStep! Bool) (top.impl.usr.chart_CruiseController_ModeLogic_mode_logic_final_state_states___root! Int) (top.impl.usr.cruise_controller_CruiseController_ModeLogic_DelayOnsetAccel_Bounded_Count_Out! Int) (top.impl.usr.cruise_controller_CruiseController_ModeLogic_DelayOnsetDecel_Bounded_Count_Out! Int) -) Bool - -(let ((X1 -Int top.impl.usr.chart_CruiseController_ModeLogic_mode_logic_final_state_states___root)) (let ((X2 Int (ite (not (= X1 1)) 1 X1))) (let ((X3 Bool (or (= X2 1) (and (>= X2 2) (<= X2 8))))) (and (= top.usr.OK! X3) (let ((X4 Bool (and (not top.usr.decelSet) top.usr.decelSet!))) (let ((X5 Bool (and (and (and (and (not top.usr.cancel!) (not top.usr.brakePedal!)) (ite (= top.usr.carGear! 3) true false)) (ite (>= top.usr.carSpeed! 15.0) true false)) top.usr.validInputs!))) (let ((X6 Bool (and (not top.usr.accelResume) top.usr.accelResume!))) (and (= top.impl.usr.cruise_controller_CruiseController_ModeLogic_DelayOnsetDecel_Bounded_Count_Out! -(ite (<= (ite (>= 0 -(ite top.usr.decelSet! -(+ top.impl.usr.cruise_controller_CruiseController_ModeLogic_DelayOnsetDecel_Bounded_Count_Out 1) 0)) 0 -(ite top.usr.decelSet! -(+ top.impl.usr.cruise_controller_CruiseController_ModeLogic_DelayOnsetDecel_Bounded_Count_Out 1) 0)) 20) (ite (>= 0 -(ite top.usr.decelSet! -(+ top.impl.usr.cruise_controller_CruiseController_ModeLogic_DelayOnsetDecel_Bounded_Count_Out 1) 0)) 0 -(ite top.usr.decelSet! -(+ top.impl.usr.cruise_controller_CruiseController_ModeLogic_DelayOnsetDecel_Bounded_Count_Out 1) 0)) 20)) (= top.impl.usr.cruise_controller_CruiseController_ModeLogic_DelayOnsetAccel_Bounded_Count_Out! -(ite (<= (ite (>= 0 -(ite top.usr.accelResume! -(+ top.impl.usr.cruise_controller_CruiseController_ModeLogic_DelayOnsetAccel_Bounded_Count_Out 1) 0)) 0 -(ite top.usr.accelResume! -(+ top.impl.usr.cruise_controller_CruiseController_ModeLogic_DelayOnsetAccel_Bounded_Count_Out 1) 0)) 20) (ite (>= 0 -(ite top.usr.accelResume! -(+ top.impl.usr.cruise_controller_CruiseController_ModeLogic_DelayOnsetAccel_Bounded_Count_Out 1) 0)) 0 -(ite top.usr.accelResume! -(+ top.impl.usr.cruise_controller_CruiseController_ModeLogic_DelayOnsetAccel_Bounded_Count_Out 1) 0)) 20)) (= top.impl.usr.chart_CruiseController_ModeLogic_mode_logic_rlt_evtInitStep! -(ite top.impl.usr.chart_CruiseController_ModeLogic_mode_logic____wakeup___ -false top.impl.usr.chart_CruiseController_ModeLogic_mode_logic_rlt_evtInitStep)) (let ((X7 Int (ite (not top.usr.onOff!) 0 1))) (let ((X8 Bool (and (and (>= X1 2) (<= X1 8)) (not (ite (not (= X7 0)) true false))))) (let ((X9 Int (ite X8 (ite (and (>= X1 2) (<= X1 8)) 0 X1) X1))) (let ((X10 Int (ite X8 (ite (not (= X9 1)) 1 X9) X9))) (let ((X11 Bool (and (= X10 1) (and (ite (not (= X7 0)) true false) (not X8))))) (let ((X12 Int (ite X11 (ite (= X10 1) 0 X10) X10))) (let ((X13 Int (ite (not (and (>= X12 2) (<= X12 8))) 2 X12))) (let ((X14 Bool (and (not (and (>= X12 2) (<= X12 8))) (and (>= X13 2) (<= X13 8))))) (let ((X15 Int (ite X14 (ite (not (= X13 7)) 7 X13) X13))) (let ((X16 Int (ite X11 X15 X12))) (let ((X17 Bool (or X11 X8))) (let ((X18 Int (ite (not X5) 0 1))) (let ((X19 Bool (and (and (>= X16 3) (<= X16 6)) (not (ite (not (= X18 0)) true false))))) (let ((X20 -Int (ite X19 -(ite (and (>= X16 3) (<= X16 6)) 2 X16) X16))) (let ((X21 Int (ite X19 (ite (not (= X20 8)) 8 X20) X20))) (let ((X22 Int (ite (not X4) 0 1))) (let ((X23 Bool (and (= X21 8) (and (and (ite (not (= (ite (not (= X22 1)) 0 1) 0)) true false) (ite (not (= (ite (not (= X18 1)) 0 1) 0)) true false)) (not X19))))) (let ((X24 Int (ite X23 (ite (= X21 8) 2 X21) X21))) (let ((X25 -Int (ite (not (and (>= X24 3) (<= X24 6))) 3 X24))) (let ((X26 Bool (and (not (and (>= X24 3) (<= X24 6))) (and (>= X25 3) (<= X25 6))))) (let ((X27 -Int (ite X26 -(ite (not (= X25 4)) 4 X25) X25))) (let ((X28 Int (ite X23 X27 X24))) (let ((X29 Bool (or X23 X19))) (let ((X30 Bool (and (= X28 8) (and (and (ite (not -(= (ite (not -(= (ite (not X6) 0 1) 1)) 0 1) 0)) true false) (ite (not -(= (ite (not (= X18 1)) 0 1) 0)) true false)) (not X29))))) (let ((X31 -Int (ite X30 (ite (= X28 8) 2 X28) X28))) (let ((X32 -Int (ite (not (and (>= X31 3) (<= X31 6))) 3 X31))) (let ((X33 Bool (and (not -(and (>= X31 3) (<= X31 6))) (and (>= X32 3) (<= X32 6))))) (let ((X34 -Int (ite X33 -(ite (not (= X32 4)) 4 X32) X32))) (let ((X35 Int (ite X30 X34 X31))) (let ((X36 Bool (or X30 X29))) (let ((X37 Bool (and (= X35 7) (and (and (ite (not -(= (ite (not (= X22 1)) 0 1) 0)) true false) (ite (not -(= (ite (not (= X18 1)) 0 1) 0)) true false)) (not X36))))) (let ((X38 -Int (ite X37 -(ite (= X35 7) 2 X35) X35))) (let ((X39 -Int (ite (not -(and (>= X38 3) (<= X38 6))) 3 X38))) (let ((X40 Bool (and (not -(and (>= X38 3) (<= X38 6))) (and (>= X39 3) (<= X39 6))))) (let ((X41 -Int (ite X40 -(ite (not (= X39 4)) 4 X39) X39))) (let ((X42 Int (ite X37 X41 X38))) (let ((X43 Bool (or X37 X36))) (let ((X44 Bool (and (= X42 4) (= X22 1)))) (let ((X45 -Int (ite X44 -(ite (= X42 4) 3 X42) X42))) (let ((X46 -Int (ite X44 -(ite (not (= X45 4)) 4 X45) X45))) (let ((X47 -Int (ite (not -(ite (= top.impl.usr.cruise_controller_CruiseController_ModeLogic_DelayOnsetAccel_Bounded_Count_Out! 20) true false)) 0 1))) (let ((X48 Bool (and (= X46 4) (and (= X47 1) (not X44))))) (let ((X49 -Int (ite X48 -(ite (= X46 4) 3 X46) X46))) (let ((X50 -Int (ite X48 -(ite (not (= X49 5)) 5 X49) X49))) (let ((X51 Bool (or X48 X44))) (let ((X52 -Int (ite (not -(ite (= top.impl.usr.cruise_controller_CruiseController_ModeLogic_DelayOnsetDecel_Bounded_Count_Out! 20) true false)) 0 1))) (let ((X53 Bool (and (= X50 4) (and (= X52 1) (not X51))))) (let ((X54 -Int (ite X53 -(ite (= X50 4) 3 X50) X50))) (let ((X55 -Int (ite X53 -(ite (not -(= X54 6)) 6 X54) X54))) (let ((X56 Bool (or X53 X51))) (let ((X57 Bool (and (= X55 6) (and (= X52 0) (not X56))))) (let ((X58 -Int (ite X57 -(ite (= X55 6) 3 X55) X55))) (let ((X59 -Int (ite X57 -(ite (not -(= X58 4)) 4 X58) X58))) (let ((X60 Bool -(or X57 X56))) (let ((X61 Bool -(and (= X59 5) (and (= X47 0) (not X60))))) (let ((X62 -Int (ite X61 -(ite (= X59 5) 3 X59) X59))) (let ((X63 -Int (ite X61 -(ite (not -(= X62 4)) 4 X62) X62))) (and (= top.impl.usr.chart_CruiseController_ModeLogic_mode_logic____wakeup___! true) (= top.impl.usr.chart_CruiseController_ModeLogic_mode_logic_final_state_states___root! -(ite top.impl.usr.chart_CruiseController_ModeLogic_mode_logic____wakeup___! -(ite top.impl.usr.chart_CruiseController_ModeLogic_mode_logic_rlt_evtInitStep! X2 -(ite (and (not X17) (and (>= X16 2) (<= X16 -8))) (ite (and (not X43) (and (>= X42 -3) (<= X42 -6))) X63 X42) X16)) X1)) (<= 0 X47 1) (<= 0 X22 1) (<= 0 X18 1) (<= 0 X7 1) (<= 0 X52 1) (not top.res.init_flag!))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ) -(define-fun -prop ( -(top.usr.onOff Bool) (top.usr.decelSet Bool) (top.usr.accelResume Bool) (top.usr.cancel Bool) (top.usr.brakePedal Bool) (top.usr.carGear Int) (top.usr.carSpeed Real) (top.usr.validInputs Bool) (top.usr.OK Bool) (top.res.init_flag Bool) (top.impl.usr.chart_CruiseController_ModeLogic_mode_logic____wakeup___ Bool) (top.impl.usr.chart_CruiseController_ModeLogic_mode_logic_rlt_evtInitStep Bool) (top.impl.usr.chart_CruiseController_ModeLogic_mode_logic_final_state_states___root Int) (top.impl.usr.cruise_controller_CruiseController_ModeLogic_DelayOnsetAccel_Bounded_Count_Out Int) (top.impl.usr.cruise_controller_CruiseController_ModeLogic_DelayOnsetDecel_Bounded_Count_Out Int) ) Bool - top.usr.OK -) -(inv-constraint str_invariant init trans prop) -(check-synth) diff --git a/test/regress/regress1/sygus/max.sy b/test/regress/regress1/sygus/max.sy new file mode 100644 index 000000000..37ed848ef --- /dev/null +++ b/test/regress/regress1/sygus/max.sy @@ -0,0 +1,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) diff --git a/test/regress/regress1/sygus/mpg_guard1-dd.sy b/test/regress/regress1/sygus/mpg_guard1-dd.sy deleted file mode 100644 index 31800a36f..000000000 --- a/test/regress/regress1/sygus/mpg_guard1-dd.sy +++ /dev/null @@ -1,27 +0,0 @@ -; EXPECT: unsat -; COMMAND-LINE: --sygus-out=status -(set-logic LIA) - -(synth-fun eq1 ( (x Int) (y Int) ) Int - ((Start Int (x - y - 0 - (+ Start Start) - (- Start Start) - (ite StartBool Start Start))) - (StartBool Bool ((and StartBool StartBool) - (<= Start Start) - (= Start Start))))) - -(define-fun iteB (( b1 Bool ) (b2 Bool ) (b3 Bool )) Bool (or (and b1 b2) (and (not b1) b3))) - -(declare-var x Int) -(declare-var y Int) - -(constraint (iteB (>= x 0) - (= (eq1 x y) (+ x x)) - (= (eq1 x y) x) -)) - -(check-synth) - diff --git a/test/regress/regress1/sygus/multi-fun-polynomial2.sy b/test/regress/regress1/sygus/multi-fun-polynomial2.sy new file mode 100644 index 000000000..22a2e0a4b --- /dev/null +++ b/test/regress/regress1/sygus/multi-fun-polynomial2.sy @@ -0,0 +1,35 @@ +; EXPECT: unsat +; COMMAND-LINE: --sygus-out=status + +(set-logic LIA) + +(synth-fun addExpr1 ((x Int) (y Int)) Int + ((Start Int (x + y + 0 + 1 + (+ Start Start) + (- Start Start) + )) + )) + +(synth-fun addExpr2 ((x Int) (y Int)) Int + ((Start Int (x + y + 0 + 1 + (+ Start Start) + (- Start Start) + )) + )) + + +(declare-var x Int) +(declare-var y Int) + +(constraint (= (+ (addExpr1 x y) (addExpr2 y x)) (- x y))) + + +(check-synth) + +; (x, y), (x-y, 0) ... are valid solutions diff --git a/test/regress/regress1/sygus/nflat-fwd-3.sy b/test/regress/regress1/sygus/nflat-fwd-3.sy new file mode 100644 index 000000000..a1776cf93 --- /dev/null +++ b/test/regress/regress1/sygus/nflat-fwd-3.sy @@ -0,0 +1,11 @@ +; EXPECT: unsat +; COMMAND-LINE: --sygus-out=status +(set-logic LIA) +(synth-fun f ((x Int)) Int + ((Start Int ((+ (+ Con Con) Con) x)) + (Con Int (0 1)))) + +(declare-var x Int) +(constraint (= (f x) 2)) +(check-synth) + diff --git a/test/regress/regress1/sygus/nflat-fwd.sy b/test/regress/regress1/sygus/nflat-fwd.sy new file mode 100644 index 000000000..da26a6c93 --- /dev/null +++ b/test/regress/regress1/sygus/nflat-fwd.sy @@ -0,0 +1,11 @@ +; EXPECT: unsat +; COMMAND-LINE: --sygus-out=status +(set-logic LIA) +(synth-fun f ((x Int)) Int + ((Start Int ((+ Con Con) (+ (+ Start Start) Con) x)) + (Con Int (0 1)))) + +(declare-var x Int) +(constraint (= (f x) (* 2 x))) +(check-synth) + diff --git a/test/regress/regress1/sygus/nia-max-square-ns.sy b/test/regress/regress1/sygus/nia-max-square-ns.sy new file mode 100644 index 000000000..6e7f70ff0 --- /dev/null +++ b/test/regress/regress1/sygus/nia-max-square-ns.sy @@ -0,0 +1,13 @@ +; EXPECT: unsat +; COMMAND-LINE: --cegqi-si=all --sygus-out=status --nl-ext-tplanes +(set-logic NIA) + +(synth-fun max ((x Int) (y Int)) Int) + +(declare-var x Int) +(declare-var y Int) + +(constraint (>= (max x y) (* x x))) +(constraint (>= (max x y) (* y y))) + +(check-synth) diff --git a/test/regress/regress1/sygus/nia-max-square.sy b/test/regress/regress1/sygus/nia-max-square.sy deleted file mode 100644 index e023e837b..000000000 --- a/test/regress/regress1/sygus/nia-max-square.sy +++ /dev/null @@ -1,21 +0,0 @@ -; EXPECT: unsat -; COMMAND-LINE: --sygus-out=status --nl-ext-tplanes -(set-logic NIA) - -(synth-fun max ((x Int) (y Int)) Int - ((Start Int (0 1 x y - (+ Start Start) - (- 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 x))) -(constraint (>= (max x y) (* y y))) - -(check-synth) diff --git a/test/regress/regress1/sygus/no-flat-simp.sy b/test/regress/regress1/sygus/no-flat-simp.sy new file mode 100644 index 000000000..c0f0e4c0f --- /dev/null +++ b/test/regress/regress1/sygus/no-flat-simp.sy @@ -0,0 +1,20 @@ +; EXPECT: unsat +; COMMAND-LINE: --sygus-out=status + +(set-logic LIA) + +(synth-fun f ((x Int) (y Int)) Int + ((Start Int (x + y + 0 + (- Start Start) + (+ Start (+ Start Start)))))) + +(declare-var x Int) +(declare-var y Int) + +(constraint (= (f x y) (+ x y))) + + +(check-synth) + diff --git a/test/regress/regress1/sygus/no-mention.sy b/test/regress/regress1/sygus/no-mention.sy new file mode 100644 index 000000000..f964d6039 --- /dev/null +++ b/test/regress/regress1/sygus/no-mention.sy @@ -0,0 +1,15 @@ +; EXPECT: unsat +; COMMAND-LINE: --sygus-out=status +(set-logic LIA) + +(synth-fun p ((x Int) (y Int)) Int) +(synth-fun m ((x Int) (y Int)) Int) +(synth-fun n ((x Int)) Int) + +(declare-var x Int) +(declare-var y Int) + +(constraint (>= (m x y) x)) + +(check-synth) + diff --git a/test/regress/regress1/sygus/process-10-vars.sy b/test/regress/regress1/sygus/process-10-vars.sy new file mode 100644 index 000000000..523abd70d --- /dev/null +++ b/test/regress/regress1/sygus/process-10-vars.sy @@ -0,0 +1,24 @@ +; COMMAND-LINE: --cegqi-si=none --sygus-out=status +; EXPECT: unsat +(set-logic LIA) + +(synth-fun f ((x1 Int) (x2 Int) (x3 Int) (x4 Int) (x5 Int) (x6 Int) (x7 Int) (x8 Int) (x9 Int) (x10 Int)) Int) + + +(declare-var x1 Int) +(declare-var x2 Int) +(declare-var x3 Int) +(declare-var x4 Int) +(declare-var x5 Int) +(declare-var x6 Int) +(declare-var x7 Int) +(declare-var x8 Int) +(declare-var x9 Int) +(declare-var x10 Int) + +; should be able to determine that arguments 1...6, 8...10 are irrelevant for f + +(constraint (>= (f x1 x2 x3 x4 x5 x6 x7 x8 x9 x10) (+ x7 x7 x7))) + +(check-synth) + diff --git a/test/regress/regress1/sygus/process-arg-invariance.sy b/test/regress/regress1/sygus/process-arg-invariance.sy deleted file mode 100644 index 3c18b6c75..000000000 --- a/test/regress/regress1/sygus/process-arg-invariance.sy +++ /dev/null @@ -1,18 +0,0 @@ -; COMMAND-LINE: --cegqi-si=none --sygus-out=status --no-sygus-add-const-grammar -; EXPECT: unsat -(set-logic LIA) - -(synth-fun f ((x1 Int) (x2 Int) (x3 Int) (x4 Int) (x5 Int) (x6 Int) (x7 Int) (x8 Int) (x9 Int) (x10 Int)) Int) - - -(declare-var x Int) -(declare-var y Int) - -; should be able to determine that only 3 arguments -; (one of 5...9, one of 1 or 4, one of 2 or 3) is relevant for f - -(constraint (> (f (+ x x) (+ x 1) (+ x 1) (+ x x) x x x x x 0) (+ x x x))) -(constraint (<= (f x x x x x x x x x 0) (+ x x x))) - -(check-synth) - diff --git a/test/regress/regress1/sygus/qe.sy b/test/regress/regress1/sygus/qe.sy new file mode 100644 index 000000000..77e16efcb --- /dev/null +++ b/test/regress/regress1/sygus/qe.sy @@ -0,0 +1,12 @@ +; EXPECT: unsat +; COMMAND-LINE: --cegqi-si=all --sygus-out=status --sygus-qe-preproc +(set-logic LIA) + +(synth-fun f ((x Int)) Int) + +(declare-var x Int) +(declare-var y Int) + +(constraint (=> (or (= y 2) (= y 3)) (> (f x) y))) + +(check-synth) diff --git a/test/regress/regress1/sygus/strings-concat-3-args.sy b/test/regress/regress1/sygus/strings-concat-3-args.sy new file mode 100644 index 000000000..6628ff746 --- /dev/null +++ b/test/regress/regress1/sygus/strings-concat-3-args.sy @@ -0,0 +1,18 @@ +; EXPECT: unsat +; COMMAND-LINE: --sygus-out=status +(set-logic SLIA) +(synth-fun f ((x String)) String +((Start String (ntString)) + +(ntString String (x "" (str.++ ntStringConst ntString ntString))) + +(ntStringConst String ("a" "b" " ")) + +)) + +; can be solved with concat PBE strategy, although we currently are not (issue #1259) +; regardless, this is small enough to solve quickly +(constraint (= (f "def") "ab def")) + +(check-synth) + diff --git a/test/regress/regress1/sygus/strings-double-rec.sy b/test/regress/regress1/sygus/strings-double-rec.sy new file mode 100644 index 000000000..ea9caadea --- /dev/null +++ b/test/regress/regress1/sygus/strings-double-rec.sy @@ -0,0 +1,16 @@ +; EXPECT: unsat +; COMMAND-LINE: --sygus-out=status +(set-logic SLIA) + +(synth-fun f ((name String)) String + ((Start String (name "A" "B" "" (str.++ Start1 Start2))) + (Start1 String (name "A" "B" "")) + (Start2 String (name "B" "A" (str.++ Start2 Start))) +)) + + +(declare-var name String) + +(constraint (= (f "BB") "AAAAAAAAAAAA")) + +(check-synth) diff --git a/test/regress/regress1/sygus/strings-small.sy b/test/regress/regress1/sygus/strings-small.sy new file mode 100644 index 000000000..7d976ff39 --- /dev/null +++ b/test/regress/regress1/sygus/strings-small.sy @@ -0,0 +1,35 @@ +; EXPECT: unsat +; COMMAND-LINE: --sygus-out=status +(set-logic SLIA) +(synth-fun f ((firstname String) (lastname String)) String +((Start String (ntString)) + +(ntString String ( +firstname +lastname +" " +(str.++ ntString ntString))) + +(ntInt Int ( +0 +1 +2 +(+ ntInt ntInt) +(- ntInt ntInt) +(str.len ntString) +(str.to.int ntString) +(str.indexof ntString ntString ntInt))) + +(ntBool Bool ( +true +false +(str.prefixof ntString ntString) +(str.suffixof ntString ntString) +(str.contains ntString ntString))) + +)) + +(constraint (= (f "Nancy" "FreeHafer") "Nancy FreeHafer")) + +(check-synth) + diff --git a/test/regress/regress1/sygus/strings-template-infer-unused.sy b/test/regress/regress1/sygus/strings-template-infer-unused.sy new file mode 100644 index 000000000..d0bee5564 --- /dev/null +++ b/test/regress/regress1/sygus/strings-template-infer-unused.sy @@ -0,0 +1,16 @@ +; EXPECT: unsat +; COMMAND-LINE: --sygus-out=status +(set-logic SLIA) + +(define-fun cA ((x String) (w String) (y String) (z String)) String (str.++ (str.++ x "A") y)) + +(synth-fun f ((name String)) String + ((Start String (name "A" "B" "" + (cA Start Start Start Start))))) + + +(declare-var name String) + +(constraint (= (f "BB") "AAAAAAAAAAAA")) + +(check-synth) diff --git a/test/regress/regress1/sygus/strings-template-infer.sy b/test/regress/regress1/sygus/strings-template-infer.sy new file mode 100644 index 000000000..13c4d7dac --- /dev/null +++ b/test/regress/regress1/sygus/strings-template-infer.sy @@ -0,0 +1,16 @@ +; EXPECT: unsat +; COMMAND-LINE: --sygus-out=status +(set-logic SLIA) + +(define-fun cA ((x String) (y String)) String (str.++ (str.++ x "A") y)) + +(synth-fun f ((name String)) String + ((Start String (name "A" "B" "" + (cA Start Start))))) + + +(declare-var name String) + +(constraint (= (f "BB") "AAAAAAAAAAAA")) + +(check-synth) diff --git a/test/regress/regress1/sygus/strings-trivial-simp.sy b/test/regress/regress1/sygus/strings-trivial-simp.sy new file mode 100644 index 000000000..f5e41a8f5 --- /dev/null +++ b/test/regress/regress1/sygus/strings-trivial-simp.sy @@ -0,0 +1,14 @@ +; EXPECT: unsat +; COMMAND-LINE: --sygus-out=status +(set-logic SLIA) + +(synth-fun f ((name String)) String + ((Start String (name "A" "B" + (str.++ Start Start))))) + + +(declare-var name String) + +(constraint (= (f "BB") "AAAAAAAAAAAABAAAAAAAABAAA")) + +(check-synth) diff --git a/test/regress/regress1/sygus/strings-trivial-two-type.sy b/test/regress/regress1/sygus/strings-trivial-two-type.sy new file mode 100644 index 000000000..86c71aa3a --- /dev/null +++ b/test/regress/regress1/sygus/strings-trivial-two-type.sy @@ -0,0 +1,18 @@ +; EXPECT: unsat +; COMMAND-LINE: --sygus-out=status +(set-logic SLIA) + +(synth-fun f ((name String)) String + ((Start String (ntString)) + (ntString String (name "B" "" + (str.++ ntStringC ntString))) + (ntStringC String (name "A" "")) + + )) + + +(declare-var name String) + +(constraint (= (f "B") "AAAAAAAAAAAAAAAAAAAAAAAAA")) + +(check-synth) diff --git a/test/regress/regress1/sygus/strings-trivial.sy b/test/regress/regress1/sygus/strings-trivial.sy new file mode 100644 index 000000000..9af0a1bb1 --- /dev/null +++ b/test/regress/regress1/sygus/strings-trivial.sy @@ -0,0 +1,15 @@ +; EXPECT: unsat +; COMMAND-LINE: --sygus-out=status +(set-logic SLIA) + +(synth-fun f ((name String)) String + ((Start String (ntString)) + (ntString String (name "A" "B" + (str.++ ntString ntString))))) + + +(declare-var name String) + +(constraint (= (f "B") "AAAAAAAAAAAAAAAAAAAAAAAAA")) + +(check-synth) diff --git a/test/regress/regress1/sygus/sygus-dt.sy b/test/regress/regress1/sygus/sygus-dt.sy new file mode 100644 index 000000000..d496e3fdc --- /dev/null +++ b/test/regress/regress1/sygus/sygus-dt.sy @@ -0,0 +1,16 @@ +; EXPECT: unsat +; COMMAND-LINE: --sygus-out=status + +(set-logic LIA) + +(declare-datatypes ((List 0)) (((cons (head Int) (tail List)) (nil)))) +(define-fun g ((x Int)) List (cons (+ x 1) nil)) +(define-fun i () List (cons 3 nil)) + +(synth-fun f ((x Int)) List ((Start List ((g StartInt) i (cons StartInt Start) (nil) (tail Start))) + (StartInt Int (x 0 1 (+ StartInt StartInt))))) + +(declare-var x Int) + +(constraint (= (f x) (cons x nil))) +(check-synth) diff --git a/test/regress/regress1/sygus/three.sy b/test/regress/regress1/sygus/three.sy deleted file mode 100644 index 831e5beb1..000000000 --- a/test/regress/regress1/sygus/three.sy +++ /dev/null @@ -1,30 +0,0 @@ -; EXPECT: unsat -; COMMAND-LINE: --sygus-out=status - -(set-logic LIA) - -(synth-fun f ((x Int)) Int - ((Start Int ( - x - 3 - 7 - 10 - (* Start Start) - (mod Start Start))))) - -(declare-var x Int) - -(constraint (= (f x) (f (+ x 10)))) -(constraint (= (f 1) 3)) -(constraint (= (f 2) 6)) -(constraint (= (f 3) 9)) -(constraint (= (f 4) 2)) -(constraint (= (f 5) 5)) -(constraint (= (f 6) 8)) -(constraint (= (f 7) 1)) -(constraint (= (f 8) 4)) -(constraint (= (f 9) 7)) -(constraint (= (f 0) 0)) - -(check-synth) - diff --git a/test/regress/regress1/sygus/tl-type-0.sy b/test/regress/regress1/sygus/tl-type-0.sy new file mode 100644 index 000000000..ceda89d78 --- /dev/null +++ b/test/regress/regress1/sygus/tl-type-0.sy @@ -0,0 +1,11 @@ +; EXPECT: unsat +; COMMAND-LINE: --cegqi-si=none --sygus-out=status +(set-logic LIA) +(synth-fun f ((x Int)) Int + ((Start Int ((+ Term Term))) + (Term Int (x 0)))) + +(declare-var x Int) +(constraint (= (f x) 0)) +(check-synth) + diff --git a/test/regress/regress1/sygus/tl-type-4x.sy b/test/regress/regress1/sygus/tl-type-4x.sy new file mode 100644 index 000000000..bf8eee5ee --- /dev/null +++ b/test/regress/regress1/sygus/tl-type-4x.sy @@ -0,0 +1,11 @@ +; EXPECT: unsat +; COMMAND-LINE: --cegqi-si=none --sygus-out=status +(set-logic LIA) +(synth-fun f ((x Int)) Int + ((Start Int (Term (+ Start Start))) + (Term Int (x 0)))) + +(declare-var x Int) +(constraint (= (f x) (* 4 x))) +(check-synth) + diff --git a/test/regress/regress1/sygus/tl-type.sy b/test/regress/regress1/sygus/tl-type.sy new file mode 100644 index 000000000..6f25a570e --- /dev/null +++ b/test/regress/regress1/sygus/tl-type.sy @@ -0,0 +1,11 @@ +; EXPECT: unsat +; COMMAND-LINE: --cegqi-si=none --sygus-out=status +(set-logic LIA) +(synth-fun f ((x Int)) Int + ((Start Int (Term (+ Start Start))) + (Term Int (x 0)))) + +(declare-var x Int) +(constraint (= (f x) (* 3 x))) +(check-synth) + diff --git a/test/regress/regress1/sygus/triv-type-mismatch-si.sy b/test/regress/regress1/sygus/triv-type-mismatch-si.sy new file mode 100644 index 000000000..37c5a7f53 --- /dev/null +++ b/test/regress/regress1/sygus/triv-type-mismatch-si.sy @@ -0,0 +1,13 @@ +; EXPECT: unsat +; COMMAND-LINE: --sygus-out=status +(set-logic LIA) + +(synth-fun R ((y Int)) Bool) +(synth-fun e () Int) + +(declare-var x Int) + +(constraint (=> (= x e) (R x))) + +(check-synth) + diff --git a/test/regress/regress1/sygus/twolets1.sy b/test/regress/regress1/sygus/twolets1.sy new file mode 100644 index 000000000..06d2ecb71 --- /dev/null +++ b/test/regress/regress1/sygus/twolets1.sy @@ -0,0 +1,40 @@ +; EXPECT: unsat +; COMMAND-LINE: --cegqi-si=all --sygus-out=status +(set-logic LIA) + +;; f1 is x plus 2 ;; f2 is 2x plus 5 + +(define-fun let0 ((x Int) (y Int) (z Int)) Int (+ (+ y x) z)) + +(synth-fun f1 ((x Int)) Int + ( + (Start Int ( + (let0 Intx CInt CInt) + ) + ) + (Intx Int (x)) + (CInt Int (0 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15)) + + ) +) + +(synth-fun f2 ((x Int)) Int + ( + (Start Int (x + (let0 Intx Start CInt) + ) + ) + (Intx Int (x)) + (CInt Int (0 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15)) + + ) +) + + +(declare-var x Int) + +(constraint (= (+ (f1 x)(f2 x)) (+ (+ x x) (+ x 8)))) +(constraint (= (- (f2 x)(f1 x)) (+ x 2))) + +(check-synth) + diff --git a/test/regress/regress1/sygus/twolets2-orig.sy b/test/regress/regress1/sygus/twolets2-orig.sy new file mode 100644 index 000000000..50f7ad544 --- /dev/null +++ b/test/regress/regress1/sygus/twolets2-orig.sy @@ -0,0 +1,28 @@ +; EXPECT: unsat +; COMMAND-LINE: --cegqi-si=all --sygus-out=status +(set-logic LIA) +(synth-fun f1 ((x Int)) Int + ( + (Start Int ( + (let ((y Int CInt) (z Int CInt)) (+ (+ y x) z)) + ) + ) + (CInt Int (0 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15)) + + ) +) +(synth-fun f2 ((x Int)) Int + ( + (Start Int (x + (let ((y Int Start) (z Int CInt)) (+ (+ y x) z)) + ) + ) + (CInt Int (0 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15)) + + ) +) +(declare-var x1 Int) +(declare-var x2 Int) +(constraint (= (+ (f1 x1)(f2 x2)) (+ (+ x2 x2) (+ x1 8)))) +(check-synth) + diff --git a/test/regress/regress1/sygus/inv_gen_n_c11.sy b/test/regress/regress1/sygus/unbdd_inv_gen_winf1.sy index 9e04682a5..d45cec38b 100644 --- a/test/regress/regress1/sygus/inv_gen_n_c11.sy +++ b/test/regress/regress1/sygus/unbdd_inv_gen_winf1.sy @@ -1,7 +1,8 @@ ; EXPECT: unsat ; COMMAND-LINE: --sygus-out=status + (set-logic LIA) -(synth-fun inv ((i Int) (l Int)) Bool +(synth-fun inv ((x Int)) Bool ( (Start Bool ((and AtomicFormula AtomicFormula) (or AtomicFormula AtomicFormula))) @@ -9,8 +10,8 @@ (Sum Int ((+ Term Term))) (Term Int ((* Sign Var))) (Sign Int (0 1 -1)) - (Var Int (i l)) - (Const Int (-7 -6 -5 -4 -3 -2 -1 0 1 2 3 4 5 6 7)) + (Var Int (x)) + (Const Int ((+ Const Const) (- Const Const) 0 1)) ) ) @@ -23,14 +24,13 @@ (define-fun or4 ((b1 Bool) (b2 Bool) (b3 Bool) (b4 Bool)) Bool (or (or3 b1 b2 b3) b4)) (define-fun or5 ((b1 Bool) (b2 Bool) (b3 Bool) (b4 Bool) (b5 Bool)) Bool (or (or4 b1 b2 b3 b4) b5)) -(declare-var i Int) -(declare-var l Int) -(declare-var i1 Int) -(declare-var l1 Int) -(declare-var l2 Int) +(declare-var s Int) + +(declare-var x Int) -(constraint (implies (= l 0) (inv i l))) -(constraint (implies (and5 (inv i l) (implies (= l 4) (= l1 0)) (implies (not (= l 4)) (= l1 l)) (not (or (< l1 0) (>= l1 5))) (= l2 (+ l1 1))) (inv i l2))) -(constraint (implies (and4 (inv i l) (implies (= l 4) (= l1 0)) (implies (not (= l 4)) (= l1 l)) (or (< l1 0) (>= l1 5))) false)) +(constraint (implies (= x 0) (inv x))) +(constraint (implies (inv x) (= x 0))) +(constraint (implies (inv x) (inv x))) +(constraint (implies (and (inv x) false) (not (= x 0)))) (check-synth) |