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)

3 files changed, 41 insertions, 30 deletions

diff --git a/src/printer/ast/ast_printer.cpp b/src/printer/ast/ast_printer.cpp
index 39d76728a..85742feef 100644
--- a/src/printer/ast/ast_printer.cpp
+++ b/src/printer/ast/ast_printer.cpp
@@ -152,6 +152,7 @@ void AstPrinter::toStream(std::ostream& out, const Command* c,
      tryToStream<DefineNamedFunctionCommand>(out, c) ||
      tryToStream<SimplifyCommand>(out, c) ||
      tryToStream<GetValueCommand>(out, c) ||
+     tryToStream<GetModelCommand>(out, c) ||
      tryToStream<GetAssignmentCommand>(out, c) ||
      tryToStream<GetAssertionsCommand>(out, c) ||
      tryToStream<SetBenchmarkStatusCommand>(out, c) ||
@@ -187,7 +188,7 @@ void AstPrinter::toStream(std::ostream& out, const CommandStatus* s) const throw
 }/* AstPrinter::toStream(CommandStatus*) */
 
 void AstPrinter::toStream(std::ostream& out, Model* m, Command* c, int c_type ) const throw(){
-
+  out << "Model()";
 }
 
 static void toStream(std::ostream& out, const EmptyCommand* c)  throw() {
@@ -293,6 +294,10 @@ static void toStream(std::ostream& out, const GetValueCommand* c) throw() {
   out << " >> )";
 }
 
+static void toStream(std::ostream& out, const GetModelCommand* c) throw() {
+  out << "GetModel()";
+}
+
 static void toStream(std::ostream& out, const GetAssignmentCommand* c) throw() {
   out << "GetAssignment()";
 }
diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp
index 5803ad23f..7f66d6fa0 100644
--- a/src/printer/cvc/cvc_printer.cpp
+++ b/src/printer/cvc/cvc_printer.cpp
@@ -98,7 +98,7 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo
     if(types) {
       // print the whole type, but not *its* type
       out << ":";
-      n.getType().toStream(out, -1, false, language::output::LANG_CVC4);
+      n.getType().toStream(out, -1, false, false, language::output::LANG_CVC4);
     }
     return;
   }
@@ -164,10 +164,11 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo
       break;
 
     default:
-      Warning() << "Constant printing not implemented for the case of " << n.getKind() << endl;
-      out << n.getKind();
-      break;
+      // fall back on whatever operator<< does on underlying type; we
+      // might luck out and print something reasonable
+      kind::metakind::NodeValueConstPrinter::toStream(out, n);
     }
+
     return;
   }
 
@@ -213,6 +214,10 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo
     case kind::TUPLE:
       // no-op
       break;
+    case kind::LAMBDA:
+      op << "LAMBDA";
+      opType = PREFIX;
+      break;
     case kind::APPLY:
       toStream(op, n.getOperator(), depth, types, true);
       break;
@@ -225,6 +230,7 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo
       }
     }
     break;
+
     // BOOL
     case kind::AND:
       op << "AND";
@@ -691,6 +697,7 @@ void CvcPrinter::toStream(std::ostream& out, const Command* c,
      tryToStream<DefineNamedFunctionCommand>(out, c) ||
      tryToStream<SimplifyCommand>(out, c) ||
      tryToStream<GetValueCommand>(out, c) ||
+     tryToStream<GetModelCommand>(out, c) ||
      tryToStream<GetAssignmentCommand>(out, c) ||
      tryToStream<GetAssertionsCommand>(out, c) ||
      tryToStream<SetBenchmarkStatusCommand>(out, c) ||
@@ -768,17 +775,7 @@ void CvcPrinter::toStream(std::ostream& out, Model* m, Command* c, int c_type )
     }else{
       out << tn;
     }
-    out << " = ";
-    if( tn.isFunction() || tn.isPredicate() ){
-      out << "LAMBDA (";
-      for( size_t i=0; i<tn.getNumChildren()-1; i++ ){
-        if( i>0 ) out << ", ";
-        out << "$x" << (i+1) << " : " << tn[i];
-      }
-      out << "): ";
-    }
-    out << tm->getValue( n );
-    out << ";" << std::endl;
+    out << " = " << tm->getValue( n ) << ";" << std::endl;
 
 /*
     //for table format (work in progress)
@@ -920,6 +917,10 @@ static void toStream(std::ostream& out, const GetValueCommand* c) throw() {
   out << " ))";
 }
 
+static void toStream(std::ostream& out, const GetModelCommand* c) throw() {
+  out << "% (get-model)";
+}
+
 static void toStream(std::ostream& out, const GetAssignmentCommand* c) throw() {
   out << "% (get-assignment)";
 }
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 9400b7732..8356f9e49 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -177,6 +177,12 @@ void Smt2Printer::toStream(std::ostream& out, TNode n,
       out << n.getConst<Datatype>().getName();
       break;
 
+    case kind::UNINTERPRETED_CONSTANT: {
+      const UninterpretedConstant& uc = n.getConst<UninterpretedConstant>();
+      out << '@' << uc;
+      break;
+    }
+
     default:
       // fall back on whatever operator<< does on underlying type; we
       // might luck out and be SMT-LIB v2 compliant
@@ -480,6 +486,7 @@ void Smt2Printer::toStream(std::ostream& out, const Command* c,
      tryToStream<DefineNamedFunctionCommand>(out, c) ||
      tryToStream<SimplifyCommand>(out, c) ||
      tryToStream<GetValueCommand>(out, c) ||
+     tryToStream<GetModelCommand>(out, c) ||
      tryToStream<GetAssignmentCommand>(out, c) ||
      tryToStream<GetAssertionsCommand>(out, c) ||
      tryToStream<SetBenchmarkStatusCommand>(out, c) ||
@@ -546,21 +553,15 @@ void Smt2Printer::toStream(std::ostream& out, Model* m, Command* c, int c_type )
     }
   }else if( c_type==Model::COMMAND_DECLARE_FUN ){
     Node n = Node::fromExpr( ((DeclareFunctionCommand*)c)->getFunction() );
-    TypeNode tn = n.getType();
-    out << "(define-fun " << n << " (";
-    if( tn.isFunction() || tn.isPredicate() ){
-      for( size_t i=0; i<tn.getNumChildren()-1; i++ ){
-        if( i>0 ) out << " ";
-        out << "($x" << (i+1) << " " << tn[i] << ")";
-      }
-      out << ") " << tn.getRangeType();
-    }else{
-      out << ") " << tn;
+    Node val = tm->getValue( n );
+    if(val.getKind() == kind::LAMBDA) {
+      out << "(define-fun " << n << " " << val[0]
+          << " " << n.getType().getRangeType()
+          << " " << val[1] << ")" << std::endl;
+    } else {
+      out << "(define-fun " << n << " () "
+          << n.getType() << " " << val << ")" << std::endl;
     }
-    out << " ";
-    out << tm->getValue( n );
-    out << ")" << std::endl;
-
 /*
     //for table format (work in progress)
     bool printedModel = false;
@@ -713,6 +714,10 @@ static void toStream(std::ostream& out, const GetValueCommand* c) throw() {
   out << " ))";
 }
 
+static void toStream(std::ostream& out, const GetModelCommand* c) throw() {
+  out << "(get-model)";
+}
+
 static void toStream(std::ostream& out, const GetAssignmentCommand* c) throw() {
   out << "(get-assignment)";
 }