From: Andrew Reynolds Date: Wed, 1 Nov 2017 15:08:19 +0000 (-0500) Subject: (Move-only) Refactor and document theory model part 2 (#1305) X-Git-Tag: cvc5-1.0.0~5519 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=bdcc170e1bf5bb62904c4a3ebbdc9902096799ba;p=cvc5.git (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. --- diff --git a/src/Makefile.am b/src/Makefile.am index 3648e824b..d370a73bc 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -175,9 +175,13 @@ libcvc4_la_SOURCES = \ theory/theory_engine.h \ theory/theory_model.cpp \ theory/theory_model.h \ + theory/theory_model_builder.cpp \ + theory/theory_model_builder.h \ theory/theory_registrar.h \ theory/theory_test_utils.h \ theory/type_enumerator.h \ + theory/type_set.cpp \ + theory/type_set.h \ theory/unconstrained_simplifier.cpp \ theory/unconstrained_simplifier.h \ theory/valuation.cpp \ diff --git a/src/theory/quantifiers/model_builder.h b/src/theory/quantifiers/model_builder.h index 2900320bb..2dc561074 100644 --- a/src/theory/quantifiers/model_builder.h +++ b/src/theory/quantifiers/model_builder.h @@ -18,7 +18,7 @@ #define __CVC4__THEORY__QUANTIFIERS__MODEL_BUILDER_H #include "theory/quantifiers_engine.h" -#include "theory/theory_model.h" +#include "theory/theory_model_builder.h" #include "theory/uf/theory_uf_model.h" namespace CVC4 { diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 402ba61ff..6c49f2914 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -596,7 +596,7 @@ void TheoryEngine::check(Theory::Effort effort) { printAssertions("theory::assertions-model"); } //checks for theories requiring the model go at last call - d_curr_model->setNeedsBuild(); + d_curr_model->reset(); for (TheoryId theoryId = THEORY_FIRST; theoryId < THEORY_LAST; ++theoryId) { if( theoryId!=THEORY_QUANTIFIERS ){ Theory* theory = d_theoryTable[theoryId]; 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* repSet, std::map< Node, Node >& assertedReps, Node eqc ) { - Trace("model-builder-debug") << "Is " << val << " and excluded codatatype value for " << eqc << "? " << std::endl; - for (set::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& 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().getIndex().toUnsignedInt(); - Trace("model-builder-debug") << " Index is " << index << std::endl; - return index>0 && index>=card; - } - for( unsigned i=0; i& 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; iisBuilt()); - 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::iterator type_it; - set::iterator i, i2; - bool changed, unassignedAssignable, assignOne = false; - set 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* 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* 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* noRepSetPtr = typeNoRepSet.getSet( t ); - if( noRepSetPtr==NULL ){ - continue; - } - set& 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* repSet = typeRepSet.getSet(t); - TypeNode tb = t.getBaseType(); - if (!assignOne) { - set* 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& 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& noRepSet = TypeSet::getSet(it); - set::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::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 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; id_uf_terms[f].size(); i++ ){ - Node un = m->d_uf_terms[f][i]; - vector 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; imkBoundVar( 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; isecond.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; jmkNode( 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 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 >::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 */ diff --git a/src/theory/theory_model.h b/src/theory/theory_model.h index 0d73cd72a..a8726f490 100644 --- a/src/theory/theory_model.h +++ b/src/theory/theory_model.h @@ -21,51 +21,80 @@ #include #include "smt/model.h" -#include "theory/uf/equality_engine.h" #include "theory/rep_set.h" #include "theory/substitutions.h" #include "theory/type_enumerator.h" +#include "theory/type_set.h" +#include "theory/uf/equality_engine.h" namespace CVC4 { namespace theory { -/** - * Theory Model class. - * For Model m, should call m.initialize() before using. +/** Theory Model class. + * + * This class represents a model produced by the TheoryEngine. + * The data structures used to represent a model are: + * (1) d_equalityEngine : an equality engine object, which stores + * an equivalence relation over all terms that exist in + * the current set of assertions. + * (2) d_substitutions : a substitution map storing cases of + * explicitly solved terms, for instance during preprocessing. + * (3) d_reps : a map from equivalence class representatives of + * the equality engine to the (constant) representatives + * assigned to that equivalence class. + * (4) d_uf_models : a map from uninterpreted functions to their + * lambda representation. + * (5) d_rep_set : a data structure that allows interpretations + * for types to be represented as terms. This is useful for + * finite model finding. + * + * These data structures are built after a full effort check with + * no lemmas sent, within a call to: + * TheoryEngineModelBuilder::buildModel(...) + * which includes subcalls to TheoryX::collectModelInfo(...) calls. + * + * These calls may modify the model object using the interface + * functions below, including: + * - assertEquality, assertPredicate, assertRepresentative, + * assertEqualityEngine. + * - assignFunctionDefinition + * + * During and after this building process, these calls may use + * interface functions below to guide the model construction: + * - hasTerm, getRepresentative, areEqual, areDisequal + * - getEqualityEngine + * - getRepSet + * - hasAssignedFunctionDefinition, getFunctionsToAssign + * + * After this building process, the function getValue can be + * used to query the value of nodes. */ class TheoryModel : public Model { friend class TheoryEngineModelBuilder; - public: TheoryModel(context::Context* c, std::string name, bool enableFuncModels); virtual ~TheoryModel() throw(); - /** get comments */ - void getComments(std::ostream& out) const; - /** is built */ - bool isBuilt() { return d_modelBuilt; } - /** set need build */ - void setNeedsBuild() { d_modelBuilt = false; } - /** - * Get value function. This should be called only after a ModelBuilder has called buildModel(...) - * on this model. + /** reset the model */ + virtual void reset(); + /** is built + * + * Have we (attempted to) build this model since the last + * call to reset? Notice for model building techniques + * that are not guaranteed to succeed (such as + * when quantified formulas are enabled), a true return + * value does not imply that this is a model of the + * current assertions. */ - Node getValue( TNode n, bool useDontCares = false ) const; - - //---------------------------- separation logic - /** set the heap and value sep.nil is equal to */ - void setHeapModel(Node h, Node neq); - /** get the heap and value sep.nil is equal to */ - bool getHeapModel(Expr& h, Expr& neq) const; - //---------------------------- end separation logic - + bool isBuilt() { return d_modelBuilt; } + //---------------------------- for building the model /** Adds a substitution from x to t. */ void addSubstitution(TNode x, TNode t, bool invalidateCache = true); - /** add term function - * addTerm( n ) will do any model-specific processing necessary for n, - * such as constraining the interpretation of uninterpreted functions, - * and adding n to the equality engine of this model + /** add term + * This will do any model-specific processing necessary for n, + * such as constraining the interpretation of uninterpreted functions, + * and adding n to the equality engine of this model. */ virtual void addTerm(TNode n); /** assert equality holds in the model */ @@ -81,6 +110,7 @@ public: * functions. */ void assertRepresentative(TNode n); + //---------------------------- end building the model // ------------------- general equality queries /** does the equality engine of this model have term a? */ @@ -95,6 +125,23 @@ public: eq::EqualityEngine* getEqualityEngine() { return d_equalityEngine; } // ------------------- end general equality queries + /** Get value function. + * This should be called only after a ModelBuilder + * has called buildModel(...) on this model. + * useDontCares is whether to return Node::null() if + * n does not occur in the equality engine. + */ + Node getValue(TNode n, bool useDontCares = false) const; + /** get comments */ + void getComments(std::ostream& out) const; + + //---------------------------- separation logic + /** set the heap and value sep.nil is equal to */ + void setHeapModel(Node h, Node neq); + /** get the heap and value sep.nil is equal to */ + bool getHeapModel(Expr& h, Expr& neq) const; + //---------------------------- end separation logic + /** get the representative set object */ const RepSet* getRepSet() const { return &d_rep_set; } /** get the representative set object (FIXME: remove this, see #1199) */ @@ -145,19 +192,23 @@ public: /** true/false nodes */ Node d_true; Node d_false; - mutable std::unordered_map d_modelCache; /** comment stream to include in printing */ std::stringstream d_comment_str; - /** reset the model */ - virtual void reset(); - /** - * Get model value function. This function is called by getValue + /** Get model value function. + * + * This function is a helper function for getValue. + * hasBoundVars is whether n may contain bound variables + * useDontCares is whether to return Node::null() if + * n does not occur in the equality engine. */ Node getModelValue(TNode n, bool hasBoundVars = false, bool useDontCares = false) const; private: + /** cache for getModelValue */ + mutable std::unordered_map d_modelCache; + //---------------------------- separation logic /** the value of the heap */ Node d_sep_heap; @@ -170,234 +221,12 @@ public: bool d_enableFuncModels; /** map from function terms to the (lambda) definitions * After the model is built, the domain of this map is all terms of function - * type - * that appear as terms in d_equalityEngine. + * type that appear as terms in d_equalityEngine. */ std::map d_uf_models; //---------------------------- end function values };/* class TheoryModel */ -/* - * Class that encapsulates a map from types to sets of nodes - */ -class TypeSet { -public: - typedef std::unordered_map*, TypeNodeHashFunction> TypeSetMap; - typedef std::unordered_map TypeToTypeEnumMap; - typedef TypeSetMap::iterator iterator; - typedef TypeSetMap::const_iterator const_iterator; -private: - TypeSetMap d_typeSet; - TypeToTypeEnumMap d_teMap; - TypeEnumeratorProperties * d_tep; - - /* 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; i* s; - if (it == d_typeSet.end()) { - s = new std::set; - d_typeSet[t] = s; - } - else { - s = (*it).second; - } - s->insert(n); - } - - std::set* getSet(TypeNode t) const - { - const_iterator it = d_typeSet.find(t); - if (it == d_typeSet.end()) { - return NULL; - } - return (*it).second; - } - - Node nextTypeEnum(TypeNode t, bool useBaseType = false) - { - TypeEnumerator* te; - TypeToTypeEnumMap::iterator it = d_teMap.find(t); - if (it == d_teMap.end()) { - te = new TypeEnumerator(t, d_tep); - d_teMap[t] = te; - } - else { - te = (*it).second; - } - if (te->isFinished()) { - return Node(); - } - - if (useBaseType) { - t = t.getBaseType(); - } - iterator itSet = d_typeSet.find(t); - std::set* s; - if (itSet == d_typeSet.end()) { - s = new std::set; - d_typeSet[t] = s; - } - else { - s = (*itSet).second; - } - Node n = **te; - while (s->find(n) != s->end()) { - ++(*te); - if (te->isFinished()) { - return Node(); - } - n = **te; - } - s->insert(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; - } - - bool empty() - { - return d_typeSet.empty(); - } - - iterator begin() - { - return d_typeSet.begin(); - } - - iterator end() - { - return d_typeSet.end(); - } - - static TypeNode getType(iterator it) - { - return (*it).first; - } - - static std::set& getSet(iterator it) - { - return *(*it).second; - } - -};/* class TypeSet */ - -/** TheoryEngineModelBuilder class - * This model builder will consult all theories in a theory engine for - * collectModelInfo( ... ) when building a model. - */ -class TheoryEngineModelBuilder : public ModelBuilder -{ -protected: - /** pointer to theory engine */ - TheoryEngine* d_te; - typedef std::unordered_map NodeMap; - NodeMap d_normalizedCache; - typedef std::unordered_set NodeSet; - std::map< Node, Node > d_constantReps; - - /** process build model */ - virtual bool preProcessBuildModel(TheoryModel* m); - virtual bool processBuildModel(TheoryModel* m); - virtual void debugModel( TheoryModel* m ) {} - /** normalize representative */ - Node normalize(TheoryModel* m, TNode r, bool evalOnly); - 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 ); - /** involves usort */ - bool involvesUSort( TypeNode tn ); - bool isExcludedUSortValue( std::map< TypeNode, unsigned >& eqc_usort_count, Node v, std::map< Node, bool >& visited ); -protected: - /** assign function f based on the model m. - * This construction is based on "table form". For example: - * (f 0 1) = 1 - * (f 0 2) = 2 - * (f 1 1) = 3 - * ... - * becomes: - * f = (lambda xy. (ite (and (= x 0) (= y 1)) 1 - * (ite (and (= x 0) (= y 2)) 2 - * (ite (and (= x 1) (= y 1)) 3 ...))) - */ - void assignFunction(TheoryModel* m, Node f); - /** assign function f based on the model m. - * This construction is based on "dag form". For example: - * (f 0 1) = 1 - * (f 0 2) = 2 - * (f 1 1) = 3 - * ... - * becomes: - * f = (lambda xy. (ite (= x 0) (ite (= y 1) 1 - * (ite (= y 2) 2 ...)) - * (ite (= x 1) (ite (= y 1) 3 ...) - * ...)) - * - * where the above is represented as a directed acyclic graph (dag). - * This construction is accomplished by assigning values to (f c) - * terms before f, e.g. - * (f 0) = (lambda y. (ite (= y 1) 1 - * (ite (= y 2) 2 ...)) - * (f 1) = (lambda y. (ite (= y 1) 3 ...)) - * where - * f = (lambda xy. (ite (= x 0) ((f 0) y) - * (ite (= x 1) ((f 1) y) ...)) - */ - void assignHoFunction(TheoryModel* m, Node f); - /** Assign all unassigned functions in the model m (those returned by TheoryModel::getFunctionsToAssign), - * using the two functions above. Currently: - * If ufHo is disabled, we call assignFunction for all functions. - * If ufHo is enabled, we call assignHoFunction. - */ - void assignFunctions(TheoryModel* m); -public: - TheoryEngineModelBuilder(TheoryEngine* te); - virtual ~TheoryEngineModelBuilder(){} - /** Build model function. - * Should be called only on TheoryModels m - */ - bool buildModel(Model* m); - void debugCheckModel(Model* m); -};/* class TheoryEngineModelBuilder */ - }/* CVC4::theory namespace */ }/* CVC4 namespace */ diff --git a/src/theory/theory_model_builder.cpp b/src/theory/theory_model_builder.cpp new file mode 100644 index 000000000..b08c8f1ca --- /dev/null +++ b/src/theory/theory_model_builder.cpp @@ -0,0 +1,1144 @@ +/********************* */ +/*! \file theory_model_builder.cpp + ** \verbatim + ** Top contributors (to current version): + ** Clark Barrett, Andrew Reynolds, Morgan Deters + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Implementation of theory model buidler class + **/ +#include "theory/theory_model_builder.h" + +#include "options/quantifiers_options.h" +#include "options/smt_options.h" +#include "options/uf_options.h" +#include "theory/theory_engine.h" +#include "theory/uf/theory_uf_model.h" + +using namespace std; +using namespace CVC4::kind; +using namespace CVC4::context; + +namespace CVC4 { +namespace theory { + +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::addAssignableSubterms(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) + { + addAssignableSubterms(*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* repSet, + std::map& assertedReps, + Node eqc) +{ + Trace("model-builder-debug") + << "Is " << val << " and excluded codatatype value for " << eqc << "? " + << std::endl; + for (set::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& eqc_usort_count, + Node v, + std::map& 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().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& type_list, + std::unordered_set& visiting) +{ + if (std::find(type_list.begin(), type_list.end(), tn) == type_list.end()) + { + if (visiting.find(tn) == visiting.end()) + { + visiting.insert(tn); + /* 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()); + + // Reset model + tm->reset(); + + // mark as built + tm->d_modelBuilt = true; + + // 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 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) + { + addAssignableSubterms(*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 assertedReps; + TypeSet typeConstSet, typeRepSet, typeNoRepSet; + TypeEnumeratorProperties tep; + if (options::finiteModelFind()) + { + tep.d_fixed_usort_card = true; + for (std::map::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 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::unordered_set visiting; + addToTypeList(eqct.getBaseType(), type_list, visiting); + } + else + { + typeNoRepSet.add(eqct, eqc); + std::unordered_set 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::iterator type_it; + set::iterator i, i2; + bool changed, unassignedAssignable, assignOne = false; + set 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* 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* 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* noRepSetPtr = typeNoRepSet.getSet(t); + if (noRepSetPtr == NULL) + { + continue; + } + set& 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* repSet = typeRepSet.getSet(t); + TypeNode tb = t.getBaseType(); + if (!assignOne) + { + set* 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 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 + 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& 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::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& noRepSet = TypeSet::getSet(it); + set::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::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::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 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 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 argTypes = type.getArgTypes(); + std::vector args; + std::vector 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 >::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 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 d_type_size; + // get the size of type tn + unsigned getTypeSize(TypeNode tn) + { + std::map::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 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 */ diff --git a/src/theory/theory_model_builder.h b/src/theory/theory_model_builder.h new file mode 100644 index 000000000..c24d50cbf --- /dev/null +++ b/src/theory/theory_model_builder.h @@ -0,0 +1,253 @@ +/********************* */ +/*! \file theory_model.h + ** \verbatim + ** Top contributors (to current version): + ** Clark Barrett, Morgan Deters, Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Model class + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__THEORY__THEORY_MODEL_BUILDER_H +#define __CVC4__THEORY__THEORY_MODEL_BUILDER_H + +#include +#include + +#include "theory/theory_model.h" + +namespace CVC4 { +namespace theory { + +/** TheoryEngineModelBuilder class + * + * This is the class used by TheoryEngine + * for constructing TheoryModel objects, which is the class + * that represents models for a set of assertions. + * + * A call to TheoryEngineModelBuilder::buildModel(...) is made + * after a full effort check passes with no theory solvers + * adding lemmas or conflicts, and theory combination passes + * with no splits on shared terms. If buildModel is successful, + * this will set up the data structures in TheoryModel to represent + * a model for the current set of assertions. + */ +class TheoryEngineModelBuilder : public ModelBuilder +{ + typedef std::unordered_map NodeMap; + typedef std::unordered_set NodeSet; + + public: + TheoryEngineModelBuilder(TheoryEngine* te); + virtual ~TheoryEngineModelBuilder() {} + /** Build model function. + * + * Should be called only on TheoryModels m. + * + * This constructs the model m, via the following steps: + * (1) call TheoryEngine::collectModelInfo, + * (2) builder-specified pre-processing, + * (3) find the equivalence classes of m's + * equality engine that initially contain constants, + * (4) assign constants to all equivalence classes + * of m's equality engine, through alternating + * iterations of evaluation and enumeration, + * (5) builder-specific post-processing. + * + * This function returns false if any of the above + * steps results in a lemma sent on an output channel. + * Lemmas may be sent on an output channel by this + * builder in steps (2) or (5), for instance, if the model we + * are building fails to satisfy a quantified formula. + */ + virtual bool buildModel(Model* m) override; + /** Debug check model. + * + * This throws an assertion failure if the model + * contains an equivalence class with two terms t1 and t2 + * such that t1^M != t2^M. + */ + void debugCheckModel(Model* m); + + protected: + /** pointer to theory engine */ + TheoryEngine* d_te; + + //-----------------------------------virtual functions + /** pre-process build model + * Do pre-processing specific to this model builder. + * Called in step (2) of the build construction, + * described above. + */ + virtual bool preProcessBuildModel(TheoryModel* m); + /** process build model + * Do processing specific to this model builder. + * Called in step (5) of the build construction, + * described above. + * By default, this assigns values to each function + * that appears in m's equality engine. + */ + virtual bool processBuildModel(TheoryModel* m); + /** debug the model + * Check assertions and printing debug information for the model. + * Calls after step (5) described above is complete. + */ + virtual void debugModel(TheoryModel* m) {} + //-----------------------------------end virtual functions + + /** is n assignable? + * + * A term n is assignable if its value + * is unconstrained by a standard model. + * Examples of assignable terms are: + * - variables, + * - applications of array select, + * - applications of datatype selectors, + * - applications of uninterpreted functions. + * Assignable terms must be first-order, that is, + * all instances of the above terms are not + * assignable if they have a higher-order (function) type. + */ + bool isAssignable(TNode n); + /** add assignable subterms + * Adds all assignable subterms of n to tm's equality engine. + */ + void addAssignableSubterms(TNode n, TheoryModel* tm, NodeSet& cache); + /** normalize representative r + * + * This returns a term that is equivalent to r's + * interpretation in the model m. It may do so + * by rewriting the application of r's operator to the + * result of normalizing each of r's children, if + * each child is constant. + */ + Node normalize(TheoryModel* m, TNode r, bool evalOnly); + /** assign constant representative + * + * Called when equivalence class eqc is assigned a constant + * representative const_rep. + * + * eqc should be a representative of tm's equality engine. + */ + void assignConstantRep(TheoryModel* tm, Node eqc, Node const_rep); + /** add to type list + * + * This adds to type_list the list of types that tn is built from. + * For example, if tn is (Array Int Bool) and type_list is empty, + * then we append ( Int, Bool, (Array Int Bool) ) to type_list. + */ + void addToTypeList( + TypeNode tn, + std::vector& type_list, + std::unordered_set& visiting); + /** assign function f based on the model m. + * This construction is based on "table form". For example: + * (f 0 1) = 1 + * (f 0 2) = 2 + * (f 1 1) = 3 + * ... + * becomes: + * f = (lambda xy. (ite (and (= x 0) (= y 1)) 1 + * (ite (and (= x 0) (= y 2)) 2 + * (ite (and (= x 1) (= y 1)) 3 ...))) + */ + void assignFunction(TheoryModel* m, Node f); + /** assign function f based on the model m. + * This construction is based on "dag form". For example: + * (f 0 1) = 1 + * (f 0 2) = 2 + * (f 1 1) = 3 + * ... + * becomes: + * f = (lambda xy. (ite (= x 0) (ite (= y 1) 1 + * (ite (= y 2) 2 ...)) + * (ite (= x 1) (ite (= y 1) 3 ...) + * ...)) + * + * where the above is represented as a directed acyclic graph (dag). + * This construction is accomplished by assigning values to (f c) + * terms before f, e.g. + * (f 0) = (lambda y. (ite (= y 1) 1 + * (ite (= y 2) 2 ...)) + * (f 1) = (lambda y. (ite (= y 1) 3 ...)) + * where + * f = (lambda xy. (ite (= x 0) ((f 0) y) + * (ite (= x 1) ((f 1) y) ...)) + */ + void assignHoFunction(TheoryModel* m, Node f); + /** assign functions + * + * Assign all unassigned functions in the model m (those returned by + * TheoryModel::getFunctionsToAssign), + * using the two functions above. Currently: + * If ufHo is disabled, we call assignFunction for all functions. + * If ufHo is enabled, we call assignHoFunction. + */ + void assignFunctions(TheoryModel* m); + + private: + /** normalized cache + * A temporary cache mapping terms to their + * normalized form, used during buildModel. + */ + NodeMap d_normalizedCache; + /** mapping from terms to the constant associated with their equivalence class + */ + std::map d_constantReps; + + //------------------------------------for codatatypes + /** is v an excluded codatatype value? + * + * If this returns true, then v is a value + * that cannot be used during enumeration in step (4) + * of model construction. + * + * repSet is the set of representatives of the same type as v, + * assertedReps is a map from representatives t, + * eqc is the equivalence class that v reside. + * + * This function is used to avoid alpha-equivalent + * assignments for codatatype terms, described in + * Reynolds/Blanchette CADE 2015. In particular, + * this function returns true if v is in + * the set V^{x}_I from page 9, where x is eqc + * and I is the model we are building. + */ + bool isExcludedCdtValue(Node v, + std::set* repSet, + std::map& assertedReps, + Node eqc); + /** is codatatype value match + * + * This returns true if v is r{ eqc -> t } for some t. + * If this function returns true, then t above is + * stored in eqc_m. + */ + bool isCdtValueMatch(Node v, Node r, Node eqc, Node& eqc_m); + //------------------------------------end for codatatypes + + //---------------------------------for debugging finite model finding + /** does type tn involve an uninterpreted sort? */ + bool involvesUSort(TypeNode tn); + /** is v an excluded value based on uninterpreted sorts? + * This gives an assertion failure in the case that v contains + * an uninterpreted constant whose index is out of the bounds + * specified by eqc_usort_count. + */ + bool isExcludedUSortValue(std::map& eqc_usort_count, + Node v, + std::map& visited); + //---------------------------------end for debugging finite model finding + +}; /* class TheoryEngineModelBuilder */ + +} /* CVC4::theory namespace */ +} /* CVC4 namespace */ + +#endif /* __CVC4__THEORY__THEORY_MODEL_BUILDER_H */ diff --git a/src/theory/type_set.cpp b/src/theory/type_set.cpp new file mode 100644 index 000000000..e7caa667b --- /dev/null +++ b/src/theory/type_set.cpp @@ -0,0 +1,146 @@ +/********************* */ +/*! \file type_set.cpp + ** \verbatim + ** Top contributors (to current version): + ** Clark Barrett, Andrew Reynolds, Morgan Deters + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Implementation of type set class + **/ +#include "theory/type_set.h" + +using namespace std; +using namespace CVC4::kind; + +namespace CVC4 { +namespace theory { + +TypeSet::~TypeSet() +{ + iterator it; + for (it = d_typeSet.begin(); it != d_typeSet.end(); ++it) + { + if ((*it).second != NULL) + { + delete (*it).second; + } + } + TypeToTypeEnumMap::iterator it2; + for (it2 = d_teMap.begin(); it2 != d_teMap.end(); ++it2) + { + if ((*it2).second != NULL) + { + delete (*it2).second; + } + } +} + +void TypeSet::setTypeEnumeratorProperties(TypeEnumeratorProperties* tep) +{ + d_tep = tep; +} + +void TypeSet::add(TypeNode t, TNode n) +{ + iterator it = d_typeSet.find(t); + std::set* s; + if (it == d_typeSet.end()) + { + s = new std::set; + d_typeSet[t] = s; + } + else + { + s = (*it).second; + } + s->insert(n); +} + +std::set* TypeSet::getSet(TypeNode t) const +{ + const_iterator it = d_typeSet.find(t); + if (it == d_typeSet.end()) + { + return NULL; + } + return (*it).second; +} + +Node TypeSet::nextTypeEnum(TypeNode t, bool useBaseType) +{ + TypeEnumerator* te; + TypeToTypeEnumMap::iterator it = d_teMap.find(t); + if (it == d_teMap.end()) + { + te = new TypeEnumerator(t, d_tep); + d_teMap[t] = te; + } + else + { + te = (*it).second; + } + if (te->isFinished()) + { + return Node(); + } + + if (useBaseType) + { + t = t.getBaseType(); + } + iterator itSet = d_typeSet.find(t); + std::set* s; + if (itSet == d_typeSet.end()) + { + s = new std::set; + d_typeSet[t] = s; + } + else + { + s = (*itSet).second; + } + Node n = **te; + while (s->find(n) != s->end()) + { + ++(*te); + if (te->isFinished()) + { + return Node(); + } + n = **te; + } + s->insert(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 + // previously enumerated values + std::unordered_set visited; + addSubTerms(n, visited); + ++(*te); + return n; +} + +void TypeSet::addSubTerms(TNode n, + std::unordered_set& visited, + bool topLevel) +{ + if (visited.find(n) == visited.end()) + { + visited.insert(n); + if (!topLevel) + { + add(n.getType(), n); + } + for (unsigned i = 0; i < n.getNumChildren(); i++) + { + addSubTerms(n[i], visited, false); + } + } +} + +} /* namespace CVC4::theory */ +} /* namespace CVC4 */ diff --git a/src/theory/type_set.h b/src/theory/type_set.h new file mode 100644 index 000000000..2d9be97be --- /dev/null +++ b/src/theory/type_set.h @@ -0,0 +1,90 @@ +/********************* */ +/*! \file type_set.h + ** \verbatim + ** Top contributors (to current version): + ** Clark Barrett, Morgan Deters, Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Type set class + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__THEORY__TYPE_SET_H +#define __CVC4__THEORY__TYPE_SET_H + +#include +#include + +#include "theory/type_enumerator.h" + +namespace CVC4 { +namespace theory { + +/* Type set + * + * This class encapsulates a map from types to sets of nodes. + */ +class TypeSet +{ + public: + typedef std::unordered_map*, TypeNodeHashFunction> + TypeSetMap; + typedef std::unordered_map + TypeToTypeEnumMap; + typedef TypeSetMap::iterator iterator; + typedef TypeSetMap::const_iterator const_iterator; + + public: + TypeSet() : d_tep(NULL) {} + ~TypeSet(); + /** set the properties of the type set + * + * These indicate information such as finite bounds + * on the number of unique uninterpreted constants that can be + * enumerated by this class. + */ + void setTypeEnumeratorProperties(TypeEnumeratorProperties* tep); + /** add node n to the set of values of t */ + void add(TypeNode t, TNode n); + /** get the set of values of type t */ + std::set* getSet(TypeNode t) const; + /** get the next enumerated term of type t + * + * useBaseType is whether + */ + Node nextTypeEnum(TypeNode t, bool useBaseType = false); + + bool empty() { return d_typeSet.empty(); } + iterator begin() { return d_typeSet.begin(); } + iterator end() { return d_typeSet.end(); } + static TypeNode getType(iterator it) { return (*it).first; } + static std::set& getSet(iterator it) { return *(*it).second; } + private: + /** sets of values for each type */ + TypeSetMap d_typeSet; + /** type enumerators for each type */ + TypeToTypeEnumMap d_teMap; + /** pointer the type enumerator properties for this class. */ + TypeEnumeratorProperties* d_tep; + + /* add all sub-terms of n to the sets of this class + * + * If topLevel is true, then we add strict subterms only. + * + * Note that recursive traversal here is over enumerated expressions + * (very low expression depth). + */ + void addSubTerms(TNode n, + std::unordered_set& visited, + bool topLevel = true); +}; /* class TypeSet */ + +} /* CVC4::theory namespace */ +} /* CVC4 namespace */ + +#endif /* __CVC4__THEORY__TYPE_SET_H */