Add more examples to the documentation (#6569)

This PR adds (most of) the existing examples to the documentation, and does some other minor updates on the documentation. Some details:
- for consistency, all cpp examples are moved from examples/api to examples/api/cpp
- add capabilities for SMT-LIB examples, and two simple smt2 examples
- more docs/examples/*.rst files
- two new documentation categories: installation (how to obtain, compile and install cvc5) and binary (about the cvc5 binary)

1 files changed, 132 insertions, 0 deletions

diff --git a/examples/api/cpp/sygus-grammar.cpp b/examples/api/cpp/sygus-grammar.cpp
new file mode 100644
index 000000000..ce5a1bc8b
--- /dev/null
+++ b/examples/api/cpp/sygus-grammar.cpp
@@ -0,0 +1,132 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Abdalrhman Mohamed, Mudathir Mohamed, Aina Niemetz
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ * in the top-level source directory and their institutional affiliations.
+ * All rights reserved.  See the file COPYING in the top-level source
+ * directory for licensing information.
+ * ****************************************************************************
+ *
+ * A simple demonstration of the Sygus API.
+ *
+ * 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)
+ *
+ * (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)
+ *
+ * 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))))
+ * )
+ */
+
+#include <cvc5/cvc5.h>
+
+#include <iostream>
+
+#include "utils.h"
+
+using namespace cvc5::api;
+
+int main()
+{
+  Solver slv;
+
+  // required options
+  slv.setOption("lang", "sygus2");
+  slv.setOption("incremental", "false");
+
+  // set the logic
+  slv.setLogic("LIA");
+
+  Sort integer = slv.getIntegerSort();
+  Sort boolean = slv.getBooleanSort();
+
+  // declare input variable for the function-to-synthesize
+  Term x = slv.mkVar(integer, "x");
+
+  // declare the grammar non-terminal
+  Term start = slv.mkVar(integer, "Start");
+
+  // define the rules
+  Term zero = slv.mkInteger(0);
+  Term neg_x = slv.mkTerm(UMINUS, x);
+  Term plus = slv.mkTerm(PLUS, x, start);
+
+  // create the grammar object
+  Grammar g1 = slv.mkSygusGrammar({x}, {start});
+
+  // bind each non-terminal to its rules
+  g1.addRules(start, {neg_x, plus});
+
+  // copy the first grammar with all of its non-termainals and their rules
+  Grammar g2 = g1;
+  Grammar g3 = g1;
+
+  // add parameters as rules for the start symbol. Similar to "(Variable Int)"
+  g2.addAnyVariable(start);
+
+  // declare the functions-to-synthesize
+  Term id1 = slv.synthFun("id1", {x}, integer, g1);
+  Term id2 = slv.synthFun("id2", {x}, integer, g2);
+
+  g3.addRule(start, zero);
+
+  Term id3 = slv.synthFun("id3", {x}, integer, g3);
+
+  // g1 is reusable as long as it remains unmodified after first use
+  Term id4 = slv.synthFun("id4", {x}, integer, g1);
+
+  // declare universal variables.
+  Term varX = slv.mkSygusVar(integer, "x");
+
+  Term id1_x = slv.mkTerm(APPLY_UF, id1, varX);
+  Term id2_x = slv.mkTerm(APPLY_UF, id2, varX);
+  Term id3_x = slv.mkTerm(APPLY_UF, id3, varX);
+  Term id4_x = slv.mkTerm(APPLY_UF, id4, varX);
+
+  // 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
+  if (slv.checkSynth().isUnsat())
+  {
+    // Output should be equivalent to:
+    // (
+    //   (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))))
+    // )
+    std::vector<Term> terms = {id1, id2, id3, id4};
+    printSynthSolutions(terms, slv.getSynthSolutions(terms));
+  }
+
+  return 0;
+}