New C++ API: Fix checks for mkTerm. (#2820)

This required fixing the OpTerm handling for mkTerm functions in the API.

3 files changed, 22 insertions, 25 deletions

diff --git a/examples/api/bitvectors-new.cpp b/examples/api/bitvectors-new.cpp
index cd34a5130..7070f6748 100644
--- a/examples/api/bitvectors-new.cpp
+++ b/examples/api/bitvectors-new.cpp
@@ -24,9 +24,8 @@ using namespace CVC4::api;
 
 int main()
 {
-
   Solver slv;
-  slv.setLogic("QF_BV"); // Set the logic
+  slv.setLogic("QF_BV");  // Set the logic
 
   // The following example has been adapted from the book A Hacker's Delight by
   // Henry S. Warren.
@@ -64,8 +63,9 @@ int main()
   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)
+  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;
@@ -114,9 +114,9 @@ int main()
   cout << " Expect invalid. " << endl;
   cout << " CVC4: " << slv.checkValidAssuming(v) << endl;
 
-  // Assert that a is odd 
+  // Assert that a is odd
   OpTerm extract_op = slv.mkOpTerm(BITVECTOR_EXTRACT_OP, 0, 0);
-  Term  lsb_of_a = slv.mkTerm(extract_op, a);
+  Term lsb_of_a = slv.mkTerm(BITVECTOR_EXTRACT, 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;
diff --git a/examples/api/datatypes-new.cpp b/examples/api/datatypes-new.cpp
index 48560e894..14ddcd383 100644
--- a/examples/api/datatypes-new.cpp
+++ b/examples/api/datatypes-new.cpp
@@ -57,18 +57,15 @@ void test(Solver& slv, Sort& consListSort)
       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;
+            << "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)
+  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();
+    for (DatatypeConstructor::const_iterator j = (*i).begin(); j != (*i).end();
          ++j)
     {
       std::cout << " + arg: " << *j << std::endl;
@@ -91,7 +88,8 @@ void test(Solver& slv, Sort& consListSort)
   // 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
+  DatatypeDecl paramConsListSpec("paramlist",
+                                 sort);  // give the datatype a name
   DatatypeConstructorDecl paramCons("cons");
   DatatypeConstructorDecl paramNil("nil");
   DatatypeSelectorDecl paramHead("head", sort);
@@ -122,7 +120,7 @@ void test(Solver& slv, Sort& consListSort)
 
   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::cout << "head_a is " << head_a << " of sort " << head_a.getSort()
             << std::endl
             << "sort of cons is "
             << paramConsList.getConstructorTerm("cons").getSort() << std::endl
@@ -145,7 +143,7 @@ int main()
   // 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
+  DatatypeDecl consListSpec("list");  // give the datatype a name
   DatatypeConstructorDecl cons("cons");
   DatatypeSelectorDecl head("head", slv.getIntegerSort());
   DatatypeSelectorDecl tail("tail", DatatypeDeclSelfSort());
@@ -155,8 +153,7 @@ int main()
   DatatypeConstructorDecl nil("nil");
   consListSpec.addConstructor(nil);
 
-  std::cout << "spec is:" << std::endl
-            << consListSpec << std::endl;
+  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.
@@ -168,13 +165,13 @@ int main()
 
   test(slv, consListSort);
 
-  std::cout << std::endl << ">>> Alternatively, use declareDatatype" << std::endl;
+  std::cout << std::endl
+            << ">>> Alternatively, use declareDatatype" << std::endl;
   std::cout << std::endl;
 
-  std::vector<DatatypeConstructorDecl> ctors = { cons, nil };
+  std::vector<DatatypeConstructorDecl> ctors = {cons, nil};
   Sort consListSort2 = slv.declareDatatype("list2", ctors);
   test(slv, consListSort2);
 
-
   return 0;
 }
diff --git a/examples/api/extract-new.cpp b/examples/api/extract-new.cpp
index 8d31c1b12..96961458e 100644
--- a/examples/api/extract-new.cpp
+++ b/examples/api/extract-new.cpp
@@ -32,16 +32,16 @@ int main()
   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);
+  Term x_31_1 = slv.mkTerm(BITVECTOR_EXTRACT, 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);
+  Term x_30_0 = slv.mkTerm(BITVECTOR_EXTRACT, 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);
+  Term x_31_31 = slv.mkTerm(BITVECTOR_EXTRACT, 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 x_0_0 = slv.mkTerm(BITVECTOR_EXTRACT, ext_0_0, x);
 
   Term eq = slv.mkTerm(EQUAL, x_31_1, x_30_0);
   cout << " Asserting: " << eq << endl;