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 : : * Implementation of theory proof step buffer utility.
11 : : */
12 : :
13 : : #include "proof/theory_proof_step_buffer.h"
14 : :
15 : : #include "proof/proof.h"
16 : : #include "proof/proof_node_algorithm.h"
17 : :
18 : : using namespace cvc5::internal::kind;
19 : :
20 : : namespace cvc5::internal {
21 : :
22 : 3883167 : TheoryProofStepBuffer::TheoryProofStepBuffer(ProofChecker* pc,
23 : : bool ensureUnique,
24 : 3883167 : bool autoSym)
25 : 3883167 : : ProofStepBuffer(pc, ensureUnique, autoSym)
26 : : {
27 : 3883167 : }
28 : :
29 : 45260 : bool TheoryProofStepBuffer::applyEqIntro(Node src,
30 : : Node tgt,
31 : : const std::vector<Node>& exp,
32 : : MethodId ids,
33 : : MethodId ida,
34 : : MethodId idr,
35 : : bool useExpected)
36 : : {
37 : 45260 : std::vector<Node> args;
38 : 45260 : args.push_back(src);
39 : 45260 : addMethodIds(src.getNodeManager(), args, ids, ida, idr);
40 : : bool added;
41 : 45260 : Node expected = src.eqNode(tgt);
42 : : Node res = tryStep(added,
43 : : ProofRule::MACRO_SR_EQ_INTRO,
44 : : exp,
45 : : args,
46 [ + - ]: 45260 : useExpected ? expected : Node::null());
47 [ - + ]: 45260 : if (res.isNull())
48 : : {
49 : : // failed to apply
50 : 0 : return false;
51 : : }
52 : : // should have concluded the expected equality
53 [ - + ]: 45260 : if (res != expected)
54 : : {
55 : : // did not provide the correct target
56 [ - - ]: 0 : if (added)
57 : : {
58 : 0 : popStep();
59 : : }
60 : 0 : return false;
61 : : }
62 : : // successfully proved src == tgt.
63 : 45260 : return true;
64 : 45260 : }
65 : :
66 : 14629 : bool TheoryProofStepBuffer::applyPredTransform(Node src,
67 : : Node tgt,
68 : : const std::vector<Node>& exp,
69 : : MethodId ids,
70 : : MethodId ida,
71 : : MethodId idr,
72 : : bool useExpected)
73 : : {
74 : : // symmetric equalities
75 : 14629 : if (d_autoSym && CDProof::isSame(src, tgt))
76 : : {
77 : 5325 : return true;
78 : : }
79 : 9304 : std::vector<Node> children;
80 : 9304 : children.push_back(src);
81 : 9304 : std::vector<Node> args;
82 : : // try to prove that tgt rewrites to src
83 : 9304 : children.insert(children.end(), exp.begin(), exp.end());
84 : 9304 : args.push_back(tgt);
85 : 9304 : addMethodIds(src.getNodeManager(), args, ids, ida, idr);
86 : : Node res = tryStep(ProofRule::MACRO_SR_PRED_TRANSFORM,
87 : : children,
88 : : args,
89 [ - + ]: 9304 : useExpected ? tgt : Node::null());
90 [ + + ]: 9304 : if (res.isNull())
91 : : {
92 : : // failed to apply
93 : 1219 : return false;
94 : : }
95 : : // should definitely have concluded tgt
96 [ - + ][ - + ]: 8085 : Assert(res == tgt);
[ - - ]
97 : 8085 : return true;
98 : 9304 : }
99 : :
100 : 23069 : bool TheoryProofStepBuffer::applyPredIntro(Node tgt,
101 : : const std::vector<Node>& exp,
102 : : MethodId ids,
103 : : MethodId ida,
104 : : MethodId idr,
105 : : bool useExpected)
106 : : {
107 : 23069 : std::vector<Node> args;
108 : 23069 : args.push_back(tgt);
109 : 23069 : addMethodIds(tgt.getNodeManager(), args, ids, ida, idr);
110 : : Node res = tryStep(ProofRule::MACRO_SR_PRED_INTRO,
111 : : exp,
112 : : args,
113 [ - + ]: 23069 : useExpected ? tgt : Node::null());
114 [ + + ]: 23069 : if (res.isNull())
115 : : {
116 : 18792 : return false;
117 : : }
118 [ - + ][ - + ]: 4277 : Assert(res == tgt);
[ - - ]
119 : 4277 : return true;
120 : 23069 : }
121 : :
122 : 5179 : Node TheoryProofStepBuffer::applyPredElim(Node src,
123 : : const std::vector<Node>& exp,
124 : : MethodId ids,
125 : : MethodId ida,
126 : : MethodId idr)
127 : : {
128 : 5179 : std::vector<Node> children;
129 : 5179 : children.push_back(src);
130 : 5179 : children.insert(children.end(), exp.begin(), exp.end());
131 : 5179 : std::vector<Node> args;
132 : 5179 : addMethodIds(src.getNodeManager(), args, ids, ida, idr);
133 : : bool added;
134 : 5179 : Node srcRew = tryStep(added, ProofRule::MACRO_SR_PRED_ELIM, children, args);
135 : 5179 : if (d_autoSym && added && CDProof::isSame(src, srcRew))
136 : : {
137 : 0 : popStep();
138 : : }
139 : 10358 : return srcRew;
140 : 5179 : }
141 : :
142 : 3809519 : Node TheoryProofStepBuffer::factorReorderElimDoubleNeg(Node n)
143 : : {
144 [ - + ]: 3809519 : if (n.getKind() != Kind::OR)
145 : : {
146 : 0 : return elimDoubleNegLit(n);
147 : : }
148 : 3809519 : NodeManager* nm = n.getNodeManager();
149 : 3809519 : std::vector<Node> children{n.begin(), n.end()};
150 : 3809519 : std::vector<Node> childrenEqs;
151 : : // eliminate double neg for each lit. Do it first because it may expose
152 : : // duplicates
153 : 3809519 : bool hasDoubleNeg = false;
154 [ + + ]: 15769330 : for (unsigned i = 0; i < children.size(); ++i)
155 : : {
156 : 11959811 : if (children[i].getKind() == Kind::NOT
157 [ + + ][ + + ]: 23919622 : && children[i][0].getKind() == Kind::NOT)
[ + + ][ + + ]
[ - - ]
158 : : {
159 : 743680 : hasDoubleNeg = true;
160 : 743680 : childrenEqs.push_back(children[i].eqNode(children[i][0][0]));
161 : 2231040 : addStep(ProofRule::MACRO_SR_PRED_INTRO,
162 : : {},
163 : 743680 : {childrenEqs.back()},
164 : 743680 : childrenEqs.back());
165 : : // update child
166 : 743680 : children[i] = children[i][0][0];
167 : : }
168 : : else
169 : : {
170 : 11216131 : childrenEqs.push_back(children[i].eqNode(children[i]));
171 : 22432262 : addStep(ProofRule::REFL, {}, {children[i]}, childrenEqs.back());
172 : : }
173 : : }
174 [ + + ]: 3809519 : if (hasDoubleNeg)
175 : : {
176 : 489649 : Node oldn = n;
177 : 489649 : n = nm->mkNode(Kind::OR, children);
178 : : // Create a congruence step to justify replacement of each doubly negated
179 : : // literal. This is done to avoid having to use MACRO_SR_PRED_TRANSFORM
180 : : // from the old clause to the new one, which, under the standard rewriter,
181 : : // may not hold. An example is
182 : : //
183 : : // ---------------------------------------------------------------------
184 : : // (or (or (not x2) x1 x2) (not (not x2))) = (or (or (not x2) x1 x2) x2)
185 : : //
186 : : // which fails due to factoring not happening after flattening.
187 : : //
188 : : // Using congruence only the
189 : : //
190 : : // ------------------ MACRO_SR_PRED_INTRO
191 : : // (not (not t)) = t
192 : : //
193 : : // steps are added, which, since double negation is eliminated in a
194 : : // pre-rewrite in the Boolean rewriter, will always hold under the
195 : : // standard rewriter.
196 : 489649 : std::vector<Node> cargs;
197 : 489649 : ProofRule cr = expr::getCongRule(oldn, cargs);
198 : 489649 : Node congEq = oldn.eqNode(n);
199 : 489649 : addStep(cr, childrenEqs, cargs, congEq);
200 : : // add an equality resolution step to derive normalize clause
201 [ + + ][ - - ]: 1468947 : addStep(ProofRule::EQ_RESOLVE, {oldn, congEq}, {}, n);
202 : 489649 : }
203 : 3809519 : children.clear();
204 : : // remove duplicates while keeping the order of children
205 : 3809519 : std::unordered_set<TNode> clauseSet;
206 : 3809519 : unsigned size = n.getNumChildren();
207 [ + + ]: 15769330 : for (unsigned i = 0; i < size; ++i)
208 : : {
209 [ + + ]: 11959811 : if (clauseSet.count(n[i]))
210 : : {
211 : 9347 : continue;
212 : : }
213 : 11950464 : children.push_back(n[i]);
214 : 11950464 : clauseSet.insert(n[i]);
215 : : }
216 : : // if factoring changed
217 [ + + ]: 3809519 : if (children.size() < size)
218 : : {
219 : 5785 : Node factored = children.empty() ? nm->mkConst<bool>(false)
220 : 5785 : : children.size() == 1 ? children[0]
221 [ - + ][ - + ]: 11570 : : nm->mkNode(Kind::OR, children);
222 : : // don't overwrite what already has a proof step to avoid cycles
223 : 11570 : addStep(ProofRule::FACTORING, {n}, {}, factored);
224 : 5785 : n = factored;
225 : 5785 : }
226 : : // nothing to order
227 [ - + ]: 3809519 : if (children.size() < 2)
228 : : {
229 : 0 : return n;
230 : : }
231 : : // order
232 : 3809519 : std::sort(children.begin(), children.end());
233 : 3809519 : Node ordered = nm->mkNode(Kind::OR, children);
234 : : // if ordering changed
235 [ + + ]: 3809519 : if (ordered != n)
236 : : {
237 : : // don't overwrite what already has a proof step to avoid cycles
238 : 8930403 : addStep(ProofRule::REORDERING, {n}, {ordered}, ordered);
239 : : }
240 : 3809519 : return ordered;
241 : 3809519 : }
242 : :
243 : 0 : Node TheoryProofStepBuffer::elimDoubleNegLit(Node n)
244 : : {
245 : : // eliminate double neg
246 : 0 : if (n.getKind() == Kind::NOT && n[0].getKind() == Kind::NOT)
247 : : {
248 : 0 : addStep(ProofRule::NOT_NOT_ELIM, {n}, {}, n[0][0]);
249 : 0 : return n[0][0];
250 : : }
251 : 0 : return n;
252 : : }
253 : :
254 : : } // namespace cvc5::internal
|
