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 | |
| parent | a507aa5f1904055782e1ba01083faf1fd0fb86f7 (diff) | |
Convert V1 Sygus files to V2. (#4136)
Diffstat (limited to 'test')
150 files changed, 1207 insertions, 1267 deletions
diff --git a/test/regress/regress0/expect/scrub.08.sy b/test/regress/regress0/expect/scrub.08.sy index aec265f2b..02879cb8d 100644 --- a/test/regress/regress0/expect/scrub.08.sy +++ b/test/regress/regress0/expect/scrub.08.sy @@ -1,4 +1,4 @@ -; COMMAND-LINE: --cegqi-si=all --sygus-out=status --no-sygus-repair-const +; COMMAND-LINE: --lang=sygus2 --cegqi-si=all --sygus-out=status --no-sygus-repair-const ; SCRUBBER: sed -e 's/The fact in question: .*$/The fact in question: TERM/' ; EXPECT: (error "A non-linear fact was asserted to arithmetic in a linear logic. ; EXPECT: The fact in question: TERM diff --git a/test/regress/regress0/sygus/General_plus10.sy b/test/regress/regress0/sygus/General_plus10.sy index 1792749e2..69bcd0f08 100755 --- a/test/regress/regress0/sygus/General_plus10.sy +++ b/test/regress/regress0/sygus/General_plus10.sy @@ -1,11 +1,10 @@ ; EXPECT: unsat -; COMMAND-LINE: --cegqi-si=all --sygus-out=status +; COMMAND-LINE: --lang=sygus2 --cegqi-si=all --sygus-out=status (set-logic LIA) -(synth-fun fb () Int ((Start Int ((Constant Int))))) -(synth-fun fc () Int ((Start Int ((Constant Int))))) +(synth-fun fb () Int ((Start Int)) ((Start Int ((Constant Int))))) +(synth-fun fc () Int ((Start Int)) ((Start Int ((Constant Int))))) -(constraint (= fc (+ fb 10))) +(constraint (= fc (+ fb 10))) (check-synth) - diff --git a/test/regress/regress0/sygus/aig-si.sy b/test/regress/regress0/sygus/aig-si.sy index ef12e3c0e..9330546d8 100644 --- a/test/regress/regress0/sygus/aig-si.sy +++ b/test/regress/regress0/sygus/aig-si.sy @@ -1,11 +1,12 @@ ; EXPECT: unsat -; COMMAND-LINE: --cegqi-si=all --cegqi-si-abort --decision=internal --cbqi --cbqi-prereg-inst --sygus-out=status +; COMMAND-LINE: --lang=sygus2 --cegqi-si=all --cegqi-si-abort --decision=internal --cbqi --cbqi-prereg-inst --sygus-out=status (set-logic BV) (define-fun parity ((a Bool) (b Bool) (c Bool) (d Bool)) Bool (xor (not (xor a b)) (not (xor c d)))) (synth-fun AIG ((a Bool) (b Bool) (c Bool) (d Bool)) Bool + ((Start Bool)) ((Start Bool ((and Start Start) (not Start) a b c d)))) (declare-var a Bool) diff --git a/test/regress/regress0/sygus/array-grammar-select.sy b/test/regress/regress0/sygus/array-grammar-select.sy index d216bbb24..2c0b4cf9a 100644 --- a/test/regress/regress0/sygus/array-grammar-select.sy +++ b/test/regress/regress0/sygus/array-grammar-select.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --sygus-out=status +; COMMAND-LINE: --lang=sygus2 --sygus-out=status (set-logic ALIA) (synth-fun f diff --git a/test/regress/regress0/sygus/array-grammar-store.sy b/test/regress/regress0/sygus/array-grammar-store.sy index 70525e83b..025a17b15 100644 --- a/test/regress/regress0/sygus/array-grammar-store.sy +++ b/test/regress/regress0/sygus/array-grammar-store.sy @@ -1,13 +1,13 @@ ; EXPECT: unsat -; COMMAND-LINE: --sygus-out=status +; COMMAND-LINE: --lang=sygus2 --sygus-out=status (set-logic ABV) (synth-fun f - ((s (Array (BitVec 4) (BitVec 4))) (t (BitVec 4))) - (Array (BitVec 4) (BitVec 4)) + ((s (Array (_ BitVec 4) (_ BitVec 4))) (t (_ BitVec 4))) + (Array (_ BitVec 4) (_ BitVec 4)) ) -(declare-var x (Array (BitVec 4) (BitVec 4))) +(declare-var x (Array (_ BitVec 4) (_ BitVec 4))) (constraint (= (= (store x #b0000 #b0000) (store x #b0001 #b0000)) (= (f x #b0000) (f x #b0001)))) diff --git a/test/regress/regress0/sygus/ccp16.lus.sy b/test/regress/regress0/sygus/ccp16.lus.sy index 662069105..91fe27b0b 100644 --- a/test/regress/regress0/sygus/ccp16.lus.sy +++ b/test/regress/regress0/sygus/ccp16.lus.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --sygus-out=status +; COMMAND-LINE: --lang=sygus2 --sygus-out=status (set-logic SAT) (define-fun @@ -30,9 +30,6 @@ )) -(declare-primed-var top.usr.OK Bool) -(declare-primed-var top.res.init_flag Bool) - (define-fun init ( (top.usr.OK Bool) diff --git a/test/regress/regress0/sygus/cegqi-si-string-triv-2fun.sy b/test/regress/regress0/sygus/cegqi-si-string-triv-2fun.sy index fc8864f55..8fe64697b 100644 --- a/test/regress/regress0/sygus/cegqi-si-string-triv-2fun.sy +++ b/test/regress/regress0/sygus/cegqi-si-string-triv-2fun.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) (y String)) String) diff --git a/test/regress/regress0/sygus/cegqi-si-string-triv.sy b/test/regress/regress0/sygus/cegqi-si-string-triv.sy index 86a68574f..f5ce07ec6 100644 --- a/test/regress/regress0/sygus/cegqi-si-string-triv.sy +++ b/test/regress/regress0/sygus/cegqi-si-string-triv.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) (y String)) String) diff --git a/test/regress/regress0/sygus/dt-no-syntax.sy b/test/regress/regress0/sygus/dt-no-syntax.sy index f4de9b055..e33edf36c 100644 --- a/test/regress/regress0/sygus/dt-no-syntax.sy +++ b/test/regress/regress0/sygus/dt-no-syntax.sy @@ -1,4 +1,4 @@ -; COMMAND-LINE: --sygus-out=status +; COMMAND-LINE: --lang=sygus2 --sygus-out=status ; EXPECT: unsat (set-logic LIA) diff --git a/test/regress/regress0/sygus/dt-sel-parse1.sy b/test/regress/regress0/sygus/dt-sel-parse1.sy index 52edb3278..52f068055 100644 --- a/test/regress/regress0/sygus/dt-sel-parse1.sy +++ b/test/regress/regress0/sygus/dt-sel-parse1.sy @@ -1,4 +1,4 @@ -; COMMAND-LINE: --sygus-out=status +; COMMAND-LINE: --lang=sygus2 --sygus-out=status ; EXPECT: unsat (set-logic ALL_SUPPORTED) @@ -27,6 +27,7 @@ ; provide synthesis template (synth-fun f ((secret Ship) (prior ShipRange) (response Bool)) ShipRange +((Start ShipRange) (B Bool) (SR ShipRange) (IR IntRange) (LR LocRange) (I Int)) ( (Start ShipRange ((ite B SR SR))) (B Bool (response)) diff --git a/test/regress/regress0/sygus/hd-05-d1-prog-nogrammar.sy b/test/regress/regress0/sygus/hd-05-d1-prog-nogrammar.sy index 71af1e916..b410e5d23 100644 --- a/test/regress/regress0/sygus/hd-05-d1-prog-nogrammar.sy +++ b/test/regress/regress0/sygus/hd-05-d1-prog-nogrammar.sy @@ -1,10 +1,10 @@ -; COMMAND-LINE: --sygus-out=status --cegqi-si=none +; COMMAND-LINE: --lang=sygus2 --sygus-out=status --cegqi-si=none ; EXPECT: unsat (set-logic BV) -(synth-fun f ((x (BitVec 32))) (BitVec 32)) +(synth-fun f ((x (_ BitVec 32))) (_ BitVec 32)) -(declare-var x (BitVec 32)) +(declare-var x (_ BitVec 32)) (constraint (= (bvor x #x00000001) (f x))) (check-synth) diff --git a/test/regress/regress0/sygus/inv-different-var-order.sy b/test/regress/regress0/sygus/inv-different-var-order.sy index c3f43fc07..7b7d50e22 100644 --- a/test/regress/regress0/sygus/inv-different-var-order.sy +++ b/test/regress/regress0/sygus/inv-different-var-order.sy @@ -1,10 +1,7 @@ -; COMMAND-LINE: --sygus-out=status +; COMMAND-LINE: --lang=sygus2 --sygus-out=status ;EXPECT: unsat (set-logic LIA) (synth-inv inv-f ((x Int) (y Int) (b Bool))) -(declare-primed-var b Bool) -(declare-primed-var x Int) -(declare-primed-var y Int) (define-fun pre-f ((x Int) (y Int) (b Bool)) Bool (and (and (>= x 5) (<= x 9)) @@ -19,4 +16,4 @@ ) (define-fun post-f ((x Int) (y Int) (b Bool)) Bool true) (inv-constraint inv-f pre-f trans-f post-f) -(check-synth)
\ No newline at end of file +(check-synth) diff --git a/test/regress/regress0/sygus/issue3624.sy b/test/regress/regress0/sygus/issue3624.sy index cc677bb9c..992965432 100644 --- a/test/regress/regress0/sygus/issue3624.sy +++ b/test/regress/regress0/sygus/issue3624.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --sygus-out=status +; COMMAND-LINE: --lang=sygus2 --sygus-out=status (set-logic ALL) (declare-var A Bool) (declare-var B (Array Int Bool)) diff --git a/test/regress/regress0/sygus/let-ringer.sy b/test/regress/regress0/sygus/let-ringer.sy index 1bb85bed9..9f9eea2a8 100644 --- a/test/regress/regress0/sygus/let-ringer.sy +++ b/test/regress/regress0/sygus/let-ringer.sy @@ -1,11 +1,12 @@ ; EXPECT: unsat -; COMMAND-LINE: --cegqi-si=all --sygus-out=status -; COMMAND-LINE: --cegqi-si=all --sygus-unif-pi=complete --sygus-out=status +; COMMAND-LINE: --lang=sygus2 --cegqi-si=all --sygus-out=status +; COMMAND-LINE: --lang=sygus2 --cegqi-si=all --sygus-unif-pi=complete --sygus-out=status (set-logic LIA) (define-fun g ((x Int)) Int (ite (= x 1) 15 19)) (define-fun letf ((z Int) (w Int) (s Int) (x Int)) Int (+ z (+ x (+ x (+ s (+ 1 (+ (g w) z))))))) (synth-fun f ((x Int)) Int + ((Start Int)) ((Start Int (x 0 1 diff --git a/test/regress/regress0/sygus/let-simp.sy b/test/regress/regress0/sygus/let-simp.sy index 7e191e312..91a865035 100644 --- a/test/regress/regress0/sygus/let-simp.sy +++ b/test/regress/regress0/sygus/let-simp.sy @@ -1,8 +1,9 @@ ; EXPECT: unsat -; COMMAND-LINE: --cegqi-si=all --sygus-out=status +; COMMAND-LINE: --lang=sygus2 --cegqi-si=all --sygus-out=status (set-logic LIA) (define-fun letf ((z Int)) Int (+ z z)) (synth-fun f ((x Int) (y Int)) Int + ((Start Int)) ((Start Int (x y 0 @@ -13,4 +14,3 @@ (declare-var y Int) (constraint (= (f x y) (* 3 x))) (check-synth) - diff --git a/test/regress/regress0/sygus/no-syntax-test-bool.sy b/test/regress/regress0/sygus/no-syntax-test-bool.sy index c6c9383bb..4978b7a57 100644 --- a/test/regress/regress0/sygus/no-syntax-test-bool.sy +++ b/test/regress/regress0/sygus/no-syntax-test-bool.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --sygus-out=status +; COMMAND-LINE: --lang=sygus2 --sygus-out=status (set-logic LIA) @@ -12,4 +12,3 @@ (check-synth) - diff --git a/test/regress/regress0/sygus/no-syntax-test.sy b/test/regress/regress0/sygus/no-syntax-test.sy index f27a07ee7..696d413ad 100644 --- a/test/regress/regress0/sygus/no-syntax-test.sy +++ b/test/regress/regress0/sygus/no-syntax-test.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --sygus-out=status +; COMMAND-LINE: --lang=sygus2 --sygus-out=status (set-logic LIA) @@ -12,4 +12,3 @@ (check-synth) - diff --git a/test/regress/regress0/sygus/parity-AIG-d0.sy b/test/regress/regress0/sygus/parity-AIG-d0.sy index 50c7d39a0..09fae5410 100644 --- a/test/regress/regress0/sygus/parity-AIG-d0.sy +++ b/test/regress/regress0/sygus/parity-AIG-d0.sy @@ -1,11 +1,12 @@ ; EXPECT: unsat -; COMMAND-LINE: --cegqi-si=all --sygus-out=status +; COMMAND-LINE: --lang=sygus2 --cegqi-si=all --sygus-out=status (set-logic BV) (define-fun parity ((a Bool) (b Bool) (c Bool) (d Bool)) Bool (xor (not (xor a b)) (not (xor c d)))) (synth-fun AIG ((a Bool) (b Bool) (c Bool) (d Bool)) Bool + ((Start Bool)) ((Start Bool ((and Start Start) (not Start) a b c d)))) (declare-var a Bool) diff --git a/test/regress/regress0/sygus/parse-bv-let.sy b/test/regress/regress0/sygus/parse-bv-let.sy index 1329918fc..60bb804b6 100644 --- a/test/regress/regress0/sygus/parse-bv-let.sy +++ b/test/regress/regress0/sygus/parse-bv-let.sy @@ -1,20 +1,21 @@ ; EXPECT: unsat -; COMMAND-LINE: --sygus-out=status +; COMMAND-LINE: --lang=sygus2 --sygus-out=status (set-logic BV) -(define-fun bit-reset ((x (BitVec 32)) (bit (BitVec 32))) (BitVec 32) - (let ((modulo-shift (BitVec 32) (bvand bit #x0000001f))) - (bvand modulo-shift x))) +(define-fun bit-reset ((x (_ BitVec 32)) (bit (_ BitVec 32))) (_ BitVec 32) + (let ((modulo-shift (bvand bit #x0000001f))) + (bvand modulo-shift x))) -(synth-fun btr ((x (BitVec 32)) (bit (BitVec 32))) (BitVec 32) - ((Start (BitVec 32) ( - (Constant (BitVec 32)) - (Variable (BitVec 32)) - (bvneg Start) (bvnot Start) (bvadd Start Start) (bvand Start Start) (bvlshr Start Start) (bvmul Start Start) (bvor Start Start) (bvshl Start Start) +(synth-fun btr ((x (_ BitVec 32)) (bit (_ BitVec 32))) (_ BitVec 32) + ((Start (_ BitVec 32))) + ((Start (_ BitVec 32) ( + (Constant (_ BitVec 32)) + (Variable (_ BitVec 32)) + (bvneg Start) (bvnot Start) (bvadd Start Start) (bvand Start Start) (bvlshr Start Start) (bvmul Start Start) (bvor Start Start) (bvshl Start Start) )))) -(declare-var x (BitVec 32)) -(declare-var bit (BitVec 32)) +(declare-var x (_ BitVec 32)) +(declare-var bit (_ BitVec 32)) (constraint (= (btr x bit) #b00000000000000000000000000000000)) (check-synth) diff --git a/test/regress/regress0/sygus/pbe-pred-contra.sy b/test/regress/regress0/sygus/pbe-pred-contra.sy index 5fbe91e2e..99c308173 100644 --- a/test/regress/regress0/sygus/pbe-pred-contra.sy +++ b/test/regress/regress0/sygus/pbe-pred-contra.sy @@ -1,4 +1,4 @@ -; COMMAND-LINE: --cegqi-si=none --sygus-out=status +; COMMAND-LINE: --lang=sygus2 --cegqi-si=none --sygus-out=status ; EXPECT: unknown (set-logic LIA) (synth-fun P ((x Int)) Bool) diff --git a/test/regress/regress0/sygus/real-si-all.sy b/test/regress/regress0/sygus/real-si-all.sy index 81f0ad22f..26524cdf6 100644 --- a/test/regress/regress0/sygus/real-si-all.sy +++ b/test/regress/regress0/sygus/real-si-all.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --sygus-out=status +; COMMAND-LINE: --lang=sygus2 --sygus-out=status (set-logic LRA) diff --git a/test/regress/regress0/sygus/strings-unconstrained.sy b/test/regress/regress0/sygus/strings-unconstrained.sy index 39c392487..49272165d 100644 --- a/test/regress/regress0/sygus/strings-unconstrained.sy +++ b/test/regress/regress0/sygus/strings-unconstrained.sy @@ -1,10 +1,9 @@ ; EXPECT: unsat -; COMMAND-LINE: --sygus-out=status +; COMMAND-LINE: --lang=sygus2 --sygus-out=status (set-logic SLIA) (synth-fun f ((firstname String) (lastname String)) String -((Start String (ntString)) - -(ntString String ( +((ntString String)) +((ntString String ( firstname lastname " " @@ -12,4 +11,3 @@ lastname )) (check-synth) - diff --git a/test/regress/regress0/sygus/sygus-no-wf.sy b/test/regress/regress0/sygus/sygus-no-wf.sy index 40a3d5547..e89d07fd9 100644 --- a/test/regress/regress0/sygus/sygus-no-wf.sy +++ b/test/regress/regress0/sygus/sygus-no-wf.sy @@ -1,7 +1,8 @@ -; COMMAND-LINE: --sygus-out=status +; COMMAND-LINE: --lang=sygus2 --sygus-out=status ; EXPECT: unsat (set-logic ALL) (synth-fun f ((x0 Bool)) Bool + ((B Bool) (I Int)) ( (B Bool ((Variable Bool) (Constant Bool) (= I I) )) (I Int ((Constant Int) (+ I I))) diff --git a/test/regress/regress0/sygus/uminus_one.sy b/test/regress/regress0/sygus/uminus_one.sy index 94040bf45..9024ac3b6 100644 --- a/test/regress/regress0/sygus/uminus_one.sy +++ b/test/regress/regress0/sygus/uminus_one.sy @@ -1,7 +1,7 @@ ; 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 ((- 1))))) +(synth-fun f ((x Int)) Int ((Start Int)) ((Start Int ((- 1))))) (declare-var x Int) (constraint (= (f x) (- 1))) (check-synth) diff --git a/test/regress/regress0/sygus/univ_3-long-repeat-conflict.sy b/test/regress/regress0/sygus/univ_3-long-repeat-conflict.sy index c2ed642be..b9bd8e815 100644 --- a/test/regress/regress0/sygus/univ_3-long-repeat-conflict.sy +++ b/test/regress/regress0/sygus/univ_3-long-repeat-conflict.sy @@ -1,21 +1,21 @@ ; EXPECT: unknown -; COMMAND-LINE: --sygus-out=status +; COMMAND-LINE: --lang=sygus2 --sygus-out=status (set-logic SLIA) - + (synth-fun f ((col1 String) (col2 String)) String - ((Start String (ntString)) - (ntString String (col1 col2 " " "," "USA" "PA" "CT" "CA" "MD" "NY" + ((ntString String) (ntInt Int) (ntBool Bool)) + ((ntString String (col1 col2 " " "," "USA" "PA" "CT" "CA" "MD" "NY" (str.++ ntString ntString) (str.replace ntString ntString ntString) (str.at ntString ntInt) - (int.to.str ntInt) + (str.from_int ntInt) (ite ntBool ntString ntString) (str.substr ntString ntInt ntInt))) (ntInt Int (0 1 2 (+ ntInt ntInt) (- ntInt ntInt) (str.len ntString) - (str.to.int ntString) + (str.to_int ntString) (str.indexof ntString ntString ntInt))) (ntBool Bool (true false (str.prefixof ntString ntString) diff --git a/test/regress/regress1/rr-verify/bool-crci.sy b/test/regress/regress1/rr-verify/bool-crci.sy index 955245f87..75837695d 100644 --- a/test/regress/regress1/rr-verify/bool-crci.sy +++ b/test/regress/regress1/rr-verify/bool-crci.sy @@ -1,11 +1,12 @@ -; COMMAND-LINE: --sygus-rr --sygus-samples=1000 --sygus-abort-size=3 --sygus-rr-verify-abort --no-sygus-sym-break +; COMMAND-LINE: --lang=sygus2 --sygus-rr --sygus-samples=1000 --sygus-abort-size=3 --sygus-rr-verify-abort --no-sygus-sym-break ; EXPECT: (error "Maximum term size (3) for enumerative SyGuS exceeded.") ; SCRUBBER: grep -v -E '(\(define-fun|\(candidate-rewrite)' ; EXIT: 1 (set-logic BV) -(synth-fun f ( (x Bool) (y Bool) (z Bool) (w Bool) ) Bool +(synth-fun f ( (x Bool) (y Bool) (z Bool) (w Bool) ) Bool + ( (Start Bool) (depth1 Bool) (depth2 Bool) (depth3 Bool) (depth4 Bool) ) ((Start Bool ( (and depth1 depth1) (not depth1) diff --git a/test/regress/regress1/rr-verify/bv-term-32.sy b/test/regress/regress1/rr-verify/bv-term-32.sy index 6c07bd8aa..9dfb19451 100644 --- a/test/regress/regress1/rr-verify/bv-term-32.sy +++ b/test/regress/regress1/rr-verify/bv-term-32.sy @@ -1,13 +1,14 @@ -; COMMAND-LINE: --sygus-rr --sygus-samples=1000 --sygus-abort-size=1 --sygus-rr-verify-abort --no-sygus-sym-break +; COMMAND-LINE: --lang=sygus2 --sygus-rr --sygus-samples=1000 --sygus-abort-size=1 --sygus-rr-verify-abort --no-sygus-sym-break ; EXPECT: (error "Maximum term size (1) for enumerative SyGuS exceeded.") ; SCRUBBER: grep -v -E '(\(define-fun|\(candidate-rewrite)' ; EXIT: 1 (set-logic BV) -(synth-fun f ((s (BitVec 32)) (t (BitVec 32))) (BitVec 32) +(synth-fun f ((s (_ BitVec 32)) (t (_ BitVec 32))) (_ BitVec 32) + ((Start (_ BitVec 32))) ( - (Start (BitVec 32) ( + (Start (_ BitVec 32) ( s t #x00000000 diff --git a/test/regress/regress1/rr-verify/bv-term.sy b/test/regress/regress1/rr-verify/bv-term.sy index f310396d2..9a11128d7 100644 --- a/test/regress/regress1/rr-verify/bv-term.sy +++ b/test/regress/regress1/rr-verify/bv-term.sy @@ -1,14 +1,15 @@ -; COMMAND-LINE: --sygus-rr --sygus-samples=1000 --sygus-abort-size=2 --sygus-rr-verify-abort --no-sygus-sym-break -; COMMAND-LINE: --sygus-rr-synth --sygus-samples=1000 --sygus-abort-size=2 --sygus-rr-verify-abort --sygus-rr-synth-check +; COMMAND-LINE: --lang=sygus2 --sygus-rr --sygus-samples=1000 --sygus-abort-size=2 --sygus-rr-verify-abort --no-sygus-sym-break +; COMMAND-LINE: --lang=sygus2 --sygus-rr-synth --sygus-samples=1000 --sygus-abort-size=2 --sygus-rr-verify-abort --sygus-rr-synth-check ; EXPECT: (error "Maximum term size (2) for enumerative SyGuS exceeded.") ; SCRUBBER: grep -v -E '(\(define-fun|\(candidate-rewrite|\(rewrite)' ; EXIT: 1 (set-logic BV) -(synth-fun f ((s (BitVec 4)) (t (BitVec 4))) (BitVec 4) +(synth-fun f ((s (_ BitVec 4)) (t (_ BitVec 4))) (_ BitVec 4) + ((Start (_ BitVec 4))) ( - (Start (BitVec 4) ( + (Start (_ BitVec 4) ( s t #x0 diff --git a/test/regress/regress1/rr-verify/fp-arith.sy b/test/regress/regress1/rr-verify/fp-arith.sy index e8b97d610..30828ca76 100644 --- a/test/regress/regress1/rr-verify/fp-arith.sy +++ b/test/regress/regress1/rr-verify/fp-arith.sy @@ -1,5 +1,5 @@ ; REQUIRES: symfpu -; COMMAND-LINE: --sygus-rr --sygus-samples=0 --sygus-rr-synth-check --sygus-abort-size=1 --sygus-rr-verify-abort --no-sygus-sym-break --fp-exp +; COMMAND-LINE: --lang=sygus2 --sygus-rr --sygus-samples=0 --sygus-rr-synth-check --sygus-abort-size=1 --sygus-rr-verify-abort --no-sygus-sym-break --fp-exp ; EXPECT: (error "Maximum term size (1) for enumerative SyGuS exceeded.") ; SCRUBBER: grep -v -E '(\(define-fun|\(rewrite)' ; EXIT: 1 @@ -13,6 +13,7 @@ (define-fun fp_nan () Float16 (_ NaN 5 11)) (synth-fun f ( (r RoundingMode) (x Float16) (y Float16)) Float16 +((Start Float16)) ( (Start Float16 ( (fp.abs Start) diff --git a/test/regress/regress1/rr-verify/fp-bool.sy b/test/regress/regress1/rr-verify/fp-bool.sy index bf0692f7d..6704198c3 100644 --- a/test/regress/regress1/rr-verify/fp-bool.sy +++ b/test/regress/regress1/rr-verify/fp-bool.sy @@ -1,5 +1,5 @@ ; REQUIRES: symfpu -; COMMAND-LINE: --sygus-rr --sygus-samples=0 --sygus-rr-synth-check --sygus-abort-size=1 --sygus-rr-verify-abort --no-sygus-sym-break --fp-exp +; COMMAND-LINE: --lang=sygus2 --sygus-rr --sygus-samples=0 --sygus-rr-synth-check --sygus-abort-size=1 --sygus-rr-verify-abort --no-sygus-sym-break --fp-exp ; EXPECT: (error "Maximum term size (1) for enumerative SyGuS exceeded.") ; SCRUBBER: grep -v -E '(\(define-fun|\(rewrite)' ; EXIT: 1 @@ -13,6 +13,7 @@ (define-fun fp_nan () Float16 (_ NaN 5 11)) (synth-fun f ( (r RoundingMode) (x Float16) (y Float16)) Bool +((Start Bool) (FpOp Float16)) ( (Start Bool ( (fp.isNaN FpOp) diff --git a/test/regress/regress1/rr-verify/string-term.sy b/test/regress/regress1/rr-verify/string-term.sy index 8f6593148..404719f6c 100644 --- a/test/regress/regress1/rr-verify/string-term.sy +++ b/test/regress/regress1/rr-verify/string-term.sy @@ -1,24 +1,25 @@ -; COMMAND-LINE: --sygus-rr --sygus-samples=1000 --sygus-abort-size=1 --sygus-rr-verify-abort --no-sygus-sym-break +; COMMAND-LINE: --lang=sygus2 --sygus-rr --sygus-samples=1000 --sygus-abort-size=1 --sygus-rr-verify-abort --no-sygus-sym-break ; EXPECT: (error "Maximum term size (1) for enumerative SyGuS exceeded.") ; SCRUBBER: grep -v -E '(\(define-fun|\(candidate-rewrite)' ; EXIT: 1 (set-logic SLIA) -(synth-fun f ((x String) (y String) (z Int)) String ( +(synth-fun f ((x String) (y String) (z Int)) String +((Start String) (StartInt Int)) ( (Start String ( x y "A" "B" "" (str.++ Start Start) (str.replace Start Start Start) (str.at Start StartInt) - (int.to.str StartInt) + (str.from_int StartInt) (str.substr Start StartInt StartInt))) (StartInt Int ( 0 1 z (+ StartInt StartInt) (- StartInt StartInt) (str.len Start) - (str.to.int Start) + (str.to_int Start) (str.indexof Start Start StartInt))) )) diff --git a/test/regress/regress1/sygus/Base16_1.sy b/test/regress/regress1/sygus/Base16_1.sy index b54c7688b..b84e5bb48 100644 --- a/test/regress/regress1/sygus/Base16_1.sy +++ b/test/regress/regress1/sygus/Base16_1.sy @@ -1,17 +1,18 @@ ; EXPECT: unsat -; COMMAND-LINE: --sygus-qe-preproc --cbqi-full --sygus-out=status --cegqi-si=all +; COMMAND-LINE: --lang=sygus2 --sygus-qe-preproc --cbqi-full --sygus-out=status --cegqi-si=all (set-logic BV) -(define-fun B ((h (BitVec 8)) (l (BitVec 8)) (v (BitVec 8))) (BitVec 8) (bvlshr (bvshl v (bvsub #x07 h)) (bvsub #x07 (bvsub h l)))) +(define-fun B ((h (_ BitVec 8)) (l (_ BitVec 8)) (v (_ BitVec 8))) (_ BitVec 8) (bvlshr (bvshl v (bvsub #x07 h)) (bvsub #x07 (bvsub h l)))) -(define-fun E ((x (BitVec 8))) (BitVec 8) (bvadd x #x41)) +(define-fun E ((x (_ BitVec 8))) (_ BitVec 8) (bvadd x #x41)) -(define-fun f ((x (BitVec 8))) (BitVec 8) (bvsub x #x41)) +(define-fun f ((x (_ BitVec 8))) (_ BitVec 8) (bvsub x #x41)) -(define-fun d ((x (BitVec 8))) Bool (bvule x #x3f)) +(define-fun d ((x (_ BitVec 8))) Bool (bvule x #x3f)) -(synth-fun D ((x (BitVec 8)) (y (BitVec 8)) ) (BitVec 8) - ((Start (BitVec 8) ( +(synth-fun D ((x (_ BitVec 8)) (y (_ BitVec 8)) ) (_ BitVec 8) + ((Start (_ BitVec 8)) (Const (_ BitVec 8))) + ((Start (_ BitVec 8) ( (f Start) x y Const (bvshl Start Start) (bvnot Start) (bvand Start Start) @@ -22,13 +23,11 @@ (bvlshr Start Start) (bvsub Start Start) )) - (Const (BitVec 8) (#x01 #x03 #x06 #x07 #x04 #x05 #x02 #x00)) + (Const (_ BitVec 8) (#x01 #x03 #x06 #x07 #x04 #x05 #x02 #x00)) )) -(declare-var x (BitVec 8)) +(declare-var x (_ BitVec 8)) (constraint (= x (D (E (B #x07 #x04 x) ) (E (B #x03 #x00 x)) )) ) ; notice we don't have solution reconstruction for this -(check-synth) - - +(check-synth) diff --git a/test/regress/regress1/sygus/VC22_a.sy b/test/regress/regress1/sygus/VC22_a.sy index ce437bc34..f60f661dd 100644 --- a/test/regress/regress1/sygus/VC22_a.sy +++ b/test/regress/regress1/sygus/VC22_a.sy @@ -1,9 +1,10 @@ ; EXPECT: unsat -; COMMAND-LINE: --sygus-out=status -; COMMAND-LINE: --sygus-out=status --cegis-sample=use +; COMMAND-LINE: --lang=sygus2 --sygus-out=status +; COMMAND-LINE: --lang=sygus2 --sygus-out=status --cegis-sample=use (set-logic LIA) (synth-fun f ((x1 Int) (x2 Int)) Int + ((Start Int) (StartBool Bool)) ((Start Int (0 1 x1 x2 (ite StartBool Start Start))) (StartBool Bool ((= Start Start))))) @@ -24,7 +25,6 @@ (define-fun InVorZero ((v Int)) Bool (or (InV1 v) (Zero v))) - (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))))) @@ -58,4 +58,3 @@ (constraint (or (Bad x1 x2) (not (Zero (f x1 x2))))) (check-synth) - diff --git a/test/regress/regress1/sygus/abv.sy b/test/regress/regress1/sygus/abv.sy index d9a8a019c..d42553c1b 100644 --- a/test/regress/regress1/sygus/abv.sy +++ b/test/regress/regress1/sygus/abv.sy @@ -1,61 +1,66 @@ ; EXPECT: unsat -; COMMAND-LINE: --sygus-out=status +; COMMAND-LINE: --lang=sygus2 --sygus-out=status (set-logic ABV) -(define-sort AddrSort () (BitVec 32)) -(define-sort ValSort () (BitVec 8)) +(define-sort AddrSort () (_ BitVec 32)) +(define-sort ValSort () (_ BitVec 8)) (define-sort MemSort () (Array AddrSort ValSort)) ; Write the value y to index x -(define-fun WriteArr - ; Args - ((x AddrSort) (y ValSort) (arrIn MemSort)) - - ; Return value - MemSort - - ; Function Body - (store arrIn x y) +(define-fun WriteArr + ; Args + ((x AddrSort) (y ValSort) (arrIn MemSort)) + + ; Return value + MemSort + + ; Function Body + (store arrIn x y) ) ; Read from index x -(define-fun ReadArr - ; Args - ((x AddrSort) (arrIn MemSort)) - - ; Return value - ValSort - - ; Function Body - (select arrIn x) +(define-fun ReadArr + ; Args + ((x AddrSort) (arrIn MemSort)) + + ; Return value + ValSort + + ; Function Body + (select arrIn x) ) (define-fun letf ((m MemSort) (v1 AddrSort) (v2 AddrSort)) ValSort - (bvadd - (ReadArr v1 m) + (bvadd + (ReadArr v1 m) (ReadArr v2 m))) -(synth-fun f - ; Args - ((x0 ValSort) (x1 ValSort) (idx0 AddrSort) (idx1 AddrSort) (mem MemSort)) - - ; Return value - ValSort - - ; Grammar - ( - (StartArray MemSort ( - (WriteArr (Variable AddrSort) (Variable ValSort) StartArray) - (WriteArr (Variable AddrSort) (Variable ValSort) mem))) - - (Start ValSort ( - (letf StartArray (Variable AddrSort) (Variable AddrSort)))) +(synth-fun f + ; Args + ((x0 ValSort) (x1 ValSort) (idx0 AddrSort) (idx1 AddrSort) (mem MemSort)) + + ; Return value + ValSort + + ; Grammar + ((Start ValSort) (StartArray MemSort) (ASVar AddrSort) (VSVar ValSort)) + ( + (Start ValSort ( + (letf StartArray ASVar ASVar))) + + (StartArray MemSort ( + (WriteArr ASVar VSVar StartArray) + (WriteArr ASVar VSVar mem))) + + ; "Hack" to avoid parse errors in V2 format. + (ASVar AddrSort ((Variable AddrSort))) + (VSVar ValSort ((Variable ValSort))) )) -(declare-var a (BitVec 8)) -(declare-var b (BitVec 8)) -(declare-var c (BitVec 32)) -(declare-var d (BitVec 32)) -(declare-var e (Array (BitVec 32) (BitVec 8))) +(declare-var a (_ BitVec 8)) +(declare-var b (_ BitVec 8)) +(declare-var c (_ BitVec 32)) +(declare-var d (_ BitVec 32)) +(declare-var e (Array (_ BitVec 32) (_ BitVec 8))) (constraint (=> (not (= c d)) (= (bvadd a b) (f a b c d e)))) (check-synth) diff --git a/test/regress/regress1/sygus/array_search_2.sy b/test/regress/regress1/sygus/array_search_2.sy index 93cbf9ce9..1a7c5888c 100644 --- a/test/regress/regress1/sygus/array_search_2.sy +++ b/test/regress/regress1/sygus/array_search_2.sy @@ -1,8 +1,8 @@ ; REQUIRES: proof ; EXPECT: unsat -; COMMAND-LINE: --cegqi-si=all --sygus-out=status --cegqi-si-sol-min-core --proof +; COMMAND-LINE: --lang=sygus2 --cegqi-si=all --sygus-out=status --cegqi-si-sol-min-core --proof (set-logic LIA) -(synth-fun findIdx ( (y1 Int) (y2 Int) (k1 Int)) Int ((Start Int ( 0 1 2 y1 y2 k1 (ite BoolExpr Start Start))) (BoolExpr Bool ((< Start Start) (<= Start Start) (> Start Start) (>= Start Start))))) +(synth-fun findIdx ((y1 Int) (y2 Int) (k1 Int)) Int ((Start Int) (BoolExpr Bool)) ((Start Int ( 0 1 2 y1 y2 k1 (ite BoolExpr Start Start))) (BoolExpr Bool ((< Start Start) (<= Start Start) (> Start Start) (>= Start Start))))) (declare-var x1 Int) (declare-var x2 Int) (declare-var k Int) diff --git a/test/regress/regress1/sygus/array_search_5-Q-easy.sy b/test/regress/regress1/sygus/array_search_5-Q-easy.sy index 8be52a577..dd1783d85 100644 --- a/test/regress/regress1/sygus/array_search_5-Q-easy.sy +++ b/test/regress/regress1/sygus/array_search_5-Q-easy.sy @@ -1,8 +1,12 @@ ; EXPECT: unsat -; COMMAND-LINE: --cegqi-si=all --sygus-out=status --decision=justification -( set-logic LIA ) -( synth-fun findIdx ( ( y1 Int ) ( y2 Int ) ( y3 Int ) ( y4 Int ) ( y5 Int ) ( k1 Int ) ) Int ( - (Start Int ( NT1 +; COMMAND-LINE: --lang=sygus2 --cegqi-si=all --sygus-out=status --decision=justification +(set-logic LIA) + +(synth-fun findIdx ((y1 Int) (y2 Int) (y3 Int) (y4 Int) (y5 Int) (k1 Int)) Int + ((Start Int) (NT1 Int) (NT2 Bool) (NT3 Int) (NT4 Int) (NT5 Bool) (NT6 Bool) (NT7 Int) (NT8 Int) (NT9 Int) (NT10 Int) + (NT11 Int) (NT12 Bool) (NT13 Int) (NT14 Int) (NT15 Bool) (NT16 Bool) (NT17 Bool) (NT18 Bool) (NT19 Bool)) ( + (Start Int ( + NT1 NT3 NT4 NT7 @@ -13,7 +17,8 @@ NT13 NT14 )) - (NT1 Int ( y5 + (NT1 Int ( + y5 k1 1 y2 @@ -26,22 +31,27 @@ y3 3 )) - (NT2 Bool ( (< NT1 NT1) + (NT2 Bool ( + (< NT1 NT1) (> NT1 NT1) (>= NT1 NT1) (<= NT1 NT1) )) - (NT3 Int ( (ite NT2 NT1 NT1) + (NT3 Int ( + (ite NT2 NT1 NT1) )) - (NT4 Int ( (ite NT5 NT1 NT1) + (NT4 Int ( + (ite NT5 NT1 NT1) (ite NT2 NT3 NT1) )) - (NT5 Bool ( (< NT3 NT1) + (NT5 Bool ( + (< NT3 NT1) (<= NT3 NT1) (>= NT3 NT1) (> NT3 NT1) )) - (NT6 Bool ( (<= NT4 NT1) + (NT6 Bool ( + (<= NT4 NT1) (> NT4 NT1) (<= NT3 NT3) (> NT3 NT3) @@ -50,33 +60,39 @@ (< NT3 NT3) (>= NT3 NT3) )) - (NT7 Int ( (ite NT6 NT1 NT1) + (NT7 Int ( + (ite NT6 NT1 NT1) (ite NT2 NT4 NT1) )) - (NT8 Int ( (ite NT2 NT7 NT1) + (NT8 Int ( + (ite NT2 NT7 NT1) (ite NT5 NT4 NT1) (ite NT15 NT1 NT1) (ite NT5 NT1 NT4) )) - (NT9 Int ( (ite NT2 NT8 NT1) + (NT9 Int ( + (ite NT2 NT8 NT1) (ite NT12 NT1 NT1) (ite NT6 NT1 NT4) (ite NT6 NT4 NT1) (ite NT5 NT7 NT1) )) - (NT10 Int ( (ite NT5 NT8 NT1) + (NT10 Int ( + (ite NT5 NT8 NT1) (ite NT16 NT1 NT1) (ite NT2 NT9 NT1) (ite NT6 NT7 NT1) (ite NT5 NT4 NT4) )) - (NT11 Int ( (ite NT6 NT8 NT1) + (NT11 Int ( + (ite NT6 NT8 NT1) (ite NT2 NT10 NT1) (ite NT5 NT9 NT1) (ite NT17 NT1 NT1) (ite NT6 NT4 NT4) )) - (NT12 Bool ( (< NT4 NT4) + (NT12 Bool ( + (< NT4 NT4) (> NT4 NT4) (<= NT8 NT1) (< NT8 NT1) @@ -85,31 +101,36 @@ (>= NT8 NT1) (>= NT4 NT4) )) - (NT13 Int ( (ite NT18 NT1 NT1) + (NT13 Int ( + (ite NT18 NT1 NT1) (ite NT12 NT7 NT1) (ite NT5 NT10 NT1) (ite NT6 NT9 NT1) (ite NT12 NT1 NT7) (ite NT2 NT11 NT1) )) - (NT14 Int ( (ite NT12 NT1 NT8) + (NT14 Int ( + (ite NT12 NT1 NT8) (ite NT6 NT10 NT1) (ite NT5 NT11 NT1) (ite NT19 NT1 NT1) (ite NT12 NT8 NT1) (ite NT2 NT13 NT1) )) - (NT15 Bool ( (>= NT7 NT1) + (NT15 Bool ( + (>= NT7 NT1) (< NT7 NT1) (> NT7 NT1) (<= NT7 NT1) )) - (NT16 Bool ( (< NT9 NT1) + (NT16 Bool ( + (< NT9 NT1) (>= NT9 NT1) (> NT9 NT1) (<= NT9 NT1) )) - (NT17 Bool ( (< NT7 NT7) + (NT17 Bool ( + (< NT7 NT7) (<= NT10 NT1) (>= NT10 NT1) (> NT10 NT1) @@ -118,12 +139,14 @@ (>= NT7 NT7) (<= NT7 NT7) )) - (NT18 Bool ( (< NT11 NT1) + (NT18 Bool ( + (< NT11 NT1) (> NT11 NT1) (>= NT11 NT1) (<= NT11 NT1) )) - (NT19 Bool ( (>= NT13 NT1) + (NT19 Bool ( + (>= NT13 NT1) (>= NT8 NT8) (< NT13 NT1) (> NT13 NT1) @@ -133,12 +156,13 @@ (<= NT13 NT1) )) )) - ( declare-var x1 Int ) - ( declare-var x2 Int ) - ( declare-var x3 Int ) - ( declare-var x4 Int ) - ( declare-var x5 Int ) - ( declare-var k Int ) - ( constraint ( => ( and ( < x1 x2 ) ( and ( < x2 x3 ) ( and ( < x3 x4 ) ( < x4 x5 ) ) ) ) ( => ( < k x1 ) ( = ( findIdx x1 x2 x3 x4 x5 k ) 0 ) ) ) ) - ( check-synth ) +(declare-var x1 Int) +(declare-var x2 Int) +(declare-var x3 Int) +(declare-var x4 Int) +(declare-var x5 Int) +(declare-var k Int) + +(constraint (=> (and (< x1 x2) (and (< x2 x3) (and (< x3 x4) (< x4 x5)))) (=> (< k x1) (= (findIdx x1 x2 x3 x4 x5 k) 0)))) +(check-synth) diff --git a/test/regress/regress1/sygus/array_sum_2_5.sy b/test/regress/regress1/sygus/array_sum_2_5.sy index 84a75d086..84046f30a 100644 --- a/test/regress/regress1/sygus/array_sum_2_5.sy +++ b/test/regress/regress1/sygus/array_sum_2_5.sy @@ -1,7 +1,7 @@ ; EXPECT: unsat -; COMMAND-LINE: --cegqi-si=all --sygus-out=status +; COMMAND-LINE: --lang=sygus2 --cegqi-si=all --sygus-out=status (set-logic LIA) -(synth-fun findSum ( (y1 Int) (y2 Int) )Int ((Start Int ( 0 1 2 y1 y2 (+ Start Start) (ite BoolExpr Start Start))) (BoolExpr Bool ((< Start Start) (<= Start Start) (> Start Start) (>= Start Start))))) +(synth-fun findSum ( (y1 Int) (y2 Int) )Int ((Start Int) (BoolExpr Bool)) ((Start Int ( 0 1 2 y1 y2 (+ Start Start) (ite BoolExpr Start Start))) (BoolExpr Bool ((< Start Start) (<= Start Start) (> Start Start) (>= Start Start))))) (declare-var x1 Int) (declare-var x2 Int) (constraint (=> (> (+ x1 x2) 5) (= (findSum x1 x2 ) (+ x1 x2)))) diff --git a/test/regress/regress1/sygus/bvudiv-by-2.sy b/test/regress/regress1/sygus/bvudiv-by-2.sy index d6491972a..2bd8fc0dc 100644 --- a/test/regress/regress1/sygus/bvudiv-by-2.sy +++ b/test/regress/regress1/sygus/bvudiv-by-2.sy @@ -1,9 +1,10 @@ ; EXPECT: unsat -; COMMAND-LINE: --sygus-out=status +; COMMAND-LINE: --lang=sygus2 --sygus-out=status (set-logic BV) -(synth-fun f ((x (BitVec 32))) (BitVec 32) -((Start (BitVec 32) +(synth-fun f ((x (_ BitVec 32))) (_ BitVec 32) +((Start (_ BitVec 32)) (StartBool Bool)) +((Start (_ BitVec 32) ( (bvudiv Start Start) (bvurem Start Start) @@ -16,7 +17,7 @@ (bvugt Start Start) (= Start Start) )))) -(declare-var x (BitVec 32) ) +(declare-var x (_ BitVec 32) ) ; property (constraint (= (f #x00000008) #x00000004)) diff --git a/test/regress/regress1/sygus/car_3.lus.sy b/test/regress/regress1/sygus/car_3.lus.sy index 9432d3131..3b58a997c 100755 --- a/test/regress/regress1/sygus/car_3.lus.sy +++ b/test/regress/regress1/sygus/car_3.lus.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --sygus-out=status --sygus-unif-pi=cond-enum-igain --decision=justification +; COMMAND-LINE: --lang=sygus2 --sygus-out=status --sygus-unif-pi=cond-enum-igain --decision=justification (set-logic LIA) diff --git a/test/regress/regress1/sygus/cegar1.sy b/test/regress/regress1/sygus/cegar1.sy index ee85db88a..d3b2030de 100644 --- a/test/regress/regress1/sygus/cegar1.sy +++ b/test/regress/regress1/sygus/cegar1.sy @@ -1,15 +1,12 @@ ; EXPECT: unsat -; COMMAND-LINE: --sygus-inv-templ=post --sygus-out=status +; COMMAND-LINE: --lang=sygus2 --sygus-inv-templ=post --sygus-out=status (set-logic LIA) (synth-inv inv-f ((x Int) (y Int))) -(declare-primed-var x Int) -(declare-primed-var y Int) - (define-fun pre-f ((x Int) (y Int)) Bool (and (and (>= x 0) -(and (<= x 2) +(and (<= x 2) (<= y 2))) (>= y 0))) (define-fun trans-f ((x Int) (y Int) (x! Int) (y! Int)) Bool diff --git a/test/regress/regress1/sygus/cegis-unif-inv-eq-fair.sy b/test/regress/regress1/sygus/cegis-unif-inv-eq-fair.sy index df0214316..c3b09011c 100644 --- a/test/regress/regress1/sygus/cegis-unif-inv-eq-fair.sy +++ b/test/regress/regress1/sygus/cegis-unif-inv-eq-fair.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --sygus-unif-pi=complete --sygus-bool-ite-return-const --sygus-out=status +; COMMAND-LINE: --lang=sygus2 --sygus-unif-pi=complete --sygus-bool-ite-return-const --sygus-out=status (set-logic LIA) (define-fun @@ -187,9 +187,9 @@ ) Bool (let - ((X1 Bool top.res.abs_10@0)) + ((X1 top.res.abs_10@0)) (let - ((X2 Int top.res.abs_4@0)) + ((X2 top.res.abs_4@0)) (and (= top.usr.OK@0 (=> X1 (< X2 4))) (__node_init_voiture_0 @@ -258,9 +258,9 @@ ) Bool (let - ((X1 Bool top.res.abs_10@1)) + ((X1 top.res.abs_10@1)) (let - ((X2 Int top.res.abs_4@1)) + ((X2 top.res.abs_4@1)) (and (= top.usr.OK@1 (=> X1 (< X2 4))) (__node_trans_voiture_0 @@ -334,25 +334,6 @@ )) -(declare-primed-var top.usr.m Bool) -(declare-primed-var top.usr.s Bool) -(declare-primed-var top.usr.OK Bool) -(declare-primed-var top.res.init_flag Bool) -(declare-primed-var top.res.abs_0 Bool) -(declare-primed-var top.res.abs_1 Bool) -(declare-primed-var top.res.abs_2 Bool) -(declare-primed-var top.res.abs_3 Int) -(declare-primed-var top.res.abs_4 Int) -(declare-primed-var top.res.abs_5 Int) -(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.abs_9 Bool) -(declare-primed-var top.res.abs_10 Bool) -(declare-primed-var top.res.inst_3 Bool) -(declare-primed-var top.res.inst_2 Bool) -(declare-primed-var top.res.inst_1 Bool) -(declare-primed-var top.res.inst_0 Bool) (define-fun init ( @@ -378,9 +359,9 @@ ) Bool (let - ((X1 Bool top.res.abs_10)) + ((X1 top.res.abs_10)) (let - ((X2 Int top.res.abs_4)) + ((X2 top.res.abs_4)) (and (= top.usr.OK (=> X1 (< X2 4))) (__node_init_voiture_0 @@ -454,9 +435,9 @@ ) Bool (let - ((X1 Bool top.res.abs_10!)) + ((X1 top.res.abs_10!)) (let - ((X2 Int top.res.abs_4!)) + ((X2 top.res.abs_4!)) (and (= top.usr.OK! (=> X1 (< X2 4))) (__node_trans_voiture_0 diff --git a/test/regress/regress1/sygus/cegisunif-depth1.sy b/test/regress/regress1/sygus/cegisunif-depth1.sy index 9f6f65907..06c4d3a78 100644 --- a/test/regress/regress1/sygus/cegisunif-depth1.sy +++ b/test/regress/regress1/sygus/cegisunif-depth1.sy @@ -1,8 +1,9 @@ ; EXPECT: unsat -; COMMAND-LINE: --sygus-unif-pi=complete --sygus-out=status +; COMMAND-LINE: --lang=sygus2 --sygus-unif-pi=complete --sygus-out=status (set-logic LIA) (synth-fun f ((x Int) (y Int)) Int + ((Start Int) (CBool Bool)) ( (Start Int (0 1 x y diff --git a/test/regress/regress1/sygus/cggmp.sy b/test/regress/regress1/sygus/cggmp.sy index a3247e4f4..551528633 100644 --- a/test/regress/regress1/sygus/cggmp.sy +++ b/test/regress/regress1/sygus/cggmp.sy @@ -1,15 +1,12 @@ ; EXPECT: unsat -; COMMAND-LINE: --sygus-inv-templ=pre --sygus-out=status +; COMMAND-LINE: --lang=sygus2 --sygus-inv-templ=pre --sygus-out=status (set-logic LIA) (synth-inv inv-f ((i Int) (j Int))) -(declare-primed-var i Int) -(declare-primed-var j Int) - (define-fun pre-f ((i Int) (j Int)) Bool -(and (= i 1) +(and (= i 1) (= j 10))) (define-fun trans-f ((i Int) (j Int) (i! Int) (j! Int)) Bool diff --git a/test/regress/regress1/sygus/clock-inc-tuple.sy b/test/regress/regress1/sygus/clock-inc-tuple.sy index 65b17605d..c9705f7b8 100644 --- a/test/regress/regress1/sygus/clock-inc-tuple.sy +++ b/test/regress/regress1/sygus/clock-inc-tuple.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --cegqi-si=all --sygus-out=status --decision=justification +; COMMAND-LINE: --lang=sygus2 --cegqi-si=all --sygus-out=status --decision=justification (set-logic ALL_SUPPORTED) (declare-var m Int) @@ -8,7 +8,7 @@ (declare-datatypes ((tuple2 0)) ( ((tuple2 (_m Int) (_s Int))) )) (synth-fun x12 ((m Int) (s Int) (inc Int)) tuple2) -(constraint (=> -(and (>= m 0) (>= s 0) (< s 3) (> inc 0)) +(constraint (=> +(and (>= m 0) (>= s 0) (< s 3) (> inc 0)) (and (>= (_m (x12 m s inc)) 0) (>= (_s (x12 m s inc)) 0) (< (_s (x12 m s inc)) 3) (= (+ (* (_m (x12 m s inc)) 3) (_s (x12 m s inc))) (+ (+ (* m 3) s) inc))))) (check-synth) diff --git a/test/regress/regress1/sygus/commutative-stream.sy b/test/regress/regress1/sygus/commutative-stream.sy index 8203fd9cf..5febabc42 100644 --- a/test/regress/regress1/sygus/commutative-stream.sy +++ b/test/regress/regress1/sygus/commutative-stream.sy @@ -3,11 +3,12 @@ ; EXPECT: (error "Maximum term size (2) for enumerative SyGuS exceeded.") ; EXIT: 1 -; COMMAND-LINE: --sygus-stream --sygus-abort-size=2 --sygus-active-gen=none --decision=justification +; COMMAND-LINE: --lang=sygus2 --sygus-stream --sygus-abort-size=2 --sygus-active-gen=none --decision=justification (set-logic LIA) (synth-fun comm ((x Int) (y Int)) Int + ((Start Int)) ((Start Int (x y (+ Start Start) diff --git a/test/regress/regress1/sygus/commutative.sy b/test/regress/regress1/sygus/commutative.sy index 24201b453..7fe07c3fa 100644 --- a/test/regress/regress1/sygus/commutative.sy +++ b/test/regress/regress1/sygus/commutative.sy @@ -1,9 +1,10 @@ ; EXPECT: unsat -; COMMAND-LINE: --sygus-out=status +; COMMAND-LINE: --lang=sygus2 --sygus-out=status (set-logic LIA) (synth-fun comm ((x Int) (y Int)) Int + ((Start Int)) ((Start Int (x y (+ Start Start) diff --git a/test/regress/regress1/sygus/constant-bool-si-all.sy b/test/regress/regress1/sygus/constant-bool-si-all.sy index 45d49e75b..18a60f176 100644 --- a/test/regress/regress1/sygus/constant-bool-si-all.sy +++ b/test/regress/regress1/sygus/constant-bool-si-all.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 () Bool) (synth-fun g () Bool) diff --git a/test/regress/regress1/sygus/constant-dec-tree-bug.sy b/test/regress/regress1/sygus/constant-dec-tree-bug.sy index e20520a4a..ddbf07d61 100644 --- a/test/regress/regress1/sygus/constant-dec-tree-bug.sy +++ b/test/regress/regress1/sygus/constant-dec-tree-bug.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --sygus-out=status --sygus-unif-pi=complete +; COMMAND-LINE: --lang=sygus2 --sygus-out=status --sygus-unif-pi=complete (set-logic LIA) (synth-fun u ((x Int)) Int) diff --git a/test/regress/regress1/sygus/constant-ite-bv.sy b/test/regress/regress1/sygus/constant-ite-bv.sy index 330ef026e..356c71d1d 100644 --- a/test/regress/regress1/sygus/constant-ite-bv.sy +++ b/test/regress/regress1/sygus/constant-ite-bv.sy @@ -1,16 +1,17 @@ ; EXPECT: unsat -; COMMAND-LINE: --sygus-out=status --no-sygus-pbe --sygus-repair-const +; COMMAND-LINE: --lang=sygus2 --sygus-out=status --no-sygus-pbe --sygus-repair-const (set-logic BV) -(synth-fun f ( (x (BitVec 64))) (BitVec 64) +(synth-fun f ( (x (_ BitVec 64))) (_ BitVec 64) +((Start (_ BitVec 64)) (StartBool Bool)) ( -(Start (BitVec 64) ( +(Start (_ BitVec 64) ( #x0000000000000000 #x0000000000000001 x (bvnot Start) (bvadd Start Start) (ite StartBool Start Start) - (Constant (BitVec 64)) + (Constant (_ BitVec 64)) )) (StartBool Bool ((bvule Start Start))) ) diff --git a/test/regress/regress1/sygus/constant.sy b/test/regress/regress1/sygus/constant.sy index 1bb3e59fa..1416d566d 100644 --- a/test/regress/regress1/sygus/constant.sy +++ b/test/regress/regress1/sygus/constant.sy @@ -1,9 +1,10 @@ ; EXPECT: unsat -; COMMAND-LINE: --sygus-out=status +; COMMAND-LINE: --lang=sygus2 --sygus-out=status (set-logic LIA) (synth-fun constant ((x Int)) Int + ((Start Int)) ((Start Int (x 0 1 diff --git a/test/regress/regress1/sygus/crci-ssb-unk.sy b/test/regress/regress1/sygus/crci-ssb-unk.sy index f2b28db9c..d59fd297d 100644 --- a/test/regress/regress1/sygus/crci-ssb-unk.sy +++ b/test/regress/regress1/sygus/crci-ssb-unk.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --sygus-out=status +; COMMAND-LINE: --lang=sygus2 --sygus-out=status (set-logic BV) @@ -10,6 +10,7 @@ (synth-fun skel ( (LN4 Bool) (LN91 Bool) ) Bool + ((Start Bool) (depth1 Bool) (depth2 Bool) (depth3 Bool) (depth4 Bool)) ((Start Bool ( (and depth1 depth1) (xor depth1 depth1) diff --git a/test/regress/regress1/sygus/crcy-si-rcons.sy b/test/regress/regress1/sygus/crcy-si-rcons.sy index 6e2f54c31..70aec7c4c 100644 --- a/test/regress/regress1/sygus/crcy-si-rcons.sy +++ b/test/regress/regress1/sygus/crcy-si-rcons.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --cegqi-si=all --cegqi-si-abort --decision=internal --cegqi-si-rcons=try --sygus-out=status +; COMMAND-LINE: --lang=sygus2 --cegqi-si=all --cegqi-si-abort --decision=internal --cegqi-si-rcons=try --sygus-out=status (set-logic BV) @@ -10,6 +10,8 @@ (synth-fun skel ( (LN24 Bool) (k3 Bool) (LN129 Bool) (LN141 Bool) ) Bool + ((Start Bool) (depth1 Bool) (depth2 Bool) (depth3 Bool) (depth4 Bool) + (depth5 Bool) (depth6 Bool) (depth7 Bool) (depth8 Bool)) ((Start Bool ( (and depth1 depth1) (not depth1) diff --git a/test/regress/regress1/sygus/crcy-si.sy b/test/regress/regress1/sygus/crcy-si.sy index 46500ee4d..1c0abc4fe 100644 --- a/test/regress/regress1/sygus/crcy-si.sy +++ b/test/regress/regress1/sygus/crcy-si.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --sygus-out=status +; COMMAND-LINE: --lang=sygus2 --sygus-out=status (set-logic BV) @@ -8,6 +8,7 @@ ) (synth-fun Imp ((k1 Bool) (k2 Bool) (k3 Bool)) Bool + ((Start Bool) (d1 Bool) (d2 Bool)) ((Start Bool ( (and d1 d1) (or d1 d1) (xor d1 d1) (not d1) ) ) (d1 Bool ( (and d2 d2) (or d2 d2) (xor d2 d2) (not d2) ) ) (d2 Bool ( k1 k2 k3) ) ) diff --git a/test/regress/regress1/sygus/cube-nia.sy b/test/regress/regress1/sygus/cube-nia.sy index da7d98e66..ef57840fe 100644 --- a/test/regress/regress1/sygus/cube-nia.sy +++ b/test/regress/regress1/sygus/cube-nia.sy @@ -1,24 +1,23 @@ ; EXPECT: unsat -; COMMAND-LINE: --sygus-out=status +; COMMAND-LINE: --lang=sygus2 --sygus-out=status (set-logic NIA) (synth-fun cube ((x Int)) Int + ((ntInt Int) (ntBool Bool)) ( - (Start Int (ntInt)) - - (ntBool Bool - ( - (> ntInt ntInt) - (= ntInt ntInt) - ) - ) (ntInt Int (1 x (* ntInt ntInt) (ite ntBool ntInt ntInt) ) ) + (ntBool Bool + ( + (> ntInt ntInt) + (= ntInt ntInt) + ) + ) ) ) diff --git a/test/regress/regress1/sygus/double.sy b/test/regress/regress1/sygus/double.sy index f3fea3122..0ba822278 100644 --- a/test/regress/regress1/sygus/double.sy +++ b/test/regress/regress1/sygus/double.sy @@ -1,12 +1,12 @@ ; EXPECT: unsat
-; COMMAND-LINE: --sygus-out=status
+; COMMAND-LINE: --lang=sygus2 --sygus-out=status
(set-logic SLIA)
(declare-datatype Ex ((Ex2 (ex Int))))
(synth-fun double ((x1 Ex)) Int
+ ((ntInt Int) (ntEx Ex))
(
- (Start Int (ntInt))
(ntInt Int
(
(ex ntEx)
diff --git a/test/regress/regress1/sygus/dt-test-ns.sy b/test/regress/regress1/sygus/dt-test-ns.sy index a6e8ac5c2..3d078cc25 100644 --- a/test/regress/regress1/sygus/dt-test-ns.sy +++ b/test/regress/regress1/sygus/dt-test-ns.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --cegqi-si=all --sygus-out=status +; COMMAND-LINE: --lang=sygus2 --cegqi-si=all --sygus-out=status (set-logic LIA) (declare-datatypes ((List 0)) (((cons (head Int) (tail List)) (nil)))) @@ -11,4 +11,3 @@ (constraint (is-cons (f x))) (constraint (and (= (head (f x)) x) (= (head (f x)) (+ 5 (head (tail (f x))))))) (check-synth) - diff --git a/test/regress/regress1/sygus/dup-op.sy b/test/regress/regress1/sygus/dup-op.sy index e2c69282e..517849b2a 100644 --- a/test/regress/regress1/sygus/dup-op.sy +++ b/test/regress/regress1/sygus/dup-op.sy @@ -1,11 +1,11 @@ ; EXPECT: unsat -; COMMAND-LINE: --cegqi-si=none --sygus-out=status +; COMMAND-LINE: --lang=sygus2 --cegqi-si=none --sygus-out=status (set-logic LIA) (synth-fun f ((x Int)) Int + ((Start Int) (Con Int)) ((Start Int ((+ Con Con) (+ Start Start) x)) (Con Int (0 1)))) (declare-var x Int) (constraint (= (f x) (* 2 x))) (check-synth) - diff --git a/test/regress/regress1/sygus/enum-test.sy b/test/regress/regress1/sygus/enum-test.sy index 7364747fc..55b2eb69e 100644 --- a/test/regress/regress1/sygus/enum-test.sy +++ b/test/regress/regress1/sygus/enum-test.sy @@ -1,9 +1,9 @@ ; EXPECT: unsat -; COMMAND-LINE: --cegqi-si=all --sygus-out=status +; COMMAND-LINE: --lang=sygus2 --cegqi-si=all --sygus-out=status (set-logic LIA) ;; this is the custom enumeration datatype syntax from an early proposal of the sygus standard (define-sort D (Enum (a b))) (define-fun f ((x D)) Int (ite (= x D::a) 3 7)) -(synth-fun g () D ((Start D (D::a D::b)))) +(synth-fun g () D ((Start D)) ((Start D (D::a D::b)))) (constraint (= (f g) 7)) (check-synth) diff --git a/test/regress/regress1/sygus/error1-dt.sy b/test/regress/regress1/sygus/error1-dt.sy index 67f73aded..1ae8cabd9 100644 --- a/test/regress/regress1/sygus/error1-dt.sy +++ b/test/regress/regress1/sygus/error1-dt.sy @@ -1,21 +1,21 @@ ; EXPECT: unsat -; COMMAND-LINE: --sygus-out=status --cegqi-si=none --sygus-active-gen=enum +; COMMAND-LINE: --lang=sygus2 --sygus-out=status --cegqi-si=none --sygus-active-gen=enum (set-logic ALL_SUPPORTED) -(declare-datatypes ((IntRange 0)) +(declare-datatypes ((IntRange 0)) (((IntRange (lower Int) (upper Int))))) -(declare-datatypes ((Loc 0)) +(declare-datatypes ((Loc 0)) (((Loc (x Int) (y Int))))) -(declare-datatypes ((LocRange 0)) +(declare-datatypes ((LocRange 0)) (((LocRange (xD IntRange) (yD IntRange))))) -(declare-datatypes ((Ship 0)) +(declare-datatypes ((Ship 0)) (((Ship (shipCapacity Int) (shipLoc Loc))))) -(declare-datatypes ((ShipRange 0)) +(declare-datatypes ((ShipRange 0)) (((ShipRange (shipCapacityD IntRange) (shipLocD LocRange))))) (define-fun betweenInt ((x Int) (r IntRange)) Bool @@ -61,10 +61,10 @@ (declare-var prior ShipRange) (declare-var response Bool) -(constraint - (=> (betweenShip secret (f secret prior response)) - (= response - (and (atLeast secret) +(constraint + (=> (betweenShip secret (f secret prior response)) + (= response + (and (atLeast secret) (subsetShip (f secret prior response) prior)))) ) diff --git a/test/regress/regress1/sygus/extract.sy b/test/regress/regress1/sygus/extract.sy index d1541fa87..f3cfa09a2 100644 --- a/test/regress/regress1/sygus/extract.sy +++ b/test/regress/regress1/sygus/extract.sy @@ -1,18 +1,19 @@ ; EXPECT: unsat
-; COMMAND-LINE: --sygus-out=status
+; COMMAND-LINE: --lang=sygus2 --sygus-out=status
(set-logic ALL_SUPPORTED)
(declare-datatype Ex ((Ex2 (ex Int))))
(synth-fun ident ((x1 Ex)) Int
+ ((Start Int) (ntInt Int) (ntEx Ex))
(
(Start Int (ntInt))
(ntInt Int
(
(ex ntEx)
- )
+ )
)
- (ntEx Ex ( x1 ) )
+ (ntEx Ex ( x1 ))
)
)
(constraint (= (ident (Ex2 1)) 1))
diff --git a/test/regress/regress1/sygus/fg_polynomial3.sy b/test/regress/regress1/sygus/fg_polynomial3.sy index d70516bf1..2da3809a8 100644 --- a/test/regress/regress1/sygus/fg_polynomial3.sy +++ b/test/regress/regress1/sygus/fg_polynomial3.sy @@ -1,13 +1,11 @@ ; EXPECT: unsat -; COMMAND-LINE: --sygus-out=status +; COMMAND-LINE: --lang=sygus2 --sygus-out=status (set-logic LIA) -(synth-fun addExpr1 ((x Int) (y Int)) Int -) +(synth-fun addExpr1 ((x Int) (y Int)) Int) -(synth-fun addExpr2 ((x Int) (y Int)) Int -) +(synth-fun addExpr2 ((x Int) (y Int)) Int) (declare-var x Int) (declare-var y Int) @@ -15,4 +13,3 @@ (constraint (= (+ (addExpr1 x y) (addExpr2 y x)) (- x (+ x y)))) (check-synth) - diff --git a/test/regress/regress1/sygus/find_sc_bvult_bvnot.sy b/test/regress/regress1/sygus/find_sc_bvult_bvnot.sy index efec0e0e7..145064141 100644 --- a/test/regress/regress1/sygus/find_sc_bvult_bvnot.sy +++ b/test/regress/regress1/sygus/find_sc_bvult_bvnot.sy @@ -1,11 +1,12 @@ ; EXPECT: unsat -; COMMAND-LINE: --sygus-out=status -; COMMAND-LINE: --sygus-out=status --cegis-sample=trust --no-check-synth-sol +; COMMAND-LINE: --lang=sygus2 --sygus-out=status +; COMMAND-LINE: --lang=sygus2 --sygus-out=status --cegis-sample=trust --no-check-synth-sol (set-logic BV) ; we test --cegis-sample=trust since we can exhaustively sample BV4 -(synth-fun SC ((s (BitVec 4)) (t (BitVec 4))) Bool +(synth-fun SC ((s (_ BitVec 4)) (t (_ BitVec 4))) Bool + ((Start Bool) (StartBv (_ BitVec 4))) ((Start Bool ( true false @@ -19,7 +20,7 @@ (bvuge StartBv StartBv) (bvsge StartBv StartBv) )) - (StartBv (BitVec 4) ( + (StartBv (_ BitVec 4) ( s t #x0 @@ -36,15 +37,15 @@ )) )) -(declare-var s (BitVec 4)) -(declare-var t (BitVec 4)) +(declare-var s (_ BitVec 4)) +(declare-var t (_ BitVec 4)) (define-fun udivtotal ((a (_ BitVec 4)) (b (_ BitVec 4))) (_ BitVec 4) (ite (= b #x0) #xF (bvudiv a b)) ) (define-fun uremtotal ((a (_ BitVec 4)) (b (_ BitVec 4))) (_ BitVec 4) (ite (= b #x0) a (bvurem a b)) ) -(define-fun case ((x (BitVec 4)) (s (BitVec 4)) (t (BitVec 4))) Bool +(define-fun case ((x (_ BitVec 4)) (s (_ BitVec 4)) (t (_ BitVec 4))) Bool (bvult (bvnot x) t) ) (constraint diff --git a/test/regress/regress1/sygus/hd-01-d1-prog.sy b/test/regress/regress1/sygus/hd-01-d1-prog.sy index bbdbda1bd..9a28d6d79 100644 --- a/test/regress/regress1/sygus/hd-01-d1-prog.sy +++ b/test/regress/regress1/sygus/hd-01-d1-prog.sy @@ -1,22 +1,23 @@ ; EXPECT: unsat -; COMMAND-LINE: --sygus-out=status +; COMMAND-LINE: --lang=sygus2 --sygus-out=status (set-logic BV) -(define-fun hd01 ((x (BitVec 32))) (BitVec 32) (bvand x (bvsub x #x00000001))) +(define-fun hd01 ((x (_ BitVec 32))) (_ BitVec 32) (bvand x (bvsub x #x00000001))) -(synth-fun f ((x (BitVec 32))) (BitVec 32) - ((Start (BitVec 32) ((bvand Start Start) - (bvsub Start Start) - (bvor Start Start) - (bvadd Start Start) - (bvxor Start Start) - x - #x00000000 - #xFFFFFFFF - #x00000001)))) +(synth-fun f ((x (_ BitVec 32))) (_ BitVec 32) + ((Start (_ BitVec 32))) + ((Start (_ BitVec 32) ( + (bvand Start Start) + (bvsub Start Start) + (bvor Start Start) + (bvadd Start Start) + (bvxor Start Start) + x + #x00000000 + #xFFFFFFFF + #x00000001)))) -(declare-var x (BitVec 32)) +(declare-var x (_ BitVec 32)) (constraint (= (hd01 x) (f x))) (check-synth) - diff --git a/test/regress/regress1/sygus/hd-sdiv.sy b/test/regress/regress1/sygus/hd-sdiv.sy index 37e1daf88..c4c90c6f6 100644 --- a/test/regress/regress1/sygus/hd-sdiv.sy +++ b/test/regress/regress1/sygus/hd-sdiv.sy @@ -1,16 +1,16 @@ ; EXPECT: unsat -; COMMAND-LINE: --cegqi-si=none --sygus-out=status +; COMMAND-LINE: --lang=sygus2 --cegqi-si=none --sygus-out=status (set-logic BV) -(define-fun hd01 ((x (BitVec 32))) (BitVec 32) (bvand x #x00000001)) +(define-fun hd01 ((x (_ BitVec 32))) (_ BitVec 32) (bvand x #x00000001)) -(synth-fun f ((x (BitVec 32))) (BitVec 32) - ((Start (BitVec 32) ((bvsdiv Start Start) - (bvand Start Start) +(synth-fun f ((x (_ BitVec 32))) (_ BitVec 32) + ((Start (_ BitVec 32))) + ((Start (_ BitVec 32) ((bvsdiv Start Start) + (bvand Start Start) x #x00000001)))) -(declare-var y (BitVec 32)) +(declare-var y (_ BitVec 32)) (constraint (= (hd01 y) (f y))) (check-synth) - diff --git a/test/regress/regress1/sygus/ho-sygus.sy b/test/regress/regress1/sygus/ho-sygus.sy index c66485817..893c2034e 100644 --- a/test/regress/regress1/sygus/ho-sygus.sy +++ b/test/regress/regress1/sygus/ho-sygus.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --sygus-out=status --uf-ho +; COMMAND-LINE: --lang=sygus2 --sygus-out=status --uf-ho (set-logic ALL) (synth-fun f ((y (-> Int Int)) (z Int)) Int) (declare-var z (-> Int Int)) diff --git a/test/regress/regress1/sygus/icfp_14.12-flip-args.sy b/test/regress/regress1/sygus/icfp_14.12-flip-args.sy index a1e93cc44..96851045c 100644 --- a/test/regress/regress1/sygus/icfp_14.12-flip-args.sy +++ b/test/regress/regress1/sygus/icfp_14.12-flip-args.sy @@ -1,28 +1,26 @@ ; 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 ((y (BitVec 64)) (x (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 ((y (_ BitVec 64)) (x (_ BitVec 64)) (z (_ BitVec 64))) (_ BitVec 64) (ite (= x #x0000000000000001) y z)) -(synth-fun f ( (x (BitVec 64))) (BitVec 64) -( - -(Start (BitVec 64) (#x0000000000000000 #x0000000000000001 x (bvnot Start) - (shl1 Start) - (shr1 Start) - (shr4 Start) - (shr16 Start) - (bvand Start Start) - (bvor Start Start) - (bvxor Start Start) - (bvadd Start Start) - (if0 Start Start Start) - )) -) +(synth-fun f ( (x (_ BitVec 64))) (_ BitVec 64) +((Start (_ BitVec 64))) +((Start (_ BitVec 64) (#x0000000000000000 #x0000000000000001 x (bvnot Start) + (shl1 Start) + (shr1 Start) + (shr4 Start) + (shr16 Start) + (bvand Start Start) + (bvor Start Start) + (bvxor Start Start) + (bvadd Start Start) + (if0 Start Start Start) +))) ) (constraint (= (f #x6E393354DFFAAB51) #xC8E366559002AA57)) (constraint (= (f #xFDA75AD598A27135) #x812C529533AEC765)) diff --git a/test/regress/regress1/sygus/icfp_14.12.sy b/test/regress/regress1/sygus/icfp_14.12.sy index 51b86f0f5..6f76346d5 100644 --- a/test/regress/regress1/sygus/icfp_14.12.sy +++ b/test/regress/regress1/sygus/icfp_14.12.sy @@ -1,28 +1,26 @@ ; 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) -( - -(Start (BitVec 64) (#x0000000000000000 #x0000000000000001 x (bvnot Start) - (shl1 Start) - (shr1 Start) - (shr4 Start) - (shr16 Start) - (bvand Start Start) - (bvor Start Start) - (bvxor Start Start) - (bvadd Start Start) - (if0 Start Start Start) - )) -) +(synth-fun f ( (x (_ BitVec 64))) (_ BitVec 64) +((Start (_ BitVec 64))) +((Start (_ BitVec 64) (#x0000000000000000 #x0000000000000001 x (bvnot Start) + (shl1 Start) + (shr1 Start) + (shr4 Start) + (shr16 Start) + (bvand Start Start) + (bvor Start Start) + (bvxor Start Start) + (bvadd Start Start) + (if0 Start Start Start) +))) ) (constraint (= (f #x6E393354DFFAAB51) #xC8E366559002AA57)) (constraint (= (f #xFDA75AD598A27135) #x812C529533AEC765)) diff --git a/test/regress/regress1/sygus/icfp_14_12_diff_types.sy b/test/regress/regress1/sygus/icfp_14_12_diff_types.sy index f83277757..212943cab 100644 --- a/test/regress/regress1/sygus/icfp_14_12_diff_types.sy +++ b/test/regress/regress1/sygus/icfp_14_12_diff_types.sy @@ -1,23 +1,21 @@ ; EXPECT: unsat -; COMMAND-LINE: --sygus-out=status +; COMMAND-LINE: --lang=sygus2 --sygus-out=status (set-logic BV) -(define-fun if0 ((x (BitVec 64)) (y (BitVec 64)) (z (BitVec 64))) (BitVec 64) (ite (= x #x0000000000000001) y z)) +(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) - (bvand Start Start) - (bvor Start Start) - (bvxor Start Start) - (bvadd Start Start) - (if0 Start Start2 Start2) - (ite StartBool Start Start2) +(synth-fun f ( (x (_ BitVec 64))) (_ BitVec 64) +((Start (_ BitVec 64)) (Start2 (_ BitVec 64)) (StartBool Bool)) +((Start (_ BitVec 64) (#x0000000000000000 #x0000000000000001 x (bvnot Start) + (bvand Start Start) + (bvor Start Start) + (bvxor Start Start) + (bvadd Start Start) + (if0 Start Start2 Start2) + (ite StartBool Start Start2) )) -(Start2 (BitVec 64) (#x0000000000000000 #x0000000000000002)) -(StartBool Bool ((= Start Start))) -) + (Start2 (_ BitVec 64) (#x0000000000000000 #x0000000000000002)) + (StartBool Bool ((= Start Start)))) ) (constraint (= (f #x0000000000000001) #x0000000000000001)) (constraint (= (f #x1ED2E25068744C80) #x0000000000000000)) diff --git a/test/regress/regress1/sygus/icfp_28_10.sy b/test/regress/regress1/sygus/icfp_28_10.sy index 212ae37f5..4ca73b87f 100644 --- a/test/regress/regress1/sygus/icfp_28_10.sy +++ b/test/regress/regress1/sygus/icfp_28_10.sy @@ -1,19 +1,18 @@ ; 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) -( - -(Start (BitVec 64) (#x0000000000000000 #x0000000000000001 x (bvnot Start) - (shl1 Start) +(synth-fun f ( (x (_ BitVec 64))) (_ BitVec 64) +((Start (_ BitVec 64))) +((Start (_ BitVec 64) (#x0000000000000000 #x0000000000000001 x (bvnot Start) + (shl1 Start) (shr1 Start) (shr4 Start) (shr16 Start) @@ -21,8 +20,7 @@ (bvor Start Start) (bvxor Start Start) (bvadd Start Start) - (if0 Start Start Start) - )) + (if0 Start Start Start))) ) ) diff --git a/test/regress/regress1/sygus/icfp_easy-ite.sy b/test/regress/regress1/sygus/icfp_easy-ite.sy index f0cbbdc53..63cc4736c 100644 --- a/test/regress/regress1/sygus/icfp_easy-ite.sy +++ b/test/regress/regress1/sygus/icfp_easy-ite.sy @@ -1,28 +1,27 @@ ; 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) -( - -(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) +(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) )) -(StartBool Bool ((= Start #x0000000000000001))) + (StartBool Bool ((= Start #x0000000000000001))) ) ) (constraint (= (f #x0000000000000001) #x0000000000000001)) diff --git a/test/regress/regress1/sygus/int-any-const.sy b/test/regress/regress1/sygus/int-any-const.sy index b5de57533..18e7ed06e 100644 --- a/test/regress/regress1/sygus/int-any-const.sy +++ b/test/regress/regress1/sygus/int-any-const.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --sygus-out=status --no-sygus-pbe --cegqi-si=none --sygus-grammar-cons=any-term-concise +; COMMAND-LINE: --lang=sygus2 --sygus-out=status --no-sygus-pbe --cegqi-si=none --sygus-grammar-cons=any-term-concise (set-logic LIA) (synth-fun f ((x Int) (y Int)) Int) diff --git a/test/regress/regress1/sygus/inv-example.sy b/test/regress/regress1/sygus/inv-example.sy index ff68bc06c..bcc6c0aa8 100644 --- a/test/regress/regress1/sygus/inv-example.sy +++ b/test/regress/regress1/sygus/inv-example.sy @@ -1,10 +1,7 @@ ; EXPECT: unsat -; COMMAND-LINE: --sygus-out=status +; COMMAND-LINE: --lang=sygus2 --sygus-out=status (set-logic LIA) (synth-inv inv-f ((x Int) (y Int) (b Bool))) -(declare-primed-var x Int) -(declare-primed-var y Int) -(declare-primed-var b Bool) (define-fun pre-f ((x Int) (y Int) (b Bool)) Bool (and (and (>= x 5) (<= x 9)) (and (>= y 1) (<= y 3)))) (define-fun trans-f ((x Int) (y Int) (b Bool) (x! Int) (y! Int) (b! Bool)) Bool (and (and (= b! b) (= y! x)) (ite b (= x! (+ x 10)) (= x! (+ x 12))))) (define-fun post-f ((x Int) (y Int) (b Bool)) Bool (<= y x)) diff --git a/test/regress/regress1/sygus/inv-missed-sol-true.sy b/test/regress/regress1/sygus/inv-missed-sol-true.sy index b04022766..f8a3136f2 100644 --- a/test/regress/regress1/sygus/inv-missed-sol-true.sy +++ b/test/regress/regress1/sygus/inv-missed-sol-true.sy @@ -1,12 +1,9 @@ ; EXPECT: unsat -; COMMAND-LINE: --sygus-out=status +; COMMAND-LINE: --lang=sygus2 --sygus-out=status (set-logic LIA) (synth-inv inv-f ((x Int) (z Int))) -(declare-primed-var x Int) -(declare-primed-var z Int) - (define-fun pre-f ((x Int) (z Int)) Bool (and (> x (- 0 100)) (< x 200) (> z 100) (< z 200))) @@ -22,4 +19,4 @@ (inv-constraint inv-f pre-f trans-f post-f) -(check-synth)
\ No newline at end of file +(check-synth) diff --git a/test/regress/regress1/sygus/inv-unused.sy b/test/regress/regress1/sygus/inv-unused.sy index 91ba95d39..a5eb41b26 100644 --- a/test/regress/regress1/sygus/inv-unused.sy +++ b/test/regress/regress1/sygus/inv-unused.sy @@ -1,10 +1,7 @@ ; EXPECT: unsat -; COMMAND-LINE: --sygus-out=status +; COMMAND-LINE: --lang=sygus2 --sygus-out=status (set-logic LIA) (synth-inv inv-f ((x Int) (y Int) (b Bool))) -(declare-primed-var x Int) -(declare-primed-var y Int) -(declare-primed-var b Bool) (define-fun pre-f ((x Int) (y Int) (b Bool)) Bool (and (>= x 5) (<= x 9))) (define-fun trans-f ((x Int) (y Int) (b Bool) (x! Int) (y! Int) (b! Bool)) Bool (= x! (+ x 1))) (define-fun post-f ((x Int) (y Int) (b Bool)) Bool (> x 0)) diff --git a/test/regress/regress1/sygus/inv_gen_fig8.sy b/test/regress/regress1/sygus/inv_gen_fig8.sy index 19c36e4dc..5c1aa4852 100644 --- a/test/regress/regress1/sygus/inv_gen_fig8.sy +++ b/test/regress/regress1/sygus/inv_gen_fig8.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --sygus-out=status +; COMMAND-LINE: --lang=sygus2 --sygus-out=status (set-logic LIA) (synth-fun inv ((l Int)) Bool ( @@ -8,9 +8,9 @@ (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 (l)) - (Const Int (-3 -2 -1 0 1 2 3)) + (Const Int ((- 3) (- 2) (- 1) 0 1 2 3)) ) ) @@ -36,11 +36,11 @@ (declare-var x4p Int) (constraint (implies (and6 (= l 0) (or (= x0p (+ x0 1)) (= x0p (- x0 1))) - (or (= x1p (+ x1 1)) (= x1p (- x1 1))) - (or (= x2p (+ x2 1)) (= x2p (- x2 1))) - (or (= x3p (+ x3 1)) (= x3p (- x3 1))) - (or (= x4p (+ x4 1)) (= x4p (- x4 1)))) - (inv l))) + (or (= x1p (+ x1 1)) (= x1p (- x1 1))) + (or (= x2p (+ x2 1)) (= x2p (- x2 1))) + (or (= x3p (+ x3 1)) (= x3p (- x3 1))) + (or (= x4p (+ x4 1)) (= x4p (- x4 1)))) + (inv l))) (constraint (implies (and (inv l) (not (= l 0))) false)) (check-synth) diff --git a/test/regress/regress1/sygus/issue2914.sy b/test/regress/regress1/sygus/issue2914.sy index 0f125a870..71a5a5987 100644 --- a/test/regress/regress1/sygus/issue2914.sy +++ b/test/regress/regress1/sygus/issue2914.sy @@ -1,18 +1,12 @@ ; EXPECT: unsat -; COMMAND-LINE: --sygus-out=status +; COMMAND-LINE: --lang=sygus2 --sygus-out=status (set-logic SLIA) -(declare-datatype JSIdentifier ((JSString (jsString String)) (Error ))) -(synth-fun substring ((x1 String) (x3 Int))String - ((Start String (ntString)) - (ntInt Int - (0 x3) - ) - (ntJSIdentifier JSIdentifier - ( - Error - ) - ) +(declare-datatype JSIdentifier ((JSString (jsString String)) (Error))) + +(synth-fun substring ((x1 String) (x3 Int)) String + ((ntString String) (ntInt Int) (ntJSIdentifier JSIdentifier)) + ( (ntString String (x1 (str.substr ntString ntInt ntInt) @@ -20,7 +14,16 @@ (str.++ ntString ntString) ) ) + (ntInt Int + (0 x3) + ) + (ntJSIdentifier JSIdentifier + ( + Error + ) + ) ) ) + (constraint (= (substring "ey" 1) "e")) (check-synth) diff --git a/test/regress/regress1/sygus/issue2935.sy b/test/regress/regress1/sygus/issue2935.sy index 5616d19f5..ea8011a5e 100644 --- a/test/regress/regress1/sygus/issue2935.sy +++ b/test/regress/regress1/sygus/issue2935.sy @@ -1,10 +1,18 @@ ; EXPECT: unsat -; COMMAND-LINE: --sygus-out=status +; COMMAND-LINE: --lang=sygus2 --sygus-out=status (set-logic SLIA) -(declare-datatype JSIdentifier ((JSInt (jsInt Int)) (JSString (jsString String)) )) + +(declare-datatype JSIdentifier ((JSInt (jsInt Int)) (JSString (jsString String)))) (synth-fun f ((x1_ JSIdentifier)(x2_ String)) JSIdentifier - ((Start JSIdentifier (ntJSIdentifier)) + ((ntJSIdentifier JSIdentifier) (ntInt Int) (ntString String) (ntBool Bool)) + ( + (ntJSIdentifier JSIdentifier + (x1_ + (ite ntBool ntJSIdentifier ntJSIdentifier) + (JSString ntString) + ) + ) (ntInt Int (1 (+ ntInt ntInt) @@ -18,19 +26,15 @@ ) ) (ntBool Bool - ( + ( (= ntString ntString) ) ) - (ntJSIdentifier JSIdentifier - ( x1_ - (ite ntBool ntJSIdentifier ntJSIdentifier) - (JSString ntString) - ) - ) ) ) + (constraint (= (f (JSString "") "") (JSString ""))) (constraint (= (f (JSString "M") "W") (JSString "M"))) (constraint (= (f (JSString "Moon") "") (JSString "on"))) + (check-synth) diff --git a/test/regress/regress1/sygus/issue3320-quant.sy b/test/regress/regress1/sygus/issue3320-quant.sy index a7b76182e..2d99ba5cf 100644 --- a/test/regress/regress1/sygus/issue3320-quant.sy +++ b/test/regress/regress1/sygus/issue3320-quant.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --sygus-out=status +; COMMAND-LINE: --lang=sygus2 --sygus-out=status (set-logic LIA) (declare-var x Int) (declare-var y Int) diff --git a/test/regress/regress1/sygus/issue3649.sy b/test/regress/regress1/sygus/issue3649.sy index 12949c55a..b650c4ca6 100644 --- a/test/regress/regress1/sygus/issue3649.sy +++ b/test/regress/regress1/sygus/issue3649.sy @@ -1,5 +1,5 @@ ; EXPECT: unknown -; COMMAND-LINE: --sygus-out=status +; COMMAND-LINE: --lang=sygus2 --sygus-out=status (set-logic ALL) (synth-fun inv-fn ((i Int) (x (Array Int Int)) (c Int)) Bool) @@ -18,7 +18,6 @@ (declare-var i! Int) (declare-var c Int) - (constraint (=> (init-fn i x c) (inv-fn i x c))) (constraint (=> (inv-fn i x c) (post-fn i x c))) (check-synth) diff --git a/test/regress/regress1/sygus/large-const-simp.sy b/test/regress/regress1/sygus/large-const-simp.sy index 31f660b2a..d93644197 100644 --- a/test/regress/regress1/sygus/large-const-simp.sy +++ b/test/regress/regress1/sygus/large-const-simp.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --cegqi-si=none --sygus-out=status --sygus-add-const-grammar +; COMMAND-LINE: --lang=sygus2 --cegqi-si=none --sygus-out=status --sygus-add-const-grammar (set-logic LIA) (synth-fun lc ((x Int)) Int) diff --git a/test/regress/regress1/sygus/let-bug-simp.sy b/test/regress/regress1/sygus/let-bug-simp.sy index 5c2dccff0..1f383ab43 100644 --- a/test/regress/regress1/sygus/let-bug-simp.sy +++ b/test/regress/regress1/sygus/let-bug-simp.sy @@ -1,15 +1,19 @@ ; EXPECT: unsat -; COMMAND-LINE: --sygus-out=status +; COMMAND-LINE: --lang=sygus2 --sygus-out=status (set-logic LIA) -(define-fun letf ((z Int) (v1 Int) (v2 Int)) Bool - (or - (= v1 z) +(define-fun letf ((z Int) (v1 Int) (v2 Int)) Bool + (or + (= v1 z) (= v2 z))) (synth-fun f ((x0 Int) (x1 Int)) Bool +((Start Bool) (StartInt Int) (IntVar Int)) ( - (StartInt Int (5)) + (Start Bool ( (letf StartInt IntVar IntVar) )) - (Start Bool ( (letf StartInt (Variable Int) (Variable Int)) )) + (StartInt Int (5)) + + ; "Hack" to avoid parse errors in V2 format. + (IntVar Int ((Variable Int))) ) ) diff --git a/test/regress/regress1/sygus/list-head-x.sy b/test/regress/regress1/sygus/list-head-x.sy index 6c5c1a97b..83ac8290d 100644 --- a/test/regress/regress1/sygus/list-head-x.sy +++ b/test/regress/regress1/sygus/list-head-x.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --cegqi-si=all --sygus-out=status +; COMMAND-LINE: --lang=sygus2 --cegqi-si=all --sygus-out=status (set-logic ALL_SUPPORTED) (declare-datatypes ((List 0)) (((cons (head Int) (tail List)) (nil)))) diff --git a/test/regress/regress1/sygus/logiccell_help.sy b/test/regress/regress1/sygus/logiccell_help.sy index 1ba05e648..d6e8a75a4 100644 --- a/test/regress/regress1/sygus/logiccell_help.sy +++ b/test/regress/regress1/sygus/logiccell_help.sy @@ -1,119 +1,118 @@ ; EXPECT: unsat -; COMMAND-LINE: --sygus-out=status --sygus-repair-const +; COMMAND-LINE: --lang=sygus2 --sygus-out=status --sygus-repair-const (set-logic BV) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ; Utils ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -(define-sort Bit () (BitVec 1)) +(define-sort Bit () (_ BitVec 1)) -(define-fun bit2bool ((b Bit)) Bool +(define-fun bit2bool ((b Bit)) Bool (= b #b1) ) -(define-fun extend ((i (BitVec 4))) (BitVec 16) +(define-fun extend ((i (_ BitVec 4))) (_ BitVec 16) (concat #b000000000000 i) ) -(define-fun extractBit ((i (BitVec 4)) (x (BitVec 16))) Bit - ((_ extract 0 0) (bvlshr x (extend i))) +(define-fun extractBit ((i (_ BitVec 4)) (x (_ BitVec 16))) Bit + ((_ extract 0 0) (bvlshr x (extend i))) ) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ; Arch ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -(define-fun lut4 ((i0 Bit) (i1 Bit) (i2 Bit) (i3 Bit) (lut_val (BitVec 16))) Bit +(define-fun lut4 ((i0 Bit) (i1 Bit) (i2 Bit) (i3 Bit) (lut_val (_ BitVec 16))) Bit (extractBit (concat i0 i1 i2 i3) lut_val) ) (define-fun carry ((i0 Bit) (i1 Bit) (ci Bit)) Bit - (bvor (bvand i0 i1) (bvand i0 ci) (bvand i1 ci)) + (bvor (bvand i0 i1) (bvand i0 ci) (bvand i1 ci)) ) (define-fun mux2 ((s Bit) (i0 Bit) (i1 Bit)) Bit ;(ite (bit2bool s) i0 i1) - (bvor (bvand s i0) (bvand (bvnot s) i1)) + (bvor (bvand s i0) (bvand (bvnot s) i1)) ) (define-fun logic-cell ( - (i0 Bit) (i1 Bit) (i2 Bit) (i3 Bit) (c_in Bit) ; inputs - (s Bit) (lut_val (BitVec 16)) ;configs - ) (BitVec 2) ; Cout O - (let ( - (c_out Bit (carry i1 i2 c_in)) - (l_out Bit (lut4 i0 i1 i2 (mux2 s i3 c_in) lut_val)) - ) - (concat c_out l_out) + (i0 Bit) (i1 Bit) (i2 Bit) (i3 Bit) (c_in Bit) ; inputs + (s Bit) (lut_val (_ BitVec 16)) ;configs + ) (_ BitVec 2) ; Cout O + (let ( + (c_out (carry i1 i2 c_in)) + (l_out (lut4 i0 i1 i2 (mux2 s i3 c_in) lut_val)) + ) + (concat c_out l_out) )) (define-fun plb2 ( - (i_0_0 Bit) (i_0_1 Bit) (i_0_2 Bit) (i_0_3 Bit) - (i_1_0 Bit) (i_1_1 Bit) (i_1_2 Bit) (i_1_3 Bit) - (c_in Bit) - (s_0 Bit) (lut_val_0 (BitVec 16)) ;configs - (s_1 Bit) (lut_val_1 (BitVec 16)) ;configs - ) (BitVec 3) - (let ((lc0 (BitVec 2) (logic-cell i_0_0 i_0_1 i_0_2 i_0_3 c_in s_0 lut_val_0))) - (let ((lc1 (BitVec 2) (logic-cell i_1_0 i_1_1 i_1_2 i_1_3 ((_ extract 1 1) lc0) s_1 lut_val_1))) - (concat lc1 ((_ extract 0 0) lc0)) - )) + (i_0_0 Bit) (i_0_1 Bit) (i_0_2 Bit) (i_0_3 Bit) + (i_1_0 Bit) (i_1_1 Bit) (i_1_2 Bit) (i_1_3 Bit) + (c_in Bit) + (s_0 Bit) (lut_val_0 (_ BitVec 16)) ;configs + (s_1 Bit) (lut_val_1 (_ BitVec 16)) ;configs + ) (_ BitVec 3) + (let ((lc0 (logic-cell i_0_0 i_0_1 i_0_2 i_0_3 c_in s_0 lut_val_0))) + (let ((lc1 (logic-cell i_1_0 i_1_1 i_1_2 i_1_3 ((_ extract 1 1) lc0) s_1 lut_val_1))) + (concat lc1 ((_ extract 0 0) lc0)) + )) ) - ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ; synth ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -(define-fun extract2 ((i (BitVec 1)) (x (BitVec 2))) Bit - ((_ extract 0 0) (bvlshr x (concat #b0 i))) +(define-fun extract2 ((i (_ BitVec 1)) (x (_ BitVec 2))) Bit + ((_ extract 0 0) (bvlshr x (concat #b0 i))) ) -(synth-fun f ((x (BitVec 2)) (y (BitVec 2)) (c_in Bit)) (BitVec 3) ( - (Start (BitVec 3) ( - (plb2 #b0 (extract2 #b0 x) (extract2 #b0 y) #b0 - #b0 (extract2 #b1 x) (extract2 #b1 y) #b0 - Cin - S LUT_VAL - S LUT_VAL) - )) - (Cin Bit ( - c_in - (Constant Bit) - )) - (S Bit ( - (Constant Bit) - )) - (LUT_VAL (BitVec 16) ( - (Constant (BitVec 16)) - )) +(synth-fun f ((x (_ BitVec 2)) (y (_ BitVec 2)) (c_in Bit)) (_ BitVec 3) + ((Start (_ BitVec 3)) (Cin Bit) (S Bit) (LUT_VAL (_ BitVec 16))) ( + (Start (_ BitVec 3) ( + (plb2 #b0 (extract2 #b0 x) (extract2 #b0 y) #b0 + #b0 (extract2 #b1 x) (extract2 #b1 y) #b0 + Cin + S LUT_VAL + S LUT_VAL) + )) + (Cin Bit ( + c_in + (Constant Bit) + )) + (S Bit ( + (Constant Bit) + )) + (LUT_VAL (_ BitVec 16) ( + (Constant (_ BitVec 16)) + )) )) -(declare-var x (BitVec 2)) -(declare-var y (BitVec 2)) +(declare-var x (_ BitVec 2)) +(declare-var y (_ BitVec 2)) -(constraint (= - (bvadd (concat #b0 x) (concat #b0 y)) - (f x y #b0) +(constraint (= + (bvadd (concat #b0 x) (concat #b0 y)) + (f x y #b0) )) -(constraint (= - (bvadd (bvadd (concat #b0 x) (concat #b0 y)) #b001) - (f x y #b1) +(constraint (= + (bvadd (bvadd (concat #b0 x) (concat #b0 y)) #b001) + (f x y #b1) )) - (check-synth) - -;(define-fun lut4_ite ((I0 Bit) (I1 Bit) (I2 Bit) (I3 Bit) (LUT_VAL (BitVec 16))) Bit -; (let ((s3 (BitVec 8) (ite (bit2bool I3) ((_ extract 15 8) LUT_VAL) ((_ extract 7 0) LUT_VAL)))) -; (let ((s2 (BitVec 4) (ite (bit2bool I2) ((_ extract 7 4) s3) ((_ extract 3 0) s3)))) -; (let ((s1 (BitVec 2) (ite (bit2bool I1) ((_ extract 3 2) s2) ((_ extract 1 0) s2)))) -; (let ((s0 (BitVec 1) (ite (bit2bool I0) ((_ extract 1 1) s1) ((_ extract 0 0) s1)))) -; s0 -; ) -; ) -; ) -; ) + +;(define-fun lut4_ite ((I0 Bit) (I1 Bit) (I2 Bit) (I3 Bit) (LUT_VAL (_ BitVec 16))) Bit +; (let ((s3 (_ BitVec 8) (ite (bit2bool I3) ((_ extract 15 8) LUT_VAL) ((_ extract 7 0) LUT_VAL)))) +; (let ((s2 (ite (bit2bool I2) ((_ extract 7 4) s3) ((_ extract 3 0) s3)))) +; (let ((s1 (ite (bit2bool I1) ((_ extract 3 2) s2) ((_ extract 1 0) s2)))) +; (let ((s0 (ite (bit2bool I0) ((_ extract 1 1) s1) ((_ extract 0 0) s1)))) +; s0 +; ) +; ) +; ) +; ) ;) diff --git a/test/regress/regress1/sygus/max2-bv.sy b/test/regress/regress1/sygus/max2-bv.sy index 297bd9179..fa98ef26b 100644 --- a/test/regress/regress1/sygus/max2-bv.sy +++ b/test/regress/regress1/sygus/max2-bv.sy @@ -1,26 +1,17 @@ ; EXPECT: unsat -; COMMAND-LINE: --sygus-out=status +; COMMAND-LINE: --lang=sygus2 --sygus-out=status (set-logic BV) -(synth-fun max2 ((x (BitVec 32))(y (BitVec 32))) (BitVec 32) -) +(synth-fun max2 ((x (_ BitVec 32)) (y (_ BitVec 32))) (_ BitVec 32)) -(declare-var x (BitVec 32)) +(declare-var x (_ BitVec 32)) -(declare-var y (BitVec 32)) +(declare-var y (_ BitVec 32)) -(constraint -(bvuge (max2 x y) x) -) +(constraint (bvuge (max2 x y) x)) -(constraint -(bvuge (max2 x y) y) -) +(constraint (bvuge (max2 x y) y)) -(constraint -(or (= x (max2 x y)) (= y (max2 x y))) -) +(constraint (or (= x (max2 x y)) (= y (max2 x y)))) (check-synth) - - diff --git a/test/regress/regress1/sygus/multi-fun-polynomial2.sy b/test/regress/regress1/sygus/multi-fun-polynomial2.sy index 22a2e0a4b..a20bf853d 100644 --- a/test/regress/regress1/sygus/multi-fun-polynomial2.sy +++ b/test/regress/regress1/sygus/multi-fun-polynomial2.sy @@ -1,27 +1,29 @@ ; EXPECT: unsat -; COMMAND-LINE: --sygus-out=status +; COMMAND-LINE: --lang=sygus2 --sygus-out=status (set-logic LIA) (synth-fun addExpr1 ((x Int) (y Int)) Int + ((Start Int)) ((Start Int (x y - 0 - 1 + 0 + 1 (+ Start Start) (- Start Start) )) - )) + )) (synth-fun addExpr2 ((x Int) (y Int)) Int +((Start Int)) ((Start Int (x y - 0 - 1 + 0 + 1 (+ Start Start) (- Start Start) )) - )) + )) (declare-var x Int) diff --git a/test/regress/regress1/sygus/nflat-fwd-3.sy b/test/regress/regress1/sygus/nflat-fwd-3.sy index a1776cf93..f9b6708d5 100644 --- a/test/regress/regress1/sygus/nflat-fwd-3.sy +++ b/test/regress/regress1/sygus/nflat-fwd-3.sy @@ -1,11 +1,11 @@ ; 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) (Con Int)) ((Start Int ((+ (+ Con Con) Con) x)) (Con Int (0 1)))) (declare-var x Int) (constraint (= (f x) 2)) (check-synth) - diff --git a/test/regress/regress1/sygus/nflat-fwd.sy b/test/regress/regress1/sygus/nflat-fwd.sy index da26a6c93..c36232a5d 100644 --- a/test/regress/regress1/sygus/nflat-fwd.sy +++ b/test/regress/regress1/sygus/nflat-fwd.sy @@ -1,11 +1,11 @@ ; 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) (Con Int)) ((Start Int ((+ Con Con) (+ (+ Start Start) Con) x)) (Con Int (0 1)))) (declare-var x Int) (constraint (= (f x) (* 2 x))) (check-synth) - diff --git a/test/regress/regress1/sygus/nia-max-square-ns.sy b/test/regress/regress1/sygus/nia-max-square-ns.sy index 6e7f70ff0..5d63ab023 100644 --- a/test/regress/regress1/sygus/nia-max-square-ns.sy +++ b/test/regress/regress1/sygus/nia-max-square-ns.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --cegqi-si=all --sygus-out=status --nl-ext-tplanes +; COMMAND-LINE: --lang=sygus2 --cegqi-si=all --sygus-out=status --nl-ext-tplanes (set-logic NIA) (synth-fun max ((x Int) (y Int)) Int) diff --git a/test/regress/regress1/sygus/no-flat-simp.sy b/test/regress/regress1/sygus/no-flat-simp.sy index c0f0e4c0f..42b73394b 100644 --- a/test/regress/regress1/sygus/no-flat-simp.sy +++ b/test/regress/regress1/sygus/no-flat-simp.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) (y Int)) Int + ((Start Int)) ((Start Int (x y 0 @@ -15,6 +16,4 @@ (constraint (= (f x y) (+ x y))) - (check-synth) - diff --git a/test/regress/regress1/sygus/no-mention.sy b/test/regress/regress1/sygus/no-mention.sy index f964d6039..ff10c1263 100644 --- a/test/regress/regress1/sygus/no-mention.sy +++ b/test/regress/regress1/sygus/no-mention.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --sygus-out=status +; COMMAND-LINE: --lang=sygus2 --sygus-out=status (set-logic LIA) (synth-fun p ((x Int) (y Int)) Int) @@ -12,4 +12,3 @@ (constraint (>= (m x y) x)) (check-synth) - diff --git a/test/regress/regress1/sygus/pbe_multi.sy b/test/regress/regress1/sygus/pbe_multi.sy index 70cb6b2d2..4c588ee17 100644 --- a/test/regress/regress1/sygus/pbe_multi.sy +++ b/test/regress/regress1/sygus/pbe_multi.sy @@ -1,27 +1,25 @@ ; 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))
-
-(synth-fun f ( (x (BitVec 64))) (BitVec 64)
-(
-
-(Start (BitVec 64) (#x0000000000000000 #x0000000000000001 x (bvnot Start)
- (shl1 Start)
- (shr1 Start)
- (shr4 Start)
- (shr16 Start)
- (bvand Start Start)
- (bvor Start Start)
- (bvxor Start Start)
- (bvadd Start Start)
- (if0 Start Start Start)
- ))
+(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)))
+((Start (_ BitVec 64) (#x0000000000000000 #x0000000000000001 x (bvnot Start)
+ (shl1 Start)
+ (shr1 Start)
+ (shr4 Start)
+ (shr16 Start)
+ (bvand Start Start)
+ (bvor Start Start)
+ (bvxor Start Start)
+ (bvadd Start Start)
+ (if0 Start Start Start)))
)
)
@@ -37,20 +35,18 @@ (constraint (= (f #x483db90b3dee6596) #x0000483db90b3dee))
(constraint (= (f #x55376e703c4a1ea8) #x000055376e703c4a))
-(synth-fun g ( (x (BitVec 64))) (BitVec 64)
-(
-
-(Start (BitVec 64) (#x0000000000000000 #x0000000000000001 x (bvnot Start)
- (shl1 Start)
- (shr1 Start)
- (shr4 Start)
- (shr16 Start)
- (bvand Start Start)
- (bvor Start Start)
- (bvxor Start Start)
- (bvadd Start Start)
- (if0 Start Start Start)
- ))
+(synth-fun g ( (x (_ BitVec 64))) (_ BitVec 64)
+((Start (_ BitVec 64)))
+((Start (_ BitVec 64) (#x0000000000000000 #x0000000000000001 x (bvnot Start)
+ (shl1 Start)
+ (shr1 Start)
+ (shr4 Start)
+ (shr16 Start)
+ (bvand Start Start)
+ (bvor Start Start)
+ (bvxor Start Start)
+ (bvadd Start Start)
+ (if0 Start Start Start)))
)
)
diff --git a/test/regress/regress1/sygus/phone-1-long.sy b/test/regress/regress1/sygus/phone-1-long.sy index 00a031ed4..0b402acf5 100644 --- a/test/regress/regress1/sygus/phone-1-long.sy +++ b/test/regress/regress1/sygus/phone-1-long.sy @@ -1,25 +1,21 @@ -; COMMAND-LINE: --cegqi-si=none --sygus-out=status --sygus-fair=direct
+; COMMAND-LINE: --lang=sygus2 --cegqi-si=none --sygus-out=status --sygus-fair=direct
; EXPECT: unsat
(set-logic SLIA)
-
+
(synth-fun f ((name String)) String
- ((Start String (ntString))
- (ntString String (name " "
+ ((ntString String) (ntInt Int))
+ ((ntString String (name " "
(str.++ ntString ntString)
(str.replace ntString ntString ntString)
(str.at ntString ntInt)
- (int.to.str ntInt)
+ (str.from_int ntInt)
(str.substr ntString ntInt ntInt)))
(ntInt Int (0 1 2 3 4 5
(+ ntInt ntInt)
(- ntInt ntInt)
(str.len ntString)
- (str.to.int ntString)
- (str.indexof ntString ntString ntInt)))
- (ntBool Bool (true false
- (str.prefixof ntString ntString)
- (str.suffixof ntString ntString)
- (str.contains ntString ntString)))))
+ (str.to_int ntString)
+ (str.indexof ntString ntString ntInt)))))
(declare-var name String)
(constraint (= (f "938-242-504") "242"))
diff --git a/test/regress/regress1/sygus/planning-unif.sy b/test/regress/regress1/sygus/planning-unif.sy index 3a715501a..212c25595 100644 --- a/test/regress/regress1/sygus/planning-unif.sy +++ b/test/regress/regress1/sygus/planning-unif.sy @@ -1,8 +1,8 @@ ; EXPECT: unsat -; COMMAND-LINE: --sygus-unif-pi=complete --sygus-out=status +; COMMAND-LINE: --lang=sygus2 --sygus-unif-pi=complete --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 @@ -11,19 +11,19 @@ (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 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 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 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 @@ -37,12 +37,12 @@ currPoint)))) (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 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 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))))) @@ -51,42 +51,42 @@ currPoint)))) (= 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 (= 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 (= 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 (= 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 (= 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 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 (= 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 (= 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 (= 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 (= 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 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,15 +134,15 @@ currPoint)))) 7 8 9 - )) + )) (StartBool Bool ((and StartBool StartBool) (or StartBool StartBool) (not StartBool) (<= CondInt CondInt) (= CondInt CondInt) - (>= CondInt CondInt))))) - - (constraint (or + (>= CondInt CondInt))))) + +(constraint (or (and (= (interpret-move (interpret-move (interpret-move 0 (move 0 99 98)) (move (interpret-move 0 (move 0 99 98)) o0-1 o1-1)) (move (interpret-move (interpret-move 0 (move 0 99 98)) (move (interpret-move 0 (move 0 99 98)) o0-1 o1-1)) o0-2 o1-2)) 30) (and (no-overlaps-one-step 0 (move 0 99 98) 99 o0-1 98 o1-1) (and (no-overlaps-one-step (interpret-move 0 (move 0 99 98)) (move (interpret-move 0 (move 0 99 98)) o0-1 o1-1) o0-1 o0-2 o1-1 o1-2) (and (no-overlaps-one-step (interpret-move (interpret-move 0 (move 0 99 98)) (move (interpret-move 0 (move 0 99 98)) o0-1 o1-1)) (move (interpret-move (interpret-move 0 (move 0 99 98)) (move (interpret-move 0 (move 0 99 98)) o0-1 o1-1)) o0-2 o1-2) o0-2 o0-3 o1-2 o1-3) true)))) diff --git a/test/regress/regress1/sygus/process-10-vars.sy b/test/regress/regress1/sygus/process-10-vars.sy index 77990473f..6a9a80a49 100644 --- a/test/regress/regress1/sygus/process-10-vars.sy +++ b/test/regress/regress1/sygus/process-10-vars.sy @@ -1,4 +1,4 @@ -; COMMAND-LINE: --cegqi-si=none --sygus-out=status --sygus-arg-relevant +; COMMAND-LINE: --lang=sygus2 --cegqi-si=none --sygus-out=status --sygus-arg-relevant ; EXPECT: unsat (set-logic LIA) diff --git a/test/regress/regress1/sygus/qe.sy b/test/regress/regress1/sygus/qe.sy index 77e16efcb..c8d56229a 100644 --- a/test/regress/regress1/sygus/qe.sy +++ b/test/regress/regress1/sygus/qe.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --cegqi-si=all --sygus-out=status --sygus-qe-preproc +; COMMAND-LINE: --lang=sygus2 --cegqi-si=all --sygus-out=status --sygus-qe-preproc (set-logic LIA) (synth-fun f ((x Int)) Int) diff --git a/test/regress/regress1/sygus/real-any-const.sy b/test/regress/regress1/sygus/real-any-const.sy index 2b59b7301..431d0c1b0 100644 --- a/test/regress/regress1/sygus/real-any-const.sy +++ b/test/regress/regress1/sygus/real-any-const.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --sygus-out=status --no-sygus-pbe --cegqi-si=none --sygus-grammar-cons=any-term-concise +; COMMAND-LINE: --lang=sygus2 --sygus-out=status --no-sygus-pbe --cegqi-si=none --sygus-grammar-cons=any-term-concise (set-logic LRA) (synth-fun f ((x Real) (y Real)) Real) diff --git a/test/regress/regress1/sygus/real-grammar.sy b/test/regress/regress1/sygus/real-grammar.sy index c2f4ae0bc..128a94c1d 100644 --- a/test/regress/regress1/sygus/real-grammar.sy +++ b/test/regress/regress1/sygus/real-grammar.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --sygus-out=status --cegqi-si=none +; COMMAND-LINE: --lang=sygus2 --sygus-out=status --cegqi-si=none (set-logic LRA) diff --git a/test/regress/regress1/sygus/sets-pred-test.sy b/test/regress/regress1/sygus/sets-pred-test.sy index 284325712..f45329b27 100644 --- a/test/regress/regress1/sygus/sets-pred-test.sy +++ b/test/regress/regress1/sygus/sets-pred-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 P ((x (Set Int))) Bool) diff --git a/test/regress/regress1/sygus/stopwatch-bt.sy b/test/regress/regress1/sygus/stopwatch-bt.sy index 291ae6099..c33e16bcd 100644 --- a/test/regress/regress1/sygus/stopwatch-bt.sy +++ b/test/regress/regress1/sygus/stopwatch-bt.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --sygus-inv-templ=post --sygus-out=status +; COMMAND-LINE: --lang=sygus2 --sygus-inv-templ=post --sygus-out=status (set-logic LIA) (define-fun @@ -116,14 +116,6 @@ )) -(declare-primed-var stopwatch.usr.toggle Bool) -(declare-primed-var stopwatch.usr.reset Bool) -(declare-primed-var stopwatch.usr.count Int) -(declare-primed-var stopwatch.res.init_flag Bool) -(declare-primed-var stopwatch.res.abs_0 Bool) -(declare-primed-var stopwatch.impl.usr.running Bool) -(declare-primed-var stopwatch.res.abs_1 Int) -(declare-primed-var stopwatch.res.inst_0 Bool) (define-fun init ( diff --git a/test/regress/regress1/sygus/strings-any-term1.sy b/test/regress/regress1/sygus/strings-any-term1.sy index 3d8fd7530..cca2edb2c 100644 --- a/test/regress/regress1/sygus/strings-any-term1.sy +++ b/test/regress/regress1/sygus/strings-any-term1.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --sygus-out=status --no-sygus-pbe --cegqi-si=none --sygus-grammar-cons=any-term +; COMMAND-LINE: --lang=sygus2 --sygus-out=status --no-sygus-pbe --cegqi-si=none --sygus-grammar-cons=any-term (set-logic ALL) (synth-fun f ((x String) (y String)) Int) (declare-var x String) diff --git a/test/regress/regress1/sygus/strings-concat-3-args.sy b/test/regress/regress1/sygus/strings-concat-3-args.sy index 6628ff746..681d3ccff 100644 --- a/test/regress/regress1/sygus/strings-concat-3-args.sy +++ b/test/regress/regress1/sygus/strings-concat-3-args.sy @@ -1,10 +1,10 @@ ; EXPECT: unsat -; COMMAND-LINE: --sygus-out=status +; COMMAND-LINE: --lang=sygus2 --sygus-out=status (set-logic SLIA) (synth-fun f ((x String)) String -((Start String (ntString)) +((ntString String) (ntStringConst String)) -(ntString String (x "" (str.++ ntStringConst ntString ntString))) +((ntString String (x "" (str.++ ntStringConst ntString ntString))) (ntStringConst String ("a" "b" " ")) @@ -15,4 +15,3 @@ (constraint (= (f "def") "ab def")) (check-synth) - diff --git a/test/regress/regress1/sygus/strings-double-rec.sy b/test/regress/regress1/sygus/strings-double-rec.sy index ea9caadea..0c21015e7 100644 --- a/test/regress/regress1/sygus/strings-double-rec.sy +++ b/test/regress/regress1/sygus/strings-double-rec.sy @@ -1,8 +1,9 @@ ; EXPECT: unsat -; COMMAND-LINE: --sygus-out=status +; COMMAND-LINE: --lang=sygus2 --sygus-out=status (set-logic SLIA) - + (synth-fun f ((name String)) String + ((Start String) (Start1 String) (Start2 String)) ((Start String (name "A" "B" "" (str.++ Start1 Start2))) (Start1 String (name "A" "B" "")) (Start2 String (name "B" "A" (str.++ Start2 Start))) @@ -10,7 +11,7 @@ (declare-var name String) - + (constraint (= (f "BB") "AAAAAAAAAAAA")) - + (check-synth) diff --git a/test/regress/regress1/sygus/strings-no-syntax.sy b/test/regress/regress1/sygus/strings-no-syntax.sy index 4959d6fe1..8abb33f33 100644 --- a/test/regress/regress1/sygus/strings-no-syntax.sy +++ b/test/regress/regress1/sygus/strings-no-syntax.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) (y String)) String) diff --git a/test/regress/regress1/sygus/strings-small.sy b/test/regress/regress1/sygus/strings-small.sy index 7d976ff39..834898b02 100644 --- a/test/regress/regress1/sygus/strings-small.sy +++ b/test/regress/regress1/sygus/strings-small.sy @@ -1,27 +1,27 @@ ; EXPECT: unsat -; COMMAND-LINE: --sygus-out=status +; COMMAND-LINE: --lang=sygus2 --sygus-out=status (set-logic SLIA) (synth-fun f ((firstname String) (lastname String)) String -((Start String (ntString)) +((ntString String) (ntInt Int) (ntBool Bool)) -(ntString String ( -firstname -lastname +((ntString String ( +firstname +lastname " " (str.++ ntString ntString))) (ntInt Int ( -0 -1 +0 +1 2 (+ ntInt ntInt) (- ntInt ntInt) (str.len ntString) -(str.to.int ntString) +(str.to_int ntString) (str.indexof ntString ntString ntInt))) (ntBool Bool ( -true +true false (str.prefixof ntString ntString) (str.suffixof ntString ntString) @@ -32,4 +32,3 @@ false (constraint (= (f "Nancy" "FreeHafer") "Nancy FreeHafer")) (check-synth) - diff --git a/test/regress/regress1/sygus/strings-template-infer-unused.sy b/test/regress/regress1/sygus/strings-template-infer-unused.sy index d0bee5564..2c075388a 100644 --- a/test/regress/regress1/sygus/strings-template-infer-unused.sy +++ b/test/regress/regress1/sygus/strings-template-infer-unused.sy @@ -1,16 +1,17 @@ ; EXPECT: unsat -; COMMAND-LINE: --sygus-out=status +; COMMAND-LINE: --lang=sygus2 --sygus-out=status (set-logic SLIA) - + (define-fun cA ((x String) (w String) (y String) (z String)) String (str.++ (str.++ x "A") y)) - + (synth-fun f ((name String)) String + ((Start String)) ((Start String (name "A" "B" "" - (cA Start Start Start Start))))) + (cA Start Start Start Start))))) (declare-var name String) - + (constraint (= (f "BB") "AAAAAAAAAAAA")) - + (check-synth) diff --git a/test/regress/regress1/sygus/strings-template-infer.sy b/test/regress/regress1/sygus/strings-template-infer.sy index 13c4d7dac..8cbce19b6 100644 --- a/test/regress/regress1/sygus/strings-template-infer.sy +++ b/test/regress/regress1/sygus/strings-template-infer.sy @@ -1,16 +1,17 @@ ; EXPECT: unsat -; COMMAND-LINE: --sygus-out=status +; COMMAND-LINE: --lang=sygus2 --sygus-out=status (set-logic SLIA) - + (define-fun cA ((x String) (y String)) String (str.++ (str.++ x "A") y)) - + (synth-fun f ((name String)) String + ((Start String)) ((Start String (name "A" "B" "" - (cA Start Start))))) + (cA Start Start))))) (declare-var name String) - + (constraint (= (f "BB") "AAAAAAAAAAAA")) - + (check-synth) diff --git a/test/regress/regress1/sygus/strings-trivial-simp.sy b/test/regress/regress1/sygus/strings-trivial-simp.sy index f5e41a8f5..c0e3f0ea6 100644 --- a/test/regress/regress1/sygus/strings-trivial-simp.sy +++ b/test/regress/regress1/sygus/strings-trivial-simp.sy @@ -1,14 +1,15 @@ ; EXPECT: unsat -; COMMAND-LINE: --sygus-out=status +; COMMAND-LINE: --lang=sygus2 --sygus-out=status (set-logic SLIA) - + (synth-fun f ((name String)) String + ((Start String)) ((Start String (name "A" "B" - (str.++ Start Start))))) + (str.++ Start Start))))) (declare-var name String) - + (constraint (= (f "BB") "AAAAAAAAAAAABAAAAAAAABAAA")) - + (check-synth) diff --git a/test/regress/regress1/sygus/strings-trivial-two-type.sy b/test/regress/regress1/sygus/strings-trivial-two-type.sy index 86c71aa3a..ba9ac5064 100644 --- a/test/regress/regress1/sygus/strings-trivial-two-type.sy +++ b/test/regress/regress1/sygus/strings-trivial-two-type.sy @@ -1,18 +1,17 @@ ; EXPECT: unsat -; COMMAND-LINE: --sygus-out=status +; COMMAND-LINE: --lang=sygus2 --sygus-out=status (set-logic SLIA) - + (synth-fun f ((name String)) String - ((Start String (ntString)) - (ntString String (name "B" "" - (str.++ ntStringC ntString))) + ((ntString String) (ntStringC String)) + ((ntString String (name "B" "" + (str.++ ntStringC ntString))) (ntStringC String (name "A" "")) - - )) + )) (declare-var name String) - + (constraint (= (f "B") "AAAAAAAAAAAAAAAAAAAAAAAAA")) - + (check-synth) diff --git a/test/regress/regress1/sygus/strings-trivial.sy b/test/regress/regress1/sygus/strings-trivial.sy index 9af0a1bb1..7fe96cf14 100644 --- a/test/regress/regress1/sygus/strings-trivial.sy +++ b/test/regress/regress1/sygus/strings-trivial.sy @@ -1,15 +1,15 @@ ; EXPECT: unsat -; COMMAND-LINE: --sygus-out=status +; COMMAND-LINE: --lang=sygus2 --sygus-out=status (set-logic SLIA) - + (synth-fun f ((name String)) String - ((Start String (ntString)) - (ntString String (name "A" "B" - (str.++ ntString ntString))))) + ((ntString String)) + ((ntString String (name "A" "B" + (str.++ ntString ntString))))) (declare-var name String) - + (constraint (= (f "B") "AAAAAAAAAAAAAAAAAAAAAAAAA")) - + (check-synth) diff --git a/test/regress/regress1/sygus/sygus-dt.sy b/test/regress/regress1/sygus/sygus-dt.sy index 336c59b27..7539fdd0d 100644 --- a/test/regress/regress1/sygus/sygus-dt.sy +++ b/test/regress/regress1/sygus/sygus-dt.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --sygus-out=status --decision=justification +; COMMAND-LINE: --lang=sygus2 --sygus-out=status --decision=justification (set-logic LIA) @@ -7,8 +7,10 @@ (define-fun g ((x Int)) List (cons (+ x 1) nil)) (define-fun i () List (cons 3 nil)) -(synth-fun f ((x Int)) List ((Start List ((g StartInt) i (cons StartInt Start) nil (tail Start))) - (StartInt Int (x 0 1 (+ StartInt StartInt))))) +(synth-fun f ((x Int)) List + ((Start List) (StartInt Int)) + ((Start List ((g StartInt) i (cons StartInt Start) nil (tail Start))) + (StartInt Int (x 0 1 (+ StartInt StartInt))))) (declare-var x Int) diff --git a/test/regress/regress1/sygus/sygus-lambda-fv.sy b/test/regress/regress1/sygus/sygus-lambda-fv.sy index d2a3700ce..d96960c83 100644 --- a/test/regress/regress1/sygus/sygus-lambda-fv.sy +++ b/test/regress/regress1/sygus/sygus-lambda-fv.sy @@ -1,10 +1,11 @@ ; EXPECT: unsat -; COMMAND-LINE: --sygus-out=status +; COMMAND-LINE: --lang=sygus2 --sygus-out=status (set-logic ALL) -(synth-fun SC ((y (BitVec 32)) (w (BitVec 32)) ) (BitVec 32) +(synth-fun SC ((y (_ BitVec 32)) (w (_ BitVec 32)) ) (_ BitVec 32) + ((Start (_ BitVec 32)) (StartBool Bool)) ( - (Start (BitVec 32) ( + (Start (_ BitVec 32) ( y w #x00000000 diff --git a/test/regress/regress1/sygus/t8.sy b/test/regress/regress1/sygus/t8.sy index 4dd726875..6ac904832 100644 --- a/test/regress/regress1/sygus/t8.sy +++ b/test/regress/regress1/sygus/t8.sy @@ -1,31 +1,30 @@ ; EXPECT: unsat -; COMMAND-LINE: --sygus-out=status -(set-logic LIA) +; COMMAND-LINE: --lang=sygus2 --sygus-out=status +(set-logic LIA) ( -synth-fun f_143-17-143-55 ( (x2 Int) (x1 Int) (parentNode Int) (EMPTY_PARENT Int)) Bool - ((Start Bool ( -(< IntExpr IntExpr) -(and Start Start) -(= IntExpr IntExpr) -(not Start ) -(<= IntExpr IntExpr) -(or Start Start) - - - -)) -(IntExpr Int ( -x2 x1 parentNode EMPTY_PARENT -0 1 -)) - - ) +synth-fun f_143-17-143-55 ((x2 Int) (x1 Int) (parentNode Int) (EMPTY_PARENT Int)) Bool +((Start Bool) (IntExpr Int)) +( + (Start Bool ( + (< IntExpr IntExpr) + (and Start Start) + (= IntExpr IntExpr) + (not Start) + (<= IntExpr IntExpr) + (or Start Start) + )) + (IntExpr Int ( + x2 x1 parentNode EMPTY_PARENT + 0 1 + )) +) ) + (declare-var x2_143-17-143-55 Int) (declare-var x1_143-17-143-55 Int) (declare-var parentNode_143-17-143-55 Int) (declare-var EMPTY_PARENT_143-17-143-55 Int) -(constraint (=> (and (= parentNode_143-17-143-55 0) (and (= EMPTY_PARENT_143-17-143-55 -1) (and (= x2_143-17-143-55 1) (= x1_143-17-143-55 1)) ) ) (= (f_143-17-143-55 x2_143-17-143-55 x1_143-17-143-55 parentNode_143-17-143-55 EMPTY_PARENT_143-17-143-55 ) true))) +(constraint (=> (and (= parentNode_143-17-143-55 0) (and (= EMPTY_PARENT_143-17-143-55 (- 1)) (and (= x2_143-17-143-55 1) (= x1_143-17-143-55 1)))) (= (f_143-17-143-55 x2_143-17-143-55 x1_143-17-143-55 parentNode_143-17-143-55 EMPTY_PARENT_143-17-143-55) true))) (check-synth) diff --git a/test/regress/regress1/sygus/temp_input_to_synth_ic-error-121418.sy b/test/regress/regress1/sygus/temp_input_to_synth_ic-error-121418.sy index 4efd90314..fa8bdc2d7 100644 --- a/test/regress/regress1/sygus/temp_input_to_synth_ic-error-121418.sy +++ b/test/regress/regress1/sygus/temp_input_to_synth_ic-error-121418.sy @@ -1,9 +1,10 @@ ; REQUIRES: symfpu ; EXPECT: unsat -; COMMAND-LINE: --sygus-out=status +; COMMAND-LINE: --lang=sygus2 --sygus-out=status (set-logic ALL) (define-sort FP () (_ FloatingPoint 3 5)) (synth-fun IC ((t FP)) Bool + ((Start Bool) (StartFP FP) (StartRM RoundingMode)) ((Start Bool ( true false diff --git a/test/regress/regress1/sygus/tester.sy b/test/regress/regress1/sygus/tester.sy index 282bc122c..c5b72b009 100644 --- a/test/regress/regress1/sygus/tester.sy +++ b/test/regress/regress1/sygus/tester.sy @@ -1,15 +1,15 @@ ; EXPECT: unsat -; COMMAND-LINE: --sygus-out=status +; COMMAND-LINE: --lang=sygus2 --sygus-out=status (set-logic DTSLIA) (declare-datatype DT ((A (a Int)) (B (b String)) (JSBool (jsBool Bool)))) -(define-fun isA ((i DT)) Bool ((_ is A) i) ) -(define-fun isB ((i DT)) Bool ((_ is B) i) ) +(define-fun isA ((i DT)) Bool ((_ is A) i)) +(define-fun isB ((i DT)) Bool ((_ is B) i)) (synth-fun add ((x1 DT)) DT + ((ntDT DT) (ntBool Bool) (ntInt Int)) ( - (Start DT (ntDT)) (ntDT DT ( x1 (JSBool ntBool) diff --git a/test/regress/regress1/sygus/tl-type-0.sy b/test/regress/regress1/sygus/tl-type-0.sy index ceda89d78..0beea8056 100644 --- a/test/regress/regress1/sygus/tl-type-0.sy +++ b/test/regress/regress1/sygus/tl-type-0.sy @@ -1,11 +1,11 @@ ; EXPECT: unsat -; COMMAND-LINE: --cegqi-si=none --sygus-out=status +; COMMAND-LINE: --lang=sygus2 --cegqi-si=none --sygus-out=status (set-logic LIA) (synth-fun f ((x Int)) Int + ((Start Int) (Term Int)) ((Start Int ((+ Term Term))) (Term Int (x 0)))) (declare-var x Int) (constraint (= (f x) 0)) (check-synth) - diff --git a/test/regress/regress1/sygus/tl-type-4x.sy b/test/regress/regress1/sygus/tl-type-4x.sy index bf8eee5ee..7c4403397 100644 --- a/test/regress/regress1/sygus/tl-type-4x.sy +++ b/test/regress/regress1/sygus/tl-type-4x.sy @@ -1,11 +1,11 @@ ; EXPECT: unsat -; COMMAND-LINE: --cegqi-si=none --sygus-out=status +; COMMAND-LINE: --lang=sygus2 --cegqi-si=none --sygus-out=status (set-logic LIA) (synth-fun f ((x Int)) Int + ((Start Int) (Term Int)) ((Start Int (Term (+ Start Start))) (Term Int (x 0)))) (declare-var x Int) (constraint (= (f x) (* 4 x))) (check-synth) - diff --git a/test/regress/regress1/sygus/tl-type.sy b/test/regress/regress1/sygus/tl-type.sy index 6f25a570e..fe39ddd8e 100644 --- a/test/regress/regress1/sygus/tl-type.sy +++ b/test/regress/regress1/sygus/tl-type.sy @@ -1,11 +1,11 @@ ; EXPECT: unsat -; COMMAND-LINE: --cegqi-si=none --sygus-out=status +; COMMAND-LINE: --lang=sygus2 --cegqi-si=none --sygus-out=status (set-logic LIA) (synth-fun f ((x Int)) Int + ((Start Int) (Term Int)) ((Start Int (Term (+ Start Start))) (Term Int (x 0)))) (declare-var x Int) (constraint (= (f x) (* 3 x))) (check-synth) - diff --git a/test/regress/regress1/sygus/triv-type-mismatch-si.sy b/test/regress/regress1/sygus/triv-type-mismatch-si.sy index 37c5a7f53..6ef891560 100644 --- a/test/regress/regress1/sygus/triv-type-mismatch-si.sy +++ b/test/regress/regress1/sygus/triv-type-mismatch-si.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --sygus-out=status +; COMMAND-LINE: --lang=sygus2 --sygus-out=status (set-logic LIA) (synth-fun R ((y Int)) Bool) @@ -10,4 +10,3 @@ (constraint (=> (= x e) (R x))) (check-synth) - diff --git a/test/regress/regress1/sygus/trivial-stream.sy b/test/regress/regress1/sygus/trivial-stream.sy index 33abb6ee8..8d3e91b06 100644 --- a/test/regress/regress1/sygus/trivial-stream.sy +++ b/test/regress/regress1/sygus/trivial-stream.sy @@ -3,15 +3,16 @@ ; EXPECT: (error "Maximum term size (0) for enumerative SyGuS exceeded.") ; EXIT: 1 -; COMMAND-LINE: --sygus-stream --sygus-abort-size=0 --sygus-active-gen=var-agnostic +; COMMAND-LINE: --lang=sygus2 --sygus-stream --sygus-abort-size=0 --sygus-active-gen=var-agnostic (set-logic LIA) (synth-fun triv ((x Int) (y Int)) Int + ((Start Int)) ((Start Int (x y (+ Start Start) )) - )) + )) (check-synth) diff --git a/test/regress/regress1/sygus/twolets1.sy b/test/regress/regress1/sygus/twolets1.sy index 06d2ecb71..b78bf7647 100644 --- a/test/regress/regress1/sygus/twolets1.sy +++ b/test/regress/regress1/sygus/twolets1.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --cegqi-si=all --sygus-out=status +; COMMAND-LINE: --lang=sygus2 --cegqi-si=all --sygus-out=status (set-logic LIA) ;; f1 is x plus 2 ;; f2 is 2x plus 5 @@ -7,6 +7,7 @@ (define-fun let0 ((x Int) (y Int) (z Int)) Int (+ (+ y x) z)) (synth-fun f1 ((x Int)) Int + ((Start Int) (Intx Int) (CInt Int)) ( (Start Int ( (let0 Intx CInt CInt) @@ -14,11 +15,11 @@ ) (Intx Int (x)) (CInt Int (0 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15)) - ) ) (synth-fun f2 ((x Int)) Int + ((Start Int) (Intx Int) (CInt Int)) ( (Start Int (x (let0 Intx Start CInt) @@ -26,15 +27,13 @@ ) (Intx Int (x)) (CInt Int (0 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15)) - ) ) (declare-var x Int) -(constraint (= (+ (f1 x)(f2 x)) (+ (+ x x) (+ x 8)))) -(constraint (= (- (f2 x)(f1 x)) (+ x 2))) +(constraint (= (+ (f1 x) (f2 x)) (+ (+ x x) (+ x 8)))) +(constraint (= (- (f2 x) (f1 x)) (+ x 2))) (check-synth) - diff --git a/test/regress/regress1/sygus/twolets2-orig.sy b/test/regress/regress1/sygus/twolets2-orig.sy index a92c0b014..ca1e512a1 100644 --- a/test/regress/regress1/sygus/twolets2-orig.sy +++ b/test/regress/regress1/sygus/twolets2-orig.sy @@ -1,29 +1,28 @@ ; EXPECT: unsat -; COMMAND-LINE: --cegqi-si=all --sygus-out=status +; COMMAND-LINE: --lang=sygus2 --cegqi-si=all --sygus-out=status (set-logic LIA) (define-fun letf ((x Int) (y Int) (z Int)) Int (+ (+ y x) z)) (synth-fun f1 ((x Int)) Int + ((Start Int) (CInt Int)) ( (Start Int ( (letf x CInt CInt) ) ) (CInt Int (0 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15)) - ) ) (synth-fun f2 ((x Int)) Int + ((Start Int) (CInt Int)) ( (Start Int (x (letf x Start CInt) ) ) (CInt Int (0 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15)) - ) ) (declare-var x1 Int) (declare-var x2 Int) -(constraint (= (+ (f1 x1)(f2 x2)) (+ (+ x2 x2) (+ x1 8)))) +(constraint (= (+ (f1 x1) (f2 x2)) (+ (+ x2 x2) (+ x1 8)))) (check-synth) - diff --git a/test/regress/regress1/sygus/unbdd_inv_gen_ex7.sy b/test/regress/regress1/sygus/unbdd_inv_gen_ex7.sy index 73d410d51..34abb6de8 100644 --- a/test/regress/regress1/sygus/unbdd_inv_gen_ex7.sy +++ b/test/regress/regress1/sygus/unbdd_inv_gen_ex7.sy @@ -1,14 +1,15 @@ ; EXPECT: unsat -; COMMAND-LINE: --sygus-out=status +; COMMAND-LINE: --lang=sygus2 --sygus-out=status (set-logic LIA) (synth-fun inv ((i Int) (y 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 y l)) (Const Int ((+ Const Const) (- Const Const) 0 1)) ) @@ -35,6 +36,6 @@ (constraint (implies (or3 (< x 0) (< y 0) (> y x)) true)) (constraint (implies (and3 (not (or3 (< x 0) (< y 0) (> y x))) (= l x) (= i 0)) (inv i y l))) (constraint (implies (and4 (inv i y l) (< i y) (not (or (< i 0) (>= i l))) (= i1 (+ i 1))) (inv i1 y l))) -(constraint (implies (and3 (inv i y l) (< i y) (or (< i 0) (>= i l))) false)) +(constraint (implies (and3 (inv i y l) (< i y) (or (< i 0) (>= i l))) false)) (check-synth) diff --git a/test/regress/regress1/sygus/unbdd_inv_gen_winf1.sy b/test/regress/regress1/sygus/unbdd_inv_gen_winf1.sy index d45cec38b..edfc2176b 100644 --- a/test/regress/regress1/sygus/unbdd_inv_gen_winf1.sy +++ b/test/regress/regress1/sygus/unbdd_inv_gen_winf1.sy @@ -1,15 +1,16 @@ ; EXPECT: unsat -; COMMAND-LINE: --sygus-out=status +; COMMAND-LINE: --lang=sygus2 --sygus-out=status (set-logic LIA) (synth-fun inv ((x 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 (x)) (Const Int ((+ Const Const) (- Const Const) 0 1)) ) diff --git a/test/regress/regress1/sygus/unifpi-solve-car_1.lus.sy b/test/regress/regress1/sygus/unifpi-solve-car_1.lus.sy index 38267c10d..c1d196f60 100644 --- a/test/regress/regress1/sygus/unifpi-solve-car_1.lus.sy +++ b/test/regress/regress1/sygus/unifpi-solve-car_1.lus.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --sygus-out=status --sygus-grammar-cons=any-term-concise --sygus-unif-pi=complete +; COMMAND-LINE: --lang=sygus2 --sygus-out=status --sygus-grammar-cons=any-term-concise --sygus-unif-pi=complete (set-logic LIA) @@ -189,11 +189,11 @@ ) Bool (let - ((X1 Int top.res.abs_3_a_0)) + ((X1 top.res.abs_3_a_0)) (and (= top.res.abs_10_a_0 (and top.res.abs_9_a_0 (< X1 32767))) (let - ((X2 Bool top.res.abs_11_a_0)) + ((X2 top.res.abs_11_a_0)) (and (= top.usr.OK_a_0 (=> X2 (>= X1 0))) (__node_init_voiture_0 @@ -267,11 +267,11 @@ ) Bool (let - ((X1 Int top.res.abs_3_a_1)) + ((X1 top.res.abs_3_a_1)) (and (= top.res.abs_10_a_1 (and top.res.abs_9_a_1 (< X1 32767))) (let - ((X2 Bool top.res.abs_11_a_1)) + ((X2 top.res.abs_11_a_1)) (and (= top.usr.OK_a_1 (=> X2 (>= X1 0))) (__node_trans_voiture_0 @@ -346,26 +346,6 @@ )) -(declare-primed-var top.usr.m Bool) -(declare-primed-var top.usr.s Bool) -(declare-primed-var top.usr.OK Bool) -(declare-primed-var top.res.init_flag Bool) -(declare-primed-var top.res.abs_0 Bool) -(declare-primed-var top.res.abs_1 Bool) -(declare-primed-var top.res.abs_2 Bool) -(declare-primed-var top.res.abs_3 Int) -(declare-primed-var top.res.abs_4 Int) -(declare-primed-var top.res.abs_5 Int) -(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.abs_9 Bool) -(declare-primed-var top.res.abs_10 Bool) -(declare-primed-var top.res.abs_11 Bool) -(declare-primed-var top.res.inst_3 Bool) -(declare-primed-var top.res.inst_2 Bool) -(declare-primed-var top.res.inst_1 Bool) -(declare-primed-var top.res.inst_0 Bool) (define-fun init ( @@ -392,11 +372,11 @@ ) Bool (let - ((X1 Int top.res.abs_3)) + ((X1 top.res.abs_3)) (and (= top.res.abs_10 (and top.res.abs_9 (< X1 32767))) (let - ((X2 Bool top.res.abs_11)) + ((X2 top.res.abs_11)) (and (= top.usr.OK (=> X2 (>= X1 0))) (__node_init_voiture_0 @@ -472,11 +452,11 @@ ) Bool (let - ((X1 Int top.res.abs_3!)) + ((X1 top.res.abs_3!)) (and (= top.res.abs_10! (and top.res.abs_9! (< X1 32767))) (let - ((X2 Bool top.res.abs_11!)) + ((X2 top.res.abs_11!)) (and (= top.usr.OK! (=> X2 (>= X1 0))) (__node_trans_voiture_0 diff --git a/test/regress/regress1/sygus/univ_2-long-repeat.sy b/test/regress/regress1/sygus/univ_2-long-repeat.sy index ac9493b2d..a2c4c028d 100644 --- a/test/regress/regress1/sygus/univ_2-long-repeat.sy +++ b/test/regress/regress1/sygus/univ_2-long-repeat.sy @@ -1,89 +1,89 @@ ; EXPECT: unsat
-; COMMAND-LINE: --sygus-fair=direct --sygus-out=status
+; COMMAND-LINE: --lang=sygus2 --sygus-fair=direct --sygus-out=status
(set-logic SLIA)
-
+
(synth-fun f ((col1 String) (col2 String)) String
- ((Start String (ntString))
- (ntString String (col1 col2 " " "," "USA" "PA" "CT" "CA" "MD" "NY"
+ ((ntString String) (ntInt Int) (ntBool Bool))
+ ((ntString String (col1 col2 " " "," "USA" "PA" "CT" "CA" "MD" "NY"
(str.++ ntString ntString)
(str.replace ntString ntString ntString)
(str.at ntString ntInt)
- (int.to.str ntInt)
+ (str.from_int ntInt)
(ite ntBool ntString ntString)
(str.substr ntString ntInt ntInt)))
(ntInt Int (0 1 2
(+ ntInt ntInt)
(- ntInt ntInt)
(str.len ntString)
- (str.to.int ntString)
+ (str.to_int ntString)
(str.indexof ntString ntString ntInt)))
(ntBool Bool (true false
(str.prefixof ntString ntString)
(str.suffixof ntString ntString)
(str.contains ntString ntString)))))
-
(declare-var col1 String)
(declare-var col2 String)
-(constraint (= (f "UC Berkeley" "Berkeley, CA")
+
+(constraint (= (f "UC Berkeley" "Berkeley, CA")
"UC Berkeley, Berkeley, CA, USA"))
-(constraint (= (f "University of Pennsylvania" "Phialdelphia, PA, USA")
+(constraint (= (f "University of Pennsylvania" "Phialdelphia, PA, USA")
"University of Pennsylvania, Phialdelphia, PA, USA"))
-(constraint (= (f "UCLA" "Los Angeles, CA")
+(constraint (= (f "UCLA" "Los Angeles, CA")
"UCLA, Los Angeles, CA, USA"))
-(constraint (= (f "Cornell University" "Ithaca, New York, USA")
+(constraint (= (f "Cornell University" "Ithaca, New York, USA")
"Cornell University, Ithaca, New York, USA"))
-(constraint (= (f "Penn" "Philadelphia, PA, USA")
+(constraint (= (f "Penn" "Philadelphia, PA, USA")
"Penn, Philadelphia, PA, USA"))
-(constraint (= (f "University of Michigan" "Ann Arbor, MI, USA")
+(constraint (= (f "University of Michigan" "Ann Arbor, MI, USA")
"University of Michigan, Ann Arbor, MI, USA"))
-(constraint (= (f "UC Berkeley" "Berkeley, CA")
+(constraint (= (f "UC Berkeley" "Berkeley, CA")
"UC Berkeley, Berkeley, CA, USA"))
-(constraint (= (f "MIT" "Cambridge, MA")
+(constraint (= (f "MIT" "Cambridge, MA")
"MIT, Cambridge, MA, USA"))
-(constraint (= (f "University of Pennsylvania" "Phialdelphia, PA, USA")
+(constraint (= (f "University of Pennsylvania" "Phialdelphia, PA, USA")
"University of Pennsylvania, Phialdelphia, PA, USA"))
-(constraint (= (f "UCLA" "Los Angeles, CA")
- "UCLA, Los Angeles, CA, USA"))
-(constraint (= (f "University of Maryland College Park" "College Park, MD")
+(constraint (= (f "UCLA" "Los Angeles, CA")
+ "UCLA, Los Angeles, CA, USA"))
+(constraint (= (f "University of Maryland College Park" "College Park, MD")
"University of Maryland College Park, College Park, MD, USA"))
-(constraint (= (f "University of Michigan" "Ann Arbor, MI, USA")
+(constraint (= (f "University of Michigan" "Ann Arbor, MI, USA")
"University of Michigan, Ann Arbor, MI, USA"))
-(constraint (= (f "UC Berkeley" "Berkeley, CA")
+(constraint (= (f "UC Berkeley" "Berkeley, CA")
"UC Berkeley, Berkeley, CA, USA"))
-(constraint (= (f "MIT" "Cambridge, MA")
+(constraint (= (f "MIT" "Cambridge, MA")
"MIT, Cambridge, MA, USA"))
-(constraint (= (f "Rice University" "Houston, TX")
+(constraint (= (f "Rice University" "Houston, TX")
"Rice University, Houston, TX, USA"))
-(constraint (= (f "Yale University" "New Haven, CT, USA")
+(constraint (= (f "Yale University" "New Haven, CT, USA")
"Yale University, New Haven, CT, USA"))
-(constraint (= (f "Columbia University" "New York, NY, USA")
+(constraint (= (f "Columbia University" "New York, NY, USA")
"Columbia University, New York, NY, USA"))
-(constraint (= (f "NYU" "New York, New York, USA")
+(constraint (= (f "NYU" "New York, New York, USA")
"NYU, New York, New York, USA"))
-(constraint (= (f "Drexel University" "Philadelphia, PA")
- "Drexel University, Philadelphia, PA, USA"))
-(constraint (= (f "UC Berkeley" "Berkeley, CA")
+(constraint (= (f "Drexel University" "Philadelphia, PA")
+ "Drexel University, Philadelphia, PA, USA"))
+(constraint (= (f "UC Berkeley" "Berkeley, CA")
"UC Berkeley, Berkeley, CA, USA"))
-(constraint (= (f "UIUC" "Urbana, IL")
+(constraint (= (f "UIUC" "Urbana, IL")
"UIUC, Urbana, IL, USA"))
-(constraint (= (f "Temple University" "Philadelphia, PA")
+(constraint (= (f "Temple University" "Philadelphia, PA")
"Temple University, Philadelphia, PA, USA"))
-(constraint (= (f "Harvard University" "Cambridge, MA, USA")
+(constraint (= (f "Harvard University" "Cambridge, MA, USA")
"Harvard University, Cambridge, MA, USA"))
-(constraint (= (f "University of Connecticut" "Storrs, CT, USA")
+(constraint (= (f "University of Connecticut" "Storrs, CT, USA")
"University of Connecticut, Storrs, CT, USA"))
-(constraint (= (f "Drexel University" "Philadelphia, PA")
+(constraint (= (f "Drexel University" "Philadelphia, PA")
"Drexel University, Philadelphia, PA, USA"))
-(constraint (= (f "NYU" "New York, New York, USA")
- "NYU, New York, New York, USA"))
-(constraint (= (f "UIUC" "Urbana, IL")
- "UIUC, Urbana, IL, USA"))
-(constraint (= (f "New Haven University" "New Haven, CT, USA")
+(constraint (= (f "NYU" "New York, New York, USA")
+ "NYU, New York, New York, USA"))
+(constraint (= (f "UIUC" "Urbana, IL")
+ "UIUC, Urbana, IL, USA"))
+(constraint (= (f "New Haven University" "New Haven, CT, USA")
"New Haven University, New Haven, CT, USA"))
-(constraint (= (f "University of California, Santa Barbara" "Santa Barbara, CA, USA")
+(constraint (= (f "University of California, Santa Barbara" "Santa Barbara, CA, USA")
"University of California, Santa Barbara, Santa Barbara, CA, USA"))
-(constraint (= (f "University of Connecticut" "Storrs, CT, USA")
- "University of Connecticut, Storrs, CT, USA"))
-
+(constraint (= (f "University of Connecticut" "Storrs, CT, USA")
+ "University of Connecticut, Storrs, CT, USA"))
+
(check-synth)
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))))) diff --git a/test/regress/regress3/sixfuncs.sy b/test/regress/regress3/sixfuncs.sy index 0acdcf25e..89f112e0a 100644 --- a/test/regress/regress3/sixfuncs.sy +++ b/test/regress/regress3/sixfuncs.sy @@ -1,59 +1,65 @@ ; EXPECT: unsat -; COMMAND-LINE: --sygus-out=status --decision=justification +; COMMAND-LINE: --lang=sygus2 --sygus-out=status --decision=justification (set-logic LIA) (synth-fun f1 ((p1 Int) (P1 Int)) Int - ((Start Int ( - p1 - P1 - (- Start Start) - (+ Start Start) - ) - ))) + ((Start Int)) + ((Start Int ( + p1 + P1 + (- Start Start) + (+ Start Start) + ))) +) (synth-fun f2 ((p1 Int) (P1 Int)) Int - ((Start Int ( - p1 - P1 - (+ Start Start) - ) - ))) + ((Start Int)) + ((Start Int ( + p1 + P1 + (+ Start Start) + ))) +) (synth-fun f3 ((p1 Int) (P1 Int)) Int - ((Start Int ( - p1 - P1 - (- Start Start) - (+ Start Start) - ) - ))) + ((Start Int)) + ((Start Int ( + p1 + P1 + (- Start Start) + (+ Start Start) + ))) +) (synth-fun f4 ((p1 Int) (P1 Int)) Int - ((Start Int ( - p1 - P1 - (- Start Start) - (+ Start Start) - ) - ))) + ((Start Int)) + ((Start Int ( + p1 + P1 + (- Start Start) + (+ Start Start) + ))) +) (synth-fun f5 ((p1 Int) (P1 Int)) Int - ((Start Int ( - p1 - P1 - (- Start Start) - (+ Start Start) - ) - ))) + ((Start Int)) + ((Start Int ( + p1 + P1 + (- Start Start) + (+ Start Start) + ))) +) (synth-fun g1 ((p1 Int) (P1 Int)) Int - ((Start Int ( - p1 - P1 - (- Start Start) - (+ Start Start) - ) - ))) + ((Start Int)) + ((Start Int ( + p1 + P1 + (- Start Start) + (+ Start Start) + ))) +) (declare-var x Int) @@ -61,8 +67,8 @@ (constraint (= (+ (f1 x y) (f1 x y)) (f2 x y))) (constraint (= (- (+ (f1 x y) (f2 x y)) y) (f3 x y))) -(constraint (= (+ (f2 x y) (f2 x y)) (f4 x y))) -(constraint (= (+ (f4 x y) (f1 x y)) (f5 x y))) +(constraint (= (+ (f2 x y) (f2 x y)) (f4 x y))) +(constraint (= (+ (f4 x y) (f1 x y)) (f5 x y))) (constraint (= (- (f1 x y) y) (g1 x y))) @@ -80,4 +86,3 @@ ;; g3: y+3 ;; g4: 2y+6 ;; g5: 3y+x+7 - diff --git a/test/regress/regress3/strings-any-term.sy b/test/regress/regress3/strings-any-term.sy index 88b30b208..3827585ec 100644 --- a/test/regress/regress3/strings-any-term.sy +++ b/test/regress/regress3/strings-any-term.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --sygus-out=status --no-sygus-pbe --cegqi-si=none --sygus-grammar-cons=any-term --sygus-active-gen=none +; COMMAND-LINE: --lang=sygus2 --sygus-out=status --no-sygus-pbe --cegqi-si=none --sygus-grammar-cons=any-term --sygus-active-gen=none (set-logic ALL) (synth-fun f ((x String) (y String)) Int) (declare-var x String) |