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 : : * Implementation of arithmetic proof checker.
11 : : */
12 : :
13 : : #include "theory/arith/proof_checker.h"
14 : :
15 : : #include <iostream>
16 : : #include <set>
17 : :
18 : : #include "expr/skolem_manager.h"
19 : : #include "theory/arith/arith_poly_norm.h"
20 : : #include "theory/arith/arith_utilities.h"
21 : : #include "theory/arith/linear/constraint.h"
22 : : #include "theory/arith/operator_elim.h"
23 : :
24 : : using namespace cvc5::internal::kind;
25 : :
26 : : namespace cvc5::internal {
27 : : namespace theory {
28 : : namespace arith {
29 : :
30 : 28698 : ArithProofRuleChecker::ArithProofRuleChecker(NodeManager* nm)
31 : : : ProofRuleChecker(nm),
32 : 28698 : d_extChecker(nm),
33 : 28698 : d_pow2Checker(nm),
34 : 28698 : d_trChecker(nm)
35 : : #ifdef CVC5_POLY_IMP
36 : : ,
37 : 57396 : d_covChecker(nm)
38 : : #endif
39 : : {
40 : 28698 : }
41 : :
42 : 15170 : void ArithProofRuleChecker::registerTo(ProofChecker* pc)
43 : : {
44 : 15170 : pc->registerChecker(ProofRule::MACRO_ARITH_SCALE_SUM_UB, this);
45 : 15170 : pc->registerChecker(ProofRule::ARITH_SUM_UB, this);
46 : 15170 : pc->registerChecker(ProofRule::ARITH_TRICHOTOMY, this);
47 : 15170 : pc->registerChecker(ProofRule::INT_TIGHT_UB, this);
48 : 15170 : pc->registerChecker(ProofRule::INT_TIGHT_LB, this);
49 : 15170 : pc->registerChecker(ProofRule::ARITH_REDUCTION, this);
50 : 15170 : pc->registerChecker(ProofRule::ARITH_MULT_POS, this);
51 : 15170 : pc->registerChecker(ProofRule::ARITH_MULT_NEG, this);
52 : 15170 : pc->registerChecker(ProofRule::ARITH_POLY_NORM, this);
53 : 15170 : pc->registerChecker(ProofRule::ARITH_POLY_NORM_REL, this);
54 : : // register the extended proof checkers
55 : 15170 : d_extChecker.registerTo(pc);
56 : 15170 : d_pow2Checker.registerTo(pc);
57 : 15170 : d_trChecker.registerTo(pc);
58 : : #ifdef CVC5_POLY_IMP
59 : 15170 : d_covChecker.registerTo(pc);
60 : : #endif
61 : 15170 : }
62 : :
63 : 1017207 : Node ArithProofRuleChecker::checkInternal(ProofRule id,
64 : : const std::vector<Node>& children,
65 : : const std::vector<Node>& args)
66 : : {
67 : 1017207 : NodeManager* nm = nodeManager();
68 [ - + ]: 1017207 : if (TraceIsOn("arith::pf::check"))
69 : : {
70 [ - - ]: 0 : Trace("arith::pf::check") << "Arith ProofRule:" << id << std::endl;
71 [ - - ]: 0 : Trace("arith::pf::check") << " children: " << std::endl;
72 [ - - ]: 0 : for (const auto& c : children)
73 : : {
74 [ - - ]: 0 : Trace("arith::pf::check") << " * " << c << std::endl;
75 : : }
76 [ - - ]: 0 : Trace("arith::pf::check") << " args:" << std::endl;
77 [ - - ]: 0 : for (const auto& c : args)
78 : : {
79 [ - - ]: 0 : Trace("arith::pf::check") << " * " << c << std::endl;
80 : : }
81 : : }
82 [ + + ][ + + ]: 1017207 : switch (id)
[ + + ][ + + ]
[ + + ][ - ]
83 : : {
84 : 17814 : case ProofRule::ARITH_MULT_POS:
85 : : {
86 [ - + ][ - + ]: 17814 : Assert(children.empty());
[ - - ]
87 [ - + ][ - + ]: 17814 : Assert(args.size() == 2);
[ - - ]
88 : 17814 : Node mult = args[0];
89 : 17814 : Kind rel = args[1].getKind();
90 [ + + ][ + + ]: 17814 : Assert(rel == Kind::EQUAL || rel == Kind::LT || rel == Kind::LEQ
[ + + ][ + + ]
[ + + ][ + + ]
[ + + ][ + - ]
[ - + ][ - + ]
[ - - ]
91 : : || rel == Kind::GT || rel == Kind::GEQ);
92 : 17814 : Node lhs = args[1][0];
93 : 17814 : Node rhs = args[1][1];
94 : 35628 : Node zero = nm->mkConstRealOrInt(mult.getType(), Rational(0));
95 : 53442 : return nm->mkNode(Kind::IMPLIES,
96 [ + + ][ - - ]: 106884 : {nm->mkAnd(std::vector<Node>{
97 : 71256 : nm->mkNode(Kind::GT, mult, zero), args[1]}),
98 [ + + ][ - - ]: 89070 : nm->mkNode(rel,
99 : 35628 : {nm->mkNode(Kind::MULT, mult, lhs),
100 [ + + ][ - - ]: 124698 : nm->mkNode(Kind::MULT, mult, rhs)})});
101 : 17814 : }
102 : 121641 : case ProofRule::ARITH_MULT_NEG:
103 : : {
104 [ - + ][ - + ]: 121641 : Assert(children.empty());
[ - - ]
105 [ - + ][ - + ]: 121641 : Assert(args.size() == 2);
[ - - ]
106 : 121641 : Node mult = args[0];
107 : 121641 : Kind rel = args[1].getKind();
108 [ + + ][ + + ]: 121641 : Assert(rel == Kind::EQUAL || rel == Kind::LT || rel == Kind::LEQ
[ + + ][ + + ]
[ + + ][ + + ]
[ + + ][ + - ]
[ - + ][ - + ]
[ - - ]
109 : : || rel == Kind::GT || rel == Kind::GEQ);
110 : 121641 : Kind rel_inv = reverseRelationKind(rel);
111 : 121641 : Node lhs = args[1][0];
112 : 121641 : Node rhs = args[1][1];
113 : 243282 : Node zero = nm->mkConstRealOrInt(mult.getType(), Rational(0));
114 : 364923 : return nm->mkNode(Kind::IMPLIES,
115 [ + + ][ - - ]: 729846 : {nm->mkAnd(std::vector<Node>{
116 : 486564 : nm->mkNode(Kind::LT, mult, zero), args[1]}),
117 [ + + ][ - - ]: 608205 : nm->mkNode(rel_inv,
118 : 243282 : {nm->mkNode(Kind::MULT, mult, lhs),
119 [ + + ][ - - ]: 851487 : nm->mkNode(Kind::MULT, mult, rhs)})});
120 : 121641 : }
121 : 92476 : case ProofRule::ARITH_SUM_UB:
122 : : {
123 [ - + ]: 92476 : if (children.size() < 2)
124 : : {
125 : 0 : return Node::null();
126 : : }
127 : :
128 : : // Whether a strict inequality is in the sum.
129 : 92476 : bool strict = false;
130 : 92476 : NodeBuilder leftSum(nm, Kind::ADD);
131 : 92476 : NodeBuilder rightSum(nm, Kind::ADD);
132 [ + + ]: 495384 : for (size_t i = 0; i < children.size(); ++i)
133 : : {
134 : : // Adjust strictness
135 [ + + ][ - ]: 402908 : switch (children[i].getKind())
136 : : {
137 : 74966 : case Kind::LT:
138 : : {
139 : 74966 : strict = true;
140 : 74966 : break;
141 : : }
142 : 327942 : case Kind::LEQ:
143 : : case Kind::EQUAL:
144 : : {
145 : 327942 : break;
146 : : }
147 : 0 : default:
148 : : {
149 [ - - ]: 0 : Trace("arith::pf::check")
150 : 0 : << "Bad kind: " << children[i].getKind() << std::endl;
151 : 0 : return Node::null();
152 : : }
153 : : }
154 : 402908 : leftSum << children[i][0];
155 : 402908 : rightSum << children[i][1];
156 : : }
157 : 277428 : Node r = nm->mkNode(strict ? Kind::LT : Kind::LEQ,
158 [ + + ]: 277428 : {leftSum.constructNode(), rightSum.constructNode()});
159 : 92476 : return r;
160 : 92476 : }
161 : 677901 : case ProofRule::MACRO_ARITH_SCALE_SUM_UB:
162 : : {
163 : : //================================================= Arithmetic rules
164 : : // ======== Adding Inequalities
165 : : // Note: an ArithLiteral is a term of the form (>< poly const)
166 : : // where
167 : : // >< is >=, >, ==, <, <=, or not(== ...).
168 : : // poly is a polynomial
169 : : // const is a rational constant
170 : :
171 : : // Children: (P1:l1, ..., Pn:ln)
172 : : // where each li is an ArithLiteral
173 : : // not(= ...) is dis-allowed!
174 : : //
175 : : // Arguments: (k1, ..., kn), non-zero reals
176 : : // ---------------------
177 : : // Conclusion: (>< t1 t2)
178 : : // where >< is the fusion of the combination of the ><i, (flipping each
179 : : // it its ki is negative). >< is always one of <, <= NB: this implies
180 : : // that lower bounds must have negative ki,
181 : : // and upper bounds must have positive ki.
182 : : // t1 is the sum of the scaled polynomials (k_1 * poly_1 + ... + k_n *
183 : : // poly_n) t2 is the sum of the scaled constants (k_1 * const_1 + ... +
184 : : // k_n * const_n)
185 [ - + ][ - + ]: 677901 : Assert(children.size() == args.size());
[ - - ]
186 [ - + ]: 677901 : if (children.size() < 2)
187 : : {
188 : 0 : return Node::null();
189 : : }
190 : :
191 : : // Whether a strict inequality is in the sum.
192 : 677901 : bool strict = false;
193 : 677901 : NodeBuilder leftSum(nm, Kind::ADD);
194 : 677901 : NodeBuilder rightSum(nm, Kind::ADD);
195 [ + + ]: 2565555 : for (size_t i = 0; i < children.size(); ++i)
196 : : {
197 : 1887654 : Rational scalar = args[i].getConst<Rational>();
198 [ - + ]: 1887654 : if (scalar == 0)
199 : : {
200 [ - - ]: 0 : Trace("arith::pf::check") << "Error: zero scalar" << std::endl;
201 : 0 : return Node::null();
202 : : }
203 : :
204 : : // Adjust strictness
205 [ + + ][ - ]: 1887654 : switch (children[i].getKind())
206 : : {
207 : 356758 : case Kind::GT:
208 : : case Kind::LT:
209 : : {
210 : 356758 : strict = true;
211 : 356758 : break;
212 : : }
213 : 1530896 : case Kind::GEQ:
214 : : case Kind::LEQ:
215 : : case Kind::EQUAL:
216 : : {
217 : 1530896 : break;
218 : : }
219 : 0 : default:
220 : : {
221 [ - - ]: 0 : Trace("arith::pf::check")
222 : 0 : << "Bad kind: " << children[i].getKind() << std::endl;
223 : : }
224 : : }
225 : : // check for spurious mixed arithmetic
226 : 3775308 : if (children[i][0].getType().isReal()
227 : 3775308 : || children[i][1].getType().isReal())
228 : : {
229 [ - + ]: 649983 : if (args[i].getType().isInteger())
230 : : {
231 : : // Should use real for predicates over reals. This is only
232 : : // necessary for avoiding spurious usage of mixed arithmetic, but we
233 : : // check here to be pedantic.
234 : 0 : return Node::null();
235 : : }
236 : : }
237 [ + + ][ - + ]: 1237671 : else if (args[i].getType().isReal() && scalar.isIntegral())
[ + - ][ - + ]
[ - - ]
238 : : {
239 : : // conversely, don't use (integral) real for integer relation.
240 : 0 : return Node::null();
241 : : }
242 : : // Check sign
243 [ + + ][ + - ]: 1887654 : switch (children[i].getKind())
244 : : {
245 : 456308 : case Kind::GT:
246 : : case Kind::GEQ:
247 : : {
248 [ - + ]: 456308 : if (scalar > 0)
249 : : {
250 [ - - ]: 0 : Trace("arith::pf::check")
251 : 0 : << "Positive scalar for lower bound: " << scalar << " for "
252 : 0 : << children[i] << std::endl;
253 : 0 : return Node::null();
254 : : }
255 : 456308 : break;
256 : : }
257 : 572742 : case Kind::LEQ:
258 : : case Kind::LT:
259 : : {
260 [ - + ]: 572742 : if (scalar < 0)
261 : : {
262 [ - - ]: 0 : Trace("arith::pf::check")
263 : 0 : << "Negative scalar for upper bound: " << scalar << " for "
264 : 0 : << children[i] << std::endl;
265 : 0 : return Node::null();
266 : : }
267 : 572742 : break;
268 : : }
269 : 858604 : case Kind::EQUAL:
270 : : {
271 : 858604 : break;
272 : : }
273 : 0 : default:
274 : : {
275 [ - - ]: 0 : Trace("arith::pf::check")
276 : 0 : << "Bad kind: " << children[i].getKind() << std::endl;
277 : : }
278 : : }
279 : : // if multiplying by one, don't introduce MULT
280 [ + + ]: 1887654 : if (scalar == 1)
281 : : {
282 : 863919 : leftSum << children[i][0];
283 : 863919 : rightSum << children[i][1];
284 : : }
285 : : else
286 : : {
287 : 1023735 : leftSum << nm->mkNode(Kind::MULT, args[i], children[i][0]);
288 : 1023735 : rightSum << nm->mkNode(Kind::MULT, args[i], children[i][1]);
289 : : }
290 [ + - ]: 1887654 : }
291 : 2033703 : Node r = nm->mkNode(strict ? Kind::LT : Kind::LEQ,
292 [ + + ]: 2033703 : {leftSum.constructNode(), rightSum.constructNode()});
293 : 677901 : return r;
294 : 677901 : }
295 : 869 : case ProofRule::INT_TIGHT_LB:
296 : : {
297 : : // Children: (P:(> i c))
298 : : // where i has integer type.
299 : : // Arguments: none
300 : : // ---------------------
301 : : // Conclusion: (>= i leastIntGreaterThan(c)})
302 : 1738 : if (children.size() != 1
303 [ - + ]: 869 : || (children[0].getKind() != Kind::GT
304 [ - - ]: 0 : && children[0].getKind() != Kind::GEQ)
305 : 1738 : || !children[0][0].getType().isInteger() || !children[0][1].isConst())
306 : : {
307 [ - - ]: 0 : Trace("arith::pf::check") << "Illformed input: " << children;
308 : 0 : return Node::null();
309 : : }
310 : : else
311 : : {
312 : 869 : Rational originalBound = children[0][1].getConst<Rational>();
313 : 869 : Rational newBound = leastIntGreaterThan(originalBound);
314 : 869 : Node rational = nm->mkConstInt(newBound);
315 : 869 : return nm->mkNode(Kind::GEQ, children[0][0], rational);
316 : 869 : }
317 : : }
318 : 15372 : case ProofRule::INT_TIGHT_UB:
319 : : {
320 : : // ======== Tightening Strict Integer Upper Bounds
321 : : // Children: (P:(< i c))
322 : : // where i has integer type.
323 : : // Arguments: none
324 : : // ---------------------
325 : : // Conclusion: (<= i greatestIntLessThan(c)})
326 : 30744 : if (children.size() != 1
327 [ - + ]: 15372 : || (children[0].getKind() != Kind::LT
328 [ - - ]: 0 : && children[0].getKind() != Kind::LEQ)
329 : 30744 : || !children[0][0].getType().isInteger() || !children[0][1].isConst())
330 : : {
331 [ - - ]: 0 : Trace("arith::pf::check") << "Illformed input: " << children;
332 : 0 : return Node::null();
333 : : }
334 : : else
335 : : {
336 : 15372 : Rational originalBound = children[0][1].getConst<Rational>();
337 : 15372 : Rational newBound = greatestIntLessThan(originalBound);
338 : 15372 : Node rational = nm->mkConstInt(newBound);
339 : 15372 : return nm->mkNode(Kind::LEQ, children[0][0], rational);
340 : 15372 : }
341 : : }
342 : 7051 : case ProofRule::ARITH_TRICHOTOMY:
343 : : {
344 : 7051 : Node a = negateProofLiteral(children[0]);
345 : 7051 : Node b = negateProofLiteral(children[1]);
346 : 7051 : if (a[0] == b[0] && a[1] == b[1])
347 : : {
348 : 7051 : std::set<Kind> cmps;
349 : 7051 : cmps.insert(a.getKind());
350 : 7051 : cmps.insert(b.getKind());
351 : 7051 : Kind retk = Kind::UNDEFINED_KIND;
352 [ + + ]: 7051 : if (cmps.count(Kind::EQUAL) == 0)
353 : : {
354 : 4127 : retk = Kind::EQUAL;
355 : : }
356 [ + + ]: 7051 : if (cmps.count(Kind::GT) == 0)
357 : : {
358 [ - + ]: 1506 : if (retk != Kind::UNDEFINED_KIND)
359 : : {
360 [ - - ]: 0 : Trace("arith::pf::check")
361 : 0 : << "Error: No GT and " << retk << std::endl;
362 : 0 : return Node::null();
363 : : }
364 : 1506 : retk = Kind::GT;
365 : : }
366 [ + + ]: 7051 : if (cmps.count(Kind::LT) == 0)
367 : : {
368 [ - + ]: 1418 : if (retk != Kind::UNDEFINED_KIND)
369 : : {
370 [ - - ]: 0 : Trace("arith::pf::check")
371 : 0 : << "Error: No LT and " << retk << std::endl;
372 : 0 : return Node::null();
373 : : }
374 : 1418 : retk = Kind::LT;
375 : : }
376 : 7051 : return nm->mkNode(retk, a[0], a[1]);
377 : 7051 : }
378 : : else
379 : : {
380 [ - - ]: 0 : Trace("arith::pf::check")
381 : 0 : << "Error: Different polynomials / values" << std::endl;
382 [ - - ]: 0 : Trace("arith::pf::check") << " a: " << a << std::endl;
383 [ - - ]: 0 : Trace("arith::pf::check") << " b: " << b << std::endl;
384 : 0 : return Node::null();
385 : : }
386 : : // Check that all have the same constant:
387 : 7051 : }
388 : 1552 : case ProofRule::ARITH_REDUCTION:
389 : : {
390 [ - + ][ - + ]: 1552 : Assert(children.empty());
[ - - ]
391 [ - + ][ - + ]: 1552 : Assert(args.size() == 1);
[ - - ]
392 : 1552 : return OperatorElim::getAxiomFor(nm, args[0]);
393 : : }
394 : 53701 : case ProofRule::ARITH_POLY_NORM:
395 : : {
396 [ - + ][ - + ]: 53701 : Assert(children.empty());
[ - - ]
397 [ - + ][ - + ]: 53701 : Assert(args.size() == 1);
[ - - ]
398 : 53701 : if (args[0].getKind() != Kind::EQUAL
399 : 107402 : || !args[0][0].getType().isRealOrInt())
400 : : {
401 : 0 : return Node::null();
402 : : }
403 [ - + ]: 53701 : if (!PolyNorm::isArithPolyNorm(args[0][0], args[0][1]))
404 : : {
405 : 0 : return Node::null();
406 : : }
407 : 53701 : return args[0];
408 : : }
409 : 28830 : case ProofRule::ARITH_POLY_NORM_REL:
410 : : {
411 [ - + ][ - + ]: 28830 : Assert(children.size() == 1);
[ - - ]
412 [ - + ][ - + ]: 28830 : Assert(args.size() == 1);
[ - - ]
413 [ - + ]: 28830 : if (args[0].getKind() != Kind::EQUAL)
414 : : {
415 : 0 : return Node::null();
416 : : }
417 : 28830 : Kind k = args[0][0].getKind();
418 [ + + ][ + + ]: 28830 : if (k != Kind::LT && k != Kind::LEQ && k != Kind::EQUAL && k != Kind::GT
[ + + ][ + + ]
419 [ - + ]: 11867 : && k != Kind::GEQ)
420 : : {
421 : 0 : return Node::null();
422 : : }
423 [ - + ]: 28830 : if (children[0].getKind() != Kind::EQUAL)
424 : : {
425 : 0 : return Node::null();
426 : : }
427 : 28830 : Node l = children[0][0];
428 : 28830 : Node r = children[0][1];
429 [ + - ][ - + ]: 28830 : if (l.getKind() != Kind::MULT || r.getKind() != Kind::MULT)
[ - + ]
430 : : {
431 : 0 : return Node::null();
432 : : }
433 : 28830 : Node lr = l[1];
434 [ + + ]: 28830 : lr = lr.getKind() == Kind::TO_REAL ? lr[0] : lr;
435 : 28830 : Node rr = r[1];
436 [ + + ]: 28830 : rr = rr.getKind() == Kind::TO_REAL ? rr[0] : rr;
437 [ + - ][ - + ]: 28830 : if (lr.getKind() != Kind::SUB || rr.getKind() != Kind::SUB)
[ - + ]
438 : : {
439 : 0 : return Node::null();
440 : : }
441 : 28830 : Node cx = l[0];
442 : 28830 : Node x1 = lr[0];
443 : 28830 : Node x2 = lr[1];
444 : 28830 : Node cy = r[0];
445 : 28830 : Node y1 = rr[0];
446 : 28830 : Node y2 = rr[1];
447 : 28830 : if ((cx.getKind() == Kind::CONST_INTEGER
448 [ + - ]: 11686 : || cx.getKind() == Kind::CONST_RATIONAL)
449 [ + + ][ + + ]: 52202 : && (cy.getKind() == Kind::CONST_INTEGER
[ + - ]
450 [ + - ]: 11686 : || cy.getKind() == Kind::CONST_RATIONAL))
451 : : {
452 : 28830 : Rational c1 = cx.getConst<Rational>();
453 : 28830 : Rational c2 = cy.getConst<Rational>();
454 [ + - ][ - + ]: 28830 : if (c1.sgn() == 0 || c2.sgn() == 0)
[ - + ]
455 : : {
456 : 0 : return Node::null();
457 : : }
458 [ + + ][ - + ]: 28830 : if (k != Kind::EQUAL && c1.sgn() != c2.sgn())
[ - + ]
459 : : {
460 : 0 : return Node::null();
461 : : }
462 [ + - ][ + - ]: 28830 : }
463 : 57660 : Node ret = nm->mkNode(k, x1, x2).eqNode(nm->mkNode(k, y1, y2));
464 [ - + ]: 28830 : if (ret != args[0])
465 : : {
466 : 0 : return Node::null();
467 : : }
468 : 28830 : return ret;
469 : 28830 : }
470 : 0 : default: return Node::null();
471 : : }
472 : : }
473 : : } // namespace arith
474 : : } // namespace theory
475 : : } // namespace cvc5::internal
|
