From 35c39b2cdc3905af8ad4739c20971d8b35889582 Mon Sep 17 00:00:00 2001
From: Aina Niemetz <aina.niemetz@gmail.com>
Date: Mon, 23 Jul 2018 12:29:03 -0700
Subject: [PATCH] New C++ API: declare-datatype. (#2166)

---
 examples/api/datatypes-new.cpp | 75 ++++++++++++++++++++--------------
 src/api/cvc4cpp.cpp            | 15 +++++++
 src/api/cvc4cpp.h              | 11 +++++
 3 files changed, 70 insertions(+), 31 deletions(-)

diff --git a/examples/api/datatypes-new.cpp b/examples/api/datatypes-new.cpp
index 9ec679f8e..0989d3c48 100644
--- a/examples/api/datatypes-new.cpp
+++ b/examples/api/datatypes-new.cpp
@@ -20,38 +20,8 @@
 #include "api/cvc4cpp.h"
 using namespace CVC4::api;
 
-int main()
+void test(Solver& slv, Sort& consListSort)
 {
-  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
@@ -160,6 +130,49 @@ int main()
   slv.assertFormula(assertion);
   std::cout << "Expect sat." << std::endl;
   std::cout << "CVC4: " << slv.checkSat() << std::endl;
+}
+
+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);
+
+  test(slv, consListSort);
+
+  std::cout << std::endl << ">>> Alternatively, use declareDatatype" << std::endl;
+  std::cout << std::endl;
+
+  std::vector<DatatypeConstructorDecl> ctors = { cons, nil };
+  Sort consListSort2 = slv.declareDatatype("list2", ctors);
+  test(slv, consListSort2);
+
 
   return 0;
 }
diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp
index 488590deb..938dc127d 100644
--- a/src/api/cvc4cpp.cpp
+++ b/src/api/cvc4cpp.cpp
@@ -2213,5 +2213,20 @@ std::vector<Expr> Solver::termVectorToExprs(
   return res;
 }
 
+/**
+ *  ( declare-datatype <symbol> <datatype_decl> )
+ */
+Sort Solver::declareDatatype(
+    const std::string& symbol,
+    const std::vector<DatatypeConstructorDecl>& ctors) const
+{
+  DatatypeDecl dtdecl(symbol);
+  for (const DatatypeConstructorDecl& ctor : ctors)
+  {
+    dtdecl.addConstructor(ctor);
+  }
+  return mkDatatypeSort(dtdecl);
+}
+
 }  // namespace api
 }  // namespace CVC4
diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h
index 6007aadcc..b76fbb08f 100644
--- a/src/api/cvc4cpp.h
+++ b/src/api/cvc4cpp.h
@@ -2117,6 +2117,17 @@ class CVC4_PUBLIC Solver
    */
   Term declareConst(const std::string& symbol, Sort sort) const;
 
+  /**
+   * Create datatype sort.
+   * SMT-LIB: ( declare-datatype <symbol> <datatype_decl> )
+   * @param symbol the name of the datatype sort
+   * @param ctors the constructor declarations of the datatype sort
+   * @return the datatype sort
+   */
+  Sort declareDatatype(
+      const std::string& symbol,
+      const std::vector<DatatypeConstructorDecl>& ctors) const;
+
   /**
    * Declare 0-arity function symbol.
    * SMT-LIB: ( declare-fun <symbol> ( ) <sort> )
-- 
2.30.2