diff options
author | Morgan Deters <mdeters@cs.nyu.edu> | 2013-06-03 18:18:24 -0400 |
---|---|---|
committer | Morgan Deters <mdeters@cs.nyu.edu> | 2013-12-24 10:55:46 -0500 |
commit | 8cde77abf105c7c712b72da6e25f695a687559a1 (patch) | |
tree | 0460a176b91586b73d6970323dec69ad3ba36259 /examples | |
parent | ff7d33c2f75668fde0f149943e3cf1bedad1102f (diff) |
Java datatype API fixups, datatype API examples
Diffstat (limited to 'examples')
-rw-r--r-- | examples/README | 19 | ||||
-rw-r--r-- | examples/api/Makefile.am | 9 | ||||
-rw-r--r-- | examples/api/datatypes.cpp | 105 | ||||
-rw-r--r-- | examples/api/java/Datatypes.java | 104 | ||||
-rw-r--r-- | examples/api/java/Makefile.am | 2 |
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 |