Enable sygusRecFun by default and fixes SyGuS+RecFun+HO issues (#3502)

6 files changed, 81 insertions, 5 deletions

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/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
index c175094ee..e805fdc20 100644
--- a/test/regress/regress1/sygus/rec-fun-while-1.sy
+++ b/test/regress/regress1/sygus/rec-fun-while-1.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --sygus-out=status --lang=sygus2 --sygus-rec-fun --no-e-matching --no-check-synth-sol
+; COMMAND-LINE: --sygus-out=status --lang=sygus2 --no-check-synth-sol
 
 (set-logic ALL)
 
diff --git a/test/regress/regress1/sygus/rec-fun-while-2.sy b/test/regress/regress1/sygus/rec-fun-while-2.sy
index 87a4f2a6e..7e32384b3 100644
--- a/test/regress/regress1/sygus/rec-fun-while-2.sy
+++ b/test/regress/regress1/sygus/rec-fun-while-2.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --sygus-out=status --lang=sygus2 --sygus-rec-fun --no-e-matching --no-check-synth-sol
+; COMMAND-LINE: --sygus-out=status --lang=sygus2 --no-check-synth-sol
 
 (set-logic ALL)
 
diff --git a/test/regress/regress1/sygus/rec-fun-while-infinite.sy b/test/regress/regress1/sygus/rec-fun-while-infinite.sy
index 85f8268c5..b43b3d5e2 100644
--- a/test/regress/regress1/sygus/rec-fun-while-infinite.sy
+++ b/test/regress/regress1/sygus/rec-fun-while-infinite.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unknown
-; COMMAND-LINE: --sygus-out=status --lang=sygus2 --sygus-rec-fun --no-e-matching --no-check-synth-sol
+; COMMAND-LINE: --sygus-out=status --lang=sygus2 --no-check-synth-sol
 
 (set-logic ALL)