From 9d677333439c15677b6891ee8f6bd368a5df9f0a Mon Sep 17 00:00:00 2001 From: ajreynol Date: Fri, 15 Jan 2016 23:57:56 +0100 Subject: [PATCH] Type enumerators take optional argument indicating fixed cardinalities of uninterpreted sorts. Modify TheoryModelBuilder. Fix bug in fmf-empty-sorts. --- src/theory/arith/type_enumerator.h | 8 ++--- src/theory/arrays/type_enumerator.h | 17 +++++++---- src/theory/booleans/type_enumerator.h | 4 +-- src/theory/builtin/type_enumerator.h | 30 +++++++++++++++---- src/theory/bv/type_enumerator.h | 4 +-- src/theory/datatypes/type_enumerator.cpp | 4 +-- src/theory/datatypes/type_enumerator.h | 25 +++++++++++----- src/theory/mktheorytraits | 4 +-- src/theory/quantifiers/model_engine.cpp | 2 +- src/theory/sets/theory_sets_type_enumerator.h | 10 +++++-- src/theory/strings/type_enumerator.h | 4 +-- src/theory/theory_model.cpp | 14 +++++++++ src/theory/theory_model.h | 6 ++-- src/theory/type_enumerator.h | 20 ++++++++++--- src/theory/type_enumerator_template.cpp | 4 +-- 15 files changed, 111 insertions(+), 45 deletions(-) diff --git a/src/theory/arith/type_enumerator.h b/src/theory/arith/type_enumerator.h index c4501fc43..dc2b6f115 100644 --- a/src/theory/arith/type_enumerator.h +++ b/src/theory/arith/type_enumerator.h @@ -3,7 +3,7 @@ ** \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 @@ -34,7 +34,7 @@ class RationalEnumerator : public TypeEnumeratorBase { public: - RationalEnumerator(TypeNode type) throw(AssertionException) : + RationalEnumerator(TypeNode type, TypeEnumeratorProperties * tep = NULL) throw(AssertionException) : TypeEnumeratorBase(type), d_rat(0) { Assert(type.getKind() == kind::TYPE_CONSTANT && @@ -81,7 +81,7 @@ class IntegerEnumerator : public TypeEnumeratorBase { public: - IntegerEnumerator(TypeNode type) throw(AssertionException) : + IntegerEnumerator(TypeNode type, TypeEnumeratorProperties * tep = NULL) throw(AssertionException) : TypeEnumeratorBase(type), d_int(0) { Assert(type.getKind() == kind::TYPE_CONSTANT && @@ -115,7 +115,7 @@ class SubrangeEnumerator : public TypeEnumeratorBase { public: - SubrangeEnumerator(TypeNode type) throw(AssertionException) : + SubrangeEnumerator(TypeNode type, TypeEnumeratorProperties * tep = NULL) throw(AssertionException) : TypeEnumeratorBase(type), d_int(0), d_bounds(type.getConst()), diff --git a/src/theory/arrays/type_enumerator.h b/src/theory/arrays/type_enumerator.h index 2c6fc56ab..ace23eb82 100644 --- a/src/theory/arrays/type_enumerator.h +++ b/src/theory/arrays/type_enumerator.h @@ -3,7 +3,7 @@ ** \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 @@ -29,6 +29,8 @@ namespace theory { namespace arrays { class ArrayEnumerator : public TypeEnumeratorBase { + /** type properties */ + TypeEnumeratorProperties * d_tep; TypeEnumerator d_index; TypeNode d_constituentType; NodeManager* d_nm; @@ -39,9 +41,10 @@ class ArrayEnumerator : public TypeEnumeratorBase { public: - ArrayEnumerator(TypeNode type) throw(AssertionException) : + ArrayEnumerator(TypeNode type, TypeEnumeratorProperties * tep = NULL) throw(AssertionException) : TypeEnumeratorBase(type), - d_index(type.getArrayIndexType()), + d_tep(tep), + d_index(type.getArrayIndexType(), tep), d_constituentType(type.getArrayConstituentType()), d_nm(NodeManager::currentNM()), d_indexVec(), @@ -50,8 +53,9 @@ public: 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 @@ -59,6 +63,7 @@ public: // by the TypeEnumerator framework. ArrayEnumerator(const ArrayEnumerator& ae) throw() : TypeEnumeratorBase(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), @@ -122,7 +127,7 @@ public: 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; @@ -132,7 +137,7 @@ public: } 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; diff --git a/src/theory/booleans/type_enumerator.h b/src/theory/booleans/type_enumerator.h index 34b1401e8..3849f8435 100644 --- a/src/theory/booleans/type_enumerator.h +++ b/src/theory/booleans/type_enumerator.h @@ -3,7 +3,7 @@ ** \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 @@ -32,7 +32,7 @@ class BooleanEnumerator : public TypeEnumeratorBase { public: - BooleanEnumerator(TypeNode type) : + BooleanEnumerator(TypeNode type, TypeEnumeratorProperties * tep = NULL) : TypeEnumeratorBase(type), d_value(FALSE) { Assert(type.getKind() == kind::TYPE_CONSTANT && diff --git a/src/theory/builtin/type_enumerator.h b/src/theory/builtin/type_enumerator.h index 635cf7dc7..5ef0e4ab8 100644 --- a/src/theory/builtin/type_enumerator.h +++ b/src/theory/builtin/type_enumerator.h @@ -3,7 +3,7 @@ ** \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 @@ -31,16 +31,32 @@ namespace builtin { class UninterpretedSortEnumerator : public TypeEnumeratorBase { 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(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)); } @@ -50,7 +66,11 @@ public: } bool isFinished() throw() { - return false; + if( d_has_fixed_bound ){ + return d_count>=d_fixed_bound; + }else{ + return false; + } } };/* class UninterpretedSortEnumerator */ diff --git a/src/theory/bv/type_enumerator.h b/src/theory/bv/type_enumerator.h index db98ef66b..da06b1152 100644 --- a/src/theory/bv/type_enumerator.h +++ b/src/theory/bv/type_enumerator.h @@ -3,7 +3,7 @@ ** \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 @@ -35,7 +35,7 @@ class BitVectorEnumerator : public TypeEnumeratorBase { public: - BitVectorEnumerator(TypeNode type) throw(AssertionException) : + BitVectorEnumerator(TypeNode type, TypeEnumeratorProperties * tep = NULL) throw(AssertionException) : TypeEnumeratorBase(type), d_size(type.getBitVectorSize()), d_bits(0) { diff --git a/src/theory/datatypes/type_enumerator.cpp b/src/theory/datatypes/type_enumerator.cpp index 26689c81a..57d16d31c 100644 --- a/src/theory/datatypes/type_enumerator.cpp +++ b/src/theory/datatypes/type_enumerator.cpp @@ -35,10 +35,10 @@ Node DatatypesEnumerator::getTermEnum( TypeNode tn, unsigned i ){ 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{ diff --git a/src/theory/datatypes/type_enumerator.h b/src/theory/datatypes/type_enumerator.h index 0e5aad640..67dabafe4 100644 --- a/src/theory/datatypes/type_enumerator.h +++ b/src/theory/datatypes/type_enumerator.h @@ -30,6 +30,8 @@ namespace datatypes { class DatatypesEnumerator : public TypeEnumeratorBase { + /** type properties */ + TypeEnumeratorProperties * d_tep; /** The datatype we're enumerating */ const Datatype& d_datatype; /** extra cons */ @@ -78,15 +80,17 @@ class DatatypesEnumerator : public TypeEnumeratorBase { void init(); public: - DatatypesEnumerator(TypeNode type) throw() : + DatatypesEnumerator(TypeNode type, TypeEnumeratorProperties * tep = NULL) throw() : TypeEnumeratorBase(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(type), + d_tep(tep), d_datatype(DatatypeType(type.toType()).getDatatype()), d_type(type) { d_child_enum = childEnum; @@ -94,6 +98,7 @@ public: } DatatypesEnumerator(const DatatypesEnumerator& de) throw() : TypeEnumeratorBase(de.getType()), + d_tep(de.d_tep), d_datatype(de.d_datatype), d_type(de.d_type), d_ctor(de.d_ctor), @@ -172,13 +177,14 @@ public: };/* DatatypesEnumerator */ class TupleEnumerator : public TypeEnumeratorBase { + 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); } } @@ -194,14 +200,15 @@ class TupleEnumerator : public TypeEnumeratorBase { public: - TupleEnumerator(TypeNode type) throw() : - TypeEnumeratorBase(type) { + TupleEnumerator(TypeNode type, TypeEnumeratorProperties * tep = NULL) throw() : + TypeEnumeratorBase(type), d_tep(tep) { Assert(type.isTuple()); newEnumerators(); } TupleEnumerator(const TupleEnumerator& te) throw() : TypeEnumeratorBase(te.getType()), + d_tep(te.d_tep), d_enumerators(NULL) { if(te.d_enumerators != NULL) { @@ -236,7 +243,7 @@ public: 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; @@ -255,6 +262,7 @@ public: };/* TupleEnumerator */ class RecordEnumerator : public TypeEnumeratorBase { + TypeEnumeratorProperties * d_tep; TypeEnumerator** d_enumerators; /** Allocate and initialize the delegate enumerators */ @@ -279,14 +287,15 @@ class RecordEnumerator : public TypeEnumeratorBase { public: - RecordEnumerator(TypeNode type) throw() : - TypeEnumeratorBase(type) { + RecordEnumerator(TypeNode type, TypeEnumeratorProperties * tep = NULL) throw() : + TypeEnumeratorBase(type), d_tep(tep) { Assert(type.isRecord()); newEnumerators(); } RecordEnumerator(const RecordEnumerator& re) throw() : TypeEnumeratorBase(re.getType()), + d_tep(re.d_tep), d_enumerators(NULL) { if(re.d_enumerators != NULL) { diff --git a/src/theory/mktheorytraits b/src/theory/mktheorytraits index d6725997d..b6162ec38 100755 --- a/src/theory/mktheorytraits +++ b/src/theory/mktheorytraits @@ -234,14 +234,14 @@ function enumerator { #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 diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp index eb827edc3..4b173c833 100644 --- a/src/theory/quantifiers/model_engine.cpp +++ b/src/theory/quantifiers/model_engine.cpp @@ -232,7 +232,7 @@ bool ModelEngine::considerQuantifiedFormula( Node q ) { for( unsigned i=0; igetModel()->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; } diff --git a/src/theory/sets/theory_sets_type_enumerator.h b/src/theory/sets/theory_sets_type_enumerator.h index fa8f108c3..bb0e1794c 100644 --- a/src/theory/sets/theory_sets_type_enumerator.h +++ b/src/theory/sets/theory_sets_type_enumerator.h @@ -3,7 +3,7 @@ ** \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 @@ -32,6 +32,8 @@ namespace theory { namespace sets { class SetEnumerator : public TypeEnumeratorBase { + /** type properties */ + TypeEnumeratorProperties * d_tep; unsigned d_index; TypeNode d_constituentType; NodeManager* d_nm; @@ -42,8 +44,9 @@ class SetEnumerator : public TypeEnumeratorBase { public: - SetEnumerator(TypeNode type) throw(AssertionException) : + SetEnumerator(TypeNode type, TypeEnumeratorProperties * tep = NULL) throw(AssertionException) : TypeEnumeratorBase(type), + d_tep(tep), d_index(0), d_constituentType(type.getSetElementType()), d_nm(NodeManager::currentNM()), @@ -62,6 +65,7 @@ public: // by the TypeEnumerator framework. SetEnumerator(const SetEnumerator& ae) throw() : TypeEnumeratorBase(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), @@ -145,7 +149,7 @@ public: 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) { diff --git a/src/theory/strings/type_enumerator.h b/src/theory/strings/type_enumerator.h index cfc3fe02b..bdaa683c1 100644 --- a/src/theory/strings/type_enumerator.h +++ b/src/theory/strings/type_enumerator.h @@ -3,7 +3,7 @@ ** \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 @@ -40,7 +40,7 @@ class StringEnumerator : public TypeEnumeratorBase { } public: - StringEnumerator(TypeNode type) throw(AssertionException) : + StringEnumerator(TypeNode type, TypeEnumeratorProperties * tep = NULL) throw(AssertionException) : TypeEnumeratorBase(type) { Assert(type.getKind() == kind::TYPE_CONSTANT && type.getConst() == STRING_TYPE); diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp index c6837ddf4..5ddb1c31a 100644 --- a/src/theory/theory_model.cpp +++ b/src/theory/theory_model.cpp @@ -587,6 +587,14 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel) // 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) { @@ -810,14 +818,20 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel) 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()) { diff --git a/src/theory/theory_model.h b/src/theory/theory_model.h index 8ee4e843d..e609bf703 100644 --- a/src/theory/theory_model.h +++ b/src/theory/theory_model.h @@ -130,8 +130,10 @@ public: 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) { @@ -146,7 +148,7 @@ private: } } } - + void setTypeEnumeratorProperties( TypeEnumeratorProperties * tep ) { d_tep = tep; } void add(TypeNode t, TNode n) { iterator it = d_typeSet.find(t); @@ -175,7 +177,7 @@ private: 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 { diff --git a/src/theory/type_enumerator.h b/src/theory/type_enumerator.h index 015cbb288..951967f50 100644 --- a/src/theory/type_enumerator.h +++ b/src/theory/type_enumerator.h @@ -3,7 +3,7 @@ ** \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 @@ -62,6 +62,18 @@ public: };/* 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 TypeEnumeratorBase : public TypeEnumeratorInterface { public: @@ -77,13 +89,13 @@ 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) : diff --git a/src/theory/type_enumerator_template.cpp b/src/theory/type_enumerator_template.cpp index f0eafed18..6f9b565bf 100644 --- a/src/theory/type_enumerator_template.cpp +++ b/src/theory/type_enumerator_template.cpp @@ -3,7 +3,7 @@ ** \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 @@ -29,7 +29,7 @@ using namespace std; 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()) { -- 2.30.2