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)

1 files changed, 14 insertions, 2 deletions

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