Adding model assertions after SAT responses.

To enable, use --check-models.  Turning on the option can be done in debug or optimized builds, regardless of whether normal assertions are on or not.  This is to allow us to check the generated models in long-running queries, and might be useful to end users as a double-check too.

By default, --check-models is quiet (no output unless it detects a problem).  That allows regression runs to pass unless there are problems:

  make regress CVC4_REGRESSION_ARGS=--check-models

To see it work, use -v in addition to --check-models.

There may still be bugs in the feature itself, but already I've found some apparent model-generation bugs (and discussed with Andy) from this feature, so it seems useful in its current state.

--check-models turns on what SMT-LIBv2 calls "interactive mode" (which keeps the list of user assertions around), and also implies --produce-models.  This version does NOT require incremental-mode, which one design did (the one mentioned in yesterday's meeting).

Also:

* TheoryUF::collectModelInfo() now generates UninterpretedConstants (rather than non-constants)
* The UF rewriter now reduces (APPLY_UF (LAMBDA...) args...), and treats uninterpreted constants correctly (e.g. uc_U_1 != uc_U_2)
* The SubstitutionMap now supports substitutions of operators for paramaterized kinds (e.g., function symbols)

9 files changed, 62 insertions, 33 deletions

diff --git a/src/theory/builtin/kinds b/src/theory/builtin/kinds
index c4c3435a2..1218f3809 100644
--- a/src/theory/builtin/kinds
+++ b/src/theory/builtin/kinds
@@ -341,6 +341,7 @@ typerule EQUAL ::CVC4::theory::builtin::EqualityTypeRule
 typerule DISTINCT ::CVC4::theory::builtin::DistinctTypeRule
 typerule TUPLE ::CVC4::theory::builtin::TupleTypeRule
 typerule LAMBDA ::CVC4::theory::builtin::LambdaTypeRule
+construle LAMBDA ::CVC4::theory::builtin::LambdaTypeRule
 
 constant SUBTYPE_TYPE \
     ::CVC4::Predicate \
diff --git a/src/theory/builtin/theory_builtin_type_rules.h b/src/theory/builtin/theory_builtin_type_rules.h
index 95ede1c46..7bc1d956d 100644
--- a/src/theory/builtin/theory_builtin_type_rules.h
+++ b/src/theory/builtin/theory_builtin_type_rules.h
@@ -161,6 +161,11 @@ public:
     TypeNode rangeType = n[1].getType(check);
     return nodeManager->mkFunctionType(argTypes, rangeType);
   }
