src/theory/relevance_manager.cpp

   1 /*********************                                                        */
   2 /*! \file relevance_manager.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 Implementation of relevance manager.
  13  **/
  14
  15 #include "theory/relevance_manager.h"
  16
  17 using namespace CVC4::kind;
  18
  19 namespace CVC4 {
  20 namespace theory {
  21
  22 RelevanceManager::RelevanceManager(context::UserContext* userContext,
  23                                    Valuation val)
  24     : d_val(val), d_input(userContext), d_computed(false), d_success(false)
  25 {
  26 }
  27
  28 void RelevanceManager::notifyPreprocessedAssertions(
  29     const std::vector<Node>& assertions)
  30 {
  31   // add to input list, which is user-context dependent
  32   std::vector<Node> toProcess;
  33   for (const Node& a : assertions)
  34   {
  35     if (a.getKind() == AND)
  36     {
  37       // split top-level AND
  38       for (const Node& ac : a)
  39       {
  40         toProcess.push_back(ac);
  41       }
  42     }
  43     else
  44     {
  45       d_input.push_back(a);
  46     }
  47   }
  48   addAssertionsInternal(toProcess);
  49 }
  50
  51 void RelevanceManager::notifyPreprocessedAssertion(Node n)
  52 {
  53   std::vector<Node> toProcess;
  54   toProcess.push_back(n);
  55   addAssertionsInternal(toProcess);
  56 }
  57
  58 void RelevanceManager::addAssertionsInternal(std::vector<Node>& toProcess)
  59 {
  60   size_t i = 0;
  61   while (i < toProcess.size())
  62   {
  63     Node a = toProcess[i];
  64     if (a.getKind() == AND)
  65     {
  66       // split AND
  67       for (const Node& ac : a)
  68       {
  69         toProcess.push_back(ac);
  70       }
  71     }
  72     else
  73     {
  74       // note that a could be a literal, in which case we could add it to
  75       // an "always relevant" set here.
  76       d_input.push_back(a);
  77     }
  78     i++;
  79   }
  80 }
  81
  82 void RelevanceManager::resetRound()
  83 {
  84   d_computed = false;
  85   d_rset.clear();
  86 }
  87
  88 void RelevanceManager::computeRelevance()
  89 {
  90   d_computed = true;
  91   Trace("rel-manager") << "RelevanceManager::computeRelevance..." << std::endl;
  92   std::unordered_map<TNode, int, TNodeHashFunction> cache;
  93   for (const Node& node: d_input)
  94   {
  95     TNode n = node;
  96     int val = justify(n, cache);
  97     if (val != 1)
  98     {
  99       std::stringstream serr;
 100       serr << "RelevanceManager::computeRelevance: WARNING: failed to justify "
 101            << n;
 102       Trace("rel-manager") << serr.str() << std::endl;
 103       Assert(false) << serr.str();
 104       d_success = false;
 105       return;
 106     }
 107   }
 108   Trace("rel-manager") << "...success, size = " << d_rset.size() << std::endl;
 109   d_success = true;
 110 }
 111
 112 bool RelevanceManager::isBooleanConnective(TNode cur)
 113 {
 114   Kind k = cur.getKind();
 115   return k == NOT || k == IMPLIES || k == AND || k == OR || k == ITE || k == XOR
 116          || (k == EQUAL && cur[0].getType().isBoolean());
 117 }
 118
 119 bool RelevanceManager::updateJustifyLastChild(
 120     TNode cur,
 121     std::vector<int>& childrenJustify,
 122     std::unordered_map<TNode, int, TNodeHashFunction>& cache)
 123 {
 124   // This method is run when we are informed that child index of cur
 125   // has justify status lastChildJustify. We return true if we would like to
 126   // compute the next child, in this case we push the status of the current
 127   // child to childrenJustify.
 128   size_t nchildren = cur.getNumChildren();
 129   Assert(isBooleanConnective(cur));
 130   size_t index = childrenJustify.size();
 131   Assert(index < nchildren);
 132   Assert(cache.find(cur[index]) != cache.end());
 133   Kind k = cur.getKind();
 134   // Lookup the last child's value in the overall cache, we may choose to
 135   // add this to childrenJustify if we return true.
 136   int lastChildJustify = cache[cur[index]];
 137   if (k == NOT)
 138   {
 139     cache[cur] = -lastChildJustify;
 140   }
 141   else if (k == IMPLIES || k == AND || k == OR)
 142   {
 143     if (lastChildJustify != 0)
 144     {
 145       // See if we short circuited? The value for short circuiting is false if
 146       // we are AND or the first child of IMPLIES.
 147       if (lastChildJustify
 148           == ((k == AND || (k == IMPLIES && index == 0)) ? -1 : 1))
 149       {
 150         cache[cur] = k == AND ? -1 : 1;
 151         return false;
 152       }
 153     }
 154     if (index + 1 == nchildren)
 155     {
 156       // finished all children, compute the overall value
 157       int ret = k == AND ? 1 : -1;
 158       for (int cv : childrenJustify)
 159       {
 160         if (cv == 0)
 161         {
 162           ret = 0;
 163           break;
 164         }
 165       }
 166       cache[cur] = ret;
 167     }
 168     else
 169     {
 170       // continue
 171       childrenJustify.push_back(lastChildJustify);
 172       return true;
 173     }
 174   }
 175   else if (lastChildJustify == 0)
 176   {
 177     // all other cases, an unknown child implies we are unknown
 178     cache[cur] = 0;
 179   }
 180   else if (k == ITE)
 181   {
 182     if (index == 0)
 183     {
 184       Assert(lastChildJustify != 0);
 185       // continue with branch
 186       childrenJustify.push_back(lastChildJustify);
 187       if (lastChildJustify == -1)
 188       {
 189         // also mark first branch as don't care
 190         childrenJustify.push_back(0);
 191       }
 192       return true;
 193     }
 194     else
 195     {
 196       // should be in proper branch
 197       Assert(childrenJustify[0] == (index == 1 ? 1 : -1));
 198       // we are the value of the branch
 199       cache[cur] = lastChildJustify;
 200     }
 201   }
 202   else
 203   {
 204     Assert(k == XOR || k == EQUAL);
 205     Assert(nchildren == 2);
 206     Assert(lastChildJustify != 0);
 207     if (index == 0)
 208     {
 209       // must compute the other child
 210       childrenJustify.push_back(lastChildJustify);
 211       return true;
 212     }
 213     else
 214     {
 215       // both children known, compute value
 216       Assert(childrenJustify.size() == 1 && childrenJustify[0] != 0);
 217       cache[cur] =
 218           ((k == XOR ? -1 : 1) * lastChildJustify == childrenJustify[0]) ? 1
 219                                                                          : -1;
 220     }
 221   }
 222   return false;
 223 }
 224
 225 int RelevanceManager::justify(
 226     TNode n, std::unordered_map<TNode, int, TNodeHashFunction>& cache)
 227 {
 228   // the vector of values of children
 229   std::unordered_map<TNode, std::vector<int>, TNodeHashFunction> childJustify;
 230   std::unordered_map<TNode, int, TNodeHashFunction>::iterator it;
 231   std::unordered_map<TNode, std::vector<int>, TNodeHashFunction>::iterator itc;
 232   std::vector<TNode> visit;
 233   TNode cur;
 234   visit.push_back(n);
 235   do
 236   {
 237     cur = visit.back();
 238     // should always have Boolean type
 239     Assert(cur.getType().isBoolean());
 240     it = cache.find(cur);
 241     if (it != cache.end())
 242     {
 243       visit.pop_back();
 244       // already computed value
 245       continue;
 246     }
 247     itc = childJustify.find(cur);
 248     // have we traversed to children yet?
 249     if (itc == childJustify.end())
 250     {
 251       // are we not a Boolean connective (including NOT)?
 252       if (isBooleanConnective(cur))
 253       {
 254         // initialize its children justify vector as empty
 255         childJustify[cur].clear();
 256         // start with the first child
 257         visit.push_back(cur[0]);
 258       }
 259       else
 260       {
 261         visit.pop_back();
 262         // The atom case, lookup the value in the valuation class to
 263         // see its current value in the SAT solver, if it has one.
 264         int ret = 0;
 265         // otherwise we look up the value
 266         bool value;
 267         if (d_val.hasSatValue(cur, value))
 268         {
 269           ret = value ? 1 : -1;
 270           d_rset.insert(cur);
 271         }
 272         cache[cur] = ret;
 273       }
 274     }
 275     else
 276     {
 277       // this processes the impact of the current child on the value of cur,
 278       // and possibly requests that a new child is computed.
 279       if (updateJustifyLastChild(cur, itc->second, cache))
 280       {
 281         Assert(itc->second.size() < cur.getNumChildren());
 282         TNode nextChild = cur[itc->second.size()];
 283         visit.push_back(nextChild);
 284       }
 285       else
 286       {
 287         visit.pop_back();
 288       }
 289     }
 290   } while (!visit.empty());
 291   Assert(cache.find(n) != cache.end());
 292   return cache[n];
 293 }
 294
 295 bool RelevanceManager::isRelevant(Node lit)
 296 {
 297   if (!d_computed)
 298   {
 299     computeRelevance();
 300   }
 301   if (!d_success)
 302   {
 303     // always relevant if we failed to compute
 304     return true;
 305   }
 306   // agnostic to negation
 307   while (lit.getKind() == NOT)
 308   {
 309     lit = lit[0];
 310   }
 311   return d_rset.find(lit) != d_rset.end();
 312 }
 313
 314 }  // namespace theory
 315 }  // namespace CVC4