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                 :            :  * parse ff bitsums
      11                 :            :  */
      12                 :            : 
      13                 :            : #include "preprocessing/passes/ff_bitsum.h"
      14                 :            : 
      15                 :            : // external includes
      16                 :            : 
      17                 :            : // std includes
      18                 :            : #include <unordered_set>
      19                 :            : 
      20                 :            : // internal includes
      21                 :            : #include "expr/algorithm/flatten.h"
      22                 :            : #include "expr/node_traversal.h"
      23                 :            : #include "preprocessing/assertion_pipeline.h"
      24                 :            : #include "theory/ff/parse.h"
      25                 :            : 
      26                 :            : namespace cvc5::internal {
      27                 :            : namespace preprocessing {
      28                 :            : namespace passes {
      29                 :            : 
      30                 :      51598 : FfBitsum::FfBitsum(PreprocessingPassContext* preprocContext)
      31                 :      51598 :     : PreprocessingPass(preprocContext, "ff-bitsum")
      32                 :            : {
      33                 :      51598 : }
      34                 :            : 
      35                 :         10 : Node mkAdd(NodeManager* nm, const std::vector<Node>& children)
      36                 :            : {
      37 [ -  + ][ -  + ]:         10 :   Assert(children.size() > 0);
                 [ -  - ]
      38                 :         17 :   return children.size() == 1 ? children[0]
      39         [ +  + ]:         27 :                               : nm->mkNode(Kind::FINITE_FIELD_ADD, children);
      40                 :            : }
      41                 :            : 
      42                 :         66 : PreprocessingPassResult FfBitsum::applyInternal(
      43                 :            :     AssertionPipeline* assertionsToPreprocess)
      44                 :            : {
      45                 :            :   // collect bits
      46                 :         66 :   std::unordered_set<Node> bits;
      47         [ +  + ]:        390 :   for (uint64_t i = 0, n = assertionsToPreprocess->size(); i < n; ++i)
      48                 :            :   {
      49                 :        324 :     std::vector<TNode> anded{};
      50                 :        324 :     TNode assertion = (*assertionsToPreprocess)[i];
      51                 :        324 :     expr::algorithm::flatten(assertion, anded, Kind::AND);
      52         [ +  + ]:        648 :     for (const auto& fact : anded)
      53                 :            :     {
      54                 :        324 :       if (fact.getKind() == Kind::EQUAL && fact[0].getType().isFiniteField())
      55                 :            :       {
      56                 :        110 :         auto bitOpt = theory::ff::parse::bitConstraint(fact);
      57         [ +  + ]:        110 :         if (bitOpt.has_value())
      58                 :            :         {
      59                 :         57 :           bits.insert(*bitOpt);
      60                 :            :         }
      61                 :        110 :       }
      62                 :            :     }
      63                 :        324 :   }
      64                 :            : 
      65                 :            :   // collect bitsums
      66                 :         66 :   auto nm = nodeManager();
      67                 :         66 :   std::unordered_map<Node, Node> cache{};
      68         [ +  + ]:        390 :   for (uint64_t i = 0, n = assertionsToPreprocess->size(); i < n; ++i)
      69                 :            :   {
      70                 :        324 :     Node fact = (*assertionsToPreprocess)[i];
      71                 :        324 :     for (TNode current :
      72                 :       1851 :          NodeDfsIterable(fact, VisitOrder::POSTORDER, [&cache](TNode nn) {
      73                 :       1851 :            return cache.count(nn);
      74         [ +  + ]:       2096 :          }))
      75                 :            :     {
      76                 :       1448 :       Node translation;
      77 [ -  + ][ -  + ]:       1448 :       Assert(!cache.count(current));
                 [ -  - ]
      78         [ +  + ]:       1448 :       if (current.getNumChildren() == 0)
      79                 :            :       {
      80                 :        430 :         translation = current;
      81                 :            :       }
      82                 :            :       else
      83                 :            :       {
      84                 :       1018 :         Kind oldKind = current.getKind();
      85                 :       1018 :         NodeBuilder builder(nm, oldKind);
      86         [ +  + ]:       1018 :         if (current.getMetaKind() == kind::MetaKind::PARAMETERIZED)
      87                 :            :         {
      88                 :         32 :           builder << current.getOperator();
      89                 :            :         }
      90         [ +  + ]:       3225 :         for (TNode c : current)
      91                 :            :         {
      92                 :       2207 :           builder << cache.at(c);
      93                 :       2207 :         }
      94                 :       1018 :         translation = builder;
      95         [ +  + ]:       1018 :         if (translation.getKind() == Kind::FINITE_FIELD_ADD)
      96                 :            :         {
      97                 :        143 :           auto bs = theory::ff::parse::bitSums(translation, bits);
      98 [ +  + ][ +  + ]:        143 :           if (bs.has_value() && bs->first.size() > 0)
                 [ +  + ]
      99                 :            :           {
     100         [ +  + ]:         20 :             for (const auto& [multiplier, bitSeq] : bs->first)
     101                 :            :             {
     102 [ -  + ][ -  + ]:         10 :               Assert(bitSeq.size() > 1);
                 [ -  - ]
     103                 :         10 :               Node bitsum = nm->mkNode(Kind::FINITE_FIELD_BITSUM, bitSeq);
     104                 :         10 :               Node scaled = multiplier.isOne()
     105                 :            :                                 ? bitsum
     106                 :            :                                 : nm->mkNode(Kind::FINITE_FIELD_MULT,
     107         [ -  - ]:          0 :                                              nm->mkConst(multiplier),
     108                 :         14 :                                              bitsum);
     109         [ +  - ]:         10 :               Trace("ff::bitsum") << "found " << scaled << std::endl;
     110                 :         10 :               bs->second.push_back(scaled);
     111                 :         10 :             }
     112                 :         10 :             translation = mkAdd(nm, std::move(bs->second));
     113                 :            :           }
     114                 :        143 :         }
     115                 :       1018 :       }
     116                 :       1448 :       cache[current] = translation;
     117                 :       1772 :     }
     118                 :        324 :     Node newFact = cache[fact];
     119         [ +  + ]:        324 :     if (newFact != fact)
     120                 :            :     {
     121                 :         18 :       assertionsToPreprocess->replace(
     122                 :            :           i, newFact, nullptr, TrustId::PREPROCESS_FF_BITSUM);
     123                 :            :     }
     124                 :        324 :   }
     125                 :            : 
     126                 :         66 :   return PreprocessingPassResult::NO_CONFLICT;
     127                 :         66 : }
     128                 :            : 
     129                 :            : }  // namespace passes
     130                 :            : }  // namespace preprocessing
     131                 :            : }  // namespace cvc5::internal