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