summaryrefslogtreecommitdiff
path: root/src/theory
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory')
-rw-r--r--src/theory/quantifiers/fmf/full_model_check.cpp17
-rw-r--r--src/theory/theory_model.cpp19
-rw-r--r--src/theory/theory_model.h2
-rw-r--r--src/theory/theory_model_builder.cpp42
-rw-r--r--src/theory/theory_model_builder.h5
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<Node, Def * >::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<Node>& repSet = TypeSet::getSet(it);
+ std::set<Node>& 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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback