Fix mistakes in sygus API comments. (#4520)

diff --git a/examples/api/sygus-fun.cpp b/examples/api/sygus-fun.cpp
index 6c47ec71597a2d593e67a7a880982c104aa78c6c..449d8d060a8e6994b32da7580a6d66af85ffd1bd 100644 (file)
--- a/examples/api/sygus-fun.cpp
+++ b/examples/api/sygus-fun.cpp
@@ -65,7 +65,7 @@ int main()
   Sort integer = slv.getIntegerSort();
   Sort boolean = slv.getBooleanSort();
 
-  // declare input variables for the function-to-synthesize
+  // declare input variables for the functions-to-synthesize
   Term x = slv.mkVar(integer, "x");
   Term y = slv.mkVar(integer, "y");
 
@@ -92,7 +92,7 @@ int main()
   g.addRules(start, {zero, one, x, y, plus, minus, ite});
   g.addRules(start_bool, {And, Not, leq});
 
-  // declare the function-to-synthesize. Optionally, provide the grammar
+  // declare the functions-to-synthesize. Optionally, provide the grammar
   // constraints
   Term max = slv.synthFun("max", {x, y}, integer, g);
   Term min = slv.synthFun("min", {x, y}, integer);
@@ -104,7 +104,7 @@ int main()
   Term max_x_y = slv.mkTerm(APPLY_UF, max, varX, varY);
   Term min_x_y = slv.mkTerm(APPLY_UF, min, varX, varY);
 
-  // add logical constraints
+  // add semantic constraints
   // (constraint (>= (max x y) x))
   slv.addSygusConstraint(slv.mkTerm(GEQ, max_x_y, varX));
 

diff --git a/examples/api/sygus-grammar.cpp b/examples/api/sygus-grammar.cpp
index c2e624c1fc1d202fcccd7e4d841f6f73b501e95c..8536706ce18ccadca348e49524ae58b09aeea15a 100644 (file)
--- a/examples/api/sygus-grammar.cpp
+++ b/examples/api/sygus-grammar.cpp
@@ -11,8 +11,9 @@
  **
  ** \brief A simple demonstration of the Sygus API.
  **
- ** A simple demonstration of how to use the Sygus API to synthesize max and min
- ** functions. Here is the same problem written in Sygus V2 format:
+ ** A simple demonstration of how to use Grammar to add syntax constraints to
+ ** the Sygus solution for the identity function. Here is the same problem
+ ** written in Sygus V2 format:
  **
  ** (set-logic LIA)
  **
@@ -34,9 +35,11 @@
  **
  ** (check-synth)
  **
- ** The printed output to 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))
+ ** The printed output to 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))))
  **/
 
 #include <cvc4/api/cvc4cpp.h>
@@ -59,10 +62,10 @@ int main()
   Sort integer = slv.getIntegerSort();
   Sort boolean = slv.getBooleanSort();
 
-  // declare input variables for the function-to-synthesize
+  // declare input variable for the function-to-synthesize
   Term x = slv.mkVar(integer, "x");
 
-  // declare the grammar non-terminals
+  // declare the grammar non-terminal
   Term start = slv.mkVar(integer, "Start");
 
   // define the rules
@@ -80,10 +83,10 @@ int main()
   Grammar g2 = g1;
   Grammar g3 = g1;
 
-  // add parameters as rules to the start symbol. Similar to "(Variable Int)"
+  // add parameters as rules for the start symbol. Similar to "(Variable Int)"
   g2.addAnyVariable(start);
 
-  // declare the function-to-synthesizse
+  // declare the functions-to-synthesize
   Term id1 = slv.synthFun("id1", {x}, integer, g1);
   Term id2 = slv.synthFun("id2", {x}, integer, g2);
 
@@ -102,8 +105,8 @@ int main()
   Term id3_x = slv.mkTerm(APPLY_UF, id3, varX);
   Term id4_x = slv.mkTerm(APPLY_UF, id4, varX);
 
-  // add logical constraints
-  // (constraint (= (id1 x) (id2 x) x))
+  // add semantic constraints
+  // (constraint (= (id1 x) (id2 x) (id3 x) (id4 x) x))
   slv.addSygusConstraint(slv.mkTerm(EQUAL, {id1_x, id2_x, id3_x, id4_x, varX}));
 
   // print solutions if available

diff --git a/examples/api/sygus-inv.cpp b/examples/api/sygus-inv.cpp
index 061ad8c1f1fa4ab5a642a0d7699c4598748a9423..7deb5cc8315cfcee5287d49d28c888c0cfbb1e1d 100644 (file)
--- a/examples/api/sygus-inv.cpp
+++ b/examples/api/sygus-inv.cpp
@@ -72,7 +72,7 @@ int main()
   Term trans_f = slv.defineFun("trans-f", {x, xp}, boolean, ite);
   Term post_f = slv.defineFun("post-f", {x}, boolean, slv.mkTerm(LEQ, x, ten));
 
-  // declare the invariant-to-synthesize.
+  // declare the invariant-to-synthesize
   Term inv_f = slv.synthInv("inv-f", {x});
 
   slv.addSygusInvConstraint(inv_f, pre_f, trans_f, post_f);