Merge branch 'master' into rmTearDownIncrementalrmTearDownIncremental

11 files changed, 205 insertions, 34 deletions

diff --git a/examples/api/cpp/CMakeLists.txt b/examples/api/cpp/CMakeLists.txt
index bff7caa4d..6f66fdc5f 100644
--- a/examples/api/cpp/CMakeLists.txt
+++ b/examples/api/cpp/CMakeLists.txt
@@ -24,6 +24,7 @@ set(CVC5_EXAMPLES_API
   sets
   sequences
   strings
+  quickstart 
 )
 
 foreach(example ${CVC5_EXAMPLES_API})
diff --git a/examples/api/cpp/bitvectors.cpp b/examples/api/cpp/bitvectors.cpp
index 8768bd996..51f438a2d 100644
--- a/examples/api/cpp/bitvectors.cpp
+++ b/examples/api/cpp/bitvectors.cpp
@@ -10,7 +10,7 @@
  * directory for licensing information.
  * ****************************************************************************
  *
- * A simple demonstration of the solving capabilities of the CVC4
+ * A simple demonstration of the solving capabilities of the cvc5
  * bit-vector solver.
  *
  */
@@ -43,7 +43,7 @@ int main()
   //
   //(2) x = a + b - x;
   //
-  // We will use CVC4 to prove that the three pieces of code above are all
+  // We will use cvc5 to prove that the three pieces of code above are all
   // equivalent by encoding the problem in the bit-vector theory.
 
   // Creating a bit-vector type of width 32
@@ -73,7 +73,7 @@ int main()
   Term assignment0 = slv.mkTerm(EQUAL, new_x, ite);
 
   // Assert the encoding of code (0)
-  cout << "Asserting " << assignment0 << " to CVC4 " << endl;
+  cout << "Asserting " << assignment0 << " to cvc5 " << endl;
   slv.assertFormula(assignment0);
   cout << "Pushing a new context." << endl;
   slv.push();
@@ -83,14 +83,14 @@ int main()
   Term a_xor_b_xor_x = slv.mkTerm(BITVECTOR_XOR, a, b, x);
   Term assignment1 = slv.mkTerm(EQUAL, new_x_, a_xor_b_xor_x);
 
-  // Assert encoding to CVC4 in current context;
-  cout << "Asserting " << assignment1 << " to CVC4 " << endl;
+  // Assert encoding to cvc5 in current context;
+  cout << "Asserting " << assignment1 << " to cvc5 " << endl;
   slv.assertFormula(assignment1);
   Term new_x_eq_new_x_ = slv.mkTerm(EQUAL, new_x, new_x_);
 
   cout << " Check entailment assuming: " << new_x_eq_new_x_ << endl;
   cout << " Expect ENTAILED. " << endl;
-  cout << " CVC4: " << slv.checkEntailed(new_x_eq_new_x_) << endl;
+  cout << " cvc5: " << slv.checkEntailed(new_x_eq_new_x_) << endl;
   cout << " Popping context. " << endl;
   slv.pop();
 
@@ -100,19 +100,19 @@ int main()
   Term a_plus_b_minus_x = slv.mkTerm(BITVECTOR_SUB, a_plus_b, x);
   Term assignment2 = slv.mkTerm(EQUAL, new_x_, a_plus_b_minus_x);
 
-  // Assert encoding to CVC4 in current context;
-  cout << "Asserting " << assignment2 << " to CVC4 " << endl;
+  // Assert encoding to cvc5 in current context;
+  cout << "Asserting " << assignment2 << " to cvc5 " << endl;
   slv.assertFormula(assignment2);
 
   cout << " Check entailment assuming: " << new_x_eq_new_x_ << endl;
   cout << " Expect ENTAILED. " << endl;
-  cout << " CVC4: " << slv.checkEntailed(new_x_eq_new_x_) << endl;
+  cout << " cvc5: " << slv.checkEntailed(new_x_eq_new_x_) << endl;
 
   Term x_neq_x = slv.mkTerm(EQUAL, x, x).notTerm();
   std::vector<Term> v{new_x_eq_new_x_, x_neq_x};
   cout << " Check entailment assuming: " << v << endl;
   cout << " Expect NOT_ENTAILED. " << endl;
