From dd36a32c43f91652091c6f301d25dfc5f0204ccd Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 9 Nov 2021 11:17:22 -0600 Subject: [PATCH] Preparation for non-constant lambda models (#7604) This makes our core model construction amenable to (non-constant) lambdas as assignments to function equivalence classes for higher-order. We currently only generate almost constant functions for values of functions. After this PR, we allow explicitly provided lambdas as representatives provided by a theory, which will be used by the higher-order extension. It also makes some improvements to debug check models regarding checking when representatives are equal to their model values. --- .../quantifiers/fmf/full_model_check.cpp | 17 +++++++- src/theory/theory_model.cpp | 19 +++++++-- src/theory/theory_model.h | 2 +- src/theory/theory_model_builder.cpp | 42 ++++++++++++------- src/theory/theory_model_builder.h | 5 +++ 5 files changed, 64 insertions(+), 21 deletions(-) diff --git a/src/theory/quantifiers/fmf/full_model_check.cpp b/src/theory/quantifiers/fmf/full_model_check.cpp index dcb674bd4..be69617c7 100644 --- a/src/theory/quantifiers/fmf/full_model_check.cpp +++ b/src/theory/quantifiers/fmf/full_model_check.cpp @@ -399,6 +399,12 @@ bool FullModelChecker::processBuildModel(TheoryModel* m){ //reset the model d_fm->d_models[op]->reset(); + // if we've already assigned the function, ignore + if (m->hasAssignedFunctionDefinition(op)) + { + continue; + } + std::vector< Node > add_conds; std::vector< Node > add_values; bool needsDefault = true; @@ -539,8 +545,15 @@ bool FullModelChecker::processBuildModel(TheoryModel* m){ //make function values for( std::map::iterator it = fm->d_models.begin(); it != fm->d_models.end(); ++it ){ - Node f_def = getFunctionValue( fm, it->first, "$x" ); - m->assignFunctionDefinition( it->first, f_def ); + // For lazy lambda lifting, a function may already have been assigned + // during uf::HoExtension's collectModelValues method. In this case, + // the Def in it->second was not used, as all such functions are eagerly + // eliminated. + if (!m->hasAssignedFunctionDefinition(it->first)) + { + Node f_def = getFunctionValue(fm, it->first, "$x"); + m->assignFunctionDefinition(it->first, f_def); + } } return TheoryEngineModelBuilder::processBuildModel( m ); } diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp index 599e192f8..a91a185a0 100644 --- a/src/theory/theory_model.cpp +++ b/src/theory/theory_model.cpp @@ -690,11 +690,13 @@ void TheoryModel::assignFunctionDefinition( Node f, Node f_def ) { if (logicInfo().isHigherOrder()) { - //we must rewrite the function value since the definition needs to be a constant value + // we must rewrite the function value since the definition needs to be a + // constant value. This does not need to be the case if we are assigning a + // lambda to the equivalence class in isolation, so we do not assert that + // f_def is constant here. f_def = rewrite(f_def); Trace("model-builder-debug") << "Model value (post-rewrite) : " << f_def << std::endl; - Assert(f_def.isConst()) << "Non-constant f_def: " << f_def; } // d_uf_models only stores models for variables @@ -715,7 +717,8 @@ void TheoryModel::assignFunctionDefinition( Node f, Node f_def ) { 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 ) ){ + if (n.isVar() && !hasAssignedFunctionDefinition(n)) + { d_uf_models[n] = f_def; Trace("model-builder") << " Assigning function (" << n << ") to function definition of " << f << std::endl; } @@ -725,6 +728,11 @@ void TheoryModel::assignFunctionDefinition( Node f, Node f_def ) { } } +bool TheoryModel::hasAssignedFunctionDefinition(Node f) const +{ + return d_uf_models.find(f) != d_uf_models.end(); +} + std::vector< Node > TheoryModel::getFunctionsToAssign() { std::vector< Node > funcs_to_assign; std::map< Node, Node > func_to_rep; @@ -733,6 +741,11 @@ std::vector< Node > TheoryModel::getFunctionsToAssign() { 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()); + // lambdas do not need assignments + if (n.getKind() == LAMBDA) + { + continue; + } // should not have been solved for in a substitution Assert(d_env.getTopLevelSubstitutions().apply(n) == n); if( !hasAssignedFunctionDefinition( n ) ){ diff --git a/src/theory/theory_model.h b/src/theory/theory_model.h index deffb595c..6d900b39e 100644 --- a/src/theory/theory_model.h +++ b/src/theory/theory_model.h @@ -340,7 +340,7 @@ class TheoryModel : protected EnvObj /** 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(); } + bool hasAssignedFunctionDefinition(Node f) const; /** 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. diff --git a/src/theory/theory_model_builder.cpp b/src/theory/theory_model_builder.cpp index 34659031e..bc63aef97 100644 --- a/src/theory/theory_model_builder.cpp +++ b/src/theory/theory_model_builder.cpp @@ -125,6 +125,11 @@ bool TheoryEngineModelBuilder::isAssignerActive(TheoryModel* tm, Assigner& a) return true; } +bool TheoryEngineModelBuilder::isValue(TNode n) +{ + return n.getKind() == kind::LAMBDA || n.isConst(); +} + bool TheoryEngineModelBuilder::isAssignable(TNode n) { if (n.getKind() == kind::SELECT || n.getKind() == kind::APPLY_SELECTOR_TOTAL) @@ -499,8 +504,10 @@ bool TheoryEngineModelBuilder::buildModel(TheoryModel* tm) tm->addTermInternal(n); // (2) Record constant representative or assign representative, if - // applicable - if (n.isConst()) + // applicable. We check if n is a value here, e.g. a term for which + // isConst returns true, or a lambda. The latter is required only for + // higher-order. + if (isValue(n)) { Assert(constRep.isNull()); constRep = n; @@ -984,9 +991,9 @@ bool TheoryEngineModelBuilder::buildModel(TheoryModel* tm) } else { + // Otherwise, we get the first value from the type enumerator. Trace("model-builder-debug") << "Get first value from finite type..." << std::endl; - // Otherwise, we get the first value from the type enumerator. TypeEnumerator te(t); n = *te; } @@ -1023,7 +1030,7 @@ bool TheoryEngineModelBuilder::buildModel(TheoryModel* tm) // Assert that all representatives have been converted to constants for (it = typeRepSet.begin(); it != typeRepSet.end(); ++it) { - set& repSet = TypeSet::getSet(it); + std::set& repSet = TypeSet::getSet(it); if (!repSet.empty()) { Trace("model-builder") << "***Non-empty repSet, size = " << repSet.size() @@ -1121,18 +1128,24 @@ void TheoryEngineModelBuilder::debugCheckModel(TheoryModel* tm) << "Representative " << rep << " of " << n << " violates type constraints (" << rep.getType() << " and " << n.getType() << ")"; - // non-linear mult is not necessarily accurate wrt getValue - if (n.getKind() != kind::NONLINEAR_MULT) + Node val = tm->getValue(*eqc_i); + if (val != rep) { - if (tm->getValue(*eqc_i) != rep) + std::stringstream err; + err << "Failed representative check:" << std::endl + << "( " << repCheckInstance << ") " + << "n: " << n << endl + << "getValue(n): " << tm->getValue(n) << std::endl + << "rep: " << rep << std::endl; + if (val.isConst() && rep.isConst()) + { + AlwaysAssert(val == rep) << err.str(); + } + else { - std::stringstream err; - err << "Failed representative check:" << std::endl - << "( " << repCheckInstance << ") " - << "n: " << n << endl - << "getValue(n): " << tm->getValue(n) << std::endl - << "rep: " << rep << std::endl; - AlwaysAssert(tm->getValue(*eqc_i) == rep) << err.str(); + // if it does not evaluate, it is just a warning, which may be the + // case for non-constant values, e.g. lambdas. + warning() << err.str(); } } } @@ -1302,7 +1315,6 @@ void TheoryEngineModelBuilder::assignHoFunction(TheoryModel* m, Node 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 = rewrite(args[0].eqNode(hni)); Node hnv = m->getRepresentative(hn); diff --git a/src/theory/theory_model_builder.h b/src/theory/theory_model_builder.h index fb6204b69..b716ad7d8 100644 --- a/src/theory/theory_model_builder.h +++ b/src/theory/theory_model_builder.h @@ -126,6 +126,11 @@ class TheoryEngineModelBuilder : protected EnvObj * state of the model m. */ Node evaluateEqc(TheoryModel* m, TNode r); + /** + * Is the node n a "value"? This is true if n is constant, or if n is a + * lambda. + */ + static bool isValue(TNode n); /** is n an assignable expression? * * A term n is an assignable expression if its value is unconstrained by a -- 2.30.2