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, 136 insertions, 0 deletions

diff --git a/examples/api/cpp/combination.cpp b/examples/api/cpp/combination.cpp
new file mode 100644
index 000000000..d47897a7c
--- /dev/null
+++ b/examples/api/cpp/combination.cpp
@@ -0,0 +1,136 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Aina Niemetz, Tim King, Mudathir Mohamed
+ *
+ * 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 capabilities of cvc5
+ *
+ * A simple demonstration of how to use uninterpreted functions, combining this
+ * with arithmetic, and extracting a model at the end of a satisfiable query.
+ * The model is displayed using getValue().
+ */
+
+#include <cvc5/cvc5.h>
+
+#include <iostream>
+
+using namespace std;
+using namespace cvc5::api;
+
+void prefixPrintGetValue(Solver& slv, Term t, int level = 0)
+{
+  cout << "slv.getValue(" << t << "): " << slv.getValue(t) << endl;
+
+  for (const Term& c : t)
+  {
+    prefixPrintGetValue(slv, c, level + 1);
+  }
+}
+
+int main()
+{
+  Solver slv;
+  slv.setOption("produce-models", "true");  // Produce Models
+  slv.setOption("output-language", "cvc"); // Set the output-language to CVC's
+  slv.setOption("dag-thresh", "0"); // Disable dagifying the output
+  slv.setOption("output-language", "smt2"); // use smt-lib v2 as output language
+  slv.setLogic(string("QF_UFLIRA"));
+
+  // Sorts
+  Sort u = slv.mkUninterpretedSort("u");
+  Sort integer = slv.getIntegerSort();
+  Sort boolean = slv.getBooleanSort();
+  Sort uToInt = slv.mkFunctionSort(u, integer);
+  Sort intPred = slv.mkFunctionSort(integer, boolean);
+
+  // Variables
+  Term x = slv.mkConst(u, "x");
+  Term y = slv.mkConst(u, "y");
+
+  // Functions
+  Term f = slv.mkConst(uToInt, "f");
+  Term p = slv.mkConst(intPred, "p");
+
+  // Constants
+  Term zero = slv.mkInteger(0);
+  Term one = slv.mkInteger(1);
+
+  // Terms
+  Term f_x = slv.mkTerm(APPLY_UF, f, x);
+  Term f_y = slv.mkTerm(APPLY_UF, f, y);
+  Term sum = slv.mkTerm(PLUS, f_x, f_y);
+  Term p_0 = slv.mkTerm(APPLY_UF, p, zero);
+  Term p_f_y = slv.mkTerm(APPLY_UF, p, f_y);
+
+  // Construct the assertions
+  Term assertions = slv.mkTerm(AND,
+      vector<Term>{
+      slv.mkTerm(LEQ, zero, f_x),  // 0 <= f(x)
+      slv.mkTerm(LEQ, zero, f_y),  // 0 <= f(y)
+      slv.mkTerm(LEQ, sum, one),   // f(x) + f(y) <= 1
+      p_0.notTerm(),               // not p(0)
+      p_f_y                        // p(f(y))
+      });
+  slv.assertFormula(assertions);
+
+  cout << "Given the following assertions:" << endl
+       << assertions << endl << endl;
+
+  cout << "Prove x /= y is entailed. " << endl
+       << "cvc5: " << slv.checkEntailed(slv.mkTerm(DISTINCT, x, y)) << "."
+       << endl
+       << endl;
+
+  cout << "Call checkSat to show that the assertions are satisfiable. "
+       << endl
+       << "cvc5: "
+       << slv.checkSat() << "."<< endl << endl;
+
+  cout << "Call slv.getValue(...) on terms of interest."
+       << endl;
+  cout << "slv.getValue(" << f_x << "): " << slv.getValue(f_x) << endl;
+  cout << "slv.getValue(" << f_y << "): " << slv.getValue(f_y) << endl;
+  cout << "slv.getValue(" << sum << "): " << slv.getValue(sum) << endl;
+  cout << "slv.getValue(" << p_0 << "): " << slv.getValue(p_0) << endl;
+  cout << "slv.getValue(" << p_f_y << "): " << slv.getValue(p_f_y)
+       << endl << endl;
+
+  cout << "Alternatively, iterate over assertions and call slv.getValue(...) "
+       << "on all terms."
+       << endl;
+  prefixPrintGetValue(slv, assertions);
+
+  cout << endl;
+  cout << "You can also use nested loops to iterate over terms." << endl;
+  for (Term::const_iterator it = assertions.begin();
+       it != assertions.end();
+       ++it)
+  {
+    cout << "term: " << *it << endl;
+    for (Term::const_iterator it2 = (*it).begin();
+         it2 != (*it).end();
+         ++it2)
+    {
+      cout << " + child: " << *it2 << std::endl;
+    }
+  }
+  cout << endl;
+  cout << "Alternatively, you can also use for-each loops." << endl;
+  for (const Term& t : assertions)
+  {
+    cout << "term: " << t << endl;
+    for (const Term& c : t)
+    {
+      cout << " + child: " << c << endl;
+    }
+  }
+
+  return 0;
+}