-  cout << " CVC4: " << slv.checkEntailed(v) << endl;
+  cout << " cvc5: " << slv.checkEntailed(v) << endl;
 
   // Assert that a is odd
   Op extract_op = slv.mkOp(BITVECTOR_EXTRACT, 0, 0);
@@ -123,6 +123,6 @@ int main()
   cout << "Check satisfiability." << endl;
   slv.assertFormula(a_odd);
   cout << " Expect sat. " << endl;
-  cout << " CVC4: " << slv.checkSat() << endl;
+  cout << " cvc5: " << slv.checkSat() << endl;
   return 0;
 }
diff --git a/examples/api/cpp/bitvectors_and_arrays.cpp b/examples/api/cpp/bitvectors_and_arrays.cpp
index 547b294a0..6b58daf1b 100644
--- a/examples/api/cpp/bitvectors_and_arrays.cpp
+++ b/examples/api/cpp/bitvectors_and_arrays.cpp
@@ -10,7 +10,7 @@
  * directory for licensing information.
  * ****************************************************************************
  *
- * A simple demonstration of the solving capabilities of the CVC4
+ * A simple demonstration of the solving capabilities of the cvc5
  * bit-vector and array solvers.
  *
  */
@@ -84,10 +84,10 @@ int main()
 
   Term query = slv.mkTerm(NOT, slv.mkTerm(AND, assertions));
 
-  cout << "Asserting " << query << " to CVC4 " << endl;
+  cout << "Asserting " << query << " to cvc5 " << endl;
   slv.assertFormula(query);
   cout << "Expect sat. " << endl;
-  cout << "CVC4: " << slv.checkSatAssuming(slv.mkTrue()) << endl;
+  cout << "cvc5: " << slv.checkSatAssuming(slv.mkTrue()) << endl;
 
   // Getting the model
   cout << "The satisfying model is: " << endl;
diff --git a/examples/api/cpp/datatypes.cpp b/examples/api/cpp/datatypes.cpp
index 76c6da0f0..1ba9beaf1 100644
--- a/examples/api/cpp/datatypes.cpp
+++ b/examples/api/cpp/datatypes.cpp
@@ -10,7 +10,7 @@
  * directory for licensing information.
  * ****************************************************************************
  *
- * An example of using inductive datatypes in CVC4.
+ * An example of using inductive datatypes in cvc5.
  */
 
 #include <cvc5/cvc5.h>
@@ -127,7 +127,7 @@ void test(Solver& slv, Sort& consListSort)
   std::cout << "Assert " << assertion << std::endl;
   slv.assertFormula(assertion);
   std::cout << "Expect sat." << std::endl;
-  std::cout << "CVC4: " << slv.checkSat() << std::endl;
+  std::cout << "cvc5: " << slv.checkSat() << std::endl;
 }
 
 int main()
@@ -153,7 +153,7 @@ int main()
   std::cout << "spec is:" << std::endl << consListSpec << std::endl;
 
   // Keep in mind that "DatatypeDecl" is the specification class for
-  // datatypes---"DatatypeDecl" is not itself a CVC4 Sort.
+  // datatypes---"DatatypeDecl" is not itself a cvc5 Sort.
   // Now that our Datatype is fully specified, we can get a Sort for it.
   // This step resolves the "SelfSort" reference and creates
   // symbols for all the constructors, etc.
diff --git a/examples/api/cpp/extract.cpp b/examples/api/cpp/extract.cpp
index d21c59d59..b5de58d26 100644
--- a/examples/api/cpp/extract.cpp
+++ b/examples/api/cpp/extract.cpp
@@ -10,7 +10,7 @@
  * directory for licensing information.
  * ****************************************************************************
  *
- * A simple demonstration of the solving capabilities of the CVC4
+ * A simple demonstration of the solving capabilities of the cvc5
  * bit-vector solver.
  *
  */
@@ -50,7 +50,7 @@ int main()
   Term eq2 = slv.mkTerm(EQUAL, x_31_31, x_0_0);
   cout << " Check entailment assuming: " << eq2 << endl;
   cout << " Expect ENTAILED. " << endl;
