Java datatype API fixups, datatype API examples

5 files changed, 228 insertions, 11 deletions

diff --git a/examples/README b/examples/README
index 246388085..d64ed3469 100644
--- a/examples/README
+++ b/examples/README
@@ -10,6 +10,12 @@ world" examples, and do not fully demonstrate the interfaces, but
 function as a starting point to using simple expressions and solving
 functionality through each library.
 
+*** Targetted examples
+
+The "api" directory contains some more specifically-targetted
+examples (for bitvectors, for arithmetic, etc.).  The "api/java"
+directory contains the same examples in Java.
+
 *** Installing example source code
 
 Examples are not automatically installed by "make install".  If you
@@ -21,13 +27,8 @@ in /usr/local/share/doc/cvc4/examples).
 *** Building examples
 
 Examples can be built as a separate step, after building CVC4 from
-source.  After building CVC4, you can run "make examples" (or just
-"make" from *inside* the examples directory).  You'll find the built
-binaries in builds/examples (or just in "examples" if you configured a
-build directory outside of the source tree).
-
-Many of the language bindings examples (python, ocaml, ruby, etc.) do
-not need to be compiled to run.  These are not compiled by
-"make"---see the comments in the files for ideas on how to run them.
+source.  After building CVC4, you can run "make examples".  You'll
+find the built binaries in builds/examples (or just in "examples" if
+you configured a build directory outside of the source tree).
 
--- Morgan Deters <mdeters@cs.nyu.edu>  Wed, 03 Oct 2012 15:47:33 -0400
+-- Morgan Deters <mdeters@cs.nyu.edu>  Tue, 24 Dec 2013 09:12:59 -0500
diff --git a/examples/api/Makefile.am b/examples/api/Makefile.am
index 6dba17b05..0d0236376 100644
--- a/examples/api/Makefile.am
+++ b/examples/api/Makefile.am
@@ -10,8 +10,8 @@ noinst_PROGRAMS = \
 	helloworld \
 	combination \
 	bitvectors \
-	bitvectors_and_arrays
-
+	bitvectors_and_arrays \
+	datatypes
 
 noinst_DATA =
 
@@ -40,6 +40,11 @@ bitvectors_SOURCES = \
 bitvectors_LDADD = \
 	@builddir@/../../src/libcvc4.la
 
+datatypes_SOURCES = \
+	datatypes.cpp
+datatypes_LDADD = \
+	@builddir@/../../src/libcvc4.la
+
 # for installation
 examplesdir = $(docdir)/$(subdir)
 examples_DATA = $(DIST_SOURCES) $(EXTRA_DIST)
