Add sygus examples to documentation (#7303)

For some reason, we didn't have any SMT-LIB (or rather SyGuS) example files for the SyGuS examples yet.
This PR adds these missing examples.

3 files changed, 52 insertions, 0 deletions

diff --git a/examples/api/smtlib/sygus-fun.sy b/examples/api/smtlib/sygus-fun.sy
new file mode 100644
index 000000000..171b3fe54
--- /dev/null
+++ b/examples/api/smtlib/sygus-fun.sy
@@ -0,0 +1,24 @@
+; The printed output for this example should be equivalent to:
+; (
+;   (define-fun max ((x Int) (y Int)) Int (ite (<= x y) y x))
+;   (define-fun min ((x Int) (y Int)) Int (ite (<= x y) x y))
+; )
+
+(set-logic LIA)
+(synth-fun max ((x Int) (y Int)) Int
+  ((Start Int) (StartBool Bool))
+  ((Start Int (0 1 x y
+               (+ Start Start)
+               (- Start Start)
+               (ite StartBool Start Start)))
+   (StartBool Bool ((and StartBool StartBool)
+                    (not StartBool)
+                    (<= Start Start)))))
+(synth-fun min ((x Int) (y Int)) Int)
+(declare-var x Int)
+(declare-var y Int)
+(constraint (>= (max x y) x))
+(constraint (>= (max x y) y))
+(constraint (or (= x (max x y)) (= y (max x y))))
+(constraint (= (+ (max x y) (min x y)) (+ x y)))
+(check-synth)
diff --git a/examples/api/smtlib/sygus-grammar.sy b/examples/api/smtlib/sygus-grammar.sy
new file mode 100644
index 000000000..e8c5cd5d8
--- /dev/null
+++ b/examples/api/smtlib/sygus-grammar.sy
@@ -0,0 +1,16 @@
+; The printed output for this example should look like:
+; (
+;   (define-fun id1 ((x Int)) Int (+ x (+ x (- x))))
+;   (define-fun id2 ((x Int)) Int x)
+;   (define-fun id3 ((x Int)) Int (+ x 0))
+;   (define-fun id4 ((x Int)) Int (+ x (+ x (- x))))
+; )
+
+(set-logic LIA)
+(synth-fun id1 ((x Int)) Int ((Start Int)) ((Start Int ((- x) (+ x Start)))))
+(synth-fun id2 ((x Int)) Int ((Start Int)) ((Start Int ((Variable Int) (- x) (+ x Start)))))
+(synth-fun id3 ((x Int)) Int ((Start Int)) ((Start Int (0 (- x) (+ x Start)))))
+(synth-fun id4 ((x Int)) Int ((Start Int)) ((Start Int ((- x) (+ x Start)))))
+(declare-var x Int)
+(constraint (= (id1 x) (id2 x) (id3 x) (id4 x) x))
+(check-synth)
diff --git a/examples/api/smtlib/sygus-inv.sy b/examples/api/smtlib/sygus-inv.sy
new file mode 100644
index 000000000..6d284df44
--- /dev/null
+++ b/examples/api/smtlib/sygus-inv.sy
@@ -0,0 +1,12 @@
+; The printed output for this example should be equivalent to:
+; (
+;   (define-fun inv-f ((x Int)) Bool (not (>= x 11)))
+; )
+
+(set-logic LIA)
+(synth-inv inv-f ((x Int)))
+(define-fun pre-f ((x Int)) Bool (= x 0))
+(define-fun trans-f ((x Int) (xp Int)) Bool (ite (< x 10) (= xp (+ x 1)) (= xp x)))
+(define-fun post-f ((x Int)) Bool (<= x 10))
+(inv-constraint inv-f pre-f trans-f post-f)
+(check-synth)