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