+
+  inline static bool computeIsConst(NodeManager* nodeManager, TNode n) {
+    Assert(n.getKind() == kind::LAMBDA);
+    return true;
+  }
 };/* class LambdaTypeRule */
 
 class SortProperties {
diff --git a/src/theory/model.cpp b/src/theory/model.cpp
index ed2d69308..ee61c9345 100644
--- a/src/theory/model.cpp
+++ b/src/theory/model.cpp
@@ -98,7 +98,7 @@ Node TheoryModel::getModelValue( TNode n ){
   Trace("model") << "TheoryModel::getModelValue " << n << std::endl;
 
   //// special case: prop engine handles boolean vars
-  //if(metakind == kind::metakind::VARIABLE && n.getType().isBoolean()) {
+  //if(n.isVar() && n.getType().isBoolean()) {
   //  Trace("model") << "-> Propositional variable." << std::endl;
   //  return d_te->getPropEngine()->getValue( n );
   //}
diff --git a/src/theory/substitutions.cpp b/src/theory/substitutions.cpp
index b7c9278e1..b5f846735 100644
--- a/src/theory/substitutions.cpp
+++ b/src/theory/substitutions.cpp
@@ -75,7 +75,7 @@ Node SubstitutionMap::internalSubstitute(TNode t) {
       // Children have been processed, so substitute
       NodeBuilder<> builder(current.getKind());
       if (current.getMetaKind() == kind::metakind::PARAMETERIZED) {
-        builder << current.getOperator();
+        builder << Node(d_substitutionCache[current.getOperator()]);
       }
       for (unsigned i = 0; i < current.getNumChildren(); ++ i) {
         Assert(d_substitutionCache.find(current[i]) != d_substitutionCache.end());
@@ -105,8 +105,16 @@ Node SubstitutionMap::internalSubstitute(TNode t) {
       toVisit.pop_back();
     } else {
       // Mark that we have added the children if any
-      if (current.getNumChildren() > 0) {
+      if (current.getNumChildren() > 0 || current.getMetaKind() == kind::metakind::PARAMETERIZED) {
         stackHead.children_added = true;
+        // We need to add the operator, if any
+        if(current.getMetaKind() == kind::metakind::PARAMETERIZED) {
+          TNode opNode = current.getOperator();
+          NodeCache::iterator opFind = d_substitutionCache.find(opNode);
+          if (opFind == d_substitutionCache.end()) {
+            toVisit.push_back(opNode);
+          }
+        }
         // We need to add the children
         for(TNode::iterator child_it = current.begin(); child_it != current.end(); ++ child_it) {
           TNode childNode = *child_it;
@@ -255,6 +263,10 @@ void SubstitutionMap::addSubstitution(TNode x, TNode t, bool invalidateCache)
   Debug("substitution") << "SubstitutionMap::addSubstitution(" << x << ", " << t << ")" << std::endl;
   Assert(d_substitutions.find(x) == d_substitutions.end());
 
+  // this causes a later assert-fail (the rhs != current one, above) anyway
+  // putting it here is easier to diagnose
+  Assert(x != t, "cannot substitute a term for itself");
+
   d_substitutions[x] = t;
 
   // Also invalidate the cache if necessary
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index b0a290b7d..c9fb36830 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -85,7 +85,7 @@ TheoryEngine::TheoryEngine(context::Context* context,
   // initialize the quantifiers engine
   d_quantEngine = new QuantifiersEngine(context, this);
 
-  //build model information if applicable
+  // build model information if applicable
   d_curr_model = new theory::DefaultModel( context, "DefaultModel", true );
   d_curr_model_builder = new theory::TheoryEngineModelBuilder( this );
 
@@ -105,6 +105,9 @@ TheoryEngine::~TheoryEngine() {
     }
   }
 
+  delete d_curr_model_builder;
+  delete d_curr_model;
+
   delete d_quantEngine;
 
   StatisticsRegistry::unregisterStat(&d_combineTheoriesTime);
diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
index a1500e084..9809b948e 100644
--- a/src/theory/uf/theory_uf.cpp
+++ b/src/theory/uf/theory_uf.cpp
@@ -195,31 +195,6 @@ Node TheoryUF::explain(TNode literal) {
 void TheoryUF::collectModelInfo( TheoryModel* m, bool fullModel ){
   m->assertEqualityEngine( &d_equalityEngine );
   if( fullModel ){
-#if 1
-    std::map< TypeNode, int > type_count;
-    //must choose proper representatives
-    // for each equivalence class, specify the constructor as a representative
-    eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine );
-    while( !eqcs_i.isFinished() ){
-      Node eqc = (*eqcs_i);
-      TypeNode tn = eqc.getType();
-      if( tn.isSort() ){
-        if( type_count.find( tn )==type_count.end() ){
-          type_count[tn] = 0;
-        }
-        std::stringstream ss;
-        ss << Expr::setlanguage(options::outputLanguage());
-        ss << "$t_" << tn << (type_count[tn]+1);
-        type_count[tn]++;
-        Node rep = NodeManager::currentNM()->mkSkolem( ss.str(), tn );
-        Trace("mkVar") << "TheoryUF::collectModelInfo:  make variable " << rep << " : " << tn << std::endl;
-        //specify the constant as the representative
-        m->assertEquality( eqc, rep, true );
-        m->assertRepresentative( rep );
-      }
-      ++eqcs_i;
-    }
-#else
     std::map< TypeNode, TypeEnumerator* > type_enums;
     //must choose proper representatives
     // for each equivalence class, specify the constructor as a representative
@@ -239,7 +214,6 @@ void TheoryUF::collectModelInfo( TheoryModel* m, bool fullModel ){
       }
       ++eqcs_i;
     }
- #endif
   }
 }
 
diff --git a/src/theory/uf/theory_uf_model.cpp b/src/theory/uf/theory_uf_model.cpp
index b8110a2aa..8c79f69df 100644
--- a/src/theory/uf/theory_uf_model.cpp
+++ b/src/theory/uf/theory_uf_model.cpp
@@ -268,7 +268,7 @@ Node UfModelTree::getFunctionValue( const char* argPrefix ){
   for( size_t i=0; i<type.getNumChildren()-1; i++ ){
     std::stringstream ss;
     ss << argPrefix << (i+1);
-    vars.push_back( NodeManager::currentNM()->mkSkolem( ss.str(), type[i] ) );
+    vars.push_back( NodeManager::currentNM()->mkBoundVar( ss.str(), type[i] ) );
   }
   return getFunctionValue( vars );
 }
@@ -415,4 +415,4 @@ Node UfModelPreferenceData::getBestDefaultValue( Node defaultTerm, TheoryModel*
   Debug("fmf-model-cons") << "     # quantifiers pro = " << d_value_pro_con[0][defaultVal].size() << std::endl;
   Debug("fmf-model-cons") << "     # quantifiers con = " << d_value_pro_con[1][defaultVal].size() << std::endl;
   return defaultVal;
-}
\ No newline at end of file
+}
diff --git a/src/theory/uf/theory_uf_model.h b/src/theory/uf/theory_uf_model.h
index 61c0714a3..fd346bc3c 100644
--- a/src/theory/uf/theory_uf_model.h
+++ b/src/theory/uf/theory_uf_model.h
@@ -127,7 +127,11 @@ public:
   /** getFunctionValue
     *   Returns a representation of this function.
     */
-  Node getFunctionValue( std::vector< Node >& args ){ return d_tree.getFunctionValue( args, 0, Node::null() ); }
+  Node getFunctionValue( std::vector< Node >& args ){
+    Node body = d_tree.getFunctionValue( args, 0, Node::null() );
+    Node boundVarList = NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, args);
+    return NodeManager::currentNM()->mkNode(kind::LAMBDA, boundVarList, body);
+  }
   /** getFunctionValue for args with set prefix */
   Node getFunctionValue( const char* argPrefix );
   /** update
diff --git a/src/theory/uf/theory_uf_rewriter.h b/src/theory/uf/theory_uf_rewriter.h
index 8ba39f372..f70d89b30 100644
--- a/src/theory/uf/theory_uf_rewriter.h
+++ b/src/theory/uf/theory_uf_rewriter.h
@@ -36,12 +36,27 @@ public:
     if(node.getKind() == kind::EQUAL || node.getKind() == kind::IFF) {
       if(node[0] == node[1]) {
         return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(true));
+      } else if(node[0].isConst() && node[1].isConst()) {
+        // uninterpreted constants are all distinct
+        return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(false));
       }
       if (node[0] > node[1]) {
         Node newNode = NodeManager::currentNM()->mkNode(node.getKind(), node[1], node[0]);
         return RewriteResponse(REWRITE_DONE, newNode);
       }
     }
+    if(node.getKind() == kind::APPLY_UF && node.getOperator().getKind() == kind::LAMBDA) {
+      // resolve away the lambda
+      context::Context fakeContext;
+      theory::SubstitutionMap substitutions(&fakeContext);
+      TNode lambda = node.getOperator();
+      for(TNode::iterator formal = lambda[0].begin(), arg = node.begin(); formal != lambda[0].end(); ++formal, ++arg) {
+        // typechecking should ensure that the APPLY_UF is well-typed, correct arity, etc.
+        Assert(formal != node.end());
+        substitutions.addSubstitution(*formal, *arg);
+      }
+      return RewriteResponse(REWRITE_DONE, substitutions.apply(lambda[1]));
+    }
     return RewriteResponse(REWRITE_DONE, node);
   }
 
@@ -49,7 +64,22 @@ public:
     if(node.getKind() == kind::EQUAL || node.getKind() == kind::IFF) {
       if(node[0] == node[1]) {
         return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(true));
+      } else if(node[0].isConst() && node[1].isConst()) {
+        // uninterpreted constants are all distinct
+        return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(false));
+      }
+    }
+    if(node.getKind() == kind::APPLY_UF && node.getOperator().getKind() == kind::LAMBDA) {
+      // resolve away the lambda
+      context::Context fakeContext;
+      theory::SubstitutionMap substitutions(&fakeContext);
+      TNode lambda = node.getOperator();
+      for(TNode::iterator formal = lambda[0].begin(), arg = node.begin(); formal != lambda[0].end(); ++formal, ++arg) {
+        // typechecking should ensure that the APPLY_UF is well-typed, correct arity, etc.
+        Assert(formal != node.end());
+        substitutions.addSubstitution(*formal, *arg);
       }
+      return RewriteResponse(REWRITE_DONE, substitutions.apply(lambda[1]));
     }
     return RewriteResponse(REWRITE_DONE, node);
   }