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