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