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                 :            :  * The BVToInt preprocessing pass.
      11                 :            :  *
      12                 :            :  * Converts bit-vector operations into integer operations.
      13                 :            :  *
      14                 :            :  */
      15                 :            : 
      16                 :            : #include "preprocessing/passes/bv_to_int.h"
      17                 :            : 
      18                 :            : #include <cmath>
      19                 :            : #include <string>
      20                 :            : #include <unordered_map>
      21                 :            : #include <vector>
      22                 :            : 
      23                 :            : #include "expr/node.h"
      24                 :            : #include "expr/node_traversal.h"
      25                 :            : #include "options/smt_options.h"
      26                 :            : #include "options/uf_options.h"
      27                 :            : #include "preprocessing/assertion_pipeline.h"
      28                 :            : #include "theory/bv/theory_bv_rewrite_rules_operator_elimination.h"
      29                 :            : #include "theory/bv/theory_bv_rewrite_rules_simplification.h"
      30                 :            : #include "theory/rewriter.h"
      31                 :            : 
      32                 :            : namespace cvc5::internal {
      33                 :            : namespace preprocessing {
      34                 :            : namespace passes {
      35                 :            : 
      36                 :            : using namespace std;
      37                 :            : using namespace cvc5::internal::theory;
      38                 :            : using namespace cvc5::internal::theory::bv;
      39                 :            : 
      40                 :      51930 : BVToInt::BVToInt(PreprocessingPassContext* preprocContext)
      41                 :            :     : PreprocessingPass(preprocContext, "bv-to-int"),
      42                 :      51930 :       d_intBlaster(preprocContext->getEnv(),
      43                 :      51930 :                    options().smt.solveBVAsInt,
      44                 :      51930 :                    options().smt.BVAndIntegerGranularity)
      45                 :            : {
      46                 :      51930 : }
      47                 :            : 
      48                 :        542 : PreprocessingPassResult BVToInt::applyInternal(
      49                 :            :     AssertionPipeline* assertionsToPreprocess)
      50                 :            : {
      51                 :            :   // vector of boolean nodes for additional constraints
      52                 :            :   // this will always contain range constraints
      53                 :            :   // and for options::SolveBVAsIntMode::BITWISE, it will
      54                 :            :   // also include bitwise assertion constraints
      55                 :        542 :   std::vector<TrustNode> additionalConstraints;
      56                 :        542 :   std::map<Node, Node> skolems;
      57         [ +  + ]:       2374 :   for (uint64_t i = 0; i < assertionsToPreprocess->size(); ++i)
      58                 :            :   {
      59                 :            :     // ensure bv rewritten
      60                 :       1834 :     assertionsToPreprocess->ensureRewritten(i);
      61                 :       1834 :     Node bvNode = (*assertionsToPreprocess)[i];
      62                 :            :     TrustNode tr =
      63                 :       1836 :         d_intBlaster.trustedIntBlast(bvNode, additionalConstraints, skolems);
      64         [ +  + ]:       1832 :     if (tr.isNull())
      65                 :            :     {
      66                 :            :       // int blaster did not apply
      67                 :        897 :       continue;
      68                 :            :     }
      69         [ +  - ]:        935 :     Trace("bv-to-int-debug") << "bv node: " << bvNode << std::endl;
      70                 :        935 :     Trace("bv-to-int-debug") << "int node: " << tr.getProven()[1] << std::endl;
      71                 :        935 :     assertionsToPreprocess->replaceTrusted(i, tr);
      72                 :            :     // ensure integer rewritten
      73                 :        935 :     assertionsToPreprocess->ensureRewritten(i);
      74 [ +  + ][ +  + ]:       2731 :   }
      75                 :        540 :   addFinalizeAssertions(assertionsToPreprocess, additionalConstraints);
      76                 :        540 :   addSkolemDefinitions(skolems);
      77                 :        540 :   return PreprocessingPassResult::NO_CONFLICT;
      78                 :        544 : }
      79                 :            : 
      80                 :        540 : void BVToInt::addSkolemDefinitions(const std::map<Node, Node>& skolems)
      81                 :            : {
      82                 :        540 :   map<Node, Node>::const_iterator it;
      83         [ +  + ]:       1600 :   for (it = skolems.begin(); it != skolems.end(); it++)
      84                 :            :   {
      85                 :       1060 :     Node originalSkolem = it->first;
      86                 :       1060 :     Node definition = it->second;
      87                 :       1060 :     std::vector<Node> args;
      88                 :       1060 :     Node body;
      89         [ +  + ]:       1060 :     if (definition.getType().isFunction())
      90                 :            :     {
      91                 :        129 :       args.insert(args.end(), definition[0].begin(), definition[0].end());
      92                 :        129 :       body = definition[1];
      93                 :            :     }
      94                 :            :     else
      95                 :            :     {
      96                 :        931 :       body = definition;
      97                 :            :     }
      98         [ +  - ]:       2120 :     Trace("bv-to-int-debug") << "adding substitution: " << "[" << originalSkolem
      99                 :       1060 :                              << "] ----> [" << definition << "]" << std::endl;
     100                 :       1060 :     d_preprocContext->addSubstitution(originalSkolem, definition);
     101                 :       1060 :   }
     102                 :        540 : }
     103                 :            : 
     104                 :        540 : void BVToInt::addFinalizeAssertions(
     105                 :            :     AssertionPipeline* assertionsToPreprocess,
     106                 :            :     const std::vector<TrustNode>& additionalConstraints)
     107                 :            : {
     108         [ +  - ]:        540 :   Trace("bv-to-int-debug") << "range constraints:" << std::endl;
     109         [ +  + ]:       1583 :   for (const TrustNode& tlem : additionalConstraints)
     110                 :            :   {
     111 [ +  - ][ -  + ]:       1043 :     Trace("bv-to-int-debug") << "- " << tlem.getProven() << std::endl;
                 [ -  - ]
     112                 :       1043 :     assertionsToPreprocess->pushBackTrusted(tlem);
     113                 :            :   }
     114                 :        540 : }
     115                 :            : 
     116                 :            : }  // namespace passes
     117                 :            : }  // namespace preprocessing
     118                 :            : }  // namespace cvc5::internal