diff options
Diffstat (limited to 'test/regress/regress1')
| -rw-r--r-- | test/regress/regress1/sygus/issue3498.smt2 | 7 | ||||
| -rw-r--r-- | test/regress/regress1/sygus/list_recursor.sy | 2 | ||||
| -rw-r--r-- | test/regress/regress1/sygus/once_2.sy | 44 | ||||
| -rw-r--r-- | test/regress/regress1/sygus/rec-fun-swap.sy | 76 | ||||
| -rw-r--r-- | test/regress/regress1/sygus/rec-fun-sygus.sy | 2 | ||||
| -rw-r--r-- | test/regress/regress1/sygus/rec-fun-while-1.sy | 92 | ||||
| -rw-r--r-- | test/regress/regress1/sygus/rec-fun-while-2.sy | 93 | ||||
| -rw-r--r-- | test/regress/regress1/sygus/rec-fun-while-infinite.sy | 97 |
8 files changed, 411 insertions, 2 deletions
diff --git a/test/regress/regress1/sygus/issue3498.smt2 b/test/regress/regress1/sygus/issue3498.smt2 new file mode 100644 index 000000000..9fa8fdc1e --- /dev/null +++ b/test/regress/regress1/sygus/issue3498.smt2 @@ -0,0 +1,7 @@ +; EXPECT: sat +; COMMAND-LINE: --sygus-inference --no-check-models +(set-logic ALL) +(declare-fun x () Real) +(assert (= x 1)) +(assert (= (sqrt x) x)) +(check-sat) diff --git a/test/regress/regress1/sygus/list_recursor.sy b/test/regress/regress1/sygus/list_recursor.sy index 53c55397e..2e10a0c71 100644 --- a/test/regress/regress1/sygus/list_recursor.sy +++ b/test/regress/regress1/sygus/list_recursor.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --sygus-out=status --sygus-rec-fun --lang=sygus2 --uf-ho +; COMMAND-LINE: --sygus-out=status --lang=sygus2 --uf-ho (set-logic ALL) diff --git a/test/regress/regress1/sygus/once_2.sy b/test/regress/regress1/sygus/once_2.sy new file mode 100644 index 000000000..af6d56aaf --- /dev/null +++ b/test/regress/regress1/sygus/once_2.sy @@ -0,0 +1,44 @@ +; EXPECT: unsat +; COMMAND-LINE: --lang=sygus2 --sygus-out=status +(set-logic BV) + +(define-sort Stream () (_ BitVec 2)) + +(define-fun BV_ONE () Stream (_ bv1 2)) + +(define-fun + O ( (X Stream) ) Stream + (bvneg (bvand X (bvnot (bvsub X BV_ONE)))) +) + +(synth-fun op ((x Stream)) Stream + (( y_term Stream)) + (( y_term Stream ( + ( Constant Stream) + ( Variable Stream) + ( bvnot y_term ) + ( bvand y_term y_term ) + ( bvor y_term y_term ) + ( bvneg y_term ) + ( bvadd y_term y_term ) + ( bvsub y_term y_term ) + ( bvmul y_term y_term ) + ( bvudiv y_term y_term ) + ( bvurem y_term y_term ) + ( bvshl y_term y_term ) + ( bvlshr y_term y_term ) + )) +)) + +(define-fun C ((x Stream)) Bool + (= (op x) (O x)) +) + +(constraint (and +(C (_ bv0 2)) +(C (_ bv1 2)) +(C (_ bv2 2)) +(C (_ bv3 2)) +)) + +(check-synth) diff --git a/test/regress/regress1/sygus/rec-fun-swap.sy b/test/regress/regress1/sygus/rec-fun-swap.sy new file mode 100644 index 000000000..056d6a8fc --- /dev/null +++ b/test/regress/regress1/sygus/rec-fun-swap.sy @@ -0,0 +1,76 @@ +; EXPECT: unsat +; COMMAND-LINE: --sygus-out=status --lang=sygus2 + +(set-logic ALL) + +; The environment datatypes +(declare-datatype NVars ((x) (y))) + +(declare-datatype Pair ((pair (first NVars) (second Int)))) + +(declare-datatype Env ((cons (head Pair) (tail Env)) (nil))) + +(define-fun-rec envStore ((var NVars) (value Int) (env Env)) Env + (ite (is-nil env) + (cons (pair var value) env) + (ite (= var (first (head env))) + (cons (pair var value) (tail env)) + (cons (head env) (envStore var value (tail env))) + ) + ) + ) + +(define-fun-rec envSelect ((var NVars) (env Env)) Int + (ite (is-nil env) + (- 1) + (ite (= var (first (head env))) + (second (head env)) + (envSelect var (tail env)) + ) + ) + ) + +; Syntax for arithmetic expressions +(declare-datatype Aexp + ( + (Val (val Int)) + ) + ) + +; Function to evaluate arithmetic expressions +(define-fun-rec evalA ((env Env) (a Aexp)) Int + (val a) + ) + +; Syntax for commands +(declare-datatype Com + ( + (Skip) + (Assign (lhs NVars) (rhs Aexp)) + (CSeq (cBef Com) (aAft Com)) + ) + ) + +; Function to evaluate statements +(define-fun-rec evalC ((env Env) (c Com)) Env + (ite (is-Skip c) + env + (ite (is-Assign c) + (envStore (lhs c) (evalA env (rhs c)) env) + (evalC (evalC env (cBef c)) (aAft c))) + ) + ) + +(synth-fun prog () Com + ((C Com) (V NVars) (A Aexp) (I Int)) + ( + (C Com (Skip (Assign V A) (CSeq C C))) + (V NVars (x y)) + (A Aexp ((Val I))) + (I Int (0 1)) + ) +) + +(constraint (= (evalC (cons (pair y 0) (cons (pair x 1) nil)) prog) (cons (pair y 1) (cons (pair x 0) nil)))) + +(check-synth) diff --git a/test/regress/regress1/sygus/rec-fun-sygus.sy b/test/regress/regress1/sygus/rec-fun-sygus.sy index 13d4782d4..769e173de 100644 --- a/test/regress/regress1/sygus/rec-fun-sygus.sy +++ b/test/regress/regress1/sygus/rec-fun-sygus.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --sygus-out=status --sygus-rec-fun --lang=sygus2 +; COMMAND-LINE: --sygus-out=status --lang=sygus2 (set-logic ALL) diff --git a/test/regress/regress1/sygus/rec-fun-while-1.sy b/test/regress/regress1/sygus/rec-fun-while-1.sy new file mode 100644 index 000000000..e805fdc20 --- /dev/null +++ b/test/regress/regress1/sygus/rec-fun-while-1.sy @@ -0,0 +1,92 @@ +; EXPECT: unsat +; COMMAND-LINE: --sygus-out=status --lang=sygus2 --no-check-synth-sol + +(set-logic ALL) + +; The environment datatypes +(declare-datatype NVars ((x))) + +(declare-datatype Pair ((build (first NVars) (second Int)))) + +(declare-datatype Env ((cons (head Pair) (tail Env)) (nil))) + +(define-fun-rec envStore ((var NVars) (value Int) (env Env)) Env + (ite (is-nil env) + (cons (build var value) env) + (ite (= var (first (head env))) + (cons (build var value) (tail env)) + (cons (head env) (envStore var value (tail env))) + ) + ) + ) + +(define-fun-rec envSelect ((var NVars) (env Env)) Int + (ite (is-nil env) + 0 + (ite (= var (first (head env))) + (second (head env)) + (envSelect var (tail env)) + ) + ) + ) + +; Syntax for arithmetic expressions +(declare-datatype Aexp + ( + (Val (val Int)) + (Var (name NVars)) + (Add (addL Aexp) (addR Aexp)) + ) + ) + +; Function to evaluate arithmetic expressions +(define-fun-rec evalA ((env Env) (a Aexp)) Int + (ite (is-Val a) + (val a) + (envSelect (name a) env) + )) + +; Syntax for boolean expressions +(declare-datatype Bexp + ( + (LT (ltL Aexp) (ltR Aexp)) + ) + ) + +; Function to evaluate boolean expressions +(define-fun-rec evalB ((env Env) (b Bexp)) Bool + (< (evalA env (ltL b)) (evalA env (ltR b))) + ) + +; Syntax for commands +(declare-datatype Com + ( + (Assign (lhs NVars) (rhs Aexp)) + (While (wCond Bexp) (wCom Com)) + ) + ) + +; Function to evaluate statements +(define-fun-rec evalC ((env Env) (c Com)) Env + (ite (is-Assign c) + (envStore (lhs c) (evalA env (rhs c)) env) + (ite (evalB env (wCond c)) (evalC (evalC env (wCom c)) c) env) + ) + ) + +(synth-fun prog () Com + ((C1 Com) (C2 Com) (VX NVars) (A1 Aexp) (A2 Aexp) (B Bexp) (I Int)) + ( + (C1 Com ((While B C2))) + (C2 Com ((Assign VX A2))) + (VX NVars (x)) + (A1 Aexp ((Var VX))) + (A2 Aexp ((Val I))) + (B Bexp ((LT A1 A2))) + (I Int (0 1 (+ I I))) + ) +) + +(constraint (= (evalC (cons (build x 0) nil) prog) (cons (build x 2) nil))) + +(check-synth) diff --git a/test/regress/regress1/sygus/rec-fun-while-2.sy b/test/regress/regress1/sygus/rec-fun-while-2.sy new file mode 100644 index 000000000..7e32384b3 --- /dev/null +++ b/test/regress/regress1/sygus/rec-fun-while-2.sy @@ -0,0 +1,93 @@ +; EXPECT: unsat +; COMMAND-LINE: --sygus-out=status --lang=sygus2 --no-check-synth-sol + +(set-logic ALL) + +; The environment datatypes +(declare-datatype NVars ((x) (y))) + +(declare-datatype Pair ((build (first NVars) (second Int)))) + +(declare-datatype Env ((cons (head Pair) (tail Env)) (nil))) + +(define-fun-rec envStore ((var NVars) (value Int) (env Env)) Env + (ite (is-nil env) + (cons (build var value) env) + (ite (= var (first (head env))) + (cons (build var value) (tail env)) + (cons (head env) (envStore var value (tail env))) + ) + ) + ) + +(define-fun-rec envSelect ((var NVars) (env Env)) Int + (ite (is-nil env) + 0 + (ite (= var (first (head env))) + (second (head env)) + (envSelect var (tail env)) + ) + ) + ) + +; Syntax for arithmetic expressions +(declare-datatype Aexp + ( + (Val (val Int)) + (Var (name NVars)) + (Add (addL Aexp) (addR Aexp)) + (Sub (subL Aexp) (subR Aexp)) + ) + ) + +; Function to evaluate arithmetic expressions +(define-fun-rec evalA ((env Env) (a Aexp)) Int + (ite (is-Val a) + (val a) + (envSelect (name a) env) + )) + +; Syntax for boolean expressions +(declare-datatype Bexp + ( + (GTH (geqL Aexp) (geqR Aexp)) + ) + ) + +; Function to evaluate boolean expressions +(define-fun-rec evalB ((env Env) (b Bexp)) Bool + (> (evalA env (geqL b)) (evalA env (geqR b))) + ) + +; Syntax for commands +(declare-datatype Com + ( + (Assign (lhs NVars) (rhs Aexp)) + (While (wCond Bexp) (wCom Com)) + ) + ) + +; Function to evaluate statements +(define-fun-rec evalC ((env Env) (c Com)) Env + (ite (is-Assign c) + (envStore (lhs c) (evalA env (rhs c)) env) + (ite (evalB env (wCond c)) (evalC (evalC env (wCom c)) c) env) + ) + ) + +(synth-fun prog () Com + ((C1 Com) (C2 Com) (VX NVars) (A1 Aexp) (A2 Aexp) (B Bexp) (I Int)) + ( + (C1 Com ((While B C2))) + (C2 Com ((Assign VX A2))) + (VX NVars (x)) + (A1 Aexp ((Var VX))) + (A2 Aexp ((Val I))) + (B Bexp ((GTH A2 A1))) + (I Int (2)) + ) +) + +(constraint (= (evalC (cons (build x 0) nil) prog) (cons (build x 2) nil))) + +(check-synth) diff --git a/test/regress/regress1/sygus/rec-fun-while-infinite.sy b/test/regress/regress1/sygus/rec-fun-while-infinite.sy new file mode 100644 index 000000000..b43b3d5e2 --- /dev/null +++ b/test/regress/regress1/sygus/rec-fun-while-infinite.sy @@ -0,0 +1,97 @@ +; EXPECT: unknown +; COMMAND-LINE: --sygus-out=status --lang=sygus2 --no-check-synth-sol + +(set-logic ALL) + +; The environment datatypes +(declare-datatype NVars ((x) (y))) + +(declare-datatype Pair ((build (first NVars) (second Int)))) + +(declare-datatype Env ((cons (head Pair) (tail Env)) (nil))) + +(define-fun-rec envStore ((var NVars) (value Int) (env Env)) Env + (ite (is-nil env) + (cons (build var value) env) + (ite (= var (first (head env))) + (cons (build var value) (tail env)) + (cons (head env) (envStore var value (tail env))) + ) + ) + ) + +(define-fun-rec envSelect ((var NVars) (env Env)) Int + (ite (is-nil env) + 0 + (ite (= var (first (head env))) + (second (head env)) + (envSelect var (tail env)) + ) + ) + ) + +; Syntax for arithmetic expressions +(declare-datatype Aexp + ( + (Val (val Int)) + (Var (name NVars)) + (Add (addL Aexp) (addR Aexp)) + ) + ) + +; Function to evaluate arithmetic expressions +(define-fun-rec evalA ((env Env) (a Aexp)) Int + (ite (is-Val a) + (val a) + (ite (is-Var a) + (envSelect (name a) env) + ; (is-Add a) + (+ (evalA env (addL a)) (evalA env (addR a))) + ))) + +; Syntax for boolean expressions +(declare-datatype Bexp + ( + (TRUE) + )) + +; Function to evaluate boolean expressions +(define-fun-rec evalB ((env Env) (b Bexp)) Bool + (is-TRUE b) +) + +; Syntax for commands +(declare-datatype Com + ( + (Assign (lhs NVars) (rhs Aexp)) + (While (wCond Bexp) (wCom Com)) + ) + ) + +; Function to evaluate statements +(define-fun-rec evalC ((env Env) (c Com)) Env + (ite (is-Assign c) + (envStore (lhs c) (evalA env (rhs c)) env) + ; (is-While c) + (ite (evalB env (wCond c)) (evalC (evalC env (wCom c)) c) env) + ) + ) + + +(synth-fun prog () Com + ((C1 Com) (C2 Com) (V NVars) (A1 Aexp) (A2 Aexp) (A3 Aexp) (B Bexp) (I Int)) + ( + (C1 Com ((While B C2))) + (C2 Com ((Assign V A1))) + (V NVars (x)) + (A1 Aexp ((Var V))) + (A2 Aexp ((Val I))) + (A3 Aexp ((Add A1 A2))) + (B Bexp (TRUE)) + (I Int (1)) + ) +) + +(constraint (= (evalC (cons (build x 1) nil) prog) (cons (build x 1) nil))) + +(check-synth) |