From 8cde77abf105c7c712b72da6e25f695a687559a1 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Mon, 3 Jun 2013 18:18:24 -0400 Subject: [PATCH] Java datatype API fixups, datatype API examples --- NEWS | 2 + examples/README | 19 ++--- examples/api/Makefile.am | 9 ++- examples/api/datatypes.cpp | 105 +++++++++++++++++++++++++ examples/api/java/Datatypes.java | 104 +++++++++++++++++++++++++ examples/api/java/Makefile.am | 2 + src/cvc4.i | 1 + src/proof/sat_proof.h | 2 +- src/proof/theory_proof.h | 2 +- src/smt/smt_engine.cpp | 12 +-- src/smt/smt_engine.i | 2 +- src/util/datatype.cpp | 6 +- src/util/datatype.h | 73 ++++++++++++++---- src/util/datatype.i | 128 ++++++++++++++++++++++++++++--- src/util/proof.i | 5 ++ 15 files changed, 424 insertions(+), 48 deletions(-) create mode 100644 examples/api/datatypes.cpp create mode 100644 examples/api/java/Datatypes.java create mode 100644 src/util/proof.i diff --git a/NEWS b/NEWS index dd1de35a4..74b9a6c0a 100644 --- a/NEWS +++ b/NEWS @@ -12,6 +12,8 @@ Changes since 1.3 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 ================= 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 Wed, 03 Oct 2012 15:47:33 -0400 +-- Morgan Deters 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 +#include "smt/smt_engine.h" // for use with make examples +#include "util/language.h" // for use with make examples +//#include // 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 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 diff --git a/src/cvc4.i b/src/cvc4.i index ec3aa43cb..aadbc374d 100644 --- a/src/cvc4.i +++ b/src/cvc4.i @@ -269,6 +269,7 @@ std::set CVC4::JavaInputStreamAdapter::s_adapters; %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" diff --git a/src/proof/sat_proof.h b/src/proof/sat_proof.h index 477eeeb99..d555ca529 100644 --- a/src/proof/sat_proof.h +++ b/src/proof/sat_proof.h @@ -253,7 +253,7 @@ public: 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: diff --git a/src/proof/theory_proof.h b/src/proof/theory_proof.h index 739299b7d..0a7772a4b 100644 --- a/src/proof/theory_proof.h +++ b/src/proof/theory_proof.h @@ -44,7 +44,7 @@ namespace CVC4 { 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); diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index ec37eaf26..f26456cae 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -2506,7 +2506,7 @@ void SmtEnginePrivate::doMiplibTrick() { 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) { @@ -2514,7 +2514,7 @@ void SmtEnginePrivate::doMiplibTrick() { } 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) { @@ -2534,12 +2534,12 @@ void SmtEnginePrivate::doMiplibTrick() { 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; } @@ -2563,7 +2563,7 @@ void SmtEnginePrivate::doMiplibTrick() { 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()"); @@ -3493,7 +3493,7 @@ Expr SmtEngine::simplify(const Expr& ex) throw(TypeCheckingException, LogicExcep 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 diff --git a/src/smt/smt_engine.i b/src/smt/smt_engine.i index ff4105241..00c332bd1 100644 --- a/src/smt/smt_engine.i +++ b/src/smt/smt_engine.i @@ -43,8 +43,8 @@ SWIGEXPORT void JNICALL Java_edu_nyu_acsys_CVC4_SmtEngine_dlRef(JNIEnv* jenv, jc } %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" diff --git a/src/util/datatype.cpp b/src/util/datatype.cpp index 5fa893336..8d70e4ffc 100644 --- a/src/util/datatype.cpp +++ b/src/util/datatype.cpp @@ -102,7 +102,7 @@ void Datatype::resolve(ExprManager* em, 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::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++); @@ -416,7 +416,7 @@ void DatatypeConstructor::resolve(ExprManager* em, DatatypeType self, 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::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); @@ -461,7 +461,7 @@ void DatatypeConstructor::resolve(ExprManager* em, DatatypeType self, 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::iterator i = d_args.begin(), i_end = d_args.end(); i != i_end; ++i) { (*i).d_constructor = d_constructor; } } diff --git a/src/util/datatype.h b/src/util/datatype.h index 802704803..99a303950 100644 --- a/src/util/datatype.h +++ b/src/util/datatype.h @@ -40,6 +40,47 @@ namespace CVC4 { class CVC4_PUBLIC ExprManager; +class CVC4_PUBLIC DatatypeConstructor; +class CVC4_PUBLIC DatatypeConstructorArg; + +class CVC4_PUBLIC DatatypeConstructorIterator { + const std::vector* d_v; + size_t d_i; + + friend class Datatype; + + DatatypeConstructorIterator(const std::vector& 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* d_v; + size_t d_i; + + friend class DatatypeConstructor; + + DatatypeConstructorArgIterator(const std::vector& 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. */ @@ -134,9 +175,9 @@ class CVC4_PUBLIC DatatypeConstructor { public: /** The type for iterators over constructor arguments. */ - typedef std::vector::iterator iterator; + typedef DatatypeConstructorArgIterator iterator; /** The (const) type for iterators over constructor arguments. */ - typedef std::vector::const_iterator const_iterator; + typedef DatatypeConstructorArgIterator const_iterator; private: @@ -394,9 +435,9 @@ public: static size_t indexOf(Expr item) CVC4_PUBLIC; /** The type for iterators over constructors. */ - typedef std::vector::iterator iterator; + typedef DatatypeConstructorIterator iterator; /** The (const) type for iterators over constructors. */ - typedef std::vector::const_iterator const_iterator; + typedef DatatypeConstructorIterator const_iterator; private: std::string d_name; @@ -540,13 +581,13 @@ public: inline bool isResolved() const throw(); /** Get the beginning iterator over DatatypeConstructors. */ - inline std::vector::iterator begin() throw(); + inline iterator begin() throw(); /** Get the ending iterator over DatatypeConstructors. */ - inline std::vector::iterator end() throw(); + inline iterator end() throw(); /** Get the beginning const_iterator over DatatypeConstructors. */ - inline std::vector::const_iterator begin() const throw(); + inline const_iterator begin() const throw(); /** Get the ending const_iterator over DatatypeConstructors. */ - inline std::vector::const_iterator end() const throw(); + inline const_iterator end() const throw(); /** Get the ith DatatypeConstructor. */ const DatatypeConstructor& operator[](size_t index) const; @@ -669,19 +710,19 @@ inline bool Datatype::isResolved() const throw() { } 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() { @@ -710,19 +751,19 @@ inline bool DatatypeConstructorArg::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 */ diff --git a/src/util/datatype.i b/src/util/datatype.i index c07caa805..403fb31bc 100644 --- a/src/util/datatype.i +++ b/src/util/datatype.i @@ -1,5 +1,12 @@ %{ #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 > { @@ -32,34 +39,137 @@ %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 iterator() { + return CVC4::JavaIteratorAdapter(*$self); + } + + std::string toString() const { + std::stringstream ss; + ss << *$self; + return ss.str(); + } +} +%extend CVC4::DatatypeConstructor { + CVC4::JavaIteratorAdapter iterator() { + return CVC4::JavaIteratorAdapter(*$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"; +%typemap(javainterfaces) CVC4::DatatypeConstructor "java.lang.Iterable"; + +// the JavaIteratorAdapter should not be public, and implements Iterator +%typemap(javaclassmodifiers) CVC4::JavaIteratorAdapter "class"; +%typemap(javaclassmodifiers) CVC4::JavaIteratorAdapter "class"; +%typemap(javainterfaces) CVC4::JavaIteratorAdapter "java.util.Iterator"; +%typemap(javainterfaces) CVC4::JavaIteratorAdapter "java.util.Iterator"; +// add some functions to the Java side (do it here because there's no way to do these in C++) +%typemap(javacode) CVC4::JavaIteratorAdapter " + 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 " + 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::getNext() "private"; +%javamethodmodifiers CVC4::JavaIteratorAdapter::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; +%template(JavaIteratorAdapter_DatatypeConstructor) CVC4::JavaIteratorAdapter; + +#endif /* SWIGJAVA */ diff --git a/src/util/proof.i b/src/util/proof.i new file mode 100644 index 000000000..22dff1043 --- /dev/null +++ b/src/util/proof.i @@ -0,0 +1,5 @@ +%{ +#include "util/proof.h" +%} + +%include "util/proof.h" -- 2.30.2