1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Andrew Reynolds, Gereon Kremer, 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 |
|
* Implementation of inference to proof conversion. |
14 |
|
*/ |
15 |
|
|
16 |
|
#include "theory/strings/infer_proof_cons.h" |
17 |
|
|
18 |
|
#include "expr/skolem_manager.h" |
19 |
|
#include "options/smt_options.h" |
20 |
|
#include "options/strings_options.h" |
21 |
|
#include "proof/proof_node_manager.h" |
22 |
|
#include "theory/builtin/proof_checker.h" |
23 |
|
#include "theory/rewriter.h" |
24 |
|
#include "theory/strings/regexp_operation.h" |
25 |
|
#include "theory/strings/theory_strings_utils.h" |
26 |
|
#include "util/statistics_registry.h" |
27 |
|
|
28 |
|
using namespace cvc5::kind; |
29 |
|
|
30 |
|
namespace cvc5 { |
31 |
|
namespace theory { |
32 |
|
namespace strings { |
33 |
|
|
34 |
1245 |
InferProofCons::InferProofCons(context::Context* c, |
35 |
|
ProofNodeManager* pnm, |
36 |
1245 |
SequencesStatistics& statistics) |
37 |
1245 |
: d_pnm(pnm), d_lazyFactMap(c), d_statistics(statistics) |
38 |
|
{ |
39 |
1245 |
Assert(d_pnm != nullptr); |
40 |
1245 |
} |
41 |
|
|
42 |
5024 |
void InferProofCons::notifyFact(const InferInfo& ii) |
43 |
|
{ |
44 |
9988 |
Node fact = ii.d_conc; |
45 |
10048 |
Trace("strings-ipc-debug") |
46 |
5024 |
<< "InferProofCons::notifyFact: " << ii << std::endl; |
47 |
5024 |
if (d_lazyFactMap.find(fact) != d_lazyFactMap.end()) |
48 |
|
{ |
49 |
58 |
Trace("strings-ipc-debug") << "...duplicate!" << std::endl; |
50 |
58 |
return; |
51 |
|
} |
52 |
9930 |
Node symFact = CDProof::getSymmFact(fact); |
53 |
4966 |
if (!symFact.isNull() && d_lazyFactMap.find(symFact) != d_lazyFactMap.end()) |
54 |
|
{ |
55 |
2 |
Trace("strings-ipc-debug") << "...duplicate (sym)!" << std::endl; |
56 |
2 |
return; |
57 |
|
} |
58 |
9928 |
std::shared_ptr<InferInfo> iic = std::make_shared<InferInfo>(ii); |
59 |
4964 |
d_lazyFactMap.insert(ii.d_conc, iic); |
60 |
|
} |
61 |
|
|
62 |
2879 |
void InferProofCons::convert(InferenceId infer, |
63 |
|
bool isRev, |
64 |
|
Node conc, |
65 |
|
const std::vector<Node>& exp, |
66 |
|
ProofStep& ps, |
67 |
|
TheoryProofStepBuffer& psb, |
68 |
|
bool& useBuffer) |
69 |
|
{ |
70 |
|
// by default, don't use the buffer |
71 |
2879 |
useBuffer = false; |
72 |
|
// Must flatten children with respect to AND to be ready to explain. |
73 |
|
// We store the index where each flattened vector begins, since some |
74 |
|
// explanations are grouped together using AND. |
75 |
5758 |
std::vector<size_t> startExpIndex; |
76 |
8578 |
for (const Node& ec : exp) |
77 |
|
{ |
78 |
|
// store the index in the flattened vector |
79 |
5699 |
startExpIndex.push_back(ps.d_children.size()); |
80 |
5699 |
utils::flattenOp(AND, ec, ps.d_children); |
81 |
|
} |
82 |
|
// debug print |
83 |
2879 |
if (Trace.isOn("strings-ipc-debug")) |
84 |
|
{ |
85 |
|
Trace("strings-ipc-debug") << "InferProofCons::convert: " << infer |
86 |
|
<< (isRev ? " :rev " : " ") << conc << std::endl; |
87 |
|
for (const Node& ec : exp) |
88 |
|
{ |
89 |
|
Trace("strings-ipc-debug") << " e: " << ec << std::endl; |
90 |
|
} |
91 |
|
} |
92 |
|
// try to find a set of proof steps to incorporate into the buffer |
93 |
2879 |
psb.clear(); |
94 |
2879 |
NodeManager* nm = NodeManager::currentNM(); |
95 |
5758 |
Node nodeIsRev = nm->mkConst(isRev); |
96 |
2879 |
switch (infer) |
97 |
|
{ |
98 |
|
// ========================== equal by substitution+rewriting |
99 |
730 |
case InferenceId::STRINGS_I_NORM_S: |
100 |
|
case InferenceId::STRINGS_I_CONST_MERGE: |
101 |
|
case InferenceId::STRINGS_I_NORM: |
102 |
|
case InferenceId::STRINGS_LEN_NORM: |
103 |
|
case InferenceId::STRINGS_NORMAL_FORM: |
104 |
|
case InferenceId::STRINGS_CODE_PROXY: |
105 |
|
{ |
106 |
730 |
ps.d_args.push_back(conc); |
107 |
|
// will attempt this rule |
108 |
730 |
ps.d_rule = PfRule::MACRO_SR_PRED_INTRO; |
109 |
|
} |
110 |
730 |
break; |
111 |
|
// ========================== substitution + rewriting |
112 |
290 |
case InferenceId::STRINGS_RE_NF_CONFLICT: |
113 |
|
case InferenceId::STRINGS_EXTF: |
114 |
|
case InferenceId::STRINGS_EXTF_N: |
115 |
|
case InferenceId::STRINGS_EXTF_D: |
116 |
|
case InferenceId::STRINGS_EXTF_D_N: |
117 |
|
case InferenceId::STRINGS_I_CONST_CONFLICT: |
118 |
|
case InferenceId::STRINGS_UNIT_CONST_CONFLICT: |
119 |
|
{ |
120 |
290 |
if (!ps.d_children.empty()) |
121 |
|
{ |
122 |
342 |
std::vector<Node> exps(ps.d_children.begin(), ps.d_children.end() - 1); |
123 |
342 |
Node src = ps.d_children[ps.d_children.size() - 1]; |
124 |
171 |
if (psb.applyPredTransform(src, conc, exps)) |
125 |
|
{ |
126 |
100 |
useBuffer = true; |
127 |
|
} |
128 |
|
} |
129 |
290 |
if (!useBuffer) |
130 |
|
{ |
131 |
|
// use the predicate version? |
132 |
190 |
ps.d_args.push_back(conc); |
133 |
190 |
ps.d_rule = PfRule::MACRO_SR_PRED_INTRO; |
134 |
|
} |
135 |
|
} |
136 |
290 |
break; |
137 |
|
// ========================== rewrite pred |
138 |
49 |
case InferenceId::STRINGS_EXTF_EQ_REW: |
139 |
|
{ |
140 |
|
// the last child is the predicate we are operating on, move to front |
141 |
67 |
Node src = ps.d_children[ps.d_children.size() - 1]; |
142 |
67 |
std::vector<Node> expe(ps.d_children.begin(), ps.d_children.end() - 1); |
143 |
|
// start with a default rewrite |
144 |
67 |
Node mainEqSRew = psb.applyPredElim(src, expe); |
145 |
49 |
if (mainEqSRew == conc) |
146 |
|
{ |
147 |
1 |
useBuffer = true; |
148 |
1 |
break; |
149 |
|
} |
150 |
|
// may need the "extended equality rewrite" |
151 |
|
Node mainEqSRew2 = psb.applyPredElim(mainEqSRew, |
152 |
|
{}, |
153 |
|
MethodId::SB_DEFAULT, |
154 |
|
MethodId::SBA_SEQUENTIAL, |
155 |
66 |
MethodId::RW_REWRITE_EQ_EXT); |
156 |
48 |
if (mainEqSRew2 == conc) |
157 |
|
{ |
158 |
30 |
useBuffer = true; |
159 |
30 |
break; |
160 |
|
} |
161 |
|
// rewrite again with default rewriter |
162 |
36 |
Node mainEqSRew3 = psb.applyPredElim(mainEqSRew2, {}); |
163 |
36 |
useBuffer = (mainEqSRew3 == conc); |
164 |
|
} |
165 |
18 |
break; |
166 |
|
// ========================== substitution+rewriting, CONCAT_EQ, ... |
167 |
824 |
case InferenceId::STRINGS_F_CONST: |
168 |
|
case InferenceId::STRINGS_F_UNIFY: |
169 |
|
case InferenceId::STRINGS_F_ENDPOINT_EMP: |
170 |
|
case InferenceId::STRINGS_F_ENDPOINT_EQ: |
171 |
|
case InferenceId::STRINGS_F_NCTN: |
172 |
|
case InferenceId::STRINGS_N_EQ_CONF: |
173 |
|
case InferenceId::STRINGS_N_CONST: |
174 |
|
case InferenceId::STRINGS_N_UNIFY: |
175 |
|
case InferenceId::STRINGS_N_ENDPOINT_EMP: |
176 |
|
case InferenceId::STRINGS_N_ENDPOINT_EQ: |
177 |
|
case InferenceId::STRINGS_N_NCTN: |
178 |
|
case InferenceId::STRINGS_SSPLIT_CST_PROP: |
179 |
|
case InferenceId::STRINGS_SSPLIT_VAR_PROP: |
180 |
|
case InferenceId::STRINGS_SSPLIT_CST: |
181 |
|
case InferenceId::STRINGS_SSPLIT_VAR: |
182 |
|
{ |
183 |
1648 |
Trace("strings-ipc-core") << "Generate core rule for " << infer |
184 |
824 |
<< " (rev=" << isRev << ")" << std::endl; |
185 |
|
// All of the above inferences have the form: |
186 |
|
// (explanation for why t and s have the same prefix/suffix) ^ |
187 |
|
// t = s ^ |
188 |
|
// (length constraint)? |
189 |
|
// We call t=s the "main equality" below. The length constraint is |
190 |
|
// optional, which we split on below. |
191 |
824 |
size_t nchild = ps.d_children.size(); |
192 |
824 |
size_t mainEqIndex = 0; |
193 |
824 |
bool mainEqIndexSet = false; |
194 |
|
// the length constraint |
195 |
1591 |
std::vector<Node> lenConstraint; |
196 |
|
// these inferences have a length constraint as the last explain |
197 |
824 |
if (infer == InferenceId::STRINGS_N_UNIFY || infer == InferenceId::STRINGS_F_UNIFY |
198 |
533 |
|| infer == InferenceId::STRINGS_SSPLIT_CST || infer == InferenceId::STRINGS_SSPLIT_VAR |
199 |
397 |
|| infer == InferenceId::STRINGS_SSPLIT_VAR_PROP |
200 |
358 |
|| infer == InferenceId::STRINGS_SSPLIT_CST_PROP) |
201 |
|
{ |
202 |
956 |
if (exp.size() >= 2) |
203 |
|
{ |
204 |
478 |
Assert(exp.size() <= startExpIndex.size()); |
205 |
|
// The index of the "main" equality is the last equality before |
206 |
|
// the length explanation. |
207 |
478 |
mainEqIndex = startExpIndex[exp.size() - 1] - 1; |
208 |
478 |
mainEqIndexSet = true; |
209 |
|
// the remainder is the length constraint |
210 |
1434 |
lenConstraint.insert(lenConstraint.end(), |
211 |
956 |
ps.d_children.begin() + mainEqIndex + 1, |
212 |
1912 |
ps.d_children.end()); |
213 |
|
} |
214 |
|
} |
215 |
346 |
else if (nchild >= 1) |
216 |
|
{ |
217 |
|
// The index of the main equality is the last child. |
218 |
346 |
mainEqIndex = nchild - 1; |
219 |
346 |
mainEqIndexSet = true; |
220 |
|
} |
221 |
1591 |
Node mainEq; |
222 |
824 |
if (mainEqIndexSet) |
223 |
|
{ |
224 |
824 |
mainEq = ps.d_children[mainEqIndex]; |
225 |
1648 |
Trace("strings-ipc-core") << "Main equality " << mainEq << " at index " |
226 |
824 |
<< mainEqIndex << std::endl; |
227 |
|
} |
228 |
824 |
if (mainEq.isNull() || mainEq.getKind() != EQUAL) |
229 |
|
{ |
230 |
|
Trace("strings-ipc-core") |
231 |
|
<< "...failed to find main equality" << std::endl; |
232 |
|
break; |
233 |
|
} |
234 |
|
// apply MACRO_SR_PRED_ELIM using equalities up to the main eq |
235 |
1591 |
std::vector<Node> childrenSRew; |
236 |
824 |
childrenSRew.push_back(mainEq); |
237 |
2472 |
childrenSRew.insert(childrenSRew.end(), |
238 |
|
ps.d_children.begin(), |
239 |
3296 |
ps.d_children.begin() + mainEqIndex); |
240 |
|
Node mainEqSRew = |
241 |
1591 |
psb.tryStep(PfRule::MACRO_SR_PRED_ELIM, childrenSRew, {}); |
242 |
824 |
if (CDProof::isSame(mainEqSRew, mainEq)) |
243 |
|
{ |
244 |
191 |
Trace("strings-ipc-core") << "...undo step" << std::endl; |
245 |
|
// the rule added above was not necessary |
246 |
191 |
psb.popStep(); |
247 |
|
} |
248 |
633 |
else if (mainEqSRew == conc) |
249 |
|
{ |
250 |
|
Trace("strings-ipc-core") << "...success after rewrite!" << std::endl; |
251 |
|
useBuffer = true; |
252 |
|
break; |
253 |
|
} |
254 |
1648 |
Trace("strings-ipc-core") |
255 |
824 |
<< "Main equality after subs+rewrite " << mainEqSRew << std::endl; |
256 |
|
// now, apply CONCAT_EQ to get the remainder |
257 |
1591 |
std::vector<Node> childrenCeq; |
258 |
824 |
childrenCeq.push_back(mainEqSRew); |
259 |
1591 |
std::vector<Node> argsCeq; |
260 |
824 |
argsCeq.push_back(nodeIsRev); |
261 |
1591 |
Node mainEqCeq = psb.tryStep(PfRule::CONCAT_EQ, childrenCeq, argsCeq); |
262 |
1648 |
Trace("strings-ipc-core") |
263 |
824 |
<< "Main equality after CONCAT_EQ " << mainEqCeq << std::endl; |
264 |
824 |
if (mainEqCeq.isNull() || mainEqCeq.getKind() != EQUAL) |
265 |
|
{ |
266 |
|
// fail |
267 |
|
break; |
268 |
|
} |
269 |
824 |
else if (mainEqCeq == mainEqSRew) |
270 |
|
{ |
271 |
340 |
Trace("strings-ipc-core") << "...undo step" << std::endl; |
272 |
|
// not necessary, probably first component of equality |
273 |
340 |
psb.popStep(); |
274 |
|
} |
275 |
|
// Now, mainEqCeq is an equality t ++ ... == s ++ ... where the |
276 |
|
// inference involved t and s. |
277 |
824 |
if (infer == InferenceId::STRINGS_N_ENDPOINT_EQ |
278 |
611 |
|| infer == InferenceId::STRINGS_N_ENDPOINT_EMP |
279 |
611 |
|| infer == InferenceId::STRINGS_F_ENDPOINT_EQ |
280 |
552 |
|| infer == InferenceId::STRINGS_F_ENDPOINT_EMP) |
281 |
|
{ |
282 |
|
// Should be equal to conclusion already, or rewrite to it. |
283 |
|
// Notice that this step is necessary to handle the "rproc" |
284 |
|
// optimization in processSimpleNEq. Alternatively, this could |
285 |
|
// possibly be done by CONCAT_EQ with !isRev. |
286 |
544 |
std::vector<Node> cexp; |
287 |
272 |
if (psb.applyPredTransform(mainEqCeq, |
288 |
|
conc, |
289 |
|
cexp, |
290 |
|
MethodId::SB_DEFAULT, |
291 |
|
MethodId::SBA_SEQUENTIAL, |
292 |
|
MethodId::RW_REWRITE_EQ_EXT)) |
293 |
|
{ |
294 |
540 |
Trace("strings-ipc-core") << "Transformed to " << conc |
295 |
270 |
<< " via pred transform" << std::endl; |
296 |
|
// success |
297 |
270 |
useBuffer = true; |
298 |
270 |
Trace("strings-ipc-core") << "...success!" << std::endl; |
299 |
272 |
} |
300 |
|
// Otherwise, note that EMP rules conclude ti = "" where |
301 |
|
// t1 ++ ... ++ tn == "". However, these are very rarely applied, let |
302 |
|
// alone for 2+ children. This case is intentionally unhandled here. |
303 |
|
} |
304 |
552 |
else if (infer == InferenceId::STRINGS_N_CONST || infer == InferenceId::STRINGS_F_CONST |
305 |
535 |
|| infer == InferenceId::STRINGS_N_EQ_CONF) |
306 |
|
{ |
307 |
|
// should be a constant conflict |
308 |
34 |
std::vector<Node> childrenC; |
309 |
17 |
childrenC.push_back(mainEqCeq); |
310 |
34 |
std::vector<Node> argsC; |
311 |
17 |
argsC.push_back(nodeIsRev); |
312 |
34 |
Node mainEqC = psb.tryStep(PfRule::CONCAT_CONFLICT, childrenC, argsC); |
313 |
17 |
if (mainEqC == conc) |
314 |
|
{ |
315 |
17 |
useBuffer = true; |
316 |
17 |
Trace("strings-ipc-core") << "...success!" << std::endl; |
317 |
17 |
} |
318 |
|
} |
319 |
|
else |
320 |
|
{ |
321 |
1013 |
std::vector<Node> tvec; |
322 |
1013 |
std::vector<Node> svec; |
323 |
535 |
utils::getConcat(mainEqCeq[0], tvec); |
324 |
535 |
utils::getConcat(mainEqCeq[1], svec); |
325 |
1013 |
Node t0 = tvec[isRev ? tvec.size() - 1 : 0]; |
326 |
1013 |
Node s0 = svec[isRev ? svec.size() - 1 : 0]; |
327 |
535 |
bool applySym = false; |
328 |
|
// may need to apply symmetry |
329 |
1070 |
if ((infer == InferenceId::STRINGS_SSPLIT_CST |
330 |
406 |
|| infer == InferenceId::STRINGS_SSPLIT_CST_PROP) |
331 |
676 |
&& t0.isConst()) |
332 |
|
{ |
333 |
79 |
Assert(!s0.isConst()); |
334 |
79 |
applySym = true; |
335 |
79 |
std::swap(t0, s0); |
336 |
|
} |
337 |
535 |
if (infer == InferenceId::STRINGS_N_UNIFY || infer == InferenceId::STRINGS_F_UNIFY) |
338 |
|
{ |
339 |
291 |
if (conc.getKind() != EQUAL) |
340 |
|
{ |
341 |
|
break; |
342 |
|
} |
343 |
|
// one side should match, the other side could be a split constant |
344 |
291 |
if (conc[0] != t0 && conc[1] != s0) |
345 |
|
{ |
346 |
144 |
applySym = true; |
347 |
144 |
std::swap(t0, s0); |
348 |
|
} |
349 |
291 |
Assert(conc[0].isConst() == t0.isConst()); |
350 |
291 |
Assert(conc[1].isConst() == s0.isConst()); |
351 |
|
} |
352 |
535 |
PfRule rule = PfRule::UNKNOWN; |
353 |
|
// the form of the required length constraint expected by the proof |
354 |
1013 |
Node lenReq; |
355 |
535 |
bool lenSuccess = false; |
356 |
535 |
if (infer == InferenceId::STRINGS_N_UNIFY || infer == InferenceId::STRINGS_F_UNIFY) |
357 |
|
{ |
358 |
|
// the required premise for unify is always len(x) = len(y), |
359 |
|
// however the explanation may not be literally this. Thus, we |
360 |
|
// need to reconstruct a proof from the given explanation. |
361 |
|
// it should be the case that lenConstraint => lenReq. |
362 |
|
// We use terms in the conclusion equality, not t0, s0 here. |
363 |
873 |
lenReq = nm->mkNode(STRING_LENGTH, conc[0]) |
364 |
582 |
.eqNode(nm->mkNode(STRING_LENGTH, conc[1])); |
365 |
291 |
lenSuccess = convertLengthPf(lenReq, lenConstraint, psb); |
366 |
291 |
rule = PfRule::CONCAT_UNIFY; |
367 |
|
} |
368 |
244 |
else if (infer == InferenceId::STRINGS_SSPLIT_VAR) |
369 |
|
{ |
370 |
|
// it should be the case that lenConstraint => lenReq |
371 |
21 |
lenReq = nm->mkNode(STRING_LENGTH, t0) |
372 |
14 |
.eqNode(nm->mkNode(STRING_LENGTH, s0)) |
373 |
14 |
.notNode(); |
374 |
7 |
lenSuccess = convertLengthPf(lenReq, lenConstraint, psb); |
375 |
7 |
rule = PfRule::CONCAT_SPLIT; |
376 |
|
} |
377 |
237 |
else if (infer == InferenceId::STRINGS_SSPLIT_CST) |
378 |
|
{ |
379 |
|
// it should be the case that lenConstraint => lenReq |
380 |
387 |
lenReq = nm->mkNode(STRING_LENGTH, t0) |
381 |
258 |
.eqNode(nm->mkConst(Rational(0))) |
382 |
258 |
.notNode(); |
383 |
129 |
lenSuccess = convertLengthPf(lenReq, lenConstraint, psb); |
384 |
129 |
rule = PfRule::CONCAT_CSPLIT; |
385 |
|
} |
386 |
108 |
else if (infer == InferenceId::STRINGS_SSPLIT_VAR_PROP) |
387 |
|
{ |
388 |
|
// it should be the case that lenConstraint => lenReq |
389 |
60 |
for (unsigned r = 0; r < 2; r++) |
390 |
|
{ |
391 |
180 |
lenReq = nm->mkNode(GT, |
392 |
120 |
nm->mkNode(STRING_LENGTH, t0), |
393 |
120 |
nm->mkNode(STRING_LENGTH, s0)); |
394 |
60 |
if (convertLengthPf(lenReq, lenConstraint, psb)) |
395 |
|
{ |
396 |
39 |
lenSuccess = true; |
397 |
39 |
break; |
398 |
|
} |
399 |
21 |
if (r == 0) |
400 |
|
{ |
401 |
|
// may be the other direction |
402 |
21 |
applySym = true; |
403 |
21 |
std::swap(t0, s0); |
404 |
|
} |
405 |
|
} |
406 |
39 |
rule = PfRule::CONCAT_LPROP; |
407 |
|
} |
408 |
69 |
else if (infer == InferenceId::STRINGS_SSPLIT_CST_PROP) |
409 |
|
{ |
410 |
|
// it should be the case that lenConstraint => lenReq |
411 |
36 |
lenReq = nm->mkNode(STRING_LENGTH, t0) |
412 |
24 |
.eqNode(nm->mkConst(Rational(0))) |
413 |
24 |
.notNode(); |
414 |
12 |
lenSuccess = convertLengthPf(lenReq, lenConstraint, psb); |
415 |
12 |
rule = PfRule::CONCAT_CPROP; |
416 |
|
} |
417 |
535 |
if (!lenSuccess) |
418 |
|
{ |
419 |
114 |
Trace("strings-ipc-core") |
420 |
57 |
<< "...failed due to length constraint" << std::endl; |
421 |
57 |
break; |
422 |
|
} |
423 |
|
// apply symmetry if necessary |
424 |
478 |
if (applySym) |
425 |
|
{ |
426 |
488 |
std::vector<Node> childrenSymm; |
427 |
244 |
childrenSymm.push_back(mainEqCeq); |
428 |
|
// note this explicit step may not be necessary |
429 |
244 |
mainEqCeq = psb.tryStep(PfRule::SYMM, childrenSymm, {}); |
430 |
488 |
Trace("strings-ipc-core") |
431 |
244 |
<< "Main equality after SYMM " << mainEqCeq << std::endl; |
432 |
|
} |
433 |
478 |
if (rule != PfRule::UNKNOWN) |
434 |
|
{ |
435 |
956 |
Trace("strings-ipc-core") |
436 |
478 |
<< "Core rule length requirement is " << lenReq << std::endl; |
437 |
|
// apply the given rule |
438 |
956 |
std::vector<Node> childrenMain; |
439 |
478 |
childrenMain.push_back(mainEqCeq); |
440 |
478 |
childrenMain.push_back(lenReq); |
441 |
956 |
std::vector<Node> argsMain; |
442 |
478 |
argsMain.push_back(nodeIsRev); |
443 |
956 |
Node mainEqMain = psb.tryStep(rule, childrenMain, argsMain); |
444 |
956 |
Trace("strings-ipc-core") << "Main equality after " << rule << " " |
445 |
478 |
<< mainEqMain << std::endl; |
446 |
478 |
if (mainEqMain == mainEqCeq) |
447 |
|
{ |
448 |
3 |
Trace("strings-ipc-core") << "...undo step" << std::endl; |
449 |
|
// not necessary, probably first component of equality |
450 |
3 |
psb.popStep(); |
451 |
|
} |
452 |
|
// either equal or rewrites to it |
453 |
956 |
std::vector<Node> cexp; |
454 |
478 |
if (psb.applyPredTransform(mainEqMain, conc, cexp)) |
455 |
|
{ |
456 |
|
// requires that length success is also true |
457 |
477 |
useBuffer = true; |
458 |
477 |
Trace("strings-ipc-core") << "...success" << std::endl; |
459 |
|
} |
460 |
|
else |
461 |
|
{ |
462 |
1 |
Trace("strings-ipc-core") << "...fail" << std::endl; |
463 |
|
} |
464 |
|
} |
465 |
|
else |
466 |
|
{ |
467 |
|
// should always have given a rule to try above |
468 |
|
Assert(false) << "No reconstruction rule given for " << infer; |
469 |
|
} |
470 |
767 |
} |
471 |
|
} |
472 |
767 |
break; |
473 |
|
// ========================== Disequalities |
474 |
6 |
case InferenceId::STRINGS_DEQ_DISL_FIRST_CHAR_STRING_SPLIT: |
475 |
|
case InferenceId::STRINGS_DEQ_DISL_STRINGS_SPLIT: |
476 |
|
{ |
477 |
18 |
if (conc.getKind() != AND || conc.getNumChildren() != 2 |
478 |
12 |
|| conc[0].getKind() != EQUAL || !conc[0][0].getType().isStringLike() |
479 |
12 |
|| conc[1].getKind() != EQUAL |
480 |
18 |
|| conc[1][0].getKind() != STRING_LENGTH) |
481 |
|
{ |
482 |
|
Trace("strings-ipc-deq") << "malformed application" << std::endl; |
483 |
|
Assert(false) << "unexpected conclusion " << conc << " for " << infer; |
484 |
|
} |
485 |
|
else |
486 |
|
{ |
487 |
|
Node lenReq = |
488 |
12 |
nm->mkNode(GEQ, nm->mkNode(STRING_LENGTH, conc[0][0]), conc[1][1]); |
489 |
12 |
Trace("strings-ipc-deq") |
490 |
6 |
<< "length requirement is " << lenReq << std::endl; |
491 |
6 |
if (convertLengthPf(lenReq, ps.d_children, psb)) |
492 |
|
{ |
493 |
2 |
Trace("strings-ipc-deq") << "...success length" << std::endl; |
494 |
|
// make the proof |
495 |
4 |
std::vector<Node> childrenMain; |
496 |
2 |
childrenMain.push_back(lenReq); |
497 |
4 |
std::vector<Node> argsMain; |
498 |
2 |
argsMain.push_back(nodeIsRev); |
499 |
|
Node mainConc = |
500 |
4 |
psb.tryStep(PfRule::STRING_DECOMPOSE, childrenMain, argsMain); |
501 |
4 |
Trace("strings-ipc-deq") |
502 |
2 |
<< "...main conclusion is " << mainConc << std::endl; |
503 |
2 |
useBuffer = (mainConc == conc); |
504 |
4 |
Trace("strings-ipc-deq") |
505 |
2 |
<< "...success is " << useBuffer << std::endl; |
506 |
|
} |
507 |
|
else |
508 |
|
{ |
509 |
4 |
Trace("strings-ipc-deq") << "...fail length" << std::endl; |
510 |
|
} |
511 |
|
} |
512 |
|
} |
513 |
6 |
break; |
514 |
|
// ========================== Boolean split |
515 |
145 |
case InferenceId::STRINGS_CARD_SP: |
516 |
|
case InferenceId::STRINGS_LEN_SPLIT: |
517 |
|
case InferenceId::STRINGS_LEN_SPLIT_EMP: |
518 |
|
case InferenceId::STRINGS_DEQ_DISL_EMP_SPLIT: |
519 |
|
case InferenceId::STRINGS_DEQ_DISL_FIRST_CHAR_EQ_SPLIT: |
520 |
|
case InferenceId::STRINGS_DEQ_STRINGS_EQ: |
521 |
|
case InferenceId::STRINGS_DEQ_LENS_EQ: |
522 |
|
case InferenceId::STRINGS_DEQ_LENGTH_SP: |
523 |
|
{ |
524 |
145 |
if (conc.getKind() != OR) |
525 |
|
{ |
526 |
|
// This should never happen. If it does, we resort to using |
527 |
|
// STRING_TRUST below (in production mode). |
528 |
|
Assert(false) << "Expected OR conclusion for " << infer; |
529 |
|
} |
530 |
|
else |
531 |
|
{ |
532 |
145 |
ps.d_rule = PfRule::SPLIT; |
533 |
145 |
Assert(ps.d_children.empty()); |
534 |
145 |
ps.d_args.push_back(conc[0]); |
535 |
|
} |
536 |
|
} |
537 |
145 |
break; |
538 |
|
// ========================== Regular expression unfolding |
539 |
52 |
case InferenceId::STRINGS_RE_UNFOLD_POS: |
540 |
|
case InferenceId::STRINGS_RE_UNFOLD_NEG: |
541 |
|
{ |
542 |
52 |
Assert (!ps.d_children.empty()); |
543 |
52 |
size_t nchild = ps.d_children.size(); |
544 |
104 |
Node mem = ps.d_children[nchild-1]; |
545 |
52 |
if (nchild>1) |
546 |
|
{ |
547 |
|
// if more than one, apply MACRO_SR_PRED_ELIM |
548 |
|
std::vector<Node> tcs; |
549 |
|
tcs.insert(tcs.end(), |
550 |
|
ps.d_children.begin(), |
551 |
|
ps.d_children.begin() + (nchild-1)); |
552 |
|
mem = psb.applyPredElim(mem, tcs); |
553 |
|
useBuffer = true; |
554 |
|
} |
555 |
52 |
PfRule r = PfRule::UNKNOWN; |
556 |
52 |
if (mem.isNull()) |
557 |
|
{ |
558 |
|
// failed to eliminate above |
559 |
|
Assert(false) << "Failed to apply MACRO_SR_PRED_ELIM for RE unfold"; |
560 |
|
useBuffer = false; |
561 |
|
} |
562 |
52 |
else if (infer == InferenceId::STRINGS_RE_UNFOLD_POS) |
563 |
|
{ |
564 |
39 |
r = PfRule::RE_UNFOLD_POS; |
565 |
|
} |
566 |
|
else |
567 |
|
{ |
568 |
13 |
r = PfRule::RE_UNFOLD_NEG; |
569 |
|
// it may be an optimized form of concat simplification |
570 |
13 |
Assert(mem.getKind() == NOT && mem[0].getKind() == STRING_IN_REGEXP); |
571 |
13 |
if (mem[0][1].getKind() == REGEXP_CONCAT) |
572 |
|
{ |
573 |
|
size_t index; |
574 |
22 |
Node reLen = RegExpOpr::getRegExpConcatFixed(mem[0][1], index); |
575 |
|
// if we can find a fixed length for a component, use the optimized |
576 |
|
// version |
577 |
11 |
if (!reLen.isNull()) |
578 |
|
{ |
579 |
9 |
r = PfRule::RE_UNFOLD_NEG_CONCAT_FIXED; |
580 |
|
} |
581 |
|
} |
582 |
|
} |
583 |
52 |
if (useBuffer) |
584 |
|
{ |
585 |
|
mem = psb.tryStep(r, {mem}, {}); |
586 |
|
// should match the conclusion |
587 |
|
useBuffer = (mem==conc); |
588 |
|
} |
589 |
|
else |
590 |
|
{ |
591 |
52 |
ps.d_rule = r; |
592 |
52 |
} |
593 |
|
} |
594 |
52 |
break; |
595 |
|
// ========================== Reduction |
596 |
457 |
case InferenceId::STRINGS_CTN_POS: |
597 |
|
case InferenceId::STRINGS_CTN_NEG_EQUAL: |
598 |
|
{ |
599 |
457 |
if (ps.d_children.size() != 1) |
600 |
|
{ |
601 |
2 |
break; |
602 |
|
} |
603 |
456 |
bool polarity = ps.d_children[0].getKind() != NOT; |
604 |
912 |
Node atom = polarity ? ps.d_children[0] : ps.d_children[0][0]; |
605 |
912 |
std::vector<Node> args; |
606 |
456 |
args.push_back(atom); |
607 |
912 |
Node res = psb.tryStep(PfRule::STRING_EAGER_REDUCTION, {}, args); |
608 |
456 |
if (res.isNull()) |
609 |
|
{ |
610 |
|
break; |
611 |
|
} |
612 |
|
// ite( contains(x,t), x = k1 ++ t ++ k2, x != t ) |
613 |
912 |
std::vector<Node> tiChildren; |
614 |
456 |
tiChildren.push_back(ps.d_children[0]); |
615 |
|
Node ctnt = psb.tryStep( |
616 |
912 |
polarity ? PfRule::TRUE_INTRO : PfRule::FALSE_INTRO, tiChildren, {}); |
617 |
456 |
if (ctnt.isNull() || ctnt.getKind() != EQUAL) |
618 |
|
{ |
619 |
|
break; |
620 |
|
} |
621 |
912 |
std::vector<Node> tchildren; |
622 |
456 |
tchildren.push_back(ctnt); |
623 |
|
// apply substitution { contains(x,t) -> true|false } and rewrite to get |
624 |
|
// conclusion x = k1 ++ t ++ k2 or x != t. |
625 |
456 |
if (psb.applyPredTransform(res, conc, tchildren)) |
626 |
|
{ |
627 |
456 |
useBuffer = true; |
628 |
457 |
} |
629 |
|
} |
630 |
456 |
break; |
631 |
|
|
632 |
215 |
case InferenceId::STRINGS_REDUCTION: |
633 |
|
{ |
634 |
215 |
size_t nchild = conc.getNumChildren(); |
635 |
430 |
Node mainEq; |
636 |
215 |
if (conc.getKind() == EQUAL) |
637 |
|
{ |
638 |
4 |
mainEq = conc; |
639 |
|
} |
640 |
211 |
else if (conc.getKind() == AND && conc[nchild - 1].getKind() == EQUAL) |
641 |
|
{ |
642 |
211 |
mainEq = conc[nchild - 1]; |
643 |
|
} |
644 |
215 |
if (mainEq.isNull()) |
645 |
|
{ |
646 |
|
Trace("strings-ipc-red") << "Bad Reduction: " << conc << std::endl; |
647 |
|
Assert(false) << "Unexpected reduction " << conc; |
648 |
|
break; |
649 |
|
} |
650 |
430 |
std::vector<Node> argsRed; |
651 |
|
// the left hand side of the last conjunct is the term we are reducing |
652 |
215 |
argsRed.push_back(mainEq[0]); |
653 |
430 |
Node red = psb.tryStep(PfRule::STRING_REDUCTION, {}, argsRed); |
654 |
215 |
Trace("strings-ipc-red") << "Reduction : " << red << std::endl; |
655 |
215 |
if (!red.isNull()) |
656 |
|
{ |
657 |
|
// either equal or rewrites to it |
658 |
430 |
std::vector<Node> cexp; |
659 |
215 |
if (psb.applyPredTransform(red, conc, cexp)) |
660 |
|
{ |
661 |
203 |
Trace("strings-ipc-red") << "...success!" << std::endl; |
662 |
203 |
useBuffer = true; |
663 |
|
} |
664 |
|
else |
665 |
|
{ |
666 |
12 |
Trace("strings-ipc-red") << "...failed to reduce" << std::endl; |
667 |
|
} |
668 |
215 |
} |
669 |
|
} |
670 |
215 |
break; |
671 |
|
// ========================== code injectivity |
672 |
53 |
case InferenceId::STRINGS_CODE_INJ: |
673 |
|
{ |
674 |
53 |
ps.d_rule = PfRule::STRING_CODE_INJ; |
675 |
53 |
Assert(conc.getKind() == OR && conc.getNumChildren() == 3 |
676 |
|
&& conc[2].getKind() == EQUAL); |
677 |
53 |
ps.d_args.push_back(conc[2][0]); |
678 |
53 |
ps.d_args.push_back(conc[2][1]); |
679 |
|
} |
680 |
53 |
break; |
681 |
|
// ========================== unit injectivity |
682 |
8 |
case InferenceId::STRINGS_UNIT_INJ: |
683 |
|
{ |
684 |
8 |
ps.d_rule = PfRule::STRING_SEQ_UNIT_INJ; |
685 |
|
} |
686 |
8 |
break; |
687 |
|
// ========================== prefix conflict |
688 |
39 |
case InferenceId::STRINGS_PREFIX_CONFLICT: |
689 |
|
{ |
690 |
39 |
Trace("strings-ipc-prefix") << "Prefix conflict..." << std::endl; |
691 |
78 |
std::vector<Node> eqs; |
692 |
94 |
for (const Node& e : ps.d_children) |
693 |
|
{ |
694 |
55 |
Kind ek = e.getKind(); |
695 |
55 |
if (ek == EQUAL) |
696 |
|
{ |
697 |
39 |
Trace("strings-ipc-prefix") << "- equality : " << e << std::endl; |
698 |
39 |
eqs.push_back(e); |
699 |
|
} |
700 |
16 |
else if (ek == STRING_IN_REGEXP) |
701 |
|
{ |
702 |
|
// unfold it and extract the equality |
703 |
32 |
std::vector<Node> children; |
704 |
16 |
children.push_back(e); |
705 |
32 |
std::vector<Node> args; |
706 |
32 |
Node eunf = psb.tryStep(PfRule::RE_UNFOLD_POS, children, args); |
707 |
32 |
Trace("strings-ipc-prefix") |
708 |
16 |
<< "--- " << e << " unfolds to " << eunf << std::endl; |
709 |
16 |
if (eunf.isNull()) |
710 |
|
{ |
711 |
|
continue; |
712 |
|
} |
713 |
16 |
else if (eunf.getKind() == AND) |
714 |
|
{ |
715 |
|
// equality is the first conjunct |
716 |
32 |
std::vector<Node> childrenAE; |
717 |
16 |
childrenAE.push_back(eunf); |
718 |
32 |
std::vector<Node> argsAE; |
719 |
16 |
argsAE.push_back(nm->mkConst(Rational(0))); |
720 |
32 |
Node eunfAE = psb.tryStep(PfRule::AND_ELIM, childrenAE, argsAE); |
721 |
32 |
Trace("strings-ipc-prefix") |
722 |
16 |
<< "--- and elim to " << eunfAE << std::endl; |
723 |
16 |
if (eunfAE.isNull() || eunfAE.getKind() != EQUAL) |
724 |
|
{ |
725 |
|
Assert(false) |
726 |
|
<< "Unexpected unfolded premise " << eunf << " for " << infer; |
727 |
|
continue; |
728 |
|
} |
729 |
32 |
Trace("strings-ipc-prefix") |
730 |
16 |
<< "- equality : " << eunfAE << std::endl; |
731 |
16 |
eqs.push_back(eunfAE); |
732 |
|
} |
733 |
|
else if (eunf.getKind() == EQUAL) |
734 |
|
{ |
735 |
|
Trace("strings-ipc-prefix") << "- equality : " << eunf << std::endl; |
736 |
|
eqs.push_back(eunf); |
737 |
|
} |
738 |
|
} |
739 |
|
else |
740 |
|
{ |
741 |
|
// not sure how to use this assumption |
742 |
|
Assert(false) << "Unexpected premise " << e << " for " << infer; |
743 |
|
} |
744 |
|
} |
745 |
39 |
if (eqs.empty()) |
746 |
|
{ |
747 |
|
break; |
748 |
|
} |
749 |
|
// connect via transitivity |
750 |
78 |
Node curr = eqs[0]; |
751 |
55 |
for (size_t i = 1, esize = eqs.size(); i < esize; i++) |
752 |
|
{ |
753 |
32 |
Node prev = curr; |
754 |
16 |
curr = convertTrans(curr, eqs[1], psb); |
755 |
16 |
if (curr.isNull()) |
756 |
|
{ |
757 |
|
break; |
758 |
|
} |
759 |
16 |
Trace("strings-ipc-prefix") << "- Via trans: " << curr << std::endl; |
760 |
|
} |
761 |
39 |
if (curr.isNull()) |
762 |
|
{ |
763 |
|
break; |
764 |
|
} |
765 |
78 |
Trace("strings-ipc-prefix") |
766 |
39 |
<< "- Possible conflicting equality : " << curr << std::endl; |
767 |
78 |
std::vector<Node> emp; |
768 |
78 |
Node concE = psb.applyPredElim(curr, emp); |
769 |
78 |
Trace("strings-ipc-prefix") |
770 |
39 |
<< "- After pred elim: " << concE << std::endl; |
771 |
39 |
if (concE == conc) |
772 |
|
{ |
773 |
|
Trace("strings-ipc-prefix") << "...success!" << std::endl; |
774 |
|
useBuffer = true; |
775 |
39 |
} |
776 |
|
} |
777 |
39 |
break; |
778 |
|
// ========================== regular expressions |
779 |
7 |
case InferenceId::STRINGS_RE_INTER_INCLUDE: |
780 |
|
case InferenceId::STRINGS_RE_INTER_CONF: |
781 |
|
case InferenceId::STRINGS_RE_INTER_INFER: |
782 |
|
{ |
783 |
14 |
std::vector<Node> reiExp; |
784 |
14 |
std::vector<Node> reis; |
785 |
14 |
std::vector<Node> reiChildren; |
786 |
14 |
std::vector<Node> reiChildrenOrig; |
787 |
14 |
Node x; |
788 |
|
// make the regular expression intersection that summarizes all |
789 |
|
// memberships in the explanation |
790 |
23 |
for (const Node& c : ps.d_children) |
791 |
|
{ |
792 |
16 |
bool polarity = c.getKind() != NOT; |
793 |
30 |
Node catom = polarity ? c : c[0]; |
794 |
18 |
if (catom.getKind() != STRING_IN_REGEXP) |
795 |
|
{ |
796 |
2 |
Assert(c.getKind() == EQUAL); |
797 |
2 |
if (c.getKind() == EQUAL) |
798 |
|
{ |
799 |
2 |
reiExp.push_back(c); |
800 |
|
} |
801 |
2 |
continue; |
802 |
|
} |
803 |
14 |
if (x.isNull()) |
804 |
|
{ |
805 |
|
// just take the first LHS; others should be equated to it by exp |
806 |
7 |
x = catom[0]; |
807 |
|
} |
808 |
|
Node rcurr = |
809 |
28 |
polarity ? catom[1] : nm->mkNode(REGEXP_COMPLEMENT, catom[1]); |
810 |
14 |
reis.push_back(rcurr); |
811 |
28 |
Node mem = nm->mkNode(STRING_IN_REGEXP, catom[0], rcurr); |
812 |
14 |
reiChildren.push_back(mem); |
813 |
14 |
reiChildrenOrig.push_back(c); |
814 |
|
} |
815 |
|
// go back and justify each premise |
816 |
7 |
bool successChildren = true; |
817 |
21 |
for (size_t i = 0, nchild = reiChildren.size(); i < nchild; i++) |
818 |
|
{ |
819 |
14 |
if (!psb.applyPredTransform(reiChildrenOrig[i], reiChildren[i], reiExp)) |
820 |
|
{ |
821 |
|
Trace("strings-ipc-re") |
822 |
|
<< "... failed to justify child " << reiChildren[i] << " from " |
823 |
|
<< reiChildrenOrig[i] << std::endl; |
824 |
|
successChildren = false; |
825 |
|
break; |
826 |
|
} |
827 |
|
} |
828 |
7 |
if (!successChildren) |
829 |
|
{ |
830 |
|
break; |
831 |
|
} |
832 |
14 |
Node mem = psb.tryStep(PfRule::RE_INTER, reiChildren, {}); |
833 |
14 |
Trace("strings-ipc-re") |
834 |
7 |
<< "Regular expression summary: " << mem << std::endl; |
835 |
|
// the conclusion is rewritable to the premises via rewriting? |
836 |
7 |
if (psb.applyPredTransform(mem, conc, {})) |
837 |
|
{ |
838 |
2 |
Trace("strings-ipc-re") << "... success!" << std::endl; |
839 |
2 |
useBuffer = true; |
840 |
|
} |
841 |
|
else |
842 |
|
{ |
843 |
10 |
Trace("strings-ipc-re") |
844 |
5 |
<< "...failed to rewrite to conclusion" << std::endl; |
845 |
7 |
} |
846 |
|
} |
847 |
7 |
break; |
848 |
|
// ========================== unknown and currently unsupported |
849 |
4 |
case InferenceId::STRINGS_CARDINALITY: |
850 |
|
case InferenceId::STRINGS_I_CYCLE_E: |
851 |
|
case InferenceId::STRINGS_I_CYCLE: |
852 |
|
case InferenceId::STRINGS_INFER_EMP: |
853 |
|
case InferenceId::STRINGS_RE_DELTA: |
854 |
|
case InferenceId::STRINGS_RE_DELTA_CONF: |
855 |
|
case InferenceId::STRINGS_RE_DERIVE: |
856 |
|
case InferenceId::STRINGS_FLOOP: |
857 |
|
case InferenceId::STRINGS_FLOOP_CONFLICT: |
858 |
|
case InferenceId::STRINGS_DEQ_NORM_EMP: |
859 |
|
case InferenceId::STRINGS_CTN_TRANS: |
860 |
|
case InferenceId::STRINGS_CTN_DECOMPOSE: |
861 |
|
default: |
862 |
|
// do nothing, these will be converted to STRING_TRUST below since the |
863 |
|
// rule is unknown. |
864 |
4 |
break; |
865 |
|
} |
866 |
|
|
867 |
|
// now see if we would succeed with the checker-to-try |
868 |
2879 |
bool success = false; |
869 |
2879 |
if (ps.d_rule != PfRule::UNKNOWN) |
870 |
|
{ |
871 |
2356 |
Trace("strings-ipc") << "For " << infer << ", try proof rule " << ps.d_rule |
872 |
1178 |
<< "..."; |
873 |
1178 |
Assert(ps.d_rule != PfRule::UNKNOWN); |
874 |
2356 |
Node pconc = psb.tryStep(ps.d_rule, ps.d_children, ps.d_args); |
875 |
1178 |
if (pconc.isNull() || pconc != conc) |
876 |
|
{ |
877 |
50 |
Trace("strings-ipc") << "failed, pconc is " << pconc << " (expected " |
878 |
25 |
<< conc << ")" << std::endl; |
879 |
25 |
ps.d_rule = PfRule::UNKNOWN; |
880 |
|
} |
881 |
|
else |
882 |
|
{ |
883 |
|
// successfully set up a single step proof in ps |
884 |
1153 |
success = true; |
885 |
1153 |
Trace("strings-ipc") << "success!" << std::endl; |
886 |
|
} |
887 |
|
} |
888 |
1701 |
else if (useBuffer) |
889 |
|
{ |
890 |
|
// successfully set up a multi step proof in psb |
891 |
1566 |
success = true; |
892 |
|
} |
893 |
|
else |
894 |
|
{ |
895 |
270 |
Trace("strings-ipc") << "For " << infer << " " << conc |
896 |
135 |
<< ", no proof rule, failed" << std::endl; |
897 |
|
} |
898 |
2879 |
if (!success) |
899 |
|
{ |
900 |
|
// debug print |
901 |
160 |
if (Trace.isOn("strings-ipc-fail")) |
902 |
|
{ |
903 |
|
Trace("strings-ipc-fail") |
904 |
|
<< "InferProofCons::convert: Failed " << infer |
905 |
|
<< (isRev ? " :rev " : " ") << conc << std::endl; |
906 |
|
for (const Node& ec : exp) |
907 |
|
{ |
908 |
|
Trace("strings-ipc-fail") << " e: " << ec << std::endl; |
909 |
|
} |
910 |
|
} |
911 |
|
// untrustworthy conversion, the argument of STRING_TRUST is its conclusion |
912 |
160 |
ps.d_args.clear(); |
913 |
160 |
ps.d_args.push_back(conc); |
914 |
|
// use the trust rule |
915 |
160 |
ps.d_rule = PfRule::STRING_TRUST; |
916 |
|
// add to stats |
917 |
160 |
d_statistics.d_inferencesNoPf << infer; |
918 |
|
} |
919 |
2879 |
if (Trace.isOn("strings-ipc-debug")) |
920 |
|
{ |
921 |
|
if (useBuffer) |
922 |
|
{ |
923 |
|
Trace("strings-ipc-debug") |
924 |
|
<< "InferProofCons::convert returned buffer with " |
925 |
|
<< psb.getNumSteps() << " steps:" << std::endl; |
926 |
|
const std::vector<std::pair<Node, ProofStep>>& steps = psb.getSteps(); |
927 |
|
for (const std::pair<Node, ProofStep>& step : steps) |
928 |
|
{ |
929 |
|
Trace("strings-ipc-debug") |
930 |
|
<< "- " << step.first << " via " << step.second << std::endl; |
931 |
|
} |
932 |
|
} |
933 |
|
else |
934 |
|
{ |
935 |
|
Trace("strings-ipc-debug") |
936 |
|
<< "InferProofCons::convert returned " << ps << std::endl; |
937 |
|
} |
938 |
|
} |
939 |
2879 |
} |
940 |
|
|
941 |
505 |
bool InferProofCons::convertLengthPf(Node lenReq, |
942 |
|
const std::vector<Node>& lenExp, |
943 |
|
TheoryProofStepBuffer& psb) |
944 |
|
{ |
945 |
865 |
for (const Node& le : lenExp) |
946 |
|
{ |
947 |
637 |
if (lenReq == le) |
948 |
|
{ |
949 |
277 |
return true; |
950 |
|
} |
951 |
|
} |
952 |
456 |
Trace("strings-ipc-len") << "Must explain " << lenReq << " by " << lenExp |
953 |
228 |
<< std::endl; |
954 |
295 |
for (const Node& le : lenExp) |
955 |
|
{ |
956 |
|
// probably rewrites to it? |
957 |
337 |
std::vector<Node> exp; |
958 |
270 |
if (psb.applyPredTransform(le, lenReq, exp)) |
959 |
|
{ |
960 |
118 |
Trace("strings-ipc-len") << "...success by rewrite" << std::endl; |
961 |
118 |
return true; |
962 |
|
} |
963 |
|
// maybe x != "" => len(x) != 0 |
964 |
219 |
std::vector<Node> children; |
965 |
152 |
children.push_back(le); |
966 |
219 |
std::vector<Node> args; |
967 |
219 |
Node res = psb.tryStep(PfRule::STRING_LENGTH_NON_EMPTY, children, args); |
968 |
152 |
if (res == lenReq) |
969 |
|
{ |
970 |
85 |
Trace("strings-ipc-len") << "...success by LENGTH_NON_EMPTY" << std::endl; |
971 |
85 |
return true; |
972 |
|
} |
973 |
|
} |
974 |
25 |
Trace("strings-ipc-len") << "...failed" << std::endl; |
975 |
25 |
return false; |
976 |
|
} |
977 |
|
|
978 |
16 |
Node InferProofCons::convertTrans(Node eqa, |
979 |
|
Node eqb, |
980 |
|
TheoryProofStepBuffer& psb) |
981 |
|
{ |
982 |
16 |
if (eqa.getKind() != EQUAL || eqb.getKind() != EQUAL) |
983 |
|
{ |
984 |
|
return Node::null(); |
985 |
|
} |
986 |
16 |
for (uint32_t i = 0; i < 2; i++) |
987 |
|
{ |
988 |
16 |
Node eqaSym = i == 0 ? eqa[1].eqNode(eqa[0]) : eqa; |
989 |
18 |
for (uint32_t j = 0; j < 2; j++) |
990 |
|
{ |
991 |
20 |
Node eqbSym = j == 0 ? eqb : eqb[1].eqNode(eqb[1]); |
992 |
18 |
if (eqa[i] == eqb[j]) |
993 |
|
{ |
994 |
32 |
std::vector<Node> children; |
995 |
16 |
children.push_back(eqaSym); |
996 |
16 |
children.push_back(eqbSym); |
997 |
16 |
return psb.tryStep(PfRule::TRANS, children, {}); |
998 |
|
} |
999 |
|
} |
1000 |
|
} |
1001 |
|
return Node::null(); |
1002 |
|
} |
1003 |
|
|
1004 |
2879 |
std::shared_ptr<ProofNode> InferProofCons::getProofFor(Node fact) |
1005 |
|
{ |
1006 |
|
// temporary proof |
1007 |
5758 |
CDProof pf(d_pnm); |
1008 |
|
// get the inference |
1009 |
2879 |
NodeInferInfoMap::iterator it = d_lazyFactMap.find(fact); |
1010 |
2879 |
if (it == d_lazyFactMap.end()) |
1011 |
|
{ |
1012 |
|
Node factSym = CDProof::getSymmFact(fact); |
1013 |
|
if (!factSym.isNull()) |
1014 |
|
{ |
1015 |
|
// Use the symmetric fact. There is no need to explictly make a |
1016 |
|
// SYMM proof, as this is handled by CDProof::getProofFor below. |
1017 |
|
it = d_lazyFactMap.find(factSym); |
1018 |
|
} |
1019 |
|
} |
1020 |
2879 |
AlwaysAssert(it != d_lazyFactMap.end()); |
1021 |
|
// now go back and convert it to proof steps and add to proof |
1022 |
2879 |
bool useBuffer = false; |
1023 |
5758 |
ProofStep ps; |
1024 |
5758 |
TheoryProofStepBuffer psb(d_pnm->getChecker()); |
1025 |
5758 |
std::shared_ptr<InferInfo> ii = (*it).second; |
1026 |
|
// run the conversion |
1027 |
2879 |
convert(ii->getId(), ii->d_idRev, ii->d_conc, ii->d_premises, ps, psb, useBuffer); |
1028 |
|
// make the proof based on the step or the buffer |
1029 |
2879 |
if (useBuffer) |
1030 |
|
{ |
1031 |
1566 |
if (!pf.addSteps(psb)) |
1032 |
|
{ |
1033 |
|
return nullptr; |
1034 |
|
} |
1035 |
|
} |
1036 |
|
else |
1037 |
|
{ |
1038 |
1313 |
if (!pf.addStep(fact, ps)) |
1039 |
|
{ |
1040 |
|
return nullptr; |
1041 |
|
} |
1042 |
|
} |
1043 |
2879 |
return pf.getProofFor(fact); |
1044 |
|
} |
1045 |
|
|
1046 |
7810 |
std::string InferProofCons::identify() const |
1047 |
|
{ |
1048 |
7810 |
return "strings::InferProofCons"; |
1049 |
|
} |
1050 |
|
|
1051 |
|
} // namespace strings |
1052 |
|
} // namespace theory |
1053 |
29340 |
} // namespace cvc5 |