class RationalEnumerator : public TypeEnumeratorBase<RationalEnumerator> {
Rational d_rat;
-public:
-
- RationalEnumerator(TypeNode type, TypeEnumeratorProperties * tep = NULL) throw(AssertionException) :
- TypeEnumeratorBase<RationalEnumerator>(type),
- d_rat(0) {
+ public:
+ RationalEnumerator(TypeNode type, TypeEnumeratorProperties* tep = nullptr)
+ : TypeEnumeratorBase<RationalEnumerator>(type), d_rat(0)
+ {
Assert(type.getKind() == kind::TYPE_CONSTANT &&
type.getConst<TypeConstant>() == REAL_TYPE);
}
- Node operator*() throw() {
- return NodeManager::currentNM()->mkConst(d_rat);
- }
-
- RationalEnumerator& operator++() throw() {
+ Node operator*() override { return NodeManager::currentNM()->mkConst(d_rat); }
+ RationalEnumerator& operator++() override
+ {
// sequence is 0, then diagonal with negatives interleaved
// ( 0, 1/1, -1/1, 2/1, -2/1, 1/2, -1/2, 3/1, -3/1, 1/3, -1/3,
// 4/1, -4/1, 3/2, -3/2, 2/3, -2/3, 1/4, -1/4, ...)
return *this;
}
- bool isFinished() throw() {
- return false;
- }
-
+ bool isFinished() override { return false; }
};/* class RationalEnumerator */
class IntegerEnumerator : public TypeEnumeratorBase<IntegerEnumerator> {
Integer d_int;
-public:
-
- IntegerEnumerator(TypeNode type, TypeEnumeratorProperties * tep = NULL) throw(AssertionException) :
- TypeEnumeratorBase<IntegerEnumerator>(type),
- d_int(0) {
+ public:
+ IntegerEnumerator(TypeNode type, TypeEnumeratorProperties* tep = nullptr)
+ : TypeEnumeratorBase<IntegerEnumerator>(type), d_int(0)
+ {
Assert(type.getKind() == kind::TYPE_CONSTANT &&
type.getConst<TypeConstant>() == INTEGER_TYPE);
}
- Node operator*() throw() {
+ Node operator*() override
+ {
return NodeManager::currentNM()->mkConst(Rational(d_int));
}
- IntegerEnumerator& operator++() throw() {
+ IntegerEnumerator& operator++() override
+ {
// sequence is 0, 1, -1, 2, -2, 3, -3, ...
if(d_int <= 0) {
d_int = -d_int + 1;
return *this;
}
- bool isFinished() throw() {
- return false;
- }
-
+ bool isFinished() override { return false; }
};/* class IntegerEnumerator */
}/* CVC4::theory::arith namespace */
bool d_finished;
Node d_arrayConst;
-public:
-
- ArrayEnumerator(TypeNode type, TypeEnumeratorProperties * tep = NULL) :
- TypeEnumeratorBase<ArrayEnumerator>(type),
- d_tep(tep),
- d_index(type.getArrayIndexType(), tep),
- d_constituentType(type.getArrayConstituentType()),
- d_nm(NodeManager::currentNM()),
- d_indexVec(),
- d_constituentVec(),
- d_finished(false),
- d_arrayConst()
+ public:
+ ArrayEnumerator(TypeNode type, TypeEnumeratorProperties* tep = nullptr)
+ : TypeEnumeratorBase<ArrayEnumerator>(type),
+ d_tep(tep),
+ d_index(type.getArrayIndexType(), tep),
+ d_constituentType(type.getArrayConstituentType()),
+ d_nm(NodeManager::currentNM()),
+ d_indexVec(),
+ d_constituentVec(),
+ d_finished(false),
+ d_arrayConst()
{
d_indexVec.push_back(*d_index);
d_constituentVec.push_back(new TypeEnumerator(d_constituentType, d_tep));
// An array enumerator could be large, and generally you don't want to
// go around copying these things; but a copy ctor is presently required
// by the TypeEnumerator framework.
- ArrayEnumerator(const ArrayEnumerator& ae) throw() :
- TypeEnumeratorBase<ArrayEnumerator>(ae.d_nm->mkArrayType(ae.d_index.getType(), ae.d_constituentType)),
- d_tep(ae.d_tep),
- d_index(ae.d_index),
- d_constituentType(ae.d_constituentType),
- d_nm(ae.d_nm),
- d_indexVec(ae.d_indexVec),
- d_constituentVec(),// copied below
- d_finished(ae.d_finished),
- d_arrayConst(ae.d_arrayConst)
+ ArrayEnumerator(const ArrayEnumerator& ae)
+ : TypeEnumeratorBase<ArrayEnumerator>(
+ ae.d_nm->mkArrayType(ae.d_index.getType(), ae.d_constituentType)),
+ d_tep(ae.d_tep),
+ d_index(ae.d_index),
+ d_constituentType(ae.d_constituentType),
+ d_nm(ae.d_nm),
+ d_indexVec(ae.d_indexVec),
+ d_constituentVec(), // copied below
+ d_finished(ae.d_finished),
+ d_arrayConst(ae.d_arrayConst)
{
for(std::vector<TypeEnumerator*>::const_iterator i =
ae.d_constituentVec.begin(), i_end = ae.d_constituentVec.end();
}
}
- Node operator*() {
+ Node operator*() override
+ {
if (d_finished) {
throw NoMoreValuesException(getType());
}
return n;
}
- ArrayEnumerator& operator++() {
+ ArrayEnumerator& operator++() override
+ {
Trace("array-type-enum") << "operator++ called, **this = " << **this << std::endl;
if (d_finished) {
return *this;
}
- bool isFinished() throw() {
+ bool isFinished() override
+ {
Trace("array-type-enum") << "isFinished returning: " << d_finished << std::endl;
return d_finished;
}
class BooleanEnumerator : public TypeEnumeratorBase<BooleanEnumerator> {
enum { FALSE, TRUE, DONE } d_value;
-public:
-
- BooleanEnumerator(TypeNode type, TypeEnumeratorProperties * tep = NULL) :
- TypeEnumeratorBase<BooleanEnumerator>(type),
- d_value(FALSE) {
+ public:
+ BooleanEnumerator(TypeNode type, TypeEnumeratorProperties* tep = nullptr)
+ : TypeEnumeratorBase<BooleanEnumerator>(type), d_value(FALSE)
+ {
Assert(type.getKind() == kind::TYPE_CONSTANT &&
type.getConst<TypeConstant>() == BOOLEAN_TYPE);
}
}
}
- BooleanEnumerator& operator++() throw() {
+ BooleanEnumerator& operator++() override
+ {
// sequence is FALSE, TRUE
if(d_value == FALSE) {
d_value = TRUE;
return *this;
}
- bool isFinished() throw() {
- return d_value == DONE;
- }
-
+ bool isFinished() override { return d_value == DONE; }
};/* class BooleanEnumerator */
}/* CVC4::theory::booleans namespace */
return TheoryBuiltinRewriter::getLambdaForArrayRepresentation(a, d_bvl);
}
-FunctionEnumerator& FunctionEnumerator::operator++() throw()
+FunctionEnumerator& FunctionEnumerator::operator++()
{
++d_arrayEnum;
return *this;
} /* CVC4::theory::builtin namespace */
} /* CVC4::theory namespace */
-} /* CVC4 namespace */
\ No newline at end of file
+} /* CVC4 namespace */
Integer d_count;
bool d_has_fixed_bound;
Integer d_fixed_bound;
-public:
- UninterpretedSortEnumerator(TypeNode type, TypeEnumeratorProperties * tep = NULL) :
- TypeEnumeratorBase<UninterpretedSortEnumerator>(type),
- d_count(0) {
+ public:
+ UninterpretedSortEnumerator(TypeNode type,
+ TypeEnumeratorProperties* tep = nullptr)
+ : TypeEnumeratorBase<UninterpretedSortEnumerator>(type), d_count(0)
+ {
Assert(type.getKind() == kind::SORT_TYPE);
d_has_fixed_bound = false;
Trace("uf-type-enum") << "UF enum " << type << ", tep = " << tep << std::endl;
}
}
- Node operator*() {
+ Node operator*() override
+ {
if(isFinished()) {
throw NoMoreValuesException(getType());
}
return NodeManager::currentNM()->mkConst(UninterpretedConstant(getType().toType(), d_count));
}
- UninterpretedSortEnumerator& operator++() throw() {
+ UninterpretedSortEnumerator& operator++() override
+ {
d_count += 1;
return *this;
}
- bool isFinished() throw() {
+ bool isFinished() override
+ {
if( d_has_fixed_bound ){
return d_count>=d_fixed_bound;
}else{
/** Get the current term of the enumerator. */
Node operator*() override;
/** Increment the enumerator. */
- FunctionEnumerator& operator++() throw() override;
+ FunctionEnumerator& operator++() override;
/** is the enumerator finished? */
- bool isFinished() throw() override { return d_arrayEnum.isFinished(); }
+ bool isFinished() override { return d_arrayEnum.isFinished(); }
private:
/** Enumerates arrays, which we convert to functions. */
TypeEnumerator d_arrayEnum;
Node getCurrentTerm( unsigned index );
void init();
-public:
- DatatypesEnumerator(TypeNode type, TypeEnumeratorProperties * tep = NULL) :
- TypeEnumeratorBase<DatatypesEnumerator>(type),
- d_tep(tep),
- d_datatype(DatatypeType(type.toType()).getDatatype()),
- d_type(type) {
+ public:
+ DatatypesEnumerator(TypeNode type, TypeEnumeratorProperties* tep = nullptr)
+ : TypeEnumeratorBase<DatatypesEnumerator>(type),
+ d_tep(tep),
+ d_datatype(DatatypeType(type.toType()).getDatatype()),
+ d_type(type)
+ {
d_child_enum = false;
init();
}
- DatatypesEnumerator(TypeNode type, bool childEnum, TypeEnumeratorProperties * tep = NULL) :
- TypeEnumeratorBase<DatatypesEnumerator>(type),
- d_tep(tep),
- d_datatype(DatatypeType(type.toType()).getDatatype()),
- d_type(type) {
+ DatatypesEnumerator(TypeNode type,
+ bool childEnum,
+ TypeEnumeratorProperties* tep = nullptr)
+ : TypeEnumeratorBase<DatatypesEnumerator>(type),
+ d_tep(tep),
+ d_datatype(DatatypeType(type.toType()).getDatatype()),
+ d_type(type)
+ {
d_child_enum = childEnum;
init();
}
d_child_enum = de.d_child_enum;
}
- virtual ~DatatypesEnumerator() throw() {
- }
-
- Node operator*() {
+ Node operator*() override
+ {
Debug("dt-enum-debug") << ": get term " << this << std::endl;
if(d_ctor < d_has_debruijn + d_datatype.getNumConstructors()) {
return getCurrentTerm( d_ctor );
}
}
- DatatypesEnumerator& operator++() {
+ DatatypesEnumerator& operator++() override
+ {
Debug("dt-enum-debug") << ": increment " << this << std::endl;
unsigned prevSize = d_size_limit;
while(d_ctor < d_has_debruijn+d_datatype.getNumConstructors()) {
return *this;
}
- bool isFinished() throw() {
+ bool isFinished() override
+ {
return d_ctor >= d_has_debruijn+d_datatype.getNumConstructors();
}
bool d_finished;
Node d_setConst;
-public:
-
- SetEnumerator(TypeNode type, TypeEnumeratorProperties * tep = NULL) throw(AssertionException) :
- TypeEnumeratorBase<SetEnumerator>(type),
- d_tep(tep),
- d_index(0),
- d_constituentType(type.getSetElementType()),
- d_nm(NodeManager::currentNM()),
- d_indexVec(),
- d_constituentVec(),
- d_finished(false),
- d_setConst()
+ public:
+ SetEnumerator(TypeNode type, TypeEnumeratorProperties* tep = nullptr)
+ : TypeEnumeratorBase<SetEnumerator>(type),
+ d_tep(tep),
+ d_index(0),
+ d_constituentType(type.getSetElementType()),
+ d_nm(NodeManager::currentNM()),
+ d_indexVec(),
+ d_constituentVec(),
+ d_finished(false),
+ d_setConst()
{
// d_indexVec.push_back(false);
// d_constituentVec.push_back(new TypeEnumerator(d_constituentType));
// An set enumerator could be large, and generally you don't want to
// go around copying these things; but a copy ctor is presently required
// by the TypeEnumerator framework.
- SetEnumerator(const SetEnumerator& ae) throw() :
- TypeEnumeratorBase<SetEnumerator>(ae.d_nm->mkSetType(ae.d_constituentType)),
- d_tep(ae.d_tep),
- d_index(ae.d_index),
- d_constituentType(ae.d_constituentType),
- d_nm(ae.d_nm),
- d_indexVec(ae.d_indexVec),
- d_constituentVec(),// copied below
- d_finished(ae.d_finished),
- d_setConst(ae.d_setConst)
+ SetEnumerator(const SetEnumerator& ae)
+ : TypeEnumeratorBase<SetEnumerator>(
+ ae.d_nm->mkSetType(ae.d_constituentType)),
+ d_tep(ae.d_tep),
+ d_index(ae.d_index),
+ d_constituentType(ae.d_constituentType),
+ d_nm(ae.d_nm),
+ d_indexVec(ae.d_indexVec),
+ d_constituentVec(), // copied below
+ d_finished(ae.d_finished),
+ d_setConst(ae.d_setConst)
{
for(std::vector<TypeEnumerator*>::const_iterator i =
ae.d_constituentVec.begin(), i_end = ae.d_constituentVec.end();
}
}
- Node operator*() throw(NoMoreValuesException) {
+ Node operator*() override
+ {
if (d_finished) {
throw NoMoreValuesException(getType());
}
return n;
}
- SetEnumerator& operator++() throw() {
+ SetEnumerator& operator++() override
+ {
Trace("set-type-enum") << "operator++ called, **this = " << **this << std::endl;
if (d_finished) {
return *this;
}
- bool isFinished() throw() {
+ bool isFinished() override
+ {
Trace("set-type-enum") << "isFinished returning: " << d_finished << std::endl;
return d_finished;
}
//make constant from d_data
d_curr = NodeManager::currentNM()->mkConst( ::CVC4::String( d_data ) );
}
-public:
- StringEnumerator(TypeNode type, TypeEnumeratorProperties * tep = NULL) throw(AssertionException) :
- TypeEnumeratorBase<StringEnumerator>(type) {
+ public:
+ StringEnumerator(TypeNode type, TypeEnumeratorProperties* tep = nullptr)
+ : TypeEnumeratorBase<StringEnumerator>(type)
+ {
Assert(type.getKind() == kind::TYPE_CONSTANT &&
type.getConst<TypeConstant>() == STRING_TYPE);
d_cardinality = 256;
mkCurr();
}
- Node operator*() throw() {
- return d_curr;
- }
- StringEnumerator& operator++() {
- bool changed = false;
- do{
- for(unsigned i=0; i<d_data.size(); ++i) {
- if( d_data[i] + 1 < d_cardinality ) {
- ++d_data[i]; changed = true;
- break;
- } else {
- d_data[i] = 0;
+ Node operator*() override { return d_curr; }
+ StringEnumerator& operator++() override
+ {
+ bool changed = false;
+ do
+ {
+ for (unsigned i = 0; i < d_data.size(); ++i)
+ {
+ if (d_data[i] + 1 < d_cardinality)
+ {
+ ++d_data[i];
+ changed = true;
+ break;
+ }
+ else
+ {
+ d_data[i] = 0;
+ }
}
- }
- if(!changed) {
- d_data.push_back( 0 );
- }
- }while(!changed);
+ if (!changed)
+ {
+ d_data.push_back(0);
+ }
+ } while (!changed);
- mkCurr();
+ mkCurr();
return *this;
}
- bool isFinished() throw() {
- return d_curr.isNull();
- }
-
+ bool isFinished() override { return d_curr.isNull(); }
};/* class StringEnumerator */
class StringEnumeratorLength {
-private:
+ private:
unsigned d_cardinality;
std::vector< unsigned > d_data;
Node d_curr;
//make constant from d_data
d_curr = NodeManager::currentNM()->mkConst( ::CVC4::String( d_data ) );
}
-public:
+
+ public:
StringEnumeratorLength(unsigned length, unsigned card = 256) : d_cardinality(card) {
for( unsigned i=0; i<length; i++ ){
d_data.push_back( 0 );
mkCurr();
}
- Node operator*() throw() {
- return d_curr;
- }
-
+ Node operator*() { return d_curr; }
StringEnumeratorLength& operator++() {
bool changed = false;
for(unsigned i=0; i<d_data.size(); ++i) {
return *this;
}
- bool isFinished() throw() {
- return d_curr.isNull();
- }
+ bool isFinished() { return d_curr.isNull(); }
};
}/* CVC4::theory::strings namespace */
class TypeEnumerator {
TypeEnumeratorInterface* d_te;
- static TypeEnumeratorInterface* mkTypeEnumerator(TypeNode type, TypeEnumeratorProperties * tep)
- throw(AssertionException);
+ static TypeEnumeratorInterface* mkTypeEnumerator(
+ TypeNode type, TypeEnumeratorProperties* tep);
-public:
-
- TypeEnumerator(TypeNode type, TypeEnumeratorProperties * tep = NULL) throw() :
- d_te(mkTypeEnumerator(type, tep)) {
+ public:
+ TypeEnumerator(TypeNode type, TypeEnumeratorProperties* tep = nullptr)
+ : d_te(mkTypeEnumerator(type, tep))
+ {
}
TypeEnumerator(const TypeEnumerator& te) :
}
~TypeEnumerator() { delete d_te; }
-
- bool isFinished() throw() {
+ bool isFinished()
+ {
// On Mac clang, there appears to be a code generation bug in an exception
// block here. For now, there doesn't appear a good workaround; just disable
// assertions on that setup.
#endif /* CVC4_ASSERTIONS && !(APPLE || clang) */
return d_te->isFinished();
}
- Node operator*() throw(NoMoreValuesException) {
+ Node operator*()
+ {
// On Mac clang, there appears to be a code generation bug in an exception
// block above (and perhaps here, too). For now, there doesn't appear a
// good workaround; just disable assertions on that setup.
return **d_te;
#endif /* CVC4_ASSERTIONS && !(APPLE || clang) */
}
- TypeEnumerator& operator++() throw() { ++*d_te; return *this; }
- TypeEnumerator operator++(int) throw() { TypeEnumerator te = *this; ++*d_te; return te; }
-
- TypeNode getType() const throw() { return d_te->getType(); }
+ TypeEnumerator& operator++()
+ {
+ ++*d_te;
+ return *this;
+ }
+ TypeEnumerator operator++(int)
+ {
+ TypeEnumerator te = *this;
+ ++*d_te;
+ return te;
+ }
+ TypeNode getType() const { return d_te->getType(); }
};/* class TypeEnumerator */
}/* CVC4::theory namespace */
namespace CVC4 {
namespace theory {
-TypeEnumeratorInterface* TypeEnumerator::mkTypeEnumerator(TypeNode type, TypeEnumeratorProperties * tep) throw(AssertionException) {
+TypeEnumeratorInterface* TypeEnumerator::mkTypeEnumerator(
+ TypeNode type, TypeEnumeratorProperties* tep)
+{
switch(type.getKind()) {
case kind::TYPE_CONSTANT:
switch(type.getConst<TypeConstant>()) {
projects / cvc5.git / commitdiff