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 : : * A generic utility for inferring proofs for arithmetic lemmas.
11 : : */
12 : :
13 : : #include "theory/arith/arith_proof_rcons.h"
14 : :
15 : : #include "proof/conv_proof_generator.h"
16 : : #include "proof/proof.h"
17 : : #include "proof/proof_node.h"
18 : : #include "theory/arith/arith_msum.h"
19 : : #include "theory/arith/arith_subs.h"
20 : : #include "util/rational.h"
21 : :
22 : : namespace cvc5::internal {
23 : : namespace theory {
24 : : namespace arith {
25 : :
26 : : namespace {
27 : :
28 : : /**
29 : : * Returns true if lit iff (>= lhs rhs) for constant rhs.
30 : : */
31 : 18 : bool getGeqBound(const Node& lit, Node& lhs, Rational& rhs)
32 : : {
33 [ + - ][ - + ]: 18 : if (lit.getKind() != Kind::GEQ || lit[1].getKind() != Kind::CONST_INTEGER)
[ + - ][ - + ]
[ - - ]
34 : : {
35 : 0 : return false;
36 : : }
37 : 18 : lhs = lit[0];
38 : 18 : rhs = lit[1].getConst<Rational>();
39 : 18 : return true;
40 : : }
41 : :
42 : : } // namespace
43 : :
44 : 118 : ArithProofRCons::ArithProofRCons(Env& env, TrustId id) : EnvObj(env), d_id(id)
45 : : {
46 : 118 : d_false = nodeManager()->mkConst(false);
47 : 118 : }
48 : :
49 : 118 : ArithProofRCons::~ArithProofRCons() {}
50 : :
51 : 353 : bool ArithProofRCons::solveEquality(CDProof& cdp,
52 : : TConvProofGenerator& tcnv,
53 : : ArithSubs& asubs,
54 : : const Node& as)
55 : : {
56 [ - + ][ - + ]: 353 : Assert(as.getKind() == Kind::EQUAL);
[ - - ]
57 : 353 : Node asr = rewrite(as);
58 [ + - ]: 353 : Trace("arith-proof-rcons") << "...under subs+rewrite: " << asr << std::endl;
59 : : // see if there is a variable to solve for
60 : 353 : std::map<Node, Node> msum;
61 : : // Use rewritten form to get the monomial, we will prove a = as by tcnv
62 : : // and as = (v = val) by MACRO_SR_PRED_TRANSFORM below.
63 [ - + ]: 353 : if (!ArithMSum::getMonomialSumLit(asr, msum))
64 : : {
65 [ - - ]: 0 : Trace("arith-proof-rcons") << "......failed msum" << std::endl;
66 : 0 : return false;
67 : : }
68 [ + + ]: 810 : for (const std::pair<const Node, Node>& m : msum)
69 : : {
70 [ + + ][ + + ]: 690 : if (m.first.isNull() || !m.second.isNull())
[ + + ]
71 : : {
72 [ + - ]: 914 : Trace("arith-proof-rcons") << "......nonfactor " << m.first << " ("
73 : 457 : << m.second << ")" << std::endl;
74 : 457 : continue;
75 : : }
76 : 233 : Node veq_c, val;
77 : 233 : int ires = ArithMSum::isolate(m.first, msum, veq_c, val, Kind::EQUAL);
78 [ + - ][ - + ]: 233 : if (ires == 0 || !veq_c.isNull())
[ - + ]
79 : : {
80 [ - - ]: 0 : Trace("arith-proof-rcons") << "......no isolate " << m.first << std::endl;
81 : 0 : continue;
82 : : }
83 [ + - ]: 466 : Trace("arith-proof-rcons")
84 : 233 : << "SUBS: " << m.first << " = " << val << std::endl;
85 : 233 : Node eq = m.first.eqNode(val);
86 [ + + ]: 233 : if (!CDProof::isSame(as, eq))
87 : : {
88 : 687 : cdp.addStep(eq, ProofRule::MACRO_SR_PRED_TRANSFORM, {as}, {eq});
89 : : }
90 : : // to ensure a fixed point substitution, we apply the current
91 : : // substitution to the range of previous substitutions
92 [ + + ]: 233 : if (!asubs.empty())
93 : : {
94 : 115 : ArithSubs stmp;
95 : 115 : stmp.add(m.first, val);
96 [ + + ]: 386 : for (size_t i = 0, ns = asubs.d_subs.size(); i < ns; i++)
97 : : {
98 : 271 : asubs.d_subs[i] = stmp.applyArith(asubs.d_subs[i], false);
99 : : }
100 : 115 : }
101 : 233 : asubs.add(m.first, val);
102 : 233 : tcnv.addRewriteStep(m.first, val, &cdp);
103 : 233 : return true;
104 [ - + ][ - + ]: 699 : }
105 [ + - ]: 240 : Trace("arith-proof-rcons")
106 : 120 : << "...failed solve equality (no factor)" << std::endl;
107 : 120 : return false;
108 : 353 : }
109 : :
110 : 18 : Node ArithProofRCons::applySR(ArithSubs& asubs, const Node& a)
111 : : {
112 : 18 : Node as = asubs.applyArith(a, false);
113 : 36 : return rewrite(as);
114 : 18 : }
115 : :
116 : 149 : Node ArithProofRCons::applySR(CDProof& cdp,
117 : : TConvProofGenerator& tcnv,
118 : : ArithSubs& asubs,
119 : : const Node& a)
120 : : {
121 : 149 : Node as = asubs.applyArith(a, false);
122 : 149 : Node asr = rewrite(as);
123 [ + - ]: 149 : Trace("arith-proof-rcons") << "...have " << asr << std::endl;
124 [ + + ]: 149 : if (a != as)
125 : : {
126 : 139 : std::shared_ptr<ProofNode> pfn = tcnv.getProofForRewriting(a);
127 : 278 : Assert(pfn->getResult()[1] == as)
128 : 139 : << "no-solve: got " << pfn->getResult()[1] << ", expected " << as;
129 : 139 : cdp.addProof(pfn);
130 [ + + ][ - - ]: 417 : cdp.addStep(as, ProofRule::EQ_RESOLVE, {a, a.eqNode(as)}, {});
131 : 139 : }
132 [ + + ]: 149 : if (!CDProof::isSame(as, asr))
133 : : {
134 : 417 : cdp.addStep(asr, ProofRule::MACRO_SR_PRED_TRANSFORM, {as}, {asr});
135 : : }
136 : 298 : return asr;
137 : 149 : }
138 : :
139 : 118 : std::shared_ptr<ProofNode> ArithProofRCons::getProofFor(Node fact)
140 : : {
141 [ + - ]: 118 : Trace("arith-proof-rcons") << "ArithProofRCons: prove " << fact << std::endl;
142 : 236 : CDProof cdp(d_env);
143 : 118 : bool success = false;
144 : : // ARITH_DIO_LEMMA can typically be reconstructed via substitution+rewriting.
145 [ + - ]: 118 : if (d_id == TrustId::ARITH_DIO_LEMMA)
146 : : {
147 [ - + ][ - + ]: 118 : Assert(fact.getKind() == Kind::NOT);
[ - - ]
148 : 118 : std::vector<Node> assumps;
149 [ + - ]: 118 : if (fact[0].getKind() == Kind::AND)
150 : : {
151 : 118 : assumps.insert(assumps.end(), fact[0].begin(), fact[0].end());
152 : : }
153 : : else
154 : : {
155 : 0 : assumps.push_back(fact[0]);
156 : : }
157 : 118 : ArithSubs asubs;
158 : 118 : std::vector<Node> assumpsNoSolve;
159 : : // Do not traverse non-linear terms
160 : 118 : ArithSubsTermContext astc(false);
161 : : // This proof generator is intended to provide proofs for asubs.applyArith.
162 : : // In particular, we maintain the invariant that if
163 : : // asubs.applyArith(a) = as, then tcnv.getProofForRewriting(a) returns a
164 : : // proof of (= a as).
165 : : TConvProofGenerator tcnv(d_env,
166 : : nullptr,
167 : : TConvPolicy::FIXPOINT,
168 : : TConvCachePolicy::NEVER,
169 : : "ArithRConsTConv",
170 : 236 : &astc);
171 : : // if we have not yet found a contradiction, we look for contradictions, or
172 : : // further entailed equalities.
173 : 118 : bool addedSubs = true;
174 : 118 : std::unordered_set<Node> solved;
175 [ + + ][ + - ]: 305 : while (!success && addedSubs)
176 : : {
177 [ + - ]: 187 : Trace("arith-proof-rcons") << "==== Iterate" << std::endl;
178 : 187 : addedSubs = false;
179 : : // check if two unsolved literals rewrite to the negation of one another
180 : 187 : std::map<Node, bool> pols;
181 : 187 : std::map<Node, Node> psrc;
182 : 187 : std::map<Node, bool>::iterator itp;
183 [ + + ]: 1122 : std::map<Node, Node> boundingLits[2];
184 [ + + ]: 638 : for (const Node& a : assumps)
185 : : {
186 [ + + ]: 569 : if (solved.find(a) != solved.end())
187 : : {
188 : : // already solved
189 : 402 : continue;
190 : : }
191 [ + - ]: 515 : Trace("arith-proof-rcons") << "- process " << a << std::endl;
192 : 515 : Node as = asubs.applyArith(a, false);
193 : 515 : Node asr = rewrite(as);
194 [ + - ]: 515 : Trace("arith-proof-rcons") << " - SR to " << asr << std::endl;
195 [ + + ]: 515 : if (asr == d_false)
196 : : {
197 [ + - ]: 97 : Trace("arith-proof-rcons") << "...success!" << std::endl;
198 : : // apply substitution + rewriting again, with proofs
199 : 97 : applySR(cdp, tcnv, asubs, a);
200 : 97 : success = true;
201 : 97 : break;
202 : : }
203 : : // if its an equality, try to turn it into a substitution
204 [ + + ]: 418 : if (asr.getKind() == Kind::EQUAL)
205 : : {
206 : : // must remember the proof prior to changing the substitution
207 : 348 : std::shared_ptr<ProofNode> pfn;
208 [ + + ]: 348 : if (a != as)
209 : : {
210 : 58 : pfn = tcnv.getProofForRewriting(a);
211 : : }
212 [ + + ]: 348 : if (solveEquality(cdp, tcnv, asubs, as))
213 : : {
214 : 228 : addedSubs = true;
215 : 228 : solved.insert(a);
216 [ + + ]: 228 : if (pfn != nullptr)
217 : : {
218 : 54 : cdp.addProof(pfn);
219 [ + + ][ - - ]: 162 : cdp.addStep(as, ProofRule::EQ_RESOLVE, {a, a.eqNode(as)}, {});
220 : : }
221 : : }
222 : 348 : continue;
223 : 348 : }
224 : 70 : bool pol = asr.getKind() != Kind::NOT;
225 [ + + ]: 70 : Node aslit = pol ? asr : asr[0];
226 : 70 : itp = pols.find(aslit);
227 : : // look for conflicting atoms
228 [ + + ]: 70 : if (itp != pols.end())
229 : : {
230 [ + - ]: 21 : if (itp->second != pol)
231 : : {
232 : : // apply substitution + rewriting again, with proofs
233 : 21 : Node a1 = applySR(cdp, tcnv, asubs, a);
234 [ - + ][ - + ]: 21 : Assert(a1 == asr);
[ - - ]
235 : 21 : Node a2 = applySR(cdp, tcnv, asubs, psrc[aslit]);
236 [ - + ][ - + ]: 21 : Assert(a2 == asr.negate());
[ - - ]
237 : 21 : Node asn = aslit.notNode();
238 [ + + ][ - - ]: 63 : cdp.addStep(d_false, ProofRule::CONTRA, {aslit, asn}, {});
239 : 21 : success = true;
240 [ + - ]: 21 : Trace("arith-proof-rcons") << "......contradiction" << std::endl;
241 : 21 : break;
242 : 21 : }
243 : : }
244 : : else
245 : : {
246 : 49 : pols[aslit] = pol;
247 : 49 : psrc[aslit] = a;
248 : : }
249 : : // otherwise remember bounds
250 [ + - ]: 49 : if (aslit.getKind() == Kind::GEQ)
251 : : {
252 [ + + ]: 49 : boundingLits[pol ? 0 : 1][aslit[0]] = a;
253 : : }
254 [ + + ][ + + ]: 1002 : }
[ + + ][ + + ]
255 : : // if not successful, see if we can use trichotomy to infer that
256 : : // upper, lower bounds entail an equality.
257 [ + + ]: 187 : if (!success)
258 : : {
259 : 69 : std::map<Node, Node>& bl0 = boundingLits[0];
260 : 69 : std::map<Node, Node>& bl1 = boundingLits[1];
261 : 69 : std::map<Node, Node>::iterator itb;
262 : 69 : Rational negone(-1);
263 : 69 : NodeManager* nm = nodeManager();
264 [ + + ]: 73 : for (const std::pair<const Node, Node>& bl : bl0)
265 : : {
266 : 9 : itb = bl1.find(bl.first);
267 [ - + ]: 9 : if (itb == bl1.end())
268 : : {
269 : 0 : continue;
270 : : }
271 : : // reconstruct the literals of the form
272 : : // (>= t c1) and (not (>= t c2)).
273 : 9 : Node l1 = applySR(asubs, bl.second);
274 [ - + ]: 9 : l1 = l1.getKind() == Kind::NOT ? l1[0] : l1;
275 : 9 : Node l2 = applySR(asubs, itb->second);
276 [ + - ]: 9 : l2 = l2.getKind() == Kind::NOT ? l2[0] : l2;
277 [ + - ]: 18 : Trace("arith-proof-rcons") << "......dual binding lits " << l1
278 : 9 : << ", not " << l2 << std::endl;
279 : 9 : Node lhs1, lhs2;
280 : 9 : Rational c1, c2;
281 [ + - ]: 18 : if (!getGeqBound(l1, lhs1, c1) || !getGeqBound(l2, lhs2, c2)
282 [ + - ][ - + ]: 18 : || lhs1 != lhs2)
[ - + ]
283 : : {
284 : 0 : continue;
285 : : }
286 : 9 : Rational c2m1 = c2 + negone;
287 : : // if c1 == c2-1, then this implies t = c1.
288 [ + + ]: 9 : if (c1 == c2m1)
289 : : {
290 : : // apply substitution + rewriting with proofs now
291 : 5 : applySR(cdp, tcnv, asubs, bl.second);
292 : 5 : applySR(cdp, tcnv, asubs, itb->second);
293 : : Node l2strict =
294 : 10 : nm->mkNode(Kind::GT, l2[0], nm->mkConstInt(c2m1)).notNode();
295 : 5 : Node l2n = l2.notNode();
296 : 5 : Node equiv = l2n.eqNode(l2strict);
297 : 10 : cdp.addStep(equiv, ProofRule::MACRO_SR_PRED_INTRO, {}, {equiv});
298 [ + + ][ - - ]: 15 : cdp.addStep(l2strict, ProofRule::EQ_RESOLVE, {l2n, equiv}, {});
299 : 10 : Node eq = l1[0].eqNode(l1[1]);
300 [ + + ][ - - ]: 15 : cdp.addStep(eq, ProofRule::ARITH_TRICHOTOMY, {l1, l2strict}, {});
301 [ + - ]: 10 : Trace("arith-proof-rcons")
302 : 5 : << ".......solves to " << eq << " by trichotomy" << std::endl;
303 [ + - ]: 5 : if (solveEquality(cdp, tcnv, asubs, eq))
304 : : {
305 : 5 : addedSubs = true;
306 : 5 : solved.insert(bl.second);
307 : 5 : solved.insert(itb->second);
308 : 5 : break;
309 : : }
310 [ - + ][ - + ]: 20 : }
[ - + ][ - + ]
311 : : // NOTE: otherwise if c1 > c2-1, this implies a contradiction,
312 : : // although it appears that this case does not happen in DIO lemmas.
313 : : // If it did, we would fail with a proof hole here.
314 [ + + ][ + - ]: 39 : }
[ + + ][ - + ]
[ + - ][ + + ]
[ - + ][ + - ]
[ + + ][ - + ]
315 : 69 : }
316 [ + + ][ - - ]: 748 : }
317 [ + - ]: 118 : if (success)
318 : : {
319 : 236 : cdp.addStep(fact, ProofRule::SCOPE, {d_false}, assumps);
320 : : }
321 : 118 : }
322 [ - + ]: 118 : if (!success)
323 : : {
324 [ - - ]: 0 : Trace("arith-proof-rcons") << "...failed!" << std::endl;
325 : 0 : cdp.addTrustedStep(fact, d_id, {}, {});
326 : : }
327 : 236 : return cdp.getProofFor(fact);
328 : 118 : }
329 : :
330 : 0 : std::string ArithProofRCons::identify() const { return "ArithProofRCons"; }
331 : :
332 : : } // namespace arith
333 : : } // namespace theory
334 : : } // namespace cvc5::internal
|