-  cout << " CVC4: " << slv.checkEntailed(eq2) << endl;
+  cout << " cvc5: " << slv.checkEntailed(eq2) << endl;
 
   return 0;
 }
diff --git a/examples/api/cpp/helloworld.cpp b/examples/api/cpp/helloworld.cpp
index 21eb8e8fc..3d11d1bd0 100644
--- a/examples/api/cpp/helloworld.cpp
+++ b/examples/api/cpp/helloworld.cpp
@@ -10,7 +10,7 @@
  * directory for licensing information.
  * ****************************************************************************
  *
- * A very simple CVC4 example.
+ * A very simple cvc5 example.
  */
 
 #include <cvc5/cvc5.h>
diff --git a/examples/api/cpp/linear_arith.cpp b/examples/api/cpp/linear_arith.cpp
index 02ddd956c..979959d21 100644
--- a/examples/api/cpp/linear_arith.cpp
+++ b/examples/api/cpp/linear_arith.cpp
@@ -11,7 +11,7 @@
  * ****************************************************************************
  *
  * A simple demonstration of the linear arithmetic solving capabilities and
- * the push pop of CVC4. This also gives an example option.
+ * the push pop of cvc5. This also gives an example option.
  */
 
 #include <iostream>
@@ -60,9 +60,9 @@ int main()
 
   slv.push();
   Term diff_leq_two_thirds = slv.mkTerm(LEQ, diff, two_thirds);
-  cout << "Prove that " << diff_leq_two_thirds << " with CVC4." << endl;
-  cout << "CVC4 should report ENTAILED." << endl;
-  cout << "Result from CVC4 is: " << slv.checkEntailed(diff_leq_two_thirds)
+  cout << "Prove that " << diff_leq_two_thirds << " with cvc5." << endl;
+  cout << "cvc5 should report ENTAILED." << endl;
+  cout << "Result from cvc5 is: " << slv.checkEntailed(diff_leq_two_thirds)
        << endl;
   slv.pop();
 
@@ -72,9 +72,9 @@ int main()
   Term diff_is_two_thirds = slv.mkTerm(EQUAL, diff, two_thirds);
   slv.assertFormula(diff_is_two_thirds);
   cout << "Show that the assertions are consistent with " << endl;
-  cout << diff_is_two_thirds << " with CVC4." << endl;
-  cout << "CVC4 should report SAT." << endl;
-  cout << "Result from CVC4 is: " << slv.checkSat() << endl;
+  cout << diff_is_two_thirds << " with cvc5." << endl;
+  cout << "cvc5 should report SAT." << endl;
+  cout << "Result from cvc5 is: " << slv.checkSat() << endl;
   slv.pop();
 
   cout << "Thus the maximum value of (y - x) is 2/3."<< endl;
