1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Andrew Reynolds, Dejan Jovanovic, Morgan Deters |
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 theory preprocessor. |
14 |
|
*/ |
15 |
|
|
16 |
|
#include "theory/theory_preprocessor.h" |
17 |
|
|
18 |
|
#include "expr/skolem_manager.h" |
19 |
|
#include "proof/lazy_proof.h" |
20 |
|
#include "smt/logic_exception.h" |
21 |
|
#include "theory/logic_info.h" |
22 |
|
#include "theory/rewriter.h" |
23 |
|
#include "theory/theory_engine.h" |
24 |
|
|
25 |
|
using namespace std; |
26 |
|
|
27 |
|
namespace cvc5 { |
28 |
|
namespace theory { |
29 |
|
|
30 |
15338 |
TheoryPreprocessor::TheoryPreprocessor(Env& env, TheoryEngine& engine) |
31 |
|
: EnvObj(env), |
32 |
|
d_engine(engine), |
33 |
15338 |
d_ppCache(userContext()), |
34 |
15338 |
d_rtfCache(userContext()), |
35 |
|
d_tfr(env), |
36 |
|
d_tpg(nullptr), |
37 |
|
d_tpgRtf(nullptr), |
38 |
|
d_tpgRew(nullptr), |
39 |
|
d_tspg(nullptr), |
40 |
46014 |
d_lp(nullptr) |
41 |
|
{ |
42 |
|
// proofs are enabled in the theory preprocessor regardless of the proof mode |
43 |
15338 |
ProofNodeManager* pnm = env.getProofNodeManager(); |
44 |
15338 |
if (pnm != nullptr) |
45 |
|
{ |
46 |
8003 |
context::Context* u = userContext(); |
47 |
16006 |
d_tpg.reset( |
48 |
|
new TConvProofGenerator(pnm, |
49 |
|
u, |
50 |
|
TConvPolicy::FIXPOINT, |
51 |
|
TConvCachePolicy::NEVER, |
52 |
|
"TheoryPreprocessor::preprocess_rewrite", |
53 |
8003 |
&d_iqtc)); |
54 |
16006 |
d_tpgRtf.reset(new TConvProofGenerator(pnm, |
55 |
|
u, |
56 |
|
TConvPolicy::FIXPOINT, |
57 |
|
TConvCachePolicy::NEVER, |
58 |
|
"TheoryPreprocessor::rtf", |
59 |
8003 |
&d_iqtc)); |
60 |
16006 |
d_tpgRew.reset(new TConvProofGenerator(pnm, |
61 |
|
u, |
62 |
|
TConvPolicy::ONCE, |
63 |
|
TConvCachePolicy::NEVER, |
64 |
8003 |
"TheoryPreprocessor::pprew")); |
65 |
16006 |
d_lp.reset( |
66 |
8003 |
new LazyCDProof(pnm, nullptr, u, "TheoryPreprocessor::LazyCDProof")); |
67 |
|
// Make the main term conversion sequence generator, which tracks up to |
68 |
|
// three conversions made in succession: |
69 |
|
// (1) rewriting |
70 |
|
// (2) (theory preprocessing+rewriting until fixed point)+term formula |
71 |
|
// removal+rewriting. |
72 |
16006 |
std::vector<ProofGenerator*> ts; |
73 |
8003 |
ts.push_back(d_tpgRew.get()); |
74 |
8003 |
ts.push_back(d_tpgRtf.get()); |
75 |
24009 |
d_tspg.reset(new TConvSeqProofGenerator( |
76 |
16006 |
pnm, ts, userContext(), "TheoryPreprocessor::sequence")); |
77 |
|
} |
78 |
15338 |
} |
79 |
|
|
80 |
15333 |
TheoryPreprocessor::~TheoryPreprocessor() {} |
81 |
|
|
82 |
340061 |
TrustNode TheoryPreprocessor::preprocess(TNode node, |
83 |
|
std::vector<SkolemLemma>& newLemmas) |
84 |
|
{ |
85 |
340061 |
return preprocessInternal(node, newLemmas, true); |
86 |
|
} |
87 |
|
|
88 |
878652 |
TrustNode TheoryPreprocessor::preprocessInternal( |
89 |
|
TNode node, std::vector<SkolemLemma>& newLemmas, bool procLemmas) |
90 |
|
{ |
91 |
|
// In this method, all rewriting steps of node are stored in d_tpg. |
92 |
|
|
93 |
878652 |
Trace("tpp") << "TheoryPreprocessor::preprocess: start " << node << std::endl; |
94 |
|
|
95 |
|
// We must rewrite before preprocessing, because some terms when rewritten |
96 |
|
// may introduce new terms that are not top-level and require preprocessing. |
97 |
|
// An example of this is (forall ((x Int)) (and (tail L) (P x))) which |
98 |
|
// rewrites to (and (tail L) (forall ((x Int)) (P x))). The subterm (tail L) |
99 |
|
// must be preprocessed as a child here. |
100 |
1757304 |
Node irNode = rewriteWithProof(node, d_tpgRew.get(), true); |
101 |
|
|
102 |
|
// run theory preprocessing |
103 |
1757304 |
TrustNode tpp = theoryPreprocess(irNode, newLemmas); |
104 |
1757276 |
Node ppNode = tpp.getNode(); |
105 |
|
|
106 |
878638 |
if (Trace.isOn("tpp-debug")) |
107 |
|
{ |
108 |
|
if (node != irNode) |
109 |
|
{ |
110 |
|
Trace("tpp-debug") << "after initial rewriting : " << irNode << std::endl; |
111 |
|
} |
112 |
|
if (irNode != ppNode) |
113 |
|
{ |
114 |
|
Trace("tpp-debug") |
115 |
|
<< "after preprocessing + rewriting and term formula removal : " |
116 |
|
<< ppNode << std::endl; |
117 |
|
} |
118 |
|
Trace("tpp-debug") << "TheoryPreprocessor::preprocess: finish" << std::endl; |
119 |
|
} |
120 |
|
|
121 |
878638 |
if (procLemmas) |
122 |
|
{ |
123 |
|
// Also must preprocess the new lemmas. This is especially important for |
124 |
|
// formulas containing witness terms whose bodies are not in preprocessed |
125 |
|
// form, as term formula removal introduces new lemmas for these that |
126 |
|
// require theory-preprocessing. |
127 |
849585 |
size_t i = 0; |
128 |
907691 |
while (i < newLemmas.size()) |
129 |
|
{ |
130 |
58106 |
TrustNode cur = newLemmas[i].d_lemma; |
131 |
29053 |
newLemmas[i].d_lemma = preprocessLemmaInternal(cur, newLemmas, false); |
132 |
29053 |
Trace("tpp") << "Final lemma : " << newLemmas[i].getProven() << std::endl; |
133 |
29053 |
i++; |
134 |
|
} |
135 |
|
} |
136 |
|
|
137 |
878638 |
if (node == ppNode) |
138 |
|
{ |
139 |
1386012 |
Trace("tpp-debug") << "...TheoryPreprocessor::preprocess returned no change" |
140 |
693006 |
<< std::endl; |
141 |
|
// no change |
142 |
693006 |
return TrustNode::null(); |
143 |
|
} |
144 |
|
|
145 |
|
// Now, sequence the conversion steps if proofs are enabled. |
146 |
371264 |
TrustNode tret; |
147 |
185632 |
if (isProofEnabled()) |
148 |
|
{ |
149 |
150210 |
std::vector<Node> cterms; |
150 |
75105 |
cterms.push_back(node); |
151 |
75105 |
cterms.push_back(irNode); |
152 |
75105 |
cterms.push_back(ppNode); |
153 |
|
// We have that: |
154 |
|
// node -> irNode via rewriting |
155 |
|
// irNode -> ppNode via theory-preprocessing + rewriting + tf removal |
156 |
75105 |
tret = d_tspg->mkTrustRewriteSequence(cterms); |
157 |
75105 |
tret.debugCheckClosed("tpp-debug", "TheoryPreprocessor::lemma_ret"); |
158 |
|
} |
159 |
|
else |
160 |
|
{ |
161 |
110527 |
tret = TrustNode::mkTrustRewrite(node, ppNode, nullptr); |
162 |
|
} |
163 |
|
|
164 |
371264 |
Trace("tpp-debug") << "...TheoryPreprocessor::preprocess returned " |
165 |
185632 |
<< tret.getNode() << std::endl; |
166 |
371264 |
Trace("tpp") << "TheoryPreprocessor::preprocess: return " << tret.getNode() |
167 |
185632 |
<< ", procLemmas=" << procLemmas |
168 |
185632 |
<< ", # lemmas = " << newLemmas.size() << std::endl; |
169 |
185632 |
return tret; |
170 |
|
} |
171 |
|
|
172 |
509538 |
TrustNode TheoryPreprocessor::preprocessLemma( |
173 |
|
TrustNode node, std::vector<SkolemLemma>& newLemmas) |
174 |
|
{ |
175 |
509538 |
return preprocessLemmaInternal(node, newLemmas, true); |
176 |
|
} |
177 |
|
|
178 |
538591 |
TrustNode TheoryPreprocessor::preprocessLemmaInternal( |
179 |
|
TrustNode node, std::vector<SkolemLemma>& newLemmas, bool procLemmas) |
180 |
|
{ |
181 |
|
// what was originally proven |
182 |
1077182 |
Node lemma = node.getProven(); |
183 |
1077182 |
TrustNode tplemma = preprocessInternal(lemma, newLemmas, procLemmas); |
184 |
538589 |
if (tplemma.isNull()) |
185 |
|
{ |
186 |
|
// no change needed |
187 |
392155 |
return node; |
188 |
|
} |
189 |
146434 |
Assert(tplemma.getKind() == TrustNodeKind::REWRITE); |
190 |
|
// what it was preprocessed to |
191 |
292868 |
Node lemmap = tplemma.getNode(); |
192 |
146434 |
Assert(lemmap != node.getProven()); |
193 |
|
// process the preprocessing |
194 |
146434 |
if (isProofEnabled()) |
195 |
|
{ |
196 |
55965 |
Assert(d_lp != nullptr); |
197 |
|
// add the original proof to the lazy proof |
198 |
111930 |
d_lp->addLazyStep( |
199 |
111930 |
node.getProven(), node.getGenerator(), PfRule::THEORY_PREPROCESS_LEMMA); |
200 |
|
// only need to do anything if lemmap changed in a non-trivial way |
201 |
55965 |
if (!CDProof::isSame(lemmap, lemma)) |
202 |
|
{ |
203 |
51706 |
d_lp->addLazyStep(tplemma.getProven(), |
204 |
|
tplemma.getGenerator(), |
205 |
|
PfRule::THEORY_PREPROCESS, |
206 |
|
true, |
207 |
|
"TheoryEngine::lemma_pp"); |
208 |
|
// ---------- from node -------------- from theory preprocess |
209 |
|
// lemma lemma = lemmap |
210 |
|
// ------------------------------------------ EQ_RESOLVE |
211 |
|
// lemmap |
212 |
103412 |
std::vector<Node> pfChildren; |
213 |
51706 |
pfChildren.push_back(lemma); |
214 |
51706 |
pfChildren.push_back(tplemma.getProven()); |
215 |
51706 |
d_lp->addStep(lemmap, PfRule::EQ_RESOLVE, pfChildren, {}); |
216 |
|
} |
217 |
|
} |
218 |
146434 |
return TrustNode::mkTrustLemma(lemmap, d_lp.get()); |
219 |
|
} |
220 |
|
|
221 |
2 |
RemoveTermFormulas& TheoryPreprocessor::getRemoveTermFormulas() |
222 |
|
{ |
223 |
2 |
return d_tfr; |
224 |
|
} |
225 |
|
|
226 |
11274411 |
struct preprocess_stack_element |
227 |
|
{ |
228 |
|
TNode node; |
229 |
|
bool children_added; |
230 |
2721593 |
preprocess_stack_element(TNode n) : node(n), children_added(false) {} |
231 |
|
}; |
232 |
|
|
233 |
878652 |
TrustNode TheoryPreprocessor::theoryPreprocess( |
234 |
|
TNode assertion, std::vector<SkolemLemma>& newLemmas) |
235 |
|
{ |
236 |
1757304 |
Trace("theory::preprocess") |
237 |
878652 |
<< "TheoryPreprocessor::theoryPreprocess(" << assertion << ")" << endl; |
238 |
|
// spendResource(); |
239 |
|
|
240 |
|
// Do a topological sort of the subexpressions and substitute them |
241 |
1757304 |
vector<preprocess_stack_element> toVisit; |
242 |
878652 |
toVisit.push_back(assertion); |
243 |
|
|
244 |
11040222 |
while (!toVisit.empty()) |
245 |
|
{ |
246 |
|
// The current node we are processing |
247 |
5080799 |
preprocess_stack_element& stackHead = toVisit.back(); |
248 |
8453885 |
TNode current = stackHead.node; |
249 |
|
|
250 |
10161598 |
Trace("theory::preprocess-debug") |
251 |
5080799 |
<< "TheoryPreprocessor::theoryPreprocess processing " << current |
252 |
5080799 |
<< endl; |
253 |
|
|
254 |
|
// If node already in the cache we're done, pop from the stack |
255 |
6088813 |
if (d_rtfCache.find(current) != d_rtfCache.end()) |
256 |
|
{ |
257 |
1008014 |
toVisit.pop_back(); |
258 |
1008014 |
continue; |
259 |
|
} |
260 |
|
|
261 |
4072785 |
TheoryId tid = Theory::theoryOf(current); |
262 |
|
|
263 |
4072785 |
if (!logicInfo().isTheoryEnabled(tid) && tid != THEORY_SAT_SOLVER) |
264 |
|
{ |
265 |
|
stringstream ss; |
266 |
|
ss << "The logic was specified as " << logicInfo().getLogicString() |
267 |
|
<< ", which doesn't include " << tid |
268 |
|
<< ", but got a preprocessing-time fact for that theory." << endl |
269 |
|
<< "The fact:" << endl |
270 |
|
<< current; |
271 |
|
throw LogicException(ss.str()); |
272 |
|
} |
273 |
|
// If this is an atom, we preprocess its terms with the theory ppRewriter |
274 |
4072785 |
if (tid != THEORY_BOOL) |
275 |
|
{ |
276 |
1399426 |
Node ppRewritten = ppTheoryRewrite(current, newLemmas); |
277 |
699699 |
Assert(Rewriter::rewrite(ppRewritten) == ppRewritten); |
278 |
699699 |
if (isProofEnabled() && ppRewritten != current) |
279 |
|
{ |
280 |
|
TrustNode trn = |
281 |
7674 |
TrustNode::mkTrustRewrite(current, ppRewritten, d_tpg.get()); |
282 |
3837 |
registerTrustedRewrite(trn, d_tpgRtf.get(), true); |
283 |
|
} |
284 |
|
|
285 |
|
// Term formula removal without fixed point. We do not need to do fixed |
286 |
|
// point since newLemmas are theory-preprocessed until fixed point in |
287 |
|
// preprocessInternal (at top-level, when procLemmas=true). |
288 |
1399398 |
TrustNode ttfr = d_tfr.run(ppRewritten, newLemmas, false); |
289 |
1399398 |
Node rtfNode = ppRewritten; |
290 |
699699 |
if (!ttfr.isNull()) |
291 |
|
{ |
292 |
64553 |
rtfNode = ttfr.getNode(); |
293 |
64553 |
registerTrustedRewrite(ttfr, d_tpgRtf.get(), true); |
294 |
|
} |
295 |
|
// Finish the conversion by rewriting. Notice that we must consider this a |
296 |
|
// pre-rewrite since we do not recursively register the rewriting steps |
297 |
|
// of subterms of rtfNode. For example, if this step rewrites |
298 |
|
// (not A) ---> B, then if registered a pre-rewrite, it will apply when |
299 |
|
// reconstructing proofs via d_tpgRtf. However, if it is a post-rewrite |
300 |
|
// it will fail to apply if another call to this class registers A -> C, |
301 |
|
// in which case (not C) will be returned instead of B (see issue 6754). |
302 |
1399398 |
Node retNode = rewriteWithProof(rtfNode, d_tpgRtf.get(), true); |
303 |
699699 |
d_rtfCache[current] = retNode; |
304 |
699699 |
continue; |
305 |
|
} |
306 |
|
|
307 |
|
// Not yet substituted, so process |
308 |
3373072 |
if (stackHead.children_added) |
309 |
|
{ |
310 |
|
// Children have been processed, so substitute |
311 |
3319036 |
NodeBuilder builder(current.getKind()); |
312 |
1659518 |
if (current.getMetaKind() == kind::metakind::PARAMETERIZED) |
313 |
|
{ |
314 |
|
builder << current.getOperator(); |
315 |
|
} |
316 |
6955387 |
for (unsigned i = 0; i < current.getNumChildren(); ++i) |
317 |
|
{ |
318 |
5295869 |
Assert(d_rtfCache.find(current[i]) != d_rtfCache.end()); |
319 |
5295869 |
builder << d_rtfCache[current[i]].get(); |
320 |
|
} |
321 |
|
// Mark the substitution and continue |
322 |
3319036 |
Node result = builder; |
323 |
|
// always rewrite here, since current may not be in rewritten form after |
324 |
|
// reconstruction |
325 |
1659518 |
result = rewriteWithProof(result, d_tpgRtf.get(), false); |
326 |
3319036 |
Trace("theory::preprocess-debug") |
327 |
1659518 |
<< "TheoryPreprocessor::theoryPreprocess setting " << current |
328 |
1659518 |
<< " -> " << result << endl; |
329 |
1659518 |
d_rtfCache[current] = result; |
330 |
1659518 |
toVisit.pop_back(); |
331 |
|
} |
332 |
|
else |
333 |
|
{ |
334 |
|
// Mark that we have added the children if any |
335 |
1713554 |
if (current.getNumChildren() > 0) |
336 |
|
{ |
337 |
1659530 |
stackHead.children_added = true; |
338 |
|
// We need to add the children |
339 |
6955425 |
for (TNode::iterator child_it = current.begin(); |
340 |
6955425 |
child_it != current.end(); |
341 |
|
++child_it) |
342 |
|
{ |
343 |
10591790 |
TNode childNode = *child_it; |
344 |
5295895 |
if (d_rtfCache.find(childNode) == d_rtfCache.end()) |
345 |
|
{ |
346 |
1842941 |
toVisit.push_back(childNode); |
347 |
|
} |
348 |
|
} |
349 |
|
} |
350 |
|
else |
351 |
|
{ |
352 |
|
// No children, so we're done |
353 |
108048 |
Trace("theory::preprocess-debug") |
354 |
54024 |
<< "SubstitutionMap::internalSubstitute setting " << current |
355 |
54024 |
<< " -> " << current << endl; |
356 |
54024 |
d_rtfCache[current] = current; |
357 |
54024 |
toVisit.pop_back(); |
358 |
|
} |
359 |
|
} |
360 |
|
} |
361 |
878638 |
Assert(d_rtfCache.find(assertion) != d_rtfCache.end()); |
362 |
|
// Return the substituted version |
363 |
1757276 |
Node res = d_rtfCache[assertion]; |
364 |
1757276 |
return TrustNode::mkTrustRewrite(assertion, res, d_tpg.get()); |
365 |
|
} |
366 |
|
|
367 |
|
// Recursively traverse a term and call the theory rewriter on its sub-terms |
368 |
3044172 |
Node TheoryPreprocessor::ppTheoryRewrite(TNode term, |
369 |
|
std::vector<SkolemLemma>& lems) |
370 |
|
{ |
371 |
3044172 |
NodeMap::iterator find = d_ppCache.find(term); |
372 |
3044172 |
if (find != d_ppCache.end()) |
373 |
|
{ |
374 |
668145 |
return (*find).second; |
375 |
|
} |
376 |
2376027 |
if (term.getNumChildren() == 0) |
377 |
|
{ |
378 |
1226249 |
return preprocessWithProof(term, lems); |
379 |
|
} |
380 |
|
// should be in rewritten form here |
381 |
1149782 |
Assert(term == Rewriter::rewrite(term)); |
382 |
1149782 |
Trace("theory-pp") << "ppTheoryRewrite { " << term << endl; |
383 |
|
// do not rewrite inside quantifiers |
384 |
2299564 |
Node newTerm = term; |
385 |
1149782 |
if (!term.isClosure()) |
386 |
|
{ |
387 |
2242496 |
NodeBuilder newNode(term.getKind()); |
388 |
1121248 |
if (term.getMetaKind() == kind::metakind::PARAMETERIZED) |
389 |
|
{ |
390 |
212952 |
newNode << term.getOperator(); |
391 |
|
} |
392 |
3458854 |
for (const Node& nt : term) |
393 |
|
{ |
394 |
2337606 |
newNode << ppTheoryRewrite(nt, lems); |
395 |
|
} |
396 |
1121232 |
newTerm = Node(newNode); |
397 |
1121232 |
newTerm = rewriteWithProof(newTerm, d_tpg.get(), false); |
398 |
|
} |
399 |
1149766 |
newTerm = preprocessWithProof(newTerm, lems); |
400 |
1149756 |
d_ppCache[term] = newTerm; |
401 |
1149756 |
Trace("theory-pp") << "ppTheoryRewrite returning " << newTerm << "}" << endl; |
402 |
1149756 |
return newTerm; |
403 |
|
} |
404 |
|
|
405 |
4365954 |
Node TheoryPreprocessor::rewriteWithProof(Node term, |
406 |
|
TConvProofGenerator* pg, |
407 |
|
bool isPre) |
408 |
|
{ |
409 |
4365954 |
Node termr = Rewriter::rewrite(term); |
410 |
|
// store rewrite step if tracking proofs and it rewrites |
411 |
4365954 |
if (isProofEnabled()) |
412 |
|
{ |
413 |
|
// may rewrite the same term more than once, thus check hasRewriteStep |
414 |
2199194 |
if (termr != term) |
415 |
|
{ |
416 |
150498 |
Trace("tpp-debug") << "TheoryPreprocessor: addRewriteStep (rewriting) " |
417 |
75249 |
<< term << " -> " << termr << std::endl; |
418 |
|
// always use term context hash 0 (default) |
419 |
75249 |
pg->addRewriteStep(term, termr, PfRule::REWRITE, {}, {term}, isPre); |
420 |
|
} |
421 |
|
} |
422 |
4365954 |
return termr; |
423 |
|
} |
424 |
|
|
425 |
2376011 |
Node TheoryPreprocessor::preprocessWithProof(Node term, |
426 |
|
std::vector<SkolemLemma>& lems) |
427 |
|
{ |
428 |
|
// Important that it is in rewritten form, to ensure that the rewrite steps |
429 |
|
// recorded in d_tpg are functional. In other words, there should not |
430 |
|
// be steps from the same term to multiple rewritten forms, which would be |
431 |
|
// the case if we registered a preprocessing step for a non-rewritten term. |
432 |
2376011 |
Assert(term == Rewriter::rewrite(term)); |
433 |
4752022 |
Trace("tpp-debug2") << "preprocessWithProof " << term |
434 |
2376011 |
<< ", #lems = " << lems.size() << std::endl; |
435 |
|
// We never call ppRewrite on equalities here, since equalities have a |
436 |
|
// special status. In particular, notice that theory preprocessing can be |
437 |
|
// called on all formulas asserted to theory engine, including those generated |
438 |
|
// as new literals appearing in lemmas. Calling ppRewrite on equalities is |
439 |
|
// incompatible with theory combination where a split on equality requested |
440 |
|
// by a theory could be preprocessed to something else, thus making theory |
441 |
|
// combination either non-terminating or result in solution soundness. |
442 |
|
// Notice that an alternative solution is to ensure that certain lemmas |
443 |
|
// (e.g. splits from theory combination) can never have theory preprocessing |
444 |
|
// applied to them. However, it is more uniform to say that theory |
445 |
|
// preprocessing is applied to all formulas. This makes it so that e.g. |
446 |
|
// theory solvers do not need to specify whether they want their lemmas to |
447 |
|
// be theory-preprocessed or not. |
448 |
2376011 |
if (term.getKind() == kind::EQUAL) |
449 |
|
{ |
450 |
354893 |
return term; |
451 |
|
} |
452 |
|
// call ppRewrite for the given theory |
453 |
4042236 |
TrustNode trn = d_engine.theoryOf(term)->ppRewrite(term, lems); |
454 |
4042208 |
Trace("tpp-debug2") << "preprocessWithProof returned " << trn |
455 |
2021104 |
<< ", #lems = " << lems.size() << std::endl; |
456 |
2021104 |
if (trn.isNull()) |
457 |
|
{ |
458 |
|
// no change, return |
459 |
2014251 |
return term; |
460 |
|
} |
461 |
13706 |
Node termr = trn.getNode(); |
462 |
6853 |
Assert(term != termr); |
463 |
6853 |
if (isProofEnabled()) |
464 |
|
{ |
465 |
3617 |
registerTrustedRewrite(trn, d_tpg.get(), false); |
466 |
|
} |
467 |
|
// Rewrite again here, which notice is a *pre* rewrite. |
468 |
6853 |
termr = rewriteWithProof(termr, d_tpg.get(), true); |
469 |
6853 |
return ppTheoryRewrite(termr, lems); |
470 |
|
} |
471 |
|
|
472 |
5476579 |
bool TheoryPreprocessor::isProofEnabled() const { return d_tpg != nullptr; } |
473 |
|
|
474 |
72007 |
void TheoryPreprocessor::registerTrustedRewrite(TrustNode trn, |
475 |
|
TConvProofGenerator* pg, |
476 |
|
bool isPre) |
477 |
|
{ |
478 |
72007 |
if (!isProofEnabled() || trn.isNull()) |
479 |
|
{ |
480 |
29510 |
return; |
481 |
|
} |
482 |
42497 |
Assert(trn.getKind() == TrustNodeKind::REWRITE); |
483 |
84994 |
Node eq = trn.getProven(); |
484 |
84994 |
Node term = eq[0]; |
485 |
84994 |
Node termr = eq[1]; |
486 |
42497 |
if (trn.getGenerator() != nullptr) |
487 |
|
{ |
488 |
77774 |
Trace("tpp-debug") << "TheoryPreprocessor: addRewriteStep (generator) " |
489 |
38887 |
<< term << " -> " << termr << std::endl; |
490 |
38887 |
trn.debugCheckClosed("tpp-debug", |
491 |
|
"TheoryPreprocessor::preprocessWithProof"); |
492 |
|
// always use term context hash 0 (default) |
493 |
38887 |
pg->addRewriteStep( |
494 |
|
term, termr, trn.getGenerator(), isPre, PfRule::ASSUME, true); |
495 |
|
} |
496 |
|
else |
497 |
|
{ |
498 |
7220 |
Trace("tpp-debug") << "TheoryPreprocessor: addRewriteStep (trusted) " |
499 |
3610 |
<< term << " -> " << termr << std::endl; |
500 |
|
// small step trust |
501 |
7220 |
pg->addRewriteStep(term, |
502 |
|
termr, |
503 |
|
PfRule::THEORY_PREPROCESS, |
504 |
|
{}, |
505 |
|
{term.eqNode(termr)}, |
506 |
3610 |
isPre); |
507 |
|
} |
508 |
|
} |
509 |
|
|
510 |
|
} // namespace theory |
511 |
31125 |
} // namespace cvc5 |