diff --git a/examples/api/datatypes.cpp b/examples/api/datatypes.cpp
new file mode 100644
index 000000000..6492ad465
--- /dev/null
+++ b/examples/api/datatypes.cpp
@@ -0,0 +1,105 @@
+/*********************                                                        */
+/*! \file datatypes.cpp
+ ** \verbatim
+ ** Original author: Morgan Deters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2013  New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief An example of using inductive datatypes in CVC4
+ **
+ ** An example of using inductive datatypes in CVC4.
+ **/
+
+#include <iostream>
+#include "smt/smt_engine.h" // for use with make examples
+#include "util/language.h" // for use with make examples
+//#include <cvc4/cvc4.h> // To follow the wiki
+
+using namespace CVC4;
+
+int main() {
+  ExprManager em;
+  SmtEngine smt(&em);
+
+  std::cout << Expr::setlanguage(language::output::LANG_CVC4);
+
+  // 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"---at which point function
+  // symbols are assigned to its constructors, selectors, and testers.
+
+  Datatype consListSpec("list"); // give the datatype a name
+  DatatypeConstructor cons("cons");
+  cons.addArg("head", em.integerType());
+  cons.addArg("tail", DatatypeSelfType()); // a list
+  consListSpec.addConstructor(cons);
+  DatatypeConstructor nil("nil");
+  consListSpec.addConstructor(nil);
+
+  std::cout << "spec is:" << std::endl
+            << consListSpec << std::endl;
+
+  // Keep in mind that "Datatype" is the specification class for
+  // datatypes---"Datatype" is not itself a CVC4 Type.  Now that
+  // our Datatype is fully specified, we can get a Type for it.
+  // This step resolves the "SelfType" reference and creates
+  // symbols for all the constructors, etc.
+
+  DatatypeType consListType = em.mkDatatypeType(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 DatatypeType, and
+  // this Datatype object has constructor symbols (and others) filled in.
+
+  const Datatype& consList = consListType.getDatatype();
+
+  // e = cons 0 nil
+  //
+  // Here, consList["cons"] gives you the DatatypeConstructor.  To get
+  // the constructor symbol for application, use .getConstructor("cons"),
+  // which is equivalent to consList["cons"].getConstructor().  Note that
+  // "nil" is a constructor too, so it needs to be applied with
+  // APPLY_CONSTRUCTOR, even though it has no arguments.
+  Expr e = em.mkExpr(kind::APPLY_CONSTRUCTOR,
+                     consList.getConstructor("cons"),
+                     em.mkConst(Rational(0)),
+                     em.mkExpr(kind::APPLY_CONSTRUCTOR,
+                               consList.getConstructor("nil")));
+
+  std::cout << "e is " << e << std::endl
+            << "type of cons is " << consList.getConstructor("cons").getType()
+            << std::endl
+            << "type of nil is " << consList.getConstructor("nil").getType()
+            << std::endl;
+
+  // e2 = head(cons 0 nil), and of course this can be evaluated
+  //
+  // Here we first get the DatatypeConstructor for cons (with
+  // consList["cons"]) in order to get the "head" selector symbol
+  // to apply.
+  Expr e2 = em.mkExpr(kind::APPLY_SELECTOR,
+                      consList["cons"].getSelector("head"),
+                      e);
+
+  std::cout << "e2 is " << e2 << std::endl
+            << "simplify(e2) is " << smt.simplify(e2)
+            << 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::iterator i = consList.begin(); i != consList.end(); ++i) {
+    std::cout << "ctor: " << *i << std::endl;
+    for(DatatypeConstructor::iterator j = (*i).begin(); j != (*i).end(); ++j) {
+      std::cout << " + arg: " << *j << std::endl;
+    }
+  }
+
+  return 0;
+}
diff --git a/examples/api/java/Datatypes.java b/examples/api/java/Datatypes.java
new file mode 100644
index 000000000..d5d4af897
--- /dev/null
+++ b/examples/api/java/Datatypes.java
@@ -0,0 +1,104 @@
+/*********************                                                        */
+/*! \file Datatypes.java
+ ** \verbatim
+ ** Original author: Morgan Deters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2013  New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief An example of using inductive datatypes in CVC4 (Java version)
+ **
+ ** An example of using inductive datatypes in CVC4 (Java version).
+ **/
+
+import edu.nyu.acsys.CVC4.*;
+import java.util.Iterator;
+
+public class Datatypes {
+  public static void main(String[] args) {
+    System.loadLibrary("cvc4jni");
+
+    ExprManager em = new ExprManager();
+    Expr helloworld = em.mkVar("Hello World!", em.booleanType());
+    SmtEngine smt = new SmtEngine(em);
+
+    // 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"---at which point function
+    // symbols are assigned to its constructors, selectors, and testers.
+
+    Datatype consListSpec = new Datatype("list"); // give the datatype a name
+    DatatypeConstructor cons = new DatatypeConstructor("cons");
+    cons.addArg("head", em.integerType());
+    cons.addArg("tail", new DatatypeSelfType()); // a list
+    consListSpec.addConstructor(cons);
+    DatatypeConstructor nil = new DatatypeConstructor("nil");
+    consListSpec.addConstructor(nil);
+
+    System.out.println("spec is:");
+    System.out.println(consListSpec);
+
+    // Keep in mind that "Datatype" is the specification class for
+    // datatypes---"Datatype" is not itself a CVC4 Type.  Now that
+    // our Datatype is fully specified, we can get a Type for it.
+    // This step resolves the "SelfType" reference and creates
+    // symbols for all the constructors, etc.
+
+    DatatypeType consListType = em.mkDatatypeType(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 DatatypeType, and
+    // this Datatype object has constructor symbols (and others) filled in.
+
+    Datatype consList = consListType.getDatatype();
+
+    // e = cons 0 nil
+    //
+    // Here, consList.get("cons") gives you the DatatypeConstructor
+    // (just as consList["cons"] does in C++).  To get the constructor
+    // symbol for application, use .getConstructor("cons"), which is
+    // equivalent to consList.get("cons").getConstructor().  Note that
+    // "nil" is a constructor too, so it needs to be applied with
+    // APPLY_CONSTRUCTOR, even though it has no arguments.
+    Expr e = em.mkExpr(Kind.APPLY_CONSTRUCTOR,
+                       consList.getConstructor("cons"),
+                       em.mkConst(new Rational(0)),
+                       em.mkExpr(Kind.APPLY_CONSTRUCTOR,
+                                 consList.getConstructor("nil")));
+
+    System.out.println("e is " + e);
+    System.out.println("type of cons is " +
+                       consList.getConstructor("cons").getType());
+    System.out.println("type of nil is " +
+                       consList.getConstructor("nil").getType());
+
+    // e2 = head(cons 0 nil), and of course this can be evaluated
+    //
+    // Here we first get the DatatypeConstructor for cons (with
+    // consList.get("cons") in order to get the "head" selector
+    // symbol to apply.
+    Expr e2 = em.mkExpr(Kind.APPLY_SELECTOR,
+                        consList.get("cons").getSelector("head"),
+                        e);
+
+    System.out.println("e2 is " + e2);
+    System.out.println("simplify(e2) is " + smt.simplify(e2));
+    System.out.println();
+
+    // You can also iterate over a Datatype to get all its constructors,
+    // and over a DatatypeConstructor to get all its "args" (selectors)
+    for(Iterator<DatatypeConstructor> i = consList.iterator(); i.hasNext();) {
+      DatatypeConstructor ctor = i.next();
+      System.out.println("ctor: " + ctor);
+      for(Iterator j = ctor.iterator(); j.hasNext();) {
+        System.out.println(" + arg: " + j.next());
+      }
+    }
+  }
+}
diff --git a/examples/api/java/Makefile.am b/examples/api/java/Makefile.am
index f4b8f1043..7216d758e 100644
--- a/examples/api/java/Makefile.am
+++ b/examples/api/java/Makefile.am
@@ -8,6 +8,7 @@ noinst_DATA += \
 	Combination.class \
 	HelloWorld.class \
 	LinearArith.class \
+	Datatypes.class \
 	PipedInput.class
 endif
 
@@ -21,6 +22,7 @@ EXTRA_DIST = \
 	Combination.java \
 	HelloWorld.java \
 	LinearArith.java \
+	Datatypes.java \
 	PipedInput.java
 
 # for installation