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, 151 insertions, 5 deletions

diff --git a/src/smt/options b/src/smt/options
index bb0cf1a00..81891acf7 100644
--- a/src/smt/options
+++ b/src/smt/options
@@ -32,6 +32,8 @@ option doStaticLearning static-learning /--no-static-learning bool :default true
 
 common-option produceModels produce-models -m --produce-models bool :predicate CVC4::SmtEngine::beforeSearch :predicate-include "smt/smt_engine.h"
  support the get-value and get-model commands
+option checkModels check-models --check-models bool :predicate CVC4::SmtEngine::beforeSearch :predicate-include "smt/smt_engine.h"
+ after SAT/INVALID, double-check that the generated model satisfies all user assertions
 common-option produceAssignments produce-assignments --produce-assignments bool
  support the get-assignment command
 option modelFormatMode --model-format=MODE ModelFormatMode :handler CVC4::smt::stringToModelFormatMode :default MODEL_FORMAT_MODE_DEFAULT :read-write :include "smt/model_format_mode.h" :handler-include "smt/options_handlers.h"
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index b9732c32e..ba7973405 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -280,7 +280,8 @@ SmtEngine::SmtEngine(ExprManager* em) throw(AssertionException) :
   d_theoryPreprocessTime("smt::SmtEngine::theoryPreprocessTime"),
   d_cnfConversionTime("smt::SmtEngine::cnfConversionTime"),
   d_numAssertionsPre("smt::SmtEngine::numAssertionsPreITERemoval", 0),
