Branch data     Line data    Source code

       1                 :            : /******************************************************************************
       2                 :            :  * This file is part of the cvc5 project.
       3                 :            :  *
       4                 :            :  * Copyright (c) 2009-2026 by the authors listed in the file AUTHORS
       5                 :            :  * in the top-level source directory and their institutional affiliations.
       6                 :            :  * All rights reserved.  See the file COPYING in the top-level source
       7                 :            :  * directory for licensing information.
       8                 :            :  * ****************************************************************************
       9                 :            :  *
      10                 :            :  * Difficulty manager.
      11                 :            :  */
      12                 :            : 
      13                 :            : #include "theory/difficulty_manager.h"
      14                 :            : 
      15                 :            : #include "expr/node_algorithm.h"
      16                 :            : #include "options/smt_options.h"
      17                 :            : #include "smt/env.h"
      18                 :            : #include "theory/relevance_manager.h"
      19                 :            : #include "theory/theory_model.h"
      20                 :            : #include "util/rational.h"
      21                 :            : 
      22                 :            : using namespace cvc5::internal::kind;
      23                 :            : 
      24                 :            : namespace cvc5::internal {
      25                 :            : namespace theory {
      26                 :            : 
      27                 :        467 : DifficultyManager::DifficultyManager(Env& env,
      28                 :            :                                      RelevanceManager* rlv,
      29                 :        467 :                                      Valuation val)
      30                 :            :     : EnvObj(env),
      31                 :        467 :       d_rlv(rlv),
      32                 :        467 :       d_input(userContext()),
      33                 :        467 :       d_lemma(userContext()),
      34                 :        467 :       d_val(val),
      35                 :        934 :       d_dfmap(userContext())
      36                 :            : {
      37                 :        467 : }
      38                 :            : 
      39                 :        464 : void DifficultyManager::notifyInputAssertions(
      40                 :            :     const std::vector<Node>& assertions)
      41                 :            : {
      42         [ +  + ]:       1295 :   for (const Node& a : assertions)
      43                 :            :   {
      44                 :        831 :     d_input.insert(a);
      45                 :            :   }
      46                 :        464 : }
      47                 :            : 
      48                 :        454 : void DifficultyManager::getDifficultyMap(std::map<Node, Node>& dmap,
      49                 :            :                                          bool includeLemmas)
      50                 :            : {
      51                 :        454 :   NodeManager* nm = nodeManager();
      52         [ +  + ]:        939 :   for (const std::pair<const Node, uint64_t> p : d_dfmap)
      53                 :            :   {
      54         [ +  - ]:        485 :     if (!includeLemmas)
      55                 :            :     {
      56         [ +  + ]:        485 :       if (d_input.find(p.first) == d_input.end())
      57                 :            :       {
      58                 :         12 :         continue;
      59                 :            :       }
      60                 :            :     }
      61                 :        473 :     dmap[p.first] = nm->mkConstInt(Rational(p.second));
      62         [ +  + ]:        485 :   }
      63                 :        454 : }
      64                 :            : 
      65                 :          0 : uint64_t DifficultyManager::getCurrentDifficulty(const Node& n) const
      66                 :            : {
      67                 :          0 :   NodeUIntMap::const_iterator it = d_dfmap.find(n);
      68         [ -  - ]:          0 :   if (it != d_dfmap.end())
      69                 :            :   {
      70                 :          0 :     return it->second;
      71                 :            :   }
      72                 :          0 :   return 0;
      73                 :            : }
      74                 :            : 
      75                 :        593 : void DifficultyManager::notifyLemma(Node n, bool inFullEffortCheck)
      76                 :            : {
      77                 :        593 :   d_lemma.insert(n);
      78                 :            :   // compute if we should consider the lemma
      79                 :        593 :   bool considerLemma = false;
      80                 :        593 :   if (options().smt.difficultyMode
      81         [ +  + ]:        593 :       == options::DifficultyMode::LEMMA_LITERAL_ALL)
      82                 :            :   {
      83                 :        468 :     considerLemma = true;
      84                 :            :   }
      85                 :        125 :   else if (options().smt.difficultyMode
      86         [ -  + ]:        125 :            == options::DifficultyMode::LEMMA_LITERAL)
      87                 :            :   {
      88                 :          0 :     considerLemma = inFullEffortCheck;
      89                 :            :   }
      90         [ +  + ]:        593 :   if (!considerLemma)
      91                 :            :   {
      92                 :        125 :     return;
      93                 :            :   }
      94         [ +  - ]:        468 :   Trace("diff-man") << "notifyLemma: " << n << std::endl;
      95                 :        468 :   Kind nk = n.getKind();
      96                 :            :   // for lemma (or a_1 ... a_n), if a_i is a literal that is not true in the
      97                 :            :   // valuation, then we increment the difficulty of that assertion
      98                 :        468 :   std::vector<Node> litsToCheck;
      99         [ +  + ]:        468 :   if (nk == Kind::OR)
     100                 :            :   {
     101                 :         99 :     litsToCheck.insert(litsToCheck.end(), n.begin(), n.end());
     102                 :            :   }
     103         [ +  + ]:        369 :   else if (nk == Kind::IMPLIES)
     104                 :            :   {
     105                 :        106 :     litsToCheck.push_back(n[0].negate());
     106                 :        106 :     litsToCheck.push_back(n[1]);
     107                 :            :   }
     108                 :            :   else
     109                 :            :   {
     110                 :        263 :     litsToCheck.push_back(n);
     111                 :            :   }
     112                 :        468 :   size_t index = 0;
     113         [ +  + ]:       2694 :   while (index < litsToCheck.size())
     114                 :            :   {
     115                 :       2226 :     Node nc = litsToCheck[index];
     116                 :       2226 :     index++;
     117         [ +  + ]:       2226 :     if (expr::isBooleanConnective(nc))
     118                 :            :     {
     119                 :       1150 :       litsToCheck.insert(litsToCheck.end(), nc.begin(), nc.end());
     120                 :       1150 :       continue;
     121                 :            :     }
     122                 :       1076 :     TNode exp = d_rlv->getExplanationForRelevant(nc);
     123         [ +  - ]:       2152 :     Trace("diff-man-debug")
     124                 :       1076 :         << "Check literal: " << nc << ", has reason = " << (!exp.isNull())
     125                 :       1076 :         << std::endl;
     126                 :            :     // could be input assertion or lemma
     127         [ +  + ]:       1076 :     if (!exp.isNull())
     128                 :            :     {
     129                 :        602 :       incrementDifficulty(exp);
     130                 :            :     }
     131         [ +  + ]:       2226 :   }
     132                 :        468 : }
     133                 :            : 
     134                 :        313 : bool DifficultyManager::needsCandidateModel() const
     135                 :            : {
     136                 :        313 :   return options().smt.difficultyMode == options::DifficultyMode::MODEL_CHECK;
     137                 :            : }
     138                 :            : 
     139                 :         24 : void DifficultyManager::notifyCandidateModel(TheoryModel* m)
     140                 :            : {
     141 [ -  + ][ -  + ]:         24 :   Assert(needsCandidateModel());
                 [ -  - ]
     142         [ +  - ]:         48 :   Trace("diff-man") << "DifficultyManager::notifyCandidateModel, #input="
     143                 :         24 :                     << d_input.size() << " #lemma=" << d_lemma.size()
     144                 :         24 :                     << std::endl;
     145         [ +  + ]:         72 :   for (size_t i = 0; i < 2; i++)
     146                 :            :   {
     147         [ +  + ]:         48 :     NodeSet& ns = i == 0 ? d_input : d_lemma;
     148         [ +  + ]:        519 :     for (const Node& a : ns)
     149                 :            :     {
     150                 :            :       // check if each input is satisfied
     151                 :        471 :       Node av = m->getValue(a);
     152 [ +  + ][ +  + ]:        471 :       if (av.isConst() && av.getConst<bool>())
                 [ +  + ]
     153                 :            :       {
     154                 :        405 :         continue;
     155                 :            :       }
     156         [ +  - ]:         66 :       Trace("diff-man") << "  not true: " << a << std::endl;
     157                 :            :       // not satisfied, increment counter
     158                 :         66 :       incrementDifficulty(a);
     159 [ +  + ][ +  + ]:        876 :     }
     160                 :            :   }
     161         [ +  - ]:         24 :   Trace("diff-man") << std::endl;
     162                 :         24 : }
     163                 :        668 : void DifficultyManager::incrementDifficulty(TNode a, uint64_t amount)
     164                 :            : {
     165 [ -  + ][ -  + ]:        668 :   Assert(a.getType().isBoolean());
                 [ -  - ]
     166         [ +  - ]:       1336 :   Trace("diff-man") << "incrementDifficulty: " << a << " +" << amount
     167                 :        668 :                     << std::endl;
     168                 :        668 :   d_dfmap[a] = d_dfmap[a] + amount;
     169                 :        668 : }
     170                 :            : 
     171                 :            : }  // namespace theory
     172                 :            : }  // namespace cvc5::internal