New C++ API: Remove examples for old API. (#4650)

This removes obsolete examples for the old API in preparation of making
the old API private. Examples for the new API are renamed from
*-new.cpp to *.cpp.

1 files changed, 40 insertions, 42 deletions

diff --git a/examples/api/sets.cpp b/examples/api/sets.cpp
index 4e4fb4cd4..aa70b4ee4 100644
--- a/examples/api/sets.cpp
+++ b/examples/api/sets.cpp
@@ -2,7 +2,7 @@
 /*! \file sets.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Kshitij Bansal, Aina Niemetz, Tim King
+ **   Aina Niemetz
  ** 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.
@@ -16,82 +16,80 @@
 
 #include <iostream>
 
-#include <cvc4/cvc4.h>
-#include <cvc4/options/set_language.h>
+#include <cvc4/api/cvc4cpp.h>
 
 using namespace std;
-using namespace CVC4;
+using namespace CVC4::api;
 
-int main() {
-  ExprManager em;
-  SmtEngine smt(&em);
+int main()
+{
+  Solver slv;
 
   // Optionally, set the logic. We need at least UF for equality predicate,
   // integers (LIA) and sets (FS).
-  smt.setLogic("QF_UFLIAFS");
+  slv.setLogic("QF_UFLIAFS");
 
   // Produce models
-  smt.setOption("produce-models", true);
+  slv.setOption("produce-models", "true");
+  slv.setOption("output-language", "smt2");
 
-  // Set output language to SMTLIB2
-  cout << language::SetLanguage(language::output::LANG_SMTLIB_V2);
-
-  Type integer = em.integerType();
-  Type set = em.mkSetType(integer);
+  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)
   {
-    Expr A = em.mkVar("A", set);
-    Expr B = em.mkVar("B", set);
-    Expr C = em.mkVar("C", set);
+    Term A = slv.mkConst(set, "A");
+    Term B = slv.mkConst(set, "B");
+    Term C = slv.mkConst(set, "C");
 
-    Expr unionAB = em.mkExpr(kind::UNION, A, B);
-    Expr lhs = em.mkExpr(kind::INTERSECTION, unionAB, C);
+    Term unionAB = slv.mkTerm(UNION, A, B);
+    Term lhs = slv.mkTerm(INTERSECTION, unionAB, C);
 
-    Expr intersectionAC = em.mkExpr(kind::INTERSECTION, A, C);
-    Expr intersectionBC = em.mkExpr(kind::INTERSECTION, B, C);
-    Expr rhs = em.mkExpr(kind::UNION, intersectionAC, intersectionBC);
+    Term intersectionAC = slv.mkTerm(INTERSECTION, A, C);
+    Term intersectionBC = slv.mkTerm(INTERSECTION, B, C);
+    Term rhs = slv.mkTerm(UNION, intersectionAC, intersectionBC);
 
-    Expr theorem = em.mkExpr(kind::EQUAL, lhs, rhs);
+    Term theorem = slv.mkTerm(EQUAL, lhs, rhs);
 
-    cout << "CVC4 reports: " << theorem << " is " << smt.checkEntailed(theorem)
+    cout << "CVC4 reports: " << theorem << " is " << slv.checkEntailed(theorem)
          << "." << endl;
   }
 
   // Verify emptset is a subset of any set
   {
-    Expr A = em.mkVar("A", set);
-    Expr emptyset = em.mkConst(EmptySet(set));
+    Term A = slv.mkConst(set, "A");
+    Term emptyset = slv.mkEmptySet(set);
 
-    Expr theorem = em.mkExpr(kind::SUBSET, emptyset, A);
+    Term theorem = slv.mkTerm(SUBSET, emptyset, A);
 
-    cout << "CVC4 reports: " << theorem << " is " << smt.checkEntailed(theorem)
+    cout << "CVC4 reports: " << theorem << " is " << slv.checkEntailed(theorem)
          << "." << endl;
   }
 
   // Find me an element in {1, 2} intersection {2, 3}, if there is one.
   {
-    Expr one = em.mkConst(Rational(1));
-    Expr two = em.mkConst(Rational(2));
-    Expr three = em.mkConst(Rational(3));
+    Term one = slv.mkReal(1);
+    Term two = slv.mkReal(2);
+    Term three = slv.mkReal(3);
 
-    Expr singleton_one = em.mkExpr(kind::SINGLETON, one);
-    Expr singleton_two = em.mkExpr(kind::SINGLETON, two);
-    Expr singleton_three = em.mkExpr(kind::SINGLETON, three);
-    Expr one_two = em.mkExpr(kind::UNION, singleton_one, singleton_two);
-    Expr two_three = em.mkExpr(kind::UNION, singleton_two, singleton_three);
-    Expr intersection = em.mkExpr(kind::INTERSECTION, one_two, two_three);
+    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);
 
-    Expr x = em.mkVar("x", integer);
+    Term x = slv.mkConst(integer, "x");
 
-    Expr e = em.mkExpr(kind::MEMBER, x, intersection);
+    Term e = slv.mkTerm(MEMBER, x, intersection);
 
-    Result result = smt.checkSat(e);
+    Result result = slv.checkSatAssuming(e);
     cout << "CVC4 reports: " << e << " is " << result << "." << endl;
 
-    if(result == Result::SAT) {
-      cout << "For instance, " << smt.getValue(x) << " is a member." << endl;
+    if (result.isSat())
+    {
+      cout << "For instance, " << slv.getValue(x) << " is a member." << endl;
     }
   }
 }