diff options
-rw-r--r-- | src/theory/theory_model.cpp | 68 | ||||
-rw-r--r-- | src/theory/theory_model.h | 3 | ||||
-rw-r--r-- | test/regress/regress0/fmf/Makefile.am | 8 | ||||
-rwxr-xr-x | test/regress/regress0/fmf/dt-proper-model.smt2 | 16 |
4 files changed, 91 insertions, 4 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(){} diff --git a/test/regress/regress0/fmf/Makefile.am b/test/regress/regress0/fmf/Makefile.am index bca9f2e4f..5abadbcb8 100644 --- a/test/regress/regress0/fmf/Makefile.am +++ b/test/regress/regress0/fmf/Makefile.am @@ -20,7 +20,6 @@ MAKEFLAGS = -k # put it below in "TESTS +=" TESTS = \ array_card.smt2 \ - agree466.smt2 \ ALG008-1.smt2 \ german169.smt2 \ QEpres-uf.855035.smt \ @@ -43,7 +42,8 @@ TESTS = \ syn002-si-real-int.smt2 \ krs-sat.smt2 \ forall_unit_data2.smt2 \ - sc_bad_model_1221.smt2 + sc_bad_model_1221.smt2 \ + dt-proper-model.smt2 EXTRA_DIST = $(TESTS) @@ -54,11 +54,13 @@ EXTRA_DIST = $(TESTS) #TESTS += \ # error.cvc #endif -# +# # and make sure to distribute it #EXTRA_DIST += \ # error.cvc +# agree466.smt2 timeout after commit on 1/14 due to Array+FMF model construction + # synonyms for "check" in this directory .PHONY: regress regress0 test regress regress0 test: check diff --git a/test/regress/regress0/fmf/dt-proper-model.smt2 b/test/regress/regress0/fmf/dt-proper-model.smt2 new file mode 100755 index 000000000..60a0b6377 --- /dev/null +++ b/test/regress/regress0/fmf/dt-proper-model.smt2 @@ -0,0 +1,16 @@ +; COMMAND-LINE: --finite-model-find +; EXPECT: sat +(set-logic ALL_SUPPORTED) +(set-info :status sat) +(declare-sort U 0) +(declare-datatypes () ((D (cons (x Int) (y U))))) +(declare-fun d1 () D) +(declare-fun d2 () D) +(declare-fun d3 () D) +(declare-fun d4 () D) +(assert (distinct d1 d2 d3 d4)) +(assert (forall ((x U) (y U)) (= x y))) +(declare-fun a () U) +(declare-fun P (U) Bool) +(assert (P a)) +(check-sat)
\ No newline at end of file |