diff options
Diffstat (limited to 'src/util')
-rw-r--r-- | src/util/Makefile.am | 3 | ||||
-rw-r--r-- | src/util/array_store_all.i | 7 | ||||
-rw-r--r-- | src/util/bitvector.h | 5 | ||||
-rw-r--r-- | src/util/bitvector.i | 8 | ||||
-rw-r--r-- | src/util/bool.i | 2 | ||||
-rw-r--r-- | src/util/datatype.i | 2 | ||||
-rw-r--r-- | src/util/integer.i | 3 | ||||
-rw-r--r-- | src/util/rational.i | 3 | ||||
-rw-r--r-- | src/util/sexpr.i | 3 | ||||
-rw-r--r-- | src/util/statistics.i | 4 | ||||
-rw-r--r-- | src/util/subrange_bound.i | 11 |
11 files changed, 43 insertions, 8 deletions
diff --git a/src/util/Makefile.am b/src/util/Makefile.am index aa122905b..f3ae43b05 100644 --- a/src/util/Makefile.am +++ b/src/util/Makefile.am @@ -141,8 +141,7 @@ EXTRA_DIST = \ array_store_all.i \ ascription_type.i \ rational.i \ - hash.i \ - util_model.i + hash.i DISTCLEANFILES = \ integer.h.tmp \ diff --git a/src/util/array_store_all.i b/src/util/array_store_all.i index afc14d089..5e8fd7140 100644 --- a/src/util/array_store_all.i +++ b/src/util/array_store_all.i @@ -2,5 +2,12 @@ #include "util/array_store_all.h" %} +%rename(equals) CVC4::ArrayStoreAll::operator==(const ArrayStoreAll&) const; +%ignore CVC4::ArrayStoreAll::operator!=(const ArrayStoreAll&) const; +%rename(less) CVC4::ArrayStoreAll::operator<(const ArrayStoreAll&) const; +%rename(lessEqual) CVC4::ArrayStoreAll::operator<=(const ArrayStoreAll&) const; +%rename(greater) CVC4::ArrayStoreAll::operator>(const ArrayStoreAll&) const; +%rename(greaterEqual) CVC4::ArrayStoreAll::operator>=(const ArrayStoreAll&) const; + %include "expr/type.i" %include "util/array_store_all.h" diff --git a/src/util/bitvector.h b/src/util/bitvector.h index 9438113cf..bb0099157 100644 --- a/src/util/bitvector.h +++ b/src/util/bitvector.h @@ -97,11 +97,6 @@ public: return d_value != y.d_value; } - BitVector equals(const BitVector& y) const { - CheckArgument(d_size == y.d_size, y); - return d_value == y.d_value; - } - BitVector concat (const BitVector& other) const { return BitVector(d_size + other.d_size, (d_value.multiplyByPow2(other.d_size)) + other.d_value); } diff --git a/src/util/bitvector.i b/src/util/bitvector.i index 085a59b2d..220e284b3 100644 --- a/src/util/bitvector.i +++ b/src/util/bitvector.i @@ -11,9 +11,17 @@ %rename(minus) CVC4::BitVector::operator-(const BitVector&) const; %rename(minus) CVC4::BitVector::operator-() const; %rename(times) CVC4::BitVector::operator*(const BitVector&) const; +%rename(bitXor) CVC4::BitVector::operator^(const BitVector&) const; +%rename(bitOr) CVC4::BitVector::operator|(const BitVector&) const; +%rename(bitAnd) CVC4::BitVector::operator&(const BitVector&) const; %rename(complement) CVC4::BitVector::operator~() const; +%rename(less) CVC4::BitVector::operator<(const BitVector&) const; +%rename(lessEqual) CVC4::BitVector::operator<=(const BitVector&) const; +%rename(greater) CVC4::BitVector::operator>(const BitVector&) const; +%rename(greaterEqual) CVC4::BitVector::operator>=(const BitVector&) const; %rename(equals) CVC4::BitVectorExtract::operator==(const BitVectorExtract&) const; +%rename(equals) CVC4::BitVectorBitOf::operator==(const BitVectorBitOf&) const; %rename(toUnsigned) CVC4::BitVectorSize::operator unsigned() const; %rename(toUnsigned) CVC4::BitVectorRepeat::operator unsigned() const; diff --git a/src/util/bool.i b/src/util/bool.i index 39c1c35d4..47a0c4217 100644 --- a/src/util/bool.i +++ b/src/util/bool.i @@ -2,4 +2,6 @@ #include "util/bool.h" %} +%rename(apply) CVC4::BoolHashFunction::operator()(bool) const; + %include "util/bool.h" diff --git a/src/util/datatype.i b/src/util/datatype.i index 068a338b4..c07caa805 100644 --- a/src/util/datatype.i +++ b/src/util/datatype.i @@ -41,6 +41,7 @@ %rename(endConst) CVC4::Datatype::end() const; %rename(getConstructor) CVC4::Datatype::operator[](size_t) const; +%ignore CVC4::Datatype::operator[](std::string) const; %rename(apply) CVC4::DatatypeHashFunction::operator()(const Datatype&) const; %ignore CVC4::DatatypeHashFunction::operator()(const Datatype*) const; @@ -51,6 +52,7 @@ %rename(endConst) CVC4::DatatypeConstructor::end() const; %rename(getArg) CVC4::DatatypeConstructor::operator[](size_t) const; +%rename(getArg) CVC4::DatatypeConstructor::operator[](std::string) const; %ignore CVC4::operator<<(std::ostream&, const Datatype&); %ignore CVC4::operator<<(std::ostream&, const DatatypeConstructor&); diff --git a/src/util/integer.i b/src/util/integer.i index bad6b196f..c8d2f7bdf 100644 --- a/src/util/integer.i +++ b/src/util/integer.i @@ -5,6 +5,7 @@ %ignore CVC4::Integer::Integer(int); %ignore CVC4::Integer::Integer(unsigned int); %ignore CVC4::Integer::Integer(const std::string&); +%ignore CVC4::Integer::Integer(const std::string&, unsigned int); %rename(assign) CVC4::Integer::operator=(const Integer&); %rename(equals) CVC4::Integer::operator==(const Integer&) const; @@ -25,6 +26,8 @@ %rename(greater) CVC4::Integer::operator>(const Integer&) const; %rename(greaterEqual) CVC4::Integer::operator>=(const Integer&) const; +%rename(apply) CVC4::IntegerHashFunction::operator()(const CVC4::Integer&) const; + %ignore CVC4::operator<<(std::ostream&, const Integer&); %include "util/integer.h" diff --git a/src/util/rational.i b/src/util/rational.i index 135302c66..a65c78327 100644 --- a/src/util/rational.i +++ b/src/util/rational.i @@ -7,6 +7,7 @@ %ignore CVC4::Rational::Rational(int, int); %ignore CVC4::Rational::Rational(unsigned int, unsigned int); %ignore CVC4::Rational::Rational(const std::string&); +%ignore CVC4::Rational::Rational(const std::string&, unsigned int); %rename(assign) CVC4::Rational::operator=(const Rational&); %rename(equals) CVC4::Rational::operator==(const Rational&) const; @@ -25,6 +26,8 @@ %rename(greater) CVC4::Rational::operator>(const Rational&) const; %rename(greaterEqual) CVC4::Rational::operator>=(const Rational&) const; +%rename(apply) CVC4::RationalHashFunction::operator()(const CVC4::Rational&) const; + %ignore CVC4::operator<<(std::ostream&, const Rational&); %include "util/rational.h" diff --git a/src/util/sexpr.i b/src/util/sexpr.i index dba8a0f29..5d78142f3 100644 --- a/src/util/sexpr.i +++ b/src/util/sexpr.i @@ -10,4 +10,7 @@ std::string toString() const { return self->getValue(); } };/* CVC4::SExpr */ +%rename(equals) CVC4::SExpr::operator==(const SExpr&) const; +%ignore CVC4::SExpr::operator!=(const SExpr&) const; + %include "util/sexpr.h" diff --git a/src/util/statistics.i b/src/util/statistics.i index 7cc737d6c..a14fc29dd 100644 --- a/src/util/statistics.i +++ b/src/util/statistics.i @@ -2,5 +2,7 @@ #include "util/statistics.h" %} -%include "util/statistics.h" +%rename(assign) CVC4::Statistics::operator=(const StatisticsBase&); +%rename(assign) CVC4::Statistics::operator=(const Statistics& stats); +%include "util/statistics.h" diff --git a/src/util/subrange_bound.i b/src/util/subrange_bound.i index 6b02414ab..c619b5e31 100644 --- a/src/util/subrange_bound.i +++ b/src/util/subrange_bound.i @@ -4,6 +4,17 @@ %rename(equals) CVC4::SubrangeBound::operator==(const SubrangeBound&) const; %ignore CVC4::SubrangeBound::operator!=(const SubrangeBound&) const; +%rename(less) CVC4::SubrangeBound::operator<(const SubrangeBound&) const; +%rename(lessEqual) CVC4::SubrangeBound::operator<=(const SubrangeBound&) const; +%rename(greater) CVC4::SubrangeBound::operator>(const SubrangeBound&) const; +%rename(greaterEqual) CVC4::SubrangeBound::operator>=(const SubrangeBound&) const; + +%rename(equals) CVC4::SubrangeBounds::operator==(const SubrangeBounds&) const; +%ignore CVC4::SubrangeBounds::operator!=(const SubrangeBounds&) const; +%rename(less) CVC4::SubrangeBounds::operator<(const SubrangeBounds&) const; +%rename(lessEqual) CVC4::SubrangeBounds::operator<=(const SubrangeBounds&) const; +%rename(greater) CVC4::SubrangeBounds::operator>(const SubrangeBounds&) const; +%rename(greaterEqual) CVC4::SubrangeBounds::operator>=(const SubrangeBounds&) const; %ignore CVC4::operator<<(std::ostream&, const SubrangeBound&); |