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.

diff --git a/src/theory/quantifiers/fmf/full_model_check.cpp b/src/theory/quantifiers/fmf/full_model_check.cpp
index dcb674bd42b511848d6ca7adb7f76b2ddd2e23d7..be69617c79d44dba35b83d84c21fdd56b399bcc4 100644 (file)
--- 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 599e192f8f00c5d859f9e1ded4abcdc52f5f7fdb..a91a185a0486c94a252b16ea789ea013fd2394af 100644 (file)
--- 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 deffb595c9288519f1ac0905dbfd2d4f739ffcae..6d900b39edb3bc4a2b0ca98fb1fbfba88840d40a 100644 (file)
--- 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 34659031edfaa751c26a360078c064c36c5b221c..bc63aef97d3d64329ec234b96bf157c8064d0d20 100644 (file)
--- 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 fb6204b69001b82c4498216fe06389b2b92c943a..b716ad7d8a8b89755dd83f3cca3fa3d5284b9301 100644 (file)
--- 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