GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/preprocessing/passes/bv_intro_pow2.cpp Lines: 37 39 94.9 %
Date: 2021-03-22 Branches: 61 121 50.4 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file bv_intro_pow2.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Mathias Preiner, Liana Hadarean
6
 ** This file is part of the CVC4 project.
7
 ** Copyright (c) 2009-2021 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 BvIntroPow2 preprocessing pass
13
 **
14
 ** Traverses the formula and applies the IsPowerOfTwo rewrite rule. This
15
 ** preprocessing pass is particularly useful on QF_BV/pspace benchmarks and
16
 ** can be enabled via option `--bv-intro-pow2`.
17
 **/
18
19
#include "preprocessing/passes/bv_intro_pow2.h"
20
21
#include <unordered_map>
22
23
#include "preprocessing/assertion_pipeline.h"
24
#include "preprocessing/preprocessing_pass_context.h"
25
#include "theory/bv/theory_bv_rewrite_rules_simplification.h"
26
#include "theory/rewriter.h"
27
28
namespace CVC4 {
29
namespace preprocessing {
30
namespace passes {
31
32
using NodeMap = std::unordered_map<Node, Node, NodeHashFunction>;
33
using namespace CVC4::theory;
34
35
namespace {
36
37
24
Node pow2Rewrite(Node node, NodeMap& cache)
38
{
39
24
  NodeMap::const_iterator ci = cache.find(node);
40
24
  if (ci != cache.end())
41
  {
42
    Node incache = (*ci).second;
43
    return incache.isNull() ? node : incache;
44
  }
45
46
48
  Node res = Node::null();
47
24
  switch (node.getKind())
48
  {
49
6
    case kind::AND:
50
    {
51
6
      bool changed = false;
52
12
      std::vector<Node> children;
53
18
      for (unsigned i = 0, size = node.getNumChildren(); i < size; ++i)
54
      {
55
24
        Node child = node[i];
56
24
        Node found = pow2Rewrite(child, cache);
57
12
        changed = changed || (child != found);
58
12
        children.push_back(found);
59
      }
60
6
      if (changed)
61
      {
62
6
        res = NodeManager::currentNM()->mkNode(kind::AND, children);
63
6
      }
64
    }
65
6
    break;
66
67
8
    case kind::EQUAL:
68
24
      if (node[0].getType().isBitVector()
69
24
          && theory::bv::RewriteRule<theory::bv::IsPowerOfTwo>::applies(node))
70
      {
71
6
        res = theory::bv::RewriteRule<theory::bv::IsPowerOfTwo>::run<false>(node);
72
      }
73
8
      break;
74
10
    default: break;
75
  }
76
77
24
  cache.insert(std::make_pair(node, res));
78
24
  return res.isNull() ? node : res;
79
}
80
81
}  // namespace
82
83
8995
BvIntroPow2::BvIntroPow2(PreprocessingPassContext* preprocContext)
84
8995
    : PreprocessingPass(preprocContext, "bv-intro-pow2"){};
85
86
2
PreprocessingPassResult BvIntroPow2::applyInternal(
87
    AssertionPipeline* assertionsToPreprocess)
88
{
89
4
  std::unordered_map<Node, Node, NodeHashFunction> cache;
90
14
  for (unsigned i = 0, size = assertionsToPreprocess->size(); i < size; ++i)
91
  {
92
24
    Node cur = (*assertionsToPreprocess)[i];
93
24
    Node res = pow2Rewrite(cur, cache);
94
12
    if (res != cur)
95
    {
96
6
      res = Rewriter::rewrite(res);
97
6
      assertionsToPreprocess->replace(i, res);
98
    }
99
  }
100
4
  return PreprocessingPassResult::NO_CONFLICT;
101
}
102
103
104
}/* CVC4::theory::bv namespace */
105
}/* CVC4::theory namespace */
106
107
26676
}/* CVC4 namespace */