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 : : * Inference to proof conversion for sets.
11 : : */
12 : :
13 : : #include "theory/sets/infer_proof_cons.h"
14 : :
15 : : #include "expr/skolem_manager.h"
16 : : #include "proof/proof_node_algorithm.h"
17 : : #include "proof/proof_node_manager.h"
18 : : #include "proof/theory_proof_step_buffer.h"
19 : : #include "theory/builtin/proof_checker.h"
20 : : #include "theory/sets/theory_sets_rewriter.h"
21 : :
22 : : namespace cvc5::internal {
23 : : namespace theory {
24 : : namespace sets {
25 : :
26 : 10177 : InferProofCons::InferProofCons(Env& env, TheorySetsRewriter* tsr)
27 : : : EnvObj(env),
28 : 10177 : d_tsr(tsr),
29 : 10177 : d_uimap(userContext()),
30 : 10177 : d_fmap(context()),
31 : 20354 : d_expMap(context())
32 : : {
33 : 10177 : d_false = nodeManager()->mkConst(false);
34 : 10177 : }
35 : :
36 : 3646 : void InferProofCons::notifyFact(const Node& conc,
37 : : const Node& exp,
38 : : InferenceId id)
39 : : {
40 [ + - ][ + - ]: 3646 : Assert(conc.getKind() != Kind::AND && conc.getKind() != Kind::IMPLIES);
[ - + ][ - + ]
[ - - ]
41 [ + + ]: 3646 : if (d_fmap.find(conc) != d_fmap.end())
42 : : {
43 : : // already exists, redundant
44 : 367 : return;
45 : : }
46 : 3279 : d_fmap[conc] = id;
47 : 3279 : d_expMap[conc] = exp;
48 : : }
49 : :
50 : 309 : void InferProofCons::notifyConflict(const Node& conf, InferenceId id)
51 : : {
52 [ + - ]: 618 : Trace("sets-ipc-debug") << "SetsIpc::conflict " << conf << " " << id
53 : 309 : << std::endl;
54 : 309 : d_uimap[conf.notNode()] = id;
55 : 309 : }
56 : :
57 : 23003 : void InferProofCons::notifyLemma(const Node& lem, InferenceId id)
58 : : {
59 [ + - ]: 23003 : Trace("sets-ipc-debug") << "SetsIpc::lemma " << lem << " " << id << std::endl;
60 : 23003 : d_uimap[lem] = id;
61 : 23003 : }
62 : :
63 : 1952 : std::shared_ptr<ProofNode> InferProofCons::getProofFor(Node fact)
64 : : {
65 : 1952 : NodeInferenceMap::iterator it = d_uimap.find(fact);
66 [ + + ]: 1952 : if (it == d_uimap.end())
67 : : {
68 : : // should be a fact
69 : 179 : it = d_fmap.find(fact);
70 [ - + ][ - + ]: 179 : Assert(it != d_fmap.end());
[ - - ]
71 : : }
72 : 1952 : InferenceId id = it->second;
73 : :
74 : : // temporary proof
75 : 3904 : CDProof cdp(d_env);
76 : 1952 : std::vector<Node> assumps;
77 : 1952 : Node conc = fact;
78 : : // First split into conclusion and assumptions.
79 [ + + ][ + + ]: 1952 : if (fact.getKind() == Kind::IMPLIES || fact.getKind() == Kind::NOT)
[ + + ]
80 : : {
81 [ + + ]: 1209 : if (fact[0].getKind() == Kind::AND)
82 : : {
83 : 753 : assumps.insert(assumps.begin(), fact[0].begin(), fact[0].end());
84 : : }
85 : : else
86 : : {
87 : 456 : assumps.push_back(fact[0]);
88 : : }
89 [ + + ]: 1209 : if (fact.getKind() == Kind::IMPLIES)
90 : : {
91 : 1072 : conc = fact[1];
92 : : }
93 : : else
94 : : {
95 : 137 : conc = d_false;
96 : : }
97 : 2418 : cdp.addStep(fact, ProofRule::SCOPE, {conc}, {assumps});
98 : : }
99 : : else
100 : : {
101 : : // should be a fact
102 : 743 : NodeExpMap::iterator itex = d_expMap.find(fact);
103 [ + + ]: 743 : if (itex != d_expMap.end())
104 : : {
105 : 179 : Node exp = itex->second;
106 [ + + ]: 179 : if (exp.getKind() == Kind::AND)
107 : : {
108 : 147 : assumps.insert(assumps.end(), exp.begin(), exp.end());
109 : : }
110 : : else
111 : : {
112 : 32 : assumps.push_back(exp);
113 : : }
114 : 179 : }
115 : : }
116 : : // Try to convert.
117 [ + + ]: 1952 : if (!convert(cdp, id, assumps, conc))
118 : : {
119 : 867 : cdp.addTrustedStep(conc, TrustId::THEORY_INFERENCE_SETS, assumps, {});
120 : : }
121 : 3904 : return cdp.getProofFor(fact);
122 : 1952 : }
123 : :
124 : 1952 : bool InferProofCons::convert(CDProof& cdp,
125 : : InferenceId id,
126 : : const std::vector<Node>& assumps,
127 : : const Node& conc)
128 : : {
129 : : // these are handled manually
130 [ + - ][ + - ]: 1952 : Assert(id != InferenceId::SETS_PROXY
[ - + ][ - + ]
[ - - ]
131 : : && id != InferenceId::SETS_PROXY_SINGLETON);
132 [ + - ]: 1952 : Trace("sets-ipc") << "InferProofCons::convert " << id << std::endl;
133 [ + - ]: 1952 : Trace("sets-ipc") << "- assumptions: " << assumps << std::endl;
134 [ + - ]: 1952 : Trace("sets-ipc") << "- conclusion: " << conc << std::endl;
135 : 1952 : bool success = false;
136 : 1952 : TheoryProofStepBuffer psb(cdp.getManager()->getChecker(), true);
137 [ + + ][ + + ]: 1952 : switch (id)
[ + + ][ + + ]
138 : : {
139 : 364 : case InferenceId::SETS_DOWN_CLOSURE:
140 : : case InferenceId::SETS_MEM_EQ:
141 : : case InferenceId::SETS_MEM_EQ_CONFLICT:
142 : : {
143 [ - + ][ - + ]: 364 : Assert(assumps.size() >= 1);
[ - - ]
144 [ - + ][ - + ]: 364 : Assert(assumps[0].getKind() == Kind::SET_MEMBER);
[ - - ]
145 [ + - ][ + - ]: 364 : Assert(assumps.size() == 1 || assumps[1].getKind() == Kind::EQUAL);
[ - + ][ - + ]
[ - - ]
146 : : // (and (set.member x S) (= S (op T1 T2))) =>
147 : : // rewrite((set.member x (op T1 T2)))
148 : : // this holds by applying the equality as a substitution to the first
149 : : // assumption and rewriting.
150 : 364 : std::vector<Node> exp(assumps.begin() + 1, assumps.end());
151 : 364 : Node aelim = psb.applyPredElim(assumps[0], exp);
152 : 364 : success = true;
153 [ + + ]: 364 : if (!CDProof::isSame(aelim, conc))
154 : : {
155 : 11 : success = psb.applyPredTransform(aelim, conc, {});
156 : : }
157 : : // should never fail
158 [ - + ][ - + ]: 364 : Assert(success);
[ - - ]
159 : 364 : }
160 : 364 : break;
161 : 386 : case InferenceId::SETS_UP_CLOSURE:
162 : : case InferenceId::SETS_UP_CLOSURE_2:
163 : : {
164 : 386 : NodeManager* nm = nodeManager();
165 : : // An example inference is:
166 : : // (set.member x A) ^ (set.member y B) ^ (= x y) => (set.member x k)
167 : : // where k is the purification skolem for (set.inter A B).
168 [ - + ][ - + ]: 386 : Assert(conc.getKind() == Kind::SET_MEMBER);
[ - - ]
169 : 386 : Node so = SkolemManager::getUnpurifiedForm(conc[1]);
170 [ + - ]: 386 : Trace("sets-ipc") << "Unpurified form " << so << std::endl;
171 : : // We first compute the single step rewriting of the conclusion.
172 : : // For the above example, memor would be:
173 : : // (and (set.member x A) (set.member x B)).
174 : 772 : Node memo = nm->mkNode(Kind::SET_MEMBER, conc[0], so);
175 : 386 : Node memor = d_tsr->rewriteMembershipBinaryOp(memo);
176 [ + - ]: 772 : Trace("sets-ipc") << "Single step rewriting of membership " << memor
177 : 386 : << std::endl;
178 [ - + ][ - + ]: 386 : Assert(memo != memor);
[ - - ]
179 : : // collect the memberships in the premise
180 : 386 : std::vector<Node> assumpMem;
181 : 386 : std::vector<Node> assumpOther;
182 : : // We now partition the antecedant to the membership
183 : : // part (assumpMem) and the substitution part (assumpOther). The
184 : : // membership part will be equivalent via rewriting to the conclusion.
185 [ + + ]: 1225 : for (const Node& a : assumps)
186 : : {
187 [ + + ]: 839 : Node aa = a.getKind() == Kind::NOT ? a[0] : a;
188 [ + + ]: 839 : if (aa.getKind() == Kind::SET_MEMBER)
189 : : {
190 : 599 : assumpMem.push_back(a);
191 : : }
192 : : else
193 : : {
194 : 240 : assumpOther.push_back(a);
195 : : }
196 : 839 : }
197 [ + + ][ + - ]: 386 : Assert(assumpMem.size() == 1 || assumpMem.size() == 2);
[ - + ][ - + ]
[ - - ]
198 : 386 : Node msrc;
199 : : // Use AND_INTRO to put the memberships together if necessary.
200 [ + + ]: 386 : if (assumpMem.size() == 2)
201 : : {
202 : 213 : msrc = nm->mkAnd(assumpMem);
203 : 213 : psb.addStep(ProofRule::AND_INTRO, {assumpMem}, {}, msrc);
204 : : }
205 : : else
206 : : {
207 : 173 : msrc = assumpMem[0];
208 : : }
209 : : // Now, prove the equivalence between the memberships and the
210 : : // conclusion, possibly using the substituion in assumpOther.
211 : 386 : bool isOr = (memor.getKind() == Kind::OR);
212 [ + + ]: 386 : size_t ntgts = isOr ? 2 : 1;
213 [ + - ]: 477 : for (size_t i = 0; i < ntgts; i++)
214 : : {
215 [ + + ]: 477 : Node mtgt = isOr ? memor[i] : memor;
216 [ + - ]: 477 : Trace("sets-ipc") << "...try target " << mtgt << std::endl;
217 [ + + ]: 477 : if (psb.applyPredTransform(msrc, mtgt, assumpOther))
218 : : {
219 : 386 : success = true;
220 [ + + ]: 386 : if (isOr)
221 : : {
222 : : // if union, we get the desired (left or right) conclusion
223 : 346 : success = psb.applyPredIntro(memor, {mtgt}, MethodId::SB_FORMULA);
224 : : // should never fail
225 [ - + ][ - + ]: 173 : Assert(success);
[ - - ]
226 : : }
227 [ + - ]: 386 : Trace("sets-ipc") << "......success" << std::endl;
228 : 386 : break;
229 : : }
230 [ + + ]: 477 : }
231 : : // If successful, we have proven:
232 : : //
233 : : // (set.member x A) (set.member y B)
234 : : // --------------------------------------- AND_INTRO
235 : : // (and (set.member x A) (set.member y B)) (= x y)
236 : : // ------------------------------------------------- MACRO_SR_PRED_TRANS
237 : : // (set.member x (set.inter A B))
238 [ - + ]: 386 : if (!success)
239 : : {
240 : 0 : Assert(success);
241 : 0 : break;
242 : : }
243 : : // If successful, go back and show memor holds.
244 [ + - ]: 772 : Trace("sets-ipc") << "* Prove transform " << memor << " to " << memo
245 : 386 : << std::endl;
246 [ - + ]: 386 : if (!psb.applyPredTransform(memor, memo, {}))
247 : : {
248 : : // should never fail
249 : 0 : success = false;
250 : 0 : Assert(success);
251 : 0 : break;
252 : : }
253 [ + - ]: 386 : if (so != conc[1])
254 : : {
255 : 386 : std::vector<Node> ceqs;
256 : 772 : Node ceq = conc[0].eqNode(conc[0]);
257 : 772 : psb.addStep(ProofRule::REFL, {}, {conc[0]}, ceq);
258 : 386 : ceqs.push_back(ceq);
259 : 386 : ceq = so.eqNode(conc[1]);
260 [ + - ]: 772 : Trace("sets-ipc") << "* Prove equal (by original forms) " << ceq
261 : 386 : << std::endl;
262 [ + + ][ - + ]: 772 : if (!psb.addStep(ProofRule::MACRO_SR_PRED_INTRO, {}, {ceq}, ceq))
[ - - ]
263 : : {
264 : : // should never fail
265 : 0 : success = false;
266 : 0 : Assert(success);
267 : 0 : break;
268 : : }
269 : 386 : ceqs.push_back(ceq);
270 : 386 : std::vector<Node> cargs;
271 : 386 : Node cequiv = memo.eqNode(conc);
272 : 386 : ProofRule cr = expr::getCongRule(memo, cargs);
273 [ - + ]: 386 : if (!psb.addStep(cr, ceqs, cargs, cequiv))
274 : : {
275 : : // should never fail
276 : 0 : success = false;
277 : 0 : Assert(success);
278 : 0 : break;
279 : : }
280 [ + + ][ - + ]: 1158 : if (!psb.addStep(ProofRule::EQ_RESOLVE, {memo, cequiv}, {}, conc))
[ - - ]
281 : : {
282 : : // should never fail
283 : 0 : success = false;
284 : 0 : Assert(success);
285 : 0 : break;
286 : : }
287 [ + - ][ + - ]: 386 : }
[ + - ][ + - ]
288 : : // Final proof now is,using A^B as shorthand for (set.inter A B):
289 : : //
290 : : // ----- REFL ---------- MACRO_SR_PRED_INTRO
291 : : // ... x = x A^B = k
292 : : // ------------------ -------------------------------------- CONG
293 : : // (set.member x A^B) (set.member x A^B) = (set.member x k)
294 : : // --------------------------------------------------------- EQ_RESOLVE
295 : : // (set.member x k)
296 : : //
297 : : // where ... is the proof from above.
298 [ + - ][ + - ]: 386 : }
[ + - ][ + - ]
[ + - ][ + - ]
299 : 386 : break;
300 : 36 : case InferenceId::SETS_SKOLEM:
301 : : {
302 [ - + ][ - + ]: 36 : Assert(assumps.empty());
[ - - ]
303 : 36 : success = psb.applyPredIntro(conc, {});
304 [ - + ][ - + ]: 36 : Assert(success);
[ - - ]
305 : : }
306 : 36 : break;
307 : 158 : case InferenceId::SETS_DEQ:
308 : : {
309 [ - + ][ - + ]: 158 : Assert(assumps.size() == 1);
[ - - ]
310 : 158 : Node exp = assumps[0];
311 : : // ensure we are properly ordered
312 : 158 : Assert(exp.getKind() == Kind::NOT && exp[0].getKind() == Kind::EQUAL
313 : : && exp[0][0] < exp[0][1]);
314 : 632 : Node res = psb.tryStep(ProofRule::SETS_EXT, {exp}, {}, conc);
315 : 158 : success = CDProof::isSame(res, conc);
316 [ - + ][ - + ]: 158 : Assert(success);
[ - - ]
317 : 158 : }
318 : 158 : break;
319 : 32 : case InferenceId::SETS_SINGLETON_EQ:
320 : : {
321 : : // SINGLETON_INJ
322 [ - + ][ - + ]: 32 : Assert(assumps.size() == 1);
[ - - ]
323 : : Node res =
324 : 128 : psb.tryStep(ProofRule::SETS_SINGLETON_INJ, {assumps[0]}, {}, conc);
325 : 32 : success = CDProof::isSame(res, conc);
326 [ - + ][ - + ]: 32 : Assert(success);
[ - - ]
327 : 32 : }
328 : 32 : break;
329 : 24 : case InferenceId::SETS_FILTER_UP:
330 : : case InferenceId::SETS_FILTER_DOWN:
331 : : {
332 : 24 : Node mem = assumps[0];
333 [ + + ]: 24 : if (assumps.size() == 2)
334 : : {
335 : : // Transform based on the second equality A = B:
336 : : //
337 : : // ------ REFL
338 : : // x = x A = B
339 : : // ----------------------------------- CONG
340 : : // (set.member x A) (set.member x A) = (set.member x B)
341 : : // ---------------------------------------------------- EQ_RESOLVE
342 : : // (set.member x B)
343 [ - + ][ - + ]: 8 : Assert(assumps[0].getKind() == Kind::SET_MEMBER);
[ - - ]
344 [ - + ][ - + ]: 8 : Assert(assumps[1].getKind() == Kind::EQUAL);
[ - - ]
345 : 32 : Node refl = psb.tryStep(ProofRule::REFL, {}, {assumps[0][0]});
346 : 8 : std::vector<Node> cargs;
347 : 8 : ProofRule cr = expr::getCongRule(assumps[0], cargs);
348 : 8 : Node aeq = assumps[1];
349 [ + - ]: 8 : if (aeq[1] == assumps[0][1])
350 : : {
351 : : // flip?
352 : 8 : aeq = aeq[1].eqNode(aeq[0]);
353 : 16 : psb.tryStep(ProofRule::SYMM, {assumps[1]}, {});
354 : : }
355 : 40 : Node eq = psb.tryStep(cr, {refl, aeq}, cargs);
356 [ + - ]: 16 : Trace("sets-ipc") << "...via CONG is " << eq << ", now try with " << mem
357 : 8 : << std::endl;
358 [ + + ][ - - ]: 24 : mem = psb.tryStep(ProofRule::EQ_RESOLVE, {mem, eq}, {});
359 [ - + ][ - + ]: 8 : Assert(!mem.isNull());
[ - - ]
360 : 8 : }
361 : 48 : ProofRule pr = (id == InferenceId::SETS_FILTER_UP)
362 [ + + ]: 24 : ? ProofRule::SETS_FILTER_UP
363 : : : ProofRule::SETS_FILTER_DOWN;
364 : 24 : std::vector<Node> pfArgs;
365 [ + + ]: 24 : if (id == InferenceId::SETS_FILTER_UP)
366 : : {
367 : 16 : Assert(conc.getKind() == Kind::EQUAL
368 : : && conc[0].getKind() == Kind::SET_MEMBER
369 : : && conc[0][1].getKind() == Kind::SET_FILTER);
370 : 32 : Node pred = conc[0][1][0];
371 : 16 : pfArgs.push_back(pred);
372 : 16 : }
373 : 96 : Node res = psb.tryStep(pr, {mem}, pfArgs);
374 [ + - ]: 48 : Trace("sets-ipc") << "Filter rule " << id << " returns " << res
375 : 24 : << ", expects " << conc << std::endl;
376 : 24 : success = CDProof::isSame(res, conc);
377 [ - + ][ - + ]: 24 : Assert(success);
[ - - ]
378 : 24 : }
379 : 24 : break;
380 : 85 : case InferenceId::SETS_EQ_MEM_CONFLICT:
381 : : case InferenceId::SETS_EQ_MEM:
382 : : {
383 : : // Handles cases:
384 : : // (and (= S set.empty) (set.member x S)) => false
385 : : // (and (= S (set.singleton y)) (set.member x S)) => (= x y)
386 [ - + ][ - + ]: 85 : Assert(assumps.size()==2);
[ - - ]
387 [ - + ][ - + ]: 85 : Assert(assumps[0].getKind() == Kind::EQUAL);
[ - - ]
388 [ - + ][ - + ]: 85 : Assert(assumps[1].getKind() == Kind::SET_MEMBER);
[ - - ]
389 : 170 : success = psb.applyPredTransform(assumps[1], conc, {assumps[0]});
390 : : }
391 : 85 : break;
392 : 867 : case InferenceId::SETS_EQ_CONFLICT:
393 [ + - ]: 867 : default: Trace("sets-ipc") << "Unhandled " << id; break;
394 : : }
395 [ + + ]: 1952 : if (success)
396 : : {
397 [ - + ]: 1085 : if (!cdp.addSteps(psb))
398 : : {
399 : : // should not fail if success was computed correctly above
400 : 0 : DebugUnhandled();
401 : : success = false;
402 : : }
403 : : }
404 [ + - ]: 1952 : Trace("sets-ipc") << "...success = " << success << std::endl;
405 : 1952 : return success;
406 : 1952 : }
407 : :
408 : 8 : std::string InferProofCons::identify() const { return "sets::InferProofCons"; }
409 : :
410 : : } // namespace sets
411 : : } // namespace theory
412 : : } // namespace cvc5::internal
|
