diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2017-11-01 10:08:19 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2017-11-01 10:08:19 -0500 |
commit | bdcc170e1bf5bb62904c4a3ebbdc9902096799ba (patch) | |
tree | ae8e7ea4eb10d94cfdc1dac3c9d49a00e7baa0a2 /src/theory/theory_model.cpp | |
parent | 5b6551c529506592da7c66e39a911d9299944eb8 (diff) |
(Move-only) Refactor and document theory model part 2 (#1305)
* Move type set to its own file and document.
* Move theory engine model builder to its own class.
* Working on documentation.
* Document Theory Model.
* Minor
* Document theory model builder.
* Clang format
* Address review.
Diffstat (limited to 'src/theory/theory_model.cpp')
-rw-r--r-- | src/theory/theory_model.cpp | 841 |
1 files changed, 2 insertions, 839 deletions
diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp index 490ed45c9..65810109c 100644 --- a/src/theory/theory_model.cpp +++ b/src/theory/theory_model.cpp @@ -13,14 +13,10 @@ **/ #include "theory/theory_model.h" +#include "options/quantifiers_options.h" #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" -#include "theory/type_enumerator.h" -#include "theory/uf/theory_uf_model.h" using namespace std; using namespace CVC4::kind; @@ -56,6 +52,7 @@ TheoryModel::~TheoryModel() throw() { } void TheoryModel::reset(){ + d_modelBuilt = false; d_modelCache.clear(); d_comment_str.clear(); d_sep_heap = Node::null(); @@ -577,839 +574,5 @@ std::vector< Node > TheoryModel::getFunctionsToAssign() { return funcs_to_assign; } -TheoryEngineModelBuilder::TheoryEngineModelBuilder( TheoryEngine* te ) : d_te( te ){ - -} - - -bool TheoryEngineModelBuilder::isAssignable(TNode n) -{ - if( n.getKind() == kind::SELECT || n.getKind() == kind::APPLY_SELECTOR_TOTAL ){ - // selectors are always assignable (where we guarantee that they are not evaluatable here) - if( !options::ufHo() ){ - Assert( !n.getType().isFunction() ); - return true; - }else{ - // might be a function field - return !n.getType().isFunction(); - } - }else{ - // non-function variables, and fully applied functions - if( !options::ufHo() ){ - // no functions exist, all functions are fully applied - Assert( n.getKind() != kind::HO_APPLY ); - Assert( !n.getType().isFunction() ); - return n.isVar() || n.getKind() == kind::APPLY_UF; - }else{ - //Assert( n.getKind() != kind::APPLY_UF ); - return ( n.isVar() && !n.getType().isFunction() ) || n.getKind() == kind::APPLY_UF || - ( n.getKind() == kind::HO_APPLY && n[0].getType().getNumChildren()==2 ); - } - } -} - - -void TheoryEngineModelBuilder::checkTerms(TNode n, TheoryModel* tm, NodeSet& cache) -{ - if (n.getKind()==FORALL || n.getKind()==EXISTS) { - return; - } - if (cache.find(n) != cache.end()) { - return; - } - if (isAssignable(n)) { - tm->d_equalityEngine->addTerm(n); - } - for(TNode::iterator child_it = n.begin(); child_it != n.end(); ++child_it) { - checkTerms(*child_it, tm, cache); - } - cache.insert(n); -} - -void TheoryEngineModelBuilder::assignConstantRep( TheoryModel* tm, Node eqc, Node const_rep ) { - d_constantReps[eqc] = const_rep; - Trace("model-builder") << " Assign: Setting constant rep of " << eqc << " to " << const_rep << endl; - tm->d_rep_set.setTermForRepresentative(const_rep, eqc); -} - -bool TheoryEngineModelBuilder::isExcludedCdtValue( Node val, std::set<Node>* repSet, std::map< Node, Node >& assertedReps, Node eqc ) { - Trace("model-builder-debug") << "Is " << val << " and excluded codatatype value for " << eqc << "? " << std::endl; - for (set<Node>::iterator i = repSet->begin(); i != repSet->end(); ++i ) { - Assert(assertedReps.find(*i) != assertedReps.end()); - Node rep = assertedReps[*i]; - Trace("model-builder-debug") << " Rep : " << rep << std::endl; - //check matching val to rep with eqc as a free variable - Node eqc_m; - if( isCdtValueMatch( val, rep, eqc, eqc_m ) ){ - Trace("model-builder-debug") << " ...matches with " << eqc << " -> " << eqc_m << std::endl; - if( eqc_m.getKind()==kind::UNINTERPRETED_CONSTANT ){ - Trace("model-builder-debug") << "*** " << val << " is excluded datatype for " << eqc << std::endl; - return true; - } - } - } - return false; -} - -bool TheoryEngineModelBuilder::isCdtValueMatch( Node v, Node r, Node eqc, Node& eqc_m ) { - if( r==v ){ - return true; - }else if( r==eqc ){ - if( eqc_m.isNull() ){ - //only if an uninterpreted constant? - eqc_m = v; - return true; - }else{ - return v==eqc_m; - } - }else if( v.getKind()==kind::APPLY_CONSTRUCTOR && r.getKind()==kind::APPLY_CONSTRUCTOR ){ - if( v.getOperator()==r.getOperator() ){ - for( unsigned i=0; i<v.getNumChildren(); i++ ){ - if( !isCdtValueMatch( v[i], r[i], eqc, eqc_m ) ){ - return false; - } - } - return true; - } - } - 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("model-builder-debug") << "Is excluded usort value : " << v << " " << tn << std::endl; - unsigned card = eqc_usort_count[tn]; - Trace("model-builder-debug") << " Cardinality is " << card << std::endl; - unsigned index = v.getConst<UninterpretedConstant>().getIndex().toUnsignedInt(); - Trace("model-builder-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::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<dt.getNumConstructors(); i++ ){ - for( unsigned j=0; j<dt[i].getNumArgs(); j++ ){ - TypeNode ctn = TypeNode::fromType( dt[i][j].getRangeType() ); - addToTypeList( ctn, type_list, visiting ); - } - } - } - Assert( std::find( type_list.begin(), type_list.end(), tn )==type_list.end() ); - type_list.push_back( tn ); - } - } -} - -bool TheoryEngineModelBuilder::buildModel(Model* m) -{ - Trace("model-builder") << "TheoryEngineModelBuilder: buildModel" << std::endl; - TheoryModel* tm = (TheoryModel*)m; - - // buildModel should only be called once per check - Assert(!tm->isBuilt()); - tm->d_modelBuilt = true; - - // Reset model - tm->reset(); - - // Collect model info from the theories - Trace("model-builder") << "TheoryEngineModelBuilder: Collect model info..." << std::endl; - d_te->collectModelInfo(tm); - - // model-builder specific initialization - if( !preProcessBuildModel(tm) ){ - return false; - } - - // 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; - for ( ; !eqcs_i.isFinished(); ++eqcs_i) { - eq::EqClassIterator eqc_i = eq::EqClassIterator((*eqcs_i),tm->d_equalityEngine); - 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]++; - } - } - } - } - - Trace("model-builder") << "Collect representatives..." << std::endl; - - // Process all terms in the equality engine, store representatives for each EC - d_constantReps.clear(); - std::map< Node, Node > assertedReps; - 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 ){ - Trace("model-builder") << "Fixed bound (#eqc) for " << it->first << " : " << it->second << std::endl; - tep.d_fixed_card[it->first] = Integer(it->second); - } - typeConstSet.setTypeEnumeratorProperties( &tep ); - } - // 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) { - - // eqc is the equivalence class representative - Node eqc = (*eqcs_i); - Trace("model-builder") << "Processing EC: " << eqc << endl; - Assert(tm->d_equalityEngine->getRepresentative(eqc) == eqc); - TypeNode eqct = eqc.getType(); - Assert(assertedReps.find(eqc) == assertedReps.end()); - Assert(d_constantReps.find(eqc) == d_constantReps.end()); - - // Loop through terms in this EC - Node rep, const_rep; - eq::EqClassIterator eqc_i = eq::EqClassIterator(eqc, tm->d_equalityEngine); - for ( ; !eqc_i.isFinished(); ++eqc_i) { - Node n = *eqc_i; - Trace("model-builder") << " Processing Term: " << n << endl; - // Record as rep if this node was specified as a representative - if (tm->d_reps.find(n) != tm->d_reps.end()){ - //AJR: I believe this assertion is too strict, - // e.g. datatypes may assert representative for two constructor terms that are not in the care graph and are merged during collectModelInfo. - //Assert(rep.isNull()); - rep = tm->d_reps[n]; - Assert(!rep.isNull() ); - Trace("model-builder") << " Rep( " << eqc << " ) = " << rep << std::endl; - } - // Record as const_rep if this node is constant - if (n.isConst()) { - Assert(const_rep.isNull()); - const_rep = n; - Trace("model-builder") << " ConstRep( " << eqc << " ) = " << const_rep << std::endl; - } - //model-specific processing of the term - tm->addTerm(n); - } - - // Assign representative for this EC - if (!const_rep.isNull()) { - // Theories should not specify a rep if there is already a constant in the EC - //AJR: I believe this assertion is too strict, eqc with asserted reps may merge with constant eqc - //Assert(rep.isNull() || rep == const_rep); - assignConstantRep( tm, eqc, const_rep ); - typeConstSet.add(eqct.getBaseType(), const_rep); - } - else if (!rep.isNull()) { - assertedReps[eqc] = rep; - typeRepSet.add(eqct.getBaseType(), eqc); - std::map< TypeNode, bool > visiting; - addToTypeList(eqct.getBaseType(), type_list, visiting); - } - else { - typeNoRepSet.add(eqct, eqc); - std::map< TypeNode, bool > visiting; - addToTypeList(eqct, type_list, visiting); - } - } - - // Need to ensure that each EC has a constant representative. - - Trace("model-builder") << "Processing EC's..." << std::endl; - - TypeSet::iterator it; - vector<TypeNode>::iterator type_it; - set<Node>::iterator i, i2; - bool changed, unassignedAssignable, assignOne = false; - set<TypeNode> evaluableSet; - - // Double-fixed-point loop - // Outer loop handles a special corner case (see code at end of loop for details) - for (;;) { - - // Inner fixed-point loop: we are trying to learn constant values for every EC. Each time through this loop, we process all of the - // types by type and may learn some new EC values. EC's in one type may depend on EC's in another type, so we need a fixed-point loop - // to ensure that we learn as many EC values as possible - do { - changed = false; - unassignedAssignable = false; - evaluableSet.clear(); - - // Iterate over all types we've seen - for (type_it = type_list.begin(); type_it != type_list.end(); ++type_it) { - TypeNode t = *type_it; - TypeNode tb = t.getBaseType(); - set<Node>* noRepSet = typeNoRepSet.getSet(t); - - // 1. Try to evaluate the EC's in this type - if (noRepSet != NULL && !noRepSet->empty()) { - Trace("model-builder") << " Eval phase, working on type: " << t << endl; - bool assignable, evaluable, evaluated; - d_normalizedCache.clear(); - for (i = noRepSet->begin(); i != noRepSet->end(); ) { - i2 = i; - ++i; - assignable = false; - evaluable = false; - evaluated = false; - Trace("model-builder-debug") << "Look at eqc : " << (*i2) << std::endl; - eq::EqClassIterator eqc_i = eq::EqClassIterator(*i2, tm->d_equalityEngine); - for ( ; !eqc_i.isFinished(); ++eqc_i) { - Node n = *eqc_i; - Trace("model-builder-debug") << "Look at term : " << n << std::endl; - if (isAssignable(n)) { - assignable = true; - Trace("model-builder-debug") << "...assignable" << std::endl; - } - else { - evaluable = true; - Trace("model-builder-debug") << "...try to normalize" << std::endl; - Node normalized = normalize(tm, n, true); - if (normalized.isConst()) { - typeConstSet.add(tb, normalized); - assignConstantRep( tm, *i2, normalized); - Trace("model-builder") << " Eval: Setting constant rep of " << (*i2) << " to " << normalized << endl; - changed = true; - evaluated = true; - noRepSet->erase(i2); - break; - } - } - } - if (!evaluated) { - if (evaluable) { - evaluableSet.insert(tb); - } - if (assignable) { - unassignedAssignable = true; - } - } - } - } - - // 2. Normalize any non-const representative terms for this type - set<Node>* repSet = typeRepSet.getSet(t); - if (repSet != NULL && !repSet->empty()) { - Trace("model-builder") << " Normalization phase, working on type: " << t << endl; - d_normalizedCache.clear(); - for (i = repSet->begin(); i != repSet->end(); ) { - Assert(assertedReps.find(*i) != assertedReps.end()); - Node rep = assertedReps[*i]; - Node normalized = normalize(tm, rep, false); - Trace("model-builder") << " Normalizing rep (" << rep << "), normalized to (" << normalized << ")" << endl; - if (normalized.isConst()) { - changed = true; - typeConstSet.add(tb, normalized); - assignConstantRep( tm, *i, normalized); - assertedReps.erase(*i); - i2 = i; - ++i; - repSet->erase(i2); - } - else { - if (normalized != rep) { - assertedReps[*i] = normalized; - changed = true; - } - ++i; - } - } - } - } - } while (changed); - - if (!unassignedAssignable) { - break; - } - - // 3. Assign unassigned assignable EC's using type enumeration - assign a value *different* from all other EC's if the type is infinite - // Assign first value from type enumerator otherwise - for finite types, we rely on polite framework to ensure that EC's that have to be - // different are different. - - // Only make assignments on a type if: - // 1. there are no terms that share the same base type with un-normalized representatives - // 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; - //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<Node>* noRepSetPtr = typeNoRepSet.getSet( t ); - if( noRepSetPtr==NULL ){ - continue; - } - set<Node>& noRepSet = *noRepSetPtr; - if (noRepSet.empty()) { - continue; - } - - //get properties of this type - bool isCorecursive = false; - if( t.isDatatype() ){ - const Datatype& dt = ((DatatypeType)(t).toType()).getDatatype(); - isCorecursive = dt.isCodatatype() && ( !dt.isFinite( t.toType() ) || dt.isRecursiveSingleton( t.toType() ) ); - } -#ifdef CVC4_ASSERTIONS - bool isUSortFiniteRestricted = false; - if( options::finiteModelFind() ){ - isUSortFiniteRestricted = !t.isSort() && involvesUSort( t ); - } -#endif - - set<Node>* repSet = typeRepSet.getSet(t); - TypeNode tb = t.getBaseType(); - if (!assignOne) { - set<Node>* repSet = typeRepSet.getSet(tb); - if (repSet != NULL && !repSet->empty()) { - continue; - } - if (evaluableSet.find(tb) != evaluableSet.end()) { - continue; - } - } - Trace("model-builder") << " Assign phase, working on type: " << t << endl; - bool assignable, evaluable CVC4_UNUSED; - for (i = noRepSet.begin(); i != noRepSet.end(); ) { - i2 = i; - ++i; - eq::EqClassIterator eqc_i = eq::EqClassIterator(*i2, tm->d_equalityEngine); - assignable = false; - evaluable = false; - for ( ; !eqc_i.isFinished(); ++eqc_i) { - Node n = *eqc_i; - if (isAssignable(n)) { - assignable = true; - } - else { - evaluable = true; - } - } - Trace("model-builder-debug") << " eqc " << *i2 << " is assignable=" << assignable << ", evaluable=" << evaluable << std::endl; - if (assignable) { - Assert(!evaluable || assignOne); - 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; - n = typeConstSet.nextTypeEnum(t, true); - //--- AJR: this code checks whether n is a legal value - Assert( !n.isNull() ); - success = true; - Trace("model-builder-debug") << "Check if excluded : " << n << std::endl; -#ifdef CVC4_ASSERTIONS - if( isUSortFiniteRestricted ){ - //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("model-builder") << "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()) { - // 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("model-builder") << "Excluded value : " << n << " due to alpha-equivalent codatatype expression." << std::endl; - } - } - } - //--- - }while( !success ); - } - else { - TypeEnumerator te(t); - n = *te; - } - Assert(!n.isNull()); - assignConstantRep( tm, *i2, n); - changed = true; - noRepSet.erase(i2); - if (assignOne) { - assignOne = false; - break; - } - } - } - } - - // Corner case - I'm not sure this can even happen - but it's theoretically possible to have a cyclical dependency - // in EC assignment/evaluation, e.g. EC1 = {a, b + 1}; EC2 = {b, a - 1}. In this case, neither one will get assigned because we are waiting - // to be able to evaluate. But we will never be able to evaluate because the variables that need to be assigned are in - // these same EC's. In this case, repeat the whole fixed-point computation with the difference that the first EC - // that has both assignable and evaluable expressions will get assigned. - if (!changed) { - Assert(!assignOne); // check for infinite loop! - assignOne = true; - } - } - -#ifdef CVC4_ASSERTIONS - // Assert that all representatives have been converted to constants - for (it = typeRepSet.begin(); it != typeRepSet.end(); ++it) { - set<Node>& repSet = TypeSet::getSet(it); - if (!repSet.empty()) { - Trace("model-builder") << "***Non-empty repSet, size = " << repSet.size() << ", first = " << *(repSet.begin()) << endl; - Assert(false); - } - } -#endif /* CVC4_ASSERTIONS */ - - Trace("model-builder") << "Copy representatives to model..." << std::endl; - tm->d_reps.clear(); - std::map< Node, Node >::iterator itMap; - for (itMap = d_constantReps.begin(); itMap != d_constantReps.end(); ++itMap) { - tm->d_reps[itMap->first] = itMap->second; - tm->d_rep_set.add(itMap->second.getType(), itMap->second); - } - - Trace("model-builder") << "Make sure ECs have reps..." << std::endl; - // Make sure every EC has a rep - for (itMap = assertedReps.begin(); itMap != assertedReps.end(); ++itMap ) { - tm->d_reps[itMap->first] = itMap->second; - tm->d_rep_set.add(itMap->second.getType(), itMap->second); - } - for (it = typeNoRepSet.begin(); it != typeNoRepSet.end(); ++it) { - set<Node>& noRepSet = TypeSet::getSet(it); - set<Node>::iterator i; - for (i = noRepSet.begin(); i != noRepSet.end(); ++i) { - tm->d_reps[*i] = *i; - tm->d_rep_set.add((*i).getType(), *i); - } - } - - //modelBuilder-specific initialization - if( !processBuildModel( tm ) ){ - return false; - }else{ - return true; - } -} - -void TheoryEngineModelBuilder::debugCheckModel(Model* m){ - TheoryModel* tm = (TheoryModel*)m; -#ifdef CVC4_ASSERTIONS - Assert(tm->isBuilt()); - eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( tm->d_equalityEngine ); - std::map< Node, Node >::iterator itMap; - // Check that every term evaluates to its representative in the model - for (eqcs_i = eq::EqClassesIterator(tm->d_equalityEngine); !eqcs_i.isFinished(); ++eqcs_i) { - // eqc is the equivalence class representative - Node eqc = (*eqcs_i); - // get the representative - Node rep = tm->getRepresentative( eqc ); - if( !rep.isConst() && eqc.getType().isBoolean() ){ - // if Boolean, it does not necessarily have a constant representative, use get value instead - rep = tm->getValue(eqc); - Assert(rep.isConst()); - } - eq::EqClassIterator eqc_i = eq::EqClassIterator(eqc, tm->d_equalityEngine); - for ( ; !eqc_i.isFinished(); ++eqc_i) { - Node n = *eqc_i; - static int repCheckInstance = 0; - ++repCheckInstance; - - // non-linear mult is not necessarily accurate wrt getValue - if( n.getKind()!=kind::NONLINEAR_MULT ){ - Debug("check-model::rep-checking") - << "( " << repCheckInstance <<") " - << "n: " << n << endl - << "getValue(n): " << tm->getValue(n) << endl - << "rep: " << rep << endl; - Assert(tm->getValue(*eqc_i) == rep, "run with -d check-model::rep-checking for details"); - } - } - } -#endif /* CVC4_ASSERTIONS */ - - // builder-specific debugging - debugModel( tm ); -} - -Node TheoryEngineModelBuilder::normalize(TheoryModel* m, TNode r, bool evalOnly) -{ - std::map<Node, Node>::iterator itMap = d_constantReps.find(r); - if (itMap != d_constantReps.end()) { - return (*itMap).second; - } - NodeMap::iterator it = d_normalizedCache.find(r); - if (it != d_normalizedCache.end()) { - return (*it).second; - } - Trace("model-builder-debug") << "do normalize on " << r << std::endl; - Node retNode = r; - if (r.getNumChildren() > 0) { - std::vector<Node> children; - if (r.getMetaKind() == kind::metakind::PARAMETERIZED) { - children.push_back(r.getOperator()); - } - bool childrenConst = true; - for (size_t i=0; i < r.getNumChildren(); ++i) { - Node ri = r[i]; - bool recurse = true; - if (!ri.isConst()) { - if (m->d_equalityEngine->hasTerm(ri)) { - itMap = d_constantReps.find(m->d_equalityEngine->getRepresentative(ri)); - if (itMap != d_constantReps.end()) { - ri = (*itMap).second; - recurse = false; - } - else if (!evalOnly) { - recurse = false; - } - } - if (recurse) { - ri = normalize(m, ri, evalOnly); - } - if (!ri.isConst()) { - childrenConst = false; - } - } - children.push_back(ri); - } - retNode = NodeManager::currentNM()->mkNode( r.getKind(), children ); - if (childrenConst) { - retNode = Rewriter::rewrite(retNode); - Assert(retNode.getKind() == kind::APPLY_UF - || !retNode.getType().isFirstClass() - || retNode.isConst()); - } - } - d_normalizedCache[r] = retNode; - return retNode; -} - -bool TheoryEngineModelBuilder::preProcessBuildModel(TheoryModel* m) { - return true; -} - -bool TheoryEngineModelBuilder::processBuildModel(TheoryModel* m){ - assignFunctions(m); - return true; -} - -void TheoryEngineModelBuilder::assignFunction(TheoryModel* m, Node f) { - Assert( !options::ufHo() ); - uf::UfModelTree ufmt( f ); - Node default_v; - for( size_t i=0; i<m->d_uf_terms[f].size(); i++ ){ - Node un = m->d_uf_terms[f][i]; - vector<TNode> children; - children.push_back(f); - Trace("model-builder-debug") << " process term : " << un << std::endl; - for (size_t j = 0; j < un.getNumChildren(); ++j) { - Node rc = m->getRepresentative(un[j]); - Trace("model-builder-debug2") << " get rep : " << un[j] << " returned " << rc << std::endl; - Assert( rc.isConst() ); - children.push_back(rc); - } - Node simp = NodeManager::currentNM()->mkNode(un.getKind(), children); - Node v = m->getRepresentative(un); - Trace("model-builder") << " Setting (" << simp << ") to (" << v << ")" << endl; - ufmt.setValue(m, simp, v); - default_v = v; - } - if( default_v.isNull() ){ - //choose default value from model if none exists - TypeEnumerator te(f.getType().getRangeType()); - default_v = (*te); - } - ufmt.setDefaultValue( m, default_v ); - bool condenseFuncValues = options::condenseFunctionValues(); - if(condenseFuncValues) { - ufmt.simplify(); - } - std::stringstream ss; - ss << "_arg_" << f << "_"; - Node val = ufmt.getFunctionValue( ss.str().c_str(), condenseFuncValues ); - m->assignFunctionDefinition( f, val ); - //ufmt.debugPrint( std::cout, m ); -} - -void TheoryEngineModelBuilder::assignHoFunction(TheoryModel* m, Node f) { - Assert( options::ufHo() ); - TypeNode type = f.getType(); - std::vector< TypeNode > argTypes = type.getArgTypes(); - std::vector< Node > args; - std::vector< TNode > apply_args; - for( unsigned i=0; i<argTypes.size(); i++ ){ - Node v = NodeManager::currentNM()->mkBoundVar( argTypes[i] ); - args.push_back( v ); - if( i>0 ){ - apply_args.push_back( v ); - } - } - //start with the base return value (currently we use the same default value for all functions) - TypeEnumerator te(type.getRangeType()); - Node curr = (*te); - std::map< Node, std::vector< Node > >::iterator itht = m->d_ho_uf_terms.find( f ); - if( itht!=m->d_ho_uf_terms.end() ){ - for( size_t i=0; i<itht->second.size(); i++ ){ - Node hn = itht->second[i]; - Trace("model-builder-debug") << " process : " << hn << std::endl; - Assert( hn.getKind()==kind::HO_APPLY ); - Assert( m->areEqual( hn[0], f ) ); - Node hni = m->getRepresentative(hn[1]); - Trace("model-builder-debug2") << " get rep : " << hn[0] << " returned " << hni << std::endl; - Assert( hni.isConst() ); - Assert( hni.getType().isSubtypeOf( args[0].getType() ) ); - hni = Rewriter::rewrite( args[0].eqNode( hni ) ); - Node hnv = m->getRepresentative(hn); - Trace("model-builder-debug2") << " get rep val : " << hn << " returned " << hnv << std::endl; - Assert( hnv.isConst() ); - if( !apply_args.empty() ){ - Assert( hnv.getKind()==kind::LAMBDA && hnv[0].getNumChildren()+1==args.size() ); - std::vector< TNode > largs; - for( unsigned j=0; j<hnv[0].getNumChildren(); j++ ){ - largs.push_back( hnv[0][j] ); - } - Assert( largs.size()==apply_args.size() ); - hnv = hnv[1].substitute( largs.begin(), largs.end(), apply_args.begin(), apply_args.end() ); - hnv = Rewriter::rewrite( hnv ); - } - Assert( !TypeNode::leastCommonTypeNode( hnv.getType(), curr.getType() ).isNull() ); - curr = NodeManager::currentNM()->mkNode( kind::ITE, hni, hnv, curr ); - } - } - Node val = NodeManager::currentNM()->mkNode( kind::LAMBDA, - NodeManager::currentNM()->mkNode( kind::BOUND_VAR_LIST, args ), curr ); - m->assignFunctionDefinition( f, val ); -} - -// This struct is used to sort terms by the "size" of their type -// The size of the type is the number of nodes in the type, for example -// size of Int is 1 -// size of Function( Int, Int ) is 3 -// size of Function( Function( Bool, Int ), Int ) is 5 -struct sortTypeSize { - // stores the size of the type - std::map< TypeNode, unsigned > d_type_size; - // get the size of type tn - unsigned getTypeSize( TypeNode tn ) { - std::map< TypeNode, unsigned >::iterator it = d_type_size.find( tn ); - if( it!=d_type_size.end() ){ - return it->second; - }else{ - unsigned sum = 1; - for( unsigned i=0; i<tn.getNumChildren(); i++ ){ - sum += getTypeSize( tn[i] ); - } - d_type_size[tn] = sum; - return sum; - } - } -public: - // compares the type size of i and j - // returns true iff the size of i is less than that of j - // tiebreaks are determined by node value - bool operator() (Node i, Node j) { - int si = getTypeSize( i.getType() ); - int sj = getTypeSize( j.getType() ); - if( si<sj ){ - return true; - }else if( si==sj ){ - return i<j; - }else{ - return false; - } - } -}; - -void TheoryEngineModelBuilder::assignFunctions(TheoryModel* m) { - Trace("model-builder") << "Assigning function values..." << std::endl; - std::vector< Node > funcs_to_assign = m->getFunctionsToAssign(); - - if( options::ufHo() ){ - // sort based on type size if higher-order - Trace("model-builder") << "Sort functions by type..." << std::endl; - sortTypeSize sts; - std::sort( funcs_to_assign.begin(), funcs_to_assign.end(), sts ); - } - - if( Trace.isOn("model-builder") ){ - Trace("model-builder") << "...have " << funcs_to_assign.size() << " functions to assign:" << std::endl; - for( unsigned k=0; k<funcs_to_assign.size(); k++ ){ - Node f = funcs_to_assign[k]; - Trace("model-builder") << " [" << k << "] : " << f << " : " << f.getType() << std::endl; - } - } - - // construct function values - for( unsigned k=0; k<funcs_to_assign.size(); k++ ){ - Node f = funcs_to_assign[k]; - Trace("model-builder") << " Function #" << k << " is " << f << std::endl; - //std::map< Node, std::vector< Node > >::iterator itht = m->d_ho_uf_terms.find( f ); - if( !options::ufHo() ){ - Trace("model-builder") << " Assign function value for " << f << " based on APPLY_UF" << std::endl; - assignFunction( m, f ); - }else{ - Trace("model-builder") << " Assign function value for " << f << " based on curried HO_APPLY" << std::endl; - assignHoFunction( m, f ); - } - } - Trace("model-builder") << "Finished assigning function values." << std::endl; -} - } /* namespace CVC4::theory */ } /* namespace CVC4 */ |