** \verbatim
** Original author: Morgan Deters
** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Minor contributors (to current version): Andrew Reynolds
** This file is part of the CVC4 project.
** Copyright (c) 2009-2014 New York University and The University of Iowa
** See the file COPYING in the top-level source directory for licensing
public:
- RationalEnumerator(TypeNode type) throw(AssertionException) :
+ RationalEnumerator(TypeNode type, TypeEnumeratorProperties * tep = NULL) throw(AssertionException) :
TypeEnumeratorBase<RationalEnumerator>(type),
d_rat(0) {
Assert(type.getKind() == kind::TYPE_CONSTANT &&
public:
- IntegerEnumerator(TypeNode type) throw(AssertionException) :
+ IntegerEnumerator(TypeNode type, TypeEnumeratorProperties * tep = NULL) throw(AssertionException) :
TypeEnumeratorBase<IntegerEnumerator>(type),
d_int(0) {
Assert(type.getKind() == kind::TYPE_CONSTANT &&
public:
- SubrangeEnumerator(TypeNode type) throw(AssertionException) :
+ SubrangeEnumerator(TypeNode type, TypeEnumeratorProperties * tep = NULL) throw(AssertionException) :
TypeEnumeratorBase<SubrangeEnumerator>(type),
d_int(0),
d_bounds(type.getConst<SubrangeBounds>()),
** \verbatim
** Original author: Morgan Deters
** Major contributors: Clark Barrett
- ** Minor contributors (to current version): none
+ ** Minor contributors (to current version): Andrew Reynolds
** This file is part of the CVC4 project.
** Copyright (c) 2009-2014 New York University and The University of Iowa
** See the file COPYING in the top-level source directory for licensing
namespace arrays {
class ArrayEnumerator : public TypeEnumeratorBase<ArrayEnumerator> {
+ /** type properties */
+ TypeEnumeratorProperties * d_tep;
TypeEnumerator d_index;
TypeNode d_constituentType;
NodeManager* d_nm;
public:
- ArrayEnumerator(TypeNode type) throw(AssertionException) :
+ ArrayEnumerator(TypeNode type, TypeEnumeratorProperties * tep = NULL) throw(AssertionException) :
TypeEnumeratorBase<ArrayEnumerator>(type),
- d_index(type.getArrayIndexType()),
+ d_tep(tep),
+ d_index(type.getArrayIndexType(), tep),
d_constituentType(type.getArrayConstituentType()),
d_nm(NodeManager::currentNM()),
d_indexVec(),
d_arrayConst()
{
d_indexVec.push_back(*d_index);
- d_constituentVec.push_back(new TypeEnumerator(d_constituentType));
+ d_constituentVec.push_back(new TypeEnumerator(d_constituentType, d_tep));
d_arrayConst = d_nm->mkConst(ArrayStoreAll(type.toType(), (*(*d_constituentVec.back())).toExpr()));
+ Trace("array-type-enum") << "Array const : " << d_arrayConst << std::endl;
}
// An array enumerator could be large, and generally you don't want to
// 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),
return *this;
}
d_indexVec.push_back(*d_index);
- d_constituentVec.push_back(new TypeEnumerator(d_constituentType));
+ d_constituentVec.push_back(new TypeEnumerator(d_constituentType, d_tep));
++(*d_constituentVec.back());
if (d_constituentVec.back()->isFinished()) {
Trace("array-type-enum") << "operator++ finished!" << std::endl;
}
while (d_constituentVec.size() < d_indexVec.size()) {
- d_constituentVec.push_back(new TypeEnumerator(d_constituentType));
+ d_constituentVec.push_back(new TypeEnumerator(d_constituentType, d_tep));
}
Trace("array-type-enum") << "operator++ returning, **this = " << **this << std::endl;
** \verbatim
** Original author: Morgan Deters
** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Minor contributors (to current version): Andrew Reynolds
** This file is part of the CVC4 project.
** Copyright (c) 2009-2014 New York University and The University of Iowa
** See the file COPYING in the top-level source directory for licensing
public:
- BooleanEnumerator(TypeNode type) :
+ BooleanEnumerator(TypeNode type, TypeEnumeratorProperties * tep = NULL) :
TypeEnumeratorBase<BooleanEnumerator>(type),
d_value(FALSE) {
Assert(type.getKind() == kind::TYPE_CONSTANT &&
** \verbatim
** Original author: Morgan Deters
** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Minor contributors (to current version): Andrew Reynolds
** This file is part of the CVC4 project.
** Copyright (c) 2009-2014 New York University and The University of Iowa
** See the file COPYING in the top-level source directory for licensing
class UninterpretedSortEnumerator : public TypeEnumeratorBase<UninterpretedSortEnumerator> {
Integer d_count;
-
+ bool d_has_fixed_bound;
+ Integer d_fixed_bound;
public:
- UninterpretedSortEnumerator(TypeNode type) throw(AssertionException) :
+ UninterpretedSortEnumerator(TypeNode type, TypeEnumeratorProperties * tep = NULL) throw(AssertionException) :
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;
+ if( tep && tep->d_fixed_usort_card ){
+ d_has_fixed_bound = true;
+ std::map< TypeNode, Integer >::iterator it = tep->d_fixed_card.find( type );
+ if( it!=tep->d_fixed_card.end() ){
+ d_fixed_bound = it->second;
+ }else{
+ d_fixed_bound = Integer(1);
+ }
+ Trace("uf-type-enum") << "...fixed bound : " << d_fixed_bound << std::endl;
+ }
}
- Node operator*() throw() {
+ Node operator*() throw(NoMoreValuesException) {
+ if(isFinished()) {
+ throw NoMoreValuesException(getType());
+ }
return NodeManager::currentNM()->mkConst(UninterpretedConstant(getType().toType(), d_count));
}
}
bool isFinished() throw() {
- return false;
+ if( d_has_fixed_bound ){
+ return d_count>=d_fixed_bound;
+ }else{
+ return false;
+ }
}
};/* class UninterpretedSortEnumerator */
** \verbatim
** Original author: Morgan Deters
** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Minor contributors (to current version): Andrew Reynolds
** This file is part of the CVC4 project.
** Copyright (c) 2009-2014 New York University and The University of Iowa
** See the file COPYING in the top-level source directory for licensing
public:
- BitVectorEnumerator(TypeNode type) throw(AssertionException) :
+ BitVectorEnumerator(TypeNode type, TypeEnumeratorProperties * tep = NULL) throw(AssertionException) :
TypeEnumeratorBase<BitVectorEnumerator>(type),
d_size(type.getBitVectorSize()),
d_bits(0) {
d_te_index[tn] = tei;
if( tn.isDatatype() && d_has_debruijn ){
//must indicate that this is a child enumerator (do not normalize constants for it)
- DatatypesEnumerator * dte = new DatatypesEnumerator( tn, true );
+ DatatypesEnumerator * dte = new DatatypesEnumerator( tn, true, d_tep );
d_children.push_back( TypeEnumerator( dte ) );
}else{
- d_children.push_back( TypeEnumerator( tn ) );
+ d_children.push_back( TypeEnumerator( tn, d_tep ) );
}
d_terms[tn].push_back( *d_children[tei] );
}else{
class DatatypesEnumerator : public TypeEnumeratorBase<DatatypesEnumerator> {
+ /** type properties */
+ TypeEnumeratorProperties * d_tep;
/** The datatype we're enumerating */
const Datatype& d_datatype;
/** extra cons */
void init();
public:
- DatatypesEnumerator(TypeNode type) throw() :
+ DatatypesEnumerator(TypeNode type, TypeEnumeratorProperties * tep = NULL) throw() :
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) throw() :
+ DatatypesEnumerator(TypeNode type, bool childEnum, TypeEnumeratorProperties * tep = NULL) throw() :
TypeEnumeratorBase<DatatypesEnumerator>(type),
+ d_tep(tep),
d_datatype(DatatypeType(type.toType()).getDatatype()),
d_type(type) {
d_child_enum = childEnum;
}
DatatypesEnumerator(const DatatypesEnumerator& de) throw() :
TypeEnumeratorBase<DatatypesEnumerator>(de.getType()),
+ d_tep(de.d_tep),
d_datatype(de.d_datatype),
d_type(de.d_type),
d_ctor(de.d_ctor),
};/* DatatypesEnumerator */
class TupleEnumerator : public TypeEnumeratorBase<TupleEnumerator> {
+ TypeEnumeratorProperties * d_tep;
TypeEnumerator** d_enumerators;
/** Allocate and initialize the delegate enumerators */
void newEnumerators() {
d_enumerators = new TypeEnumerator*[getType().getNumChildren()];
for(size_t i = 0; i < getType().getNumChildren(); ++i) {
- d_enumerators[i] = new TypeEnumerator(getType()[i]);
+ d_enumerators[i] = new TypeEnumerator(getType()[i], d_tep);
}
}
public:
- TupleEnumerator(TypeNode type) throw() :
- TypeEnumeratorBase<TupleEnumerator>(type) {
+ TupleEnumerator(TypeNode type, TypeEnumeratorProperties * tep = NULL) throw() :
+ TypeEnumeratorBase<TupleEnumerator>(type), d_tep(tep) {
Assert(type.isTuple());
newEnumerators();
}
TupleEnumerator(const TupleEnumerator& te) throw() :
TypeEnumeratorBase<TupleEnumerator>(te.getType()),
+ d_tep(te.d_tep),
d_enumerators(NULL) {
if(te.d_enumerators != NULL) {
size_t i;
for(i = 0; i < getType().getNumChildren(); ++i) {
if(d_enumerators[i]->isFinished()) {
- *d_enumerators[i] = TypeEnumerator(getType()[i]);
+ *d_enumerators[i] = TypeEnumerator(getType()[i], d_tep);
} else {
++*d_enumerators[i];
return *this;
};/* TupleEnumerator */
class RecordEnumerator : public TypeEnumeratorBase<RecordEnumerator> {
+ TypeEnumeratorProperties * d_tep;
TypeEnumerator** d_enumerators;
/** Allocate and initialize the delegate enumerators */
public:
- RecordEnumerator(TypeNode type) throw() :
- TypeEnumeratorBase<RecordEnumerator>(type) {
+ RecordEnumerator(TypeNode type, TypeEnumeratorProperties * tep = NULL) throw() :
+ TypeEnumeratorBase<RecordEnumerator>(type), d_tep(tep) {
Assert(type.isRecord());
newEnumerators();
}
RecordEnumerator(const RecordEnumerator& re) throw() :
TypeEnumeratorBase<RecordEnumerator>(re.getType()),
+ d_tep(re.d_tep),
d_enumerators(NULL) {
if(re.d_enumerators != NULL) {
#line $lineno \"$kf\"
case $1:
#line $lineno \"$kf\"
- return new $2(type);
+ return new $2(type, tep);
"
elif expr "$type_kinds" : '.* '"$1"' ' &>/dev/null; then
mk_type_enumerator_cases="${mk_type_enumerator_cases}
#line $lineno \"$kf\"
case kind::$1:
#line $lineno \"$kf\"
- return new $2(type);
+ return new $2(type, tep);
"
else
echo "$kf:$lineno: error: don't know anything about $1; enumerator must appear after definition" >&2
for( unsigned i=0; i<q[0].getNumChildren(); i++ ){
TypeNode tn = q[0][i].getType();
//we are allowed to assume the type is empty
- if( d_quantEngine->getModel()->d_rep_set.getNumRelevantGroundReps( tn )==0 ){
+ if( tn.isSort() && d_quantEngine->getModel()->d_rep_set.getNumRelevantGroundReps( tn )==0 ){
Trace("model-engine-debug") << "Empty domain quantified formula : " << q << std::endl;
return false;
}
** \verbatim
** Original author: Kshitij Bansal
** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Minor contributors (to current version): Andrew Reynolds
** This file is part of the CVC4 project.
** Copyright (c) 2009-2014 New York University and The University of Iowa
** See the file COPYING in the top-level source directory for licensing
namespace sets {
class SetEnumerator : public TypeEnumeratorBase<SetEnumerator> {
+ /** type properties */
+ TypeEnumeratorProperties * d_tep;
unsigned d_index;
TypeNode d_constituentType;
NodeManager* d_nm;
public:
- SetEnumerator(TypeNode type) throw(AssertionException) :
+ 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()),
// 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),
if (d_constituentVec.empty()) {
++d_index;
- d_constituentVec.push_back(new TypeEnumerator(d_constituentType));
+ d_constituentVec.push_back(new TypeEnumerator(d_constituentType, d_tep));
}
while (d_constituentVec.size() < d_index) {
** \verbatim
** Original author: Tianyi Liang
** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Minor contributors (to current version): Andrew Reynolds
** This file is part of the CVC4 project.
** Copyright (c) 2009-2014 New York University and The University of Iowa
** See the file COPYING in the top-level source directory for licensing
}
public:
- StringEnumerator(TypeNode type) throw(AssertionException) :
+ StringEnumerator(TypeNode type, TypeEnumeratorProperties * tep = NULL) throw(AssertionException) :
TypeEnumeratorBase<StringEnumerator>(type) {
Assert(type.getKind() == kind::TYPE_CONSTANT &&
type.getConst<TypeConstant>() == STRING_TYPE);
// Process all terms in the equality engine, store representatives for each EC
std::map< Node, Node > assertedReps, constantReps;
TypeSet typeConstSet, typeRepSet, typeNoRepSet;
+ TypeEnumeratorProperties tep;
+ if( options::finiteModelFind() ){
+ tep.d_fixed_usort_card = true;
+ for( std::map< TypeNode, unsigned >::iterator it = eqc_usort_count.begin(); it != eqc_usort_count.end(); ++it ){
+ tep.d_fixed_card[it->first] = Integer(it->second);
+ }
+ typeConstSet.setTypeEnumeratorProperties( &tep );
+ }
std::set< TypeNode > allTypes;
eqcs_i = eq::EqClassesIterator(tm->d_equalityEngine);
for ( ; !eqcs_i.isFinished(); ++eqcs_i) {
do{
n = typeConstSet.nextTypeEnum(t, true);
//--- AJR: this code checks whether n is a legal value
+ Assert( !n.isNull() );
success = true;
+ Trace("exc-value-debug") << "Check if excluded : " << n << std::endl;
if( isUSortFiniteRestricted ){
+#ifdef CVC4_ASSERTIONS
//must not involve uninterpreted constants beyond cardinality bound (which assumed to coincide with #eqc)
+ //this is just an assertion now, since TypeEnumeratorProperties should ensure that only legal values are enumerated wrt this constraint.
std::map< Node, bool > visited;
success = !isExcludedUSortValue( eqc_usort_count, n, visited );
if( !success ){
Trace("exc-value") << "Excluded value for " << t << " : " << n << " due to out of range uninterpreted constant." << std::endl;
}
+ Assert( success );
+#endif
}
if( success && isCorecursive ){
if (repSet != NULL && !repSet->empty()) {
private:
TypeSetMap d_typeSet;
TypeToTypeEnumMap d_teMap;
+ TypeEnumeratorProperties * d_tep;
public:
+ TypeSet() : d_tep(NULL) {}
~TypeSet() {
iterator it;
for (it = d_typeSet.begin(); it != d_typeSet.end(); ++it) {
}
}
}
-
+ void setTypeEnumeratorProperties( TypeEnumeratorProperties * tep ) { d_tep = tep; }
void add(TypeNode t, TNode n)
{
iterator it = d_typeSet.find(t);
TypeEnumerator* te;
TypeToTypeEnumMap::iterator it = d_teMap.find(t);
if (it == d_teMap.end()) {
- te = new TypeEnumerator(t);
+ te = new TypeEnumerator(t, d_tep);
d_teMap[t] = te;
}
else {
** \verbatim
** Original author: Morgan Deters
** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Minor contributors (to current version): Andrew Reynolds
** This file is part of the CVC4 project.
** Copyright (c) 2009-2014 New York University and The University of Iowa
** See the file COPYING in the top-level source directory for licensing
};/* class TypeEnumeratorInterface */
+// AJR: This class stores particular information that is relevant to type enumeration.
+// For finite model finding, we set d_fixed_usort=true,
+// and store the finite cardinality bounds for each uninterpreted sort encountered in the model.
+class TypeEnumeratorProperties
+{
+public:
+ TypeEnumeratorProperties() : d_fixed_usort_card(false){}
+ Integer getFixedCardinality( TypeNode tn ) { return d_fixed_card[tn]; }
+ bool d_fixed_usort_card;
+ std::map< TypeNode, Integer > d_fixed_card;
+};
+
template <class T>
class TypeEnumeratorBase : public TypeEnumeratorInterface {
public:
class TypeEnumerator {
TypeEnumeratorInterface* d_te;
- static TypeEnumeratorInterface* mkTypeEnumerator(TypeNode type)
+ static TypeEnumeratorInterface* mkTypeEnumerator(TypeNode type, TypeEnumeratorProperties * tep)
throw(AssertionException);
public:
- TypeEnumerator(TypeNode type) throw() :
- d_te(mkTypeEnumerator(type)) {
+ TypeEnumerator(TypeNode type, TypeEnumeratorProperties * tep = NULL) throw() :
+ d_te(mkTypeEnumerator(type, tep)) {
}
TypeEnumerator(const TypeEnumerator& te) :
** \verbatim
** Original author: Morgan Deters
** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Minor contributors (to current version): Andrew Reynolds
** This file is part of the CVC4 project.
** Copyright (c) 2009-2014 New York University and The University of Iowa
** See the file COPYING in the top-level source directory for licensing
namespace CVC4 {
namespace theory {
-TypeEnumeratorInterface* TypeEnumerator::mkTypeEnumerator(TypeNode type) throw(AssertionException) {
+TypeEnumeratorInterface* TypeEnumerator::mkTypeEnumerator(TypeNode type, TypeEnumeratorProperties * tep) throw(AssertionException) {
switch(type.getKind()) {
case kind::TYPE_CONSTANT:
switch(type.getConst<TypeConstant>()) {
projects / cvc5.git / commitdiff