diff --git a/examples/api/cpp/quickstart.cpp b/examples/api/cpp/quickstart.cpp
new file mode 100644
index 000000000..5d4849bc0
--- /dev/null
+++ b/examples/api/cpp/quickstart.cpp
@@ -0,0 +1,170 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Yoni Zohar
+ *
+ * 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 api capabilities of cvc5.
+ *
+ */
+
+#include <cvc5/cvc5.h>
+
+#include <iostream>
+
+using namespace std;
+using namespace cvc5::api;
+
+int main()
+{
+  // Create a solver
+  Solver solver;
+
+  // We will ask the solver to produce models and unsat cores,
+  // hence these options should be turned on.
+  solver.setOption("produce-models", "true");
+  solver.setOption("produce-unsat-cores", "true");
+
+  // The simplest way to set a logic for the solver is to choose "ALL".
+  // This enables all logics in the solver.
+  // Alternatively, "QF_ALL" enables all logics without quantifiers.
+  // To optimize the solver's behavior for a more specific logic,
+  // use the logic name, e.g. "QF_BV" or "QF_AUFBV".
+
+  // Set the logic
+  solver.setLogic("ALL");
+
+  // In this example, we will define constraints over reals and integers.
+  // Hence, we first obtain the corresponding sorts.
+  Sort realSort = solver.getRealSort();
+  Sort intSort = solver.getIntegerSort();
+
+  // x and y will be real variables, while a and b will be integer variables.
+  // Formally, their cpp type is Term,
+  // and they are called "constants" in SMT jargon:
+  Term x = solver.mkConst(realSort, "x");
+  Term y = solver.mkConst(realSort, "y");
+  Term a = solver.mkConst(intSort, "a");
+  Term b = solver.mkConst(intSort, "b");
+
+  // Our constraints regarding x and y will be:
+  //
+  //   (1)  0 < x
+  //   (2)  0 < y
+  //   (3)  x + y < 1
+  //   (4)  x <= y
+  //
+
+  // Formally, constraints are also terms. Their sort is Boolean.
+  // We will construct these constraints gradually,
+  // by defining each of their components.
+  // We start with the constant numerals 0 and 1:
+  Term zero = solver.mkReal(0);
+  Term one = solver.mkReal(1);
+
+  // Next, we construct the term x + y
+  Term xPlusY = solver.mkTerm(PLUS, x, y);
+
+  // Now we can define the constraints.
+  // They use the operators +, <=, and <.
+  // In the API, these are denoted by PLUS, LEQ, and LT.
+  // A list of available operators is available in:
+  // src/api/cpp/cvc5_kind.h
+  Term constraint1 = solver.mkTerm(LT, zero, x);
+  Term constraint2 = solver.mkTerm(LT, zero, y);
+  Term constraint3 = solver.mkTerm(LT, xPlusY, one);
+  Term constraint4 = solver.mkTerm(LEQ, x, y);
+
+  // Now we assert the constraints to the solver.
+  solver.assertFormula(constraint1);
+  solver.assertFormula(constraint2);
+  solver.assertFormula(constraint3);
+  solver.assertFormula(constraint4);
+
+  // Check if the formula is satisfiable, that is,
+  // are there real values for x,y,z that satisfy all the constraints?
+  Result r1 = solver.checkSat();
+
+  // The result is either SAT, UNSAT, or UNKNOWN.
+  // In this case, it is SAT.
+  std::cout << "expected: sat" << std::endl;
+  std::cout << "result:" << r1 << std::endl;
+
+  // We can get the values for x and y that satisfy the constraints.
+  Term xVal = solver.getValue(x);
+  Term yVal = solver.getValue(y);
+
+  // It is also possible to get values for compound terms,
+  // even if those did not appear in the original formula.
+  Term xMinusY = solver.mkTerm(MINUS, x, y);
+  Term xMinusYVal = solver.getValue(xMinusY);
+
+  // We can now obtain thestring representations of the values.
+  std::string xStr = xVal.getRealValue();
+  std::string yStr = yVal.getRealValue();
+  std::string xMinusYStr = xMinusYVal.getRealValue();
+
+  std::cout << "value for x: " << xStr << std::endl;
+  std::cout << "value for y: " << yStr << std::endl;
+  std::cout << "value for x - y: " << xMinusYStr << std::endl;
+
+  // Further, we can convert the values to cpp types,
+  // using standard cpp conversion functions.
+  double xDouble = std::stod(xStr);
+  double yDouble = std::stod(yStr);
+  double xMinusYDouble = std::stod(xMinusYStr);
+
+  // Another way to independently compute the value of x and y would be using
+  // the ordinary cpp minus operator instead of asking the solver.
+  // However, for more complex terms,
+  // it is easier to let the solver do the evaluation.
+  double xMinusYComputed = xDouble - yDouble;
+  if (xMinusYComputed == xMinusYDouble)
+  {
+    std::cout << "computed correctly" << std::endl;
+  }
+  else
+  {
+    std::cout << "computed incorrectly" << std::endl;
+  }
+
+  // Next, we will check satisfiability of the same formula,
+  // only this time over integer variables a and b.
+
+  // We start by resetting assertions added to the solver.
+  solver.resetAssertions();
+
+  // Next, we assert the same assertions above with integers.
+  // This time, we inline the construction of terms
+  // to the assertion command.
+  solver.assertFormula(solver.mkTerm(LT, solver.mkInteger(0), a));
+  solver.assertFormula(solver.mkTerm(LT, solver.mkInteger(0), b));
+  solver.assertFormula(
+      solver.mkTerm(LT, solver.mkTerm(PLUS, a, b), solver.mkInteger(1)));
+  solver.assertFormula(solver.mkTerm(LEQ, a, b));
+
+  // We check whether the revised assertion is satisfiable.
+  Result r2 = solver.checkSat();
+
+  // This time the formula is unsatisfiable
+  std::cout << "expected: unsat" << std::endl;
+  std::cout << "result: " << r2 << std::endl;
+
+  // We can query the solver for an unsatisfiable core, i.e., a subset
+  // of the assertions that is already unsatisfiable.
+  std::vector<Term> unsatCore = solver.getUnsatCore();
+  std::cout << "unsat core size: " << unsatCore.size() << std::endl;
+  std::cout << "unsat core: " << std::endl;
+  for (const Term& t : unsatCore)
+  {
+    std::cout << t << std::endl;
+  }
+
+  return 0;
+}
diff --git a/examples/api/cpp/sequences.cpp b/examples/api/cpp/sequences.cpp
index 5ee66048f..40cacf5c7 100644
--- a/examples/api/cpp/sequences.cpp
+++ b/examples/api/cpp/sequences.cpp
@@ -10,7 +10,7 @@
  * directory for licensing information.
  * ****************************************************************************
  *
