From a63064385c56600143ac470108fe8e640a4ca3ee Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Fri, 23 Sep 2011 23:37:42 +0000 Subject: [PATCH] interface cleanup, java bindings work --- src/bindings/Makefile.am | 2 +- src/cvc4.i | 45 +++++++++++++++++++++++++++----- src/expr/Makefile.am | 1 + src/expr/expr_manager_template.h | 4 --- src/expr/expr_stream.i | 5 ++++ src/util/ascription_type.i | 1 - src/util/datatype.h | 12 ++++----- src/util/datatype.i | 19 ++++++++++++++ src/util/integer.h.in | 6 +++++ src/util/rational.h.in | 6 +++++ src/util/stats.h | 38 +++++++++++++-------------- 11 files changed, 102 insertions(+), 37 deletions(-) create mode 100644 src/expr/expr_stream.i diff --git a/src/bindings/Makefile.am b/src/bindings/Makefile.am index 31ad8c71f..c0c7f352e 100644 --- a/src/bindings/Makefile.am +++ b/src/bindings/Makefile.am @@ -81,7 +81,7 @@ ruby.cpp: tcl.cpp: $(patsubst %,%.cpp,$(filter-out c c++,$(CVC4_LANGUAGE_BINDINGS))): %.cpp: @srcdir@/../cvc4.i $(AM_V_at)mkdir -p $(patsubst %.cpp,%,$@) - $(AM_V_GEN)$(SWIG) -I@srcdir@/../include -I@srcdir@/.. -I@builddir@/.. -c++ -$(patsubst %.cpp,%,$@) -outdir $(patsubst %.cpp,%,$@) -package edu.nyu.acsys.CVC4 -o $@ $< + $(AM_V_GEN)$(SWIG) -Wall -I@srcdir@/../include -I@srcdir@/.. -I@builddir@/.. -c++ -$(patsubst %.cpp,%,$@) -outdir $(patsubst %.cpp,%,$@) -package edu.nyu.acsys.CVC4 -o $@ $< $(patsubst %,%.d,$(filter-out c c++,$(CVC4_LANGUAGE_BINDINGS))): %.d: @srcdir@/../cvc4.i $(AM_V_GEN)$(SWIG) -I@srcdir@/../include -I@srcdir@/.. -I@builddir@/.. -c++ -MM -o $(patsubst %.d,%.cpp,$@) $< diff --git a/src/cvc4.i b/src/cvc4.i index 03c258778..7f7926bfd 100644 --- a/src/cvc4.i +++ b/src/cvc4.i @@ -1,14 +1,45 @@ %import "bindings/swig.h" +%include "stdint.i" +%include "stl.i" %module CVC4 // nspace completely broken with Java packaging //%nspace; +namespace std { + class istream; + class ostream; + template class set {}; + template class hash_map {}; +} + %{ -namespace CVC4 { class Exception; } +namespace CVC4 {} using namespace CVC4; + +#include +#include +#include +#include +#include + +#include "util/sexpr.h" +#include "util/exception.h" +#include "expr/type.h" +#include "expr/expr.h" +#include "util/datatype.h" +#include "expr/command.h" %} +%template(vectorCommandPtr) std::vector< CVC4::Command* >; +%template(vectorType) std::vector< CVC4::Type >; +%template(vectorExpr) std::vector< CVC4::Expr >; +%template(vectorDatatypeType) std::vector< CVC4::DatatypeType >; +%template(vectorSExpr) std::vector< CVC4::SExpr >; +%template(vectorString) std::vector< std::string >; +%template(setType) std::set< CVC4::Type >; +%template(hashmapExpr) std::hash_map< CVC4::Expr, CVC4::Expr, CVC4::ExprHashFunction >; + %exception { try { $action @@ -38,7 +69,6 @@ using namespace CVC4; %include "util/cardinality.i" %include "util/bool.i" %include "util/sexpr.i" -%include "util/datatype.i" %include "util/output.i" %include "util/result.i" %include "util/configuration.i" @@ -46,16 +76,19 @@ using namespace CVC4; %include "util/bitvector.i" %include "util/subrange_bound.i" %include "util/array.i" -%include "util/ascription_type.i" %include "util/pseudoboolean.i" %include "util/hash.i" -%include "expr/command.i" -%include "expr/declaration_scope.i" -%include "expr/kind.i" %include "expr/type.i" +%include "util/ascription_type.i" +%include "util/datatype.i" + +%include "expr/kind.i" %include "expr/expr.i" +%include "expr/command.i" +%include "expr/declaration_scope.i" %include "expr/expr_manager.i" +%include "expr/expr_stream.i" %include "smt/smt_engine.i" %include "smt/bad_option_exception.i" diff --git a/src/expr/Makefile.am b/src/expr/Makefile.am index 03de15706..14fee33c9 100644 --- a/src/expr/Makefile.am +++ b/src/expr/Makefile.am @@ -53,6 +53,7 @@ EXTRA_DIST = \ mkkind \ mkmetakind \ mkexpr \ + expr_stream.i \ expr_manager.i \ declaration_scope.i \ command.i \ diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h index 2828ae381..77b92c873 100644 --- a/src/expr/expr_manager_template.h +++ b/src/expr/expr_manager_template.h @@ -376,10 +376,6 @@ public: /** Make a new sort with the given name. */ SortType mkSort(const std::string& name) const; - /** Make a new sort from a constructor. */ - SortType mkSort(SortConstructorType constructor, - const std::vector& children) const; - /** Make a sort constructor from a name and arity. */ SortConstructorType mkSortConstructor(const std::string& name, size_t arity) const; diff --git a/src/expr/expr_stream.i b/src/expr/expr_stream.i new file mode 100644 index 000000000..f1144623b --- /dev/null +++ b/src/expr/expr_stream.i @@ -0,0 +1,5 @@ +%{ +#include "expr/expr_stream.h" +%} + +%include "expr/expr_stream.h" diff --git a/src/util/ascription_type.i b/src/util/ascription_type.i index b0b57d5f9..d0b435a4d 100644 --- a/src/util/ascription_type.i +++ b/src/util/ascription_type.i @@ -2,7 +2,6 @@ #include "util/ascription_type.h" %} - %rename(equals) CVC4::AscriptionType::operator==(const AscriptionType&) const; %ignore CVC4::AscriptionType::operator!=(const AscriptionType&) const; diff --git a/src/util/datatype.h b/src/util/datatype.h index c64f420dd..148d85870 100644 --- a/src/util/datatype.h +++ b/src/util/datatype.h @@ -326,9 +326,9 @@ public: };/* class Datatype::Constructor */ /** The type for iterators over constructors. */ - typedef std::vector::iterator iterator; + typedef typename std::vector::iterator iterator; /** The (const) type for iterators over constructors. */ - typedef std::vector::const_iterator const_iterator; + typedef typename std::vector::const_iterator const_iterator; private: std::string d_name; @@ -448,13 +448,13 @@ public: inline bool isResolved() const throw(); /** Get the beginning iterator over Constructors. */ - inline iterator begin() throw(); + inline std::vector::iterator begin() throw(); /** Get the ending iterator over Constructors. */ - inline iterator end() throw(); + inline std::vector::iterator end() throw(); /** Get the beginning const_iterator over Constructors. */ - inline const_iterator begin() const throw(); + inline std::vector::const_iterator begin() const throw(); /** Get the ending const_iterator over Constructors. */ - inline const_iterator end() const throw(); + inline std::vector::const_iterator end() const throw(); /** Get the ith Constructor. */ const Constructor& operator[](size_t index) const; diff --git a/src/util/datatype.i b/src/util/datatype.i index 802f227eb..f306d7682 100644 --- a/src/util/datatype.i +++ b/src/util/datatype.i @@ -1,7 +1,25 @@ %{ #include "util/datatype.h" +namespace CVC4 { +//typedef CVC4::Datatype::Constructor DatatypeConstructor; +} %} +namespace CVC4 { +%rename(DatatypeConstructor) CVC4::Datatype::Constructor; +//%rename(DatatypeConstructor) CVC4::Constructor; +} + +%extend std::vector< CVC4::Datatype > { + %ignore vector(size_type); +}; +%template(vectorDatatype) std::vector< CVC4::Datatype >; + +%extend std::vector< CVC4::Datatype::Constructor > { + %ignore vector(size_type); +}; +%template(vectorDatatypeConstructor) std::vector< CVC4::Datatype::Constructor >; + %rename(equals) CVC4::Datatype::operator==(const Datatype&) const; %ignore CVC4::Datatype::operator!=(const Datatype&) const; @@ -19,4 +37,5 @@ %ignore CVC4::operator<<(std::ostream&, const Datatype::Constructor&); %ignore CVC4::operator<<(std::ostream&, const Datatype::Constructor::Arg&); + %include "util/datatype.h" diff --git a/src/util/integer.h.in b/src/util/integer.h.in index b62feb512..b2973081d 100644 --- a/src/util/integer.h.in +++ b/src/util/integer.h.in @@ -26,8 +26,14 @@ #ifdef CVC4_CLN_IMP # include "util/integer_cln_imp.h" +# if SWIG + %include "util/integer_cln_imp.h" +# endif /* SWIG */ #endif /* CVC4_CLN_IMP */ #ifdef CVC4_GMP_IMP # include "util/integer_gmp_imp.h" +# if SWIG + %include "util/integer_gmp_imp.h" +# endif /* SWIG */ #endif /* CVC4_GMP_IMP */ diff --git a/src/util/rational.h.in b/src/util/rational.h.in index 13cdb059b..17c1e31fc 100644 --- a/src/util/rational.h.in +++ b/src/util/rational.h.in @@ -26,8 +26,14 @@ #ifdef CVC4_CLN_IMP # include "util/rational_cln_imp.h" +# if SWIG + %include "util/rational_cln_imp.h" +# endif /* SWIG */ #endif /* CVC4_CLN_IMP */ #ifdef CVC4_GMP_IMP # include "util/rational_gmp_imp.h" +# if SWIG + %include "util/rational_gmp_imp.h" +# endif /* SWIG */ #endif /* CVC4_GMP_IMP */ diff --git a/src/util/stats.h b/src/util/stats.h index 42cd73c3d..3a2847512 100644 --- a/src/util/stats.h +++ b/src/util/stats.h @@ -45,7 +45,7 @@ class ExprManager; class CVC4_PUBLIC Stat; -inline std::ostream& operator<<(std::ostream& os, const ::timespec& t); +inline std::ostream& operator<<(std::ostream& os, const timespec& t); /** * The main statistics registry. This registry maintains the list of @@ -546,11 +546,11 @@ public: };/* class ListStat */ /****************************************************************************/ -/* Some utility functions for ::timespec */ +/* Some utility functions for timespec */ /****************************************************************************/ /** Compute the sum of two timespecs. */ -inline ::timespec& operator+=(::timespec& a, const ::timespec& b) { +inline timespec& operator+=(timespec& a, const timespec& b) { // assumes a.tv_nsec and b.tv_nsec are in range const long nsec_per_sec = 1000000000L; // one thousand million Assert(a.tv_nsec >= 0 && a.tv_nsec < nsec_per_sec); @@ -572,7 +572,7 @@ inline ::timespec& operator+=(::timespec& a, const ::timespec& b) { } /** Compute the difference of two timespecs. */ -inline ::timespec& operator-=(::timespec& a, const ::timespec& b) { +inline timespec& operator-=(timespec& a, const timespec& b) { // assumes a.tv_nsec and b.tv_nsec are in range const long nsec_per_sec = 1000000000L; // one thousand million Assert(a.tv_nsec >= 0 && a.tv_nsec < nsec_per_sec); @@ -593,57 +593,57 @@ inline ::timespec& operator-=(::timespec& a, const ::timespec& b) { } /** Add two timespecs. */ -inline ::timespec operator+(const ::timespec& a, const ::timespec& b) { - ::timespec result = a; +inline timespec operator+(const timespec& a, const timespec& b) { + timespec result = a; return result += b; } /** Subtract two timespecs. */ -inline ::timespec operator-(const ::timespec& a, const ::timespec& b) { - ::timespec result = a; +inline timespec operator-(const timespec& a, const timespec& b) { + timespec result = a; return result -= b; } /** Compare two timespecs for equality. */ -inline bool operator==(const ::timespec& a, const ::timespec& b) { +inline bool operator==(const timespec& a, const timespec& b) { // assumes a.tv_nsec and b.tv_nsec are in range return a.tv_sec == b.tv_sec && a.tv_nsec == b.tv_nsec; } /** Compare two timespecs for disequality. */ -inline bool operator!=(const ::timespec& a, const ::timespec& b) { +inline bool operator!=(const timespec& a, const timespec& b) { // assumes a.tv_nsec and b.tv_nsec are in range return !(a == b); } /** Compare two timespecs, returning true iff a < b. */ -inline bool operator<(const ::timespec& a, const ::timespec& b) { +inline bool operator<(const timespec& a, const timespec& b) { // assumes a.tv_nsec and b.tv_nsec are in range return a.tv_sec < b.tv_sec || (a.tv_sec == b.tv_sec && a.tv_nsec < b.tv_nsec); } /** Compare two timespecs, returning true iff a > b. */ -inline bool operator>(const ::timespec& a, const ::timespec& b) { +inline bool operator>(const timespec& a, const timespec& b) { // assumes a.tv_nsec and b.tv_nsec are in range return a.tv_sec > b.tv_sec || (a.tv_sec == b.tv_sec && a.tv_nsec > b.tv_nsec); } /** Compare two timespecs, returning true iff a <= b. */ -inline bool operator<=(const ::timespec& a, const ::timespec& b) { +inline bool operator<=(const timespec& a, const timespec& b) { // assumes a.tv_nsec and b.tv_nsec are in range return !(a > b); } /** Compare two timespecs, returning true iff a >= b. */ -inline bool operator>=(const ::timespec& a, const ::timespec& b) { +inline bool operator>=(const timespec& a, const timespec& b) { // assumes a.tv_nsec and b.tv_nsec are in range return !(a < b); } /** Output a timespec on an output stream. */ -inline std::ostream& operator<<(std::ostream& os, const ::timespec& t) { +inline std::ostream& operator<<(std::ostream& os, const timespec& t) { // assumes t.tv_nsec is in range return os << t.tv_sec << "." << std::setfill('0') << std::setw(8) << std::right << t.tv_nsec; @@ -655,11 +655,11 @@ inline std::ostream& operator<<(std::ostream& os, const ::timespec& t) { * arbitrarily, like a stopwatch; the value of the statistic at the * end is the accumulated time over all (start,stop) pairs. */ -class CVC4_PUBLIC TimerStat : public BackedStat< ::timespec > { +class CVC4_PUBLIC TimerStat : public BackedStat< timespec > { // strange: timespec isn't placed in 'std' namespace ?! /** The last start time of this timer */ - ::timespec d_start; + timespec d_start; /** Whether this timer is currently running */ bool d_running; @@ -693,9 +693,9 @@ public: * timers have a 0.0 value and are not running. */ TimerStat(const std::string& name) : - BackedStat< ::timespec >(name, ::timespec()), + BackedStat< timespec >(name, timespec()), d_running(false) { - /* ::timespec is POD and so may not be initialized to zero; + /* timespec is POD and so may not be initialized to zero; * here, ensure it is */ d_data.tv_sec = d_data.tv_nsec = 0; } -- 2.30.2