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