src/smt/check_models.cpp

   1 /*********************                                                        */
   2 /*! \file check_models.cpp
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Andrew Reynolds
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
   8  ** in the top-level source directory and their institutional affiliations.
   9  ** All rights reserved.  See the file COPYING in the top-level source
  10  ** directory for licensing information.\endverbatim
  11  **
  12  ** \brief Utility for constructing and maintaining abstract values.
  13  **/
  14
  15 #include "smt/check_models.h"
  16
  17 #include "options/smt_options.h"
  18 #include "smt/node_command.h"
  19 #include "smt/preprocessor.h"
  20 #include "theory/rewriter.h"
  21 #include "theory/substitutions.h"
  22 #include "theory/theory_engine.h"
  23
  24 using namespace CVC4::theory;
  25
  26 namespace CVC4 {
  27 namespace smt {
  28
  29 CheckModels::CheckModels(SmtSolver& s) : d_smt(s) {}
  30 CheckModels::~CheckModels() {}
  31
  32 void CheckModels::checkModel(Model* m,
  33                              context::CDList<Node>* al,
  34                              bool hardFailure)
  35 {
  36   // Throughout, we use Notice() to give diagnostic output.
  37   //
  38   // If this function is running, the user gave --check-model (or equivalent),
  39   // and if Notice() is on, the user gave --verbose (or equivalent).
  40
  41   // check-model is not guaranteed to succeed if approximate values were used.
  42   // Thus, we intentionally abort here.
  43   if (m->hasApproximations())
  44   {
  45     throw RecoverableModalException(
  46         "Cannot run check-model on a model with approximate values.");
  47   }
  48
  49   // Check individual theory assertions
  50   if (options::debugCheckModels())
  51   {
  52     TheoryEngine* te = d_smt.getTheoryEngine();
  53     Assert(te != nullptr);
  54     te->checkTheoryAssertionsWithModel(hardFailure);
  55   }
  56
  57   // Output the model
  58   Notice() << *m;
  59
  60   NodeManager* nm = NodeManager::currentNM();
  61   Preprocessor* pp = d_smt.getPreprocessor();
  62
  63   // We have a "fake context" for the substitution map (we don't need it
  64   // to be context-dependent)
  65   context::Context fakeContext;
  66   SubstitutionMap substitutions(&fakeContext,
  67                                 /* substituteUnderQuantifiers = */ false);
  68
  69   Trace("check-model") << "checkModel: Collect substitution..." << std::endl;
  70   const std::vector<Node>& decTerms = m->getDeclaredTerms();
  71   for (const Node& func : decTerms)
  72   {
  73     // We have a DECLARE-FUN:
  74     //
  75     // We'll first do some checks, then add to our substitution map
  76     // the mapping: function symbol |-> value
  77
  78     Node val = m->getValue(func);
  79
  80     Notice() << "SmtEngine::checkModel(): adding substitution: " << func
  81              << " |-> " << val << std::endl;
  82
  83     // (1) if the value is a lambda, ensure the lambda doesn't contain the
  84     // function symbol (since then the definition is recursive)
  85     if (val.getKind() == kind::LAMBDA)
  86     {
  87       // first apply the model substitutions we have so far
  88       Node n = substitutions.apply(val[1]);
  89       // now check if n contains func by doing a substitution
  90       // [func->func2] and checking equality of the Nodes.
  91       // (this just a way to check if func is in n.)
  92       SubstitutionMap subs(&fakeContext);
  93       Node func2 =
  94           nm->mkSkolem("", func.getType(), "", NodeManager::SKOLEM_NO_NOTIFY);
  95       subs.addSubstitution(func, func2);
  96       if (subs.apply(n) != n)
  97       {
  98         Notice() << "SmtEngine::checkModel(): *** PROBLEM: MODEL VALUE DEFINED "
  99                     "IN TERMS OF ITSELF ***"
 100                  << std::endl;
 101         std::stringstream ss;
 102         ss << "SmtEngine::checkModel(): ERRORS SATISFYING ASSERTIONS WITH "
 103               "MODEL:"
 104            << std::endl
 105            << "considering model value for " << func << std::endl
 106            << "body of lambda is:   " << val << std::endl;
 107         if (n != val[1])
 108         {
 109           ss << "body substitutes to: " << n << std::endl;
 110         }
 111         ss << "so " << func << " is defined in terms of itself." << std::endl
 112            << "Run with `--check-models -v' for additional diagnostics.";
 113         InternalError() << ss.str();
 114       }
 115     }
 116
 117     // (2) check that the value is actually a value
 118     else if (!val.isConst())
 119     {
 120       // This is only a warning since it could have been assigned an
 121       // unevaluable term (e.g. an application of a transcendental function).
 122       // This parallels the behavior (warnings for non-constant expressions)
 123       // when checking whether assertions are satisfied below.
 124       Warning() << "Warning : SmtEngine::checkModel(): "
 125                 << "model value for " << func << std::endl
 126                 << "             is " << val << std::endl
 127                 << "and that is not a constant (.isConst() == false)."
 128                 << std::endl
 129                 << "Run with `--check-models -v' for additional diagnostics."
 130                 << std::endl;
 131     }
 132
 133     // (3) check that it's the correct (sub)type
 134     // This was intended to be a more general check, but for now we can't do
 135     // that because e.g. "1" is an INT, which isn't a subrange type [1..10]
 136     // (etc.).
 137     else if (func.getType().isInteger() && !val.getType().isInteger())
 138     {
 139       Notice() << "SmtEngine::checkModel(): *** PROBLEM: MODEL VALUE NOT "
 140                   "CORRECT TYPE ***"
 141                << std::endl;
 142       InternalError()
 143           << "SmtEngine::checkModel(): ERRORS SATISFYING ASSERTIONS WITH "
 144              "MODEL:"
 145           << std::endl
 146           << "model value for " << func << std::endl
 147           << "             is " << val << std::endl
 148           << "value type is     " << val.getType() << std::endl
 149           << "should be of type " << func.getType() << std::endl
 150           << "Run with `--check-models -v' for additional diagnostics.";
 151     }
 152
 153     // (4) checks complete, add the substitution
 154     Trace("check-model") << "Substitution: " << func << " :=> " << val
 155                          << std::endl;
 156     substitutions.addSubstitution(func, val);
 157   }
 158
 159   Trace("check-model") << "checkModel: Check assertions..." << std::endl;
 160   std::unordered_map<Node, Node, NodeHashFunction> cache;
 161   // Now go through all our user assertions checking if they're satisfied.
 162   for (const Node& assertion : *al)
 163   {
 164     Notice() << "SmtEngine::checkModel(): checking assertion " << assertion
 165              << std::endl;
 166     Node n = assertion;
 167     Notice() << "SmtEngine::checkModel(): -- rewritten form is " << Rewriter::rewrite(n) << std::endl;
 168     Node nr = Rewriter::rewrite(substitutions.apply(n));
 169     if (nr.isConst() && nr.getConst<bool>())
 170     {
 171       continue;
 172     }
 173     // Apply any define-funs from the problem.
 174     n = pp->expandDefinitions(n, cache);
 175     Notice() << "SmtEngine::checkModel(): -- expands to " << n << std::endl;
 176
 177     // Apply our model value substitutions.
 178     n = substitutions.apply(n);
 179     Notice() << "SmtEngine::checkModel(): -- substitutes to " << n << std::endl;
 180
 181     // We look up the value before simplifying. If n contains quantifiers,
 182     // this may increases the chance of finding its value before the node is
 183     // altered by simplification below.
 184     n = m->getValue(n);
 185     Notice() << "SmtEngine::checkModel(): -- get value : " << n << std::endl;
 186
 187     // Simplify the result and replace the already-known ITEs (this is important
 188     // for ground ITEs under quantifiers).
 189     n = pp->simplify(n, true);
 190     Notice()
 191         << "SmtEngine::checkModel(): -- simplifies with ite replacement to  "
 192         << n << std::endl;
 193
 194     // Apply our model value substitutions (again), as things may have been
 195     // simplified.
 196     n = substitutions.apply(n);
 197     Notice() << "SmtEngine::checkModel(): -- re-substitutes to " << n
 198              << std::endl;
 199
 200     // As a last-ditch effort, ask model to simplify it.
 201     // Presently, this is only an issue for quantifiers, which can have a value
 202     // but don't show up in our substitution map above.
 203     n = m->getValue(n);
 204     Notice() << "SmtEngine::checkModel(): -- model-substitutes to " << n
 205              << std::endl;
 206
 207     if (n.isConst() && n.getConst<bool>())
 208     {
 209       // assertion is true, everything is fine
 210       continue;
 211     }
 212
 213     // Otherwise, we did not succeed in showing the current assertion to be
 214     // true. This may either indicate that our model is wrong, or that we cannot
 215     // check it. The latter may be the case for several reasons.
 216     // For example, quantified formulas are not checkable, although we assign
 217     // them to true/false based on the satisfying assignment. However,
 218     // quantified formulas can be modified during preprocess, so they may not
 219     // correspond to those in the satisfying assignment. Hence we throw
 220     // warnings for assertions that do not simplify to either true or false.
 221     // Other theories such as non-linear arithmetic (in particular,
 222     // transcendental functions) also have the property of not being able to
 223     // be checked precisely here.
 224     // Note that warnings like these can be avoided for quantified formulas
 225     // by making preprocessing passes explicitly record how they
 226     // rewrite quantified formulas (see cvc4-wishues#43).
 227     if (!n.isConst())
 228     {
 229       // Not constant, print a less severe warning message here.
 230       Warning() << "Warning : SmtEngine::checkModel(): cannot check simplified "
 231                    "assertion : "
 232                 << n << std::endl;
 233       continue;
 234     }
 235     // Assertions that simplify to false result in an InternalError or
 236     // Warning being thrown below (when hardFailure is false).
 237     Notice() << "SmtEngine::checkModel(): *** PROBLEM: EXPECTED `TRUE' ***"
 238              << std::endl;
 239     std::stringstream ss;
 240     ss << "SmtEngine::checkModel(): "
 241        << "ERRORS SATISFYING ASSERTIONS WITH MODEL:" << std::endl
 242        << "assertion:     " << assertion << std::endl
 243        << "simplifies to: " << n << std::endl
 244        << "expected `true'." << std::endl
 245        << "Run with `--check-models -v' for additional diagnostics.";
 246     if (hardFailure)
 247     {
 248       // internal error if hardFailure is true
 249       InternalError() << ss.str();
 250     }
 251     else
 252     {
 253       Warning() << ss.str() << std::endl;
 254     }
 255   }
 256   Trace("check-model") << "checkModel: Finish" << std::endl;
 257   Notice() << "SmtEngine::checkModel(): all assertions checked out OK !"
 258            << std::endl;
 259 }
 260
 261 }  // namespace smt
 262 }  // namespace CVC4