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