diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-01-15 00:18:49 +0100 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-01-15 00:18:49 +0100 |
commit | 081351e87edeb52facba0d0abc2e933433480444 (patch) | |
tree | 8d0192c895c4103877e12673c0927d25e53a3db3 /src | |
parent | 94fe6a0d525bff3cdd4450b2abd04eb2cb044308 (diff) |
Ensure model construction for parametric sorts involving uninterpreted sorts respect cardinality bounds on when finite model finding is enabled.
Diffstat (limited to 'src')
-rw-r--r-- | src/theory/theory_model.cpp | 68 | ||||
-rw-r--r-- | src/theory/theory_model.h | 3 |
2 files changed, 70 insertions, 1 deletions
diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp index fb5fb0f0c..c6837ddf4 100644 --- a/src/theory/theory_model.cpp +++ b/src/theory/theory_model.cpp @@ -15,6 +15,7 @@ #include "options/smt_options.h" #include "options/uf_options.h" +#include "options/quantifiers_options.h" #include "smt/smt_engine.h" #include "theory/quantifiers_engine.h" #include "theory/theory_engine.h" @@ -506,6 +507,43 @@ bool TheoryEngineModelBuilder::isCdtValueMatch( Node v, Node r, Node eqc, Node& return false; } +bool TheoryEngineModelBuilder::involvesUSort( TypeNode tn ) { + if( tn.isSort() ){ + return true; + }else if( tn.isArray() ){ + return involvesUSort( tn.getArrayIndexType() ) || involvesUSort( tn.getArrayConstituentType() ); + }else if( tn.isSet() ){ + return involvesUSort( tn.getSetElementType() ); + }else if( tn.isDatatype() ){ + const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype(); + return dt.involvesUninterpretedType(); + }else{ + return false; + } +} + +bool TheoryEngineModelBuilder::isExcludedUSortValue( std::map< TypeNode, unsigned >& eqc_usort_count, Node v, std::map< Node, bool >& visited ) { + Assert( v.isConst() ); + if( visited.find( v )==visited.end() ){ + visited[v] = true; + TypeNode tn = v.getType(); + if( tn.isSort() ){ + Trace("exc-value-debug") << "Is excluded usort value : " << v << " " << tn << std::endl; + unsigned card = eqc_usort_count[tn]; + Trace("exc-value-debug") << " Cardinality is " << card << std::endl; + unsigned index = v.getConst<UninterpretedConstant>().getIndex().toUnsignedInt(); + Trace("exc-value-debug") << " Index is " << index << std::endl; + return index>0 && index>=card; + } + for( unsigned i=0; i<v.getNumChildren(); i++ ){ + if( isExcludedUSortValue( eqc_usort_count, v[i], visited ) ){ + return true; + } + } + } + return false; +} + void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel) { Trace("model-builder") << "TheoryEngineModelBuilder: buildModel, fullModel = " << fullModel << std::endl; @@ -523,6 +561,8 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel) d_te->collectModelInfo(tm, fullModel); // Loop through all terms and make sure that assignable sub-terms are in the equality engine + // Also, record #eqc per type (for finite model finding) + std::map< TypeNode, unsigned > eqc_usort_count; eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( tm->d_equalityEngine ); { NodeSet cache; @@ -531,6 +571,14 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel) for ( ; !eqc_i.isFinished(); ++eqc_i) { checkTerms(*eqc_i, tm, cache); } + TypeNode tn = (*eqcs_i).getType(); + if( tn.isSort() ){ + if( eqc_usort_count.find( tn )==eqc_usort_count.end() ){ + eqc_usort_count[tn] = 1; + }else{ + eqc_usort_count[tn]++; + } + } } } @@ -715,11 +763,16 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel) if(t.isTuple() || t.isRecord()) { t = NodeManager::currentNM()->getDatatypeForTupleRecord(t); } + //get properties of this type bool isCorecursive = false; + bool isUSortFiniteRestricted = false; if( t.isDatatype() ){ const Datatype& dt = ((DatatypeType)(t).toType()).getDatatype(); isCorecursive = dt.isCodatatype() && ( !dt.isFinite() || dt.isRecursiveSingleton() ); } + if( options::finiteModelFind() ){ + isUSortFiniteRestricted = !t.isSort() && involvesUSort( t ); + } set<Node>* repSet = typeRepSet.getSet(t); TypeNode tb = t.getBaseType(); if (!assignOne) { @@ -756,14 +809,27 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel) bool success; do{ n = typeConstSet.nextTypeEnum(t, true); + //--- AJR: this code checks whether n is a legal value success = true; - if( isCorecursive ){ + if( isUSortFiniteRestricted ){ + //must not involve uninterpreted constants beyond cardinality bound (which assumed to coincide with #eqc) + 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; + } + } + if( success && isCorecursive ){ if (repSet != NULL && !repSet->empty()) { // in the case of codatatypes, check if it is in the set of values that we cannot assign // this will check whether n \not\in V^x_I from page 9 of Reynolds/Blanchette CADE 2015 success = !isExcludedCdtValue( n, repSet, assertedReps, *i2 ); + if( !success ){ + Trace("exc-value") << "Excluded value : " << n << " due to alpha-equivalent codatatype expression." << std::endl; + } } } + //--- }while( !success ); } else { diff --git a/src/theory/theory_model.h b/src/theory/theory_model.h index fb2c3cd01..8ee4e843d 100644 --- a/src/theory/theory_model.h +++ b/src/theory/theory_model.h @@ -260,6 +260,9 @@ protected: /** is v an excluded codatatype value */ bool isExcludedCdtValue( Node v, std::set<Node>* repSet, std::map< Node, Node >& assertedReps, Node eqc ); bool isCdtValueMatch( Node v, Node r, Node eqc, Node& eqc_m ); + /** involves usort */ + bool involvesUSort( TypeNode tn ); + bool isExcludedUSortValue( std::map< TypeNode, unsigned >& eqc_usort_count, Node v, std::map< Node, bool >& visited ); public: TheoryEngineModelBuilder(TheoryEngine* te); virtual ~TheoryEngineModelBuilder(){} |