From d7dadde871ae4775748695b0b7f9deee49576c0a Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 31 Aug 2017 00:59:24 +0200 Subject: [PATCH] Fix model construction for parametric types (#1059) Fix model construction for parametric types so that we enumerate types in order of dependencies, and avoid subterms of previously enumerated values. There was a bug in model construction for parametric types which was related to enumerating values that are subterms of other previously enumerated values created during model construction (which were not recorded). This commit adds all subterms of values we enumerate to the "already used value" sets of their respective types, as reflected in the changes to TypeSet. There is an extra wrinkle in making the above change, which was caught by the regression test/regress/regress0/fmf/dt-proper-model.smt2. The issue is specific to finite model finding and can be corrected by ensuring that base types (e.g. uninterpreted sorts) are enumerated first. The change to TheoryModel::buildModel that replaces "allTypes" with "type_list" fixes this wrinkle. This constructs a partially ordered list of types where T1 comes before T2 if values of T2 can contain terms of type T1 but not vice versa. Ordering our enumeration in this way is probably a good idea in general. This ensures we enumerate values for equivalence classes of e.g. Int before (Array Int Int) and means we exclude fewer intermediate values during model construction. --- src/theory/theory_model.cpp | 64 ++++++++++++++++--- src/theory/theory_model.h | 21 +++++- test/regress/regress0/datatypes/Makefile.am | 3 +- .../datatypes/model-subterms-min.smt2 | 18 ++++++ 4 files changed, 95 insertions(+), 11 deletions(-) create mode 100644 test/regress/regress0/datatypes/model-subterms-min.smt2 diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp index 0f92f976e..75bc40af7 100644 --- a/src/theory/theory_model.cpp +++ b/src/theory/theory_model.cpp @@ -581,6 +581,36 @@ bool TheoryEngineModelBuilder::isExcludedUSortValue( std::map< TypeNode, unsigne return false; } + +void TheoryEngineModelBuilder::addToTypeList( TypeNode tn, std::vector< TypeNode >& type_list, + std::map< TypeNode, bool >& visiting ){ + if( std::find( type_list.begin(), type_list.end(), tn )==type_list.end() ){ + if( visiting.find( tn )==visiting.end() ){ + visiting[tn] = true; + /* This must make a recursive call on all types that are subterms of + * values of the current type. + * Note that recursive traversal here is over enumerated expressions + * (very low expression depth). */ + if( tn.isArray() ){ + addToTypeList( tn.getArrayIndexType(), type_list, visiting ); + addToTypeList( tn.getArrayConstituentType(), type_list, visiting ); + }else if( tn.isSet() ){ + addToTypeList( tn.getSetElementType(), type_list, visiting ); + }else if( tn.isDatatype() ){ + const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype(); + for( unsigned i=0; i allTypes; + // AJR: build ordered list of types that ensures that base types are enumerated first. + // (I think) this is only strictly necessary for finite model finding + parametric types + // instantiated with uninterpreted sorts, but is probably a good idea to do in general + // since it leads to models with smaller term sizes. + std::vector< TypeNode > type_list; eqcs_i = eq::EqClassesIterator(tm->d_equalityEngine); for ( ; !eqcs_i.isFinished(); ++eqcs_i) { @@ -687,11 +721,13 @@ bool TheoryEngineModelBuilder::buildModel(Model* m) else if (!rep.isNull()) { assertedReps[eqc] = rep; typeRepSet.add(eqct.getBaseType(), eqc); - allTypes.insert(eqct.getBaseType()); + std::map< TypeNode, bool > visiting; + addToTypeList(eqct.getBaseType(), type_list, visiting); } else { typeNoRepSet.add(eqct, eqc); - allTypes.insert(eqct); + std::map< TypeNode, bool > visiting; + addToTypeList(eqct, type_list, visiting); } } @@ -700,7 +736,7 @@ bool TheoryEngineModelBuilder::buildModel(Model* m) Trace("model-builder") << "Processing EC's..." << std::endl; TypeSet::iterator it; - set::iterator type_it; + vector::iterator type_it; set::iterator i, i2; bool changed, unassignedAssignable, assignOne = false; set evaluableSet; @@ -718,7 +754,7 @@ bool TheoryEngineModelBuilder::buildModel(Model* m) evaluableSet.clear(); // Iterate over all types we've seen - for (type_it = allTypes.begin(); type_it != allTypes.end(); ++type_it) { + for (type_it = type_list.begin(); type_it != type_list.end(); ++type_it) { TypeNode t = *type_it; TypeNode tb = t.getBaseType(); set* noRepSet = typeNoRepSet.getSet(t); @@ -809,13 +845,23 @@ bool TheoryEngineModelBuilder::buildModel(Model* m) // 2. there are no terms that share teh same base type that are unevaluated evaluable terms // Alternatively, if 2 or 3 don't hold but we are in a special deadlock-breaking mode where assignOne is true, go ahead and make one assignment changed = false; - for (it = typeNoRepSet.begin(); it != typeNoRepSet.end(); ++it) { - set& noRepSet = TypeSet::getSet(it); + //must iterate over the ordered type list to ensure that we do not enumerate values with subterms + // having types that we are currently enumerating (when possible) + // for example, this ensures we enumerate uninterpreted sort U before (List of U) and (Array U U) + // however, it does not break cyclic type dependencies for mutually recursive datatypes, but this is handled + // by recording all subterms of enumerated values in TypeSet::addSubTerms. + for (type_it = type_list.begin(); type_it != type_list.end(); ++type_it) { + TypeNode t = *type_it; + // continue if there are no more equivalence classes of this type to assign + std::set* noRepSetPtr = typeNoRepSet.getSet( t ); + if( noRepSetPtr==NULL ){ + continue; + } + set& noRepSet = *noRepSetPtr; if (noRepSet.empty()) { continue; } - TypeNode t = TypeSet::getType(it); - + //get properties of this type bool isCorecursive = false; if( t.isDatatype() ){ diff --git a/src/theory/theory_model.h b/src/theory/theory_model.h index c1c57795b..6c9e706d4 100644 --- a/src/theory/theory_model.h +++ b/src/theory/theory_model.h @@ -152,7 +152,20 @@ private: TypeToTypeEnumMap d_teMap; TypeEnumeratorProperties * d_tep; - public: + /* Note that recursive traversal here is over enumerated expressions + * (very low expression depth). */ + void addSubTerms(TNode n, std::map< TNode, bool >& visited, bool topLevel=true){ + if( visited.find( n )==visited.end() ){ + visited[n] = true; + if( !topLevel ){ + add(n.getType(), n); + } + for( unsigned i=0; iinsert(n); + // add all subterms of n to this set as well + // this is necessary for parametric types whose values are constructed from other types + // to ensure that we do not enumerate subterms of other previous enumerated values + std::map< TNode, bool > visited; + addSubTerms(n, visited); ++(*te); return n; } @@ -282,6 +300,7 @@ protected: bool isAssignable(TNode n); void checkTerms(TNode n, TheoryModel* tm, NodeSet& cache); void assignConstantRep( TheoryModel* tm, Node eqc, Node const_rep ); + void addToTypeList( TypeNode tn, std::vector< TypeNode >& type_list, std::map< TypeNode, bool >& visiting ); /** is v an excluded codatatype value */ bool isExcludedCdtValue( Node v, std::set* repSet, std::map< Node, Node >& assertedReps, Node eqc ); bool isCdtValueMatch( Node v, Node r, Node eqc, Node& eqc_m ); diff --git a/test/regress/regress0/datatypes/Makefile.am b/test/regress/regress0/datatypes/Makefile.am index bdbbca706..adad0da32 100644 --- a/test/regress/regress0/datatypes/Makefile.am +++ b/test/regress/regress0/datatypes/Makefile.am @@ -82,7 +82,8 @@ TESTS = \ dt-match-pat-param-2.6.smt2 \ tuple-no-clash.cvc \ jsat-2.6.smt2 \ - acyclicity-sr-ground096.smt2 + acyclicity-sr-ground096.smt2 \ + model-subterms-min.smt2 # rec5 -- no longer support subrange types FAILING_TESTS = \ diff --git a/test/regress/regress0/datatypes/model-subterms-min.smt2 b/test/regress/regress0/datatypes/model-subterms-min.smt2 new file mode 100644 index 000000000..3866a509b --- /dev/null +++ b/test/regress/regress0/datatypes/model-subterms-min.smt2 @@ -0,0 +1,18 @@ +(set-logic ALL) +(set-info :status sat) +(declare-datatypes ((A 0) (B 0)) ( +((a (sa B))) +((e1) (e2 (se2 A))) +)) + +(declare-const x1 A) +(declare-const x2 B) + +(assert (distinct x1 (a x2))) + +(declare-const x3 A) + +(assert (distinct x2 (e2 x3))) + +(check-sat) + -- 2.30.2