From: Gereon Kremer <nafur42@gmail.com>
Date: Mon, 4 Oct 2021 23:46:49 +0000 (-0700)
Subject: Add sygus examples to documentation (#7303)
X-Git-Tag: cvc5-1.0.0~1125
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=ae7084ba7a16c7651d8a7b9237c903420058323e;p=cvc5.git

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.
---

diff --git a/docs/examples/sygus-fun.rst b/docs/examples/sygus-fun.rst
index 5b22ae833..02ec56577 100644
--- a/docs/examples/sygus-fun.rst
+++ b/docs/examples/sygus-fun.rst
@@ -6,3 +6,4 @@ SyGuS: Functions
     ../../examples/api/cpp/sygus-fun.cpp
     ../../examples/api/java/SygusFun.java
     ../../examples/api/python/sygus-fun.py
+    ../../examples/api/smtlib/sygus-fun.sy
diff --git a/docs/examples/sygus-grammar.rst b/docs/examples/sygus-grammar.rst
index 6c627e22f..ad22bdc85 100644
--- a/docs/examples/sygus-grammar.rst
+++ b/docs/examples/sygus-grammar.rst
@@ -6,3 +6,4 @@ SyGuS: Grammars
     ../../examples/api/cpp/sygus-grammar.cpp
     ../../examples/api/java/SygusGrammar.java
     ../../examples/api/python/sygus-grammar.py
+    ../../examples/api/smtlib/sygus-grammar.sy
diff --git a/docs/examples/sygus-inv.rst b/docs/examples/sygus-inv.rst
index 2fac909ef..54afe7727 100644
--- a/docs/examples/sygus-inv.rst
+++ b/docs/examples/sygus-inv.rst
@@ -6,3 +6,4 @@ SyGuS: Invariants
     ../../examples/api/cpp/sygus-inv.cpp
     ../../examples/api/java/SygusInv.java
     ../../examples/api/python/sygus-inv.py
+    ../../examples/api/smtlib/sygus-inv.sy
diff --git a/docs/ext/examples.py b/docs/ext/examples.py
index 7b62cee1b..42bcab3f8 100644
--- a/docs/ext/examples.py
+++ b/docs/ext/examples.py
@@ -24,6 +24,7 @@ class APIExamples(SphinxDirective):
         '.java': {'title': 'Java', 'lang': 'java'},
         '.py': {'title': 'Python', 'lang': 'python'},
         '.smt2': {'title': 'SMT-LIBv2', 'lang': 'smtlib'},
+        '.sy': {'title': 'SyGuS', 'lang': 'smtlib'},
     }
 
     # The "arguments" are actually the content of the directive
@@ -36,7 +37,7 @@ class APIExamples(SphinxDirective):
         # collect everything in a list of strings
         content = ['.. tabs::', '']
 
-        remaining = set(self.exts.keys())
+        remaining = set([self.exts[e]['lang'] for e in self.exts])
         location = '{}:{}'.format(*self.get_source_info())
 
         for file in self.content:
@@ -45,7 +46,7 @@ class APIExamples(SphinxDirective):
             if ext in self.exts:
                 title = self.exts[ext]['title']
                 lang = self.exts[ext]['lang']
-                remaining.remove(ext)
+                remaining.remove(lang)
             else:
                 self.logger.warning(f'{location} is using unknown file extension "{ext}"')
                 title = ext
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)
diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h
index 8302ce750..1c47927b7 100644
--- a/src/api/cpp/cvc5.h
+++ b/src/api/cpp/cvc5.h
@@ -935,9 +935,9 @@ class CVC5_EXPORT Op
   size_t getNumIndicesHelper() const;
 
   /**
-   * Helper for operator[](size_t i).
-   * @param i position of the index. Should be less than getNumIndicesHelper().
-   * @return the index at position i
+   * Helper for operator[](size_t index).
+   * @param index position of the index. Should be less than getNumIndicesHelper().
+   * @return the index at position index
    */
   Term getIndexHelper(size_t index) const;