defineType("RegLan", d_solver->getRegExpSort());
defineType("Int", d_solver->getIntegerSort());
- if (getLanguage() == language::input::LANG_SMTLIB_V2_6_1)
+ if (getLanguage() == language::input::LANG_SMTLIB_V2_6_1
+ || getLanguage() == language::input::LANG_SYGUS_V2)
{
defineVar("re.none", d_solver->mkRegexpEmpty());
}
-; 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
; 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)
-
; 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)
; EXPECT: unsat
-; COMMAND-LINE: --sygus-out=status
+; COMMAND-LINE: --lang=sygus2 --sygus-out=status
(set-logic ALIA)
(synth-fun f
; 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))))
; EXPECT: unsat
-; COMMAND-LINE: --sygus-out=status
+; COMMAND-LINE: --lang=sygus2 --sygus-out=status
(set-logic SAT)
(define-fun
))
-(declare-primed-var top.usr.OK Bool)
-(declare-primed-var top.res.init_flag Bool)
-
(define-fun
init (
(top.usr.OK Bool)
; 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)
; 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)
-; COMMAND-LINE: --sygus-out=status
+; COMMAND-LINE: --lang=sygus2 --sygus-out=status
; EXPECT: unsat
(set-logic LIA)
-; COMMAND-LINE: --sygus-out=status
+; COMMAND-LINE: --lang=sygus2 --sygus-out=status
; EXPECT: unsat
(set-logic ALL_SUPPORTED)
; 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))
-; 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)
-; 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))
)
(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)
; 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))
; 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
; 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
(declare-var y Int)
(constraint (= (f x y) (* 3 x)))
(check-synth)
-
; EXPECT: unsat
-; COMMAND-LINE: --sygus-out=status
+; COMMAND-LINE: --lang=sygus2 --sygus-out=status
(set-logic LIA)
(check-synth)
-
; EXPECT: unsat
-; COMMAND-LINE: --sygus-out=status
+; COMMAND-LINE: --lang=sygus2 --sygus-out=status
(set-logic LIA)
(check-synth)
-
; 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)
; 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)
-; 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)
; EXPECT: unsat
-; COMMAND-LINE: --sygus-out=status
+; COMMAND-LINE: --lang=sygus2 --sygus-out=status
(set-logic LRA)
; 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
" "
))
(check-synth)
-
-; 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)))
; 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)
; 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)
-; 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)
-; 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
-; 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
; 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
(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)
; 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
(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)
-; 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)))
))
; 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)
(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)
; 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)))))
(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)))))
(constraint (or (Bad x1 x2) (not (Zero (f x1 x2)))))
(check-synth)
-
; 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)
; 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)
; 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
NT13
NT14
))
- (NT1 Int ( y5
+ (NT1 Int (
+ y5
k1
1
y2
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)
(< 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)
(>= 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)
(>= 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)
(<= 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)
; 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))))
; 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)
(bvugt Start Start)
(= Start Start)
))))
-(declare-var x (BitVec 32) )
+(declare-var x (_ BitVec 32) )
; property
(constraint (= (f #x00000008) #x00000004))
; 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)
; 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
; 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
) 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
) 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
))
-(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 (
) 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
) 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
; 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
; 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
; 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)
(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)
; 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)
; 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)
; 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)
; 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)
; 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)))
)
; 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
; EXPECT: unsat
-; COMMAND-LINE: --sygus-out=status
+; COMMAND-LINE: --lang=sygus2 --sygus-out=status
(set-logic BV)
(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)
; 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)
(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)
; EXPECT: unsat
-; COMMAND-LINE: --sygus-out=status
+; COMMAND-LINE: --lang=sygus2 --sygus-out=status
(set-logic BV)
)
(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) ) )
; 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)
+ )
+ )
)
)
; EXPECT: unsat\r
-; COMMAND-LINE: --sygus-out=status\r
+; COMMAND-LINE: --lang=sygus2 --sygus-out=status\r
\r
(set-logic SLIA)\r
(declare-datatype Ex ((Ex2 (ex Int))))\r
\r
(synth-fun double ((x1 Ex)) Int\r
+ ((ntInt Int) (ntEx Ex))\r
(\r
- (Start Int (ntInt))\r
(ntInt Int\r
(\r
(ex ntEx)\r
; 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))))
(constraint (is-cons (f x)))
(constraint (and (= (head (f x)) x) (= (head (f x)) (+ 5 (head (tail (f x)))))))
(check-synth)
-
; 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)
-
; 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)
; 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
(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))))
)
; EXPECT: unsat\r
-; COMMAND-LINE: --sygus-out=status\r
+; COMMAND-LINE: --lang=sygus2 --sygus-out=status\r
\r
(set-logic ALL_SUPPORTED)\r
(declare-datatype Ex ((Ex2 (ex Int))))\r
\r
(synth-fun ident ((x1 Ex)) Int\r
+ ((Start Int) (ntInt Int) (ntEx Ex))\r
(\r
(Start Int (ntInt))\r
(ntInt Int\r
(\r
(ex ntEx)\r
- )\r
+ )\r
)\r
- (ntEx Ex ( x1 ) )\r
+ (ntEx Ex ( x1 ))\r
)\r
)\r
(constraint (= (ident (Ex2 1)) 1))\r
; 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)
(constraint (= (+ (addExpr1 x y) (addExpr2 y x)) (- x (+ x y))))
(check-synth)
-
; 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
(bvuge StartBv StartBv)
(bvsge StartBv StartBv)
))
- (StartBv (BitVec 4) (
+ (StartBv (_ BitVec 4) (
s
t
#x0
))
))
-(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
; 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)
-
; 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)
-
; 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))
; 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))
; 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))
; 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))
; 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)
(bvor Start Start)
(bvxor Start Start)
(bvadd Start Start)
- (if0 Start Start Start)
- ))
+ (if0 Start Start Start)))
)
)
; 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))
; 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)
; 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))
; 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)))
(inv-constraint inv-f pre-f trans-f post-f)
-(check-synth)
\ No newline at end of file
+(check-synth)
; 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))
; EXPECT: unsat
-; COMMAND-LINE: --sygus-out=status
+; COMMAND-LINE: --lang=sygus2 --sygus-out=status
(set-logic LIA)
(synth-fun inv ((l Int)) Bool
(
(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))
)
)
(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)
; 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)
(str.++ ntString ntString)
)
)
+ (ntInt Int
+ (0 x3)
+ )
+ (ntJSIdentifier JSIdentifier
+ (
+ Error
+ )
+ )
)
)
+
(constraint (= (substring "ey" 1) "e"))
(check-synth)
; 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)
)
)
(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)
; 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)
; 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)
(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)
; 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)
; 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)))
)
)
; 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))))
; 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
+; )
+; )
+; )
+; )
;)
; 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)
-
-
; 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)
; 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)
-
; 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)
-
; 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)
; 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
(constraint (= (f x y) (+ x y)))
-
(check-synth)
-
; 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)
(constraint (>= (m x y) x))
(check-synth)
-
; EXPECT: unsat\r
-; COMMAND-LINE: --sygus-out=status\r
+; COMMAND-LINE: --lang=sygus2 --sygus-out=status\r
(set-logic BV)\r
\r
-(define-fun shr1 ((x (BitVec 64))) (BitVec 64) (bvlshr x #x0000000000000001))\r
-(define-fun shr4 ((x (BitVec 64))) (BitVec 64) (bvlshr x #x0000000000000004))\r
-(define-fun shr16 ((x (BitVec 64))) (BitVec 64) (bvlshr x #x0000000000000010))\r
-(define-fun shl1 ((x (BitVec 64))) (BitVec 64) (bvshl x #x0000000000000001))\r
-(define-fun if0 ((x (BitVec 64)) (y (BitVec 64)) (z (BitVec 64))) (BitVec 64) (ite (= x #x0000000000000001) y z))\r
-\r
-(synth-fun f ( (x (BitVec 64))) (BitVec 64)\r
-(\r
-\r
-(Start (BitVec 64) (#x0000000000000000 #x0000000000000001 x (bvnot Start)\r
- (shl1 Start)\r
- (shr1 Start)\r
- (shr4 Start)\r
- (shr16 Start)\r
- (bvand Start Start)\r
- (bvor Start Start)\r
- (bvxor Start Start)\r
- (bvadd Start Start)\r
- (if0 Start Start Start)\r
- ))\r
+(define-fun shr1 ((x (_ BitVec 64))) (_ BitVec 64) (bvlshr x #x0000000000000001))\r
+(define-fun shr4 ((x (_ BitVec 64))) (_ BitVec 64) (bvlshr x #x0000000000000004))\r
+(define-fun shr16 ((x (_ BitVec 64))) (_ BitVec 64) (bvlshr x #x0000000000000010))\r
+(define-fun shl1 ((x (_ BitVec 64))) (_ BitVec 64) (bvshl x #x0000000000000001))\r
+(define-fun if0 ((x (_ BitVec 64)) (y (_ BitVec 64)) (z (_ BitVec 64))) (_ BitVec 64) (ite (= x #x0000000000000001) y z))\r
+\r
+(synth-fun f ( (x (_ BitVec 64))) (_ BitVec 64)\r
+((Start (_ BitVec 64)))\r
+((Start (_ BitVec 64) (#x0000000000000000 #x0000000000000001 x (bvnot Start)\r
+ (shl1 Start)\r
+ (shr1 Start)\r
+ (shr4 Start)\r
+ (shr16 Start)\r
+ (bvand Start Start)\r
+ (bvor Start Start)\r
+ (bvxor Start Start)\r
+ (bvadd Start Start)\r
+ (if0 Start Start Start)))\r
)\r
)\r
\r
(constraint (= (f #x483db90b3dee6596) #x0000483db90b3dee))\r
(constraint (= (f #x55376e703c4a1ea8) #x000055376e703c4a))\r
\r
-(synth-fun g ( (x (BitVec 64))) (BitVec 64)\r
-(\r
-\r
-(Start (BitVec 64) (#x0000000000000000 #x0000000000000001 x (bvnot Start)\r
- (shl1 Start)\r
- (shr1 Start)\r
- (shr4 Start)\r
- (shr16 Start)\r
- (bvand Start Start)\r
- (bvor Start Start)\r
- (bvxor Start Start)\r
- (bvadd Start Start)\r
- (if0 Start Start Start)\r
- ))\r
+(synth-fun g ( (x (_ BitVec 64))) (_ BitVec 64)\r
+((Start (_ BitVec 64)))\r
+((Start (_ BitVec 64) (#x0000000000000000 #x0000000000000001 x (bvnot Start)\r
+ (shl1 Start)\r
+ (shr1 Start)\r
+ (shr4 Start)\r
+ (shr16 Start)\r
+ (bvand Start Start)\r
+ (bvor Start Start)\r
+ (bvxor Start Start)\r
+ (bvadd Start Start)\r
+ (if0 Start Start Start)))\r
)\r
)\r
\r
-; COMMAND-LINE: --cegqi-si=none --sygus-out=status --sygus-fair=direct\r
+; COMMAND-LINE: --lang=sygus2 --cegqi-si=none --sygus-out=status --sygus-fair=direct\r
; EXPECT: unsat\r
(set-logic SLIA)\r
- \r
+\r
(synth-fun f ((name String)) String\r
- ((Start String (ntString))\r
- (ntString String (name " "\r
+ ((ntString String) (ntInt Int))\r
+ ((ntString String (name " "\r
(str.++ ntString ntString)\r
(str.replace ntString ntString ntString)\r
(str.at ntString ntInt)\r
- (int.to.str ntInt)\r
+ (str.from_int ntInt)\r
(str.substr ntString ntInt ntInt)))\r
(ntInt Int (0 1 2 3 4 5\r
(+ ntInt ntInt)\r
(- ntInt ntInt)\r
(str.len ntString)\r
- (str.to.int ntString)\r
- (str.indexof ntString ntString ntInt)))\r
- (ntBool Bool (true false\r
- (str.prefixof ntString ntString)\r
- (str.suffixof ntString ntString)\r
- (str.contains ntString ntString)))))\r
+ (str.to_int ntString)\r
+ (str.indexof ntString ntString ntInt)))))\r
\r
(declare-var name String)\r
(constraint (= (f "938-242-504") "242"))\r
; 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
(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
(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)))))
(= 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)))
(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
(get-x o1)
(+ CondInt CondInt)
(- CondInt CondInt)
- -1
+ (- 1)
0
1
2
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))))
-; 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)
; 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)
; 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)
; EXPECT: unsat
-; COMMAND-LINE: --sygus-out=status --cegqi-si=none
+; COMMAND-LINE: --lang=sygus2 --sygus-out=status --cegqi-si=none
(set-logic LRA)
; EXPECT: unsat
-; COMMAND-LINE: --sygus-out=status
+; COMMAND-LINE: --lang=sygus2 --sygus-out=status
(set-logic ALL)
(synth-fun P ((x (Set Int))) Bool)
; 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
))
-(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 (
; 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)
; 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" " "))
(constraint (= (f "def") "ab def"))
(check-synth)
-
; 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)))
(declare-var name String)
-
+
(constraint (= (f "BB") "AAAAAAAAAAAA"))
-
+
(check-synth)
; 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)
; 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)
(constraint (= (f "Nancy" "FreeHafer") "Nancy FreeHafer"))
(check-synth)
-
; 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)
; 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)
; 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)
; 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)
; 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)
; EXPECT: unsat
-; COMMAND-LINE: --sygus-out=status --decision=justification
+; COMMAND-LINE: --lang=sygus2 --sygus-out=status --decision=justification
(set-logic LIA)
(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)
; 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
; 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)
; 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
; 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)
; 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)
-
; 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)
-
; 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)
-
; EXPECT: unsat
-; COMMAND-LINE: --sygus-out=status
+; COMMAND-LINE: --lang=sygus2 --sygus-out=status
(set-logic LIA)
(synth-fun R ((y Int)) Bool)
(constraint (=> (= x e) (R x)))
(check-synth)
-
; 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)
; 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
(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)
)
(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)
)
(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)
-
; 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)
-
; 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))
)
(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)
; 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))
)
; 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)
) 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
) 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
))
-(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 (
) 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
) 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
; EXPECT: unsat\r
-; COMMAND-LINE: --sygus-fair=direct --sygus-out=status\r
+; COMMAND-LINE: --lang=sygus2 --sygus-fair=direct --sygus-out=status\r
(set-logic SLIA)\r
- \r
+\r
(synth-fun f ((col1 String) (col2 String)) String\r
- ((Start String (ntString))\r
- (ntString String (col1 col2 " " "," "USA" "PA" "CT" "CA" "MD" "NY"\r
+ ((ntString String) (ntInt Int) (ntBool Bool))\r
+ ((ntString String (col1 col2 " " "," "USA" "PA" "CT" "CA" "MD" "NY"\r
(str.++ ntString ntString)\r
(str.replace ntString ntString ntString)\r
(str.at ntString ntInt)\r
- (int.to.str ntInt)\r
+ (str.from_int ntInt)\r
(ite ntBool ntString ntString)\r
(str.substr ntString ntInt ntInt)))\r
(ntInt Int (0 1 2\r
(+ ntInt ntInt)\r
(- ntInt ntInt)\r
(str.len ntString)\r
- (str.to.int ntString)\r
+ (str.to_int ntString)\r
(str.indexof ntString ntString ntInt)))\r
(ntBool Bool (true false\r
(str.prefixof ntString ntString)\r
(str.suffixof ntString ntString)\r
(str.contains ntString ntString)))))\r
\r
-\r
(declare-var col1 String)\r
(declare-var col2 String)\r
-(constraint (= (f "UC Berkeley" "Berkeley, CA") \r
+\r
+(constraint (= (f "UC Berkeley" "Berkeley, CA")\r
"UC Berkeley, Berkeley, CA, USA"))\r
-(constraint (= (f "University of Pennsylvania" "Phialdelphia, PA, USA") \r
+(constraint (= (f "University of Pennsylvania" "Phialdelphia, PA, USA")\r
"University of Pennsylvania, Phialdelphia, PA, USA"))\r
-(constraint (= (f "UCLA" "Los Angeles, CA") \r
+(constraint (= (f "UCLA" "Los Angeles, CA")\r
"UCLA, Los Angeles, CA, USA"))\r
-(constraint (= (f "Cornell University" "Ithaca, New York, USA") \r
+(constraint (= (f "Cornell University" "Ithaca, New York, USA")\r
"Cornell University, Ithaca, New York, USA"))\r
-(constraint (= (f "Penn" "Philadelphia, PA, USA") \r
+(constraint (= (f "Penn" "Philadelphia, PA, USA")\r
"Penn, Philadelphia, PA, USA"))\r
-(constraint (= (f "University of Michigan" "Ann Arbor, MI, USA") \r
+(constraint (= (f "University of Michigan" "Ann Arbor, MI, USA")\r
"University of Michigan, Ann Arbor, MI, USA"))\r
-(constraint (= (f "UC Berkeley" "Berkeley, CA") \r
+(constraint (= (f "UC Berkeley" "Berkeley, CA")\r
"UC Berkeley, Berkeley, CA, USA"))\r
-(constraint (= (f "MIT" "Cambridge, MA") \r
+(constraint (= (f "MIT" "Cambridge, MA")\r
"MIT, Cambridge, MA, USA"))\r
-(constraint (= (f "University of Pennsylvania" "Phialdelphia, PA, USA") \r
+(constraint (= (f "University of Pennsylvania" "Phialdelphia, PA, USA")\r
"University of Pennsylvania, Phialdelphia, PA, USA"))\r
-(constraint (= (f "UCLA" "Los Angeles, CA") \r
- "UCLA, Los Angeles, CA, USA")) \r
-(constraint (= (f "University of Maryland College Park" "College Park, MD") \r
+(constraint (= (f "UCLA" "Los Angeles, CA")\r
+ "UCLA, Los Angeles, CA, USA"))\r
+(constraint (= (f "University of Maryland College Park" "College Park, MD")\r
"University of Maryland College Park, College Park, MD, USA"))\r
-(constraint (= (f "University of Michigan" "Ann Arbor, MI, USA") \r
+(constraint (= (f "University of Michigan" "Ann Arbor, MI, USA")\r
"University of Michigan, Ann Arbor, MI, USA"))\r
-(constraint (= (f "UC Berkeley" "Berkeley, CA") \r
+(constraint (= (f "UC Berkeley" "Berkeley, CA")\r
"UC Berkeley, Berkeley, CA, USA"))\r
-(constraint (= (f "MIT" "Cambridge, MA") \r
+(constraint (= (f "MIT" "Cambridge, MA")\r
"MIT, Cambridge, MA, USA"))\r
-(constraint (= (f "Rice University" "Houston, TX") \r
+(constraint (= (f "Rice University" "Houston, TX")\r
"Rice University, Houston, TX, USA"))\r
-(constraint (= (f "Yale University" "New Haven, CT, USA") \r
+(constraint (= (f "Yale University" "New Haven, CT, USA")\r
"Yale University, New Haven, CT, USA"))\r
-(constraint (= (f "Columbia University" "New York, NY, USA") \r
+(constraint (= (f "Columbia University" "New York, NY, USA")\r
"Columbia University, New York, NY, USA"))\r
-(constraint (= (f "NYU" "New York, New York, USA") \r
+(constraint (= (f "NYU" "New York, New York, USA")\r
"NYU, New York, New York, USA"))\r
-(constraint (= (f "Drexel University" "Philadelphia, PA") \r
- "Drexel University, Philadelphia, PA, USA")) \r
-(constraint (= (f "UC Berkeley" "Berkeley, CA") \r
+(constraint (= (f "Drexel University" "Philadelphia, PA")\r
+ "Drexel University, Philadelphia, PA, USA"))\r
+(constraint (= (f "UC Berkeley" "Berkeley, CA")\r
"UC Berkeley, Berkeley, CA, USA"))\r
-(constraint (= (f "UIUC" "Urbana, IL") \r
+(constraint (= (f "UIUC" "Urbana, IL")\r
"UIUC, Urbana, IL, USA"))\r
-(constraint (= (f "Temple University" "Philadelphia, PA") \r
+(constraint (= (f "Temple University" "Philadelphia, PA")\r
"Temple University, Philadelphia, PA, USA"))\r
-(constraint (= (f "Harvard University" "Cambridge, MA, USA") \r
+(constraint (= (f "Harvard University" "Cambridge, MA, USA")\r
"Harvard University, Cambridge, MA, USA"))\r
-(constraint (= (f "University of Connecticut" "Storrs, CT, USA") \r
+(constraint (= (f "University of Connecticut" "Storrs, CT, USA")\r
"University of Connecticut, Storrs, CT, USA"))\r
-(constraint (= (f "Drexel University" "Philadelphia, PA") \r
+(constraint (= (f "Drexel University" "Philadelphia, PA")\r
"Drexel University, Philadelphia, PA, USA"))\r
-(constraint (= (f "NYU" "New York, New York, USA") \r
- "NYU, New York, New York, USA")) \r
-(constraint (= (f "UIUC" "Urbana, IL") \r
- "UIUC, Urbana, IL, USA")) \r
-(constraint (= (f "New Haven University" "New Haven, CT, USA") \r
+(constraint (= (f "NYU" "New York, New York, USA")\r
+ "NYU, New York, New York, USA"))\r
+(constraint (= (f "UIUC" "Urbana, IL")\r
+ "UIUC, Urbana, IL, USA"))\r
+(constraint (= (f "New Haven University" "New Haven, CT, USA")\r
"New Haven University, New Haven, CT, USA"))\r
-(constraint (= (f "University of California, Santa Barbara" "Santa Barbara, CA, USA") \r
+(constraint (= (f "University of California, Santa Barbara" "Santa Barbara, CA, USA")\r
"University of California, Santa Barbara, Santa Barbara, CA, USA"))\r
-(constraint (= (f "University of Connecticut" "Storrs, CT, USA") \r
- "University of Connecticut, Storrs, CT, USA")) \r
- \r
+(constraint (= (f "University of Connecticut" "Storrs, CT, USA")\r
+ "University of Connecticut, Storrs, CT, USA"))\r
+\r
(check-synth)\r
; 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)
(= 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)))))
(= 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
(=
) 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)
(>=
(+
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)
(>=
(+
1))))
(let
((X5
- Bool (and
+ (and
(and
(and
(and (>= DRAGON.usr.invalid_a_0 1) (= DRAGON.usr.dirty_a_0 0))
(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
(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
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
(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
(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
(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 (
(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
(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
; 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
(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)))
(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
(get-x o1)
(+ CondInt CondInt)
(- CondInt CondInt)
- -1
+ (- 1)
0
1
2
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))))
; 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)
; 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)
)
)
-(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))
; 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)))
; 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)
; 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))
; 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))
)
)
; 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
(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
(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
(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___
) 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
(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___!
; 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)
(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)
-
; 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)
; 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
(<= 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)
-
; 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
(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)
(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)
; 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)
; EXPECT: unsat
-; COMMAND-LINE: --sygus-out=status
+; COMMAND-LINE: --lang=sygus2 --sygus-out=status
(set-logic LIA)
(constraint (= (f x y) (+ (f x x) (f y y) x 1)))
(check-synth)
-
; 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
#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)
-; 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)
(constraint (>= (g x1 x2 x3 x4 x5 x6 x7 x8 x9 x10) (+ x4 x4 x4)))
(check-synth)
-
-; 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)
(constraint (<= (f x x x x x x x x x 0) (+ x x x)))
(check-synth)
-
; 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)
(declare-var x Real)
-(constraint (and (= (f -4) -2) (= (f -9) (/ -9 2))))
+(constraint (and (= (f (- 4)) (- 2)) (= (f (- 9)) (/ (- 9) 2))))
(check-synth)
; EXPECT: unsat
-; COMMAND-LINE: --sygus-out=status
+; COMMAND-LINE: --lang=sygus2 --sygus-out=status
(set-logic ALL)
(synth-fun f ((x Int)) (Set Int))
; EXPECT: unsat
-; COMMAND-LINE: --sygus-out=status
+; COMMAND-LINE: --lang=sygus2 --sygus-out=status
(set-logic ALL)
(synth-fun f ((x String)) Int)
; 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
(constraint (= (f 0) 0))
(check-synth)
-
; 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)
(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)
(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)))))
; 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)
(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)))
;; g3: y+3
;; g4: 2y+6
;; g5: 3y+x+7
-
; 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)
projects / cvc5.git / commitdiff