Add recursive function definitions to subsolver in sygus (#6824)

This passes recursive function definitions to the verification subsolver in sygus, with a default bounded limit of 3. This required improving the interface for setting up subsolvers by allowing custom options; the sygus solver statically computes an instance of the options that it uses in all calls.

This allows us to solve non-PBE sygus problems with recursive function definitions. The PR adds an example.

2 files changed, 38 insertions, 0 deletions

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index e2e216567..260b0d9b7 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -2521,6 +2521,7 @@ set(regress_2_tests
   regress2/sygus/process-arg-invariance.sy
   regress2/sygus/real-grammar-neg.sy
   regress2/sygus/sets-fun-test.sy
+  regress2/sygus/sumn_recur_synth.sy
   regress2/sygus/strings-no-syntax-len.sy
   regress2/sygus/three.sy
   regress2/typed_v1l50016-simp.cvc
diff --git a/test/regress/regress2/sygus/sumn_recur_synth.sy b/test/regress/regress2/sygus/sumn_recur_synth.sy
new file mode 100644
index 000000000..103992dfe
--- /dev/null
+++ b/test/regress/regress2/sygus/sumn_recur_synth.sy
@@ -0,0 +1,37 @@
+; EXPECT: unsat
+; COMMAND-LINE: --lang=sygus2 --sygus-out=status
+(set-logic UFLIA)
+
+(declare-var x Int)
+(declare-var x! Int)
+(declare-var y Int)
+(declare-var y! Int)
+
+(define-fun-rec sum_n ((x Int)) Int
+                  (ite (>= x 1)
+                       (+ x (sum_n (- x 1)))
+                       0))
+
+(synth-fun inv_fun ((x Int) (y Int)) Bool
+	((C Bool) (B Bool) (E Int))
+	((C Bool ((and (>= y 1) B)))
+	 (B Bool ((= (sum_n E) E) (>= E E)))
+	 (E Int (0 1 x y (+ E E))))
+)
+
+(define-fun pre_fun ((x Int) (y Int)) Bool
+	(and (= x 0) (= y 1)))
+
+(define-fun trans_fun ((x Int) (y Int) (x! Int) (y! Int)) Bool
+	(and (<= y 2) (= x! (+ x y)) (= y! (+ y 1))))
+
+(define-fun post_fun ((x Int) (y Int)) Bool
+	(= x (sum_n (- y 1)))	
+)
+
+(constraint (=> (pre_fun x y) (inv_fun x y)))
+(constraint (=> (and (inv_fun x y) (trans_fun x y x! y!)) (inv_fun x! y!)))
+(constraint (=> (inv_fun x y) (post_fun x y)))
+
+
+(check-synth)