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