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                 :            :  * Core rewrite rules of the BV theory.
      11                 :            :  */
      12                 :            : 
      13                 :            : #include "cvc5_private.h"
      14                 :            : 
      15                 :            : #ifndef CVC5__THEORY__BV__THEORY_BV_REWRITE_RULES_CORE_H
      16                 :            : #define CVC5__THEORY__BV__THEORY_BV_REWRITE_RULES_CORE_H
      17                 :            : 
      18                 :            : #include "theory/bv/theory_bv_rewrite_rules.h"
      19                 :            : #include "theory/bv/theory_bv_utils.h"
      20                 :            : #include "util/bitvector.h"
      21                 :            : 
      22                 :            : namespace cvc5::internal {
      23                 :            : namespace theory {
      24                 :            : namespace bv {
      25                 :            : 
      26                 :            : /* -------------------------------------------------------------------------- */
      27                 :            : 
      28                 :            : template <>
      29                 :     872110 : inline bool RewriteRule<ConcatFlatten>::applies(TNode node)
      30                 :            : {
      31                 :     872110 :   return (node.getKind() == Kind::BITVECTOR_CONCAT);
      32                 :            : }
      33                 :            : 
      34                 :            : template <>
      35                 :     436055 : inline Node RewriteRule<ConcatFlatten>::apply(TNode node)
      36                 :            : {
      37         [ +  - ]:     872110 :   Trace("bv-rewrite") << "RewriteRule<ConcatFlatten>(" << node << ")"
      38                 :     436055 :                       << std::endl;
      39                 :     436055 :   NodeBuilder result(node.getNodeManager(), Kind::BITVECTOR_CONCAT);
      40                 :     436055 :   std::vector<Node> processing_stack;
      41                 :     436055 :   processing_stack.push_back(node);
      42         [ +  + ]:    3249893 :   while (!processing_stack.empty())
      43                 :            :   {
      44                 :    2813838 :     Node current = processing_stack.back();
      45                 :    2813838 :     processing_stack.pop_back();
      46         [ +  + ]:    2813838 :     if (current.getKind() == Kind::BITVECTOR_CONCAT)
      47                 :            :     {
      48         [ +  + ]:    2828405 :       for (int i = current.getNumChildren() - 1; i >= 0; i--)
      49                 :    2377783 :         processing_stack.push_back(current[i]);
      50                 :            :     }
      51                 :            :     else
      52                 :            :     {
      53                 :    2363216 :       result << current;
      54                 :            :     }
      55                 :    2813838 :   }
      56                 :     436055 :   Node resultNode = result;
      57         [ +  - ]:     872110 :   Trace("bv-rewrite") << "RewriteRule<ConcatFlatten>(" << resultNode << ")"
      58                 :     436055 :                       << std::endl;
      59                 :     872110 :   return resultNode;
      60                 :     436055 : }
      61                 :            : 
      62                 :            : /* -------------------------------------------------------------------------- */
      63                 :            : 
      64                 :            : template <>
      65                 :     847966 : inline bool RewriteRule<ConcatExtractMerge>::applies(TNode node)
      66                 :            : {
      67                 :     847966 :   return (node.getKind() == Kind::BITVECTOR_CONCAT);
      68                 :            : }
      69                 :            : 
      70                 :            : template <>
      71                 :     423747 : inline Node RewriteRule<ConcatExtractMerge>::apply(TNode node)
      72                 :            : {
      73         [ +  - ]:     847494 :   Trace("bv-rewrite") << "RewriteRule<ConcatExtractMerge>(" << node << ")"
      74                 :     423747 :                       << std::endl;
      75                 :            : 
      76                 :     423747 :   std::vector<Node> mergedExtracts;
      77                 :            : 
      78                 :     423747 :   Node current = node[0];
      79                 :     423747 :   bool mergeStarted = false;
      80                 :     423747 :   unsigned currentHigh = 0;
      81                 :     423747 :   unsigned currentLow = 0;
      82                 :            : 
      83         [ +  + ]:    2077699 :   for (size_t i = 1, end = node.getNumChildren(); i < end; ++i)
      84                 :            :   {
      85                 :            :     // The next candidate for merging
      86                 :    1653952 :     Node next = node[i];
      87                 :            :     // If the current is not an extract we just go to the next
      88         [ +  + ]:    1653952 :     if (current.getKind() != Kind::BITVECTOR_EXTRACT)
      89                 :            :     {
      90                 :    1482278 :       mergedExtracts.push_back(current);
      91                 :    1482278 :       current = next;
      92                 :    1482278 :       continue;
      93                 :            :     }
      94                 :            :     // If it is an extract and the first one, get the extract parameters
      95         [ +  + ]:     171674 :     else if (!mergeStarted)
      96                 :            :     {
      97                 :     171460 :       currentHigh = utils::getExtractHigh(current);
      98                 :     171460 :       currentLow = utils::getExtractLow(current);
      99                 :            :     }
     100                 :            : 
     101                 :            :     // If the next one can be merged, try to merge
     102                 :     171674 :     bool merged = false;
     103                 :     171674 :     if (next.getKind() == Kind::BITVECTOR_EXTRACT && current[0] == next[0])
     104                 :            :     {
     105                 :            :       // x[i : j] @ x[j - 1 : k] -> c x[i : k]
     106                 :      72386 :       unsigned nextHigh = utils::getExtractHigh(next);
     107                 :      72386 :       unsigned nextLow = utils::getExtractLow(next);
     108         [ +  + ]:      72386 :       if (nextHigh + 1 == currentLow)
     109                 :            :       {
     110                 :        380 :         currentLow = nextLow;
     111                 :        380 :         mergeStarted = true;
     112                 :        380 :         merged = true;
     113                 :            :       }
     114                 :            :     }
     115                 :            :     // If we haven't merged anything, add the previous merge and continue with
     116                 :            :     // the next
     117         [ +  + ]:     171674 :     if (!merged)
     118                 :            :     {
     119         [ +  + ]:     171294 :       if (!mergeStarted)
     120                 :     171246 :         mergedExtracts.push_back(current);
     121                 :            :       else
     122                 :         48 :         mergedExtracts.push_back(
     123                 :         96 :             utils::mkExtract(current[0], currentHigh, currentLow));
     124                 :     171294 :       current = next;
     125                 :     171294 :       mergeStarted = false;
     126                 :            :     }
     127         [ +  + ]:    1653952 :   }
     128                 :            : 
     129                 :            :   // Add the last child
     130         [ +  + ]:     423747 :   if (!mergeStarted)
     131                 :     423581 :     mergedExtracts.push_back(current);
     132                 :            :   else
     133                 :        166 :     mergedExtracts.push_back(
     134                 :        332 :         utils::mkExtract(current[0], currentHigh, currentLow));
     135                 :            : 
     136                 :            :   // Return the result
     137                 :     847494 :   return utils::mkConcat(mergedExtracts);
     138                 :     423747 : }
     139                 :            : 
     140                 :            : /* -------------------------------------------------------------------------- */
     141                 :            : 
     142                 :            : template <>
     143                 :     847544 : inline bool RewriteRule<ConcatConstantMerge>::applies(TNode node)
     144                 :            : {
     145                 :     847544 :   return node.getKind() == Kind::BITVECTOR_CONCAT;
     146                 :            : }
     147                 :            : 
     148                 :            : template <>
     149                 :     423535 : inline Node RewriteRule<ConcatConstantMerge>::apply(TNode node)
     150                 :            : {
     151         [ +  - ]:     847070 :   Trace("bv-rewrite") << "RewriteRule<ConcatConstantMerge>(" << node << ")"
     152                 :     423535 :                       << std::endl;
     153                 :            : 
     154                 :     423535 :   std::vector<Node> mergedConstants;
     155         [ +  + ]:    2453086 :   for (unsigned i = 0, end = node.getNumChildren(); i < end;)
     156                 :            :   {
     157         [ +  + ]:    2029551 :     if (node[i].getKind() != Kind::CONST_BITVECTOR)
     158                 :            :     {
     159                 :            :       // If not a constant, just add it
     160                 :    1733585 :       mergedConstants.push_back(node[i]);
     161                 :    1733585 :       ++i;
     162                 :            :     }
     163                 :            :     else
     164                 :            :     {
     165                 :            :       // Find the longest sequence of constants
     166                 :     295966 :       unsigned j = i + 1;
     167         [ +  + ]:     343414 :       while (j < end)
     168                 :            :       {
     169         [ +  + ]:     262671 :         if (node[j].getKind() != Kind::CONST_BITVECTOR)
     170                 :            :         {
     171                 :     215223 :           break;
     172                 :            :         }
     173                 :            :         else
     174                 :            :         {
     175                 :      47448 :           ++j;
     176                 :            :         }
     177                 :            :       }
     178                 :            :       // Append all the constants
     179                 :     295966 :       BitVector current = node[i].getConst<BitVector>();
     180         [ +  + ]:     343414 :       for (unsigned k = i + 1; k < j; ++k)
     181                 :            :       {
     182                 :      47448 :         current = current.concat(node[k].getConst<BitVector>());
     183                 :            :       }
     184                 :            :       // Add the new merged constant
     185                 :     295966 :       NodeManager* nm = node.getNodeManager();
     186                 :     295966 :       mergedConstants.push_back(utils::mkConst(nm, current));
     187                 :     295966 :       i = j;
     188                 :     295966 :     }
     189                 :            :   }
     190                 :            : 
     191         [ +  - ]:     847070 :   Trace("bv-rewrite") << "RewriteRule<ConcatConstantMerge>(" << node << ") => "
     192 [ -  + ][ -  - ]:     423535 :                       << utils::mkConcat(mergedConstants) << std::endl;
     193                 :            : 
     194                 :     847070 :   return utils::mkConcat(mergedConstants);
     195                 :     423535 : }
     196                 :            : 
     197                 :            : /* -------------------------------------------------------------------------- */
     198                 :            : 
     199                 :            : template <>
     200                 :    2289777 : inline bool RewriteRule<ExtractWhole>::applies(TNode node)
     201                 :            : {
     202         [ +  + ]:    2289777 :   if (node.getKind() != Kind::BITVECTOR_EXTRACT) return false;
     203                 :     445276 :   unsigned length = utils::getSize(node[0]);
     204                 :     445276 :   unsigned extractHigh = utils::getExtractHigh(node);
     205         [ +  + ]:     445276 :   if (extractHigh != length - 1) return false;
     206                 :     221855 :   unsigned extractLow = utils::getExtractLow(node);
     207         [ +  + ]:     221855 :   if (extractLow != 0) return false;
     208                 :      45726 :   return true;
     209                 :            : }
     210                 :            : 
     211                 :            : template <>
     212                 :      34001 : inline Node RewriteRule<ExtractWhole>::apply(TNode node)
     213                 :            : {
     214         [ +  - ]:      68002 :   Trace("bv-rewrite") << "RewriteRule<ExtractWhole>(" << node << ")"
     215                 :      34001 :                       << std::endl;
     216                 :      34001 :   return node[0];
     217                 :            : }
     218                 :            : 
     219                 :            : /* -------------------------------------------------------------------------- */
     220                 :            : 
     221                 :            : template <>
     222                 :     233830 : inline bool RewriteRule<ExtractConstant>::applies(TNode node)
     223                 :            : {
     224         [ +  + ]:     233830 :   if (node.getKind() != Kind::BITVECTOR_EXTRACT) return false;
     225         [ +  + ]:     222668 :   if (node[0].getKind() != Kind::CONST_BITVECTOR) return false;
     226                 :      65474 :   return true;
     227                 :            : }
     228                 :            : 
     229                 :            : template <>
     230                 :      32737 : inline Node RewriteRule<ExtractConstant>::apply(TNode node)
     231                 :            : {
     232         [ +  - ]:      65474 :   Trace("bv-rewrite") << "RewriteRule<ExtractConstant>(" << node << ")"
     233                 :      32737 :                       << std::endl;
     234                 :      32737 :   Node child = node[0];
     235                 :      32737 :   BitVector childValue = child.getConst<BitVector>();
     236                 :      32737 :   NodeManager* nm = node.getNodeManager();
     237                 :            :   return utils::mkConst(nm,
     238                 :      65474 :                         childValue.extract(utils::getExtractHigh(node),
     239                 :      65474 :                                            utils::getExtractLow(node)));
     240                 :      32737 : }
     241                 :            : 
     242                 :            : /* -------------------------------------------------------------------------- */
     243                 :            : 
     244                 :            : template <>
     245                 :     252369 : inline bool RewriteRule<ExtractConcat>::applies(TNode node)
     246                 :            : {
     247                 :            :   // Trace("bv-rewrite") << "RewriteRule<ExtractConcat>(" << node << ")" <<
     248                 :            :   // std::endl;
     249         [ +  + ]:     252369 :   if (node.getKind() != Kind::BITVECTOR_EXTRACT) return false;
     250         [ +  + ]:     251875 :   if (node[0].getKind() != Kind::BITVECTOR_CONCAT) return false;
     251                 :      45712 :   return true;
     252                 :            : }
     253                 :            : 
     254                 :            : template <>
     255                 :      22796 : inline Node RewriteRule<ExtractConcat>::apply(TNode node)
     256                 :            : {
     257         [ +  - ]:      45592 :   Trace("bv-rewrite") << "RewriteRule<ExtractConcat>(" << node << ")"
     258                 :      22796 :                       << std::endl;
     259                 :      22796 :   int extract_high = utils::getExtractHigh(node);
     260                 :      22796 :   int extract_low = utils::getExtractLow(node);
     261                 :            : 
     262                 :      22796 :   std::vector<Node> resultChildren;
     263                 :            : 
     264                 :      22796 :   Node concat = node[0];
     265 [ +  + ][ +  + ]:      70765 :   for (int i = concat.getNumChildren() - 1; i >= 0 && extract_high >= 0; i--)
     266                 :            :   {
     267                 :      47969 :     Node concatChild = concat[i];
     268                 :      47969 :     int concatChildSize = utils::getSize(concatChild);
     269         [ +  + ]:      47969 :     if (extract_low < concatChildSize)
     270                 :            :     {
     271                 :      43910 :       int extract_start = extract_low < 0 ? 0 : extract_low;
     272                 :      43910 :       int extract_end =
     273         [ +  + ]:      43910 :           extract_high < concatChildSize ? extract_high : concatChildSize - 1;
     274                 :      43910 :       resultChildren.push_back(
     275                 :      87820 :           utils::mkExtract(concatChild, extract_end, extract_start));
     276                 :            :     }
     277                 :      47969 :     extract_low -= concatChildSize;
     278                 :      47969 :     extract_high -= concatChildSize;
     279                 :      47969 :   }
     280                 :            : 
     281                 :      22796 :   std::reverse(resultChildren.begin(), resultChildren.end());
     282                 :            : 
     283                 :      45592 :   return utils::mkConcat(resultChildren);
     284                 :      22796 : }
     285                 :            : 
     286                 :            : /* -------------------------------------------------------------------------- */
     287                 :            : 
     288                 :            : template <>
     289                 :      75548 : inline bool RewriteRule<ExtractExtract>::applies(TNode node)
     290                 :            : {
     291         [ -  + ]:      75548 :   if (node.getKind() != Kind::BITVECTOR_EXTRACT) return false;
     292         [ +  + ]:      75548 :   if (node[0].getKind() != Kind::BITVECTOR_EXTRACT) return false;
     293                 :       3700 :   return true;
     294                 :            : }
     295                 :            : 
     296                 :            : template <>
     297                 :       1850 : inline Node RewriteRule<ExtractExtract>::apply(TNode node)
     298                 :            : {
     299         [ +  - ]:       3700 :   Trace("bv-rewrite") << "RewriteRule<ExtractExtract>(" << node << ")"
     300                 :       1850 :                       << std::endl;
     301                 :            : 
     302                 :            :   // x[i:j][k:l] ~>  x[k+j:l+j]
     303                 :       1850 :   uint32_t j = 0;
     304                 :       3700 :   Node child = node[0];
     305                 :            :   do
     306                 :            :   {
     307                 :       1850 :     j += utils::getExtractLow(child);
     308                 :       1850 :     child = child[0];
     309         [ -  + ]:       1850 :   } while (child.getKind() == Kind::BITVECTOR_EXTRACT);
     310                 :            : 
     311                 :       1850 :   uint32_t k = utils::getExtractHigh(node);
     312                 :       1850 :   uint32_t l = utils::getExtractLow(node);
     313                 :       1850 :   Node result = utils::mkExtract(child, k + j, l + j);
     314                 :       3700 :   return result;
     315                 :       1850 : }
     316                 :            : 
     317                 :            : /* -------------------------------------------------------------------------- */
     318                 :            : 
     319                 :            : template <>
     320                 :    1068759 : inline bool RewriteRule<FailEq>::applies(TNode node)
     321                 :            : {
     322                 :            :   // Trace("bv-rewrite") << "RewriteRule<FailEq>(" << node << ")" << std::endl;
     323         [ -  + ]:    1068759 :   if (node.getKind() != Kind::EQUAL) return false;
     324         [ +  + ]:    1068759 :   if (node[0].getKind() != Kind::CONST_BITVECTOR) return false;
     325         [ +  + ]:     436459 :   if (node[1].getKind() != Kind::CONST_BITVECTOR) return false;
     326                 :     100526 :   return node[0] != node[1];
     327                 :            : }
     328                 :            : 
     329                 :            : template <>
     330                 :      46803 : inline Node RewriteRule<FailEq>::apply(TNode node)
     331                 :            : {
     332                 :      46803 :   return utils::mkFalse(node.getNodeManager());
     333                 :            : }
     334                 :            : 
     335                 :            : /* -------------------------------------------------------------------------- */
     336                 :            : 
     337                 :            : template <>
     338                 :    1048561 : inline bool RewriteRule<SimplifyEq>::applies(TNode node)
     339                 :            : {
     340         [ +  + ]:    1048561 :   if (node.getKind() != Kind::EQUAL) return false;
     341                 :    1001758 :   return node[0] == node[1];
     342                 :            : }
     343                 :            : 
     344                 :            : template <>
     345                 :      26605 : inline Node RewriteRule<SimplifyEq>::apply(TNode node)
     346                 :            : {
     347         [ +  - ]:      26605 :   Trace("bv-rewrite") << "RewriteRule<SimplifyEq>(" << node << ")" << std::endl;
     348                 :      26605 :   return utils::mkTrue(node.getNodeManager());
     349                 :            : }
     350                 :            : 
     351                 :            : /* -------------------------------------------------------------------------- */
     352                 :            : 
     353                 :            : template <>
     354                 :    1125078 : inline bool RewriteRule<ReflexivityEq>::applies(TNode node)
     355                 :            : {
     356                 :    1125078 :   return (node.getKind() == Kind::EQUAL && node[0] > node[1]);
     357                 :            : }
     358                 :            : 
     359                 :            : template <>
     360                 :     103122 : inline Node RewriteRule<ReflexivityEq>::apply(TNode node)
     361                 :            : {
     362         [ +  - ]:     206244 :   Trace("bv-rewrite") << "RewriteRule<ReflexivityEq>(" << node << ")"
     363                 :     103122 :                       << std::endl;
     364                 :     206244 :   Node res = node[1].eqNode(node[0]);
     365                 :     103122 :   return res;
     366                 :            : }
     367                 :            : 
     368                 :            : }  // namespace bv
     369                 :            : }  // namespace theory
     370                 :            : }  // namespace cvc5::internal
     371                 :            : #endif