From f56f46f5bb5845cff0c329926f51a0377379365b Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 5 Oct 2017 07:12:47 -0500 Subject: [PATCH] Ho model (#1120) * Update model construction for higher order. If HO_APPLY terms are present for a function, we use a curried (tree) model construction to avoid exponential size model representations for function definitions. * Update comments. * Change terminology in comment. * Improve comments. --- src/theory/quantifiers/ambqi_builder.cpp | 3 +- src/theory/quantifiers/full_model_check.cpp | 3 +- src/theory/quantifiers/model_builder.cpp | 3 +- src/theory/theory_model.cpp | 421 ++++++++++++++++---- src/theory/theory_model.h | 64 ++- 5 files changed, 413 insertions(+), 81 deletions(-) diff --git a/src/theory/quantifiers/ambqi_builder.cpp b/src/theory/quantifiers/ambqi_builder.cpp index 1bab682f4..d1a3a1bec 100644 --- a/src/theory/quantifiers/ambqi_builder.cpp +++ b/src/theory/quantifiers/ambqi_builder.cpp @@ -821,7 +821,8 @@ bool AbsMbqiBuilder::processBuildModel(TheoryModel* m) { for( std::map::iterator it = fm->d_models.begin(); it != fm->d_models.end(); ++it ) { if( it->first.getType().getNumChildren()>1 ){ Trace("ambqi-model") << "Construct for " << it->first << "..." << std::endl; - m->d_uf_models[ it->first ] = fm->getFunctionValue( it->first, "$x" ); + Node f_def = fm->getFunctionValue( it->first, "$x" ); + m->assignFunctionDefinition( it->first, f_def ); } } Assert( d_addedLemmas==0 ); diff --git a/src/theory/quantifiers/full_model_check.cpp b/src/theory/quantifiers/full_model_check.cpp index 82a1c6626..6f617db42 100644 --- a/src/theory/quantifiers/full_model_check.cpp +++ b/src/theory/quantifiers/full_model_check.cpp @@ -536,7 +536,8 @@ bool FullModelChecker::processBuildModel(TheoryModel* m){ //make function values for( std::map::iterator it = fm->d_models.begin(); it != fm->d_models.end(); ++it ){ - m->d_uf_models[ it->first ] = getFunctionValue( fm, it->first, "$x" ); + Node f_def = getFunctionValue( fm, it->first, "$x" ); + m->assignFunctionDefinition( it->first, f_def ); } return TheoryEngineModelBuilder::processBuildModel( m ); } diff --git a/src/theory/quantifiers/model_builder.cpp b/src/theory/quantifiers/model_builder.cpp index 41c68a117..2b7ba7ac9 100644 --- a/src/theory/quantifiers/model_builder.cpp +++ b/src/theory/quantifiers/model_builder.cpp @@ -275,7 +275,8 @@ bool QModelBuilderIG::processBuildModel( TheoryModel* m ) { it->second.update( fm ); Trace("model-func") << "QModelBuilder: Make function value from tree " << it->first << std::endl; //construct function values - fm->d_uf_models[ it->first ] = it->second.getFunctionValue( "$x" ); + Node f_def = it->second.getFunctionValue( "$x" ); + fm->assignFunctionDefinition( it->first, f_def ); } Assert( d_addedLemmas==0 ); return TheoryEngineModelBuilder::processBuildModel( m ); diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp index 840bbd027..a4b36b87c 100644 --- a/src/theory/theory_model.cpp +++ b/src/theory/theory_model.cpp @@ -39,7 +39,8 @@ TheoryModel::TheoryModel(context::Context* c, std::string name, bool enableFuncM d_equalityEngine = new eq::EqualityEngine(d_eeContext, name, false); // The kinds we are treating as function application in congruence - d_equalityEngine->addFunctionKind(kind::APPLY_UF); + d_equalityEngine->addFunctionKind(kind::APPLY_UF, false, options::ufHo()); + d_equalityEngine->addFunctionKind(kind::HO_APPLY); d_equalityEngine->addFunctionKind(kind::SELECT); // d_equalityEngine->addFunctionKind(kind::STORE); d_equalityEngine->addFunctionKind(kind::APPLY_CONSTRUCTOR); @@ -62,6 +63,7 @@ void TheoryModel::reset(){ d_reps.clear(); d_rep_set.clear(); d_uf_terms.clear(); + d_ho_uf_terms.clear(); d_uf_models.clear(); d_eeContext->pop(); d_eeContext->push(); @@ -90,6 +92,7 @@ bool TheoryModel::getHeapModel( Expr& h, Expr& neq ) const { Node TheoryModel::getValue(TNode n, bool useDontCares) const { //apply substitutions Node nn = d_substitutions.apply(n); + Debug("model-getvalue-debug") << "[model-getvalue] getValue : substitute " << n << " to " << nn << std::endl; //get value in model nn = getModelValue(nn, false, useDontCares); if (nn.isNull()) return nn; @@ -136,6 +139,8 @@ Node TheoryModel::getModelValue(TNode n, bool hasBoundVars, bool useDontCares) c if (it != d_modelCache.end()) { return (*it).second; } + Debug("model-getvalue-debug") << "Get model value " << n << " ... "; + Debug("model-getvalue-debug") << d_equalityEngine->hasTerm(n) << std::endl; Node ret = n; if(n.getKind() == kind::EXISTS || n.getKind() == kind::FORALL || n.getKind() == kind::COMBINED_CARDINALITY_CONSTRAINT ) { // We should have terms, thanks to TheoryQuantifiers::collectModelInfo(). @@ -160,11 +165,13 @@ Node TheoryModel::getModelValue(TNode n, bool hasBoundVars, bool useDontCares) c ret = nr; } } else { + // FIXME : special case not necessary? (also address BV_ACKERMANIZE functions below), github issue #1116 if(n.getKind() == kind::LAMBDA) { NodeManager* nm = NodeManager::currentNM(); Node body = getModelValue(n[1], true); body = Rewriter::rewrite(body); ret = nm->mkNode(kind::LAMBDA, n[0], body); + ret = Rewriter::rewrite( ret ); d_modelCache[n] = ret; return ret; } @@ -172,34 +179,7 @@ Node TheoryModel::getModelValue(TNode n, bool hasBoundVars, bool useDontCares) c d_modelCache[n] = ret; return ret; } - - TypeNode t = n.getType(); - if (t.isFunction() || t.isPredicate()) { - if (d_enableFuncModels) { - std::map< Node, Node >::const_iterator it = d_uf_models.find(n); - if (it != d_uf_models.end()) { - // Existing function - ret = it->second; - d_modelCache[n] = ret; - return ret; - } - // Unknown function symbol: return LAMBDA x. c, where c is the first constant in the enumeration of the range type - vector argTypes = t.getArgTypes(); - vector args; - NodeManager* nm = NodeManager::currentNM(); - for (unsigned i = 0; i < argTypes.size(); ++i) { - args.push_back(nm->mkBoundVar(argTypes[i])); - } - Node boundVarList = nm->mkNode(kind::BOUND_VAR_LIST, args); - TypeEnumerator te(t.getRangeType()); - ret = nm->mkNode(kind::LAMBDA, boundVarList, *te); - d_modelCache[n] = ret; - return ret; - } - // TODO: if func models not enabled, throw an error? - Unreachable(); - } - + if (n.getNumChildren() > 0 && n.getKind() != kind::BITVECTOR_ACKERMANIZE_UDIV && n.getKind() != kind::BITVECTOR_ACKERMANIZE_UREM) { @@ -233,9 +213,46 @@ Node TheoryModel::getModelValue(TNode n, bool hasBoundVars, bool useDontCares) c d_modelCache[n] = ret; return ret; } - - if (!d_equalityEngine->hasTerm(n)) { - if(n.getType().isRegExp()) { + + Debug("model-getvalue-debug") << "Handling special cases for types..." << std::endl; + TypeNode t = n.getType(); + bool eeHasTerm; + if( !options::ufHo() && (t.isFunction() || t.isPredicate()) ){ + // functions are in the equality engine, but *not* as first-class members + // when higher-order is disabled. In this case, we cannot query representatives for functions + // since they are "internal" nodes according to the equality engine despite hasTerm returning true. + // However, they are first class members when higher-order is enabled. Hence, the special + // case here. + eeHasTerm = false; + }else{ + eeHasTerm = d_equalityEngine->hasTerm(n); + } + // if the term does not exist in the equality engine, return an arbitrary value + if (!eeHasTerm) { + if (t.isFunction() || t.isPredicate()) { + if (d_enableFuncModels) { + std::map< Node, Node >::const_iterator it = d_uf_models.find(n); + if (it != d_uf_models.end()) { + // Existing function + ret = it->second; + d_modelCache[n] = ret; + return ret; + } + // Unknown function symbol: return LAMBDA x. c, where c is the first constant in the enumeration of the range type + vector argTypes = t.getArgTypes(); + vector args; + NodeManager* nm = NodeManager::currentNM(); + for (unsigned i = 0; i < argTypes.size(); ++i) { + args.push_back(nm->mkBoundVar(argTypes[i])); + } + Node boundVarList = nm->mkNode(kind::BOUND_VAR_LIST, args); + TypeEnumerator te(t.getRangeType()); + ret = nm->mkNode(kind::LAMBDA, boundVarList, *te); + }else{ + // TODO: if func models not enabled, throw an error? + Unreachable(); + } + }else if(t.isRegExp()) { ret = Rewriter::rewrite(ret); } else { if (options::omitDontCares() && useDontCares) { @@ -249,6 +266,7 @@ Node TheoryModel::getModelValue(TNode n, bool hasBoundVars, bool useDontCares) c return ret; } } + Debug("model-getvalue-debug") << "get value from representative " << ret << "..." << std::endl; ret = d_equalityEngine->getRepresentative(ret); Assert(d_reps.find(ret) != d_reps.end()); std::map< Node, Node >::const_iterator it2 = d_reps.find( ret ); @@ -276,6 +294,7 @@ Node TheoryModel::getDomainValue( TypeNode tn, std::vector< Node >& exclude ){ /** add substitution */ void TheoryModel::addSubstitution( TNode x, TNode t, bool invalidateCache ){ if( !d_substitutions.hasSubstitution( x ) ){ + Debug("model") << "Add substitution in model " << x << " -> " << t << std::endl; d_substitutions.addSubstitution( x, t, invalidateCache ); } else { #ifdef CVC4_ASSERTIONS @@ -296,12 +315,29 @@ void TheoryModel::addSubstitution( TNode x, TNode t, bool invalidateCache ){ /** add term */ void TheoryModel::addTerm(TNode n ){ Assert(d_equalityEngine->hasTerm(n)); + Trace("model-builder-debug2") << "TheoryModel::addTerm : " << n << std::endl; //must collect UF terms if (n.getKind()==APPLY_UF) { Node op = n.getOperator(); if( std::find( d_uf_terms[ op ].begin(), d_uf_terms[ op ].end(), n )==d_uf_terms[ op ].end() ){ d_uf_terms[ op ].push_back( n ); - Trace("model-add-term-uf") << "Add term " << n << std::endl; + Trace("model-builder-fun") << "Add apply term " << n << std::endl; + } + }else if( n.getKind()==HO_APPLY ){ + Node op = n[0]; + if( std::find( d_ho_uf_terms[ op ].begin(), d_ho_uf_terms[ op ].end(), n )==d_ho_uf_terms[ op ].end() ){ + d_ho_uf_terms[ op ].push_back( n ); + Trace("model-builder-fun") << "Add ho apply term " << n << std::endl; + } + } + // all functions must be included, marked as higher-order + if( n.getType().isFunction() ){ + Trace("model-builder-fun") << "Add function variable (without term) " << n << std::endl; + if( d_uf_terms.find( n )==d_uf_terms.end() ){ + d_uf_terms[n].clear(); + } + if( d_ho_uf_terms.find( n )==d_ho_uf_terms.end() ){ + d_ho_uf_terms[n].clear(); } } } @@ -341,16 +377,20 @@ void TheoryModel::assertEqualityEngine(const eq::EqualityEngine* ee, set* bool predicate = false; bool predTrue = false; bool predFalse = false; + Trace("model-builder-debug") << "...asserting terms in equivalence class " << eqc; if (eqc.getType().isBoolean()) { predicate = true; predTrue = ee->areEqual(eqc, d_true); predFalse = ee->areEqual(eqc, d_false); + Trace("model-builder-debug") << ", pred = " << predTrue << "/" << predFalse; } + Trace("model-builder-debug") << std::endl; eq::EqClassIterator eqc_i = eq::EqClassIterator(eqc, ee); bool first = true; Node rep; for (; !eqc_i.isFinished(); ++eqc_i) { if (termSet != NULL && termSet->find(*eqc_i) == termSet->end()) { + Trace("model-builder-debug") << "...skip node " << (*eqc_i) << " in eqc " << eqc << std::endl; continue; } if (predicate) { @@ -465,6 +505,84 @@ void TheoryModel::printRepresentative( std::ostream& out, Node r ){ } } +void TheoryModel::assignFunctionDefinition( Node f, Node f_def ) { + Assert( d_uf_models.find( f )==d_uf_models.end() ); + Trace("model-builder") << " Assigning function (" << f << ") to (" << f_def << ")" << endl; + + if( options::ufHo() ){ + //we must rewrite the function value since the definition needs to be a constant value + f_def = Rewriter::rewrite( f_def ); + Assert( f_def.isConst() ); + } + + // d_uf_models only stores models for variables + if( f.isVar() ){ + d_uf_models[f] = f_def; + } + + if( options::ufHo() ){ + Trace("model-builder-debug") << " ...function is first-class member of equality engine" << std::endl; + // assign to representative if higher-order + Node r = d_equalityEngine->getRepresentative( f ); + //always replace the representative, since it is initially assigned to itself + Trace("model-builder") << " Assign: Setting function rep " << r << " to " << f_def << endl; + d_reps[r] = f_def; + // also assign to other assignable functions in the same equivalence class + eq::EqClassIterator eqc_i = eq::EqClassIterator(r,d_equalityEngine); + while( !eqc_i.isFinished() ) { + Node n = *eqc_i; + // if an unassigned variable function + if( n.isVar() && d_uf_terms.find( n )!=d_uf_terms.end() && !hasAssignedFunctionDefinition( n ) ){ + d_uf_models[n] = f_def; + Trace("model-builder") << " Assigning function (" << n << ") to function definition of " << f << std::endl; + } + ++eqc_i; + } + Trace("model-builder-debug") << " ...finished." << std::endl; + } +} + +std::vector< Node > TheoryModel::getFunctionsToAssign() { + std::vector< Node > funcs_to_assign; + std::map< Node, Node > func_to_rep; + + // collect functions + for( std::map< Node, std::vector< Node > >::iterator it = d_uf_terms.begin(); it != d_uf_terms.end(); ++it ){ + Node n = it->first; + Assert( !n.isNull() ); + if( !hasAssignedFunctionDefinition( n ) ){ + Trace("model-builder-fun-debug") << "Look at function : " << n << std::endl; + if( options::ufHo() ){ + // if in higher-order mode, assign function definitions modulo equality + Node r = getRepresentative( n ); + std::map< Node, Node >::iterator itf = func_to_rep.find( r ); + if( itf==func_to_rep.end() ){ + func_to_rep[r] = n; + funcs_to_assign.push_back( n ); + Trace("model-builder-fun") << "Make function " << n; + Trace("model-builder-fun") << " the assignable function in its equivalence class." << std::endl; + }else{ + // must combine uf terms + Trace("model-builder-fun") << "Copy " << it->second.size() << " uf terms"; + d_uf_terms[itf->second].insert( d_uf_terms[itf->second].end(), it->second.begin(), it->second.end() ); + std::map< Node, std::vector< Node > >::iterator ith = d_ho_uf_terms.find( n ); + if( ith!=d_ho_uf_terms.end() ){ + d_ho_uf_terms[itf->second].insert( d_ho_uf_terms[itf->second].end(), ith->second.begin(), ith->second.end() ); + Trace("model-builder-fun") << " and " << ith->second.size() << " ho uf terms"; + } + Trace("model-builder-fun") << " from " << n << " to its assignable representative function " << itf->second << std::endl; + it->second.clear(); + } + }else{ + Trace("model-builder-fun") << "Function to assign : " << n << std::endl; + funcs_to_assign.push_back( n ); + } + } + } + + Trace("model-builder-fun") << "return " << funcs_to_assign.size() << " functions to assign..." << std::endl; + return funcs_to_assign; +} TheoryEngineModelBuilder::TheoryEngineModelBuilder( TheoryEngine* te ) : d_te( te ){ @@ -473,7 +591,28 @@ TheoryEngineModelBuilder::TheoryEngineModelBuilder( TheoryEngine* te ) : d_te( t bool TheoryEngineModelBuilder::isAssignable(TNode n) { - return (n.isVar() || n.getKind() == kind::APPLY_UF || n.getKind() == kind::SELECT || n.getKind() == kind::APPLY_SELECTOR_TOTAL); + 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 ); + } + } } @@ -769,14 +908,18 @@ bool TheoryEngineModelBuilder::buildModel(Model* m) 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); @@ -967,7 +1110,7 @@ bool TheoryEngineModelBuilder::buildModel(Model* m) Assert(!assignOne); // check for infinite loop! assignOne = true; } - } + } #ifdef CVC4_ASSERTIONS // Assert that all representatives have been converted to constants @@ -1021,16 +1164,13 @@ void TheoryEngineModelBuilder::debugCheckModel(Model* m){ for (eqcs_i = eq::EqClassesIterator(tm->d_equalityEngine); !eqcs_i.isFinished(); ++eqcs_i) { // eqc is the equivalence class representative Node eqc = (*eqcs_i); - Node rep; - itMap = d_constantReps.find(eqc); - if (itMap == d_constantReps.end() && eqc.getType().isBoolean()) { + // 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()); } - else { - Assert(itMap != d_constantReps.end()); - rep = itMap->second; - } eq::EqClassIterator eqc_i = eq::EqClassIterator(eqc, tm->d_equalityEngine); for ( ; !eqc_i.isFinished(); ++eqc_i) { Node n = *eqc_i; @@ -1049,6 +1189,8 @@ void TheoryEngineModelBuilder::debugCheckModel(Model* m){ } } #endif /* CVC4_ASSERTIONS */ + + // builder-specific debugging debugModel( tm ); } @@ -1062,6 +1204,7 @@ Node TheoryEngineModelBuilder::normalize(TheoryModel* m, TNode r, bool evalOnly) 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; @@ -1107,44 +1250,170 @@ bool TheoryEngineModelBuilder::preProcessBuildModel(TheoryModel* m) { } bool TheoryEngineModelBuilder::processBuildModel(TheoryModel* m){ - Trace("model-builder") << "Assigning function values..." << endl; - //construct function values - for( std::map< Node, std::vector< Node > >::iterator it = m->d_uf_terms.begin(); it != m->d_uf_terms.end(); ++it ){ - Node n = it->first; - if( m->d_uf_models.find( n )==m->d_uf_models.end() ){ - TypeNode type = n.getType(); - Trace("model-builder") << " Assign function value for " << n << " " << type << std::endl; - uf::UfModelTree ufmt( n ); - Node default_v, un, simp, v; - for( size_t i=0; isecond.size(); i++ ){ - un = it->second[i]; - vector children; - children.push_back(n); - for (size_t j = 0; j < un.getNumChildren(); ++j) { - children.push_back(m->getRepresentative(un[j])); + 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(un.getKind(), children); - 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(type.getRangeType()); - default_v = (*te); + Assert( largs.size()==apply_args.size() ); + hnv = hnv[1].substitute( largs.begin(), largs.end(), apply_args.begin(), apply_args.end() ); + hnv = Rewriter::rewrite( hnv ); } - ufmt.setDefaultValue( m, default_v ); - if(options::condenseFunctionValues()) { - ufmt.simplify(); - } - Node val = ufmt.getFunctionValue( "_ufmt_", options::condenseFunctionValues() ); - Trace("model-builder") << " Assigning (" << n << ") to (" << val << ")" << endl; - m->d_uf_models[n] = val; - //ufmt.debugPrint( std::cout, m ); + Assert( !TypeNode::leastCommonTypeNode( hnv.getType(), curr.getType() ).isNull() ); + curr = NodeManager::currentNM()->mkNode( kind::ITE, hni, hnv, curr ); } } - return true; + 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 */ diff --git a/src/theory/theory_model.h b/src/theory/theory_model.h index 6c9e706d4..00dd215e9 100644 --- a/src/theory/theory_model.h +++ b/src/theory/theory_model.h @@ -130,12 +130,30 @@ public: void printRepresentativeDebug( const char* c, Node r ); /** print representative function */ void printRepresentative( std::ostream& out, Node r ); +private: + /** 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. + */ + std::map< Node, Node > d_uf_models; public: /** whether function models are enabled */ bool d_enableFuncModels; - //necessary information for function models + /** a map from functions f to a list of all APPLY_UF terms with operator f */ std::map< Node, std::vector< Node > > d_uf_terms; - std::map< Node, Node > d_uf_models; + /** a map from functions f to a list of all HO_APPLY terms with first argument f */ + std::map< Node, std::vector< Node > > d_ho_uf_terms; + /** assign function value f to definition f_def */ + void assignFunctionDefinition( Node f, Node f_def ); + /** have we assigned function f? */ + bool hasAssignedFunctionDefinition( Node f ) const { return d_uf_models.find( f )!=d_uf_models.end(); } + /** get the list of functions to assign. + * This list will contain all terms of function type that are terms in d_equalityEngine. + * If higher-order is enabled, we ensure that this list is sorted by type size. + * This allows us to assign functions T -> T before ( T x T ) -> T and before ( T -> T ) -> T, + * which is required for "dag form" model construction (see TheoryModelBuilder::assignHoFunction). + */ + std::vector< Node > getFunctionsToAssign(); };/* class TheoryModel */ /* @@ -307,6 +325,48 @@ protected: /** 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(){} -- 2.30.2