src/preprocessing/passes/bool_to_bv.cpp

   1 /*********************                                                        */
   2 /*! \file bool_to_bv.cpp
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Makai Mann, Yoni Zohar, Clark Barrett
   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 The BoolToBV preprocessing pass
  13  **
  14  **/
  15
  16 #include "preprocessing/passes/bool_to_bv.h"
  17
  18 #include <string>
  19
  20 #include "base/map_util.h"
  21 #include "expr/node.h"
  22 #include "smt/smt_statistics_registry.h"
  23 #include "theory/rewriter.h"
  24 #include "theory/theory.h"
  25
  26 namespace CVC4 {
  27 namespace preprocessing {
  28 namespace passes {
  29 using namespace CVC4::theory;
  30
  31 BoolToBV::BoolToBV(PreprocessingPassContext* preprocContext)
  32     : PreprocessingPass(preprocContext, "bool-to-bv"), d_statistics()
  33 {
  34   d_boolToBVMode = options::boolToBitvector();
  35 };
  36
  37 PreprocessingPassResult BoolToBV::applyInternal(
  38     AssertionPipeline* assertionsToPreprocess)
  39 {
  40   d_preprocContext->spendResource(ResourceManager::Resource::PreprocessStep);
  41
  42   size_t size = assertionsToPreprocess->size();
  43
  44   if (d_boolToBVMode == options::BoolToBVMode::ALL)
  45   {
  46     for (size_t i = 0; i < size; ++i)
  47     {
  48       Node newAssertion = lowerAssertion((*assertionsToPreprocess)[i], true);
  49       assertionsToPreprocess->replace(i, Rewriter::rewrite(newAssertion));
  50     }
  51   }
  52   else
  53   {
  54     Assert(d_boolToBVMode == options::BoolToBVMode::ITE);
  55     for (size_t i = 0; i < size; ++i)
  56     {
  57       assertionsToPreprocess->replace(
  58           i, Rewriter::rewrite(lowerIte((*assertionsToPreprocess)[i])));
  59     }
  60   }
  61
  62   return PreprocessingPassResult::NO_CONFLICT;
  63 }
  64
  65 void BoolToBV::updateCache(TNode n, TNode rebuilt)
  66 {
  67   // check more likely case first
  68   if ((n.getKind() != kind::ITE) || !n[1].getType().isBitVector())
  69   {
  70     d_lowerCache[n] = rebuilt;
  71   }
  72   else
  73   {
  74     d_iteBVLowerCache[n] = rebuilt;
  75   }
  76 }
  77
  78 Node BoolToBV::fromCache(TNode n) const
  79 {
  80   // check more likely case first
  81   if (n.getKind() != kind::ITE)
  82   {
  83     if (d_lowerCache.find(n) != d_lowerCache.end())
  84     {
  85       return d_lowerCache.at(n);
  86     }
  87   }
  88   else
  89   {
  90     if (d_iteBVLowerCache.find(n) != d_iteBVLowerCache.end())
  91     {
  92       return d_iteBVLowerCache.at(n);
  93     }
  94   }
  95   return n;
  96 }
  97
  98 inline bool BoolToBV::inCache(const Node& n) const
  99 {
 100   return (ContainsKey(d_lowerCache, n) || ContainsKey(d_iteBVLowerCache, n));
 101 }
 102
 103 bool BoolToBV::needToRebuild(TNode n) const
 104 {
 105   // check if any children were rebuilt
 106   for (const Node& nn : n)
 107   {
 108     if (inCache(nn))
 109     {
 110       return true;
 111     }
 112   }
 113   return false;
 114 }
 115
 116 Node BoolToBV::lowerAssertion(const TNode& assertion, bool allowIteIntroduction)
 117 {
 118   // first try to lower all the children
 119   for (const Node& c : assertion)
 120   {
 121     lowerNode(c, allowIteIntroduction);
 122   }
 123
 124   // now try lowering the assertion, but don't force it with an ITE (even in mode all)
 125   lowerNode(assertion, false);
 126   Node newAssertion = fromCache(assertion);
 127   TypeNode newAssertionType = newAssertion.getType();
 128   if (newAssertionType.isBitVector())
 129   {
 130     Assert(newAssertionType.getBitVectorSize() == 1);
 131     newAssertion = NodeManager::currentNM()->mkNode(
 132         kind::EQUAL, newAssertion, bv::utils::mkOne(1));
 133     newAssertionType = newAssertion.getType();
 134   }
 135   Assert(newAssertionType.isBoolean());
 136   return newAssertion;
 137 }
 138
 139 Node BoolToBV::lowerNode(const TNode& node, bool allowIteIntroduction)
 140 {
 141   std::vector<TNode> to_visit;
 142   to_visit.push_back(node);
 143   std::unordered_set<TNode, TNodeHashFunction> visited;
 144
 145   while (!to_visit.empty())
 146   {
 147     TNode n = to_visit.back();
 148     to_visit.pop_back();
 149
 150     Debug("bool-to-bv") << "BoolToBV::lowerNode: Post-order traversal with "
 151                         << n << " and visited = " << ContainsKey(visited, n)
 152                         << std::endl;
 153
 154     // Mark as visited
 155     if (ContainsKey(visited, n))
 156     {
 157       visit(n, allowIteIntroduction);
 158     }
 159     else
 160     {
 161       visited.insert(n);
 162       to_visit.push_back(n);
 163
 164       // insert children in reverse order so that they're processed in order
 165       //    important for rewriting which sorts by node id
 166       // NOTE: size_t is unsigned, so using underflow for termination condition
 167       size_t numChildren = n.getNumChildren();
 168       for (size_t i = numChildren - 1; i < numChildren; --i)
 169       {
 170         to_visit.push_back(n[i]);
 171       }
 172     }
 173   }
 174
 175   return fromCache(node);
 176 }
 177
 178 void BoolToBV::visit(const TNode& n, bool allowIteIntroduction)
 179 {
 180   Kind k = n.getKind();
 181
 182   // easy case -- just replace boolean constant
 183   if (k == kind::CONST_BOOLEAN)
 184   {
 185     updateCache(n,
 186                 (n == bv::utils::mkTrue()) ? bv::utils::mkOne(1)
 187                                            : bv::utils::mkZero(1));
 188     return;
 189   }
 190
 191   NodeManager* nm = NodeManager::currentNM();
 192   Kind new_kind = k;
 193   switch (k)
 194   {
 195     case kind::EQUAL: new_kind = kind::BITVECTOR_COMP; break;
 196     case kind::AND: new_kind = kind::BITVECTOR_AND; break;
 197     case kind::OR: new_kind = kind::BITVECTOR_OR; break;
 198     case kind::NOT: new_kind = kind::BITVECTOR_NOT; break;
 199     case kind::XOR: new_kind = kind::BITVECTOR_XOR; break;
 200     case kind::IMPLIES: new_kind = kind::BITVECTOR_OR; break;
 201     case kind::ITE: new_kind = kind::BITVECTOR_ITE; break;
 202     case kind::BITVECTOR_ULT: new_kind = kind::BITVECTOR_ULTBV; break;
 203     case kind::BITVECTOR_SLT: new_kind = kind::BITVECTOR_SLTBV; break;
 204     case kind::BITVECTOR_ULE:
 205     case kind::BITVECTOR_UGT:
 206     case kind::BITVECTOR_UGE:
 207     case kind::BITVECTOR_SLE:
 208     case kind::BITVECTOR_SGT:
 209     case kind::BITVECTOR_SGE:
 210       // Should have been removed by rewriting.
 211       Unreachable();
 212     default: break;
 213   }
 214
 215   // check if it's safe to lower or rebuild the node
 216   // Note: might have to rebuild to keep changes to children, even if this node
 217   // isn't being lowered
 218
 219   // it's safe to lower if all the children are bit-vectors
 220   bool safe_to_lower =
 221       (new_kind != k);  // don't need to lower at all if kind hasn't changed
 222
 223   // it's safe to rebuild if rebuilding doesn't change any of the types of the
 224   // children
 225   bool safe_to_rebuild = true;
 226
 227   for (const Node& nn : n)
 228   {
 229     safe_to_lower = safe_to_lower && fromCache(nn).getType().isBitVector();
 230     safe_to_rebuild = safe_to_rebuild && (fromCache(nn).getType() == nn.getType());
 231
 232     // if it's already not safe to do either, stop checking
 233     if (!safe_to_lower && !safe_to_rebuild)
 234     {
 235       break;
 236     }
 237   }
 238
 239   Debug("bool-to-bv") << "safe_to_lower = " << safe_to_lower
 240                       << ", safe_to_rebuild = " << safe_to_rebuild << std::endl;
 241
 242   if (new_kind != k && safe_to_lower)
 243   {
 244     // lower to BV
 245     rebuildNode(n, new_kind);
 246     return;
 247   }
 248   else if (new_kind != k && allowIteIntroduction && fromCache(n).getType().isBoolean())
 249   {
 250     // lower to BV using an ITE
 251
 252     if (safe_to_rebuild && needToRebuild(n))
 253     {
 254       // need to rebuild to keep changes made to descendants
 255       rebuildNode(n, k);
 256     }
 257
 258     updateCache(n,
 259                 nm->mkNode(kind::ITE,
 260                            fromCache(n),
 261                            bv::utils::mkOne(1),
 262                            bv::utils::mkZero(1)));
 263     Debug("bool-to-bv") << "BoolToBV::visit forcing " << n
 264                         << " =>\n"
 265                         << fromCache(n) << std::endl;
 266     ++(d_statistics.d_numIntroducedItes);
 267     return;
 268   }
 269   else if (safe_to_rebuild && needToRebuild(n))
 270   {
 271     // rebuild to incorporate changes to children
 272     Assert(k == new_kind);
 273     rebuildNode(n, k);
 274   }
 275   else if (allowIteIntroduction && fromCache(n).getType().isBoolean())
 276   {
 277     // force booleans (which haven't already been converted) to bit-vector
 278     // needed to maintain the invariant that all boolean children
 279     // have been converted (even constants and variables) when forcing
 280     // with ITE introductions
 281     updateCache(
 282         n, nm->mkNode(kind::ITE, n, bv::utils::mkOne(1), bv::utils::mkZero(1)));
 283     Debug("bool-to-bv") << "BoolToBV::visit forcing " << n
 284                         << " =>\n"
 285                         << fromCache(n) << std::endl;
 286     ++(d_statistics.d_numIntroducedItes);
 287   }
 288   else
 289   {
 290     // do nothing
 291     Debug("bool-to-bv") << "BoolToBV::visit skipping: " << n
 292                         << std::endl;
 293   }
 294 }
 295
 296 Node BoolToBV::lowerIte(const TNode& node)
 297 {
 298   std::vector<TNode> visit;
 299   visit.push_back(node);
 300   std::unordered_set<TNode, TNodeHashFunction> visited;
 301
 302   while (!visit.empty())
 303   {
 304     TNode n = visit.back();
 305     visit.pop_back();
 306
 307     Debug("bool-to-bv") << "BoolToBV::lowerIte: Post-order traversal with " << n
 308                         << " and visited = " << ContainsKey(visited, n)
 309                         << std::endl;
 310
 311     // Look for ITEs and mark visited
 312     if (!ContainsKey(visited, n))
 313     {
 314       if ((n.getKind() == kind::ITE) && n[1].getType().isBitVector())
 315       {
 316         Debug("bool-to-bv") << "BoolToBV::lowerIte: adding " << n[0]
 317                             << " to set of ite conditions" << std::endl;
 318         // don't force in this case -- forcing only introduces more ITEs
 319         Node loweredNode = lowerNode(n, false);
 320         // some of the lowered nodes might appear elsewhere but not in an ITE
 321         // reset the cache to prevent lowering them
 322         // the bit-vector ITEs are still tracked in d_iteBVLowerCache though
 323         d_lowerCache.clear();
 324       }
 325       else
 326       {
 327         visit.push_back(n);
 328         visited.insert(n);
 329         // insert in reverse order so that they're processed in order
 330         for (int i = n.getNumChildren() - 1; i >= 0; --i)
 331         {
 332           visit.push_back(n[i]);
 333         }
 334       }
 335     }
 336     else if (needToRebuild(n))
 337     {
 338       // Note: it's always safe to rebuild here, because we've only lowered
 339       //       ITEs of type bit-vector to BITVECTOR_ITE
 340       rebuildNode(n, n.getKind());
 341     }
 342     else
 343     {
 344       Debug("bool-to-bv")
 345           << "BoolToBV::lowerIte Skipping because don't need to rebuild: " << n
 346           << std::endl;
 347     }
 348   }
 349   return fromCache(node);
 350 }
 351
 352 void BoolToBV::rebuildNode(const TNode& n, Kind new_kind)
 353 {
 354   Kind k = n.getKind();
 355   NodeManager* nm = NodeManager::currentNM();
 356   NodeBuilder<> builder(new_kind);
 357
 358   Debug("bool-to-bv") << "BoolToBV::rebuildNode with " << n
 359                       << " and new_kind = " << kindToString(new_kind)
 360                       << std::endl;
 361
 362   if ((d_boolToBVMode == options::BoolToBVMode::ALL) && (new_kind != k))
 363   {
 364     ++(d_statistics.d_numTermsLowered);
 365   }
 366
 367   if (n.getMetaKind() == kind::metakind::PARAMETERIZED)
 368   {
 369     builder << n.getOperator();
 370   }
 371
 372   // special case IMPLIES because needs to be rewritten
 373   if ((k == kind::IMPLIES) && (new_kind != k))
 374   {
 375     builder << nm->mkNode(kind::BITVECTOR_NOT, fromCache(n[0]));
 376     builder << fromCache(n[1]);
 377   }
 378   else
 379   {
 380     for (const Node& nn : n)
 381     {
 382       builder << fromCache(nn);
 383     }
 384   }
 385
 386   Debug("bool-to-bv") << "BoolToBV::rebuildNode " << n << " =>\n"
 387                       << builder << std::endl;
 388
 389   updateCache(n, builder.constructNode());
 390 }
 391
 392 BoolToBV::Statistics::Statistics()
 393     : d_numIteToBvite("preprocessing::passes::BoolToBV::NumIteToBvite", 0),
 394       d_numTermsLowered("preprocessing::passes:BoolToBV::NumTermsLowered", 0),
 395       d_numIntroducedItes(
 396           "preprocessing::passes::BoolToBV::NumTermsForcedLowered", 0)
 397 {
 398   smtStatisticsRegistry()->registerStat(&d_numIteToBvite);
 399   if (options::boolToBitvector() == options::BoolToBVMode::ALL)
 400   {
 401     // these statistics wouldn't be correct in the ITE mode,
 402     // because it might discard rebuilt nodes if it fails to
 403     // convert a bool to width-one bit-vector (never forces)
 404     smtStatisticsRegistry()->registerStat(&d_numTermsLowered);
 405     smtStatisticsRegistry()->registerStat(&d_numIntroducedItes);
 406   }
 407 }
 408
 409 BoolToBV::Statistics::~Statistics()
 410 {
 411   smtStatisticsRegistry()->unregisterStat(&d_numIteToBvite);
 412   if (options::boolToBitvector() == options::BoolToBVMode::ALL)
 413   {
 414     smtStatisticsRegistry()->unregisterStat(&d_numTermsLowered);
 415     smtStatisticsRegistry()->unregisterStat(&d_numIntroducedItes);
 416   }
 417 }
 418
 419
 420 }  // namespace passes
 421 }  // namespace preprocessing
 422 }  // namespace CVC4