diff options
Diffstat (limited to 'src')
-rw-r--r-- | src/expr/datatype.cpp | 19 | ||||
-rw-r--r-- | src/expr/datatype.h | 4 | ||||
-rw-r--r-- | src/expr/type_node.cpp | 21 | ||||
-rw-r--r-- | src/expr/type_node.h | 7 | ||||
-rw-r--r-- | src/theory/datatypes/theory_datatypes.cpp | 6 | ||||
-rw-r--r-- | src/theory/datatypes/type_enumerator.cpp | 2 | ||||
-rw-r--r-- | src/theory/datatypes/type_enumerator.h | 2 | ||||
-rw-r--r-- | src/theory/quantifiers/quant_split.cpp | 6 | ||||
-rw-r--r-- | src/theory/term_registration_visitor.cpp | 40 | ||||
-rw-r--r-- | src/theory/theory_model.cpp | 1 |
10 files changed, 49 insertions, 59 deletions
diff --git a/src/expr/datatype.cpp b/src/expr/datatype.cpp index d14ac26d4..001f38a79 100644 --- a/src/expr/datatype.cpp +++ b/src/expr/datatype.cpp @@ -297,7 +297,7 @@ bool Datatype::isFinite() const throw(IllegalArgumentException) { return true; } -bool Datatype::isUFinite() const throw(IllegalArgumentException) { +bool Datatype::isInterpretedFinite() const throw(IllegalArgumentException) { PrettyCheckArgument(isResolved(), this, "this datatype is not yet resolved"); // we're using some internals, so we have to set up this library context ExprManagerScope ems(d_self); @@ -310,7 +310,7 @@ bool Datatype::isUFinite() const throw(IllegalArgumentException) { self.setAttribute(DatatypeUFiniteComputedAttr(), true); self.setAttribute(DatatypeUFiniteAttr(), false); for(const_iterator i = begin(), i_end = end(); i != i_end; ++i) { - if(! (*i).isUFinite()) { + if(! (*i).isInterpretedFinite()) { return false; } } @@ -850,7 +850,7 @@ bool DatatypeConstructor::isFinite() const throw(IllegalArgumentException) { return true; } -bool DatatypeConstructor::isUFinite() const throw(IllegalArgumentException) { +bool DatatypeConstructor::isInterpretedFinite() const throw(IllegalArgumentException) { PrettyCheckArgument(isResolved(), this, "this datatype constructor is not yet resolved"); // we're using some internals, so we have to set up this library context ExprManagerScope ems(d_constructor); @@ -859,18 +859,9 @@ bool DatatypeConstructor::isUFinite() const throw(IllegalArgumentException) { if(self.getAttribute(DatatypeUFiniteComputedAttr())) { return self.getAttribute(DatatypeUFiniteAttr()); } - bool success = true; for(const_iterator i = begin(), i_end = end(); i != i_end; ++i) { - Type t = (*i).getRangeType(); - if( t.isDatatype() ){ - const Datatype& dt = ((DatatypeType)t).getDatatype(); - if( !dt.isUFinite() ){ - success = false; - } - }else if(!t.isSort() && !t.getCardinality().isFinite()) { - success = false; - } - if(!success ){ + TypeNode t = TypeNode::fromType( (*i).getRangeType() ); + if(!t.isInterpretedFinite()) { self.setAttribute(DatatypeUFiniteComputedAttr(), true); self.setAttribute(DatatypeUFiniteAttr(), false); return false; diff --git a/src/expr/datatype.h b/src/expr/datatype.h index 1197b4a3b..dfd893fe8 100644 --- a/src/expr/datatype.h +++ b/src/expr/datatype.h @@ -342,7 +342,7 @@ public: * uninterpreted sorts are finite. This function can * only be called for resolved constructors. */ - bool isUFinite() const throw(IllegalArgumentException); + bool isInterpretedFinite() const throw(IllegalArgumentException); /** * Returns true iff this Datatype constructor has already been @@ -634,7 +634,7 @@ public: * datatype is not well-founded, this function returns false. The * Datatype must be resolved or an exception is thrown. */ - bool isUFinite() const throw(IllegalArgumentException); + bool isInterpretedFinite() const throw(IllegalArgumentException); /** * Return true iff this datatype is well-founded (there exist ground diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp index 5d672e6ac..dc2370bea 100644 --- a/src/expr/type_node.cpp +++ b/src/expr/type_node.cpp @@ -21,6 +21,7 @@ #include "expr/type_properties.h" #include "options/base_options.h" #include "options/expr_options.h" +#include "options/quantifiers_options.h" using namespace std; @@ -64,6 +65,26 @@ Cardinality TypeNode::getCardinality() const { return kind::getCardinality(*this); } +bool TypeNode::isInterpretedFinite() const { + if( getCardinality().isFinite() ){ + return true; + }else{ + if( options::finiteModelFind() ){ + if( isSort() ){ + return true; + }else if( isDatatype() || isParametricDatatype() ){ + const Datatype& dt = getDatatype(); + return dt.isInterpretedFinite(); + }else if( isArray() ){ + return getArrayIndexType().isInterpretedFinite() && getArrayConstituentType().isInterpretedFinite(); + }else if( isSet() ) { + return getSetElementType().isInterpretedFinite(); + } + } + return false; + } +} + bool TypeNode::isWellFounded() const { return kind::isWellFounded(*this); } diff --git a/src/expr/type_node.h b/src/expr/type_node.h index cfb61a085..46fdaa143 100644 --- a/src/expr/type_node.h +++ b/src/expr/type_node.h @@ -419,6 +419,13 @@ public: * @return a finite or infinite cardinality */ Cardinality getCardinality() const; + + /** + * Is this type interpreted as being finite. + * If finite model finding is enabled, this assumes all uninterpreted sorts + * are interpreted as finite. + */ + bool isInterpretedFinite() const; /** * Returns whether this type is well-founded. diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index 0100f1833..95d704a0e 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -191,7 +191,7 @@ void TheoryDatatypes::check(Effort e) { if( !hasLabel( eqc, n ) ){ Trace("datatypes-debug") << "No constructor..." << std::endl; const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype(); - Trace("datatypes-debug") << "Datatype " << dt << " is " << dt.isFinite() << " " << dt.isUFinite() << " " << dt.isRecursiveSingleton() << std::endl; + Trace("datatypes-debug") << "Datatype " << dt << " is " << dt.isFinite() << " " << dt.isInterpretedFinite() << " " << dt.isRecursiveSingleton() << std::endl; bool continueProc = true; if( dt.isRecursiveSingleton() ){ Trace("datatypes-debug") << "Check recursive singleton..." << std::endl; @@ -252,7 +252,7 @@ void TheoryDatatypes::check(Effort e) { if( consIndex==-1 ){ consIndex = j; } - if( options::finiteModelFind() ? !dt[ j ].isUFinite() : !dt[ j ].isFinite() ) { + if( !dt[ j ].isInterpretedFinite() ) { if( !eqc || !eqc->d_selectors ){ needSplit = false; } @@ -1497,7 +1497,7 @@ void TheoryDatatypes::collectModelInfo( TheoryModel* m, bool fullModel ){ if( neqc.isNull() ){ for( unsigned i=0; i<pcons.size(); i++ ){ //must try the infinite ones first - bool cfinite = options::finiteModelFind() ? dt[ i ].isUFinite() : dt[ i ].isFinite(); + bool cfinite = dt[ i ].isInterpretedFinite(); if( pcons[i] && (r==1)==cfinite ){ neqc = DatatypesRewriter::getInstCons( eqc, dt, i ); //for( unsigned j=0; j<neqc.getNumChildren(); j++ ){ diff --git a/src/theory/datatypes/type_enumerator.cpp b/src/theory/datatypes/type_enumerator.cpp index 6c1155237..c0539743f 100644 --- a/src/theory/datatypes/type_enumerator.cpp +++ b/src/theory/datatypes/type_enumerator.cpp @@ -172,7 +172,7 @@ Node DatatypesEnumerator::getTermEnum( TypeNode tn, unsigned i ){ Debug("dt-enum") << "datatype is " << d_type << std::endl; Debug("dt-enum") << "properties : " << d_datatype.isCodatatype() << " " << d_datatype.isRecursiveSingleton(); Debug("dt-enum") << " " << d_datatype.isFinite() << std::endl; - Debug("dt-enum") << " " << d_datatype.isUFinite() << std::endl; + Debug("dt-enum") << " " << d_datatype.isInterpretedFinite() << std::endl; if( d_datatype.isCodatatype() && hasCyclesDt( d_datatype ) ){ //start with uninterpreted constant diff --git a/src/theory/datatypes/type_enumerator.h b/src/theory/datatypes/type_enumerator.h index bbfd951b3..8473b5d69 100644 --- a/src/theory/datatypes/type_enumerator.h +++ b/src/theory/datatypes/type_enumerator.h @@ -159,7 +159,7 @@ public: } if( d_ctor>=d_has_debruijn+d_datatype.getNumConstructors() ){ //try next size limit as long as new terms were generated at last size, or other cases - if( prevSize==d_size_limit || ( d_size_limit==0 && d_datatype.isCodatatype() ) || ( options::finiteModelFind() ? !d_datatype.isUFinite() : !d_datatype.isFinite() ) ){ + if( prevSize==d_size_limit || ( d_size_limit==0 && d_datatype.isCodatatype() ) || !d_datatype.isInterpretedFinite() ){ d_size_limit++; d_ctor = d_zeroCtor; for( unsigned i=0; i<d_sel_sum.size(); i++ ){ diff --git a/src/theory/quantifiers/quant_split.cpp b/src/theory/quantifiers/quant_split.cpp index 9fb943e5e..5aff1a848 100644 --- a/src/theory/quantifiers/quant_split.cpp +++ b/src/theory/quantifiers/quant_split.cpp @@ -48,11 +48,11 @@ void QuantDSplit::preRegisterQuantifier( Node q ) { }else{ int score = -1; if( options::quantDynamicSplit()==quantifiers::QUANT_DSPLIT_MODE_AGG ){ - score = dt.isUFinite() ? 1 : -1; + score = dt.isInterpretedFinite() ? 1 : -1; }else if( options::quantDynamicSplit()==quantifiers::QUANT_DSPLIT_MODE_DEFAULT ){ - score = dt.isUFinite() ? 1 : -1; + score = dt.isInterpretedFinite() ? 1 : -1; } - Trace("quant-dsplit-debug") << "Datatype " << dt.getName() << " is score " << score << " (" << dt.isUFinite() << " " << dt.isFinite() << ")" << std::endl; + Trace("quant-dsplit-debug") << "Datatype " << dt.getName() << " is score " << score << " (" << dt.isInterpretedFinite() << " " << dt.isFinite() << ")" << std::endl; if( score>max_score ){ max_index = i; max_score = score; diff --git a/src/theory/term_registration_visitor.cpp b/src/theory/term_registration_visitor.cpp index 830e7f809..6b268805a 100644 --- a/src/theory/term_registration_visitor.cpp +++ b/src/theory/term_registration_visitor.cpp @@ -64,14 +64,8 @@ bool PreRegisterVisitor::alreadyVisited(TNode current, TNode parent) { TypeNode type = current.getType(); typeTheoryId = Theory::theoryOf(type); if (typeTheoryId != currentTheoryId) { - if (options::finiteModelFind() && type.isSort()) { - // We're looking for finite models + if (type.isInterpretedFinite()) { useType = true; - } else { - Cardinality card = type.getCardinality(); - if (card.isFinite()) { - useType = true; - } } } } @@ -130,14 +124,8 @@ void PreRegisterVisitor::visit(TNode current, TNode parent) { TypeNode type = current.getType(); typeTheoryId = Theory::theoryOf(type); if (typeTheoryId != currentTheoryId) { - if (options::finiteModelFind() && type.isSort()) { - // We're looking for finite models + if (type.isInterpretedFinite()) { useType = true; - } else { - Cardinality card = type.getCardinality(); - if (card.isFinite()) { - useType = true; - } } } } @@ -222,14 +210,8 @@ bool SharedTermsVisitor::alreadyVisited(TNode current, TNode parent) const { TypeNode type = current.getType(); typeTheoryId = Theory::theoryOf(type); if (typeTheoryId != currentTheoryId) { - if (options::finiteModelFind() && type.isSort()) { - // We're looking for finite models + if (type.isInterpretedFinite()) { useType = true; - } else { - Cardinality card = type.getCardinality(); - if (card.isFinite()) { - useType = true; - } } } } @@ -244,14 +226,8 @@ bool SharedTermsVisitor::alreadyVisited(TNode current, TNode parent) const { TypeNode type = current.getType(); typeTheoryId = Theory::theoryOf(type); if (typeTheoryId != currentTheoryId) { - if (options::finiteModelFind() && type.isSort()) { - // We're looking for finite models + if (type.isInterpretedFinite()) { useType = true; - } else { - Cardinality card = type.getCardinality(); - if (card.isFinite()) { - useType = true; - } } } } @@ -297,14 +273,8 @@ void SharedTermsVisitor::visit(TNode current, TNode parent) { TypeNode type = current.getType(); typeTheoryId = Theory::theoryOf(type); if (typeTheoryId != currentTheoryId) { - if (options::finiteModelFind() && type.isSort()) { - // We're looking for finite models + if (type.isInterpretedFinite()) { useType = true; - } else { - Cardinality card = type.getCardinality(); - if (card.isFinite()) { - useType = true; - } } } } diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp index fa7e497e2..6889d1002 100644 --- a/src/theory/theory_model.cpp +++ b/src/theory/theory_model.cpp @@ -832,6 +832,7 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel) Assert(!t.isBoolean() || (*i2).getKind() == kind::APPLY_UF); Node n; if (t.getCardinality().isInfinite()) { + // if (!t.isInterpretedFinite()) { bool success; do{ Trace("model-builder-debug") << "Enumerate term of type " << t << std::endl; |