1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Andrew Reynolds, Dejan Jovanovic, Mudathir Mohamed |
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 |
|
* Removal of term formulas. |
14 |
|
*/ |
15 |
|
#include "smt/term_formula_removal.h" |
16 |
|
|
17 |
|
#include <vector> |
18 |
|
|
19 |
|
#include "expr/attribute.h" |
20 |
|
#include "expr/lazy_proof.h" |
21 |
|
#include "expr/node_algorithm.h" |
22 |
|
#include "expr/skolem_manager.h" |
23 |
|
#include "expr/term_context_stack.h" |
24 |
|
#include "expr/term_conversion_proof_generator.h" |
25 |
|
#include "options/smt_options.h" |
26 |
|
|
27 |
|
using namespace std; |
28 |
|
|
29 |
|
namespace cvc5 { |
30 |
|
|
31 |
9494 |
RemoveTermFormulas::RemoveTermFormulas(context::UserContext* u, |
32 |
9494 |
ProofNodeManager* pnm) |
33 |
|
: d_tfCache(u), |
34 |
|
d_skolem_cache(u), |
35 |
|
d_pnm(pnm), |
36 |
|
d_tpg(nullptr), |
37 |
9494 |
d_lp(nullptr) |
38 |
|
{ |
39 |
|
// enable proofs if necessary |
40 |
9494 |
if (d_pnm != nullptr) |
41 |
|
{ |
42 |
7228 |
d_tpg.reset( |
43 |
|
new TConvProofGenerator(d_pnm, |
44 |
|
nullptr, |
45 |
|
TConvPolicy::FIXPOINT, |
46 |
|
TConvCachePolicy::NEVER, |
47 |
|
"RemoveTermFormulas::TConvProofGenerator", |
48 |
3614 |
&d_rtfc)); |
49 |
7228 |
d_lp.reset(new LazyCDProof( |
50 |
3614 |
d_pnm, nullptr, nullptr, "RemoveTermFormulas::LazyCDProof")); |
51 |
|
} |
52 |
9494 |
} |
53 |
|
|
54 |
9494 |
RemoveTermFormulas::~RemoveTermFormulas() {} |
55 |
|
|
56 |
546561 |
theory::TrustNode RemoveTermFormulas::run( |
57 |
|
TNode assertion, |
58 |
|
std::vector<theory::TrustNode>& newAsserts, |
59 |
|
std::vector<Node>& newSkolems, |
60 |
|
bool fixedPoint) |
61 |
|
{ |
62 |
1093122 |
Node itesRemoved = runInternal(assertion, newAsserts, newSkolems); |
63 |
546561 |
Assert(newAsserts.size() == newSkolems.size()); |
64 |
546561 |
if (itesRemoved == assertion) |
65 |
|
{ |
66 |
478944 |
return theory::TrustNode::null(); |
67 |
|
} |
68 |
|
// if running to fixed point, we run each new assertion through the |
69 |
|
// run lemma method |
70 |
67617 |
if (fixedPoint) |
71 |
|
{ |
72 |
2 |
size_t i = 0; |
73 |
1298 |
while (i < newAsserts.size()) |
74 |
|
{ |
75 |
1296 |
theory::TrustNode trn = newAsserts[i]; |
76 |
|
// do not run to fixed point on subcall, since we are processing all |
77 |
|
// lemmas in this loop |
78 |
648 |
newAsserts[i] = runLemma(trn, newAsserts, newSkolems, false); |
79 |
648 |
i++; |
80 |
|
} |
81 |
|
} |
82 |
|
// The rewriting of assertion can be justified by the term conversion proof |
83 |
|
// generator d_tpg. |
84 |
67617 |
return theory::TrustNode::mkTrustRewrite(assertion, itesRemoved, d_tpg.get()); |
85 |
|
} |
86 |
|
|
87 |
|
theory::TrustNode RemoveTermFormulas::run(TNode assertion) |
88 |
|
{ |
89 |
|
std::vector<theory::TrustNode> newAsserts; |
90 |
|
std::vector<Node> newSkolems; |
91 |
|
return run(assertion, newAsserts, newSkolems, false); |
92 |
|
} |
93 |
|
|
94 |
648 |
theory::TrustNode RemoveTermFormulas::runLemma( |
95 |
|
theory::TrustNode lem, |
96 |
|
std::vector<theory::TrustNode>& newAsserts, |
97 |
|
std::vector<Node>& newSkolems, |
98 |
|
bool fixedPoint) |
99 |
|
{ |
100 |
|
theory::TrustNode trn = |
101 |
1296 |
run(lem.getProven(), newAsserts, newSkolems, fixedPoint); |
102 |
648 |
if (trn.isNull()) |
103 |
|
{ |
104 |
|
// no change |
105 |
136 |
return lem; |
106 |
|
} |
107 |
512 |
Assert(trn.getKind() == theory::TrustNodeKind::REWRITE); |
108 |
1024 |
Node newAssertion = trn.getNode(); |
109 |
512 |
if (!isProofEnabled()) |
110 |
|
{ |
111 |
|
// proofs not enabled, just take result |
112 |
256 |
return theory::TrustNode::mkTrustLemma(newAssertion, nullptr); |
113 |
|
} |
114 |
512 |
Trace("rtf-proof-debug") |
115 |
256 |
<< "RemoveTermFormulas::run: setup proof for processed new lemma" |
116 |
256 |
<< std::endl; |
117 |
512 |
Node assertionPre = lem.getProven(); |
118 |
512 |
Node naEq = trn.getProven(); |
119 |
|
// this method is applying this method to TrustNode whose generator is |
120 |
|
// already d_lp (from the run method above), in which case this link is |
121 |
|
// not necessary. |
122 |
256 |
if (trn.getGenerator() != d_lp.get()) |
123 |
|
{ |
124 |
256 |
d_lp->addLazyStep(naEq, trn.getGenerator()); |
125 |
|
} |
126 |
|
// ---------------- from input ------------------------------- from trn |
127 |
|
// assertionPre assertionPre = newAssertion |
128 |
|
// ------------------------------------------------------- EQ_RESOLVE |
129 |
|
// newAssertion |
130 |
256 |
d_lp->addStep(newAssertion, PfRule::EQ_RESOLVE, {assertionPre, naEq}, {}); |
131 |
256 |
return theory::TrustNode::mkTrustLemma(newAssertion, d_lp.get()); |
132 |
|
} |
133 |
|
|
134 |
546561 |
Node RemoveTermFormulas::runInternal(TNode assertion, |
135 |
|
std::vector<theory::TrustNode>& output, |
136 |
|
std::vector<Node>& newSkolems) |
137 |
|
{ |
138 |
546561 |
NodeManager* nm = NodeManager::currentNM(); |
139 |
1093122 |
TCtxStack ctx(&d_rtfc); |
140 |
1093122 |
std::vector<bool> processedChildren; |
141 |
546561 |
ctx.pushInitial(assertion); |
142 |
546561 |
processedChildren.push_back(false); |
143 |
1093122 |
std::pair<Node, uint32_t> initial = ctx.getCurrent(); |
144 |
1093122 |
std::pair<Node, uint32_t> curr; |
145 |
1093122 |
Node node; |
146 |
|
uint32_t nodeVal; |
147 |
546561 |
TermFormulaCache::const_iterator itc; |
148 |
7808407 |
while (!ctx.empty()) |
149 |
|
{ |
150 |
3630923 |
curr = ctx.getCurrent(); |
151 |
3630923 |
itc = d_tfCache.find(curr); |
152 |
3630923 |
node = curr.first; |
153 |
3630923 |
nodeVal = curr.second; |
154 |
3630923 |
Trace("rtf-debug") << "Visit " << node << ", " << nodeVal << std::endl; |
155 |
5119936 |
if (itc != d_tfCache.end()) |
156 |
|
{ |
157 |
1489013 |
Trace("rtf-debug") << "...already computed" << std::endl; |
158 |
1489013 |
ctx.pop(); |
159 |
1489013 |
processedChildren.pop_back(); |
160 |
|
// already computed |
161 |
4195824 |
continue; |
162 |
|
} |
163 |
|
// if we have yet to process children |
164 |
2141910 |
if (!processedChildren.back()) |
165 |
|
{ |
166 |
|
// check if we should replace the current node |
167 |
2435596 |
theory::TrustNode newLem; |
168 |
2435596 |
Node currt = runCurrent(curr, newLem); |
169 |
|
// if we replaced by a skolem, we do not recurse |
170 |
1217798 |
if (!currt.isNull()) |
171 |
|
{ |
172 |
|
// if this is the first time we've seen this term, we have a new lemma |
173 |
|
// which we add to our vectors |
174 |
34314 |
if (!newLem.isNull()) |
175 |
|
{ |
176 |
29086 |
output.push_back(newLem); |
177 |
29086 |
newSkolems.push_back(currt); |
178 |
|
} |
179 |
34314 |
Trace("rtf-debug") << "...replace by skolem" << std::endl; |
180 |
34314 |
d_tfCache.insert(curr, currt); |
181 |
34314 |
ctx.pop(); |
182 |
34314 |
processedChildren.pop_back(); |
183 |
|
} |
184 |
1183484 |
else if (node.isClosure()) |
185 |
|
{ |
186 |
|
// currently, we never do any term formula removal in quantifier bodies |
187 |
27001 |
d_tfCache.insert(curr, node); |
188 |
|
} |
189 |
|
else |
190 |
|
{ |
191 |
1156483 |
size_t nchild = node.getNumChildren(); |
192 |
1156483 |
if (nchild > 0) |
193 |
|
{ |
194 |
924112 |
Trace("rtf-debug") << "...recurse to children" << std::endl; |
195 |
|
// recurse if we have children |
196 |
924112 |
processedChildren[processedChildren.size() - 1] = true; |
197 |
3057361 |
for (size_t i = 0; i < nchild; i++) |
198 |
|
{ |
199 |
2133249 |
ctx.pushChild(node, nodeVal, i); |
200 |
2133249 |
processedChildren.push_back(false); |
201 |
|
} |
202 |
|
} |
203 |
|
else |
204 |
|
{ |
205 |
232371 |
Trace("rtf-debug") << "...base case" << std::endl; |
206 |
232371 |
d_tfCache.insert(curr, node); |
207 |
232371 |
ctx.pop(); |
208 |
232371 |
processedChildren.pop_back(); |
209 |
|
} |
210 |
|
} |
211 |
1217798 |
continue; |
212 |
|
} |
213 |
924112 |
Trace("rtf-debug") << "...reconstruct" << std::endl; |
214 |
|
// otherwise, we are now finished processing children, pop the current node |
215 |
|
// and compute the result |
216 |
924112 |
ctx.pop(); |
217 |
924112 |
processedChildren.pop_back(); |
218 |
|
// if we have not already computed the result |
219 |
1848224 |
std::vector<Node> newChildren; |
220 |
924112 |
bool childChanged = false; |
221 |
924112 |
if (node.getMetaKind() == kind::metakind::PARAMETERIZED) |
222 |
|
{ |
223 |
151770 |
newChildren.push_back(node.getOperator()); |
224 |
|
} |
225 |
|
// reconstruct from the children |
226 |
1848224 |
std::pair<Node, uint32_t> currChild; |
227 |
3057361 |
for (size_t i = 0, nchild = node.getNumChildren(); i < nchild; i++) |
228 |
|
{ |
229 |
|
// recompute the value of the child |
230 |
2133249 |
uint32_t val = d_rtfc.computeValue(node, nodeVal, i); |
231 |
2133249 |
currChild = std::pair<Node, uint32_t>(node[i], val); |
232 |
2133249 |
itc = d_tfCache.find(currChild); |
233 |
2133249 |
Assert(itc != d_tfCache.end()); |
234 |
4266498 |
Node newChild = (*itc).second; |
235 |
2133249 |
Assert(!newChild.isNull()); |
236 |
2133249 |
childChanged |= (newChild != node[i]); |
237 |
2133249 |
newChildren.push_back(newChild); |
238 |
|
} |
239 |
|
// If changes, we reconstruct the node |
240 |
1848224 |
Node ret = node; |
241 |
924112 |
if (childChanged) |
242 |
|
{ |
243 |
114061 |
ret = nm->mkNode(node.getKind(), newChildren); |
244 |
|
} |
245 |
|
// cache |
246 |
924112 |
d_tfCache.insert(curr, ret); |
247 |
|
} |
248 |
546561 |
itc = d_tfCache.find(initial); |
249 |
546561 |
Assert(itc != d_tfCache.end()); |
250 |
1093122 |
return (*itc).second; |
251 |
|
} |
252 |
|
|
253 |
1217798 |
Node RemoveTermFormulas::runCurrent(std::pair<Node, uint32_t>& curr, |
254 |
|
theory::TrustNode& newLem) |
255 |
|
{ |
256 |
2435596 |
TNode node = curr.first; |
257 |
1217798 |
uint32_t cval = curr.second; |
258 |
|
bool inQuant, inTerm; |
259 |
1217798 |
RtfTermContext::getFlags(curr.second, inQuant, inTerm); |
260 |
2435596 |
Debug("ite") << "removeITEs(" << node << ")" |
261 |
1217798 |
<< " " << inQuant << " " << inTerm << std::endl; |
262 |
1217798 |
Assert(!inQuant); |
263 |
|
|
264 |
1217798 |
NodeManager *nodeManager = NodeManager::currentNM(); |
265 |
|
|
266 |
2435596 |
TypeNode nodeType = node.getType(); |
267 |
2435596 |
Node skolem; |
268 |
2435596 |
Node newAssertion; |
269 |
|
// the exists form of the assertion |
270 |
1217798 |
ProofGenerator* newAssertionPg = nullptr; |
271 |
|
// Handle non-Boolean ITEs here. Boolean ones (within terms) are handled |
272 |
|
// in the "non-variable Boolean term within term" case below. |
273 |
1217798 |
if (node.getKind() == kind::ITE && !nodeType.isBoolean()) |
274 |
|
{ |
275 |
|
// Here, we eliminate the ITE if we are not Boolean and if we are |
276 |
|
// not in a quantified formula. This policy should be in sync with |
277 |
|
// the policy for when to apply theory preprocessing to terms, see PR |
278 |
|
// #5497. |
279 |
32693 |
skolem = getSkolemForNode(node); |
280 |
32693 |
if (skolem.isNull()) |
281 |
|
{ |
282 |
54974 |
Trace("rtf-proof-debug") |
283 |
27487 |
<< "RemoveTermFormulas::run: make ITE skolem" << std::endl; |
284 |
|
// Make the skolem to represent the ITE |
285 |
27487 |
SkolemManager* sm = nodeManager->getSkolemManager(); |
286 |
27487 |
skolem = sm->mkPurifySkolem( |
287 |
|
node, |
288 |
|
"termITE", |
289 |
|
"a variable introduced due to term-level ITE removal"); |
290 |
27487 |
d_skolem_cache.insert(node, skolem); |
291 |
|
|
292 |
|
// Notice that in very rare cases, two different terms may have the |
293 |
|
// same purification skolem (see SkolemManager::mkPurifySkolem) For such |
294 |
|
// cases, for simplicity, we repeat the work of constructing the |
295 |
|
// assertion and proofs below. This is so that the proof for the new form |
296 |
|
// of the lemma is used. |
297 |
|
|
298 |
|
// The new assertion |
299 |
82461 |
newAssertion = nodeManager->mkNode( |
300 |
109948 |
kind::ITE, node[0], skolem.eqNode(node[1]), skolem.eqNode(node[2])); |
301 |
|
|
302 |
|
// we justify it internally |
303 |
27487 |
if (isProofEnabled()) |
304 |
|
{ |
305 |
28072 |
Trace("rtf-proof-debug") |
306 |
14036 |
<< "RemoveTermFormulas::run: justify " << newAssertion |
307 |
14036 |
<< " with ITE axiom" << std::endl; |
308 |
|
// ---------------------- REMOVE_TERM_FORMULA_AXIOM |
309 |
|
// (ite node[0] |
310 |
|
// (= node node[1]) ------------- MACRO_SR_PRED_INTRO |
311 |
|
// (= node node[2])) node = skolem |
312 |
|
// ------------------------------------------ MACRO_SR_PRED_TRANSFORM |
313 |
|
// (ite node[0] (= skolem node[1]) (= skolem node[2])) |
314 |
|
// |
315 |
|
// Note that the MACRO_SR_PRED_INTRO step holds due to conversion |
316 |
|
// of skolem into its witness form, which is node. |
317 |
28072 |
Node axiom = getAxiomFor(node); |
318 |
14036 |
d_lp->addStep(axiom, PfRule::REMOVE_TERM_FORMULA_AXIOM, {}, {node}); |
319 |
28072 |
Node eq = node.eqNode(skolem); |
320 |
14036 |
d_lp->addStep(eq, PfRule::MACRO_SR_PRED_INTRO, {}, {eq}); |
321 |
56144 |
d_lp->addStep(newAssertion, |
322 |
|
PfRule::MACRO_SR_PRED_TRANSFORM, |
323 |
|
{axiom, eq}, |
324 |
42108 |
{newAssertion}); |
325 |
14036 |
newAssertionPg = d_lp.get(); |
326 |
|
} |
327 |
|
} |
328 |
|
} |
329 |
1185105 |
else if (node.getKind() == kind::LAMBDA) |
330 |
|
{ |
331 |
|
// if a lambda, do lambda-lifting |
332 |
25 |
if (!expr::hasFreeVar(node)) |
333 |
|
{ |
334 |
25 |
skolem = getSkolemForNode(node); |
335 |
25 |
if (skolem.isNull()) |
336 |
|
{ |
337 |
50 |
Trace("rtf-proof-debug") |
338 |
25 |
<< "RemoveTermFormulas::run: make LAMBDA skolem" << std::endl; |
339 |
|
// Make the skolem to represent the lambda |
340 |
25 |
SkolemManager* sm = nodeManager->getSkolemManager(); |
341 |
25 |
skolem = sm->mkPurifySkolem( |
342 |
|
node, |
343 |
|
"lambdaF", |
344 |
|
"a function introduced due to term-level lambda removal"); |
345 |
25 |
d_skolem_cache.insert(node, skolem); |
346 |
|
|
347 |
|
// The new assertion |
348 |
50 |
std::vector<Node> children; |
349 |
|
// bound variable list |
350 |
25 |
children.push_back(node[0]); |
351 |
|
// body |
352 |
50 |
std::vector<Node> skolem_app_c; |
353 |
25 |
skolem_app_c.push_back(skolem); |
354 |
25 |
skolem_app_c.insert(skolem_app_c.end(), node[0].begin(), node[0].end()); |
355 |
50 |
Node skolem_app = nodeManager->mkNode(kind::APPLY_UF, skolem_app_c); |
356 |
25 |
children.push_back(skolem_app.eqNode(node[1])); |
357 |
|
// axiom defining skolem |
358 |
25 |
newAssertion = nodeManager->mkNode(kind::FORALL, children); |
359 |
|
|
360 |
|
// Lambda lifting is trivial to justify, hence we don't set a proof |
361 |
|
// generator here. In particular, replacing the skolem introduced |
362 |
|
// here with its original lambda ensures the new assertion rewrites |
363 |
|
// to true. |
364 |
|
// For example, if (lambda y. t[y]) has skolem k, then this lemma is: |
365 |
|
// forall x. k(x)=t[x] |
366 |
|
// whose witness form rewrites |
367 |
|
// forall x. (lambda y. t[y])(x)=t[x] --> forall x. t[x]=t[x] --> true |
368 |
|
} |
369 |
|
} |
370 |
|
} |
371 |
1185080 |
else if (node.getKind() == kind::WITNESS) |
372 |
|
{ |
373 |
|
// If a witness choice |
374 |
|
// For details on this operator, see |
375 |
|
// http://planetmath.org/hilbertsvarepsilonoperator. |
376 |
578 |
if (!expr::hasFreeVar(node)) |
377 |
|
{ |
378 |
|
// NOTE: we can replace by t if body is of the form (and (= z t) ...) |
379 |
578 |
skolem = getSkolemForNode(node); |
380 |
578 |
if (skolem.isNull()) |
381 |
|
{ |
382 |
1112 |
Trace("rtf-proof-debug") |
383 |
556 |
<< "RemoveTermFormulas::run: make WITNESS skolem" << std::endl; |
384 |
|
// Make the skolem to witness the choice, which notice is handled |
385 |
|
// as a special case within SkolemManager::mkPurifySkolem. |
386 |
556 |
SkolemManager* sm = nodeManager->getSkolemManager(); |
387 |
556 |
skolem = sm->mkPurifySkolem( |
388 |
|
node, |
389 |
|
"witnessK", |
390 |
|
"a skolem introduced due to term-level witness removal"); |
391 |
556 |
d_skolem_cache.insert(node, skolem); |
392 |
|
|
393 |
556 |
Assert(node[0].getNumChildren() == 1); |
394 |
|
|
395 |
|
// The new assertion is the assumption that the body |
396 |
|
// of the witness operator holds for the Skolem |
397 |
556 |
newAssertion = node[1].substitute(node[0][0], skolem); |
398 |
|
|
399 |
|
// Get the proof generator, if one exists, which was responsible for |
400 |
|
// constructing this witness term. This may not exist, in which case |
401 |
|
// the witness term was trivial to justify. This is the case e.g. for |
402 |
|
// purification witness terms. |
403 |
556 |
if (isProofEnabled()) |
404 |
|
{ |
405 |
|
Node existsAssertion = |
406 |
150 |
nodeManager->mkNode(kind::EXISTS, node[0], node[1]); |
407 |
|
// -------------------- from skolem manager |
408 |
|
// (exists x. node[1]) |
409 |
|
// -------------------- SKOLEMIZE |
410 |
|
// node[1] * { x -> skolem } |
411 |
75 |
ProofGenerator* expg = sm->getProofGenerator(existsAssertion); |
412 |
75 |
d_lp->addLazyStep(existsAssertion, |
413 |
|
expg, |
414 |
|
PfRule::WITNESS_AXIOM, |
415 |
|
true, |
416 |
|
"RemoveTermFormulas::run:skolem_pf"); |
417 |
75 |
d_lp->addStep(newAssertion, PfRule::SKOLEMIZE, {existsAssertion}, {}); |
418 |
75 |
newAssertionPg = d_lp.get(); |
419 |
|
} |
420 |
|
} |
421 |
|
} |
422 |
|
} |
423 |
3551977 |
else if (node.getKind() != kind::BOOLEAN_TERM_VARIABLE && nodeType.isBoolean() |
424 |
1751556 |
&& inTerm) |
425 |
|
{ |
426 |
|
// if a non-variable Boolean term within another term, replace it |
427 |
1018 |
skolem = getSkolemForNode(node); |
428 |
1018 |
if (skolem.isNull()) |
429 |
|
{ |
430 |
2036 |
Trace("rtf-proof-debug") |
431 |
1018 |
<< "RemoveTermFormulas::run: make BOOLEAN_TERM_VARIABLE skolem" |
432 |
1018 |
<< std::endl; |
433 |
|
// Make the skolem to represent the Boolean term |
434 |
|
// Skolems introduced for Boolean formulas appearing in terms have a |
435 |
|
// special kind (BOOLEAN_TERM_VARIABLE) that ensures they are handled |
436 |
|
// properly in theory combination. We must use this kind here instead of a |
437 |
|
// generic skolem. Notice that the name/comment are currently ignored |
438 |
|
// within SkolemManager::mkPurifySkolem, since BOOLEAN_TERM_VARIABLE |
439 |
|
// variables cannot be given names. |
440 |
1018 |
SkolemManager* sm = nodeManager->getSkolemManager(); |
441 |
1018 |
skolem = sm->mkPurifySkolem( |
442 |
|
node, |
443 |
|
"btvK", |
444 |
|
"a Boolean term variable introduced during term formula removal", |
445 |
|
NodeManager::SKOLEM_BOOL_TERM_VAR); |
446 |
1018 |
d_skolem_cache.insert(node, skolem); |
447 |
|
|
448 |
|
// The new assertion |
449 |
1018 |
newAssertion = skolem.eqNode(node); |
450 |
|
|
451 |
|
// Boolean term removal is trivial to justify, hence we don't set a proof |
452 |
|
// generator here. It is trivial to justify since it is an instance of |
453 |
|
// purification, which is justified by conversion to witness forms. |
454 |
|
} |
455 |
|
} |
456 |
|
|
457 |
|
// if the term should be replaced by a skolem |
458 |
1217798 |
if( !skolem.isNull() ){ |
459 |
|
// this must be done regardless of whether the assertion was new below, |
460 |
|
// since a formula-term may rewrite to the same skolem in multiple contexts. |
461 |
34314 |
if (isProofEnabled()) |
462 |
|
{ |
463 |
|
// justify the introduction of the skolem |
464 |
|
// ------------------- MACRO_SR_PRED_INTRO |
465 |
|
// t = witness x. x=t |
466 |
|
// The above step is trivial, since the skolems introduced above are |
467 |
|
// all purification skolems. We record this equality in the term |
468 |
|
// conversion proof generator. |
469 |
33972 |
d_tpg->addRewriteStep(node, |
470 |
|
skolem, |
471 |
|
PfRule::MACRO_SR_PRED_INTRO, |
472 |
|
{}, |
473 |
|
{node.eqNode(skolem)}, |
474 |
|
true, |
475 |
16986 |
cval); |
476 |
|
} |
477 |
|
|
478 |
|
// if the skolem was introduced in this call |
479 |
34314 |
if (!newAssertion.isNull()) |
480 |
|
{ |
481 |
58172 |
Trace("rtf-proof-debug") |
482 |
29086 |
<< "RemoveTermFormulas::run: setup proof for new assertion " |
483 |
29086 |
<< newAssertion << std::endl; |
484 |
|
// if proofs are enabled |
485 |
29086 |
if (isProofEnabled()) |
486 |
|
{ |
487 |
|
// justify the axiom that defines the skolem, if not already done so |
488 |
14441 |
if (newAssertionPg == nullptr) |
489 |
|
{ |
490 |
|
// Should have trivial justification if not yet provided. This is the |
491 |
|
// case of lambda lifting and Boolean term removal. |
492 |
|
// ---------------- MACRO_SR_PRED_INTRO |
493 |
|
// newAssertion |
494 |
660 |
d_lp->addStep( |
495 |
330 |
newAssertion, PfRule::MACRO_SR_PRED_INTRO, {}, {newAssertion}); |
496 |
|
} |
497 |
|
} |
498 |
58172 |
Trace("rtf-debug") << "*** term formula removal introduced " << skolem |
499 |
29086 |
<< " for " << node << std::endl; |
500 |
|
|
501 |
29086 |
newLem = theory::TrustNode::mkTrustLemma(newAssertion, d_lp.get()); |
502 |
|
|
503 |
29086 |
Trace("rtf-proof-debug") << "Checking closed..." << std::endl; |
504 |
29086 |
newLem.debugCheckClosed("rtf-proof-debug", |
505 |
|
"RemoveTermFormulas::run:new_assert"); |
506 |
|
} |
507 |
|
|
508 |
|
// The representation is now the skolem |
509 |
34314 |
return skolem; |
510 |
|
} |
511 |
|
|
512 |
|
// return null, indicating we will traverse children within runInternal |
513 |
1183484 |
return Node::null(); |
514 |
|
} |
515 |
|
|
516 |
34314 |
Node RemoveTermFormulas::getSkolemForNode(Node k) const |
517 |
|
{ |
518 |
|
context::CDInsertHashMap<Node, Node>::const_iterator itk = |
519 |
34314 |
d_skolem_cache.find(k); |
520 |
34314 |
if (itk != d_skolem_cache.end()) |
521 |
|
{ |
522 |
5228 |
return itk->second; |
523 |
|
} |
524 |
29086 |
return Node::null(); |
525 |
|
} |
526 |
|
|
527 |
29096 |
Node RemoveTermFormulas::getAxiomFor(Node n) |
528 |
|
{ |
529 |
29096 |
NodeManager* nm = NodeManager::currentNM(); |
530 |
29096 |
Kind k = n.getKind(); |
531 |
29096 |
if (k == kind::ITE) |
532 |
|
{ |
533 |
29096 |
return nm->mkNode(kind::ITE, n[0], n.eqNode(n[1]), n.eqNode(n[2])); |
534 |
|
} |
535 |
|
return Node::null(); |
536 |
|
} |
537 |
|
|
538 |
|
ProofGenerator* RemoveTermFormulas::getTConvProofGenerator() |
539 |
|
{ |
540 |
|
return d_tpg.get(); |
541 |
|
} |
542 |
|
|
543 |
91955 |
bool RemoveTermFormulas::isProofEnabled() const { return d_pnm != nullptr; } |
544 |
|
|
545 |
28191 |
} // namespace cvc5 |