diff options
author | Morgan Deters <mdeters@gmail.com> | 2011-09-21 03:26:13 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2011-09-21 03:26:13 +0000 |
commit | 3b1689612bb2ff984aa90cd84093ffc043d78ba9 (patch) | |
tree | 872cf423273a331e110ff3868cd5281c960dd3b1 /src/expr | |
parent | 69d8f8da6bbb856964d47a583ceb4e50060e9457 (diff) |
considerable bindings interface work, some improvements to build
Diffstat (limited to 'src/expr')
-rw-r--r-- | src/expr/expr_template.h | 2 | ||||
-rw-r--r-- | src/expr/kind.i | 2 | ||||
-rw-r--r-- | src/expr/type.cpp | 60 |
3 files changed, 33 insertions, 31 deletions
diff --git a/src/expr/expr_template.h b/src/expr/expr_template.h index e95e434fe..616a7c8ff 100644 --- a/src/expr/expr_template.h +++ b/src/expr/expr_template.h @@ -506,7 +506,7 @@ protected: friend class ExprManager; friend class NodeManager; friend class TypeCheckingException; - friend std::ostream& operator<<(std::ostream& out, const Expr& e); + friend std::ostream& CVC4::operator<<(std::ostream& out, const Expr& e); template <bool ref_count> friend class NodeTemplate; };/* class Expr */ diff --git a/src/expr/kind.i b/src/expr/kind.i index 1c17f3ff9..95c350cf3 100644 --- a/src/expr/kind.i +++ b/src/expr/kind.i @@ -8,4 +8,6 @@ %ignore CVC4::theory::operator++(TheoryId&); +%rename(Kind) CVC4::kind::Kind_t; + %include "expr/kind.h" diff --git a/src/expr/type.cpp b/src/expr/type.cpp index ff47c6eae..0edc7579b 100644 --- a/src/expr/type.cpp +++ b/src/expr/type.cpp @@ -184,7 +184,7 @@ bool Type::isBoolean() const { /** Cast to a Boolean type */ Type::operator BooleanType() const throw(AssertionException) { NodeManagerScope nms(d_nodeManager); - Assert(isBoolean()); + Assert(isNull() || isBoolean()); return BooleanType(*this); } @@ -197,7 +197,7 @@ bool Type::isInteger() const { /** Cast to a integer type */ Type::operator IntegerType() const throw(AssertionException) { NodeManagerScope nms(d_nodeManager); - Assert(isInteger()); + Assert(isNull() || isInteger()); return IntegerType(*this); } @@ -210,7 +210,7 @@ bool Type::isReal() const { /** Cast to a real type */ Type::operator RealType() const throw(AssertionException) { NodeManagerScope nms(d_nodeManager); - Assert(isReal()); + Assert(isNull() || isReal()); return RealType(*this); } @@ -223,7 +223,7 @@ bool Type::isPseudoboolean() const { /** Cast to a pseudoboolean type */ Type::operator PseudobooleanType() const throw(AssertionException) { NodeManagerScope nms(d_nodeManager); - Assert(isPseudoboolean()); + Assert(isNull() || isPseudoboolean()); return PseudobooleanType(*this); } @@ -236,14 +236,14 @@ bool Type::isBitVector() const { /** Cast to a bit-vector type */ Type::operator BitVectorType() const throw(AssertionException) { NodeManagerScope nms(d_nodeManager); - Assert(isBitVector()); + Assert(isNull() || isBitVector()); return BitVectorType(*this); } /** Cast to a Constructor type */ Type::operator DatatypeType() const throw(AssertionException) { NodeManagerScope nms(d_nodeManager); - Assert(isDatatype()); + Assert(isNull() || isDatatype()); return DatatypeType(*this); } @@ -256,7 +256,7 @@ bool Type::isDatatype() const { /** Cast to a Constructor type */ Type::operator ConstructorType() const throw(AssertionException) { NodeManagerScope nms(d_nodeManager); - Assert(isConstructor()); + Assert(isNull() || isConstructor()); return ConstructorType(*this); } @@ -269,7 +269,7 @@ bool Type::isConstructor() const { /** Cast to a Selector type */ Type::operator SelectorType() const throw(AssertionException) { NodeManagerScope nms(d_nodeManager); - Assert(isSelector()); + Assert(isNull() || isSelector()); return SelectorType(*this); } @@ -282,7 +282,7 @@ bool Type::isSelector() const { /** Cast to a Tester type */ Type::operator TesterType() const throw(AssertionException) { NodeManagerScope nms(d_nodeManager); - Assert(isTester()); + Assert(isNull() || isTester()); return TesterType(*this); } @@ -310,7 +310,7 @@ bool Type::isPredicate() const { /** Cast to a function type */ Type::operator FunctionType() const throw(AssertionException) { NodeManagerScope nms(d_nodeManager); - Assert(isFunction()); + Assert(isNull() || isFunction()); return FunctionType(*this); } @@ -323,7 +323,7 @@ bool Type::isTuple() const { /** Cast to a tuple type */ Type::operator TupleType() const throw(AssertionException) { NodeManagerScope nms(d_nodeManager); - Assert(isTuple()); + Assert(isNull() || isTuple()); return TupleType(*this); } @@ -348,7 +348,7 @@ bool Type::isSort() const { /** Cast to a sort type */ Type::operator SortType() const throw(AssertionException) { NodeManagerScope nms(d_nodeManager); - Assert(isSort()); + Assert(isNull() || isSort()); return SortType(*this); } @@ -361,7 +361,7 @@ bool Type::isSortConstructor() const { /** Cast to a sort type */ Type::operator SortConstructorType() const throw(AssertionException) { NodeManagerScope nms(d_nodeManager); - Assert(isSortConstructor()); + Assert(isNull() || isSortConstructor()); return SortConstructorType(*this); } @@ -374,7 +374,7 @@ bool Type::isKind() const { /** Cast to a kind type */ Type::operator KindType() const throw(AssertionException) { NodeManagerScope nms(d_nodeManager); - Assert(isKind()); + Assert(isNull() || isKind()); return KindType(*this); } @@ -392,7 +392,7 @@ vector<Type> FunctionType::getArgTypes() const { Type FunctionType::getRangeType() const { NodeManagerScope nms(d_nodeManager); - Assert(isFunction()); + Assert(isNull() || isFunction()); return makeType(d_typeNode->getRangeType()); } @@ -447,78 +447,78 @@ SortType SortConstructorType::instantiate(const std::vector<Type>& params) const BooleanType::BooleanType(const Type& t) throw(AssertionException) : Type(t) { - Assert(isBoolean()); + Assert(isNull() || isBoolean()); } IntegerType::IntegerType(const Type& t) throw(AssertionException) : Type(t) { - Assert(isInteger()); + Assert(isNull() || isInteger()); } RealType::RealType(const Type& t) throw(AssertionException) : Type(t) { - Assert(isReal()); + Assert(isNull() || isReal()); } PseudobooleanType::PseudobooleanType(const Type& t) throw(AssertionException) : Type(t) { - Assert(isPseudoboolean()); + Assert(isNull() || isPseudoboolean()); } BitVectorType::BitVectorType(const Type& t) throw(AssertionException) : Type(t) { - Assert(isBitVector()); + Assert(isNull() || isBitVector()); } DatatypeType::DatatypeType(const Type& t) throw(AssertionException) : Type(t) { - Assert(isDatatype()); + Assert(isNull() || isDatatype()); } ConstructorType::ConstructorType(const Type& t) throw(AssertionException) : Type(t) { - Assert(isConstructor()); + Assert(isNull() || isConstructor()); } SelectorType::SelectorType(const Type& t) throw(AssertionException) : Type(t) { - Assert(isSelector()); + Assert(isNull() || isSelector()); } TesterType::TesterType(const Type& t) throw(AssertionException) : Type(t) { - Assert(isTester()); + Assert(isNull() || isTester()); } FunctionType::FunctionType(const Type& t) throw(AssertionException) : Type(t) { - Assert(isFunction()); + Assert(isNull() || isFunction()); } TupleType::TupleType(const Type& t) throw(AssertionException) : Type(t) { - Assert(isTuple()); + Assert(isNull() || isTuple()); } ArrayType::ArrayType(const Type& t) throw(AssertionException) : Type(t) { - Assert(isArray()); + Assert(isNull() || isArray()); } KindType::KindType(const Type& t) throw(AssertionException) : Type(t) { - Assert(isKind()); + Assert(isNull() || isKind()); } SortType::SortType(const Type& t) throw(AssertionException) : Type(t) { - Assert(isSort()); + Assert(isNull() || isSort()); } SortConstructorType::SortConstructorType(const Type& t) throw(AssertionException) : Type(t) { - Assert(isSortConstructor()); + Assert(isNull() || isSortConstructor()); } unsigned BitVectorType::getSize() const { |