diff options
| author | Abdalrhman Mohamed <32971963+abdoo8080@users.noreply.github.com> | 2020-03-21 22:33:15 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-03-21 22:33:15 -0500 |
| commit | 37107284adaad3d24da0ad15cac8c88af444aeef (patch) | |
| tree | d98c5a6bf3608a50e828b129d8d8c45b2c49fc58 /test/regress/regress2 | |
| parent | a507aa5f1904055782e1ba01083faf1fd0fb86f7 (diff) | |
Convert V1 Sygus files to V2. (#4136)
Diffstat (limited to 'test/regress/regress2')
23 files changed, 376 insertions, 403 deletions
diff --git a/test/regress/regress2/sygus/DRAGON_1.lus.sy b/test/regress/regress2/sygus/DRAGON_1.lus.sy index ec2974c70..4d9510ade 100644 --- a/test/regress/regress2/sygus/DRAGON_1.lus.sy +++ b/test/regress/regress2/sygus/DRAGON_1.lus.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --sygus-out=status --sygus-unif-pi=complete --cegis-sample=use +; COMMAND-LINE: --lang=sygus2 --sygus-out=status --sygus-unif-pi=complete --cegis-sample=use (set-logic LIA) @@ -740,12 +740,12 @@ (= DRAGON.usr.exclusive_a_0 0) (let ((X1 - Bool (let - ((X1 Int DRAGON.res.nondet_4) - (X2 Int DRAGON.res.nondet_3) - (X3 Int DRAGON.res.nondet_2) - (X4 Int DRAGON.res.nondet_1) - (X5 Int DRAGON.res.nondet_0)) + (let + ((X1 DRAGON.res.nondet_4) + (X2 DRAGON.res.nondet_3) + (X3 DRAGON.res.nondet_2) + (X4 DRAGON.res.nondet_1) + (X5 DRAGON.res.nondet_0)) (and (and (and (and (>= X5 1) (= X4 0)) (= X3 0)) (= X2 0)) (= X1 0))))) @@ -755,63 +755,63 @@ (= DRAGON.usr.dirty_a_0 0) (let ((X2 - Bool (let - ((X2 Int DRAGON.res.nondet_9) - (X3 Int DRAGON.res.nondet_8) - (X4 Int DRAGON.res.nondet_7) - (X5 Int DRAGON.res.nondet_6) - (X6 Int DRAGON.res.nondet_5)) + (let + ((X2 DRAGON.res.nondet_9) + (X3 DRAGON.res.nondet_8) + (X4 DRAGON.res.nondet_7) + (X5 DRAGON.res.nondet_6) + (X6 DRAGON.res.nondet_5)) (and (>= X6 1) (>= (+ (+ (+ X5 X4) X3) X2) 1))))) (and (= DRAGON.impl.usr.mem_init_a_0 DRAGON.usr.init_invalid_a_0) (= DRAGON.usr.invalid_a_0 DRAGON.impl.usr.mem_init_a_0) (let ((X3 - Bool (let - ((X3 Int DRAGON.res.nondet_21) - (X4 Int DRAGON.res.nondet_20) - (X5 Int DRAGON.res.nondet_19) - (X6 Int DRAGON.res.nondet_18) - (X7 Int DRAGON.res.nondet_17)) + (let + ((X3 DRAGON.res.nondet_21) + (X4 DRAGON.res.nondet_20) + (X5 DRAGON.res.nondet_19) + (X6 DRAGON.res.nondet_18) + (X7 DRAGON.res.nondet_17)) (and (and (and (and (>= X7 1) (= X6 0)) (= X5 0)) (= X4 0)) (= X3 0))))) (let ((X4 - Bool (let - ((X4 Int DRAGON.res.nondet_26) - (X5 Int DRAGON.res.nondet_25) - (X6 Int DRAGON.res.nondet_24) - (X7 Int DRAGON.res.nondet_23) - (X8 Int DRAGON.res.nondet_22)) + (let + ((X4 DRAGON.res.nondet_26) + (X5 DRAGON.res.nondet_25) + (X6 DRAGON.res.nondet_24) + (X7 DRAGON.res.nondet_23) + (X8 DRAGON.res.nondet_22)) (and (>= X8 1) (>= (+ (+ (+ X7 X6) X5) X4) 1))))) (let - ((X5 Bool (let ((X5 Int DRAGON.res.nondet_27)) (>= X5 1)))) + ((X5 (let ((X5 DRAGON.res.nondet_27)) (>= X5 1)))) (let - ((X6 Bool (let ((X6 Int DRAGON.res.nondet_28)) (>= X6 1)))) + ((X6 (let ((X6 DRAGON.res.nondet_28)) (>= X6 1)))) (let - ((X7 Bool (let ((X7 Int DRAGON.res.nondet_29)) (>= X7 1)))) + ((X7 (let ((X7 DRAGON.res.nondet_29)) (>= X7 1)))) (let - ((X8 Bool (let ((X8 Int DRAGON.res.nondet_30)) (>= X8 1)))) + ((X8 (let ((X8 DRAGON.res.nondet_30)) (>= X8 1)))) (let - ((X9 Bool (let ((X9 Int DRAGON.res.nondet_10)) (>= X9 1)))) + ((X9 (let ((X9 DRAGON.res.nondet_10)) (>= X9 1)))) (let ((X10 - Bool (let - ((X10 Int DRAGON.res.nondet_12) - (X11 Int DRAGON.res.nondet_11)) + (let + ((X10 DRAGON.res.nondet_12) + (X11 DRAGON.res.nondet_11)) (and (= X11 1) (= X10 0))))) (let ((X11 - Bool (let - ((X11 Int DRAGON.res.nondet_14) - (X12 Int DRAGON.res.nondet_13)) + (let + ((X11 DRAGON.res.nondet_14) + (X12 DRAGON.res.nondet_13)) (and (= X12 0) (= X11 1))))) (let ((X12 - Bool (let - ((X12 Int DRAGON.res.nondet_16) - (X13 Int DRAGON.res.nondet_15)) + (let + ((X12 DRAGON.res.nondet_16) + (X13 DRAGON.res.nondet_15)) (>= (+ X13 X12) 2)))) (and (= @@ -898,10 +898,10 @@ ) Bool (let - ((X1 Bool (>= DRAGON.usr.exclusive_a_0 1))) + ((X1 (>= DRAGON.usr.exclusive_a_0 1))) (let ((X2 - Bool (and + (and (>= DRAGON.usr.invalid_a_0 1) (>= (+ @@ -911,10 +911,10 @@ DRAGON.usr.shared_dirty_a_0) 1)))) (let - ((X3 Bool (>= DRAGON.usr.exclusive_a_0 1))) + ((X3 (>= DRAGON.usr.exclusive_a_0 1))) (let ((X4 - Bool (and + (and (>= DRAGON.usr.invalid_a_0 1) (>= (+ @@ -925,7 +925,7 @@ 1)))) (let ((X5 - Bool (and + (and (and (and (and (>= DRAGON.usr.invalid_a_0 1) (= DRAGON.usr.dirty_a_0 0)) @@ -952,12 +952,12 @@ (ite X1 (- DRAGON.usr.exclusive_a_0 1) DRAGON.usr.exclusive_a_0) DRAGON.usr.exclusive_a_0)))))) (let - ((X6 Bool (>= DRAGON.usr.shared_a_0 1))) + ((X6 (>= DRAGON.usr.shared_a_0 1))) (let - ((X7 Bool (>= (+ DRAGON.usr.shared_dirty_a_0 DRAGON.usr.shared_a_0) 2))) + ((X7 (>= (+ DRAGON.usr.shared_dirty_a_0 DRAGON.usr.shared_a_0) 2))) (let ((X8 - Bool (and + (and (= DRAGON.usr.shared_dirty_a_0 0) (= DRAGON.usr.shared_a_0 1)))) (and @@ -993,10 +993,10 @@ (ite X6 (- DRAGON.usr.shared_a_0 1) DRAGON.usr.shared_a_0) DRAGON.usr.shared_a_0)))))) (let - ((X9 Bool (>= DRAGON.usr.shared_dirty_a_0 1))) + ((X9 (>= DRAGON.usr.shared_dirty_a_0 1))) (let ((X10 - Bool (and + (and (= DRAGON.usr.shared_dirty_a_0 1) (= DRAGON.usr.shared_a_0 0)))) (and @@ -1025,10 +1025,10 @@ DRAGON.usr.shared_dirty_a_0) DRAGON.usr.shared_dirty_a_0)))))) (let - ((X11 Bool (>= DRAGON.usr.dirty_a_0 1))) + ((X11 (>= DRAGON.usr.dirty_a_0 1))) (let ((X12 - Bool (and + (and (and (and (and @@ -1183,7 +1183,7 @@ (and (= top.res.abs_7_a_0 (and top.res.abs_6_a_0 (> top.usr.init_invalid_a_0 0))) (let - ((X1 Bool top.res.abs_5_a_0)) + ((X1 top.res.abs_5_a_0)) (and (= top.usr.OK_a_0 (=> top.res.abs_8_a_0 (not X1))) (__node_init_DRAGON_0 @@ -1352,7 +1352,7 @@ (and (= top.res.abs_7_a_1 (and top.res.abs_6_a_1 (> top.usr.init_invalid_a_1 0))) (let - ((X1 Bool top.res.abs_5_a_1)) + ((X1 top.res.abs_5_a_1)) (and (= top.usr.OK_a_1 (=> top.res.abs_8_a_1 (not X1))) (__node_trans_DRAGON_0 @@ -1501,66 +1501,37 @@ (top.res.inst_0 Bool) )) -(declare-fun top.res.nondet_30 () Int) -(declare-fun top.res.nondet_29 () Int) -(declare-fun top.res.nondet_28 () Int) -(declare-fun top.res.nondet_27 () Int) -(declare-fun top.res.nondet_26 () Int) -(declare-fun top.res.nondet_25 () Int) -(declare-fun top.res.nondet_24 () Int) -(declare-fun top.res.nondet_23 () Int) -(declare-fun top.res.nondet_22 () Int) -(declare-fun top.res.nondet_21 () Int) -(declare-fun top.res.nondet_20 () Int) -(declare-fun top.res.nondet_19 () Int) -(declare-fun top.res.nondet_18 () Int) -(declare-fun top.res.nondet_17 () Int) -(declare-fun top.res.nondet_16 () Int) -(declare-fun top.res.nondet_15 () Int) -(declare-fun top.res.nondet_14 () Int) -(declare-fun top.res.nondet_13 () Int) -(declare-fun top.res.nondet_12 () Int) -(declare-fun top.res.nondet_11 () Int) -(declare-fun top.res.nondet_10 () Int) -(declare-fun top.res.nondet_9 () Int) -(declare-fun top.res.nondet_8 () Int) -(declare-fun top.res.nondet_7 () Int) -(declare-fun top.res.nondet_6 () Int) -(declare-fun top.res.nondet_5 () Int) -(declare-fun top.res.nondet_4 () Int) -(declare-fun top.res.nondet_3 () Int) -(declare-fun top.res.nondet_2 () Int) -(declare-fun top.res.nondet_1 () Int) -(declare-fun top.res.nondet_0 () Int) - -(declare-primed-var top.usr.e01 Bool) -(declare-primed-var top.usr.e02 Bool) -(declare-primed-var top.usr.e03 Bool) -(declare-primed-var top.usr.e04 Bool) -(declare-primed-var top.usr.e05 Bool) -(declare-primed-var top.usr.e06 Bool) -(declare-primed-var top.usr.e07 Bool) -(declare-primed-var top.usr.e08 Bool) -(declare-primed-var top.usr.e09 Bool) -(declare-primed-var top.usr.e10 Bool) -(declare-primed-var top.usr.e11 Bool) -(declare-primed-var top.usr.e12 Bool) -(declare-primed-var top.usr.init_invalid Int) -(declare-primed-var top.usr.OK Bool) -(declare-primed-var top.res.init_flag Bool) -(declare-primed-var top.res.abs_0 Int) -(declare-primed-var top.res.abs_1 Int) -(declare-primed-var top.res.abs_2 Int) -(declare-primed-var top.res.abs_3 Int) -(declare-primed-var top.res.abs_4 Int) -(declare-primed-var top.res.abs_5 Bool) -(declare-primed-var top.res.abs_6 Bool) -(declare-primed-var top.res.abs_7 Bool) -(declare-primed-var top.res.abs_8 Bool) -(declare-primed-var top.res.inst_3 Bool) -(declare-primed-var top.res.inst_2 Int) -(declare-primed-var top.res.inst_1 Bool) -(declare-primed-var top.res.inst_0 Bool) +(declare-var top.res.nondet_30 Int) +(declare-var top.res.nondet_29 Int) +(declare-var top.res.nondet_28 Int) +(declare-var top.res.nondet_27 Int) +(declare-var top.res.nondet_26 Int) +(declare-var top.res.nondet_25 Int) +(declare-var top.res.nondet_24 Int) +(declare-var top.res.nondet_23 Int) +(declare-var top.res.nondet_22 Int) +(declare-var top.res.nondet_21 Int) +(declare-var top.res.nondet_20 Int) +(declare-var top.res.nondet_19 Int) +(declare-var top.res.nondet_18 Int) +(declare-var top.res.nondet_17 Int) +(declare-var top.res.nondet_16 Int) +(declare-var top.res.nondet_15 Int) +(declare-var top.res.nondet_14 Int) +(declare-var top.res.nondet_13 Int) +(declare-var top.res.nondet_12 Int) +(declare-var top.res.nondet_11 Int) +(declare-var top.res.nondet_10 Int) +(declare-var top.res.nondet_9 Int) +(declare-var top.res.nondet_8 Int) +(declare-var top.res.nondet_7 Int) +(declare-var top.res.nondet_6 Int) +(declare-var top.res.nondet_5 Int) +(declare-var top.res.nondet_4 Int) +(declare-var top.res.nondet_3 Int) +(declare-var top.res.nondet_2 Int) +(declare-var top.res.nondet_1 Int) +(declare-var top.res.nondet_0 Int) (define-fun init ( @@ -1597,7 +1568,7 @@ (and (= top.res.abs_7 (and top.res.abs_6 (> top.usr.init_invalid 0))) (let - ((X1 Bool top.res.abs_5)) + ((X1 top.res.abs_5)) (and (= top.usr.OK (=> top.res.abs_8 (not X1))) (__node_init_DRAGON_0 @@ -1741,7 +1712,7 @@ (and (= top.res.abs_7! (and top.res.abs_6! (> top.usr.init_invalid! 0))) (let - ((X1 Bool top.res.abs_5!)) + ((X1 top.res.abs_5!)) (and (= top.usr.OK! (=> top.res.abs_8! (not X1))) (__node_trans_DRAGON_0 diff --git a/test/regress/regress2/sygus/MPwL_d1s3.sy b/test/regress/regress2/sygus/MPwL_d1s3.sy index 5178cf86b..9ff13d5ab 100644 --- a/test/regress/regress2/sygus/MPwL_d1s3.sy +++ b/test/regress/regress2/sygus/MPwL_d1s3.sy @@ -1,29 +1,29 @@ ; EXPECT: unsat -; COMMAND-LINE: --sygus-out=status +; COMMAND-LINE: --lang=sygus2 --sygus-out=status (set-logic LIA) -(define-fun get-y ((currPoint Int)) Int +(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)) +(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)) +(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)) +(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 @@ -36,57 +36,57 @@ currPoint)))) (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))) + (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)))) + (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 (= 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 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 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))))))) + (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 (= 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 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 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))))))) + (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))) @@ -104,15 +104,16 @@ currPoint)))) (declare-var o1-3 Int) (synth-fun move ((currPoint Int) (o0 Int) (o1 Int)) Int + ((Start Int) (MoveId Int) (CondInt Int) (StartBool Bool)) ((Start Int ( MoveId (ite StartBool Start Start))) - (MoveId Int (0 + (MoveId Int (0 1 2 3 4 - )) + )) (CondInt Int ( (get-y currPoint) ;y coord (get-x currPoint) ;x coord @@ -122,7 +123,7 @@ currPoint)))) (get-x o1) (+ CondInt CondInt) (- CondInt CondInt) - -1 + (- 1) 0 1 2 @@ -133,16 +134,16 @@ currPoint)))) 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 + (>= CondInt CondInt))))) + +(constraint (let ((pos0 0)) (let ((mov0 (move pos0 99 98))) (let ((pos1 (interpret-move pos0 mov0))) (let ((mov1 (move pos1 o0-1 o1-1))) (let ((pos2 (interpret-move pos1 mov1))) (let ((mov2 (move pos2 o0-2 o1-2))) (let ((pos3 (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)))) diff --git a/test/regress/regress2/sygus/array_sum_dd.sy b/test/regress/regress2/sygus/array_sum_dd.sy index 6d3354d2d..2b4177843 100644 --- a/test/regress/regress2/sygus/array_sum_dd.sy +++ b/test/regress/regress2/sygus/array_sum_dd.sy @@ -1,11 +1,11 @@ ; EXPECT: unsat -; COMMAND-LINE: --sygus-out=status +; COMMAND-LINE: --lang=sygus2 --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))) +(synth-fun findSum ((y1 Int) (y2 Int)) Int ((Start Int) (BoolExpr Bool)) ( +(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))) +(constraint (=> (> (+ x1 x2) 0) (= (findSum x1 x2) x1))) +(constraint (=> (<= (+ x1 x2) 0) (= (findSum x1 x2) x2))) (check-synth) diff --git a/test/regress/regress2/sygus/cegisunif-depth1-bv.sy b/test/regress/regress2/sygus/cegisunif-depth1-bv.sy index 6b647b77d..6aa17ef30 100644 --- a/test/regress/regress2/sygus/cegisunif-depth1-bv.sy +++ b/test/regress/regress2/sygus/cegisunif-depth1-bv.sy @@ -1,10 +1,11 @@ ; EXPECT: unsat -; COMMAND-LINE: --sygus-unif-pi=complete --sygus-out=status +; COMMAND-LINE: --lang=sygus2 --sygus-unif-pi=complete --sygus-out=status (set-logic BV) -(synth-fun f ((x (BitVec 64)) (y (BitVec 64))) (BitVec 64) +(synth-fun f ((x (_ BitVec 64)) (y (_ BitVec 64))) (_ BitVec 64) + ((Start (_ BitVec 64)) (CBool Bool)) ( - (Start (BitVec 64) + (Start (_ BitVec 64) (#x0000000000000000 #x0000000000000001 x y (bvnot Start) (bvand Start Start) @@ -26,8 +27,8 @@ ) ) -(declare-var x (BitVec 64)) -(declare-var y (BitVec 64)) +(declare-var x (_ BitVec 64)) +(declare-var y (_ BitVec 64)) (constraint (= (f #x0000000000000000 #x0000000000000001) #x0000000000000000)) (constraint (= (f #x0000000000000000 #x0000000000000000) #x0000000000000001)) diff --git a/test/regress/regress2/sygus/ex23.sy b/test/regress/regress2/sygus/ex23.sy index 29e8527dc..9e3d2ea75 100644 --- a/test/regress/regress2/sygus/ex23.sy +++ b/test/regress/regress2/sygus/ex23.sy @@ -1,17 +1,12 @@ ; EXPECT: unsat -; COMMAND-LINE: --sygus-out=status --sygus-repair-const --sygus-grammar-cons=any-const +; COMMAND-LINE: --lang=sygus2 --sygus-out=status --sygus-repair-const --sygus-grammar-cons=any-const (set-logic LIA) (synth-inv inv-f ((y Int) (z Int) (c Int))) -(declare-primed-var y Int) -(declare-primed-var z Int) -(declare-primed-var c Int) - (define-fun pre-f ((y Int) (z Int) (c Int)) Bool (and (and (= c 0) (>= y 0)) (and (>= 127 y) (= z (* 36 y))))) - (define-fun trans-f ((y Int) (z Int) (c Int) (y! Int) (z! Int) (c! Int)) Bool (and (and (and (< c 36) (= z! (+ z 1))) (= c! (+ c 1))) (= y! y))) diff --git a/test/regress/regress2/sygus/examples-deq.sy b/test/regress/regress2/sygus/examples-deq.sy index 3f1295df6..5b52e1da7 100644 --- a/test/regress/regress2/sygus/examples-deq.sy +++ b/test/regress/regress2/sygus/examples-deq.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --sygus-out=status +; COMMAND-LINE: --lang=sygus2 --sygus-out=status (set-logic LIA) (synth-fun f ((x Int) (y Int)) Int) diff --git a/test/regress/regress2/sygus/icfp_easy_mt_ite.sy b/test/regress/regress2/sygus/icfp_easy_mt_ite.sy index 799633fa3..d7cc161da 100644 --- a/test/regress/regress2/sygus/icfp_easy_mt_ite.sy +++ b/test/regress/regress2/sygus/icfp_easy_mt_ite.sy @@ -1,30 +1,31 @@ ; EXPECT: unsat -; COMMAND-LINE: --sygus-out=status +; COMMAND-LINE: --lang=sygus2 --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)) +(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) +(synth-fun f ((x (_ BitVec 64))) (_ BitVec 64) +((Start (_ BitVec 64)) (StartBool Bool)) ( - -(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) - (ite StartBool Start Start) - )) +(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) + (ite StartBool Start Start) +)) (StartBool Bool ((= Start #x0000000000000001))) ) ) + (constraint (= (f #x6E393354DFFAAB51) #xC8E366559002AA57)) (constraint (= (f #xE5D371D100002E8A) #x0000000000000000)) diff --git a/test/regress/regress2/sygus/inv_gen_n_c11.sy b/test/regress/regress2/sygus/inv_gen_n_c11.sy index 9e04682a5..aebc03dea 100644 --- a/test/regress/regress2/sygus/inv_gen_n_c11.sy +++ b/test/regress/regress2/sygus/inv_gen_n_c11.sy @@ -1,16 +1,17 @@ ; EXPECT: unsat -; COMMAND-LINE: --sygus-out=status +; COMMAND-LINE: --lang=sygus2 --sygus-out=status (set-logic LIA) (synth-fun inv ((i Int) (l Int)) Bool + ((Start Bool) (AtomicFormula Bool) (Sum Int) (Term Int) (Sign Int) (Var Int) (Const Int)) ( (Start Bool ((and AtomicFormula AtomicFormula) (or AtomicFormula AtomicFormula))) (AtomicFormula Bool ((<= Sum Const) (= Sum Const))) (Sum Int ((+ Term Term))) (Term Int ((* Sign Var))) - (Sign Int (0 1 -1)) + (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)) + (Const Int ((- 7) (- 6) (- 5) (- 4) (- 3) (- 2) (- 1) 0 1 2 3 4 5 6 7)) ) ) diff --git a/test/regress/regress2/sygus/lustre-real.sy b/test/regress/regress2/sygus/lustre-real.sy index 2ca010898..99d682bcc 100644 --- a/test/regress/regress2/sygus/lustre-real.sy +++ b/test/regress/regress2/sygus/lustre-real.sy @@ -1,66 +1,66 @@ ; EXPECT: unsat -; COMMAND-LINE: --cegqi-si=none --sygus-out=status -(set-logic LIRA) +; COMMAND-LINE: --lang=sygus2 --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 +(let ((X1 0)) (let ((X2 (ite (not (= X1 1)) 1 X1))) (let ((X3 (or (= X2 1) (and (>= X2 2) (<= X2 8))))) (and (= top.usr.OK@0 X3) (let ((X4 false)) (let ((X5 (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 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 top.usr.accelResume@0 1 0)) 20)) (= top.impl.usr.chart_CruiseController_ModeLogic_mode_logic_rlt_evtInitStep@0 true) (let ((X7 (ite (not top.usr.onOff@0) 0 1))) (let ((X8 (and (and (>= X1 2) (<= X1 8)) (not (ite (not (= X7 0)) true false))))) (let ((X9 (ite X8 (ite (and (>= X1 2) (<= X1 8)) 0 X1) X1))) (let ((X10 (ite X8 (ite (not (= X9 1)) 1 X9) X9))) (let ((X11 (and (= X10 1) (and (ite (not (= X7 0)) true false) (not X8))))) (let ((X12 (ite X11 (ite (= X10 1) 0 X10) X10))) (let ((X13 (ite (not (and (>= X12 2) (<= X12 8))) 2 X12))) (let ((X14 (and (not (and (>= X12 2) (<= X12 8))) (and (>= X13 2) (<= X13 8))))) (let ((X15 (ite X14 (ite (not (= X13 7)) 7 X13) X13))) (let ((X16 (ite X11 X15 X12))) (let ((X17 (or X11 X8))) (let ((X18 (ite (not X5) 0 1))) (let ((X19 (and (and (>= X16 3) (<= X16 6)) (not (ite (not (= X18 0)) true false))))) (let ((X20 +(ite X19 +(ite (and (>= X16 3) (<= X16 6)) 2 X16) X16))) (let ((X21 (ite X19 (ite (not (= X20 8)) 8 X20) X20))) (let ((X22 (ite (not X4) 0 1))) (let ((X23 (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 (ite X23 (ite (= X21 8) 2 X21) X21))) (let ((X25 +(ite (not (and (>= X24 3) (<= X24 6))) 3 X24))) (let ((X26 (and (not (and (>= X24 3) (<= X24 6))) (and (>= X25 3) (<= X25 6))))) (let ((X27 +(ite X26 +(ite (not (= X25 4)) 4 X25) X25))) (let ((X28 (ite X23 X27 X24))) (let ((X29 (or X23 X19))) (let ((X30 (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 +(ite X30 (ite (= X28 8) 2 X28) X28))) (let ((X32 +(ite (not (and (>= X31 3) (<= X31 6))) 3 X31))) (let ((X33 (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 X33 +(ite (not (= X32 4)) 4 X32) X32))) (let ((X35 (ite X30 X34 X31))) (let ((X36 (or X30 X29))) (let ((X37 (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 X37 (ite (= X35 7) 2 X35) X35))) (let ((X39 -Int (ite (not -(and (>= X38 3) (<= X38 6))) 3 X38))) (let ((X40 Bool (and (not +(ite (not +(and (>= X38 3) (<= X38 6))) 3 X38))) (let ((X40 (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 X40 +(ite (not (= X39 4)) 4 X39) X39))) (let ((X42 (ite X37 X41 X38))) (let ((X43 (or X37 X36))) (let ((X44 (and (= X42 4) (= X22 1)))) (let ((X45 +(ite X44 (ite (= X42 4) 3 X42) X42))) (let ((X46 -Int (ite X44 +(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 (not +(ite (= top.impl.usr.cruise_controller_CruiseController_ModeLogic_DelayOnsetAccel_Bounded_Count_Out@0 20) true false)) 0 1))) (let ((X48 (and (= X46 4) (and (= X47 1) (not X44))))) (let ((X49 +(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 X48 +(ite (not (= X49 5)) 5 X49) X49))) (let ((X51 (or X48 X44))) (let ((X52 +(ite (not +(ite (= top.impl.usr.cruise_controller_CruiseController_ModeLogic_DelayOnsetDecel_Bounded_Count_Out@0 20) true false)) 0 1))) (let ((X53 (and (= X50 4) (and (= X52 1) (not X51))))) (let ((X54 +(ite X53 (ite (= X50 4) 3 X50) X50))) (let ((X55 -Int (ite X53 +(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 +(= X54 6)) 6 X54) X54))) (let ((X56 (or X53 X51))) (let ((X57 (and (= X55 6) (and (= X52 0) (not X56))))) (let ((X58 +(ite X57 (ite (= X55 6) 3 X55) X55))) (let ((X59 -Int (ite X57 +(ite X57 (ite (not -(= X58 4)) 4 X58) X58))) (let ((X60 Bool -(or X57 X56))) (let ((X61 Bool +(= X58 4)) 4 X58) X58))) (let ((X60 +(or X57 X56))) (let ((X61 (and (= X59 5) (and (= X47 0) (not X60))))) (let ((X62 -Int (ite X61 +(ite X61 (ite (= X59 5) 3 X59) X59))) (let ((X63 -Int (ite X61 +(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 @@ -74,7 +74,7 @@ __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 +top.impl.usr.chart_CruiseController_ModeLogic_mode_logic_final_state_states___root@0)) (let ((X2 (ite (not (= X1 1)) 1 X1))) (let ((X3 (or (= X2 1) (and (>= X2 2) (<= X2 8))))) (and (= top.usr.OK@1 X3) (let ((X4 (and (not top.usr.decelSet@0) top.usr.decelSet@1))) (let ((X5 (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 (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 @@ -94,56 +94,56 @@ Int top.impl.usr.chart_CruiseController_ModeLogic_mode_logic_final_state_states_ (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 +false top.impl.usr.chart_CruiseController_ModeLogic_mode_logic_rlt_evtInitStep@0)) (let ((X7 (ite (not top.usr.onOff@1) 0 1))) (let ((X8 (and (and (>= X1 2) (<= X1 8)) (not (ite (not (= X7 0)) true false))))) (let ((X9 (ite X8 (ite (and (>= X1 2) (<= X1 8)) 0 X1) X1))) (let ((X10 (ite X8 (ite (not (= X9 1)) 1 X9) X9))) (let ((X11 (and (= X10 1) (and (ite (not (= X7 0)) true false) (not X8))))) (let ((X12 (ite X11 (ite (= X10 1) 0 X10) X10))) (let ((X13 (ite (not (and (>= X12 2) (<= X12 8))) 2 X12))) (let ((X14 (and (not (and (>= X12 2) (<= X12 8))) (and (>= X13 2) (<= X13 8))))) (let ((X15 (ite X14 (ite (not (= X13 7)) 7 X13) X13))) (let ((X16 (ite X11 X15 X12))) (let ((X17 (or X11 X8))) (let ((X18 (ite (not X5) 0 1))) (let ((X19 (and (and (>= X16 3) (<= X16 6)) (not (ite (not (= X18 0)) true false))))) (let ((X20 +(ite X19 +(ite (and (>= X16 3) (<= X16 6)) 2 X16) X16))) (let ((X21 (ite X19 (ite (not (= X20 8)) 8 X20) X20))) (let ((X22 (ite (not X4) 0 1))) (let ((X23 (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 (ite X23 (ite (= X21 8) 2 X21) X21))) (let ((X25 +(ite (not (and (>= X24 3) (<= X24 6))) 3 X24))) (let ((X26 (and (not (and (>= X24 3) (<= X24 6))) (and (>= X25 3) (<= X25 6))))) (let ((X27 +(ite X26 +(ite (not (= X25 4)) 4 X25) X25))) (let ((X28 (ite X23 X27 X24))) (let ((X29 (or X23 X19))) (let ((X30 (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 +(ite X30 (ite (= X28 8) 2 X28) X28))) (let ((X32 +(ite (not (and (>= X31 3) (<= X31 6))) 3 X31))) (let ((X33 (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 X33 +(ite (not (= X32 4)) 4 X32) X32))) (let ((X35 (ite X30 X34 X31))) (let ((X36 (or X30 X29))) (let ((X37 (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 X37 (ite (= X35 7) 2 X35) X35))) (let ((X39 -Int (ite (not -(and (>= X38 3) (<= X38 6))) 3 X38))) (let ((X40 Bool (and (not +(ite (not +(and (>= X38 3) (<= X38 6))) 3 X38))) (let ((X40 (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 X40 +(ite (not (= X39 4)) 4 X39) X39))) (let ((X42 (ite X37 X41 X38))) (let ((X43 (or X37 X36))) (let ((X44 (and (= X42 4) (= X22 1)))) (let ((X45 +(ite X44 (ite (= X42 4) 3 X42) X42))) (let ((X46 -Int (ite X44 +(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 (not +(ite (= top.impl.usr.cruise_controller_CruiseController_ModeLogic_DelayOnsetAccel_Bounded_Count_Out@1 20) true false)) 0 1))) (let ((X48 (and (= X46 4) (and (= X47 1) (not X44))))) (let ((X49 +(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 X48 +(ite (not (= X49 5)) 5 X49) X49))) (let ((X51 (or X48 X44))) (let ((X52 +(ite (not +(ite (= top.impl.usr.cruise_controller_CruiseController_ModeLogic_DelayOnsetDecel_Bounded_Count_Out@1 20) true false)) 0 1))) (let ((X53 (and (= X50 4) (and (= X52 1) (not X51))))) (let ((X54 +(ite X53 (ite (= X50 4) 3 X50) X50))) (let ((X55 -Int (ite X53 +(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 +(= X54 6)) 6 X54) X54))) (let ((X56 (or X53 X51))) (let ((X57 (and (= X55 6) (and (= X52 0) (not X56))))) (let ((X58 +(ite X57 (ite (= X55 6) 3 X55) X55))) (let ((X59 -Int (ite X57 +(ite X57 (ite (not -(= X58 4)) 4 X58) X58))) (let ((X60 Bool -(or X57 X56))) (let ((X61 Bool +(= X58 4)) 4 X58) X58))) (let ((X60 +(or X57 X56))) (let ((X61 (and (= X59 5) (and (= X47 0) (not X60))))) (let ((X62 -Int (ite X61 +(ite X61 (ite (= X59 5) 3 X59) X59))) (let ((X63 -Int (ite X61 +(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 @@ -157,67 +157,66 @@ Int (ite X61 (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 +(let ((X1 0)) (let ((X2 (ite (not (= X1 1)) 1 X1))) (let ((X3 (or (= X2 1) (and (>= X2 2) (<= X2 8))))) (and (= top.usr.OK X3) (let ((X4 false)) (let ((X5 (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 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 top.usr.accelResume 1 0)) 20)) (= top.impl.usr.chart_CruiseController_ModeLogic_mode_logic_rlt_evtInitStep true) (let ((X7 (ite (not top.usr.onOff) 0 1))) (let ((X8 (and (and (>= X1 2) (<= X1 8)) (not (ite (not (= X7 0)) true false))))) (let ((X9 (ite X8 (ite (and (>= X1 2) (<= X1 8)) 0 X1) X1))) (let ((X10 (ite X8 (ite (not (= X9 1)) 1 X9) X9))) (let ((X11 (and (= X10 1) (and (ite (not (= X7 0)) true false) (not X8))))) (let ((X12 (ite X11 (ite (= X10 1) 0 X10) X10))) (let ((X13 (ite (not (and (>= X12 2) (<= X12 8))) 2 X12))) (let ((X14 (and (not (and (>= X12 2) (<= X12 8))) (and (>= X13 2) (<= X13 8))))) (let ((X15 (ite X14 (ite (not (= X13 7)) 7 X13) X13))) (let ((X16 (ite X11 X15 X12))) (let ((X17 (or X11 X8))) (let ((X18 (ite (not X5) 0 1))) (let ((X19 (and (and (>= X16 3) (<= X16 6)) (not (ite (not (= X18 0)) true false))))) (let ((X20 +(ite X19 +(ite (and (>= X16 3) (<= X16 6)) 2 X16) X16))) (let ((X21 (ite X19 (ite (not (= X20 8)) 8 X20) X20))) (let ((X22 (ite (not X4) 0 1))) (let ((X23 (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 (ite X23 (ite (= X21 8) 2 X21) X21))) (let ((X25 +(ite (not (and (>= X24 3) (<= X24 6))) 3 X24))) (let ((X26 (and (not (and (>= X24 3) (<= X24 6))) (and (>= X25 3) (<= X25 6))))) (let ((X27 +(ite X26 +(ite (not (= X25 4)) 4 X25) X25))) (let ((X28 (ite X23 X27 X24))) (let ((X29 (or X23 X19))) (let ((X30 (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 +(ite X30 (ite (= X28 8) 2 X28) X28))) (let ((X32 +(ite (not (and (>= X31 3) (<= X31 6))) 3 X31))) (let ((X33 (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 X33 +(ite (not (= X32 4)) 4 X32) X32))) (let ((X35 (ite X30 X34 X31))) (let ((X36 (or X30 X29))) (let ((X37 (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 X37 (ite (= X35 7) 2 X35) X35))) (let ((X39 -Int (ite (not -(and (>= X38 3) (<= X38 6))) 3 X38))) (let ((X40 Bool (and (not +(ite (not +(and (>= X38 3) (<= X38 6))) 3 X38))) (let ((X40 (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 X40 +(ite (not (= X39 4)) 4 X39) X39))) (let ((X42 (ite X37 X41 X38))) (let ((X43 (or X37 X36))) (let ((X44 (and (= X42 4) (= X22 1)))) (let ((X45 +(ite X44 (ite (= X42 4) 3 X42) X42))) (let ((X46 -Int (ite X44 +(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 (not +(ite (= top.impl.usr.cruise_controller_CruiseController_ModeLogic_DelayOnsetAccel_Bounded_Count_Out 20) true false)) 0 1))) (let ((X48 (and (= X46 4) (and (= X47 1) (not X44))))) (let ((X49 +(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 X48 +(ite (not (= X49 5)) 5 X49) X49))) (let ((X51 (or X48 X44))) (let ((X52 +(ite (not +(ite (= top.impl.usr.cruise_controller_CruiseController_ModeLogic_DelayOnsetDecel_Bounded_Count_Out 20) true false)) 0 1))) (let ((X53 (and (= X50 4) (and (= X52 1) (not X51))))) (let ((X54 +(ite X53 (ite (= X50 4) 3 X50) X50))) (let ((X55 -Int (ite X53 +(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 +(= X54 6)) 6 X54) X54))) (let ((X56 (or X53 X51))) (let ((X57 (and (= X55 6) (and (= X52 0) (not X56))))) (let ((X58 +(ite X57 (ite (= X55 6) 3 X55) X55))) (let ((X59 -Int (ite X57 +(ite X57 (ite (not -(= X58 4)) 4 X58) X58))) (let ((X60 Bool -(or X57 X56))) (let ((X61 Bool +(= X58 4)) 4 X58) X58))) (let ((X60 +(or X57 X56))) (let ((X61 (and (= X59 5) (and (= X47 0) (not X60))))) (let ((X62 -Int (ite X61 +(ite X61 (ite (= X59 5) 3 X59) X59))) (let ((X63 -Int (ite X61 +(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___ @@ -235,7 +234,7 @@ Int (ite X61 ) 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! +top.impl.usr.chart_CruiseController_ModeLogic_mode_logic_final_state_states___root)) (let ((X2 (ite (not (= X1 1)) 1 X1))) (let ((X3 (or (= X2 1) (and (>= X2 2) (<= X2 8))))) (and (= top.usr.OK! X3) (let ((X4 (and (not top.usr.decelSet) top.usr.decelSet!))) (let ((X5 (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 (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 @@ -255,56 +254,56 @@ Int top.impl.usr.chart_CruiseController_ModeLogic_mode_logic_final_state_states_ (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 +false top.impl.usr.chart_CruiseController_ModeLogic_mode_logic_rlt_evtInitStep)) (let ((X7 (ite (not top.usr.onOff!) 0 1))) (let ((X8 (and (and (>= X1 2) (<= X1 8)) (not (ite (not (= X7 0)) true false))))) (let ((X9 (ite X8 (ite (and (>= X1 2) (<= X1 8)) 0 X1) X1))) (let ((X10 (ite X8 (ite (not (= X9 1)) 1 X9) X9))) (let ((X11 (and (= X10 1) (and (ite (not (= X7 0)) true false) (not X8))))) (let ((X12 (ite X11 (ite (= X10 1) 0 X10) X10))) (let ((X13 (ite (not (and (>= X12 2) (<= X12 8))) 2 X12))) (let ((X14 (and (not (and (>= X12 2) (<= X12 8))) (and (>= X13 2) (<= X13 8))))) (let ((X15 (ite X14 (ite (not (= X13 7)) 7 X13) X13))) (let ((X16 (ite X11 X15 X12))) (let ((X17 (or X11 X8))) (let ((X18 (ite (not X5) 0 1))) (let ((X19 (and (and (>= X16 3) (<= X16 6)) (not (ite (not (= X18 0)) true false))))) (let ((X20 +(ite X19 +(ite (and (>= X16 3) (<= X16 6)) 2 X16) X16))) (let ((X21 (ite X19 (ite (not (= X20 8)) 8 X20) X20))) (let ((X22 (ite (not X4) 0 1))) (let ((X23 (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 (ite X23 (ite (= X21 8) 2 X21) X21))) (let ((X25 +(ite (not (and (>= X24 3) (<= X24 6))) 3 X24))) (let ((X26 (and (not (and (>= X24 3) (<= X24 6))) (and (>= X25 3) (<= X25 6))))) (let ((X27 +(ite X26 +(ite (not (= X25 4)) 4 X25) X25))) (let ((X28 (ite X23 X27 X24))) (let ((X29 (or X23 X19))) (let ((X30 (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 +(ite X30 (ite (= X28 8) 2 X28) X28))) (let ((X32 +(ite (not (and (>= X31 3) (<= X31 6))) 3 X31))) (let ((X33 (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 X33 +(ite (not (= X32 4)) 4 X32) X32))) (let ((X35 (ite X30 X34 X31))) (let ((X36 (or X30 X29))) (let ((X37 (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 X37 (ite (= X35 7) 2 X35) X35))) (let ((X39 -Int (ite (not -(and (>= X38 3) (<= X38 6))) 3 X38))) (let ((X40 Bool (and (not +(ite (not +(and (>= X38 3) (<= X38 6))) 3 X38))) (let ((X40 (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 X40 +(ite (not (= X39 4)) 4 X39) X39))) (let ((X42 (ite X37 X41 X38))) (let ((X43 (or X37 X36))) (let ((X44 (and (= X42 4) (= X22 1)))) (let ((X45 +(ite X44 (ite (= X42 4) 3 X42) X42))) (let ((X46 -Int (ite X44 +(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 (not +(ite (= top.impl.usr.cruise_controller_CruiseController_ModeLogic_DelayOnsetAccel_Bounded_Count_Out! 20) true false)) 0 1))) (let ((X48 (and (= X46 4) (and (= X47 1) (not X44))))) (let ((X49 +(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 X48 +(ite (not (= X49 5)) 5 X49) X49))) (let ((X51 (or X48 X44))) (let ((X52 +(ite (not +(ite (= top.impl.usr.cruise_controller_CruiseController_ModeLogic_DelayOnsetDecel_Bounded_Count_Out! 20) true false)) 0 1))) (let ((X53 (and (= X50 4) (and (= X52 1) (not X51))))) (let ((X54 +(ite X53 (ite (= X50 4) 3 X50) X50))) (let ((X55 -Int (ite X53 +(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 +(= X54 6)) 6 X54) X54))) (let ((X56 (or X53 X51))) (let ((X57 (and (= X55 6) (and (= X52 0) (not X56))))) (let ((X58 +(ite X57 (ite (= X55 6) 3 X55) X55))) (let ((X59 -Int (ite X57 +(ite X57 (ite (not -(= X58 4)) 4 X58) X58))) (let ((X60 Bool -(or X57 X56))) (let ((X61 Bool +(= X58 4)) 4 X58) X58))) (let ((X60 +(or X57 X56))) (let ((X61 (and (= X59 5) (and (= X47 0) (not X60))))) (let ((X62 -Int (ite X61 +(ite X61 (ite (= X59 5) 3 X59) X59))) (let ((X63 -Int (ite X61 +(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___! diff --git a/test/regress/regress2/sygus/max2-univ.sy b/test/regress/regress2/sygus/max2-univ.sy index 0e00cfd9b..d8222ded2 100644 --- a/test/regress/regress2/sygus/max2-univ.sy +++ b/test/regress/regress2/sygus/max2-univ.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --sygus-out=status +; COMMAND-LINE: --lang=sygus2 --sygus-out=status ; Synthesize the maximum of 2 integers, but property has 4 variables (requires 2 passes) (set-logic LIA) (synth-fun max2 ((x Int) (y Int)) Int) @@ -9,4 +9,3 @@ (declare-var w Int) (constraint (=> (< r 0) (=> (or (and (= x w) (= y (+ w r))) (and (= x (+ w r)) (= y w))) (= (max2 x y) w)))) (check-synth) - diff --git a/test/regress/regress2/sygus/min_IC_1.sy b/test/regress/regress2/sygus/min_IC_1.sy index a36a00019..c0cae0025 100644 --- a/test/regress/regress2/sygus/min_IC_1.sy +++ b/test/regress/regress2/sygus/min_IC_1.sy @@ -1,11 +1,12 @@ ; REQUIRES: symfpu ; EXPECT: unsat -; COMMAND-LINE: --sygus-out=status --fp-exp +; COMMAND-LINE: --lang=sygus2 --sygus-out=status --fp-exp (set-logic ALL) (define-sort FP () (_ FloatingPoint 3 5)) (define-fun IC ((t FP)) Bool (=> (fp.isInfinite t) (fp.isNegative t))) (synth-fun simpIC ((t FP)) Bool + ((Start Bool) (StartFP FP)) ((Start Bool ( (and Start Start) (not Start) diff --git a/test/regress/regress2/sygus/mpg_guard1-dd.sy b/test/regress/regress2/sygus/mpg_guard1-dd.sy index 31800a36f..98f13bb92 100644 --- a/test/regress/regress2/sygus/mpg_guard1-dd.sy +++ b/test/regress/regress2/sygus/mpg_guard1-dd.sy @@ -1,8 +1,9 @@ ; EXPECT: unsat -; COMMAND-LINE: --sygus-out=status +; COMMAND-LINE: --lang=sygus2 --sygus-out=status (set-logic LIA) -(synth-fun eq1 ( (x Int) (y Int) ) Int +(synth-fun eq1 ((x Int) (y Int)) Int + ((Start Int) (StartBool Bool)) ((Start Int (x y 0 @@ -13,15 +14,14 @@ (<= Start Start) (= Start Start))))) -(define-fun iteB (( b1 Bool ) (b2 Bool ) (b3 Bool )) Bool (or (and b1 b2) (and (not b1) b3))) +(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) +(declare-var x Int) +(declare-var y Int) -(constraint (iteB (>= x 0) +(constraint (iteB (>= x 0) (= (eq1 x y) (+ x x)) - (= (eq1 x y) x) + (= (eq1 x y) x) )) (check-synth) - diff --git a/test/regress/regress2/sygus/multi-udiv.sy b/test/regress/regress2/sygus/multi-udiv.sy index 657417595..d9deb28a3 100644 --- a/test/regress/regress2/sygus/multi-udiv.sy +++ b/test/regress/regress2/sygus/multi-udiv.sy @@ -1,9 +1,13 @@ ; EXPECT: unsat -; COMMAND-LINE: --sygus-out=status - ( set-logic BV ) - ( define-fun hd05 ( ( x ( BitVec 32 ) ) ) ( BitVec 32 ) ( bvor x ( bvsub x #x00000001 ) ) ) -( synth-fun f ( ( x ( BitVec 32 ) ) ) ( BitVec 32 ) ( - (Start ( BitVec 32 ) ( #x00000001 +; COMMAND-LINE: --lang=sygus2 --sygus-out=status +(set-logic BV) + +(define-fun hd05 ((x (_ BitVec 32))) (_ BitVec 32) (bvor x (bvsub x #x00000001))) + +(synth-fun f ((x (_ BitVec 32))) (_ BitVec 32) + ((Start (_ BitVec 32)) (NT0 (_ BitVec 32)) (NT4 (_ BitVec 32))) ( + (Start (_ BitVec 32) ( + #x00000001 #x00000000 #xffffffff x @@ -22,12 +26,14 @@ (bvor NT4 NT0) (bvadd NT4 NT0) )) - (NT0 ( BitVec 32 ) ( #x00000001 + (NT0 (_ BitVec 32) ( + #x00000001 #x00000000 #xffffffff x )) - (NT4 ( BitVec 32 ) ( (bvnot NT0) + (NT4 (_ BitVec 32) ( + (bvnot NT0) (bvneg NT0) (bvadd NT0 NT0) (bvor NT0 NT0) @@ -37,6 +43,6 @@ (bvurem NT0 NT0) )) )) - ( declare-var x ( BitVec 32 ) ) - ( constraint ( = ( hd05 x ) ( f x ) ) ) - ( check-synth ) +(declare-var x (_ BitVec 32)) +(constraint (= (hd05 x) (f x))) +(check-synth) diff --git a/test/regress/regress2/sygus/nia-max-square.sy b/test/regress/regress2/sygus/nia-max-square.sy index e023e837b..0657494b1 100644 --- a/test/regress/regress2/sygus/nia-max-square.sy +++ b/test/regress/regress2/sygus/nia-max-square.sy @@ -1,8 +1,9 @@ ; EXPECT: unsat -; COMMAND-LINE: --sygus-out=status --nl-ext-tplanes +; COMMAND-LINE: --lang=sygus2 --sygus-out=status --nl-ext-tplanes (set-logic NIA) (synth-fun max ((x Int) (y Int)) Int + ((Start Int) (StartBool Bool)) ((Start Int (0 1 x y (+ Start Start) (- Start Start) diff --git a/test/regress/regress2/sygus/no-syntax-test-no-si.sy b/test/regress/regress2/sygus/no-syntax-test-no-si.sy index 8f333811c..1906e3ef1 100644 --- a/test/regress/regress2/sygus/no-syntax-test-no-si.sy +++ b/test/regress/regress2/sygus/no-syntax-test-no-si.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --sygus-out=status +; COMMAND-LINE: --lang=sygus2 --sygus-out=status (set-logic LIA) @@ -11,4 +11,3 @@ (constraint (= (f x y) (+ (f x x) (f y y) x 1))) (check-synth) - diff --git a/test/regress/regress2/sygus/pbe_bvurem.sy b/test/regress/regress2/sygus/pbe_bvurem.sy index fc715a645..07f029577 100644 --- a/test/regress/regress2/sygus/pbe_bvurem.sy +++ b/test/regress/regress2/sygus/pbe_bvurem.sy @@ -1,8 +1,9 @@ ; EXPECT: unsat -; COMMAND-LINE: --sygus-out=status +; COMMAND-LINE: --lang=sygus2 --sygus-out=status (set-logic BV) (define-sort BV () (_ BitVec 8)) (synth-fun IC ((s BV) (t BV)) Bool + ((Start Bool) (StartBv BV)) ((Start Bool ( true false @@ -15,18 +16,18 @@ #x00 #x01 #x7E - (bvnot StartBv) - (bvmul StartBv StartBv) - (bvudiv StartBv StartBv) - (bvurem StartBv StartBv) - (bvand StartBv StartBv) + (bvnot StartBv) + (bvmul StartBv StartBv) + (bvudiv StartBv StartBv) + (bvurem StartBv StartBv) + (bvand StartBv StartBv) )) )) -(constraint (not (IC (_ bv32 8) (_ bv187 8) ))) -(constraint (not (IC (_ bv102 8) (_ bv15 8) ))) -(constraint (not (IC (_ bv92 8) (_ bv85 8) ))) -(constraint (IC (_ bv39 8) (_ bv214 8) )) -(constraint (IC (_ bv155 8) (_ bv82 8) )) -(constraint (IC (_ bv53 8) (_ bv98 8) )) -(constraint (IC (_ bv41 8) (_ bv47 8) )) +(constraint (not (IC (_ bv32 8) (_ bv187 8)))) +(constraint (not (IC (_ bv102 8) (_ bv15 8)))) +(constraint (not (IC (_ bv92 8) (_ bv85 8)))) +(constraint (IC (_ bv39 8) (_ bv214 8))) +(constraint (IC (_ bv155 8) (_ bv82 8))) +(constraint (IC (_ bv53 8) (_ bv98 8))) +(constraint (IC (_ bv41 8) (_ bv47 8))) (check-synth) diff --git a/test/regress/regress2/sygus/process-10-vars-2fun.sy b/test/regress/regress2/sygus/process-10-vars-2fun.sy index 214da82c8..fe6f5cd0c 100644 --- a/test/regress/regress2/sygus/process-10-vars-2fun.sy +++ b/test/regress/regress2/sygus/process-10-vars-2fun.sy @@ -1,4 +1,4 @@ -; COMMAND-LINE: --cegqi-si=none --sygus-out=status --no-sygus-repair-const --sygus-arg-relevant +; COMMAND-LINE: --lang=sygus2 --cegqi-si=none --sygus-out=status --no-sygus-repair-const --sygus-arg-relevant ; EXPECT: unsat (set-logic LIA) @@ -25,4 +25,3 @@ (constraint (>= (g x1 x2 x3 x4 x5 x6 x7 x8 x9 x10) (+ x4 x4 x4))) (check-synth) - diff --git a/test/regress/regress2/sygus/process-arg-invariance.sy b/test/regress/regress2/sygus/process-arg-invariance.sy index 2f1b74ddf..a50cec2d8 100644 --- a/test/regress/regress2/sygus/process-arg-invariance.sy +++ b/test/regress/regress2/sygus/process-arg-invariance.sy @@ -1,10 +1,9 @@ -; COMMAND-LINE: --cegqi-si=none --sygus-out=status --no-sygus-add-const-grammar --sygus-arg-relevant +; COMMAND-LINE: --lang=sygus2 --cegqi-si=none --sygus-out=status --no-sygus-add-const-grammar --sygus-arg-relevant ; 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) @@ -15,4 +14,3 @@ (constraint (<= (f x x x x x x x x x 0) (+ x x x))) (check-synth) - diff --git a/test/regress/regress2/sygus/real-grammar-neg.sy b/test/regress/regress2/sygus/real-grammar-neg.sy index 523c95ec2..0891e57bf 100644 --- a/test/regress/regress2/sygus/real-grammar-neg.sy +++ b/test/regress/regress2/sygus/real-grammar-neg.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --sygus-out=status --cegqi-si=none --no-sygus-pbe +; COMMAND-LINE: --lang=sygus2 --sygus-out=status --cegqi-si=none --no-sygus-pbe (set-logic LRA) @@ -7,7 +7,7 @@ (declare-var x Real) -(constraint (and (= (f -4) -2) (= (f -9) (/ -9 2)))) +(constraint (and (= (f (- 4)) (- 2)) (= (f (- 9)) (/ (- 9) 2)))) (check-synth) diff --git a/test/regress/regress2/sygus/sets-fun-test.sy b/test/regress/regress2/sygus/sets-fun-test.sy index 987d6a792..fdcaaefa9 100644 --- a/test/regress/regress2/sygus/sets-fun-test.sy +++ b/test/regress/regress2/sygus/sets-fun-test.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --sygus-out=status +; COMMAND-LINE: --lang=sygus2 --sygus-out=status (set-logic ALL) (synth-fun f ((x Int)) (Set Int)) diff --git a/test/regress/regress2/sygus/strings-no-syntax-len.sy b/test/regress/regress2/sygus/strings-no-syntax-len.sy index 22048f1ec..e0b039c16 100644 --- a/test/regress/regress2/sygus/strings-no-syntax-len.sy +++ b/test/regress/regress2/sygus/strings-no-syntax-len.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --sygus-out=status +; COMMAND-LINE: --lang=sygus2 --sygus-out=status (set-logic ALL) (synth-fun f ((x String)) Int) diff --git a/test/regress/regress2/sygus/three.sy b/test/regress/regress2/sygus/three.sy index 831e5beb1..44974caf1 100644 --- a/test/regress/regress2/sygus/three.sy +++ b/test/regress/regress2/sygus/three.sy @@ -1,9 +1,10 @@ ; EXPECT: unsat -; COMMAND-LINE: --sygus-out=status +; COMMAND-LINE: --lang=sygus2 --sygus-out=status (set-logic LIA) (synth-fun f ((x Int)) Int + ((Start Int)) ((Start Int ( x 3 @@ -27,4 +28,3 @@ (constraint (= (f 0) 0)) (check-synth) - diff --git a/test/regress/regress2/sygus/vcb.sy b/test/regress/regress2/sygus/vcb.sy index e6f43fc21..a0122193d 100644 --- a/test/regress/regress2/sygus/vcb.sy +++ b/test/regress/regress2/sygus/vcb.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --sygus-out=status --no-sygus-repair-const --decision=justification +; COMMAND-LINE: --lang=sygus2 --sygus-out=status --no-sygus-repair-const --decision=justification (set-logic LIA) (synth-fun f1 ((x1 Int) (x2 Int)) Int) @@ -10,26 +10,26 @@ (define-fun vmax () Int 2) (define-fun AllZero ((v1 Int) (v2 Int)) Bool - (and (= v1 0) (= v2 0))) + (and (= v1 0) (= v2 0))) (define-fun InV ((v1 Int) (v2 Int)) Bool - (and (and (and (>= v1 vmin) (<= v1 vmax)) (>= v2 vmin)) (<= v2 vmax))) + (and (and (and (>= v1 vmin) (<= v1 vmax)) (>= v2 vmin)) (<= v2 vmax))) (define-fun InVorZero ((v1 Int) (v2 Int)) Bool - (or (InV v1 v2) (AllZero v1 v2))) + (or (InV v1 v2) (AllZero v1 v2))) (define-fun UnsafeSame ((x1 Int) (x2 Int) (v1 Int) (v2 Int)) Bool - (or (and (>= x1 x2) (>= (+ x2 v2) (+ x1 v1))) - (and (>= x2 x1) (>= (+ x1 v1) (+ x2 v2))))) + (or (and (>= x1 x2) (>= (+ x2 v2) (+ x1 v1))) + (and (>= x2 x1) (>= (+ x1 v1) (+ x2 v2))))) (define-fun BadSame ((x1 Int) (x2 Int)) Bool - (= x1 x2)) + (= x1 x2)) (define-fun Bad ((x1 Int) (x2 Int)) Bool - (BadSame x1 x2)) + (BadSame x1 x2)) (define-fun Unsafe ((x1 Int) (x2 Int) (v1 Int) (v2 Int)) Bool - (UnsafeSame x1 x2 v1 v2)) + (UnsafeSame x1 x2 v1 v2)) (declare-var x1 Int) @@ -46,8 +46,8 @@ (f2 (+ x1 (f1 x1 x2)) (+ x2 (f2 x1 x2)))))))) (constraint (or (or (or (not (InV v1 v2)) - (Unsafe x1 x2 v1 v2)) - (AllZero (f1 (+ x1 v1) (+ x2 v2)) (f2 (+ x1 v1) (+ x2 v2)))) + (Unsafe x1 x2 v1 v2)) + (AllZero (f1 (+ x1 v1) (+ x2 v2)) (f2 (+ x1 v1) (+ x2 v2)))) (not (AllZero (f1 x1 x2) (f2 x1 x2))))) |