1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Andrew Reynolds, Mathias Preiner, 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 |
|
* Implements techniques for candidate rewrite rule filtering, which |
14 |
|
* filters the output of --sygus-rr-synth. The classes in this file implement |
15 |
|
* filtering based on congruence, variable ordering, and matching. |
16 |
|
*/ |
17 |
|
|
18 |
|
#include "theory/quantifiers/candidate_rewrite_filter.h" |
19 |
|
|
20 |
|
#include "options/base_options.h" |
21 |
|
#include "options/quantifiers_options.h" |
22 |
|
#include "printer/printer.h" |
23 |
|
|
24 |
|
using namespace cvc5::kind; |
25 |
|
|
26 |
|
namespace cvc5 { |
27 |
|
namespace theory { |
28 |
|
namespace quantifiers { |
29 |
|
|
30 |
|
// the number of d_drewrite objects we have allocated (to avoid name conflicts) |
31 |
|
static unsigned drewrite_counter = 0; |
32 |
|
|
33 |
62 |
CandidateRewriteFilter::CandidateRewriteFilter() |
34 |
|
: d_ss(nullptr), |
35 |
|
d_tds(nullptr), |
36 |
|
d_use_sygus_type(false), |
37 |
|
d_drewrite(nullptr), |
38 |
62 |
d_ssenm(*this) |
39 |
|
{ |
40 |
62 |
} |
41 |
|
|
42 |
7 |
void CandidateRewriteFilter::initialize(SygusSampler* ss, |
43 |
|
TermDbSygus* tds, |
44 |
|
bool useSygusType) |
45 |
|
{ |
46 |
7 |
d_ss = ss; |
47 |
7 |
d_use_sygus_type = useSygusType; |
48 |
7 |
d_tds = tds; |
49 |
|
// initialize members of this class |
50 |
7 |
d_match_trie.clear(); |
51 |
7 |
d_pairs.clear(); |
52 |
|
// (re)initialize the dynamic rewriter |
53 |
14 |
std::stringstream ssn; |
54 |
7 |
ssn << "_dyn_rewriter_" << drewrite_counter; |
55 |
7 |
drewrite_counter++; |
56 |
21 |
d_drewrite = std::unique_ptr<DynamicRewriter>( |
57 |
28 |
new DynamicRewriter(ssn.str(), &d_fake_context)); |
58 |
7 |
} |
59 |
|
|
60 |
229 |
bool CandidateRewriteFilter::filterPair(Node n, Node eq_n) |
61 |
|
{ |
62 |
458 |
Node bn = n; |
63 |
458 |
Node beq_n = eq_n; |
64 |
229 |
if (d_use_sygus_type) |
65 |
|
{ |
66 |
229 |
bn = d_tds->sygusToBuiltin(n); |
67 |
229 |
beq_n = d_tds->sygusToBuiltin(eq_n); |
68 |
|
} |
69 |
458 |
Trace("cr-filter") << "crewriteFilter : " << bn << "..." << beq_n |
70 |
229 |
<< std::endl; |
71 |
|
// whether we will keep this pair |
72 |
229 |
bool keep = true; |
73 |
|
|
74 |
|
// ----- check redundancy based on variables |
75 |
458 |
if (options::sygusRewSynthFilterOrder() |
76 |
229 |
|| options::sygusRewSynthFilterNonLinear()) |
77 |
|
{ |
78 |
916 |
bool nor = d_ss->checkVariables(bn, |
79 |
229 |
options::sygusRewSynthFilterOrder(), |
80 |
458 |
options::sygusRewSynthFilterNonLinear()); |
81 |
916 |
bool eqor = d_ss->checkVariables(beq_n, |
82 |
229 |
options::sygusRewSynthFilterOrder(), |
83 |
458 |
options::sygusRewSynthFilterNonLinear()); |
84 |
458 |
Trace("cr-filter-debug") |
85 |
229 |
<< "Variables ok? : " << nor << " " << eqor << std::endl; |
86 |
229 |
if (eqor || nor) |
87 |
|
{ |
88 |
|
// if only one is ordered, then we require that the ordered one's |
89 |
|
// variables cannot be a strict subset of the variables of the other. |
90 |
356 |
if (!eqor) |
91 |
|
{ |
92 |
3 |
if (d_ss->containsFreeVariables(beq_n, bn, true)) |
93 |
|
{ |
94 |
1 |
keep = false; |
95 |
|
} |
96 |
|
else |
97 |
|
{ |
98 |
|
// if the previous value stored was unordered, but n is |
99 |
|
// ordered, we prefer n. Thus, we force its addition to the |
100 |
|
// sampler database. |
101 |
2 |
d_ss->registerTerm(n, true); |
102 |
|
} |
103 |
|
} |
104 |
175 |
else if (!nor) |
105 |
|
{ |
106 |
61 |
keep = !d_ss->containsFreeVariables(bn, beq_n, true); |
107 |
|
} |
108 |
|
} |
109 |
|
else |
110 |
|
{ |
111 |
51 |
keep = false; |
112 |
|
} |
113 |
229 |
if (!keep) |
114 |
|
{ |
115 |
106 |
Trace("cr-filter") << "...redundant (unordered)" << std::endl; |
116 |
|
} |
117 |
|
} |
118 |
|
|
119 |
|
// ----- check rewriting redundancy |
120 |
229 |
if (keep && options::sygusRewSynthFilterCong()) |
121 |
|
{ |
122 |
|
// When using sygus types, this filtering applies to the builtin versions |
123 |
|
// of n and eq_n. This means that we may filter out a rewrite rule for one |
124 |
|
// sygus type based on another, e.g. we won't report x=x+0 for both A and B |
125 |
|
// in: |
126 |
|
// A -> x | 0 | A+A |
127 |
|
// B -> x | 0 | B+B |
128 |
123 |
Trace("cr-filter-debug") << "Check equal rewrite pair..." << std::endl; |
129 |
123 |
if (d_drewrite->areEqual(bn, beq_n)) |
130 |
|
{ |
131 |
|
// must be unique according to the dynamic rewriter |
132 |
2 |
Trace("cr-filter") << "...redundant (rewritable)" << std::endl; |
133 |
2 |
keep = false; |
134 |
|
} |
135 |
|
} |
136 |
|
|
137 |
229 |
if (keep && options::sygusRewSynthFilterMatch()) |
138 |
|
{ |
139 |
|
// ----- check matchable |
140 |
|
// check whether the pair is matchable with a previous one |
141 |
121 |
d_curr_pair_rhs = beq_n; |
142 |
242 |
Trace("crf-match") << "CRF check matches : " << bn << " [rhs = " << beq_n |
143 |
121 |
<< "]..." << std::endl; |
144 |
242 |
Node bni = d_drewrite->toInternal(bn); |
145 |
121 |
if (!bni.isNull()) |
146 |
|
{ |
147 |
|
// as with congruence filtering, we cache based on the builtin type |
148 |
242 |
TypeNode tn = bn.getType(); |
149 |
121 |
if (!d_match_trie[tn].getMatches(bni, &d_ssenm)) |
150 |
|
{ |
151 |
2 |
keep = false; |
152 |
2 |
Trace("cr-filter") << "...redundant (matchable)" << std::endl; |
153 |
|
// regardless, would help to remember it |
154 |
2 |
registerRelevantPair(n, eq_n); |
155 |
|
} |
156 |
|
} |
157 |
|
// if bni is null, it may involve non-first-class types that we cannot |
158 |
|
// reason about |
159 |
|
} |
160 |
|
|
161 |
229 |
if (keep) |
162 |
|
{ |
163 |
119 |
return false; |
164 |
|
} |
165 |
110 |
if (Trace.isOn("sygus-rr-filter")) |
166 |
|
{ |
167 |
|
std::stringstream ss; |
168 |
|
ss << "(redundant-rewrite "; |
169 |
|
TermDbSygus::toStreamSygus(ss, n); |
170 |
|
ss << " "; |
171 |
|
TermDbSygus::toStreamSygus(ss, eq_n); |
172 |
|
ss << ")"; |
173 |
|
Trace("sygus-rr-filter") << ss.str() << std::endl; |
174 |
|
} |
175 |
110 |
return true; |
176 |
|
} |
177 |
|
|
178 |
105 |
void CandidateRewriteFilter::registerRelevantPair(Node n, Node eq_n) |
179 |
|
{ |
180 |
210 |
Node bn = n; |
181 |
210 |
Node beq_n = eq_n; |
182 |
105 |
if (d_use_sygus_type) |
183 |
|
{ |
184 |
105 |
bn = d_tds->sygusToBuiltin(n); |
185 |
105 |
beq_n = d_tds->sygusToBuiltin(eq_n); |
186 |
|
} |
187 |
|
// ----- check rewriting redundancy |
188 |
105 |
if (options::sygusRewSynthFilterCong()) |
189 |
|
{ |
190 |
105 |
Trace("cr-filter-debug") << "Add rewrite pair..." << std::endl; |
191 |
105 |
Assert(!d_drewrite->areEqual(bn, beq_n)); |
192 |
105 |
d_drewrite->addRewrite(bn, beq_n); |
193 |
|
} |
194 |
105 |
if (options::sygusRewSynthFilterMatch()) |
195 |
|
{ |
196 |
|
// cache based on the builtin type |
197 |
210 |
TypeNode tn = bn.getType(); |
198 |
|
// add to match information |
199 |
315 |
for (unsigned r = 0; r < 2; r++) |
200 |
|
{ |
201 |
420 |
Node t = r == 0 ? bn : beq_n; |
202 |
420 |
Node to = r == 0 ? beq_n : bn; |
203 |
|
// insert in match trie if first time |
204 |
210 |
if (d_pairs.find(t) == d_pairs.end()) |
205 |
|
{ |
206 |
148 |
Trace("crf-match") << "CRF add term : " << t << std::endl; |
207 |
296 |
Node ti = d_drewrite->toInternal(t); |
208 |
148 |
if (!ti.isNull()) |
209 |
|
{ |
210 |
148 |
d_match_trie[tn].addTerm(ti); |
211 |
|
} |
212 |
|
} |
213 |
210 |
d_pairs[t].insert(to); |
214 |
|
} |
215 |
|
} |
216 |
105 |
} |
217 |
|
|
218 |
80 |
bool CandidateRewriteFilter::notify(Node s, |
219 |
|
Node n, |
220 |
|
std::vector<Node>& vars, |
221 |
|
std::vector<Node>& subs) |
222 |
|
{ |
223 |
80 |
Trace("crf-match-debug") << "Got : " << s << " matches " << n << std::endl; |
224 |
80 |
Assert(!d_curr_pair_rhs.isNull()); |
225 |
|
// convert back to original forms |
226 |
80 |
s = d_drewrite->toExternal(s); |
227 |
80 |
Assert(!s.isNull()); |
228 |
80 |
n = d_drewrite->toExternal(n); |
229 |
80 |
Assert(!n.isNull()); |
230 |
80 |
std::map<Node, std::unordered_set<Node> >::iterator it = d_pairs.find(n); |
231 |
80 |
if (Trace.isOn("crf-match")) |
232 |
|
{ |
233 |
|
Trace("crf-match") << " " << s << " matches " << n |
234 |
|
<< " under:" << std::endl; |
235 |
|
for (unsigned i = 0, size = vars.size(); i < size; i++) |
236 |
|
{ |
237 |
|
Trace("crf-match") << " " << vars[i] << " -> " << subs[i] << std::endl; |
238 |
|
} |
239 |
|
} |
240 |
|
#ifdef CVC5_ASSERTIONS |
241 |
164 |
for (unsigned i = 0, size = vars.size(); i < size; i++) |
242 |
|
{ |
243 |
|
// By using internal representation of terms, we ensure polymorphism is |
244 |
|
// handled correctly. |
245 |
84 |
Assert(vars[i].getType().isComparableTo(subs[i].getType())); |
246 |
|
} |
247 |
|
#endif |
248 |
|
// must convert the inferred substitution to original form |
249 |
160 |
std::vector<Node> esubs; |
250 |
164 |
for (const Node& sb : subs) |
251 |
|
{ |
252 |
84 |
esubs.push_back(d_drewrite->toExternal(sb)); |
253 |
|
} |
254 |
80 |
Assert(it != d_pairs.end()); |
255 |
656 |
for (const Node& nr : it->second) |
256 |
|
{ |
257 |
|
Node nrs = |
258 |
1154 |
nr.substitute(vars.begin(), vars.end(), esubs.begin(), esubs.end()); |
259 |
578 |
bool areEqual = (nrs == d_curr_pair_rhs); |
260 |
578 |
if (!areEqual && options::sygusRewSynthFilterCong()) |
261 |
|
{ |
262 |
|
// if dynamic rewriter is available, consult it |
263 |
576 |
areEqual = d_drewrite->areEqual(nrs, d_curr_pair_rhs); |
264 |
|
} |
265 |
578 |
if (areEqual) |
266 |
|
{ |
267 |
2 |
Trace("crf-match") << "*** Match, current pair: " << std::endl; |
268 |
4 |
Trace("crf-match") << " (" << s << ", " << d_curr_pair_rhs << ")" |
269 |
2 |
<< std::endl; |
270 |
2 |
Trace("crf-match") << "is an instance of previous pair:" << std::endl; |
271 |
2 |
Trace("crf-match") << " (" << n << ", " << nr << ")" << std::endl; |
272 |
2 |
return false; |
273 |
|
} |
274 |
|
} |
275 |
78 |
return true; |
276 |
|
} |
277 |
|
|
278 |
|
} // namespace quantifiers |
279 |
|
} // namespace theory |
280 |
29499 |
} // namespace cvc5 |