- * A simple demonstration of reasoning about sequences with CVC4 via C++ API.
+ * A simple demonstration of reasoning about sequences with cvc5 via C++ API.
  */
 
 #include <cvc5/cvc5.h>
@@ -57,7 +57,7 @@ int main()
 
   // check sat
   Result result = slv.checkSatAssuming(q);
-  std::cout << "CVC4 reports: " << q << " is " << result << "." << std::endl;
+  std::cout << "cvc5 reports: " << q << " is " << result << "." << std::endl;
 
   if (result.isSat())
   {
diff --git a/examples/api/cpp/sets.cpp b/examples/api/cpp/sets.cpp
index c1eded4a4..1f3a1683c 100644
--- a/examples/api/cpp/sets.cpp
+++ b/examples/api/cpp/sets.cpp
@@ -51,7 +51,7 @@ int main()
 
     Term theorem = slv.mkTerm(EQUAL, lhs, rhs);
 
-    cout << "CVC4 reports: " << theorem << " is " << slv.checkEntailed(theorem)
+    cout << "cvc5 reports: " << theorem << " is " << slv.checkEntailed(theorem)
          << "." << endl;
   }
 
@@ -62,7 +62,7 @@ int main()
 
     Term theorem = slv.mkTerm(SUBSET, emptyset, A);
 
-    cout << "CVC4 reports: " << theorem << " is " << slv.checkEntailed(theorem)
+    cout << "cvc5 reports: " << theorem << " is " << slv.checkEntailed(theorem)
          << "." << endl;
   }
 
@@ -84,7 +84,7 @@ int main()
     Term e = slv.mkTerm(MEMBER, x, intersection);
 
     Result result = slv.checkSatAssuming(e);
-    cout << "CVC4 reports: " << e << " is " << result << "." << endl;
+    cout << "cvc5 reports: " << e << " is " << result << "." << endl;
 
     if (result.isSat())
     {
diff --git a/examples/api/cpp/strings.cpp b/examples/api/cpp/strings.cpp
index a952b31d1..01e384ee7 100644
--- a/examples/api/cpp/strings.cpp
+++ b/examples/api/cpp/strings.cpp
@@ -10,7 +10,7 @@
  * directory for licensing information.
  * ****************************************************************************
  *
- * A simple demonstration of reasoning about strings with CVC4 via C++ API.
+ * A simple demonstration of reasoning about strings with cvc5 via C++ API.
  */
 
 #include <cvc5/cvc5.h>
@@ -84,7 +84,7 @@ int main()
 
   // check sat
   Result result = slv.checkSatAssuming(q);
-  std::cout << "CVC4 reports: " << q << " is " << result << "." << std::endl;
+  std::cout << "cvc5 reports: " << q << " is " << result << "." << std::endl;
 
   if(result.isSat())
   {