diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-02-15 15:31:48 -0600 |
---|---|---|
committer | Aina Niemetz <aina.niemetz@gmail.com> | 2018-02-15 13:31:48 -0800 |
commit | 55037e0bcef45c795f28ff3fcf6c1055af465c70 (patch) | |
tree | 397d89bd10e541e1206c5dafdb8cf731feb34730 /test/regress/regress2/sygus | |
parent | 52a39aca19b7238d08c3cebcfa46436a73194008 (diff) |
Refactor regressions (#1581)
Diffstat (limited to 'test/regress/regress2/sygus')
-rw-r--r-- | test/regress/regress2/sygus/MPwL_d1s3.sy | 151 | ||||
-rw-r--r-- | test/regress/regress2/sygus/Makefile.am | 42 | ||||
-rw-r--r-- | test/regress/regress2/sygus/array_sum_dd.sy | 11 | ||||
-rw-r--r-- | test/regress/regress2/sygus/icfp_easy_mt_ite.sy | 32 | ||||
-rw-r--r-- | test/regress/regress2/sygus/inv_gen_n_c11.sy | 36 | ||||
-rw-r--r-- | test/regress/regress2/sygus/lustre-real.sy | 322 | ||||
-rw-r--r-- | test/regress/regress2/sygus/max2-univ.sy | 12 | ||||
-rw-r--r-- | test/regress/regress2/sygus/mpg_guard1-dd.sy | 27 | ||||
-rw-r--r-- | test/regress/regress2/sygus/nia-max-square.sy | 21 | ||||
-rw-r--r-- | test/regress/regress2/sygus/no-syntax-test-no-si.sy | 14 | ||||
-rw-r--r-- | test/regress/regress2/sygus/process-10-vars-2fun.sy | 28 | ||||
-rw-r--r-- | test/regress/regress2/sygus/process-arg-invariance.sy | 18 | ||||
-rw-r--r-- | test/regress/regress2/sygus/real-grammar-neg.sy | 14 | ||||
-rw-r--r-- | test/regress/regress2/sygus/three.sy | 30 |
14 files changed, 758 insertions, 0 deletions
diff --git a/test/regress/regress2/sygus/MPwL_d1s3.sy b/test/regress/regress2/sygus/MPwL_d1s3.sy new file mode 100644 index 000000000..5178cf86b --- /dev/null +++ b/test/regress/regress2/sygus/MPwL_d1s3.sy @@ -0,0 +1,151 @@ +; 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/regress2/sygus/Makefile.am b/test/regress/regress2/sygus/Makefile.am new file mode 100644 index 000000000..02091c3bd --- /dev/null +++ b/test/regress/regress2/sygus/Makefile.am @@ -0,0 +1,42 @@ +# don't override a BINARY imported from a personal.mk +@mk_if@eq ($(BINARY),) +@mk_empty@BINARY = cvc4 +end@mk_if@ + +LOG_COMPILER = @srcdir@/../../run_regression +AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @abs_top_builddir@/src/main/$(BINARY)$(EXEEXT) + +if AUTOMAKE_1_11 +# old-style (pre-automake 1.12) test harness +TESTS_ENVIRONMENT = \ + $(LOG_COMPILER) \ + $(AM_LOG_FLAGS) $(LOG_FLAGS) +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 = \ + array_sum_dd.sy \ + icfp_easy_mt_ite.sy \ + inv_gen_n_c11.sy \ + MPwL_d1s3.sy \ + nia-max-square.sy \ + no-syntax-test-no-si.sy \ + process-10-vars-2fun.sy \ + process-arg-invariance.sy \ + real-grammar-neg.sy \ + lustre-real.sy \ + max2-univ.sy \ + mpg_guard1-dd.sy \ + three.sy + +EXTRA_DIST = $(TESTS) + +# synonyms for "check" in this directory +.PHONY: regress regress2 test +regress regress2 test: check + +# do nothing in this subdir +.PHONY: regress0 regress1 regress3 regress4 +regress0 regress1 regress3 regress4: diff --git a/test/regress/regress2/sygus/array_sum_dd.sy b/test/regress/regress2/sygus/array_sum_dd.sy new file mode 100644 index 000000000..6d3354d2d --- /dev/null +++ b/test/regress/regress2/sygus/array_sum_dd.sy @@ -0,0 +1,11 @@ +; 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/regress2/sygus/icfp_easy_mt_ite.sy b/test/regress/regress2/sygus/icfp_easy_mt_ite.sy new file mode 100644 index 000000000..799633fa3 --- /dev/null +++ b/test/regress/regress2/sygus/icfp_easy_mt_ite.sy @@ -0,0 +1,32 @@ +; 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) + (ite StartBool Start Start) + )) +(StartBool Bool ((= Start #x0000000000000001))) +) +) +(constraint (= (f #x6E393354DFFAAB51) #xC8E366559002AA57)) + +(constraint (= (f #xE5D371D100002E8A) #x0000000000000000)) + +(check-synth) diff --git a/test/regress/regress2/sygus/inv_gen_n_c11.sy b/test/regress/regress2/sygus/inv_gen_n_c11.sy new file mode 100644 index 000000000..9e04682a5 --- /dev/null +++ b/test/regress/regress2/sygus/inv_gen_n_c11.sy @@ -0,0 +1,36 @@ +; EXPECT: unsat +; COMMAND-LINE: --sygus-out=status +(set-logic LIA) +(synth-fun inv ((i Int) (l Int)) Bool + ( + (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)) + (Var Int (i l)) + (Const Int (-7 -6 -5 -4 -3 -2 -1 0 1 2 3 4 5 6 7)) + ) +) + +(define-fun implies ((b1 Bool) (b2 Bool)) Bool (or (not b1) b2)) +(define-fun and3 ((b1 Bool) (b2 Bool) (b3 Bool)) Bool (and (and b1 b2) b3)) +(define-fun and4 ((b1 Bool) (b2 Bool) (b3 Bool) (b4 Bool)) Bool (and (and3 b1 b2 b3) b4)) +(define-fun and5 ((b1 Bool) (b2 Bool) (b3 Bool) (b4 Bool) (b5 Bool)) Bool (and (and4 b1 b2 b3 b4) b5)) +(define-fun and6 ((b1 Bool) (b2 Bool) (b3 Bool) (b4 Bool) (b5 Bool) (b6 Bool)) Bool (and (and5 b1 b2 b3 b4 b5) b6)) +(define-fun or3 ((b1 Bool) (b2 Bool) (b3 Bool)) Bool (or (or b1 b2) b3)) +(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) + +(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)) + +(check-synth) diff --git a/test/regress/regress2/sygus/lustre-real.sy b/test/regress/regress2/sygus/lustre-real.sy new file mode 100644 index 000000000..2ca010898 --- /dev/null +++ b/test/regress/regress2/sygus/lustre-real.sy @@ -0,0 +1,322 @@ +; 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/regress2/sygus/max2-univ.sy b/test/regress/regress2/sygus/max2-univ.sy new file mode 100644 index 000000000..0e00cfd9b --- /dev/null +++ b/test/regress/regress2/sygus/max2-univ.sy @@ -0,0 +1,12 @@ +; EXPECT: unsat +; COMMAND-LINE: --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) +(declare-var x Int) +(declare-var y Int) +(declare-var r Int) +(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/mpg_guard1-dd.sy b/test/regress/regress2/sygus/mpg_guard1-dd.sy new file mode 100644 index 000000000..31800a36f --- /dev/null +++ b/test/regress/regress2/sygus/mpg_guard1-dd.sy @@ -0,0 +1,27 @@ +; 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/regress2/sygus/nia-max-square.sy b/test/regress/regress2/sygus/nia-max-square.sy new file mode 100644 index 000000000..e023e837b --- /dev/null +++ b/test/regress/regress2/sygus/nia-max-square.sy @@ -0,0 +1,21 @@ +; 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/regress2/sygus/no-syntax-test-no-si.sy b/test/regress/regress2/sygus/no-syntax-test-no-si.sy new file mode 100644 index 000000000..8f333811c --- /dev/null +++ b/test/regress/regress2/sygus/no-syntax-test-no-si.sy @@ -0,0 +1,14 @@ +; EXPECT: unsat +; COMMAND-LINE: --sygus-out=status + +(set-logic LIA) + +(synth-fun f ((x Int) (y Int)) Int) + +(declare-var x Int) +(declare-var y Int) + +(constraint (= (f x y) (+ (f x x) (f y y) x 1))) + +(check-synth) + diff --git a/test/regress/regress2/sygus/process-10-vars-2fun.sy b/test/regress/regress2/sygus/process-10-vars-2fun.sy new file mode 100644 index 000000000..00340030f --- /dev/null +++ b/test/regress/regress2/sygus/process-10-vars-2fun.sy @@ -0,0 +1,28 @@ +; 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) + +(synth-fun g ((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 +; and arguments 1...3, 5...10 are irrelevant for g + +(constraint (>= (f x1 x2 x3 x4 x5 x6 x7 x8 x9 x10) (+ x7 x7 x7))) + +(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 new file mode 100644 index 000000000..3c18b6c75 --- /dev/null +++ b/test/regress/regress2/sygus/process-arg-invariance.sy @@ -0,0 +1,18 @@ +; 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/regress2/sygus/real-grammar-neg.sy b/test/regress/regress2/sygus/real-grammar-neg.sy new file mode 100644 index 000000000..523c95ec2 --- /dev/null +++ b/test/regress/regress2/sygus/real-grammar-neg.sy @@ -0,0 +1,14 @@ +; EXPECT: unsat +; COMMAND-LINE: --sygus-out=status --cegqi-si=none --no-sygus-pbe + +(set-logic LRA) + +(synth-fun f ((x Real)) Real) + +(declare-var x Real) + +(constraint (and (= (f -4) -2) (= (f -9) (/ -9 2)))) + +(check-synth) + +; a solution is f = (/ x (+ 1 1)) diff --git a/test/regress/regress2/sygus/three.sy b/test/regress/regress2/sygus/three.sy new file mode 100644 index 000000000..831e5beb1 --- /dev/null +++ b/test/regress/regress2/sygus/three.sy @@ -0,0 +1,30 @@ +; 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) + |