-  d_numAssertionsPost("smt::SmtEngine::numAssertionsPostITERemoval", 0) {
+  d_numAssertionsPost("smt::SmtEngine::numAssertionsPostITERemoval", 0),
+  d_checkModelTime("smt::SmtEngine::checkModelTime") {
 
   SmtScope smts(this);
 
@@ -295,6 +296,7 @@ SmtEngine::SmtEngine(ExprManager* em) throw(AssertionException) :
   StatisticsRegistry::registerStat(&d_cnfConversionTime);
   StatisticsRegistry::registerStat(&d_numAssertionsPre);
   StatisticsRegistry::registerStat(&d_numAssertionsPost);
+  StatisticsRegistry::registerStat(&d_checkModelTime);
 
   // We have mutual dependency here, so we add the prop engine to the theory
   // engine later (it is non-essential there)
@@ -355,6 +357,17 @@ void SmtEngine::finalOptionsAreSet() {
     return;
   }
 
+  if(options::checkModels()) {
+    if(! options::produceModels()) {
+      Notice() << "SmtEngine: turning on produce-models to support check-model" << std::endl;
+      setOption("produce-models", SExpr("true"));
+    }
+    if(! options::interactive()) {
+      Notice() << "SmtEngine: turning on interactive-mode to support check-model" << std::endl;
+      setOption("interactive-mode", SExpr("true"));
+    }
+  }
+
   if(! d_logic.isLocked()) {
     // ensure that our heuristics are properly set up
     setLogicInternal();
@@ -430,6 +443,7 @@ SmtEngine::~SmtEngine() throw() {
     StatisticsRegistry::unregisterStat(&d_cnfConversionTime);
     StatisticsRegistry::unregisterStat(&d_numAssertionsPre);
     StatisticsRegistry::unregisterStat(&d_numAssertionsPost);
+    StatisticsRegistry::unregisterStat(&d_checkModelTime);
 
     delete d_private;
 
@@ -819,6 +833,7 @@ void SmtEngine::defineFunction(Expr func,
   // Permit (check-sat) (define-fun ...) (get-value ...) sequences.
   // Otherwise, (check-sat) (get-value ((! foo :named bar))) breaks
   // d_haveAdditions = true;
+  Debug("smt") << "definedFunctions insert " << funcNode << " " << formulaNode << std::endl;
   d_definedFunctions->insert(funcNode, def);
 }
 
@@ -1634,8 +1649,13 @@ Result SmtEngine::checkSat(const BoolExpr& e) throw(TypeCheckingException) {
 
   Trace("smt") << "SmtEngine::checkSat(" << e << ") => " << r << endl;
 
+  // Check that SAT results generate a model correctly.
+  if(options::checkModels() && r.asSatisfiabilityResult() == Result::SAT) {
+    checkModel();
+  }
+
   return r;
-}
+}/* SmtEngine::checkSat() */
 
 Result SmtEngine::query(const BoolExpr& e) throw(TypeCheckingException) {
 
@@ -1694,8 +1714,13 @@ Result SmtEngine::query(const BoolExpr& e) throw(TypeCheckingException) {
 
   Trace("smt") << "SMT query(" << e << ") ==> " << r << endl;
 
+  // Check that SAT results generate a model correctly.
+  if(options::checkModels() && r.asSatisfiabilityResult() == Result::SAT) {
+    checkModel();
+  }
+
   return r;
-}
+}/* SmtEngine::query() */
 
 Result SmtEngine::assertFormula(const BoolExpr& e) throw(TypeCheckingException) {
   Assert(e.getExprManager() == d_exprManager);
@@ -1877,7 +1902,7 @@ void SmtEngine::addToModelCommand( Command* c, int c_type ){
   }
 }
 
-Model* SmtEngine::getModel() throw(ModalException, AssertionException){
+Model* SmtEngine::getModel() throw(ModalException, AssertionException) {
   Trace("smt") << "SMT getModel()" << endl;
   SmtScope smts(this);
 
@@ -1888,7 +1913,7 @@ Model* SmtEngine::getModel() throw(ModalException, AssertionException){
   }
 
   if(d_status.isNull() ||
-     d_status.asSatisfiabilityResult() == Result::UNSAT  ||
+     d_status.asSatisfiabilityResult() == Result::UNSAT ||
      d_problemExtended) {
     const char* msg =
       "Cannot get the current model unless immediately "
@@ -1903,6 +1928,117 @@ Model* SmtEngine::getModel() throw(ModalException, AssertionException){
   return d_theoryEngine->getModel();
 }
 
+void SmtEngine::checkModel() throw(InternalErrorException) {
+  // --check-model implies --interactive, which enables the assertion list,
+  // so we should be ok.
+  Assert(d_assertionList != NULL, "don't have an assertion list to check in SmtEngine::checkModel()");
+
+  TimerStat::CodeTimer checkModelTimer(d_checkModelTime);
+
+  // Throughout, we use Notice() to give diagnostic output.
+  //
+  // If this function is running, the user gave --check-model (or equivalent),
+  // and if Notice() is on, the user gave --verbose (or equivalent).
+
+  Notice() << "SmtEngine::checkModel(): generating model" << endl;
+  theory::TheoryModel* m = d_theoryEngine->getModel();
+  if(Notice.isOn()) {
+    printModel(Notice.getStream(), m);
+  }
+
+  // We have a "fake context" for the substitution map (we don't need it
+  // to be context-dependent)
+  context::Context fakeContext;
+  theory::SubstitutionMap substitutions(&fakeContext);
+
+  for(size_t k = 0; k < m->getNumCommands(); ++k) {
+    DeclareFunctionCommand* c = dynamic_cast<DeclareFunctionCommand*>(m->getCommand(k));
+    Notice() << "SmtEngine::checkModel(): model command " << k << " : " << m->getCommand(k) << endl;
+    if(c == NULL) {
+      // we don't care about DECLARE-DATATYPES, DECLARE-SORT, ...
+      Notice() << "SmtEngine::checkModel(): skipping..." << endl;
+    } else {
+      // We have a DECLARE-FUN:
+      //
+      // We'll first do some checks, then add to our substitution map
+      // the mapping: function symbol |-> value
+
+      Expr func = c->getFunction();
+      Node val = m->getValue(func);
+
+      Notice() << "SmtEngine::checkModel(): adding substitution: " << func << " |-> " << val << endl;
+
+      // (1) check that the value is actually a value
+      if(!val.isConst()) {
+        Notice() << "SmtEngine::checkModel(): *** PROBLEM: MODEL VALUE NOT A CONSTANT ***" << endl;
+        stringstream ss;
+        ss << "SmtEngine::checkModel(): ERRORS SATISFYING ASSERTIONS WITH MODEL:" << endl
+           << "model value for " << func << endl
+           << "             is " << val << endl
+           << "and that is not a constant (.isConst() == false)." << endl
+           << "Run with `--check-models -v' for additional diagnostics.";
+        InternalError(ss.str());
+      }
+
+      // (2) if the value is a lambda, ensure the lambda doesn't contain the
+      // function symbol (since then the definition is recursive)
+      if(val.getKind() == kind::LAMBDA) {
+        // first apply the model substitutions we have so far
+        Node n = substitutions.apply(val[1]);
+        // now check if n contains func by doing a substitution
+        // [func->func2] and checking equality of the Nodes.
+        // (this just a way to check if func is in n.)
+        theory::SubstitutionMap subs(&fakeContext);
+        Node func2 = NodeManager::currentNM()->mkSkolem(TypeNode::fromType(func.getType()));
+        subs.addSubstitution(func, func2);
+        if(subs.apply(n) != n) {
+          Notice() << "SmtEngine::checkModel(): *** PROBLEM: MODEL VALUE DEFINED IN TERMS OF ITSELF ***" << endl;
+          stringstream ss;
+          ss << "SmtEngine::checkModel(): ERRORS SATISFYING ASSERTIONS WITH MODEL:" << endl
+             << "considering model value for " << func << endl
+             << "body of lambda is:   " << val << endl;
+          if(n != val[1]) {
+            ss << "body substitutes to: " << n << endl;
+          }
+          ss << "so " << func << " is defined in terms of itself." << endl
+             << "Run with `--check-models -v' for additional diagnostics.";
+          InternalError(ss.str());
+        }
+      }
+
+      // (3) checks complete, add the substitution
+      substitutions.addSubstitution(func, val);
+    }
+  }
+
+  // Now go through all our user assertions checking if they're satisfied.
+  for(AssertionList::const_iterator i = d_assertionList->begin(); i != d_assertionList->end(); ++i) {
+    Notice() << "SmtEngine::checkModel(): checking assertion " << *i << endl;
+    Node n = Node::fromExpr(*i);
+
+    // Apply our model value substitutions.
+    n = substitutions.apply(n);
+    Notice() << "SmtEngine::checkModel(): -- substitutes to " << n << endl;
+
+    // Simplify the result.
+    n = Node::fromExpr(simplify(n.toExpr()));
+    Notice() << "SmtEngine::checkModel(): -- simplifies to  " << n << endl;
+
+    // The result should be == true.
+    if(n != NodeManager::currentNM()->mkConst(true)) {
+      Notice() << "SmtEngine::checkModel(): *** PROBLEM: EXPECTED `TRUE' ***" << endl;
+      stringstream ss;
+      ss << "SmtEngine::checkModel(): ERRORS SATISFYING ASSERTIONS WITH MODEL:" << endl
+         << "assertion:     " << *i << endl
+         << "simplifies to: " << n << endl
+         << "expected `true'." << endl
+         << "Run with `--check-models -v' for additional diagnostics.";
+      InternalError(ss.str());
+    }
+  }
+  Notice() << "SmtEngine::checkModel(): all assertions checked out OK !" << endl;
+}
+
 Proof* SmtEngine::getProof() throw(ModalException, AssertionException) {
   Trace("smt") << "SMT getProof()" << endl;
   SmtScope smts(this);
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 2c99bc7eb..5b3229dea 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -198,6 +198,12 @@ class CVC4_PUBLIC SmtEngine {
   smt::SmtEnginePrivate* d_private;
 
   /**
+   * Check that a generated Model (via getModel()) actually satisfies
+   * all user assertions.
+   */
+  void checkModel() throw(InternalErrorException);
+
+  /**
    * This is something of an "init" procedure, but is idempotent; call
    * as often as you like.  Should be called whenever the final options
    * and logic for the problem are set (at least, those options that are
@@ -281,6 +287,8 @@ class CVC4_PUBLIC SmtEngine {
   IntStat d_numAssertionsPre;
   /** Num of assertions after ite removal */
   IntStat d_numAssertionsPost;
+  /** time spent in checkModel() */
+  TimerStat d_checkModelTime;
 
 public: