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_rewrite_rules_simplification.h" |
27 |
|
#include "theory/rewriter.h" |
28 |
|
|
29 |
|
namespace cvc5 { |
30 |
|
namespace preprocessing { |
31 |
|
namespace passes { |
32 |
|
|
33 |
|
using NodeMap = std::unordered_map<Node, Node>; |
34 |
|
using namespace cvc5::theory; |
35 |
|
|
36 |
|
namespace { |
37 |
|
|
38 |
24 |
Node pow2Rewrite(Node node, NodeMap& cache) |
39 |
|
{ |
40 |
24 |
NodeMap::const_iterator ci = cache.find(node); |
41 |
24 |
if (ci != cache.end()) |
42 |
|
{ |
43 |
|
Node incache = (*ci).second; |
44 |
|
return incache.isNull() ? node : incache; |
45 |
|
} |
46 |
|
|
47 |
48 |
Node res = Node::null(); |
48 |
24 |
switch (node.getKind()) |
49 |
|
{ |
50 |
6 |
case kind::AND: |
51 |
|
{ |
52 |
6 |
bool changed = false; |
53 |
12 |
std::vector<Node> children; |
54 |
18 |
for (unsigned i = 0, size = node.getNumChildren(); i < size; ++i) |
55 |
|
{ |
56 |
24 |
Node child = node[i]; |
57 |
24 |
Node found = pow2Rewrite(child, cache); |
58 |
12 |
changed = changed || (child != found); |
59 |
12 |
children.push_back(found); |
60 |
|
} |
61 |
6 |
if (changed) |
62 |
|
{ |
63 |
6 |
res = NodeManager::currentNM()->mkNode(kind::AND, children); |
64 |
6 |
} |
65 |
|
} |
66 |
6 |
break; |
67 |
|
|
68 |
8 |
case kind::EQUAL: |
69 |
24 |
if (node[0].getType().isBitVector() |
70 |
24 |
&& theory::bv::RewriteRule<theory::bv::IsPowerOfTwo>::applies(node)) |
71 |
|
{ |
72 |
6 |
res = theory::bv::RewriteRule<theory::bv::IsPowerOfTwo>::run<false>(node); |
73 |
|
} |
74 |
8 |
break; |
75 |
10 |
default: break; |
76 |
|
} |
77 |
|
|
78 |
24 |
cache.insert(std::make_pair(node, res)); |
79 |
24 |
return res.isNull() ? node : res; |
80 |
|
} |
81 |
|
|
82 |
|
} // namespace |
83 |
|
|
84 |
9913 |
BvIntroPow2::BvIntroPow2(PreprocessingPassContext* preprocContext) |
85 |
9913 |
: PreprocessingPass(preprocContext, "bv-intro-pow2"){}; |
86 |
|
|
87 |
2 |
PreprocessingPassResult BvIntroPow2::applyInternal( |
88 |
|
AssertionPipeline* assertionsToPreprocess) |
89 |
|
{ |
90 |
4 |
std::unordered_map<Node, Node> cache; |
91 |
14 |
for (unsigned i = 0, size = assertionsToPreprocess->size(); i < size; ++i) |
92 |
|
{ |
93 |
24 |
Node cur = (*assertionsToPreprocess)[i]; |
94 |
24 |
Node res = pow2Rewrite(cur, cache); |
95 |
12 |
if (res != cur) |
96 |
|
{ |
97 |
6 |
res = rewrite(res); |
98 |
6 |
assertionsToPreprocess->replace(i, res); |
99 |
|
} |
100 |
|
} |
101 |
4 |
return PreprocessingPassResult::NO_CONFLICT; |
102 |
|
} |
103 |
|
|
104 |
|
} // namespace passes |
105 |
|
} // namespace preprocessing |
106 |
|
|
107 |
29502 |
} // namespace cvc5 |