Branch data     Line data    Source code

       1                 :            : /******************************************************************************
       2                 :            :  * Top contributors (to current version):
       3                 :            :  *   Andrew Reynolds, Gereon Kremer, Morgan Deters
       4                 :            :  *
       5                 :            :  * This file is part of the cvc5 project.
       6                 :            :  *
       7                 :            :  * Copyright (c) 2009-2024 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.
      11                 :            :  * ****************************************************************************
      12                 :            :  *
      13                 :            :  * Utility for constructing and maintaining abstract values.
      14                 :            :  */
      15                 :            : 
      16                 :            : #include "smt/check_models.h"
      17                 :            : 
      18                 :            : #include "base/modal_exception.h"
      19                 :            : #include "options/quantifiers_options.h"
      20                 :            : #include "options/smt_options.h"
      21                 :            : #include "smt/env.h"
      22                 :            : #include "smt/expand_definitions.h"
      23                 :            : #include "smt/preprocessor.h"
      24                 :            : #include "smt/smt_solver.h"
      25                 :            : #include "theory/rewriter.h"
      26                 :            : #include "theory/theory_model.h"
      27                 :            : #include "theory/trust_substitutions.h"
      28                 :            : 
      29                 :            : using namespace cvc5::internal::theory;
      30                 :            : 
      31                 :            : namespace cvc5::internal {
      32                 :            : namespace smt {
      33                 :            : 
      34                 :       2336 : CheckModels::CheckModels(Env& e) : EnvObj(e) {}
      35                 :            : 
      36                 :       2994 : void CheckModels::checkModel(TheoryModel* m,
      37                 :            :                              const context::CDList<Node>& al,
      38                 :            :                              bool hardFailure)
      39                 :            : {
      40                 :            :   // Throughout, we use verbose(1) to give diagnostic output.
      41                 :            :   //
      42                 :            :   // If this function is running, the user gave --check-model (or equivalent),
      43                 :            :   // and if verbose(1) is on, the user gave --verbose (or equivalent).
      44                 :            : 
      45                 :       2994 :   Node sepHeap, sepNeq;
      46         [ -  + ]:       2994 :   if (m->getHeapModel(sepHeap, sepNeq))
      47                 :            :   {
      48                 :            :     throw RecoverableModalException(
      49                 :          0 :         "Cannot run check-model on a model with a separation logic heap.");
      50                 :            :   }
      51         [ +  + ]:       2994 :   if (options().quantifiers.fmfFunWellDefined)
      52                 :            :   {
      53                 :          4 :     warning() << "Running check-model is not guaranteed to pass when fmf-fun "
      54                 :          4 :                  "is enabled."
      55                 :          4 :               << std::endl;
      56                 :            :     // only throw warning
      57                 :          4 :     hardFailure = false;
      58                 :            :   }
      59                 :            :   // expand definitions module and substitutions
      60                 :       2994 :   std::unordered_map<Node, Node> ecache;
      61                 :       2994 :   ExpandDefs expDef(d_env);
      62                 :            : 
      63                 :       2994 :   theory::SubstitutionMap& sm = d_env.getTopLevelSubstitutions().get();
      64         [ +  - ]:       2994 :   Trace("check-model") << "checkModel: Check assertions..." << std::endl;
      65                 :       2994 :   std::unordered_map<Node, Node> cache;
      66                 :            :   // the list of assertions that did not rewrite to true
      67                 :       2994 :   std::vector<Node> noCheckList;
      68                 :            :   // Now go through all our user assertions checking if they're satisfied.
      69         [ +  + ]:      26834 :   for (const Node& assertion : al)
      70                 :            :   {
      71                 :      47680 :     verbose(1) << "SolverEngine::checkModel(): checking assertion " << assertion
      72                 :      23840 :                << std::endl;
      73                 :            : 
      74                 :            :     // Apply any define-funs from the problem. We do not expand theory symbols
      75                 :            :     // like integer division here. Hence, the code below is not able to properly
      76                 :            :     // evaluate e.g. divide-by-zero. This is intentional since the evaluation
      77                 :            :     // is not trustworthy, since the UF introduced by expanding definitions may
      78                 :            :     // not be properly constrained.
      79                 :      23840 :     Node n = sm.apply(assertion);
      80                 :      47680 :     verbose(1) << "SolverEngine::checkModel(): -- substitutes to " << n
      81                 :      23840 :                << std::endl;
      82                 :            : 
      83                 :            :     // Expand definitions, which is required for being accurate for operators
      84                 :            :     // that expand involving skolems during preprocessing. Not doing this will
      85                 :            :     // increase the spurious warnings raised by this class.
      86                 :      23840 :     n = expDef.expandDefinitions(n, cache);
      87                 :      47680 :     verbose(1) << "SolverEngine::checkModel(): -- expands to " << n
      88                 :      23840 :                << std::endl;
      89                 :            : 
      90                 :      23840 :     n = rewrite(n);
      91                 :      47680 :     verbose(1) << "SolverEngine::checkModel(): -- rewrites to " << n
      92                 :      23840 :                << std::endl;
      93                 :            : 
      94                 :            :     // We look up the value before simplifying. If n contains quantifiers,
      95                 :            :     // this may increases the chance of finding its value before the node is
      96                 :            :     // altered by simplification below.
      97                 :      23840 :     n = m->getValue(n);
      98                 :      47680 :     verbose(1) << "SolverEngine::checkModel(): -- get value : " << n
      99                 :      23840 :                << std::endl;
     100                 :            : 
     101 [ +  + ][ +  - ]:      23840 :     if (n.isConst() && n.getConst<bool>())
                 [ +  + ]
     102                 :            :     {
     103                 :            :       // assertion is true, everything is fine
     104                 :      23753 :       continue;
     105                 :            :     }
     106                 :            : 
     107                 :            :     // Otherwise, we did not succeed in showing the current assertion to be
     108                 :            :     // true. This may either indicate that our model is wrong, or that we cannot
     109                 :            :     // check it. The latter may be the case for several reasons.
     110                 :            :     // One example is the occurrence of partial operators. Another example
     111                 :            :     // are quantified formulas, which are not checkable, although we assign
     112                 :            :     // them to true/false based on the satisfying assignment. However,
     113                 :            :     // quantified formulas can be modified during preprocess, so they may not
     114                 :            :     // correspond to those in the satisfying assignment. Hence we throw
     115                 :            :     // warnings for assertions that do not simplify to either true or false.
     116                 :            :     // Other theories such as non-linear arithmetic (in particular,
     117                 :            :     // transcendental functions) also have the property of not being able to
     118                 :            :     // be checked precisely here.
     119                 :            :     // Note that warnings like these can be avoided for quantified formulas
     120                 :            :     // by making preprocessing passes explicitly record how they
     121                 :            :     // rewrite quantified formulas (see cvc4-wishues#43).
     122         [ +  - ]:         87 :     if (!n.isConst())
     123                 :            :     {
     124                 :            :       // Not constant, print a less severe warning message here.
     125                 :         87 :       warning()
     126                 :            :           << "Warning : SolverEngine::checkModel(): cannot check simplified "
     127                 :         87 :              "assertion : "
     128                 :         87 :           << n << std::endl;
     129                 :         87 :       noCheckList.push_back(n);
     130                 :         87 :       continue;
     131                 :            :     }
     132                 :            :     // Assertions that simplify to false result in an InternalError or
     133                 :            :     // Warning being thrown below (when hardFailure is false).
     134                 :          0 :     verbose(1) << "SolverEngine::checkModel(): *** PROBLEM: EXPECTED `TRUE' ***"
     135                 :          0 :                << std::endl;
     136                 :          0 :     std::stringstream ss;
     137                 :            :     ss << "SolverEngine::checkModel(): "
     138                 :          0 :        << "ERRORS SATISFYING ASSERTIONS WITH MODEL:" << std::endl
     139                 :          0 :        << "assertion:     " << assertion << std::endl
     140                 :          0 :        << "simplifies to: " << n << std::endl
     141                 :          0 :        << "expected `true'." << std::endl
     142                 :          0 :        << "Run with `--check-models -v' for additional diagnostics.";
     143         [ -  - ]:          0 :     if (hardFailure)
     144                 :            :     {
     145                 :            :       // internal error if hardFailure is true
     146                 :          0 :       InternalError() << ss.str();
     147                 :            :     }
     148                 :            :     else
     149                 :            :     {
     150                 :          0 :       warning() << ss.str() << std::endl;
     151                 :            :     }
     152                 :            :   }
     153         [ +  + ]:       2994 :   if (noCheckList.empty())
     154                 :            :   {
     155                 :       2925 :     verbose(1) << "SolverEngine::checkModel(): all assertions checked out OK !"
     156                 :       2925 :                << std::endl;
     157                 :       2925 :     return;
     158                 :            :   }
     159                 :            :   // if the noCheckList is non-empty, we could expand definitions on this list
     160                 :            :   // and check satisfiability
     161                 :            : 
     162         [ +  - ]:         69 :   Trace("check-model") << "checkModel: Finish" << std::endl;
     163                 :            : }
     164                 :            : 
     165                 :            : }  // namespace smt
     166                 :            : }  // namespace cvc5::internal