Branch data     Line data    Source code

       1                 :            : /******************************************************************************
       2                 :            :  * Top contributors (to current version):
       3                 :            :  *   Andrew Reynolds, Gereon Kremer, Aina Niemetz
       4                 :            :  *
       5                 :            :  * This file is part of the cvc5 project.
       6                 :            :  *
       7                 :            :  * Copyright (c) 2009-2025 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                 :          0 : void getTheoriesOf(Env& env, const Node& n, std::vector<TheoryId>& theories)
      35                 :            : {
      36                 :          0 :   std::unordered_set<TNode> visited;
      37                 :          0 :   std::vector<TNode> visit;
      38                 :          0 :   TNode cur;
      39                 :          0 :   visit.push_back(n);
      40                 :          0 :   do
      41                 :            :   {
      42                 :          0 :     cur = visit.back();
      43                 :          0 :     visit.pop_back();
      44         [ -  - ]:          0 :     if (visited.find(cur) == visited.end())
      45                 :            :     {
      46                 :          0 :       visited.insert(cur);
      47                 :            :       // get the theories of the term and its type
      48                 :          0 :       TheoryId tid = env.theoryOf(cur);
      49         [ -  - ]:          0 :       if (std::find(theories.begin(), theories.end(), tid) == theories.end())
      50                 :            :       {
      51                 :          0 :         theories.push_back(tid);
      52                 :            :       }
      53                 :          0 :       TheoryId ttid = env.theoryOf(cur.getType());
      54         [ -  - ]:          0 :       if (ttid!=tid)
      55                 :            :       {
      56         [ -  - ]:          0 :         if (std::find(theories.begin(), theories.end(), ttid) == theories.end())
      57                 :            :         {
      58                 :          0 :           theories.push_back(ttid);
      59                 :            :         }
      60                 :            :       }
      61                 :          0 :       visit.insert(visit.end(), cur.begin(), cur.end());
      62                 :            :     }
      63         [ -  - ]:          0 :   } while (!visit.empty());
      64                 :          0 : }
      65                 :            : 
      66                 :       2331 : CheckModels::CheckModels(Env& e) : EnvObj(e) {}
      67                 :            : 
      68                 :       2991 : void CheckModels::checkModel(TheoryModel* m,
      69                 :            :                              const context::CDList<Node>& al,
      70                 :            :                              bool hardFailure)
      71                 :            : {
      72                 :            :   // Throughout, we use verbose(1) to give diagnostic output.
      73                 :            :   //
      74                 :            :   // If this function is running, the user gave --check-model (or equivalent),
      75                 :            :   // and if verbose(1) is on, the user gave --verbose (or equivalent).
      76                 :            : 
      77                 :       2991 :   Node sepHeap, sepNeq;
      78         [ -  + ]:       2991 :   if (m->getHeapModel(sepHeap, sepNeq))
      79                 :            :   {
      80                 :            :     throw RecoverableModalException(
      81                 :          0 :         "Cannot run check-model on a model with a separation logic heap.");
      82                 :            :   }
      83         [ +  + ]:       2991 :   if (options().quantifiers.fmfFunWellDefined)
      84                 :            :   {
      85                 :          4 :     warning() << "Running check-model is not guaranteed to pass when fmf-fun "
      86                 :          4 :                  "is enabled."
      87                 :          4 :               << std::endl;
      88                 :            :     // only throw warning
      89                 :          4 :     hardFailure = false;
      90                 :            :   }
      91                 :            :   // expand definitions module and substitutions
      92                 :       2991 :   std::unordered_map<Node, Node> ecache;
      93                 :       2991 :   ExpandDefs expDef(d_env);
      94                 :            : 
      95                 :       2991 :   theory::SubstitutionMap& sm = d_env.getTopLevelSubstitutions().get();
      96         [ +  - ]:       2991 :   Trace("check-model") << "checkModel: Check assertions..." << std::endl;
      97                 :       2991 :   std::unordered_map<Node, Node> cache;
      98                 :            :   // the list of assertions that did not rewrite to true
      99                 :       2991 :   std::vector<Node> noCheckList;
     100                 :            :   // Now go through all our user assertions checking if they're satisfied.
     101         [ +  + ]:      26829 :   for (const Node& assertion : al)
     102                 :            :   {
     103                 :      47676 :     verbose(1) << "SolverEngine::checkModel(): checking assertion " << assertion
     104                 :      23838 :                << std::endl;
     105                 :            : 
     106                 :            :     // Apply any define-funs from the problem. We do not expand theory symbols
     107                 :            :     // like integer division here. Hence, the code below is not able to properly
     108                 :            :     // evaluate e.g. divide-by-zero. This is intentional since the evaluation
     109                 :            :     // is not trustworthy, since the UF introduced by expanding definitions may
     110                 :            :     // not be properly constrained.
     111                 :      23838 :     Node n = sm.apply(assertion);
     112                 :      47676 :     verbose(1) << "SolverEngine::checkModel(): -- substitutes to " << n
     113                 :      23838 :                << std::endl;
     114                 :            : 
     115                 :            :     // Expand definitions, which is required for being accurate for operators
     116                 :            :     // that expand involving skolems during preprocessing. Not doing this will
     117                 :            :     // increase the spurious warnings raised by this class.
     118                 :      23838 :     n = expDef.expandDefinitions(n, cache);
     119                 :      47676 :     verbose(1) << "SolverEngine::checkModel(): -- expands to " << n
     120                 :      23838 :                << std::endl;
     121                 :            : 
     122                 :      23838 :     n = rewrite(n);
     123                 :      47676 :     verbose(1) << "SolverEngine::checkModel(): -- rewrites to " << n
     124                 :      23838 :                << std::endl;
     125                 :            : 
     126                 :            :     // We look up the value before simplifying. If n contains quantifiers,
     127                 :            :     // this may increases the chance of finding its value before the node is
     128                 :            :     // altered by simplification below.
     129                 :      23838 :     Node nval = m->getValue(n);
     130                 :      47676 :     verbose(1) << "SolverEngine::checkModel(): -- get value : " << n
     131                 :      23838 :                << std::endl;
     132                 :            : 
     133 [ +  + ][ +  - ]:      23838 :     if (nval.isConst() && nval.getConst<bool>())
                 [ +  + ]
     134                 :            :     {
     135                 :            :       // assertion is true, everything is fine
     136                 :      23751 :       continue;
     137                 :            :     }
     138                 :            : 
     139                 :            :     // Otherwise, we did not succeed in showing the current assertion to be
     140                 :            :     // true. This may either indicate that our model is wrong, or that we cannot
     141                 :            :     // check it. The latter may be the case for several reasons.
     142                 :            :     // One example is the occurrence of partial operators. Another example
     143                 :            :     // are quantified formulas, which are not checkable, although we assign
     144                 :            :     // them to true/false based on the satisfying assignment. However,
     145                 :            :     // quantified formulas can be modified during preprocess, so they may not
     146                 :            :     // correspond to those in the satisfying assignment. Hence we throw
     147                 :            :     // warnings for assertions that do not simplify to either true or false.
     148                 :            :     // Other theories such as non-linear arithmetic (in particular,
     149                 :            :     // transcendental functions) also have the property of not being able to
     150                 :            :     // be checked precisely here.
     151                 :            :     // Note that warnings like these can be avoided for quantified formulas
     152                 :            :     // by making preprocessing passes explicitly record how they
     153                 :            :     // rewrite quantified formulas (see cvc4-wishues#43).
     154         [ +  - ]:         87 :     if (!nval.isConst())
     155                 :            :     {
     156                 :            :       // Not constant, print a less severe warning message here.
     157                 :         87 :       warning()
     158                 :            :           << "Warning : SolverEngine::checkModel(): cannot check simplified "
     159                 :         87 :              "assertion : "
     160                 :         87 :           << nval << std::endl;
     161                 :         87 :       noCheckList.push_back(nval);
     162                 :         87 :       continue;
     163                 :            :     }
     164                 :            :     // Assertions that simplify to false result in an InternalError or
     165                 :            :     // Warning being thrown below (when hardFailure is false).
     166                 :          0 :     verbose(1) << "SolverEngine::checkModel(): *** PROBLEM: EXPECTED `TRUE' ***"
     167                 :          0 :                << std::endl;
     168                 :          0 :     std::stringstream ss;
     169                 :            :     ss << "SolverEngine::checkModel(): "
     170                 :          0 :        << "ERRORS SATISFYING ASSERTIONS WITH MODEL";
     171                 :          0 :     std::stringstream ssdet;
     172                 :          0 :     ssdet << ":" << std::endl
     173                 :          0 :           << "assertion:     " << assertion << std::endl
     174                 :          0 :           << "simplifies to: " << nval << std::endl
     175                 :          0 :           << "expected `true'." << std::endl
     176                 :          0 :           << "Run with `--check-models -v' for additional diagnostics.";
     177         [ -  - ]:          0 :     if (hardFailure)
     178                 :            :     {
     179                 :            :       // compute the theories involved, e.g. for the sake of issue tracking.
     180                 :            :       // to ensure minimality, if this is a topmost AND, miniscope
     181                 :          0 :       Node nmin = n;
     182         [ -  - ]:          0 :       while (nmin.getKind() == Kind::AND)
     183                 :            :       {
     184         [ -  - ]:          0 :         for (const Node& nc : nmin)
     185                 :            :         {
     186         [ -  - ]:          0 :           if (m->getValue(nc) == nval)
     187                 :            :           {
     188                 :          0 :             nmin = nc;
     189                 :          0 :             break;
     190                 :            :           }
     191                 :            :         }
     192                 :            :       }
     193                 :            :       // collect the theories of the assertion
     194                 :          0 :       std::vector<TheoryId> theories;
     195                 :          0 :       getTheoriesOf(d_env, nmin, theories);
     196                 :          0 :       std::sort(theories.begin(), theories.end());
     197                 :          0 :       ss << " {";
     198         [ -  - ]:          0 :       for (TheoryId tid : theories)
     199                 :            :       {
     200         [ -  - ]:          0 :         if (tid != THEORY_BOOL)
     201                 :            :         {
     202                 :          0 :           ss << " " << tid;
     203                 :            :         }
     204                 :            :       }
     205                 :          0 :       ss << " }";
     206                 :            :       // internal error if hardFailure is true
     207                 :          0 :       InternalError() << ss.str() << ssdet.str();
     208                 :            :     }
     209                 :            :     else
     210                 :            :     {
     211                 :          0 :       warning() << ss.str() << ssdet.str() << std::endl;
     212                 :            :     }
     213                 :            :   }
     214         [ +  + ]:       2991 :   if (noCheckList.empty())
     215                 :            :   {
     216                 :       2922 :     verbose(1) << "SolverEngine::checkModel(): all assertions checked out OK !"
     217                 :       2922 :                << std::endl;
     218                 :       2922 :     return;
     219                 :            :   }
     220                 :            :   // if the noCheckList is non-empty, we could expand definitions on this list
     221                 :            :   // and check satisfiability
     222                 :            : 
     223         [ +  - ]:         69 :   Trace("check-model") << "checkModel: Finish" << std::endl;
     224                 :            : }
     225                 :            : 
     226                 :            : }  // namespace smt
     227                 :            : }  // namespace cvc5::internal