New C++ Api: First batch of API guards. (#4557)

This is the first batch of API guards, mainly extending existing guards
in the Solver object with checks that Ops, Terms, Sorts, and datatype objects
are associated to this solver object.

This further changes how DatatypeConstructorDecl objects are created. Previously,
they were not created via the Solver object (while DatatypeDecl was). Now, they are
created via Solver::mkDatatypeConstructorDecl, consistent with how DatatypeDecl
objects are created.

2 files changed, 12 insertions, 12 deletions

diff --git a/examples/api/datatypes-new.cpp b/examples/api/datatypes-new.cpp
index 9cfc7992c..500cb0710 100644
--- a/examples/api/datatypes-new.cpp
+++ b/examples/api/datatypes-new.cpp
@@ -91,8 +91,8 @@ void test(Solver& slv, Sort& consListSort)
   DatatypeDecl paramConsListSpec =
       slv.mkDatatypeDecl("paramlist",
                          sort);  // give the datatype a name
-  DatatypeConstructorDecl paramCons("cons");
-  DatatypeConstructorDecl paramNil("nil");
+  DatatypeConstructorDecl paramCons = slv.mkDatatypeConstructorDecl("cons");
+  DatatypeConstructorDecl paramNil = slv.mkDatatypeConstructorDecl("nil");
   paramCons.addSelector("head", sort);
   paramCons.addSelectorSelf("tail");
   paramConsListSpec.addConstructor(paramCons);
@@ -144,11 +144,11 @@ int main()
 
   DatatypeDecl consListSpec =
       slv.mkDatatypeDecl("list");  // give the datatype a name
-  DatatypeConstructorDecl cons("cons");
+  DatatypeConstructorDecl cons = slv.mkDatatypeConstructorDecl("cons");
   cons.addSelector("head", slv.getIntegerSort());
   cons.addSelectorSelf("tail");
   consListSpec.addConstructor(cons);
-  DatatypeConstructorDecl nil("nil");
+  DatatypeConstructorDecl nil = slv.mkDatatypeConstructorDecl("nil");
   consListSpec.addConstructor(nil);
 
   std::cout << "spec is:" << std::endl << consListSpec << std::endl;
@@ -167,10 +167,10 @@ int main()
             << ">>> Alternatively, use declareDatatype" << std::endl;
   std::cout << std::endl;
 
-  DatatypeConstructorDecl cons2("cons");
+  DatatypeConstructorDecl cons2 = slv.mkDatatypeConstructorDecl("cons");
   cons2.addSelector("head", slv.getIntegerSort());
   cons2.addSelectorSelf("tail");
-  DatatypeConstructorDecl nil2("nil");
+  DatatypeConstructorDecl nil2 = slv.mkDatatypeConstructorDecl("nil");
   std::vector<DatatypeConstructorDecl> ctors = {cons2, nil2};
   Sort consListSort2 = slv.declareDatatype("list2", ctors);
   test(slv, consListSort2);
diff --git a/examples/api/python/datatypes.py b/examples/api/python/datatypes.py
index ded268d69..1a67f5661 100755
--- a/examples/api/python/datatypes.py
+++ b/examples/api/python/datatypes.py
@@ -65,8 +65,8 @@ def test(slv, consListSort):
     # constructor "cons".
     sort = slv.mkParamSort("T")
     paramConsListSpec = slv.mkDatatypeDecl("paramlist", sort)
-    paramCons = pycvc4.DatatypeConstructorDecl("cons")
-    paramNil = pycvc4.DatatypeConstructorDecl("nil")
+    paramCons = slv.mkDatatypeConstructorDecl("cons")
+    paramNil = slv.mkDatatypeConstructorDecl("nil")
     paramCons.addSelector("head", sort)
     paramCons.addSelectorSelf("tail")
     paramConsListSpec.addConstructor(paramCons)
@@ -102,11 +102,11 @@ if __name__ == "__main__":
     # symbols are assigned to its constructors, selectors, and testers.
 
     consListSpec = slv.mkDatatypeDecl("list") # give the datatype a name
-    cons = pycvc4.DatatypeConstructorDecl("cons")
+    cons = slv.mkDatatypeConstructorDecl("cons")
     cons.addSelector("head", slv.getIntegerSort())
     cons.addSelectorSelf("tail")
     consListSpec.addConstructor(cons)
-    nil = pycvc4.DatatypeConstructorDecl("nil")
+    nil = slv.mkDatatypeConstructorDecl("nil")
     consListSpec.addConstructor(nil)
 
     print("spec is {}".format(consListSpec))
@@ -122,10 +122,10 @@ if __name__ == "__main__":
 
     print("### Alternatively, use declareDatatype")
 
-    cons2 = pycvc4.DatatypeConstructorDecl("cons")
+    cons2 = slv.mkDatatypeConstructorDecl("cons")
     cons2.addSelector("head", slv.getIntegerSort())
     cons2.addSelectorSelf("tail")
-    nil2 = pycvc4.DatatypeConstructorDecl("nil")
+    nil2 = slv.mkDatatypeConstructorDecl("nil")
     ctors = [cons2, nil2]
     consListSort2 = slv.declareDatatype("list2", ctors)
     test(slv, consListSort2)