Header for new C++ API. (#1697)

9 files changed, 893 insertions, 0 deletions

diff --git a/examples/api/bitvectors-new.cpp b/examples/api/bitvectors-new.cpp
new file mode 100644
index 000000000..596d0b515
--- /dev/null
+++ b/examples/api/bitvectors-new.cpp
@@ -0,0 +1,130 @@
+/*********************                                                        */
+/*! \file bitvectors.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Aina Niemetz, Liana Hadarean, Morgan Deters
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2018 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.\endverbatim
+ **
+ ** \brief A simple demonstration of the solving capabilities of the CVC4
+ ** bit-vector solver.
+ **
+ **/
+
+#include <iostream>
+
+//#include <cvc4/cvc4.h> // use this after CVC4 is properly installed
+#include "api/cvc4cpp.h"
+
+using namespace std;
+using namespace CVC4::api;
+
+int main()
+{
+
+  Solver slv;
+  slv.setLogic("QF_BV"); // Set the logic
+
+  // The following example has been adapted from the book A Hacker's Delight by
+  // Henry S. Warren.
+  //
+  // Given a variable x that can only have two values, a or b. We want to
+  // assign to x a value other than the current one. The straightforward code
+  // to do that is:
+  //
+  //(0) if (x == a ) x = b;
+  //    else x = a;
+  //
+  // Two more efficient yet equivalent methods are:
+  //
+  //(1) x = a ⊕ b ⊕ x;
+  //
+  //(2) x = a + b - x;
+  //
+  // We will use CVC4 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
+  Sort bitvector32 = slv.mkBitVectorSort(32);
+
+  std::cout << "bitvector32 " << bitvector32 << std::endl;
+  // Variables
+  Term x = slv.mkVar("x", bitvector32);
+  std::cout << "bitvector32 " << bitvector32 << std::endl;
+  Term a = slv.mkVar("a", bitvector32);
+  Term b = slv.mkVar("b", bitvector32);
+
+  // First encode the assumption that x must be equal to a or b
+  Term x_eq_a = slv.mkTerm(EQUAL, x, a);
+  Term x_eq_b = slv.mkTerm(EQUAL, x, b);
+  Term assumption = slv.mkTerm(OR, x_eq_a, x_eq_b);
+
+  // Assert the assumption
+  slv.assertFormula(assumption);
+
+  // Introduce a new variable for the new value of x after assignment.
+  Term new_x = slv.mkVar("new_x", bitvector32); // x after executing code (0)
+  Term new_x_ = slv.mkVar("new_x_", bitvector32); // x after executing code (1) or (2)
+
+  // Encoding code (0)
+  // new_x = x == a ? b : a;
+  Term ite = slv.mkTerm(ITE, x_eq_a, b, a);
+  Term assignment0 = slv.mkTerm(EQUAL, new_x, ite);
+
+  // Assert the encoding of code (0)
+  cout << "Asserting " << assignment0 << " to CVC4 " << endl;
+  slv.assertFormula(assignment0);
+  cout << "Pushing a new context." << endl;
+  slv.push();
+
+  // Encoding code (1)
+  // new_x_ = a xor b xor x
+  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;
+  slv.assertFormula(assignment1);
+  Term new_x_eq_new_x_ = slv.mkTerm(EQUAL, new_x, new_x_);
+
+  cout << " Check validity assuming: " << new_x_eq_new_x_ << endl;
+  cout << " Expect valid. " << endl;
+  cout << " CVC4: " << slv.checkValidAssuming(new_x_eq_new_x_) << endl;
+  cout << " Popping context. " << endl;
+  slv.pop();
+
+  // Encoding code (2)
+  // new_x_ = a + b - x
+  Term a_plus_b = slv.mkTerm(BITVECTOR_PLUS, a, b);
+  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;
+  slv.assertFormula(assignment2);
+
+  cout << " Check validity assuming: " << new_x_eq_new_x_ << endl;
+  cout << " Expect valid. " << endl;
+  cout << " CVC4: " << slv.checkValidAssuming(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 Validity Assuming: " << v << endl;
+  cout << " Expect invalid. " << endl;
+  cout << " CVC4: " << slv.checkValidAssuming(v) << endl;
+
+  // Assert that a is odd 
+  OpTerm extract_op = slv.mkOpTerm(BITVECTOR_EXTRACT_OP, 0, 0);
+  Term  lsb_of_a = slv.mkTerm(extract_op, a);
+  cout << "Sort of " << lsb_of_a << " is " << lsb_of_a.getSort() << endl;
+  Term a_odd = slv.mkTerm(EQUAL, lsb_of_a, slv.mkBitVector(1u, 1u));
+  cout << "Assert " << a_odd << endl;
+  cout << "Check satisfiability." << endl;
+  slv.assertFormula(a_odd);
+  cout << " Expect sat. " << endl;
+  cout << " CVC4: " << slv.checkSat() << endl;
+  return 0;
+}
diff --git a/examples/api/bitvectors_and_arrays-new.cpp b/examples/api/bitvectors_and_arrays-new.cpp
new file mode 100644
index 000000000..3d4e6bca0
--- /dev/null
+++ b/examples/api/bitvectors_and_arrays-new.cpp
@@ -0,0 +1,96 @@
+/*********************                                                        */
+/*! \file bitvectors_and_arrays.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Liana Hadarean, Aina Niemetz, Morgan Deters
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2018 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.\endverbatim
+ **
+ ** \brief A simple demonstration of the solving capabilities of the CVC4
+ ** bit-vector and array solvers.
+ **
+ **/
+
+#include <iostream>
+#include <cmath>
+// #include <cvc4/cvc4.h> // use this after CVC4 is properly installed
+#include "api/cvc4cpp.h"
+
+using namespace std;
+using namespace CVC4::api;
+
+int main()
+{
+  Solver slv;
+  slv.setOption("produce-models", "true");      // Produce Models
+  slv.setOption("output-language", "smtlib"); // output-language
+  slv.setLogic("QF_AUFBV");                   // Set the logic
+
+  // Consider the following code (where size is some previously defined constant):
+  //
+  //
+  //   Assert (current_array[0] > 0);
+  //   for (unsigned i = 1; i < k; ++i) {
+  //     current_array[i] = 2 * current_array[i - 1];
+  //     Assert (current_array[i-1] < current_array[i]);
+  //     }
+  //
+  // We want to check whether the assertion in the body of the for loop holds
+  // throughout the loop.
+
+  // Setting up the problem parameters
+  unsigned k = 4;                // number of unrollings (should be a power of 2)
+  unsigned index_size = log2(k); // size of the index
+
+
+  // Sorts
+  Sort elementSort = slv.mkBitVectorSort(32);
+  Sort indexSort = slv.mkBitVectorSort(index_size);
+  Sort arraySort = slv.mkArraySort(indexSort, elementSort);
+
+  // Variables
+  Term current_array = slv.mkVar("current_array", arraySort);
+
+  // Making a bit-vector constant
+  Term zero = slv.mkBitVector(index_size, 0u);
+
+  // Asserting that current_array[0] > 0
+  Term current_array0 = slv.mkTerm(SELECT, current_array, zero);
+  Term current_array0_gt_0 = slv.mkTerm(
+      BITVECTOR_SGT, current_array0, slv.mkBitVector(32, 0u));
+  slv.assertFormula(current_array0_gt_0);
+
+  // Building the assertions in the loop unrolling
+  Term index = slv.mkBitVector(index_size, 0u);
+  Term old_current = slv.mkTerm(SELECT, current_array, index);
+  Term two = slv.mkBitVector(32, 2u);
+
+  std::vector<Term> assertions;
+  for (unsigned i = 1; i < k; ++i) {
+    index = slv.mkBitVector(index_size, i);
+    Term new_current = slv.mkTerm(BITVECTOR_MULT, two, old_current);
+    // current[i] = 2 * current[i-1]
+    current_array = slv.mkTerm(STORE, current_array, index, new_current);
+    // current[i-1] < current [i]
+    Term current_slt_new_current = slv.mkTerm(BITVECTOR_SLT, old_current, new_current);
+    assertions.push_back(current_slt_new_current);
+
+    old_current = slv.mkTerm(SELECT, current_array, index);
+  }
+
+  Term query = slv.mkTerm(NOT, slv.mkTerm(AND, assertions));
+
+  cout << "Asserting " << query << " to CVC4 " << endl;
+  slv.assertFormula(query);
+  cout << "Expect sat. " << endl;
+  cout << "CVC4: " << slv.checkSatAssuming(slv.mkTrue()) << endl;
+
+  // Getting the model
+  cout << "The satisfying model is: " << endl;
+  cout << "  current_array = " << slv.getValue(current_array) << endl;
+  cout << "  current_array[0] = " << slv.getValue(current_array0) << endl;
+  return 0;
+}
diff --git a/examples/api/combination-new.cpp b/examples/api/combination-new.cpp
new file mode 100644
index 000000000..2956d76e6
--- /dev/null
+++ b/examples/api/combination-new.cpp
@@ -0,0 +1,139 @@
+/*********************                                                        */
+/*! \file combination.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Aina Niemetz, Tim King
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2018 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.\endverbatim
+ **
+ ** \brief A simple demonstration of the capabilities of CVC4
+ **
+ ** 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 <iostream>
+
+//#include <cvc4/cvc4.h> // use this after CVC4 is properly installed
+#include "api/cvc4cpp.h"
+
+using namespace std;
+using namespace CVC4::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", "cvc4"); // Set the output-language to CVC's
+  slv.setOption("default-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.mkVar("x", u);
+  Term y = slv.mkVar("y", u);
+
+  // Functions
+  Term f = slv.mkVar("f", uToInt);
+  Term p = slv.mkVar("p", intPred);
+
+  // 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 valid. " << endl
+       << "CVC4: " << slv.checkValidAssuming(slv.mkTerm(DISTINCT, x, y))
+       << "." << endl << endl;
+
+  cout << "Call checkSat to show that the assertions are satisfiable. "
+       << endl
+       << "CVC4: "
+       << 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 << endl << "Alternatively, print the model." << endl << endl;
+
+  slv.printModel(cout);
+
+  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;
+}
diff --git a/examples/api/datatypes-new.cpp b/examples/api/datatypes-new.cpp
new file mode 100644
index 000000000..9ec679f8e
--- /dev/null
+++ b/examples/api/datatypes-new.cpp
@@ -0,0 +1,165 @@
+/*********************                                                        */
+/*! \file datatypes.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Aina Niemetz, Morgan Deters, Tim King
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2018 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.\endverbatim
+ **
+ ** \brief An example of using inductive datatypes in CVC4
+ **
+ ** An example of using inductive datatypes in CVC4.
+ **/
+
+#include <iostream>
+//#include <cvc4/cvc4.h> // To follow the wiki
+
+#include "api/cvc4cpp.h"
+using namespace CVC4::api;
+
+int main()
+{
+  Solver slv;
+  // This example builds a simple "cons list" of integers, with
+  // two constructors, "cons" and "nil."
+
+  // Building a datatype consists of two steps.
+  // First, the datatype is specified.
+  // Second, it is "resolved" to an actual sort, at which point function
+  // symbols are assigned to its constructors, selectors, and testers.
+
+  DatatypeDecl consListSpec("list"); // give the datatype a name
+  DatatypeConstructorDecl cons("cons");
+  DatatypeSelectorDecl head("head", slv.getIntegerSort());
+  DatatypeSelectorDecl tail("tail", DatatypeDeclSelfSort());
+  cons.addSelector(head);
+  cons.addSelector(tail);
+  consListSpec.addConstructor(cons);
+  DatatypeConstructorDecl nil("nil");
+  consListSpec.addConstructor(nil);
+
+  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.
+  // 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.
+
+  Sort consListSort = slv.mkDatatypeSort(consListSpec);
+
+  // Now our old "consListSpec" is useless--the relevant information
+  // has been copied out, so we can throw that spec away.  We can get
+  // the complete spec for the datatype from the DatatypeSort, and
+  // this Datatype object has constructor symbols (and others) filled in.
+
+  Datatype consList = consListSort.getDatatype();
+
+  // t = cons 0 nil
+  //
+  // Here, consList["cons"] gives you the DatatypeConstructor.  To get
+  // the constructor symbol for application, use .getConstructor("cons"),
+  // which is equivalent to consList["cons"].getConstructor().  Note that
+  // "nil" is a constructor too, so it needs to be applied with
+  // APPLY_CONSTRUCTOR, even though it has no arguments.
+  Term t = slv.mkTerm(
+      APPLY_CONSTRUCTOR,
+      consList.getConstructorTerm("cons"),
+      slv.mkInteger(0),
+      slv.mkTerm(APPLY_CONSTRUCTOR, consList.getConstructorTerm("nil")));
+
+  std::cout << "t is " << t << std::endl
+            << "sort of cons is "
+            << consList.getConstructorTerm("cons").getSort() << std::endl
+            << "sort of nil is " << consList.getConstructorTerm("nil").getSort()
+            << std::endl;
+
+  // t2 = head(cons 0 nil), and of course this can be evaluated
+  //
+  // Here we first get the DatatypeConstructor for cons (with
+  // consList["cons"]) in order to get the "head" selector symbol
+  // to apply.
+  Term t2 =
+      slv.mkTerm(APPLY_SELECTOR, consList["cons"].getSelectorTerm("head"), t);
+
+  std::cout << "t2 is " << t2 << std::endl
+            << "simplify(t2) is " << slv.simplify(t2)
+            << std::endl << std::endl;
+
+  // You can also iterate over a Datatype to get all its constructors,
+  // and over a DatatypeConstructor to get all its "args" (selectors)
+  for (Datatype::const_iterator i = consList.begin();
+       i != consList.end();
+       ++i)
+  {
+    std::cout << "ctor: " << *i << std::endl;
+    for (DatatypeConstructor::const_iterator j = (*i).begin();
+         j != (*i).end();
+         ++j)
+    {
+      std::cout << " + arg: " << *j << std::endl;
+    }
+  }
+  std::cout << std::endl;
+
+  // Alternatively, you can use for each loops.
+  for (const auto& c : consList)
+  {
+    std::cout << "ctor: " << c << std::endl;
+    for (const auto& s : c)
+    {
+      std::cout << " + arg: " << s << std::endl;
+    }
+  }
+  std::cout << std::endl;
+
+  // You can also define parameterized datatypes.
+  // This example builds a simple parameterized list of sort T, with one
+  // constructor "cons".
+  Sort sort = slv.mkParamSort("T");
+  DatatypeDecl paramConsListSpec("paramlist", sort); // give the datatype a name
+  DatatypeConstructorDecl paramCons("cons");
+  DatatypeSelectorDecl paramHead("head", sort);
+  DatatypeSelectorDecl paramTail("tail", DatatypeDeclSelfSort());
+  paramCons.addSelector(paramHead);
+  paramCons.addSelector(paramTail);
+  paramConsListSpec.addConstructor(paramCons);
+
+  Sort paramConsListSort = slv.mkDatatypeSort(paramConsListSpec);
+  Sort paramConsIntListSort =
+      paramConsListSort.instantiate(std::vector<Sort>{slv.getIntegerSort()});
+
+  Datatype paramConsList = paramConsListSort.getDatatype();
+
+  std::cout << "parameterized datatype sort is " << std::endl;
+  for (const DatatypeConstructor& ctor : paramConsList)
+  {
+    std::cout << "ctor: " << ctor << std::endl;
+    for (const DatatypeSelector& stor : ctor)
+    {
+      std::cout << " + arg: " << stor << std::endl;
+    }
+  }
+
+  Term a = slv.declareFun("a", paramConsIntListSort);
+  std::cout << "term " << a << " is of sort " << a.getSort() << std::endl;
+
+  Term head_a = slv.mkTerm(
+      APPLY_SELECTOR, paramConsList["cons"].getSelectorTerm("head"), a);
+  std::cout << "head_a is " << head_a << " of sort " << head_a.getSort() 
+            << std::endl
+            << "sort of cons is "
+            << paramConsList.getConstructorTerm("cons").getSort() << std::endl
+            << std::endl;
+  Term assertion = slv.mkTerm(GT, head_a, slv.mkInteger(50));
+  std::cout << "Assert " << assertion << std::endl;
+  slv.assertFormula(assertion);
+  std::cout << "Expect sat." << std::endl;
+  std::cout << "CVC4: " << slv.checkSat() << std::endl;
+
+  return 0;
+}
diff --git a/examples/api/extract-new.cpp b/examples/api/extract-new.cpp
new file mode 100644
index 000000000..8d31c1b12
--- /dev/null
+++ b/examples/api/extract-new.cpp
@@ -0,0 +1,56 @@
+/*********************                                                        */
+/*! \file extract.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Clark Barrett, Aina Niemetz
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2018 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.\endverbatim
+ **
+ ** \brief A simple demonstration of the solving capabilities of the CVC4
+ ** bit-vector solver.
+ **
+ **/
+
+#include <iostream>
+
+//#include <cvc4/cvc4.h> // use this after CVC4 is properly installed
+#include "api/cvc4cpp.h"
+
+using namespace std;
+using namespace CVC4::api;
+
+int main()
+{
+  Solver slv;
+  slv.setLogic("QF_BV"); // Set the logic
+
+  Sort bitvector32 = slv.mkBitVectorSort(32);
+
+  Term x = slv.mkVar("a", bitvector32);
+
+  OpTerm ext_31_1 = slv.mkOpTerm(BITVECTOR_EXTRACT_OP, 31, 1);
+  Term x_31_1 = slv.mkTerm(ext_31_1, x);
+
+  OpTerm ext_30_0 = slv.mkOpTerm(BITVECTOR_EXTRACT_OP, 30, 0);
+  Term x_30_0 = slv.mkTerm(ext_30_0, x);
+
+  OpTerm ext_31_31 = slv.mkOpTerm(BITVECTOR_EXTRACT_OP, 31, 31);
+  Term x_31_31 = slv.mkTerm(ext_31_31, x);
+
+  OpTerm ext_0_0 = slv.mkOpTerm(BITVECTOR_EXTRACT_OP, 0, 0);
+  Term x_0_0 = slv.mkTerm(ext_0_0, x);
+
+  Term eq = slv.mkTerm(EQUAL, x_31_1, x_30_0);
+  cout << " Asserting: " << eq << endl;
+  slv.assertFormula(eq);
+
+  Term eq2 = slv.mkTerm(EQUAL, x_31_31, x_0_0);
+  cout << " Check validity assuming: " << eq2 << endl;
+  cout << " Expect valid. " << endl;
+  cout << " CVC4: " << slv.checkValidAssuming(eq2) << endl;
+
+  return 0;
+}
diff --git a/examples/api/helloworld-new.cpp b/examples/api/helloworld-new.cpp
new file mode 100644
index 000000000..7957741e5
--- /dev/null
+++ b/examples/api/helloworld-new.cpp
@@ -0,0 +1,30 @@
+/*********************                                                        */
+/*! \file helloworld.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Aina Niemetz, Tim King, Kshitij Bansal
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2018 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.\endverbatim
+ **
+ ** \brief A very simple CVC4 example
+ **
+ ** A very simple CVC4 tutorial example.
+ **/
+
+#include <iostream>
+
+#include "api/cvc4cpp.h"
+
+using namespace CVC4::api;
+
+int main()
+{
+  Solver slv;
+  Term helloworld = slv.mkVar("Hello World!", slv.getBooleanSort());
+  std::cout << helloworld << " is " << slv.checkValidAssuming(helloworld)
+            << std::endl;
+  return 0;
+}
diff --git a/examples/api/linear_arith-new.cpp b/examples/api/linear_arith-new.cpp
new file mode 100644
index 000000000..ef8faade9
--- /dev/null
+++ b/examples/api/linear_arith-new.cpp
@@ -0,0 +1,85 @@
+/*********************                                                        */
+/*! \file linear_arith.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Tim King, Aina Niemetz
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2018 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.\endverbatim
+ **
+ ** \brief A simple demonstration of the linear arithmetic capabilities of CVC4
+ **
+ ** A simple demonstration of the linear arithmetic solving capabilities and
+ ** the push pop of CVC4. This also gives an example option.
+ **/
+
+#include <iostream>
+
+//#include <cvc4/cvc4.h> // use this after CVC4 is properly installed
+#include "api/cvc4cpp.h"
+
+using namespace std;
+using namespace CVC4::api;
+
+int main()
+{
+  Solver slv;
+  slv.setLogic("QF_LIRA"); // Set the logic
+
+  // Prove that if given x (Integer) and y (Real) then
+  // the maximum value of y - x is 2/3
+
+  // Sorts
+  Sort real = slv.getRealSort();
+  Sort integer = slv.getIntegerSort();
+
+  // Variables
+  Term x = slv.mkVar("x", integer);
+  Term y = slv.mkVar("y", real);
+
+  // Constants
+  Term three = slv.mkInteger(3);
+  Term neg2 = slv.mkInteger(-2);
+  Term two_thirds = slv.mkReal(2, 3);
+
+  // Terms
+  Term three_y = slv.mkTerm(MULT, three, y);
+  Term diff = slv.mkTerm(MINUS, y, x);
+
+  // Formulas
+  Term x_geq_3y = slv.mkTerm(GEQ, x, three_y);
+  Term x_leq_y = slv.mkTerm(LEQ, x, y);
+  Term neg2_lt_x = slv.mkTerm(LT, neg2, x);
+
+  Term assertions =
+    slv.mkTerm(AND, x_geq_3y, x_leq_y, neg2_lt_x);
+
+  cout << "Given the assertions " << assertions << endl;
+  slv.assertFormula(assertions);
+
+
+  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 VALID." << endl;
+  cout << "Result from CVC4 is: "
+       << slv.checkValidAssuming(diff_leq_two_thirds) << endl;
+  slv.pop();
+
+  cout << endl;
+
+  slv.push();
+  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;
+  slv.pop();
+
+  cout << "Thus the maximum value of (y - x) is 2/3."<< endl;
+
+  return 0;
+}
diff --git a/examples/api/sets-new.cpp b/examples/api/sets-new.cpp
new file mode 100644
index 000000000..be35bcc21
--- /dev/null
+++ b/examples/api/sets-new.cpp
@@ -0,0 +1,96 @@
+/*********************                                                        */
+/*! \file sets.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Aina Niemetz, Kshitij Bansal
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2018 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.\endverbatim
+ **
+ ** \brief Reasoning about sets with CVC4.
+ **
+ ** A simple demonstration of reasoning about sets with CVC4.
+ **/
+
+#include <iostream>
+
+//#include <cvc4/cvc4.h> // use this after CVC4 is properly installed
+#include "api/cvc4cpp.h"
+
+using namespace std;
+using namespace CVC4::api;
+
+int main()
+{
+  Solver slv;
+
+  // Optionally, set the logic. We need at least UF for equality predicate,
+  // integers (LIA) and sets (FS).
+  slv.setLogic("QF_UFLIAFS");
+
+  // Produce models
+  slv.setOption("produce-models", "true");
+  slv.setOption("output-language", "smt2");
+
+  Sort integer = slv.getIntegerSort();
+  Sort set = slv.mkSetSort(integer);
+
+  // Verify union distributions over intersection
+  // (A union B) intersection C = (A intersection C) union (B intersection C)
+  {
+    Term A = slv.mkVar("A", set);
+    Term B = slv.mkVar("B", set);
+    Term C = slv.mkVar("C", set);
+
+    Term unionAB = slv.mkTerm(UNION, A, B);
+    Term lhs = slv.mkTerm(INTERSECTION, unionAB, C);
+
+    Term intersectionAC = slv.mkTerm(INTERSECTION, A, C);
+    Term intersectionBC = slv.mkTerm(INTERSECTION, B, C);
+    Term rhs = slv.mkTerm(UNION, intersectionAC, intersectionBC);
+
+    Term theorem = slv.mkTerm(EQUAL, lhs, rhs);
+
+    cout << "CVC4 reports: " << theorem << " is "
+         << slv.checkValidAssuming(theorem) << "." << endl;
+  }
+
+  // Verify emptset is a subset of any set
+  {
+    Term A = slv.mkVar("A", set);
+    Term emptyset = slv.mkEmptySet(set);
+
+    Term theorem = slv.mkTerm(SUBSET, emptyset, A);
+
+    cout << "CVC4 reports: " << theorem << " is "
+         << slv.checkValidAssuming(theorem) << "." << endl;
+  }
+
+  // Find me an element in {1, 2} intersection {2, 3}, if there is one.
+  {
+    Term one = slv.mkInteger(1);
+    Term two = slv.mkInteger(2);
+    Term three = slv.mkInteger(3);
+
+    Term singleton_one = slv.mkTerm(SINGLETON, one);
+    Term singleton_two = slv.mkTerm(SINGLETON, two);
+    Term singleton_three = slv.mkTerm(SINGLETON, three);
+    Term one_two = slv.mkTerm(UNION, singleton_one, singleton_two);
+    Term two_three = slv.mkTerm(UNION, singleton_two, singleton_three);
+    Term intersection = slv.mkTerm(INTERSECTION, one_two, two_three);
+
+    Term x = slv.mkVar("x", integer);
+
+    Term e = slv.mkTerm(MEMBER, x, intersection);
+
+    Result result = slv.checkSatAssuming(e);
+    cout << "CVC4 reports: " << e << " is " << result << "." << endl;
+
+    if (result.isSat())
+    {
+      cout << "For instance, " << slv.getValue(x) << " is a member." << endl;
+    }
+  }
+}
diff --git a/examples/api/strings-new.cpp b/examples/api/strings-new.cpp
new file mode 100644
index 000000000..2010c6909
--- /dev/null
+++ b/examples/api/strings-new.cpp
@@ -0,0 +1,96 @@
+/*********************                                                        */
+/*! \file strings.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Clark Barrett, Paul Meng, Tim King
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2017 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.\endverbatim
+ **
+ ** \brief Reasoning about strings with CVC4 via C++ API.
+ **
+ ** A simple demonstration of reasoning about strings with CVC4 via C++ API.
+ **/
+
+#include <iostream>
+
+//#include <cvc4/cvc4.h> // use this after CVC4 is properly installed
+#include "api/cvc4cpp.h"
+
+using namespace CVC4::api;
+
+int main()
+{
+  Solver slv;
+
+  // Set the logic
+  slv.setLogic("S");
+  // Produce models
+  slv.setOption("produce-models", "true");
+  // The option strings-exp is needed
+  slv.setOption("strings-exp", "true");
+  // Set output language to SMTLIB2
+  slv.setOption("output-language", "smt2");
+
+  // String type
+  Sort string = slv.getStringSort();
+
+  // std::string
+  std::string str_ab("ab");
+  // String constants
+  Term ab  = slv.mkString(str_ab);
+  Term abc = slv.mkString("abc");
+  // String variables
+  Term x = slv.mkVar("x", string);
+  Term y = slv.mkVar("y", string);
+  Term z = slv.mkVar("z", string);
+
+  // String concatenation: x.ab.y
+  Term lhs = slv.mkTerm(STRING_CONCAT, x, ab, y);
+  // String concatenation: abc.z
+  Term rhs = slv.mkTerm(STRING_CONCAT, abc, z);
+  // x.ab.y = abc.z
+  Term formula1 = slv.mkTerm(EQUAL, lhs, rhs);
+
+  // Length of y: |y|
+  Term leny = slv.mkTerm(STRING_LENGTH, y);
+  // |y| >= 0
+  Term formula2 = slv.mkTerm(GEQ, leny, slv.mkInteger(0));
+
+  // Regular expression: (ab[c-e]*f)|g|h
+  Term r = slv.mkTerm(REGEXP_UNION,
+    slv.mkTerm(REGEXP_CONCAT,
+      slv.mkTerm(STRING_TO_REGEXP, slv.mkString("ab")),
+      slv.mkTerm(REGEXP_STAR,
+        slv.mkTerm(REGEXP_RANGE, slv.mkString("c"), slv.mkString("e"))),
+      slv.mkTerm(STRING_TO_REGEXP, slv.mkString("f"))),
+    slv.mkTerm(STRING_TO_REGEXP, slv.mkString("g")),
+    slv.mkTerm(STRING_TO_REGEXP, slv.mkString("h")));
+
+  // String variables
+  Term s1 = slv.mkVar("s1", string);
+  Term s2 = slv.mkVar("s2", string);
+  // String concatenation: s1.s2
+  Term s = slv.mkTerm(STRING_CONCAT, s1, s2);
+
+  // s1.s2 in (ab[c-e]*f)|g|h
+  Term formula3 = slv.mkTerm(STRING_IN_REGEXP, s, r);
+
+  // Make a query
+  Term q = slv.mkTerm(AND,
+    formula1,
+    formula2,
+    formula3);
+
+  // check sat
+  Result result = slv.checkSatAssuming(q);
+  std::cout << "CVC4 reports: " << q << " is " << result << "." << std::endl;
+
+  if(result.isSat())
+  {
+    std::cout << "  x  = " << slv.getValue(x) << std::endl;
+    std::cout << "  s1.s2 = " << slv.getValue(s) << std::endl;
+  }
+}