diff options
author | Morgan Deters <mdeters@gmail.com> | 2011-09-23 23:37:42 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2011-09-23 23:37:42 +0000 |
commit | a63064385c56600143ac470108fe8e640a4ca3ee (patch) | |
tree | 2b1d13fbd4c05669f873964a5fee0f87cbf1a330 /src/util | |
parent | 5f742fbd0ddb1b7e89bd9f7ce8fd38bed2ebc3db (diff) |
interface cleanup, java bindings work
Diffstat (limited to 'src/util')
-rw-r--r-- | src/util/ascription_type.i | 1 | ||||
-rw-r--r-- | src/util/datatype.h | 12 | ||||
-rw-r--r-- | src/util/datatype.i | 19 | ||||
-rw-r--r-- | src/util/integer.h.in | 6 | ||||
-rw-r--r-- | src/util/rational.h.in | 6 | ||||
-rw-r--r-- | src/util/stats.h | 38 |
6 files changed, 56 insertions, 26 deletions
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<Constructor>::iterator iterator; + typedef typename std::vector<Constructor>::iterator iterator; /** The (const) type for iterators over constructors. */ - typedef std::vector<Constructor>::const_iterator const_iterator; + typedef typename std::vector<Constructor>::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<Constructor>::iterator begin() throw(); /** Get the ending iterator over Constructors. */ - inline iterator end() throw(); + inline std::vector<Constructor>::iterator end() throw(); /** Get the beginning const_iterator over Constructors. */ - inline const_iterator begin() const throw(); + inline std::vector<Constructor>::const_iterator begin() const throw(); /** Get the ending const_iterator over Constructors. */ - inline const_iterator end() const throw(); + inline std::vector<Constructor>::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; } |