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 : 51735 : RemoveTermFormulas::RemoveTermFormulas(Env& env)
31 : : : EnvObj(env),
32 : 51735 : d_tfCache(userContext()),
33 : 51735 : d_skolem_cache(userContext()),
34 : 51735 : d_tpg(nullptr),
35 : 103470 : d_lp(nullptr)
36 : : {
37 : : // enable proofs if necessary
38 : 51735 : ProofNodeManager* pnm = env.getProofNodeManager();
39 [ + + ]: 51735 : if (pnm != nullptr)
40 : : {
41 : 40074 : d_tpg.reset(
42 : : new TConvProofGenerator(env,
43 : : nullptr,
44 : : TConvPolicy::FIXPOINT,
45 : : TConvCachePolicy::NEVER,
46 : : "RemoveTermFormulas::TConvProofGenerator",
47 : 20037 : &d_rtfc));
48 : 40074 : d_tpgi.reset(
49 : : new TConvProofGenerator(env,
50 : : nullptr,
51 : : TConvPolicy::ONCE,
52 : : TConvCachePolicy::NEVER,
53 : 20037 : "RemoveTermFormulas::TConvProofGenerator"));
54 : 40074 : d_lp.reset(new LazyCDProof(
55 : 20037 : env, nullptr, nullptr, "RemoveTermFormulas::LazyCDProof"));
56 : : }
57 : 51735 : }
58 : :
59 : 51390 : 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 : 5547681 : 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 : 5547683 : Node k = runCurrentInternal(node, inTerm, newLem, 0, d_tpgi.get());
257 [ + + ]: 5547679 : if (!k.isNull())
258 : : {
259 [ + + ]: 52991 : return TrustNode::mkTrustRewrite(node, k, d_tpgi.get());
260 : : }
261 : 5494688 : return TrustNode::null();
262 : 5547679 : }
263 : :
264 : 5559366 : Node RemoveTermFormulas::runCurrentInternal(TNode node,
265 : : bool inTerm,
266 : : TrustNode& newLem,
267 : : uint32_t cval,
268 : : TConvProofGenerator* pg)
269 : : {
270 [ - + ][ - + ]: 5559366 : AlwaysAssert (node.getKind()!=Kind::WITNESS) << "WITNESS should never appear in asserted terms";
[ - - ]
271 : 5559366 : SkolemManager* sm = nodeManager()->getSkolemManager();
272 : :
273 : 5559366 : TypeNode nodeType = node.getType();
274 : 5559366 : Node skolem;
275 : 5559366 : Node newAssertion;
276 : : // the exists form of the assertion
277 : 5559366 : ProofGenerator* newAssertionPg = nullptr;
278 : : // Handle non-Boolean ITEs here. Boolean ones (within terms) are handled
279 : : // in the "non-variable Boolean term within term" case below.
280 [ + + ][ + + ]: 5559366 : if (node.getKind() == Kind::ITE && !nodeType.isBoolean())
[ + + ]
281 : : {
282 [ + + ]: 49967 : if (!d_env.isFirstClassType(nodeType))
283 : : {
284 : 2 : std::stringstream ss;
285 : 2 : ss << "ITE branches of type " << nodeType
286 : 2 : << " are currently not supported." << std::endl;
287 : 2 : throw LogicException(ss.str());
288 : 2 : }
289 : : // Here, we eliminate the ITE if we are not Boolean and if we are
290 : : // not in a quantified formula. This policy should be in sync with
291 : : // the policy for when to apply theory preprocessing to terms, see PR
292 : : // #5497.
293 : 49965 : skolem = getSkolemForNode(node);
294 [ + + ]: 49965 : if (skolem.isNull())
295 : : {
296 [ + - ]: 87894 : Trace("rtf-proof-debug")
297 : 43947 : << "RemoveTermFormulas::run: make ITE skolem" << std::endl;
298 : : // Make the skolem to represent the ITE
299 : 43947 : skolem = sm->mkPurifySkolem(node);
300 : 43947 : d_skolem_cache.insert(node, skolem);
301 : :
302 : : // Notice that in very rare cases, two different terms may have the
303 : : // same purification skolem (see SkolemManager::mkPurifySkolem) For such
304 : : // cases, for simplicity, we repeat the work of constructing the
305 : : // assertion and proofs below. This is so that the proof for the new form
306 : : // of the lemma is used.
307 : :
308 : : // The new assertion
309 : 43947 : newAssertion = nodeManager()->mkNode(
310 : 43947 : Kind::ITE, node[0], skolem.eqNode(node[1]), skolem.eqNode(node[2]));
311 : :
312 : : // we justify it internally
313 [ + + ]: 43947 : if (isProofEnabled())
314 : : {
315 [ + - ]: 56618 : Trace("rtf-proof-debug")
316 : 0 : << "RemoveTermFormulas::run: justify " << newAssertion
317 : 28309 : << " with ITE axiom" << std::endl;
318 : : // ---------------------- ITE_EQ
319 : : // (ite node[0]
320 : : // (= node node[1]) ------------- MACRO_SR_PRED_INTRO
321 : : // (= node node[2])) node = skolem
322 : : // ------------------------------------------ MACRO_SR_PRED_TRANSFORM
323 : : // (ite node[0] (= skolem node[1]) (= skolem node[2]))
324 : : //
325 : : // Note that the MACRO_SR_PRED_INTRO step holds due to conversion
326 : : // of skolem into its witness form, which is node.
327 : 28309 : Node axiom = getAxiomFor(node);
328 : 56618 : d_lp->addStep(axiom, ProofRule::ITE_EQ, {}, {node});
329 : 28309 : Node eq = node.eqNode(skolem);
330 : 56618 : d_lp->addStep(eq, ProofRule::MACRO_SR_PRED_INTRO, {}, {eq});
331 : 113236 : d_lp->addStep(newAssertion,
332 : : ProofRule::MACRO_SR_PRED_TRANSFORM,
333 : : {axiom, eq},
334 : : {newAssertion});
335 [ + - ]: 28309 : newAssertionPg = d_lp.get();
336 : 28309 : }
337 : : }
338 : : }
339 [ + + ][ + + ]: 5509399 : else if (nodeType.isBoolean() && inTerm && !d_env.isBooleanTermSkolem(node))
[ + + ][ + + ]
[ + + ][ - - ]
340 : : {
341 : : // if a purification skolem already, just use itself
342 [ + + ]: 3481 : if (sm->getId(node) == SkolemId::PURIFY)
343 : : {
344 : 47 : d_env.registerBooleanTermSkolem(node);
345 : 47 : return Node::null();
346 : : }
347 : : // if a non-variable Boolean term within another term, replace it
348 : 3434 : skolem = getSkolemForNode(node);
349 [ + - ]: 3434 : if (skolem.isNull())
350 : : {
351 [ + - ]: 6868 : Trace("rtf-proof-debug")
352 : 3434 : << "RemoveTermFormulas::run: make Boolean skolem" << std::endl;
353 : : // Make the skolem to represent the Boolean term
354 : : // Skolems introduced for Boolean formulas appearing in terms are
355 : : // purified here (SkolemId::PURIFY), which ensures they are handled
356 : : // properly in theory combination.
357 : 3434 : skolem = sm->mkPurifySkolem(node);
358 : 3434 : d_skolem_cache.insert(node, skolem);
359 : 3434 : d_env.registerBooleanTermSkolem(skolem);
360 : :
361 : : // The new assertion
362 : 3434 : newAssertion = skolem.eqNode(node);
363 : :
364 : : // Boolean term removal is trivial to justify, hence we don't set a
365 : : // proof generator here. It is trivial to justify since it is an
366 : : // instance of purification, which is justified by conversion to witness
367 : : // forms.
368 : : }
369 : : }
370 : :
371 : : // if the term should be replaced by a skolem
372 [ + + ]: 5559317 : if( !skolem.isNull() ){
373 : : // this must be done regardless of whether the assertion was new below,
374 : : // since a formula-term may rewrite to the same skolem in multiple contexts.
375 [ + + ]: 53399 : if (isProofEnabled())
376 : : {
377 : : // justify the introduction of the skolem
378 : : // ------------------- MACRO_SR_PRED_INTRO
379 : : // t = witness x. x=t
380 : : // The above step is trivial, since the skolems introduced above are
381 : : // all purification skolems. We record this equality in the term
382 : : // conversion proof generator.
383 : 66828 : pg->addRewriteStep(node,
384 : : skolem,
385 : : ProofRule::MACRO_SR_PRED_INTRO,
386 : : {},
387 : : {node.eqNode(skolem)},
388 : : true,
389 : : cval);
390 : : }
391 : :
392 : : // if the skolem was introduced in this call
393 [ + + ]: 53399 : if (!newAssertion.isNull())
394 : : {
395 [ + - ]: 94762 : Trace("rtf-proof-debug")
396 : 0 : << "RemoveTermFormulas::run: setup proof for new assertion "
397 : 47381 : << newAssertion << std::endl;
398 : : // if proofs are enabled
399 [ + + ]: 47381 : if (isProofEnabled())
400 : : {
401 : : // justify the axiom that defines the skolem, if not already done so
402 [ + + ]: 29677 : if (newAssertionPg == nullptr)
403 : : {
404 : : // Should have trivial justification if not yet provided. This is the
405 : : // case of lambda lifting and Boolean term removal.
406 : : // ---------------- MACRO_SR_PRED_INTRO
407 : : // newAssertion
408 : 2736 : d_lp->addStep(
409 : : newAssertion, ProofRule::MACRO_SR_PRED_INTRO, {}, {newAssertion});
410 : : }
411 : : }
412 [ + - ]: 94762 : Trace("rtf-debug") << "*** term formula removal introduced " << skolem
413 : 47381 : << " for " << node << std::endl;
414 : :
415 [ + + ]: 47381 : newLem = TrustNode::mkTrustLemma(newAssertion, d_lp.get());
416 : :
417 [ + - ]: 47381 : Trace("rtf-proof-debug") << "Checking closed..." << std::endl;
418 : 47381 : newLem.debugCheckClosed(
419 : : options(), "rtf-proof-debug", "RemoveTermFormulas::run:new_assert");
420 : : }
421 : :
422 : : // The representation is now the skolem
423 : 53399 : return skolem;
424 : : }
425 : :
426 : : // return null, indicating we will traverse children within runInternal
427 : 5505918 : return Node::null();
428 : 5559370 : }
429 : :
430 : 53399 : Node RemoveTermFormulas::getSkolemForNode(Node k) const
431 : : {
432 : : context::CDInsertHashMap<Node, Node>::const_iterator itk =
433 : 53399 : d_skolem_cache.find(k);
434 [ + + ]: 53399 : if (itk != d_skolem_cache.end())
435 : : {
436 : 6018 : return itk->second;
437 : : }
438 : 47381 : return Node::null();
439 : : }
440 : :
441 : 33708 : Node RemoveTermFormulas::getAxiomFor(Node n)
442 : : {
443 : 33708 : Kind k = n.getKind();
444 [ + - ]: 33708 : if (k == Kind::ITE)
445 : : {
446 : 33708 : return NodeManager::mkNode(Kind::ITE, n[0], n.eqNode(n[1]), n.eqNode(n[2]));
447 : : }
448 : 0 : return Node::null();
449 : : }
450 : :
451 : 0 : ProofGenerator* RemoveTermFormulas::getTConvProofGenerator()
452 : : {
453 [ - - ]: 0 : return d_tpg.get();
454 : : }
455 : :
456 : 144727 : bool RemoveTermFormulas::isProofEnabled() const { return d_tpg != nullptr; }
457 : :
458 : : } // namespace cvc5::internal
|
