1 files changed, 0 insertions, 139 deletions
diff --git a/examples/api/combination-new.cpp b/examples/api/combination-new.cpp
deleted file mode 100644
index ab3d80d10..000000000
--- a/examples/api/combination-new.cpp
+++ /dev/null
@@ -1,139 +0,0 @@
-/*********************                                                        */
-/*! \file combination-new.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Aina Niemetz, Andrew Reynolds
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 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/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("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.mkReal(0);
-  Term one = slv.mkReal(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
-       << "CVC4: " << slv.checkEntailed(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;
-}