diff options
Diffstat (limited to 'src/util')
-rw-r--r-- | src/util/Assert.i | 5 | ||||
-rw-r--r-- | src/util/Makefile.am | 22 | ||||
-rw-r--r-- | src/util/array.i | 5 | ||||
-rw-r--r-- | src/util/ascription_type.i | 11 | ||||
-rw-r--r-- | src/util/bitvector.i | 28 | ||||
-rw-r--r-- | src/util/bool.i | 5 | ||||
-rw-r--r-- | src/util/cardinality.h | 5 | ||||
-rw-r--r-- | src/util/cardinality.i | 23 | ||||
-rw-r--r-- | src/util/configuration.i | 5 | ||||
-rw-r--r-- | src/util/datatype.i | 22 | ||||
-rw-r--r-- | src/util/exception.h | 9 | ||||
-rw-r--r-- | src/util/exception.i | 7 | ||||
-rw-r--r-- | src/util/hash.h | 3 | ||||
-rw-r--r-- | src/util/hash.i | 5 | ||||
-rw-r--r-- | src/util/integer.h.in | 6 | ||||
-rw-r--r-- | src/util/integer.i | 29 | ||||
-rw-r--r-- | src/util/language.i | 10 | ||||
-rw-r--r-- | src/util/matcher.h | 2 | ||||
-rw-r--r-- | src/util/options.i | 9 | ||||
-rw-r--r-- | src/util/output.h | 4 | ||||
-rw-r--r-- | src/util/output.i | 10 | ||||
-rw-r--r-- | src/util/pseudoboolean.i | 11 | ||||
-rw-r--r-- | src/util/rational.h.in | 6 | ||||
-rw-r--r-- | src/util/rational.i | 29 | ||||
-rw-r--r-- | src/util/rational_cln_imp.h | 5 | ||||
-rw-r--r-- | src/util/rational_gmp_imp.h | 5 | ||||
-rw-r--r-- | src/util/result.i | 14 | ||||
-rw-r--r-- | src/util/sexpr.i | 7 | ||||
-rw-r--r-- | src/util/stats.i | 21 | ||||
-rw-r--r-- | src/util/subrange_bound.i | 10 |
30 files changed, 312 insertions, 21 deletions
diff --git a/src/util/Assert.i b/src/util/Assert.i new file mode 100644 index 000000000..11881982b --- /dev/null +++ b/src/util/Assert.i @@ -0,0 +1,5 @@ +%{ +#include "util/Assert.h" +%} + +%include "util/Assert.h" diff --git a/src/util/Makefile.am b/src/util/Makefile.am index 7f5fb459e..b8bdfabeb 100644 --- a/src/util/Makefile.am +++ b/src/util/Makefile.am @@ -139,4 +139,24 @@ EXTRA_DIST = \ rational_gmp_imp.cpp \ rational.h.in \ integer.h.in \ - tls.h.in + tls.h.in \ + integer.i \ + stats.i \ + bool.i \ + sexpr.i \ + datatype.i \ + output.i \ + cardinality.i \ + result.i \ + configuration.i \ + Assert.i \ + bitvector.i \ + subrange_bound.i \ + exception.i \ + language.i \ + array.i \ + options.i \ + ascription_type.i \ + rational.i \ + pseudoboolean.i \ + hash.i diff --git a/src/util/array.i b/src/util/array.i new file mode 100644 index 000000000..593ce9490 --- /dev/null +++ b/src/util/array.i @@ -0,0 +1,5 @@ +%{ +#include "util/array.h" +%} + +%include "util/array.h" diff --git a/src/util/ascription_type.i b/src/util/ascription_type.i new file mode 100644 index 000000000..b0b57d5f9 --- /dev/null +++ b/src/util/ascription_type.i @@ -0,0 +1,11 @@ +%{ +#include "util/ascription_type.h" +%} + + +%rename(equals) CVC4::AscriptionType::operator==(const AscriptionType&) const; +%ignore CVC4::AscriptionType::operator!=(const AscriptionType&) const; + +%ignore CVC4::operator<<(std::ostream&, AscriptionType); + +%include "util/ascription_type.h" diff --git a/src/util/bitvector.i b/src/util/bitvector.i new file mode 100644 index 000000000..085a59b2d --- /dev/null +++ b/src/util/bitvector.i @@ -0,0 +1,28 @@ +%{ +#include "util/bitvector.h" +%} + +%ignore CVC4::BitVector::BitVector(unsigned, unsigned); + +%rename(assign) CVC4::BitVector::operator=(const BitVector&); +%rename(equals) CVC4::BitVector::operator==(const BitVector&) const; +%ignore CVC4::BitVector::operator!=(const BitVector&) const; +%rename(plus) CVC4::BitVector::operator+(const BitVector&) const; +%rename(minus) CVC4::BitVector::operator-(const BitVector&) const; +%rename(minus) CVC4::BitVector::operator-() const; +%rename(times) CVC4::BitVector::operator*(const BitVector&) const; +%rename(complement) CVC4::BitVector::operator~() const; + +%rename(equals) CVC4::BitVectorExtract::operator==(const BitVectorExtract&) const; + +%rename(toUnsigned) CVC4::BitVectorSize::operator unsigned() const; +%rename(toUnsigned) CVC4::BitVectorRepeat::operator unsigned() const; +%rename(toUnsigned) CVC4::BitVectorZeroExtend::operator unsigned() const; +%rename(toUnsigned) CVC4::BitVectorSignExtend::operator unsigned() const; +%rename(toUnsigned) CVC4::BitVectorRotateLeft::operator unsigned() const; +%rename(toUnsigned) CVC4::BitVectorRotateRight::operator unsigned() const; + +%ignore CVC4::operator<<(std::ostream&, const BitVector&); +%ignore CVC4::operator<<(std::ostream&, const BitVectorExtract&); + +%include "util/bitvector.h" diff --git a/src/util/bool.i b/src/util/bool.i new file mode 100644 index 000000000..39c1c35d4 --- /dev/null +++ b/src/util/bool.i @@ -0,0 +1,5 @@ +%{ +#include "util/bool.h" +%} + +%include "util/bool.h" diff --git a/src/util/cardinality.h b/src/util/cardinality.h index 6985ae38e..e08f09bb6 100644 --- a/src/util/cardinality.h +++ b/src/util/cardinality.h @@ -22,11 +22,6 @@ #ifndef __CVC4__CARDINALITY_H #define __CVC4__CARDINALITY_H -#if SWIG -%include "util/integer.h" -%include "util/Assert.h" -#endif /* SWIG */ - #include <iostream> #include <utility> diff --git a/src/util/cardinality.i b/src/util/cardinality.i new file mode 100644 index 000000000..760f746c0 --- /dev/null +++ b/src/util/cardinality.i @@ -0,0 +1,23 @@ +%{ +#include "util/cardinality.h" +%} + +%feature("valuewrapper") CVC4::Cardinality::Beth; + +%rename(plusAssign) CVC4::Cardinality::operator+=(const Cardinality&); +%rename(timesAssign) CVC4::Cardinality::operator*=(const Cardinality&); +%rename(powerAssign) CVC4::Cardinality::operator^=(const Cardinality&); +%rename(plus) CVC4::Cardinality::operator+(const Cardinality&) const; +%rename(times) CVC4::Cardinality::operator*(const Cardinality&) const; +%rename(power) CVC4::Cardinality::operator^(const Cardinality&) const; +%rename(equals) CVC4::Cardinality::operator==(const Cardinality&) const; +%ignore CVC4::Cardinality::operator!=(const Cardinality&) const; +%rename(less) CVC4::Cardinality::operator<(const Cardinality&) const; +%rename(lessEqual) CVC4::Cardinality::operator<=(const Cardinality&) const; +%rename(greater) CVC4::Cardinality::operator>(const Cardinality&) const; +%rename(greaterEqual) CVC4::Cardinality::operator>=(const Cardinality&) const; + +%ignore CVC4::operator<<(std::ostream&, const Cardinality&); +%ignore CVC4::operator<<(std::ostream&, Cardinality::Beth); + +%include "util/cardinality.h" diff --git a/src/util/configuration.i b/src/util/configuration.i new file mode 100644 index 000000000..17c1b974b --- /dev/null +++ b/src/util/configuration.i @@ -0,0 +1,5 @@ +%{ +#include "util/configuration.h" +%} + +%include "util/configuration.h" diff --git a/src/util/datatype.i b/src/util/datatype.i new file mode 100644 index 000000000..802f227eb --- /dev/null +++ b/src/util/datatype.i @@ -0,0 +1,22 @@ +%{ +#include "util/datatype.h" +%} + +%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; + +%rename(getConstructor) CVC4::Datatype::operator[](size_t) const; + +%rename(apply) CVC4::DatatypeHashFunction::operator()(const Datatype&) const; +%ignore CVC4::DatatypeHashFunction::operator()(const Datatype*) const; +%rename(apply) CVC4::DatatypeHashFunction::operator()(const Datatype::Constructor&) const; +%ignore CVC4::DatatypeHashFunction::operator()(const Datatype::Constructor*) const; + +%ignore CVC4::operator<<(std::ostream&, const Datatype&); +%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/exception.h b/src/util/exception.h index 1b1eb224e..43a0354ca 100644 --- a/src/util/exception.h +++ b/src/util/exception.h @@ -30,16 +30,20 @@ namespace CVC4 { class CVC4_PUBLIC Exception { protected: std::string d_msg; + public: // Constructors Exception() : d_msg("Unknown exception") {} Exception(const std::string& msg) : d_msg(msg) {} Exception(const char* msg) : d_msg(msg) {} + // Destructor virtual ~Exception() throw() {} + // NON-VIRTUAL METHOD for setting and printing the error message void setMessage(const std::string& msg) { d_msg = msg; } std::string getMessage() const { return d_msg; } + /** * Get this exception as a string. Note that * cout << ex.toString(); @@ -57,16 +61,17 @@ public: toStream(ss); return ss.str(); } + /** * Printing: feel free to redefine toStream(). When overridden in * a derived class, it's recommended that this method print the * type of exception before the actual message. */ virtual void toStream(std::ostream& os) const { os << d_msg; } - // No need to overload operator<< for the inherited classes - friend std::ostream& operator<<(std::ostream& os, const Exception& e); + };/* class Exception */ +inline std::ostream& operator<<(std::ostream& os, const Exception& e) CVC4_PUBLIC; inline std::ostream& operator<<(std::ostream& os, const Exception& e) { e.toStream(os); return os; diff --git a/src/util/exception.i b/src/util/exception.i new file mode 100644 index 000000000..d3ff896d2 --- /dev/null +++ b/src/util/exception.i @@ -0,0 +1,7 @@ +%{ +#include "util/exception.h" +%} + +%ignore CVC4::operator<<(std::ostream&, const Exception&); + +%include "util/exception.h" diff --git a/src/util/hash.h b/src/util/hash.h index 10211970f..bd3fee597 100644 --- a/src/util/hash.h +++ b/src/util/hash.h @@ -22,6 +22,9 @@ #ifndef __CVC4__HASH_H #define __CVC4__HASH_H +// in case it's not been declared as a namespace yet +namespace __gnu_cxx {} + #include <ext/hash_map> namespace std { using namespace __gnu_cxx; } diff --git a/src/util/hash.i b/src/util/hash.i new file mode 100644 index 000000000..f2f1e6652 --- /dev/null +++ b/src/util/hash.i @@ -0,0 +1,5 @@ +%{ +#include "util/hash.h" +%} + +%include "util/hash.h" diff --git a/src/util/integer.h.in b/src/util/integer.h.in index b2973081d..b62feb512 100644 --- a/src/util/integer.h.in +++ b/src/util/integer.h.in @@ -26,14 +26,8 @@ #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/integer.i b/src/util/integer.i new file mode 100644 index 000000000..4aaa532a7 --- /dev/null +++ b/src/util/integer.i @@ -0,0 +1,29 @@ +%{ +#include "util/integer.h" +%} + +%ignore CVC4::Integer::Integer(int); +%ignore CVC4::Integer::Integer(unsigned int); + +%rename(assign) CVC4::Integer::operator=(const Integer&); +%rename(equals) CVC4::Integer::operator==(const Integer&) const; +%ignore CVC4::Integer::operator!=(const Integer&) const; +%rename(plus) CVC4::Integer::operator+(const Integer&) const; +%rename(minus) CVC4::Integer::operator-() const; +%rename(minus) CVC4::Integer::operator-(const Integer&) const; +%rename(times) CVC4::Integer::operator*(const Integer&) const; +%rename(dividedBy) CVC4::Integer::operator/(const Integer&) const; +%rename(modulo) CVC4::Integer::operator%(const Integer&) const; +%rename(plusAssign) CVC4::Integer::operator+=(const Integer&); +%rename(minusAssign) CVC4::Integer::operator-=(const Integer&); +%rename(timesAssign) CVC4::Integer::operator*=(const Integer&); +%rename(dividedByAssign) CVC4::Integer::operator/=(const Integer&); +%rename(moduloAssign) CVC4::Integer::operator%=(const Integer&); +%rename(less) CVC4::Integer::operator<(const Integer&) const; +%rename(lessEqual) CVC4::Integer::operator<=(const Integer&) const; +%rename(greater) CVC4::Integer::operator>(const Integer&) const; +%rename(greaterEqual) CVC4::Integer::operator>=(const Integer&) const; + +%ignore CVC4::operator<<(std::ostream&, const Integer&); + +%include "util/integer.h" diff --git a/src/util/language.i b/src/util/language.i new file mode 100644 index 000000000..cd261a73c --- /dev/null +++ b/src/util/language.i @@ -0,0 +1,10 @@ +%{ +#include "util/language.h" +%} + +%import "util/language.h" + +%ignore CVC4::operator<<(std::ostream&, CVC4::language::input::Language); +%ignore CVC4::operator<<(std::ostream&, CVC4::language::output::Language); + +%include "util/language.h" diff --git a/src/util/matcher.h b/src/util/matcher.h index 6daceb8fd..871fe528f 100644 --- a/src/util/matcher.h +++ b/src/util/matcher.h @@ -16,7 +16,7 @@ ** A class representing a type matcher. **/ -#include "cvc4_public.h" +#include "cvc4_private.h" #ifndef __CVC4__MATCHER_H #define __CVC4__MATCHER_H diff --git a/src/util/options.i b/src/util/options.i new file mode 100644 index 000000000..ad4815a33 --- /dev/null +++ b/src/util/options.i @@ -0,0 +1,9 @@ +%{ +#include "util/options.h" +%} + +%ignore CVC4::operator<<(std::ostream&, Options::SimplificationMode); +%ignore CVC4::operator<<(std::ostream&, Options::ArithPivotRule); + +%import "util/exception.h" +%include "util/options.h" diff --git a/src/util/output.h b/src/util/output.h index e096ff028..da1efe68a 100644 --- a/src/util/output.h +++ b/src/util/output.h @@ -23,6 +23,7 @@ #include <ios> #include <iostream> +#include <streambuf> #include <string> #include <cstdio> #include <cstdarg> @@ -71,6 +72,9 @@ class CVC4_PUBLIC CVC4ostream { /** The endl manipulator (why do we need to keep this?) */ std::ostream& (*const d_endl)(std::ostream&); + // do not allow use + CVC4ostream& operator=(const CVC4ostream&); + public: CVC4ostream() : d_os(NULL), diff --git a/src/util/output.i b/src/util/output.i new file mode 100644 index 000000000..c2729203a --- /dev/null +++ b/src/util/output.i @@ -0,0 +1,10 @@ +%{ +#include "util/output.h" +%} + +%import "util/output.h" + +%feature("valuewrapper") CVC4::null_streambuf; +%feature("valuewrapper") std::ostream; + +%include "util/output.h" diff --git a/src/util/pseudoboolean.i b/src/util/pseudoboolean.i new file mode 100644 index 000000000..2505a7c1e --- /dev/null +++ b/src/util/pseudoboolean.i @@ -0,0 +1,11 @@ +%{ +#include "util/pseudoboolean.h" +%} + +%rename(toBool) CVC4::Pseudoboolean::operator bool() const; +%rename(toInt) CVC4::Pseudoboolean::operator int() const; +%rename(toInteger) CVC4::Pseudoboolean::operator Integer() const; + +%ignore CVC4::operator<<(std::ostream&, CVC4::Pseudoboolean); + +%include "util/pseudoboolean.h" diff --git a/src/util/rational.h.in b/src/util/rational.h.in index 17c1e31fc..13cdb059b 100644 --- a/src/util/rational.h.in +++ b/src/util/rational.h.in @@ -26,14 +26,8 @@ #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/rational.i b/src/util/rational.i new file mode 100644 index 000000000..512d3ea50 --- /dev/null +++ b/src/util/rational.i @@ -0,0 +1,29 @@ +%{ +#include "util/rational.h" +%} + +%ignore CVC4::Rational::Rational(int); +%ignore CVC4::Rational::Rational(unsigned int); +%ignore CVC4::Rational::Rational(int, int); +%ignore CVC4::Rational::Rational(unsigned int, unsigned int); + +%rename(assign) CVC4::Rational::operator=(const Rational&); +%rename(equals) CVC4::Rational::operator==(const Rational&) const; +%ignore CVC4::Rational::operator!=(const Rational&) const; +%rename(plus) CVC4::Rational::operator+(const Rational&) const; +%rename(minus) CVC4::Rational::operator-() const; +%rename(minus) CVC4::Rational::operator-(const Rational&) const; +%rename(times) CVC4::Rational::operator*(const Rational&) const; +%rename(dividedBy) CVC4::Rational::operator/(const Rational&) const; +%rename(plusAssign) CVC4::Rational::operator+=(const Rational&); +%rename(minusAssign) CVC4::Rational::operator-=(const Rational&); +%rename(timesAssign) CVC4::Rational::operator*=(const Rational&); +%rename(dividedByAssign) CVC4::Rational::operator/=(const Rational&); +%rename(less) CVC4::Rational::operator<(const Rational&) const; +%rename(lessEqual) CVC4::Rational::operator<=(const Rational&) const; +%rename(greater) CVC4::Rational::operator>(const Rational&) const; +%rename(greaterEqual) CVC4::Rational::operator>=(const Rational&) const; + +%ignore CVC4::operator<<(std::ostream&, const Rational&); + +%include "util/rational.h" diff --git a/src/util/rational_cln_imp.h b/src/util/rational_cln_imp.h index a883500f9..2f2c14ed8 100644 --- a/src/util/rational_cln_imp.h +++ b/src/util/rational_cln_imp.h @@ -258,6 +258,11 @@ public: return (*this); } + Rational& operator/=(const Rational& y){ + d_value /= y.d_value; + return (*this); + } + /** Returns a string representing the rational in the given base. */ std::string toString(int base = 10) const { std::stringstream ss; diff --git a/src/util/rational_gmp_imp.h b/src/util/rational_gmp_imp.h index b97965169..37c3c8364 100644 --- a/src/util/rational_gmp_imp.h +++ b/src/util/rational_gmp_imp.h @@ -239,6 +239,11 @@ public: return (*this); } + Rational& operator/=(const Rational& y){ + d_value /= y.d_value; + return (*this); + } + /** Returns a string representing the rational in the given base. */ std::string toString(int base = 10) const { return d_value.get_str(base); diff --git a/src/util/result.i b/src/util/result.i new file mode 100644 index 000000000..c0d86b30a --- /dev/null +++ b/src/util/result.i @@ -0,0 +1,14 @@ +%{ +#include "util/result.h" +%} + +%ignore CVC4::operator<<(std::ostream&, const Result& r); + +%rename(equals) CVC4::Result::operator==(const Result& r) const; +%ignore CVC4::Result::operator!=(const Result& r) const; + +%ignore CVC4::operator<<(std::ostream&, enum Result::Sat); +%ignore CVC4::operator<<(std::ostream&, enum Result::Validity); +%ignore CVC4::operator<<(std::ostream&, enum Result::UnknownExplanation); + +%include "util/result.h" diff --git a/src/util/sexpr.i b/src/util/sexpr.i new file mode 100644 index 000000000..c925f9f95 --- /dev/null +++ b/src/util/sexpr.i @@ -0,0 +1,7 @@ +%{ +#include "util/sexpr.h" +%} + +%ignore CVC4::operator<<(std::ostream&, const SExpr&); + +%include "util/sexpr.h" diff --git a/src/util/stats.i b/src/util/stats.i new file mode 100644 index 000000000..48828cb7e --- /dev/null +++ b/src/util/stats.i @@ -0,0 +1,21 @@ +%{ +#include "util/stats.h" +%} + +%ignore CVC4::operator<<(std::ostream&, const ::timespec&); + +%rename(increment) CVC4::IntStat::operator++(); +%rename(plusAssign) CVC4::IntStat::operator+=(int64_t); + +%rename(plusAssign) CVC4::operator+=(::timespec&, const ::timespec&); +%rename(minusAssign) CVC4::operator-=(::timespec&, const ::timespec&); +%rename(plus) CVC4::operator+(const ::timespec&, const ::timespec&); +%rename(minus) CVC4::operator-(const ::timespec&, const ::timespec&); +%rename(equals) CVC4::operator==(const ::timespec&, const ::timespec&); +%ignore CVC4::operator!=(const ::timespec&, const ::timespec&); +%rename(less) CVC4::operator<(const ::timespec&, const ::timespec&); +%rename(lessEqual) CVC4::operator<=(const ::timespec&, const ::timespec&); +%rename(greater) CVC4::operator>(const ::timespec&, const ::timespec&); +%rename(greaterEqual) CVC4::operator>=(const ::timespec&, const ::timespec&); + +%include "util/stats.h" diff --git a/src/util/subrange_bound.i b/src/util/subrange_bound.i new file mode 100644 index 000000000..6b02414ab --- /dev/null +++ b/src/util/subrange_bound.i @@ -0,0 +1,10 @@ +%{ +#include "util/subrange_bound.h" +%} + +%rename(equals) CVC4::SubrangeBound::operator==(const SubrangeBound&) const; +%ignore CVC4::SubrangeBound::operator!=(const SubrangeBound&) const; + +%ignore CVC4::operator<<(std::ostream&, const SubrangeBound&); + +%include "util/subrange_bound.h" |