Branch data     Line data    Source code

       1                 :            : /******************************************************************************
       2                 :            :  * Top contributors (to current version):
       3                 :            :  *   Mathias Preiner, Liana Hadarean, 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                 :            :  * The BvIntroPow2 preprocessing pass.
      14                 :            :  *
      15                 :            :  * Traverses the formula and applies the IsPowerOfTwo rewrite rule. This
      16                 :            :  * preprocessing pass is particularly useful on QF_BV/pspace benchmarks and
      17                 :            :  * can be enabled via option `--bv-intro-pow2`.
      18                 :            :  */
      19                 :            : 
      20                 :            : #include "preprocessing/passes/bv_intro_pow2.h"
      21                 :            : 
      22                 :            : #include <unordered_map>
      23                 :            : 
      24                 :            : #include "preprocessing/assertion_pipeline.h"
      25                 :            : #include "preprocessing/preprocessing_pass_context.h"
      26                 :            : #include "theory/bv/theory_bv_utils.h"
      27                 :            : 
      28                 :            : namespace cvc5::internal {
      29                 :            : namespace preprocessing {
      30                 :            : namespace passes {
      31                 :            : 
      32                 :            : using NodeMap = std::unordered_map<Node, Node>;
      33                 :            : using namespace cvc5::internal::theory;
      34                 :            : 
      35                 :      50975 : BvIntroPow2::BvIntroPow2(PreprocessingPassContext* preprocContext)
      36                 :      50975 :     : PreprocessingPass(preprocContext, "bv-intro-pow2"){};
      37                 :            : 
      38                 :          5 : PreprocessingPassResult BvIntroPow2::applyInternal(
      39                 :            :     AssertionPipeline* assertionsToPreprocess)
      40                 :            : {
      41                 :          5 :   std::unordered_map<Node, Node> cache;
      42         [ +  + ]:         50 :   for (size_t i = 0, size = assertionsToPreprocess->size(); i < size; ++i)
      43                 :            :   {
      44                 :         90 :     Node cur = (*assertionsToPreprocess)[i];
      45                 :         90 :     Node res = pow2Rewrite(cur, cache);
      46         [ +  + ]:         45 :     if (res != cur)
      47                 :            :     {
      48                 :         15 :       assertionsToPreprocess->replace(
      49                 :            :           i, res, nullptr, TrustId::PREPROCESS_BV_INTRO_POW2);
      50                 :         15 :       assertionsToPreprocess->ensureRewritten(i);
      51                 :            :     }
      52                 :            :   }
      53                 :         10 :   return PreprocessingPassResult::NO_CONFLICT;
      54                 :            : }
      55                 :            : 
      56                 :         20 : bool BvIntroPow2::isPowerOfTwo(TNode node)
      57                 :            : {
      58         [ -  + ]:         20 :   if (node.getKind() != Kind::EQUAL)
      59                 :            :   {
      60                 :          0 :     return false;
      61                 :            :   }
      62 [ +  + ][ -  - ]:         20 :   if (node[0].getKind() != Kind::BITVECTOR_AND
      63 [ +  - ][ +  + ]:         20 :       && node[1].getKind() != Kind::BITVECTOR_AND)
         [ +  - ][ +  - ]
                 [ -  - ]
      64                 :            :   {
      65                 :          5 :     return false;
      66                 :            :   }
      67                 :         15 :   if (!bv::utils::isZero(node[0]) && !bv::utils::isZero(node[1]))
      68                 :            :   {
      69                 :          0 :     return false;
      70                 :            :   }
      71                 :            : 
      72         [ -  + ]:         30 :   TNode t = !bv::utils::isZero(node[0]) ? node[0] : node[1];
      73         [ -  + ]:         15 :   if (t.getNumChildren() != 2) return false;
      74                 :         30 :   TNode a = t[0];
      75                 :         30 :   TNode b = t[1];
      76         [ -  + ]:         15 :   if (bv::utils::getSize(t) < 2) return false;
      77                 :         30 :   Node diff = rewrite(nodeManager()->mkNode(Kind::BITVECTOR_SUB, a, b));
      78                 :         30 :   return (diff.isConst()
      79                 :         15 :           && (bv::utils::isOne(diff) || bv::utils::isOnes(diff)));
      80                 :            : }
      81                 :            : 
      82                 :         15 : Node BvIntroPow2::rewritePowerOfTwo(TNode node)
      83                 :            : {
      84                 :         15 :   NodeManager* nm = nodeManager();
      85         [ +  - ]:         30 :   TNode term = bv::utils::isZero(node[0]) ? node[1] : node[0];
      86                 :         30 :   TNode a = term[0];
      87                 :         30 :   TNode b = term[1];
      88                 :         15 :   uint32_t size = bv::utils::getSize(term);
      89                 :         45 :   Node diff = rewrite(nm->mkNode(Kind::BITVECTOR_SUB, a, b));
      90 [ -  + ][ -  + ]:         15 :   Assert(diff.isConst());
                 [ -  - ]
      91                 :         30 :   Node one = bv::utils::mkOne(nm, size);
      92         [ +  - ]:         30 :   TNode x = diff == one ? a : b;
      93                 :         30 :   Node sk = bv::utils::mkVar(nm, size);
      94                 :         45 :   Node sh = nm->mkNode(Kind::BITVECTOR_SHL, one, sk);
      95                 :         30 :   Node x_eq_sh = nm->mkNode(Kind::EQUAL, x, sh);
      96                 :         30 :   return x_eq_sh;
      97                 :            : }
      98                 :            : 
      99                 :         45 : Node BvIntroPow2::pow2Rewrite(Node node, std::unordered_map<Node, Node>& cache)
     100                 :            : {
     101                 :         45 :   const auto& ci = cache.find(node);
     102         [ -  + ]:         45 :   if (ci != cache.end())
     103                 :            :   {
     104                 :          0 :     Node incache = (*ci).second;
     105         [ -  - ]:          0 :     return incache.isNull() ? node : incache;
     106                 :            :   }
     107                 :            : 
     108                 :         90 :   Node res = Node::null();
     109    [ -  + ][ + ]:         45 :   switch (node.getKind())
     110                 :            :   {
     111                 :          0 :     case Kind::AND:
     112                 :            :     {
     113                 :          0 :       bool changed = false;
     114                 :          0 :       std::vector<Node> children;
     115         [ -  - ]:          0 :       for (unsigned i = 0, size = node.getNumChildren(); i < size; ++i)
     116                 :            :       {
     117                 :          0 :         Node child = node[i];
     118                 :          0 :         Node found = pow2Rewrite(child, cache);
     119                 :          0 :         changed = changed || (child != found);
     120                 :          0 :         children.push_back(found);
     121                 :            :       }
     122         [ -  - ]:          0 :       if (changed)
     123                 :            :       {
     124                 :          0 :         res = nodeManager()->mkNode(Kind::AND, children);
     125                 :            :       }
     126                 :            :     }
     127                 :          0 :     break;
     128                 :            : 
     129                 :         20 :     case Kind::EQUAL:
     130                 :         20 :       if (node[0].getType().isBitVector() && isPowerOfTwo(node))
     131                 :            :       {
     132                 :         15 :         res = rewritePowerOfTwo(node);
     133                 :            :       }
     134                 :         20 :       break;
     135                 :         25 :     default: break;
     136                 :            :   }
     137                 :            : 
     138                 :         45 :   cache.insert(std::make_pair(node, res));
     139         [ +  + ]:         45 :   return res.isNull() ? node : res;
     140                 :            : }
     141                 :            : 
     142                 :            : }  // namespace passes
     143                 :            : }  // namespace preprocessing
     144                 :            : 
     145                 :            : }  // namespace cvc5::internal