1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Alex Ozdemir, Gereon Kremer, Andres Noetzli |
4 |
|
* |
5 |
|
* This file is part of the cvc5 project. |
6 |
|
* |
7 |
|
* Copyright (c) 2009-2021 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_utilities.h" |
23 |
|
#include "theory/arith/constraint.h" |
24 |
|
#include "theory/arith/normal_form.h" |
25 |
|
#include "theory/arith/operator_elim.h" |
26 |
|
|
27 |
|
namespace cvc5 { |
28 |
|
namespace theory { |
29 |
|
namespace arith { |
30 |
|
|
31 |
3600 |
void ArithProofRuleChecker::registerTo(ProofChecker* pc) |
32 |
|
{ |
33 |
3600 |
pc->registerChecker(PfRule::MACRO_ARITH_SCALE_SUM_UB, this); |
34 |
3600 |
pc->registerChecker(PfRule::ARITH_SUM_UB, this); |
35 |
3600 |
pc->registerChecker(PfRule::ARITH_TRICHOTOMY, this); |
36 |
3600 |
pc->registerChecker(PfRule::INT_TIGHT_UB, this); |
37 |
3600 |
pc->registerChecker(PfRule::INT_TIGHT_LB, this); |
38 |
3600 |
pc->registerChecker(PfRule::ARITH_OP_ELIM_AXIOM, this); |
39 |
|
|
40 |
3600 |
pc->registerChecker(PfRule::ARITH_MULT_POS, this); |
41 |
3600 |
pc->registerChecker(PfRule::ARITH_MULT_NEG, this); |
42 |
|
// trusted rules |
43 |
3600 |
pc->registerTrustedChecker(PfRule::INT_TRUST, this, 2); |
44 |
3600 |
} |
45 |
|
|
46 |
236255 |
Node ArithProofRuleChecker::checkInternal(PfRule id, |
47 |
|
const std::vector<Node>& children, |
48 |
|
const std::vector<Node>& args) |
49 |
|
{ |
50 |
236255 |
NodeManager* nm = NodeManager::currentNM(); |
51 |
472510 |
auto zero = nm->mkConst<Rational>(0); |
52 |
236255 |
if (Debug.isOn("arith::pf::check")) |
53 |
|
{ |
54 |
|
Debug("arith::pf::check") << "Arith PfRule:" << id << std::endl; |
55 |
|
Debug("arith::pf::check") << " children: " << std::endl; |
56 |
|
for (const auto& c : children) |
57 |
|
{ |
58 |
|
Debug("arith::pf::check") << " * " << c << std::endl; |
59 |
|
} |
60 |
|
Debug("arith::pf::check") << " args:" << std::endl; |
61 |
|
for (const auto& c : args) |
62 |
|
{ |
63 |
|
Debug("arith::pf::check") << " * " << c << std::endl; |
64 |
|
} |
65 |
|
} |
66 |
236255 |
switch (id) |
67 |
|
{ |
68 |
22468 |
case PfRule::ARITH_MULT_POS: |
69 |
|
{ |
70 |
22468 |
Assert(children.empty()); |
71 |
22468 |
Assert(args.size() == 2); |
72 |
44936 |
Node mult = args[0]; |
73 |
22468 |
Kind rel = args[1].getKind(); |
74 |
22468 |
Assert(rel == Kind::EQUAL || rel == Kind::DISTINCT || rel == Kind::LT |
75 |
|
|| rel == Kind::LEQ || rel == Kind::GT || rel == Kind::GEQ); |
76 |
44936 |
Node lhs = args[1][0]; |
77 |
44936 |
Node rhs = args[1][1]; |
78 |
|
return nm->mkNode(Kind::IMPLIES, |
79 |
112340 |
nm->mkAnd(std::vector<Node>{ |
80 |
67404 |
nm->mkNode(Kind::GT, mult, zero), args[1]}), |
81 |
89872 |
nm->mkNode(rel, |
82 |
44936 |
nm->mkNode(Kind::MULT, mult, lhs), |
83 |
112340 |
nm->mkNode(Kind::MULT, mult, rhs))); |
84 |
|
} |
85 |
24857 |
case PfRule::ARITH_MULT_NEG: |
86 |
|
{ |
87 |
24857 |
Assert(children.empty()); |
88 |
24857 |
Assert(args.size() == 2); |
89 |
49714 |
Node mult = args[0]; |
90 |
24857 |
Kind rel = args[1].getKind(); |
91 |
24857 |
Assert(rel == Kind::EQUAL || rel == Kind::DISTINCT || rel == Kind::LT |
92 |
|
|| rel == Kind::LEQ || rel == Kind::GT || rel == Kind::GEQ); |
93 |
24857 |
Kind rel_inv = (rel == Kind::DISTINCT ? rel : reverseRelationKind(rel)); |
94 |
49714 |
Node lhs = args[1][0]; |
95 |
49714 |
Node rhs = args[1][1]; |
96 |
|
return nm->mkNode(Kind::IMPLIES, |
97 |
124285 |
nm->mkAnd(std::vector<Node>{ |
98 |
74571 |
nm->mkNode(Kind::LT, mult, zero), args[1]}), |
99 |
99428 |
nm->mkNode(rel_inv, |
100 |
49714 |
nm->mkNode(Kind::MULT, mult, lhs), |
101 |
124285 |
nm->mkNode(Kind::MULT, mult, rhs))); |
102 |
|
} |
103 |
8830 |
case PfRule::ARITH_SUM_UB: |
104 |
|
{ |
105 |
8830 |
if (children.size() < 2) |
106 |
|
{ |
107 |
|
return Node::null(); |
108 |
|
} |
109 |
|
|
110 |
|
// Whether a strict inequality is in the sum. |
111 |
8830 |
bool strict = false; |
112 |
17660 |
NodeBuilder leftSum(Kind::PLUS); |
113 |
17660 |
NodeBuilder rightSum(Kind::PLUS); |
114 |
55590 |
for (size_t i = 0; i < children.size(); ++i) |
115 |
|
{ |
116 |
|
// Adjust strictness |
117 |
46760 |
switch (children[i].getKind()) |
118 |
|
{ |
119 |
8562 |
case Kind::LT: |
120 |
|
{ |
121 |
8562 |
strict = true; |
122 |
8562 |
break; |
123 |
|
} |
124 |
38198 |
case Kind::LEQ: |
125 |
|
case Kind::EQUAL: |
126 |
|
{ |
127 |
38198 |
break; |
128 |
|
} |
129 |
|
default: |
130 |
|
{ |
131 |
|
Debug("arith::pf::check") |
132 |
|
<< "Bad kind: " << children[i].getKind() << std::endl; |
133 |
|
return Node::null(); |
134 |
|
} |
135 |
|
} |
136 |
46760 |
leftSum << children[i][0]; |
137 |
46760 |
rightSum << children[i][1]; |
138 |
|
} |
139 |
|
Node r = nm->mkNode(strict ? Kind::LT : Kind::LEQ, |
140 |
17660 |
leftSum.constructNode(), |
141 |
35320 |
rightSum.constructNode()); |
142 |
8830 |
return r; |
143 |
|
} |
144 |
71244 |
case PfRule::MACRO_ARITH_SCALE_SUM_UB: |
145 |
|
{ |
146 |
|
//================================================= Arithmetic rules |
147 |
|
// ======== Adding Inequalities |
148 |
|
// Note: an ArithLiteral is a term of the form (>< poly const) |
149 |
|
// where |
150 |
|
// >< is >=, >, ==, <, <=, or not(== ...). |
151 |
|
// poly is a polynomial |
152 |
|
// const is a rational constant |
153 |
|
|
154 |
|
// Children: (P1:l1, ..., Pn:ln) |
155 |
|
// where each li is an ArithLiteral |
156 |
|
// not(= ...) is dis-allowed! |
157 |
|
// |
158 |
|
// Arguments: (k1, ..., kn), non-zero reals |
159 |
|
// --------------------- |
160 |
|
// Conclusion: (>< t1 t2) |
161 |
|
// where >< is the fusion of the combination of the ><i, (flipping each |
162 |
|
// it its ki is negative). >< is always one of <, <= NB: this implies |
163 |
|
// that lower bounds must have negative ki, |
164 |
|
// and upper bounds must have positive ki. |
165 |
|
// t1 is the sum of the scaled polynomials (k_1 * poly_1 + ... + k_n * |
166 |
|
// poly_n) t2 is the sum of the scaled constants (k_1 * const_1 + ... + |
167 |
|
// k_n * const_n) |
168 |
71244 |
Assert(children.size() == args.size()); |
169 |
71244 |
if (children.size() < 2) |
170 |
|
{ |
171 |
|
return Node::null(); |
172 |
|
} |
173 |
|
|
174 |
|
// Whether a strict inequality is in the sum. |
175 |
71244 |
bool strict = false; |
176 |
142488 |
NodeBuilder leftSum(Kind::PLUS); |
177 |
142488 |
NodeBuilder rightSum(Kind::PLUS); |
178 |
302489 |
for (size_t i = 0; i < children.size(); ++i) |
179 |
|
{ |
180 |
462490 |
Rational scalar = args[i].getConst<Rational>(); |
181 |
231245 |
if (scalar == 0) |
182 |
|
{ |
183 |
|
Debug("arith::pf::check") << "Error: zero scalar" << std::endl; |
184 |
|
return Node::null(); |
185 |
|
} |
186 |
|
|
187 |
|
// Adjust strictness |
188 |
231245 |
switch (children[i].getKind()) |
189 |
|
{ |
190 |
48492 |
case Kind::GT: |
191 |
|
case Kind::LT: |
192 |
|
{ |
193 |
48492 |
strict = true; |
194 |
48492 |
break; |
195 |
|
} |
196 |
182753 |
case Kind::GEQ: |
197 |
|
case Kind::LEQ: |
198 |
|
case Kind::EQUAL: |
199 |
|
{ |
200 |
182753 |
break; |
201 |
|
} |
202 |
|
default: |
203 |
|
{ |
204 |
|
Debug("arith::pf::check") |
205 |
|
<< "Bad kind: " << children[i].getKind() << std::endl; |
206 |
|
} |
207 |
|
} |
208 |
|
// Check sign |
209 |
231245 |
switch (children[i].getKind()) |
210 |
|
{ |
211 |
67615 |
case Kind::GT: |
212 |
|
case Kind::GEQ: |
213 |
|
{ |
214 |
67615 |
if (scalar > 0) |
215 |
|
{ |
216 |
|
Debug("arith::pf::check") |
217 |
|
<< "Positive scalar for lower bound: " << scalar << " for " |
218 |
|
<< children[i] << std::endl; |
219 |
|
return Node::null(); |
220 |
|
} |
221 |
67615 |
break; |
222 |
|
} |
223 |
75889 |
case Kind::LEQ: |
224 |
|
case Kind::LT: |
225 |
|
{ |
226 |
75889 |
if (scalar < 0) |
227 |
|
{ |
228 |
|
Debug("arith::pf::check") |
229 |
|
<< "Negative scalar for upper bound: " << scalar << " for " |
230 |
|
<< children[i] << std::endl; |
231 |
|
return Node::null(); |
232 |
|
} |
233 |
75889 |
break; |
234 |
|
} |
235 |
87741 |
case Kind::EQUAL: |
236 |
|
{ |
237 |
87741 |
break; |
238 |
|
} |
239 |
|
default: |
240 |
|
{ |
241 |
|
Debug("arith::pf::check") |
242 |
|
<< "Bad kind: " << children[i].getKind() << std::endl; |
243 |
|
} |
244 |
|
} |
245 |
1156225 |
leftSum << nm->mkNode( |
246 |
1156225 |
Kind::MULT, nm->mkConst<Rational>(scalar), children[i][0]); |
247 |
1156225 |
rightSum << nm->mkNode( |
248 |
1156225 |
Kind::MULT, nm->mkConst<Rational>(scalar), children[i][1]); |
249 |
|
} |
250 |
|
Node r = nm->mkNode(strict ? Kind::LT : Kind::LEQ, |
251 |
142488 |
leftSum.constructNode(), |
252 |
284976 |
rightSum.constructNode()); |
253 |
71244 |
return r; |
254 |
|
} |
255 |
1427 |
case PfRule::INT_TIGHT_LB: |
256 |
|
{ |
257 |
|
// Children: (P:(> i c)) |
258 |
|
// where i has integer type. |
259 |
|
// Arguments: none |
260 |
|
// --------------------- |
261 |
|
// Conclusion: (>= i leastIntGreaterThan(c)}) |
262 |
2854 |
if (children.size() != 1 |
263 |
1427 |
|| (children[0].getKind() != Kind::GT |
264 |
|
&& children[0].getKind() != Kind::GEQ) |
265 |
2854 |
|| !children[0][0].getType().isInteger() |
266 |
4281 |
|| children[0][1].getKind() != Kind::CONST_RATIONAL) |
267 |
|
{ |
268 |
|
Debug("arith::pf::check") << "Illformed input: " << children; |
269 |
|
return Node::null(); |
270 |
|
} |
271 |
|
else |
272 |
|
{ |
273 |
2854 |
Rational originalBound = children[0][1].getConst<Rational>(); |
274 |
2854 |
Rational newBound = leastIntGreaterThan(originalBound); |
275 |
2854 |
Node rational = nm->mkConst<Rational>(newBound); |
276 |
1427 |
return nm->mkNode(kind::GEQ, children[0][0], rational); |
277 |
|
} |
278 |
|
} |
279 |
59636 |
case PfRule::INT_TIGHT_UB: |
280 |
|
{ |
281 |
|
// ======== Tightening Strict Integer Upper Bounds |
282 |
|
// Children: (P:(< i c)) |
283 |
|
// where i has integer type. |
284 |
|
// Arguments: none |
285 |
|
// --------------------- |
286 |
|
// Conclusion: (<= i greatestIntLessThan(c)}) |
287 |
119272 |
if (children.size() != 1 |
288 |
59636 |
|| (children[0].getKind() != Kind::LT |
289 |
|
&& children[0].getKind() != Kind::LEQ) |
290 |
119272 |
|| !children[0][0].getType().isInteger() |
291 |
178908 |
|| children[0][1].getKind() != Kind::CONST_RATIONAL) |
292 |
|
{ |
293 |
|
Debug("arith::pf::check") << "Illformed input: " << children; |
294 |
|
return Node::null(); |
295 |
|
} |
296 |
|
else |
297 |
|
{ |
298 |
119272 |
Rational originalBound = children[0][1].getConst<Rational>(); |
299 |
119272 |
Rational newBound = greatestIntLessThan(originalBound); |
300 |
119272 |
Node rational = nm->mkConst<Rational>(newBound); |
301 |
59636 |
return nm->mkNode(kind::LEQ, children[0][0], rational); |
302 |
|
} |
303 |
|
} |
304 |
44389 |
case PfRule::ARITH_TRICHOTOMY: |
305 |
|
{ |
306 |
88778 |
Node a = negateProofLiteral(children[0]); |
307 |
88778 |
Node b = negateProofLiteral(children[1]); |
308 |
88778 |
Node c = args[0]; |
309 |
44389 |
if (a[0] == b[0] && b[0] == c[0] && a[1] == b[1] && b[1] == c[1]) |
310 |
|
{ |
311 |
88778 |
std::set<Kind> cmps; |
312 |
44389 |
cmps.insert(a.getKind()); |
313 |
44389 |
cmps.insert(b.getKind()); |
314 |
44389 |
cmps.insert(c.getKind()); |
315 |
44389 |
if (cmps.count(Kind::EQUAL) == 0) |
316 |
|
{ |
317 |
|
Debug("arith::pf::check") << "Error: No = " << std::endl; |
318 |
|
return Node::null(); |
319 |
|
} |
320 |
44389 |
if (cmps.count(Kind::GT) == 0) |
321 |
|
{ |
322 |
|
Debug("arith::pf::check") << "Error: No > " << std::endl; |
323 |
|
return Node::null(); |
324 |
|
} |
325 |
44389 |
if (cmps.count(Kind::LT) == 0) |
326 |
|
{ |
327 |
|
Debug("arith::pf::check") << "Error: No < " << std::endl; |
328 |
|
return Node::null(); |
329 |
|
} |
330 |
44389 |
return args[0]; |
331 |
|
} |
332 |
|
else |
333 |
|
{ |
334 |
|
Debug("arith::pf::check") |
335 |
|
<< "Error: Different polynomials / values" << std::endl; |
336 |
|
Debug("arith::pf::check") << " a: " << a << std::endl; |
337 |
|
Debug("arith::pf::check") << " b: " << b << std::endl; |
338 |
|
Debug("arith::pf::check") << " c: " << c << std::endl; |
339 |
|
return Node::null(); |
340 |
|
} |
341 |
|
// Check that all have the same constant: |
342 |
|
} |
343 |
3404 |
case PfRule::INT_TRUST: |
344 |
|
{ |
345 |
3404 |
if (Debug.isOn("arith::pf::check::trust")) |
346 |
|
{ |
347 |
|
Debug("arith::pf::check::trust") << "Arith PfRule:" << id << std::endl; |
348 |
|
Debug("arith::pf::check::trust") << " children: " << std::endl; |
349 |
|
for (const auto& c : children) |
350 |
|
{ |
351 |
|
Debug("arith::pf::check::trust") << " * " << c << std::endl; |
352 |
|
} |
353 |
|
Debug("arith::pf::check::trust") << " args:" << std::endl; |
354 |
|
for (const auto& c : args) |
355 |
|
{ |
356 |
|
Debug("arith::pf::check::trust") << " * " << c << std::endl; |
357 |
|
} |
358 |
|
} |
359 |
3404 |
Assert(args.size() == 1); |
360 |
3404 |
return args[0]; |
361 |
|
} |
362 |
|
case PfRule::ARITH_OP_ELIM_AXIOM: |
363 |
|
{ |
364 |
|
Assert(children.empty()); |
365 |
|
Assert(args.size() == 1); |
366 |
|
return OperatorElim::getAxiomFor(args[0]); |
367 |
|
} |
368 |
|
default: return Node::null(); |
369 |
|
} |
370 |
|
} |
371 |
|
} // namespace arith |
372 |
|
} // namespace theory |
373 |
28191 |
} // namespace cvc5 |