Branch data Line data Source code
1 : : /******************************************************************************
2 : : * Top contributors (to current version):
3 : : * Andrew Reynolds, Dejan Jovanovic, Hans-Joerg Schurr
4 : : *
5 : : * This file is part of the cvc5 project.
6 : : *
7 : : * Copyright (c) 2009-2024 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 : : #include "smt/logic_exception.h"
28 : :
29 : : using namespace std;
30 : :
31 : : namespace cvc5::internal {
32 : :
33 : 50591 : RemoveTermFormulas::RemoveTermFormulas(Env& env)
34 : : : EnvObj(env),
35 : 101182 : d_tfCache(userContext()),
36 : 101182 : d_skolem_cache(userContext()),
37 : : d_tpg(nullptr),
38 : 50591 : d_lp(nullptr)
39 : : {
40 : : // enable proofs if necessary
41 : 50591 : ProofNodeManager* pnm = env.getProofNodeManager();
42 [ + + ]: 50591 : if (pnm != nullptr)
43 : : {
44 : 39086 : d_tpg.reset(
45 : : new TConvProofGenerator(env,
46 : : nullptr,
47 : : TConvPolicy::FIXPOINT,
48 : : TConvCachePolicy::NEVER,
49 : : "RemoveTermFormulas::TConvProofGenerator",
50 : 19543 : &d_rtfc));
51 : 39086 : d_tpgi.reset(
52 : : new TConvProofGenerator(env,
53 : : nullptr,
54 : : TConvPolicy::ONCE,
55 : : TConvCachePolicy::NEVER,
56 : 19543 : "RemoveTermFormulas::TConvProofGenerator"));
57 : 39086 : d_lp.reset(new LazyCDProof(
58 : 19543 : env, nullptr, nullptr, "RemoveTermFormulas::LazyCDProof"));
59 : : }
60 : 50591 : }
61 : :
62 : 50335 : RemoveTermFormulas::~RemoveTermFormulas() {}
63 : :
64 : 1633 : TrustNode RemoveTermFormulas::run(TNode assertion,
65 : : std::vector<theory::SkolemLemma>& newAsserts,
66 : : bool fixedPoint)
67 : : {
68 : 3266 : Node itesRemoved = runInternal(assertion, newAsserts);
69 [ + + ]: 1633 : if (itesRemoved == assertion)
70 : : {
71 : 1145 : return TrustNode::null();
72 : : }
73 : : // if running to fixed point, we run each new assertion through the
74 : : // run lemma method
75 [ + + ]: 488 : if (fixedPoint)
76 : : {
77 : 232 : size_t i = 0;
78 [ + + ]: 556 : while (i < newAsserts.size())
79 : : {
80 : 324 : TrustNode trn = newAsserts[i].d_lemma;
81 : : // do not run to fixed point on subcall, since we are processing all
82 : : // lemmas in this loop
83 : 324 : newAsserts[i].d_lemma = runLemma(trn, newAsserts, false);
84 : 324 : i++;
85 : : }
86 : : }
87 : : // The rewriting of assertion can be justified by the term conversion proof
88 : : // generator d_tpg.
89 [ - + ]: 488 : return TrustNode::mkTrustRewrite(assertion, itesRemoved, d_tpg.get());
90 : : }
91 : :
92 : 324 : TrustNode RemoveTermFormulas::runLemma(
93 : : TrustNode lem,
94 : : std::vector<theory::SkolemLemma>& newAsserts,
95 : : bool fixedPoint)
96 : : {
97 : 972 : TrustNode trn = run(lem.getProven(), newAsserts, fixedPoint);
98 [ + + ]: 324 : if (trn.isNull())
99 : : {
100 : : // no change
101 : 68 : return lem;
102 : : }
103 [ - + ][ - + ]: 256 : Assert(trn.getKind() == TrustNodeKind::REWRITE);
[ - - ]
104 : 512 : Node newAssertion = trn.getNode();
105 [ + - ]: 256 : if (!d_env.isTheoryProofProducing())
106 : : {
107 : : // proofs not enabled, just take result
108 : 256 : return TrustNode::mkTrustLemma(newAssertion, nullptr);
109 : : }
110 [ - - ]: 0 : Trace("rtf-proof-debug")
111 : 0 : << "RemoveTermFormulas::run: setup proof for processed new lemma"
112 : 0 : << std::endl;
113 : 0 : Node assertionPre = lem.getProven();
114 : 0 : Node naEq = trn.getProven();
115 : : // this method is applying this method to TrustNode whose generator is
116 : : // already d_lp (from the run method above), in which case this link is
117 : : // not necessary.
118 : 0 : if (trn.getGenerator() != d_lp.get())
119 : : {
120 : 0 : d_lp->addLazyStep(naEq, trn.getGenerator());
121 : : }
122 : : // ---------------- from input ------------------------------- from trn
123 : : // assertionPre assertionPre = newAssertion
124 : : // ------------------------------------------------------- EQ_RESOLVE
125 : : // newAssertion
126 : 0 : d_lp->addStep(newAssertion, ProofRule::EQ_RESOLVE, {assertionPre, naEq}, {});
127 [ - - ]: 0 : return TrustNode::mkTrustLemma(newAssertion, d_lp.get());
128 : : }
129 : :
130 : 1633 : Node RemoveTermFormulas::runInternal(TNode assertion,
131 : : std::vector<theory::SkolemLemma>& output)
132 : : {
133 : 1633 : NodeManager* nm = nodeManager();
134 : 3266 : TCtxStack ctx(&d_rtfc);
135 : 3266 : std::vector<bool> processedChildren;
136 : 1633 : ctx.pushInitial(assertion);
137 : 1633 : processedChildren.push_back(false);
138 : 3266 : std::pair<Node, uint32_t> initial = ctx.getCurrent();
139 : 3266 : std::pair<Node, uint32_t> curr;
140 : 3266 : Node node;
141 : : uint32_t nodeVal;
142 : 1633 : TermFormulaCache::const_iterator itc;
143 [ + + ]: 131231 : while (!ctx.empty())
144 : : {
145 : 129598 : curr = ctx.getCurrent();
146 : 129598 : itc = d_tfCache.find(curr);
147 : 129598 : node = curr.first;
148 : 129598 : nodeVal = curr.second;
149 [ + - ]: 129598 : Trace("rtf-debug") << "Visit " << node << ", " << nodeVal << std::endl;
150 [ + + ]: 129598 : if (itc != d_tfCache.end())
151 : : {
152 [ + - ]: 108506 : Trace("rtf-debug") << "...already computed" << std::endl;
153 : 108506 : ctx.pop();
154 : 108506 : processedChildren.pop_back();
155 : : // already computed
156 : 120057 : continue;
157 : : }
158 : : // if we have yet to process children
159 [ + + ]: 21092 : if (!processedChildren.back())
160 : : {
161 : : // check if we should replace the current node
162 : 23102 : TrustNode newLem;
163 : : bool inQuant, inTerm;
164 : 11551 : RtfTermContext::getFlags(nodeVal, inQuant, inTerm);
165 [ + - ]: 23102 : Trace("ite") << "removeITEs(" << node << ")"
166 : 11551 : << " " << inQuant << " " << inTerm << std::endl;
167 [ - + ][ - + ]: 11551 : Assert(!inQuant);
[ - - ]
168 : : Node currt =
169 : 23102 : runCurrentInternal(node, inTerm, newLem, nodeVal, d_tpg.get());
170 : : // if we replaced by a skolem, we do not recurse
171 [ + + ]: 11551 : if (!currt.isNull())
172 : : {
173 : : // if this is the first time we've seen this term, we have a new lemma
174 : : // which we add to our vectors
175 [ + + ]: 408 : if (!newLem.isNull())
176 : : {
177 : 324 : output.push_back(theory::SkolemLemma(newLem, currt));
178 : : }
179 [ + - ]: 408 : Trace("rtf-debug") << "...replace by skolem" << std::endl;
180 : 408 : d_tfCache.insert(curr, currt);
181 : 408 : ctx.pop();
182 : 408 : processedChildren.pop_back();
183 : : }
184 [ - + ]: 11143 : else if (node.isClosure())
185 : : {
186 : : // currently, we never do any term formula removal in quantifier bodies
187 : 0 : d_tfCache.insert(curr, node);
188 : : }
189 : : else
190 : : {
191 : 11143 : size_t nchild = node.getNumChildren();
192 [ + + ]: 11143 : if (nchild > 0)
193 : : {
194 [ + - ]: 9541 : Trace("rtf-debug") << "...recurse to children" << std::endl;
195 : : // recurse if we have children
196 : 9541 : processedChildren[processedChildren.size() - 1] = true;
197 [ + + ]: 127965 : for (size_t i = 0; i < nchild; i++)
198 : : {
199 : 118424 : ctx.pushChild(node, nodeVal, i);
200 : 118424 : processedChildren.push_back(false);
201 : : }
202 : : }
203 : : else
204 : : {
205 [ + - ]: 1602 : Trace("rtf-debug") << "...base case" << std::endl;
206 : 1602 : d_tfCache.insert(curr, node);
207 : 1602 : ctx.pop();
208 : 1602 : processedChildren.pop_back();
209 : : }
210 : : }
211 : 11551 : continue;
212 : : }
213 [ + - ]: 9541 : Trace("rtf-debug") << "...reconstruct" << std::endl;
214 : : // otherwise, we are now finished processing children, pop the current node
215 : : // and compute the result
216 : 9541 : ctx.pop();
217 : 9541 : processedChildren.pop_back();
218 : : // if we have not already computed the result
219 : 19082 : std::vector<Node> newChildren;
220 : 9541 : bool childChanged = false;
221 [ - + ]: 9541 : if (node.getMetaKind() == kind::metakind::PARAMETERIZED)
222 : : {
223 : 0 : newChildren.push_back(node.getOperator());
224 : : }
225 : : // reconstruct from the children
226 : 19082 : std::pair<Node, uint32_t> currChild;
227 [ + + ]: 127965 : for (size_t i = 0, nchild = node.getNumChildren(); i < nchild; i++)
228 : : {
229 : : // recompute the value of the child
230 : 118424 : uint32_t val = d_rtfc.computeValue(node, nodeVal, i);
231 : 118424 : currChild = std::pair<Node, uint32_t>(node[i], val);
232 : 118424 : itc = d_tfCache.find(currChild);
233 [ - + ][ - + ]: 118424 : Assert(itc != d_tfCache.end());
[ - - ]
234 : 236848 : Node newChild = (*itc).second;
235 [ - + ][ - + ]: 118424 : Assert(!newChild.isNull());
[ - - ]
236 : 118424 : childChanged |= (newChild != node[i]);
237 : 118424 : newChildren.push_back(newChild);
238 : : }
239 : : // If changes, we reconstruct the node
240 : 19082 : Node ret = node;
241 [ + + ]: 9541 : if (childChanged)
242 : : {
243 : 1013 : ret = nm->mkNode(node.getKind(), newChildren);
244 : : }
245 : : // cache
246 : 9541 : d_tfCache.insert(curr, ret);
247 : : }
248 : 1633 : itc = d_tfCache.find(initial);
249 [ - + ][ - + ]: 1633 : Assert(itc != d_tfCache.end());
[ - - ]
250 : 3266 : return (*itc).second;
251 : : }
252 : :
253 : 5416890 : TrustNode RemoveTermFormulas::runCurrent(TNode node,
254 : : bool inTerm,
255 : : TrustNode& newLem)
256 : : {
257 : : // use the term conversion generator that is term context insensitive, with
258 : : // cval set to 0.
259 : 10833800 : Node k = runCurrentInternal(node, inTerm, newLem, 0, d_tpgi.get());
260 [ + + ]: 5416890 : if (!k.isNull())
261 : : {
262 [ + + ]: 43490 : return TrustNode::mkTrustRewrite(node, k, d_tpgi.get());
263 : : }
264 : 5373400 : return TrustNode::null();
265 : : }
266 : :
267 : 5428440 : Node RemoveTermFormulas::runCurrentInternal(TNode node,
268 : : bool inTerm,
269 : : TrustNode& newLem,
270 : : uint32_t cval,
271 : : TConvProofGenerator* pg)
272 : : {
273 [ - + ][ - + ]: 5428440 : AlwaysAssert (node.getKind()!=Kind::WITNESS) << "WITNESS should never appear in asserted terms";
[ - - ]
274 : 5428440 : SkolemManager* sm = nodeManager()->getSkolemManager();
275 : :
276 : 10856900 : TypeNode nodeType = node.getType();
277 : 10856900 : Node skolem;
278 : 10856900 : Node newAssertion;
279 : : // the exists form of the assertion
280 : 5428440 : ProofGenerator* newAssertionPg = nullptr;
281 : : // Handle non-Boolean ITEs here. Boolean ones (within terms) are handled
282 : : // in the "non-variable Boolean term within term" case below.
283 [ + + ][ + + ]: 5428440 : if (node.getKind() == Kind::ITE && !nodeType.isBoolean())
[ + + ]
284 : : {
285 [ + + ]: 41276 : if (!nodeType.isFirstClass())
286 : : {
287 : 4 : std::stringstream ss;
288 : 2 : ss << "ITE branches of type " << nodeType
289 : 2 : << " are currently not supported." << std::endl;
290 : 2 : throw LogicException(ss.str());
291 : : }
292 : : // Here, we eliminate the ITE if we are not Boolean and if we are
293 : : // not in a quantified formula. This policy should be in sync with
294 : : // the policy for when to apply theory preprocessing to terms, see PR
295 : : // #5497.
296 : 41274 : skolem = getSkolemForNode(node);
297 [ + + ]: 41274 : if (skolem.isNull())
298 : : {
299 [ + - ]: 71458 : Trace("rtf-proof-debug")
300 : 35729 : << "RemoveTermFormulas::run: make ITE skolem" << std::endl;
301 : : // Make the skolem to represent the ITE
302 : 35729 : skolem = sm->mkPurifySkolem(node);
303 : 35729 : d_skolem_cache.insert(node, skolem);
304 : :
305 : : // Notice that in very rare cases, two different terms may have the
306 : : // same purification skolem (see SkolemManager::mkPurifySkolem) For such
307 : : // cases, for simplicity, we repeat the work of constructing the
308 : : // assertion and proofs below. This is so that the proof for the new form
309 : : // of the lemma is used.
310 : :
311 : : // The new assertion
312 : 35729 : newAssertion = nodeManager()->mkNode(
313 : 35729 : Kind::ITE, node[0], skolem.eqNode(node[1]), skolem.eqNode(node[2]));
314 : :
315 : : // we justify it internally
316 [ + + ]: 35729 : if (isProofEnabled())
317 : : {
318 [ + - ]: 47706 : Trace("rtf-proof-debug")
319 : 0 : << "RemoveTermFormulas::run: justify " << newAssertion
320 : 23853 : << " with ITE axiom" << std::endl;
321 : : // ---------------------- ITE_EQ
322 : : // (ite node[0]
323 : : // (= node node[1]) ------------- MACRO_SR_PRED_INTRO
324 : : // (= node node[2])) node = skolem
325 : : // ------------------------------------------ MACRO_SR_PRED_TRANSFORM
326 : : // (ite node[0] (= skolem node[1]) (= skolem node[2]))
327 : : //
328 : : // Note that the MACRO_SR_PRED_INTRO step holds due to conversion
329 : : // of skolem into its witness form, which is node.
330 : 47706 : Node axiom = getAxiomFor(node);
331 : 47706 : d_lp->addStep(axiom, ProofRule::ITE_EQ, {}, {node});
332 : 23853 : Node eq = node.eqNode(skolem);
333 : 47706 : d_lp->addStep(eq, ProofRule::MACRO_SR_PRED_INTRO, {}, {eq});
334 : 95412 : d_lp->addStep(newAssertion,
335 : : ProofRule::MACRO_SR_PRED_TRANSFORM,
336 : : {axiom, eq},
337 : 71559 : {newAssertion});
338 [ + - ]: 23853 : newAssertionPg = d_lp.get();
339 : : }
340 : : }
341 : : }
342 [ + + ][ + + ]: 5387170 : else if (nodeType.isBoolean() && inTerm && !d_env.isBooleanTermSkolem(node))
[ + + ][ + + ]
[ + + ][ - - ]
343 : : {
344 : : // if a purification skolem already, just use itself
345 [ + + ]: 2674 : if (sm->getId(node) == SkolemId::PURIFY)
346 : : {
347 : 50 : d_env.registerBooleanTermSkolem(node);
348 : 50 : return Node::null();
349 : : }
350 : : // if a non-variable Boolean term within another term, replace it
351 : 2624 : skolem = getSkolemForNode(node);
352 [ + - ]: 2624 : if (skolem.isNull())
353 : : {
354 [ + - ]: 5248 : Trace("rtf-proof-debug")
355 : 2624 : << "RemoveTermFormulas::run: make Boolean skolem" << std::endl;
356 : : // Make the skolem to represent the Boolean term
357 : : // Skolems introduced for Boolean formulas appearing in terms are
358 : : // purified here (SkolemId::PURIFY), which ensures they are handled
359 : : // properly in theory combination.
360 : 2624 : skolem = sm->mkPurifySkolem(node);
361 : 2624 : d_skolem_cache.insert(node, skolem);
362 : 2624 : d_env.registerBooleanTermSkolem(skolem);
363 : :
364 : : // The new assertion
365 : 2624 : newAssertion = skolem.eqNode(node);
366 : :
367 : : // Boolean term removal is trivial to justify, hence we don't set a
368 : : // proof generator here. It is trivial to justify since it is an
369 : : // instance of purification, which is justified by conversion to witness
370 : : // forms.
371 : : }
372 : : }
373 : :
374 : : // if the term should be replaced by a skolem
375 [ + + ]: 5428390 : if( !skolem.isNull() ){
376 : : // this must be done regardless of whether the assertion was new below,
377 : : // since a formula-term may rewrite to the same skolem in multiple contexts.
378 [ + + ]: 43898 : if (isProofEnabled())
379 : : {
380 : : // justify the introduction of the skolem
381 : : // ------------------- MACRO_SR_PRED_INTRO
382 : : // t = witness x. x=t
383 : : // The above step is trivial, since the skolems introduced above are
384 : : // all purification skolems. We record this equality in the term
385 : : // conversion proof generator.
386 : 56272 : pg->addRewriteStep(node,
387 : : skolem,
388 : : ProofRule::MACRO_SR_PRED_INTRO,
389 : : {},
390 : : {node.eqNode(skolem)},
391 : : true,
392 : 28136 : cval);
393 : : }
394 : :
395 : : // if the skolem was introduced in this call
396 [ + + ]: 43898 : if (!newAssertion.isNull())
397 : : {
398 [ + - ]: 76706 : Trace("rtf-proof-debug")
399 : 0 : << "RemoveTermFormulas::run: setup proof for new assertion "
400 : 38353 : << newAssertion << std::endl;
401 : : // if proofs are enabled
402 [ + + ]: 38353 : if (isProofEnabled())
403 : : {
404 : : // justify the axiom that defines the skolem, if not already done so
405 [ + + ]: 24817 : if (newAssertionPg == nullptr)
406 : : {
407 : : // Should have trivial justification if not yet provided. This is the
408 : : // case of lambda lifting and Boolean term removal.
409 : : // ---------------- MACRO_SR_PRED_INTRO
410 : : // newAssertion
411 : 1928 : d_lp->addStep(
412 : 964 : newAssertion, ProofRule::MACRO_SR_PRED_INTRO, {}, {newAssertion});
413 : : }
414 : : }
415 [ + - ]: 76706 : Trace("rtf-debug") << "*** term formula removal introduced " << skolem
416 : 38353 : << " for " << node << std::endl;
417 : :
418 [ + + ]: 38353 : newLem = TrustNode::mkTrustLemma(newAssertion, d_lp.get());
419 : :
420 [ + - ]: 38353 : Trace("rtf-proof-debug") << "Checking closed..." << std::endl;
421 : 38353 : newLem.debugCheckClosed(
422 : : options(), "rtf-proof-debug", "RemoveTermFormulas::run:new_assert");
423 : : }
424 : :
425 : : // The representation is now the skolem
426 : 43898 : return skolem;
427 : : }
428 : :
429 : : // return null, indicating we will traverse children within runInternal
430 : 5384500 : return Node::null();
431 : : }
432 : :
433 : 43898 : Node RemoveTermFormulas::getSkolemForNode(Node k) const
434 : : {
435 : : context::CDInsertHashMap<Node, Node>::const_iterator itk =
436 : 43898 : d_skolem_cache.find(k);
437 [ + + ]: 43898 : if (itk != d_skolem_cache.end())
438 : : {
439 : 5545 : return itk->second;
440 : : }
441 : 38353 : return Node::null();
442 : : }
443 : :
444 : 31686 : Node RemoveTermFormulas::getAxiomFor(Node n)
445 : : {
446 : 31686 : Kind k = n.getKind();
447 [ + - ]: 31686 : if (k == Kind::ITE)
448 : : {
449 : 31686 : return NodeManager::mkNode(Kind::ITE, n[0], n.eqNode(n[1]), n.eqNode(n[2]));
450 : : }
451 : 0 : return Node::null();
452 : : }
453 : :
454 : 0 : ProofGenerator* RemoveTermFormulas::getTConvProofGenerator()
455 : : {
456 [ - - ]: 0 : return d_tpg.get();
457 : : }
458 : :
459 : 117980 : bool RemoveTermFormulas::isProofEnabled() const { return d_tpg != nullptr; }
460 : :
461 : : } // namespace cvc5::internal
|
