src/theory/difficulty_manager.cpp

   1 /******************************************************************************
   2  * Top contributors (to current version):
   3  *   Andrew Reynolds
   4  *
   5  * This file is part of the cvc5 project.
   6  *
   7  * Copyright (c) 2009-2021 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  * Difficulty manager.
  14  */
  15
  16 #include "theory/difficulty_manager.h"
  17
  18 #include "options/smt_options.h"
  19 #include "smt/env.h"
  20 #include "theory/theory_model.h"
  21 #include "util/rational.h"
  22
  23 namespace cvc5 {
  24 namespace theory {
  25
  26 DifficultyManager::DifficultyManager(context::Context* c, Valuation val)
  27     : d_val(val), d_dfmap(c)
  28 {
  29 }
  30
  31 void DifficultyManager::getDifficultyMap(std::map<Node, Node>& dmap)
  32 {
  33   NodeManager* nm = NodeManager::currentNM();
  34   for (const std::pair<const Node, uint64_t> p : d_dfmap)
  35   {
  36     dmap[p.first] = nm->mkConst(Rational(p.second));
  37   }
  38 }
  39
  40 void DifficultyManager::notifyLemma(const std::map<TNode, TNode>& rse, Node n)
  41 {
  42   if (options::difficultyMode() != options::DifficultyMode::LEMMA_LITERAL)
  43   {
  44     return;
  45   }
  46   Trace("diff-man") << "notifyLemma: " << n << std::endl;
  47   Kind nk = n.getKind();
  48   // for lemma (or a_1 ... a_n), if a_i is a literal that is not true in the
  49   // valuation, then we increment the difficulty of that assertion
  50   std::vector<TNode> litsToCheck;
  51   if (nk == kind::OR)
  52   {
  53     litsToCheck.insert(litsToCheck.end(), n.begin(), n.end());
  54   }
  55   else if (nk == kind::IMPLIES)
  56   {
  57     litsToCheck.push_back(n[0].negate());
  58     litsToCheck.push_back(n[1]);
  59   }
  60   else
  61   {
  62     litsToCheck.push_back(n);
  63   }
  64   std::map<TNode, TNode>::const_iterator it;
  65   for (TNode nc : litsToCheck)
  66   {
  67     bool pol = nc.getKind() != kind::NOT;
  68     TNode atom = pol ? nc : nc[0];
  69     it = rse.find(atom);
  70     if (it != rse.end())
  71     {
  72       incrementDifficulty(it->second);
  73     }
  74   }
  75 }
  76
  77 void DifficultyManager::notifyCandidateModel(const NodeList& input,
  78                                              TheoryModel* m)
  79 {
  80   if (options::difficultyMode() != options::DifficultyMode::MODEL_CHECK)
  81   {
  82     return;
  83   }
  84   Trace("diff-man") << "DifficultyManager::notifyCandidateModel, #input="
  85                     << input.size() << std::endl;
  86   for (const Node& a : input)
  87   {
  88     // should have miniscoped the assertions upstream
  89     Assert(a.getKind() != kind::AND);
  90     // check if each input is satisfied
  91     Node av = m->getValue(a);
  92     if (av.isConst() && av.getConst<bool>())
  93     {
  94       continue;
  95     }
  96     Trace("diff-man") << "  not true: " << a << std::endl;
  97     // not satisfied, increment counter
  98     incrementDifficulty(a);
  99   }
 100   Trace("diff-man") << std::endl;
 101 }
 102 void DifficultyManager::incrementDifficulty(TNode a, uint64_t amount)
 103 {
 104   Assert(a.getType().isBoolean());
 105   d_dfmap[a] = d_dfmap[a] + amount;
 106 }
 107
 108 }  // namespace theory
 109 }  // namespace cvc5