Lazy evaluation via rec-funs of ITE expressions (#3482)

3 files changed, 187 insertions, 0 deletions

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 3c060a304..d810aa5be 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1743,6 +1743,8 @@ set(regress_1_tests
   regress1/sygus/qf_abv.smt2
   regress1/sygus/real-grammar.sy
   regress1/sygus/rec-fun-sygus.sy
+  regress1/sygus/rec-fun-while-1.sy
+  regress1/sygus/rec-fun-while-2.sy
   regress1/sygus/re-concat.sy
   regress1/sygus/repair-const-rl.sy
   regress1/sygus/simple-regexp.sy
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..c175094ee
--- /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 --sygus-rec-fun --no-e-matching --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..87a4f2a6e
--- /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 --sygus-rec-fun --no-e-matching --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)