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-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. |
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 { |
29 |
|
namespace preprocessing { |
30 |
|
namespace passes { |
31 |
|
|
32 |
|
using NodeMap = std::unordered_map<Node, Node>; |
33 |
|
using namespace cvc5::theory; |
34 |
|
|
35 |
15340 |
BvIntroPow2::BvIntroPow2(PreprocessingPassContext* preprocContext) |
36 |
15340 |
: PreprocessingPass(preprocContext, "bv-intro-pow2"){}; |
37 |
|
|
38 |
2 |
PreprocessingPassResult BvIntroPow2::applyInternal( |
39 |
|
AssertionPipeline* assertionsToPreprocess) |
40 |
|
{ |
41 |
4 |
std::unordered_map<Node, Node> cache; |
42 |
14 |
for (size_t i = 0, size = assertionsToPreprocess->size(); i < size; ++i) |
43 |
|
{ |
44 |
24 |
Node cur = (*assertionsToPreprocess)[i]; |
45 |
24 |
Node res = pow2Rewrite(cur, cache); |
46 |
12 |
if (res != cur) |
47 |
|
{ |
48 |
6 |
res = rewrite(res); |
49 |
6 |
assertionsToPreprocess->replace(i, res); |
50 |
|
} |
51 |
|
} |
52 |
4 |
return PreprocessingPassResult::NO_CONFLICT; |
53 |
|
} |
54 |
|
|
55 |
8 |
bool BvIntroPow2::isPowerOfTwo(TNode node) |
56 |
|
{ |
57 |
8 |
if (node.getKind() != kind::EQUAL) |
58 |
|
{ |
59 |
|
return false; |
60 |
|
} |
61 |
24 |
if (node[0].getKind() != kind::BITVECTOR_AND |
62 |
24 |
&& node[1].getKind() != kind::BITVECTOR_AND) |
63 |
|
{ |
64 |
2 |
return false; |
65 |
|
} |
66 |
6 |
if (!bv::utils::isZero(node[0]) && !bv::utils::isZero(node[1])) |
67 |
|
{ |
68 |
|
return false; |
69 |
|
} |
70 |
|
|
71 |
12 |
TNode t = !bv::utils::isZero(node[0]) ? node[0] : node[1]; |
72 |
6 |
if (t.getNumChildren() != 2) return false; |
73 |
12 |
TNode a = t[0]; |
74 |
12 |
TNode b = t[1]; |
75 |
6 |
if (bv::utils::getSize(t) < 2) return false; |
76 |
|
Node diff = |
77 |
12 |
rewrite(NodeManager::currentNM()->mkNode(kind::BITVECTOR_SUB, a, b)); |
78 |
6 |
return (diff.isConst() |
79 |
12 |
&& (bv::utils::isOne(diff) || bv::utils::isOnes(diff))); |
80 |
|
} |
81 |
|
|
82 |
6 |
Node BvIntroPow2::rewritePowerOfTwo(TNode node) |
83 |
|
{ |
84 |
6 |
NodeManager* nm = NodeManager::currentNM(); |
85 |
12 |
TNode term = bv::utils::isZero(node[0]) ? node[1] : node[0]; |
86 |
12 |
TNode a = term[0]; |
87 |
12 |
TNode b = term[1]; |
88 |
6 |
uint32_t size = bv::utils::getSize(term); |
89 |
12 |
Node diff = rewrite(nm->mkNode(kind::BITVECTOR_SUB, a, b)); |
90 |
6 |
Assert(diff.isConst()); |
91 |
12 |
Node one = bv::utils::mkOne(size); |
92 |
12 |
TNode x = diff == one ? a : b; |
93 |
12 |
Node sk = bv::utils::mkVar(size); |
94 |
12 |
Node sh = nm->mkNode(kind::BITVECTOR_SHL, one, sk); |
95 |
6 |
Node x_eq_sh = nm->mkNode(kind::EQUAL, x, sh); |
96 |
12 |
return x_eq_sh; |
97 |
|
} |
98 |
|
|
99 |
24 |
Node BvIntroPow2::pow2Rewrite(Node node, std::unordered_map<Node, Node>& cache) |
100 |
|
{ |
101 |
24 |
const auto& ci = cache.find(node); |
102 |
24 |
if (ci != cache.end()) |
103 |
|
{ |
104 |
|
Node incache = (*ci).second; |
105 |
|
return incache.isNull() ? node : incache; |
106 |
|
} |
107 |
|
|
108 |
48 |
Node res = Node::null(); |
109 |
24 |
switch (node.getKind()) |
110 |
|
{ |
111 |
6 |
case kind::AND: |
112 |
|
{ |
113 |
6 |
bool changed = false; |
114 |
12 |
std::vector<Node> children; |
115 |
18 |
for (unsigned i = 0, size = node.getNumChildren(); i < size; ++i) |
116 |
|
{ |
117 |
24 |
Node child = node[i]; |
118 |
24 |
Node found = pow2Rewrite(child, cache); |
119 |
12 |
changed = changed || (child != found); |
120 |
12 |
children.push_back(found); |
121 |
|
} |
122 |
6 |
if (changed) |
123 |
|
{ |
124 |
6 |
res = NodeManager::currentNM()->mkNode(kind::AND, children); |
125 |
6 |
} |
126 |
|
} |
127 |
6 |
break; |
128 |
|
|
129 |
8 |
case kind::EQUAL: |
130 |
8 |
if (node[0].getType().isBitVector() && isPowerOfTwo(node)) |
131 |
|
{ |
132 |
6 |
res = rewritePowerOfTwo(node); |
133 |
|
} |
134 |
8 |
break; |
135 |
10 |
default: break; |
136 |
|
} |
137 |
|
|
138 |
24 |
cache.insert(std::make_pair(node, res)); |
139 |
24 |
return res.isNull() ? node : res; |
140 |
|
} |
141 |
|
|
142 |
|
} // namespace passes |
143 |
|
} // namespace preprocessing |
144 |
|
|
145 |
31137 |
} // namespace cvc5 |