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