version of CVC4. However, the new configure option "--bsd" disables
these GPL dependences and builds the best-performing BSD-licenced version
of CVC4.
+* Small API adjustments to Datatypes to even out the API and make it
+ function better in Java.
Changes since 1.2
=================
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
*** 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
helloworld \
combination \
bitvectors \
- bitvectors_and_arrays
-
+ bitvectors_and_arrays \
+ datatypes
noinst_DATA =
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)
--- /dev/null
+/********************* */
+/*! \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;
+}
--- /dev/null
+/********************* */
+/*! \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());
+ }
+ }
+ }
+}
Combination.class \
HelloWorld.class \
LinearArith.class \
+ Datatypes.class \
PipedInput.class
endif
Combination.java \
HelloWorld.java \
LinearArith.java \
+ Datatypes.java \
PipedInput.java
# for installation
%include "util/record.i"
%include "util/regexp.i"
%include "util/uninterpreted_constant.i"
+%include "util/proof.i"
%include "expr/kind.i"
%include "expr/expr.i"
virtual void printResolutions(std::ostream& out, std::ostream& paren) = 0;
};/* class SatProof */
-class LFSCSatProof: public SatProof {
+class LFSCSatProof : public SatProof {
private:
void printResolution(ClauseId id, std::ostream& out, std::ostream& paren);
public:
void addDeclaration(Expr atom);
};
- class LFSCTheoryProof: public TheoryProof {
+ class LFSCTheoryProof : public TheoryProof {
void printDeclarations(std::ostream& os, std::ostream& paren);
public:
static void printTerm(Expr term, std::ostream& os);
const uint64_t mark = (*j).second;
const unsigned numVars = pos.getKind() == kind::AND ? pos.getNumChildren() : 1;
uint64_t expected = (uint64_t(1) << (1 << numVars)) - 1;
- expected = (expected == 0) ? -1 : expected;// fix for overflow
+ expected = (expected == 0) ? -1 : expected; // fix for overflow
Debug("miplib") << "[" << pos << "] => " << hex << mark << " expect " << expected << dec << endl;
Assert(pos.getKind() == kind::AND || pos.isVar());
if(mark != expected) {
} else {
if(mark != 3) { // exclude single-var case; nothing to check there
uint64_t sz = (uint64_t(1) << checks[pos_var].size()) - 1;
- sz = (sz == 0) ? -1 : sz;// fix for overflow
+ sz = (sz == 0) ? -1 : sz; // fix for overflow
Assert(sz == mark, "expected size %u == mark %u", sz, mark);
for(size_t k = 0; k < checks[pos_var].size(); ++k) {
if((k & (k - 1)) != 0) {
break;
}
} else {
- Assert(checks[pos_var][k] == 0, "checks[(%s,%s)][%u] should be 0, but it's %s", pos.toString().c_str(), var.toString().c_str(), k, checks[pos_var][k].toString().c_str());// we never set for single-positive-var
+ Assert(checks[pos_var][k] == 0, "checks[(%s,%s)][%u] should be 0, but it's %s", pos.toString().c_str(), var.toString().c_str(), k, checks[pos_var][k].toString().c_str()); // we never set for single-positive-var
}
}
}
if(!eligible) {
- eligible = true;// next is still eligible
+ eligible = true; // next is still eligible
continue;
}
Node leq = Rewriter::rewrite(nm->mkNode(kind::LEQ, newVar, one));
d_assertionsToCheck.push_back(Rewriter::rewrite(geq.andNode(leq)));
SubstitutionMap nullMap(&d_fakeContext);
- Theory::PPAssertStatus status CVC4_UNUSED;// just for assertions
+ Theory::PPAssertStatus status CVC4_UNUSED; // just for assertions
status = d_smt.d_theoryEngine->solve(geq, nullMap);
Assert(status == Theory::PP_ASSERT_STATUS_UNSOLVED,
"unexpected solution from arith's ppAssert()");
Expr e = d_private->substituteAbstractValues(Node::fromExpr(ex)).toExpr();
if( options::typeChecking() ) {
- e.getType(true);// ensure expr is type-checked at this point
+ e.getType(true); // ensure expr is type-checked at this point
}
// Make sure all preprocessing is done
}
%ignore CVC4::SmtEngine::setLogic(const char*);
-%ignore CVC4::SmtEngine::getProof;
%ignore CVC4::stats::getStatisticsRegistry(SmtEngine*);
%ignore CVC4::smt::beforeSearch(std::string, bool, SmtEngine*);
+%ignore CVC4::smt::currentProofManager();
%include "smt/smt_engine.h"
CheckArgument(&self.getDatatype() == this, resolutions, "Datatype::resolve(): resolutions doesn't contain me!");
d_resolved = true;
size_t index = 0;
- for(iterator i = begin(), i_end = end(); i != i_end; ++i) {
+ for(std::vector<DatatypeConstructor>::iterator i = d_constructors.begin(), i_end = d_constructors.end(); i != i_end; ++i) {
(*i).resolve(em, self, resolutions, placeholders, replacements, paramTypes, paramReplacements);
Node::fromExpr((*i).d_constructor).setAttribute(DatatypeIndexAttr(), index);
Node::fromExpr((*i).d_tester).setAttribute(DatatypeIndexAttr(), index++);
NodeManager* nm = NodeManager::fromExprManager(em);
TypeNode selfTypeNode = TypeNode::fromType(self);
size_t index = 0;
- for(iterator i = begin(), i_end = end(); i != i_end; ++i) {
+ for(std::vector<DatatypeConstructorArg>::iterator i = d_args.begin(), i_end = d_args.end(); i != i_end; ++i) {
if((*i).d_selector.isNull()) {
// the unresolved type wasn't created here; do name resolution
string typeName = (*i).d_name.substr((*i).d_name.find('\0') + 1);
d_tester = nm->mkSkolem(getTesterName(), nm->mkTesterType(selfTypeNode), "is a tester", NodeManager::SKOLEM_EXACT_NAME | NodeManager::SKOLEM_NO_NOTIFY).toExpr();
d_constructor = nm->mkSkolem(getName(), nm->mkConstructorType(*this, selfTypeNode), "is a constructor", NodeManager::SKOLEM_EXACT_NAME | NodeManager::SKOLEM_NO_NOTIFY).toExpr();
// associate constructor with all selectors
- for(iterator i = begin(), i_end = end(); i != i_end; ++i) {
+ for(std::vector<DatatypeConstructorArg>::iterator i = d_args.begin(), i_end = d_args.end(); i != i_end; ++i) {
(*i).d_constructor = d_constructor;
}
}
class CVC4_PUBLIC ExprManager;
+class CVC4_PUBLIC DatatypeConstructor;
+class CVC4_PUBLIC DatatypeConstructorArg;
+
+class CVC4_PUBLIC DatatypeConstructorIterator {
+ const std::vector<DatatypeConstructor>* d_v;
+ size_t d_i;
+
+ friend class Datatype;
+
+ DatatypeConstructorIterator(const std::vector<DatatypeConstructor>& v, bool start) : d_v(&v), d_i(start ? 0 : v.size()) {
+ }
+
+public:
+ typedef const DatatypeConstructor& value_type;
+ const DatatypeConstructor& operator*() const { return (*d_v)[d_i]; }
+ const DatatypeConstructor* operator->() const { return &(*d_v)[d_i]; }
+ DatatypeConstructorIterator& operator++() { ++d_i; return *this; }
+ DatatypeConstructorIterator operator++(int) { DatatypeConstructorIterator i(*this); ++d_i; return i; }
+ bool operator==(const DatatypeConstructorIterator& other) const { return d_v == other.d_v && d_i == other.d_i; }
+ bool operator!=(const DatatypeConstructorIterator& other) const { return d_v != other.d_v || d_i != other.d_i; }
+};/* class DatatypeConstructorIterator */
+
+class CVC4_PUBLIC DatatypeConstructorArgIterator {
+ const std::vector<DatatypeConstructorArg>* d_v;
+ size_t d_i;
+
+ friend class DatatypeConstructor;
+
+ DatatypeConstructorArgIterator(const std::vector<DatatypeConstructorArg>& v, bool start) : d_v(&v), d_i(start ? 0 : v.size()) {
+ }
+
+public:
+ typedef const DatatypeConstructorArg& value_type;
+ const DatatypeConstructorArg& operator*() const { return (*d_v)[d_i]; }
+ const DatatypeConstructorArg* operator->() const { return &(*d_v)[d_i]; }
+ DatatypeConstructorArgIterator& operator++() { ++d_i; return *this; }
+ DatatypeConstructorArgIterator operator++(int) { DatatypeConstructorArgIterator i(*this); ++d_i; return i; }
+ bool operator==(const DatatypeConstructorArgIterator& other) const { return d_v == other.d_v && d_i == other.d_i; }
+ bool operator!=(const DatatypeConstructorArgIterator& other) const { return d_v != other.d_v || d_i != other.d_i; }
+};/* class DatatypeConstructorArgIterator */
+
/**
* An exception that is thrown when a datatype resolution fails.
*/
public:
/** The type for iterators over constructor arguments. */
- typedef std::vector<DatatypeConstructorArg>::iterator iterator;
+ typedef DatatypeConstructorArgIterator iterator;
/** The (const) type for iterators over constructor arguments. */
- typedef std::vector<DatatypeConstructorArg>::const_iterator const_iterator;
+ typedef DatatypeConstructorArgIterator const_iterator;
private:
static size_t indexOf(Expr item) CVC4_PUBLIC;
/** The type for iterators over constructors. */
- typedef std::vector<DatatypeConstructor>::iterator iterator;
+ typedef DatatypeConstructorIterator iterator;
/** The (const) type for iterators over constructors. */
- typedef std::vector<DatatypeConstructor>::const_iterator const_iterator;
+ typedef DatatypeConstructorIterator const_iterator;
private:
std::string d_name;
inline bool isResolved() const throw();
/** Get the beginning iterator over DatatypeConstructors. */
- inline std::vector<DatatypeConstructor>::iterator begin() throw();
+ inline iterator begin() throw();
/** Get the ending iterator over DatatypeConstructors. */
- inline std::vector<DatatypeConstructor>::iterator end() throw();
+ inline iterator end() throw();
/** Get the beginning const_iterator over DatatypeConstructors. */
- inline std::vector<DatatypeConstructor>::const_iterator begin() const throw();
+ inline const_iterator begin() const throw();
/** Get the ending const_iterator over DatatypeConstructors. */
- inline std::vector<DatatypeConstructor>::const_iterator end() const throw();
+ inline const_iterator end() const throw();
/** Get the ith DatatypeConstructor. */
const DatatypeConstructor& operator[](size_t index) const;
}
inline Datatype::iterator Datatype::begin() throw() {
- return d_constructors.begin();
+ return iterator(d_constructors, true);
}
inline Datatype::iterator Datatype::end() throw() {
- return d_constructors.end();
+ return iterator(d_constructors, false);
}
inline Datatype::const_iterator Datatype::begin() const throw() {
- return d_constructors.begin();
+ return const_iterator(d_constructors, true);
}
inline Datatype::const_iterator Datatype::end() const throw() {
- return d_constructors.end();
+ return const_iterator(d_constructors, false);
}
inline bool DatatypeConstructor::isResolved() const throw() {
}
inline DatatypeConstructor::iterator DatatypeConstructor::begin() throw() {
- return d_args.begin();
+ return iterator(d_args, true);
}
inline DatatypeConstructor::iterator DatatypeConstructor::end() throw() {
- return d_args.end();
+ return iterator(d_args, false);
}
inline DatatypeConstructor::const_iterator DatatypeConstructor::begin() const throw() {
- return d_args.begin();
+ return const_iterator(d_args, true);
}
inline DatatypeConstructor::const_iterator DatatypeConstructor::end() const throw() {
- return d_args.end();
+ return const_iterator(d_args, false);
}
}/* CVC4 namespace */
%{
#include "util/datatype.h"
+
+#ifdef SWIGJAVA
+
+#include "bindings/java_iterator_adapter.h"
+#include "bindings/java_stream_adapters.h"
+
+#endif /* SWIGJAVA */
%}
%extend std::vector< CVC4::Datatype > {
%ignore set(int i, const CVC4::Datatype::Constructor& x);
%ignore to_array();
};
-%template(vectorDatatypeConstructor) std::vector< CVC4::DatatypeConstructor >;
+//%template(vectorDatatypeConstructor) std::vector< CVC4::DatatypeConstructor >;
%rename(equals) CVC4::Datatype::operator==(const Datatype&) const;
%ignore CVC4::Datatype::operator!=(const Datatype&) const;
-%rename(beginConst) CVC4::Datatype::begin() const;
-%rename(endConst) CVC4::Datatype::end() const;
+%ignore CVC4::Datatype::begin();
+%ignore CVC4::Datatype::end();
+%ignore CVC4::Datatype::begin() const;
+%ignore CVC4::Datatype::end() const;
-%rename(getConstructor) CVC4::Datatype::operator[](size_t) const;
-%ignore CVC4::Datatype::operator[](std::string) const;
+%rename(get) CVC4::Datatype::operator[](size_t) const;
+%rename(get) CVC4::Datatype::operator[](std::string) const;
%rename(apply) CVC4::DatatypeHashFunction::operator()(const Datatype&) const;
%ignore CVC4::DatatypeHashFunction::operator()(const Datatype*) const;
%rename(apply) CVC4::DatatypeHashFunction::operator()(const DatatypeConstructor&) const;
%ignore CVC4::DatatypeHashFunction::operator()(const DatatypeConstructor*) const;
-%rename(beginConst) CVC4::DatatypeConstructor::begin() const;
-%rename(endConst) CVC4::DatatypeConstructor::end() const;
+%ignore CVC4::DatatypeConstructor::begin();
+%ignore CVC4::DatatypeConstructor::end();
+%ignore CVC4::DatatypeConstructor::begin() const;
+%ignore CVC4::DatatypeConstructor::end() const;
-%rename(getArg) CVC4::DatatypeConstructor::operator[](size_t) const;
-%rename(getArg) CVC4::DatatypeConstructor::operator[](std::string) const;
+%rename(get) CVC4::DatatypeConstructor::operator[](size_t) const;
+%rename(get) CVC4::DatatypeConstructor::operator[](std::string) const;
%ignore CVC4::operator<<(std::ostream&, const Datatype&);
%ignore CVC4::operator<<(std::ostream&, const DatatypeConstructor&);
%ignore CVC4::operator<<(std::ostream&, const DatatypeConstructorArg&);
+%ignore CVC4::DatatypeConstructorIterator;
+%ignore CVC4::DatatypeConstructorArgIterator;
+
%feature("valuewrapper") CVC4::DatatypeUnresolvedType;
%feature("valuewrapper") CVC4::DatatypeConstructor;
+#ifdef SWIGJAVA
+
+// Instead of Datatype::begin() and end(), create an
+// iterator() method on the Java side that returns a Java-style
+// Iterator.
+%extend CVC4::Datatype {
+ CVC4::JavaIteratorAdapter<CVC4::Datatype> iterator() {
+ return CVC4::JavaIteratorAdapter<CVC4::Datatype>(*$self);
+ }
+
+ std::string toString() const {
+ std::stringstream ss;
+ ss << *$self;
+ return ss.str();
+ }
+}
+%extend CVC4::DatatypeConstructor {
+ CVC4::JavaIteratorAdapter<CVC4::DatatypeConstructor> iterator() {
+ return CVC4::JavaIteratorAdapter<CVC4::DatatypeConstructor>(*$self);
+ }
+
+ std::string toString() const {
+ std::stringstream ss;
+ ss << *$self;
+ return ss.str();
+ }
+}
+%extend CVC4::DatatypeConstructorArg {
+ std::string toString() const {
+ std::stringstream ss;
+ ss << *$self;
+ return ss.str();
+ }
+}
+
+// Datatype is "iterable" on the Java side
+%typemap(javainterfaces) CVC4::Datatype "java.lang.Iterable<DatatypeConstructor>";
+%typemap(javainterfaces) CVC4::DatatypeConstructor "java.lang.Iterable<DatatypeConstructorArg>";
+
+// the JavaIteratorAdapter should not be public, and implements Iterator
+%typemap(javaclassmodifiers) CVC4::JavaIteratorAdapter<CVC4::Datatype> "class";
+%typemap(javaclassmodifiers) CVC4::JavaIteratorAdapter<CVC4::DatatypeConstructor> "class";
+%typemap(javainterfaces) CVC4::JavaIteratorAdapter<CVC4::Datatype> "java.util.Iterator<DatatypeConstructor>";
+%typemap(javainterfaces) CVC4::JavaIteratorAdapter<CVC4::DatatypeConstructor> "java.util.Iterator<DatatypeConstructorArg>";
+// add some functions to the Java side (do it here because there's no way to do these in C++)
+%typemap(javacode) CVC4::JavaIteratorAdapter<CVC4::Datatype> "
+ public void remove() {
+ throw new java.lang.UnsupportedOperationException();
+ }
+
+ public DatatypeConstructor next() {
+ if(hasNext()) {
+ return getNext();
+ } else {
+ throw new java.util.NoSuchElementException();
+ }
+ }
+"
+%typemap(javacode) CVC4::JavaIteratorAdapter<CVC4::DatatypeConstructor> "
+ public void remove() {
+ throw new java.lang.UnsupportedOperationException();
+ }
+
+ public DatatypeConstructorArg next() {
+ if(hasNext()) {
+ return getNext();
+ } else {
+ throw new java.util.NoSuchElementException();
+ }
+ }
+"
+// getNext() just allows C++ iterator access from Java-side next(), make it private
+%javamethodmodifiers CVC4::JavaIteratorAdapter<CVC4::Datatype>::getNext() "private";
+%javamethodmodifiers CVC4::JavaIteratorAdapter<CVC4::DatatypeConstructor>::getNext() "private";
+
+// map the types appropriately.
+%typemap(jni) CVC4::Datatype::iterator::value_type "jobject";
+%typemap(jtype) CVC4::Datatype::iterator::value_type "edu.nyu.acsys.CVC4.DatatypeConstructor";
+%typemap(jstype) CVC4::Datatype::iterator::value_type "edu.nyu.acsys.CVC4.DatatypeConstructor";
+%typemap(javaout) CVC4::Datatype::iterator::value_type { return $jnicall; }
+%typemap(jni) CVC4::DatatypeConstructor::iterator::value_type "jobject";
+%typemap(jtype) CVC4::DatatypeConstructor::iterator::value_type "edu.nyu.acsys.CVC4.DatatypeConstructorArg";
+%typemap(jstype) CVC4::DatatypeConstructor::iterator::value_type "edu.nyu.acsys.CVC4.DatatypeConstructorArg";
+%typemap(javaout) CVC4::DatatypeConstructor::iterator::value_type { return $jnicall; }
+
+#endif /* SWIGJAVA */
+
%include "util/datatype.h"
+#ifdef SWIGJAVA
+
+%include "bindings/java_iterator_adapter.h"
+%include "bindings/java_stream_adapters.h"
+
+%template(JavaIteratorAdapter_Datatype) CVC4::JavaIteratorAdapter<CVC4::Datatype>;
+%template(JavaIteratorAdapter_DatatypeConstructor) CVC4::JavaIteratorAdapter<CVC4::DatatypeConstructor>;
+
+#endif /* SWIGJAVA */
--- /dev/null
+%{
+#include "util/proof.h"
+%}
+
+%include "util/proof.h"
projects / cvc5.git / commitdiff