1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Haniel Barbosa, Andrew Reynolds, Gereon Kremer |
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 NlExtPurify preprocessing pass. |
14 |
|
* |
15 |
|
* Purifies non-linear terms. |
16 |
|
*/ |
17 |
|
|
18 |
|
#include "preprocessing/passes/nl_ext_purify.h" |
19 |
|
|
20 |
|
#include "expr/skolem_manager.h" |
21 |
|
#include "preprocessing/assertion_pipeline.h" |
22 |
|
#include "theory/rewriter.h" |
23 |
|
|
24 |
|
namespace cvc5 { |
25 |
|
namespace preprocessing { |
26 |
|
namespace passes { |
27 |
|
|
28 |
|
using namespace std; |
29 |
|
using namespace cvc5::theory; |
30 |
|
|
31 |
2421 |
Node NlExtPurify::purifyNlTerms(TNode n, |
32 |
|
NodeMap& cache, |
33 |
|
NodeMap& bcache, |
34 |
|
std::vector<Node>& var_eq, |
35 |
|
bool beneathMult) |
36 |
|
{ |
37 |
2421 |
NodeManager* nm = NodeManager::currentNM(); |
38 |
2421 |
SkolemManager* sm = nm->getSkolemManager(); |
39 |
2421 |
if (beneathMult) |
40 |
|
{ |
41 |
2258 |
NodeMap::iterator find = bcache.find(n); |
42 |
2258 |
if (find != bcache.end()) |
43 |
|
{ |
44 |
2147 |
return (*find).second; |
45 |
|
} |
46 |
|
} |
47 |
|
else |
48 |
|
{ |
49 |
163 |
NodeMap::iterator find = cache.find(n); |
50 |
163 |
if (find != cache.end()) |
51 |
|
{ |
52 |
20 |
return (*find).second; |
53 |
|
} |
54 |
|
} |
55 |
254 |
if (n.isClosure()) |
56 |
|
{ |
57 |
|
// don't traverse quantified formulas |
58 |
1 |
return n; |
59 |
|
} |
60 |
506 |
Node ret = n; |
61 |
253 |
if (n.getNumChildren() > 0) |
62 |
|
{ |
63 |
182 |
if (beneathMult |
64 |
182 |
&& (n.getKind() == kind::PLUS || n.getKind() == kind::MINUS)) |
65 |
|
{ |
66 |
|
// don't do it if it rewrites to a constant |
67 |
2 |
Node nr = rewrite(n); |
68 |
1 |
if (nr.isConst()) |
69 |
|
{ |
70 |
|
// return the rewritten constant |
71 |
|
ret = nr; |
72 |
|
} |
73 |
|
else |
74 |
|
{ |
75 |
|
// new variable |
76 |
3 |
ret = sm->mkDummySkolem("__purifyNl_var", |
77 |
2 |
n.getType(), |
78 |
|
"Variable introduced in purifyNl pass"); |
79 |
2 |
Node np = purifyNlTerms(n, cache, bcache, var_eq, false); |
80 |
1 |
var_eq.push_back(np.eqNode(ret)); |
81 |
2 |
Trace("nl-ext-purify") << "Purify : " << ret << " -> " << np |
82 |
1 |
<< std::endl; |
83 |
|
} |
84 |
|
} |
85 |
|
else |
86 |
|
{ |
87 |
181 |
bool beneathMultNew = beneathMult || n.getKind() == kind::MULT; |
88 |
181 |
bool childChanged = false; |
89 |
362 |
std::vector<Node> children; |
90 |
2583 |
for (unsigned i = 0, size = n.getNumChildren(); i < size; ++i) |
91 |
|
{ |
92 |
4804 |
Node nc = purifyNlTerms(n[i], cache, bcache, var_eq, beneathMultNew); |
93 |
2402 |
childChanged = childChanged || nc != n[i]; |
94 |
2402 |
children.push_back(nc); |
95 |
|
} |
96 |
181 |
if (childChanged) |
97 |
|
{ |
98 |
9 |
ret = nm->mkNode(n.getKind(), children); |
99 |
|
} |
100 |
|
} |
101 |
|
} |
102 |
253 |
if (beneathMult) |
103 |
|
{ |
104 |
111 |
bcache[n] = ret; |
105 |
|
} |
106 |
|
else |
107 |
|
{ |
108 |
142 |
cache[n] = ret; |
109 |
|
} |
110 |
253 |
return ret; |
111 |
|
} |
112 |
|
|
113 |
6271 |
NlExtPurify::NlExtPurify(PreprocessingPassContext* preprocContext) |
114 |
6271 |
: PreprocessingPass(preprocContext, "nl-ext-purify"){}; |
115 |
|
|
116 |
4 |
PreprocessingPassResult NlExtPurify::applyInternal( |
117 |
|
AssertionPipeline* assertionsToPreprocess) |
118 |
|
{ |
119 |
8 |
unordered_map<Node, Node> cache; |
120 |
8 |
unordered_map<Node, Node> bcache; |
121 |
8 |
std::vector<Node> var_eq; |
122 |
4 |
unsigned size = assertionsToPreprocess->size(); |
123 |
22 |
for (unsigned i = 0; i < size; ++i) |
124 |
|
{ |
125 |
36 |
Node a = (*assertionsToPreprocess)[i]; |
126 |
36 |
Node ap = purifyNlTerms(a, cache, bcache, var_eq); |
127 |
18 |
if (a != ap) |
128 |
|
{ |
129 |
2 |
assertionsToPreprocess->replace(i, ap); |
130 |
4 |
Trace("nl-ext-purify") |
131 |
2 |
<< "Purify : " << a << " -> " << (*assertionsToPreprocess)[i] << "\n"; |
132 |
|
} |
133 |
|
} |
134 |
4 |
if (!var_eq.empty()) |
135 |
|
{ |
136 |
1 |
unsigned lastIndex = size - 1; |
137 |
2 |
Node veq = NodeManager::currentNM()->mkAnd(var_eq); |
138 |
1 |
assertionsToPreprocess->conjoin(lastIndex, veq); |
139 |
|
} |
140 |
8 |
return PreprocessingPassResult::NO_CONFLICT; |
141 |
|
} |
142 |
|
|
143 |
|
|
144 |
|
} // namespace passes |
145 |
|
} // namespace preprocessing |
146 |
22746 |
} // namespace cvc5 |