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 operator elimination for arithmetic.
11 : : */
12 : :
13 : : #include "theory/arith/operator_elim.h"
14 : :
15 : : #include <sstream>
16 : :
17 : : #include "expr/bound_var_manager.h"
18 : : #include "options/arith_options.h"
19 : : #include "proof/proof.h"
20 : : #include "proof/proof_node_manager.h"
21 : : #include "proof/trust_id.h"
22 : : #include "smt/env.h"
23 : : #include "smt/logic_exception.h"
24 : : #include "theory/arith/arith_utilities.h"
25 : : #include "theory/arith/nl/poly_conversion.h"
26 : : #include "theory/rewriter.h"
27 : : #include "theory/theory.h"
28 : :
29 : : using namespace cvc5::internal::kind;
30 : :
31 : : namespace cvc5::internal {
32 : : namespace theory {
33 : : namespace arith {
34 : :
35 : 28663 : OperatorElim::OperatorElim(Env& env) : EnvObj(env), d_lemmaMap(userContext()) {}
36 : :
37 : 856683 : TrustNode OperatorElim::eliminate(Node n,
38 : : std::vector<SkolemLemma>& lems,
39 : : bool partialOnly)
40 : : {
41 [ - + ][ - + ]: 856683 : Assert(rewrite(n) == n);
[ - - ]
42 : 856683 : NodeManager* nm = nodeManager();
43 : 856683 : std::vector<std::pair<Node, Node>> klems;
44 : 856683 : bool wasNonLinear = false;
45 : 856683 : Node nn = eliminateOperators(nm, n, klems, partialOnly, wasNonLinear);
46 [ + + ]: 856683 : if (nn == n)
47 : : {
48 : 849243 : return TrustNode::null();
49 : : }
50 : : // logic exception if non-linear
51 [ + + ]: 7440 : if (wasNonLinear)
52 : : {
53 [ + + ]: 3672 : if (logicInfo().isLinear())
54 : : {
55 [ + - ]: 10 : Trace("arith-logic") << "ERROR: Non-linear term in linear logic: " << n
56 : 5 : << std::endl;
57 : 5 : std::stringstream serr;
58 : 5 : serr << "A non-linear fact was asserted to arithmetic in a linear logic."
59 : 5 : << std::endl;
60 : 5 : serr << "The fact in question: " << n << std::endl;
61 : 5 : throw LogicException(serr.str());
62 : 5 : }
63 : : }
64 : : // if transcendental, we don't eliminate if not expert
65 [ + + ]: 7435 : if (isTranscendentalKind(n.getKind()))
66 : : {
67 [ - + ]: 133 : if (!options().arith.arithExp)
68 : : {
69 : 0 : return TrustNode::null();
70 : : }
71 : : }
72 : : // should only be a single lemma, if there is one
73 [ - + ][ - + ]: 7435 : Assert(klems.size() <= 1);
[ - - ]
74 [ + + ]: 12591 : for (std::pair<Node, Node>& p : klems)
75 : : {
76 : : // each skolem lemma can be justified by this class
77 : 5156 : lems.emplace_back(mkSkolemLemma(p.first, p.second, n));
78 : : }
79 : : // we can provide a proof for the rewrite as well
80 : 7435 : return TrustNode::mkTrustRewrite(n, nn, this);
81 : 856688 : }
82 : :
83 : 860842 : Node OperatorElim::eliminateOperators(NodeManager* nm,
84 : : Node node,
85 : : std::vector<std::pair<Node, Node>>& lems,
86 : : bool partialOnly,
87 : : bool& wasNonLinear)
88 : : {
89 [ + - ]: 860842 : Trace("arith-op-elim") << "node: " << node << std::endl;
90 : 860842 : SkolemManager* sm = nm->getSkolemManager();
91 : 860842 : Kind k = node.getKind();
92 [ + + ][ + + ]: 860842 : switch (k)
[ + + ][ + + ]
[ + + ][ + ]
93 : : {
94 : 941 : case Kind::TO_INTEGER:
95 : : case Kind::IS_INTEGER:
96 : : {
97 [ + + ]: 941 : if (partialOnly)
98 : : {
99 : : // not eliminating total operators
100 : 31 : return node;
101 : : }
102 : : // node[0] - 1 < toIntSkolem <= node[0]
103 : : // -1 < toIntSkolem - node[0] <= 0
104 : : // 0 <= node[0] - toIntSkolem < 1
105 : 1820 : Node pterm = nm->mkNode(Kind::TO_INTEGER, node[0]);
106 : 910 : Node v = sm->mkPurifySkolem(pterm);
107 : 910 : Node vr = nm->mkNode(Kind::TO_REAL, v);
108 : 910 : Node one = nm->mkConstReal(Rational(1));
109 : 910 : Node zero = nm->mkConstReal(Rational(0));
110 : 1820 : Node diff = nm->mkNode(Kind::SUB, node[0], vr);
111 : 1820 : Node lem = mkInRange(diff, zero, one);
112 : 910 : lems.emplace_back(lem, v);
113 [ + + ]: 910 : if (k == Kind::IS_INTEGER)
114 : : {
115 : 526 : return nm->mkNode(Kind::EQUAL, node[0], vr);
116 : : }
117 [ - + ][ - + ]: 384 : Assert(k == Kind::TO_INTEGER);
[ - - ]
118 : 384 : return v;
119 : 910 : }
120 : 60 : case Kind::INTS_LOG2:
121 : : {
122 [ + + ]: 60 : if (partialOnly)
123 : : {
124 : : // not eliminating total operators
125 : 2 : return node;
126 : : }
127 : : // for a fresh skolem v, the elimination is:
128 : : // (int.log2 x) --> v, with lemmas:
129 : : // (=> (> x 0) (and (<= (int.pow2 v) x) (< x (* 2 (int.pow2 v)))))
130 : : // (=> (<= x 0) (= v 0))
131 : 116 : Node zero = nm->mkConstInt(Integer(0));
132 : 116 : Node one = nm->mkConstInt(Integer(1));
133 : 58 : Node x = node[0];
134 : 58 : Node v = sm->mkPurifySkolem(node);
135 : 116 : Node sv = nm->mkNode(Kind::ADD, v, one);
136 : 58 : Node ptv = nm->mkNode(Kind::POW2, v);
137 : 58 : Node ptv1 = nm->mkNode(Kind::POW2, sv);
138 : 116 : Node pos_assumption = nm->mkNode(Kind::LT, zero, x);
139 : 116 : Node pos_prop1 = nm->mkNode(Kind::LEQ, ptv, x);
140 : 116 : Node pos_prop2 = nm->mkNode(Kind::LT, x, ptv1);
141 : 116 : Node pos_prop = nm->mkNode(Kind::AND, pos_prop1, pos_prop2);
142 : 116 : Node pos_lem = nm->mkNode(Kind::IMPLIES, pos_assumption, pos_prop);
143 : :
144 : 58 : Node neg_assumption = nm->mkNode(Kind::NOT, pos_assumption);
145 : 116 : Node neg_prop = nm->mkNode(Kind::EQUAL, v, zero);
146 : 116 : Node neg_lem = nm->mkNode(Kind::IMPLIES, neg_assumption, neg_prop);
147 : 116 : Node lem = nm->mkNode(Kind::AND, pos_lem, neg_lem);
148 : 58 : lems.emplace_back(lem, v);
149 : :
150 [ + - ]: 58 : Trace("arith-op-elim") << "INTS_LOG2: node" << node << std::endl;
151 [ + - ]: 58 : Trace("arith-op-elim") << "INTS_LOG2: x" << x << std::endl;
152 [ + - ]: 58 : Trace("arith-op-elim") << "INTS_LOG2: v" << v << std::endl;
153 [ + - ]: 58 : Trace("arith-op-elim") << "INTS_LOG2: lem" << lem << std::endl;
154 : 58 : return v;
155 : 58 : }
156 : 6517 : case Kind::INTS_DIVISION_TOTAL:
157 : : case Kind::INTS_MODULUS_TOTAL:
158 : : {
159 [ + + ]: 6517 : if (partialOnly)
160 : : {
161 : : // not eliminating total operators
162 : 91 : return node;
163 : : }
164 : : // we use the purification skolem for div
165 : 6426 : Node den = node[1];
166 : 6426 : Node num = node[0];
167 : 12852 : Node pterm = nm->mkNode(Kind::INTS_DIVISION_TOTAL, node[0], node[1]);
168 : 6426 : Node v = sm->mkPurifySkolem(pterm);
169 : : // make the corresponding lemma
170 : 6426 : Node lem;
171 : 12852 : Node leqNum = nm->mkNode(Kind::LEQ, nm->mkNode(Kind::MULT, den, v), num);
172 [ + + ]: 6426 : if (den.isConst())
173 : : {
174 : 5028 : const Rational& rat = den.getConst<Rational>();
175 [ + - ][ + - ]: 5028 : Assert(!num.isConst() && rat.sgn() != 0);
[ - + ][ - + ]
[ - - ]
176 : 10056 : lem = nm->mkNode(
177 : : Kind::AND,
178 : : leqNum,
179 : 10056 : nm->mkNode(
180 : : Kind::LT,
181 : : num,
182 : 10056 : nm->mkNode(
183 : : Kind::MULT,
184 : : den,
185 : 10056 : nm->mkNode(Kind::ADD,
186 : : v,
187 [ + - ]: 15084 : nm->mkConstInt(Rational(rat > 0 ? 1 : -1))))));
188 : : }
189 : : else
190 : : {
191 : 1398 : wasNonLinear = true;
192 [ + + ][ - - ]: 6990 : lem = nm->mkNode(
193 : : Kind::AND,
194 [ + + ][ - - ]: 6990 : {nm->mkNode(
195 : : Kind::IMPLIES,
196 : 2796 : {nm->mkNode(Kind::GT, den, nm->mkConstInt(Rational(0))),
197 : 2796 : nm->mkNode(
198 : : Kind::AND,
199 : : leqNum,
200 : 2796 : nm->mkNode(Kind::LT,
201 : : num,
202 : 2796 : nm->mkNode(Kind::MULT,
203 : : den,
204 : 2796 : nm->mkNode(Kind::ADD,
205 : : v,
206 : 2796 : nm->mkConstInt(
207 : 2796 : Rational(1))))))}),
208 [ + + ][ - - ]: 6990 : nm->mkNode(
209 : : Kind::IMPLIES,
210 : 2796 : {nm->mkNode(Kind::LT, den, nm->mkConstInt(Rational(0))),
211 : 2796 : nm->mkNode(
212 : : Kind::AND,
213 : : leqNum,
214 : 2796 : nm->mkNode(
215 : : Kind::LT,
216 : : num,
217 : 2796 : nm->mkNode(
218 : : Kind::MULT,
219 : : den,
220 : 2796 : nm->mkNode(Kind::ADD,
221 : : v,
222 : 4194 : nm->mkConstInt(Rational(-1))))))})});
223 : : }
224 : : // add the skolem lemma to lems
225 : 6426 : lems.emplace_back(lem, v);
226 [ + - ]: 6426 : Trace("arith-op-elim") << "lem " << lem << std::endl;
227 [ + + ]: 6426 : if (k == Kind::INTS_MODULUS_TOTAL)
228 : : {
229 : 8012 : Node nn = nm->mkNode(Kind::SUB, num, nm->mkNode(Kind::MULT, den, v));
230 : 4006 : return nn;
231 : 4006 : }
232 : 2420 : return v;
233 : 6426 : }
234 : 1002 : case Kind::DIVISION_TOTAL:
235 : : {
236 [ + + ]: 1002 : if (partialOnly)
237 : : {
238 : : // not eliminating total operators
239 : 103 : return node;
240 : : }
241 : 899 : Node num = node[0];
242 : 899 : Node den = node[1];
243 [ - + ]: 899 : if (den.isConst())
244 : : {
245 : : // No need to eliminate here, can eliminate via rewriting later.
246 : : // Moreover, rewriting may change the type of this node from real to
247 : : // int, which impacts certain issues with subtyping.
248 : 0 : return node;
249 : : }
250 : 899 : wasNonLinear = true;
251 : 1798 : Node rw = nm->mkNode(k, num, den);
252 : 899 : Node v = sm->mkPurifySkolem(rw);
253 [ + + ]: 899 : if (num.getType().isInteger())
254 : : {
255 : 89 : num = nm->mkNode(Kind::TO_REAL, num);
256 : : }
257 [ + + ]: 899 : if (den.getType().isInteger())
258 : : {
259 : 131 : den = nm->mkNode(Kind::TO_REAL, den);
260 : : }
261 : 2697 : Node lem = nm->mkNode(
262 : : Kind::IMPLIES,
263 : 1798 : {den.eqNode(mkZero(den.getType())).negate(),
264 : 1798 : nm->mkNode(Kind::EQUAL, nm->mkNode(Kind::MULT, den, v), num)});
265 : 899 : lems.emplace_back(lem, v);
266 : 899 : return v;
267 : : break;
268 : 899 : }
269 : 1161 : case Kind::DIVISION:
270 : : {
271 : 1161 : Node num = node[0];
272 : 1161 : Node den = node[1];
273 : 2322 : Node ret = nm->mkNode(Kind::DIVISION_TOTAL, num, den);
274 [ + + ][ + - ]: 1161 : if (!den.isConst() || den.getConst<Rational>().sgn() == 0)
[ + - ]
275 : : {
276 : 1161 : wasNonLinear = true;
277 : 1161 : Node divByZeroNum = getArithSkolemApp(nm, num, SkolemId::DIV_BY_ZERO);
278 : 2322 : Node denEq0 = nm->mkNode(Kind::EQUAL, den, mkZero(den.getType()));
279 : 1161 : ret = nm->mkNode(Kind::ITE, denEq0, divByZeroNum, ret);
280 : 1161 : }
281 : 1161 : return ret;
282 : : break;
283 : 1161 : }
284 : :
285 : 672 : case Kind::INTS_DIVISION:
286 : : {
287 : : // partial function: integer div
288 : 672 : Node num = node[0];
289 : 672 : Node den = node[1];
290 : 1344 : Node ret = nm->mkNode(Kind::INTS_DIVISION_TOTAL, num, den);
291 [ + + ][ + - ]: 672 : if (!den.isConst() || den.getConst<Rational>().sgn() == 0)
[ + - ]
292 : : {
293 : 672 : wasNonLinear = true;
294 : : Node intDivByZeroNum =
295 : 672 : getArithSkolemApp(nm, num, SkolemId::INT_DIV_BY_ZERO);
296 : 1344 : Node denEq0 = nm->mkNode(Kind::EQUAL, den, nm->mkConstInt(Rational(0)));
297 : 672 : ret = nm->mkNode(Kind::ITE, denEq0, intDivByZeroNum, ret);
298 : 672 : }
299 : 672 : return ret;
300 : : break;
301 : 672 : }
302 : :
303 : 924 : case Kind::INTS_MODULUS:
304 : : {
305 : : // partial function: mod
306 : 924 : Node num = node[0];
307 : 924 : Node den = node[1];
308 : 1848 : Node ret = nm->mkNode(Kind::INTS_MODULUS_TOTAL, num, den);
309 [ + + ][ + - ]: 924 : if (!den.isConst() || den.getConst<Rational>().sgn() == 0)
[ + - ]
310 : : {
311 : 924 : wasNonLinear = true;
312 : 924 : Node modZeroNum = getArithSkolemApp(nm, num, SkolemId::MOD_BY_ZERO);
313 : 1848 : Node denEq0 = nm->mkNode(Kind::EQUAL, den, nm->mkConstInt(Rational(0)));
314 : 924 : ret = nm->mkNode(Kind::ITE, denEq0, modZeroNum, ret);
315 : 924 : }
316 : 924 : return ret;
317 : : break;
318 : 924 : }
319 : :
320 : 318 : case Kind::ABS:
321 : : {
322 : 1272 : return nm->mkNode(
323 : : Kind::ITE,
324 : 636 : {nm->mkNode(Kind::LT,
325 : : node[0],
326 : 636 : nm->mkConstRealOrInt(node[0].getType(), Rational(0))),
327 : 636 : nm->mkNode(Kind::NEG, node[0]),
328 [ + + ][ - - ]: 1908 : node[0]});
329 : : break;
330 : : }
331 : 248 : case Kind::SQRT:
332 : : case Kind::ARCSINE:
333 : : case Kind::ARCCOSINE:
334 : : case Kind::ARCTANGENT:
335 : : case Kind::ARCCOSECANT:
336 : : case Kind::ARCSECANT:
337 : : case Kind::ARCCOTANGENT:
338 : : {
339 [ + + ]: 248 : if (partialOnly)
340 : : {
341 : : // not eliminating total operators
342 : 20 : return node;
343 : : }
344 : 228 : wasNonLinear = true;
345 : : // We eliminate these functions using an uninterpreted function via
346 : : // the skolem id TRANSCENDENTAL_PURIFY.
347 : : // Make (lambda ((x Real)) (f x)) for this function, using the bound
348 : : // variable manager to ensure this function is always the same.
349 : 228 : BoundVarManager* bvm = nm->getBoundVarManager();
350 : : Node x = bvm->mkBoundVar(
351 : 456 : BoundVarId::ARITH_TR_PURIFY, node.getOperator(), "x", nm->realType());
352 : : Node lam =
353 : 684 : nm->mkNode(Kind::LAMBDA,
354 : 456 : {nm->mkNode(Kind::BOUND_VAR_LIST, x), nm->mkNode(k, x)});
355 : 228 : Node fun = sm->mkSkolemFunction(SkolemId::TRANSCENDENTAL_PURIFY, lam);
356 : : // Make (@TRANSCENDENTAL_PURIFY t), where t is node[0]
357 : 456 : Node var = nm->mkNode(Kind::APPLY_UF, fun, node[0]);
358 : 228 : Node lem;
359 [ + + ]: 228 : if (k == Kind::SQRT)
360 : : {
361 : 95 : Node zero = nm->mkConstReal(Rational(0));
362 : 190 : Node eq = nm->mkNode(Kind::MULT, var, var).eqNode(node[0]);
363 : 190 : Node resNonNeg = nm->mkNode(Kind::GEQ, var, zero);
364 : :
365 : : // (sqrt x) reduces to:
366 : : // (=> (>= x 0.0) (and (>= y 0.0) (= (* y y) x))
367 : : // where y is (@TRANSCENDENTAL_PURIFY x).
368 : : //
369 : : // This makes sure that the reduction still behaves like a function,
370 : : // otherwise the reduction of (x = -1) ^ (sqrt(x) != sqrt(-1)) would be
371 : : // satisfiable.
372 [ + + ][ - - ]: 475 : lem = nm->mkNode(Kind::IMPLIES,
373 : 190 : {nm->mkNode(Kind::GEQ, node[0], zero),
374 : 285 : nm->mkNode(Kind::AND, resNonNeg, eq)});
375 : 95 : }
376 : : else
377 : : {
378 : 133 : Node pi = mkPi(nm);
379 : :
380 : : // range of the skolem
381 : 133 : Node rlem;
382 [ + + ][ + + ]: 133 : if (k == Kind::ARCSINE || k == Kind::ARCTANGENT
383 [ - + ]: 47 : || k == Kind::ARCCOSECANT)
384 : : {
385 : 172 : Node half = nm->mkConstReal(Rational(1) / Rational(2));
386 : 172 : Node pi2 = nm->mkNode(Kind::MULT, half, pi);
387 : : Node npi2 =
388 : 172 : nm->mkNode(Kind::MULT, nm->mkConstReal(Rational(-1)), pi2);
389 : : // -pi/2 < var <= pi/2
390 [ + + ][ - - ]: 430 : rlem = nm->mkNode(Kind::AND,
391 : 172 : {nm->mkNode(Kind::LT, npi2, var),
392 : 258 : nm->mkNode(Kind::LEQ, var, pi2)});
393 : 86 : }
394 : : else
395 : : {
396 : : // 0 <= var < pi
397 [ + + ][ - - ]: 235 : rlem = nm->mkNode(
398 : : Kind::AND,
399 : 94 : {nm->mkNode(Kind::LEQ, nm->mkConstReal(Rational(0)), var),
400 : 141 : nm->mkNode(Kind::LT, var, pi)});
401 : : }
402 : 133 : Node cond;
403 [ + + ][ + + ]: 133 : if (k == Kind::ARCSINE || k == Kind::ARCCOSINE || k == Kind::ARCSECANT
[ + - ]
404 [ - + ]: 46 : || k == Kind::ARCCOSECANT)
405 : : {
406 : : // -1 <= x <= 1
407 [ + + ][ - - ]: 435 : cond = nm->mkNode(
408 : : Kind::AND,
409 : 174 : {nm->mkNode(Kind::GEQ, node[0], nm->mkConstReal(Rational(-1))),
410 : 261 : nm->mkNode(Kind::LEQ, node[0], nm->mkConstReal(Rational(1)))});
411 [ + - ][ - + ]: 87 : if (k == Kind::ARCSECANT || k == Kind::ARCCOSECANT)
412 : : {
413 : 0 : cond = cond.notNode();
414 : : }
415 : : }
416 : :
417 : : Kind rk;
418 : : switch (k)
419 : : {
420 : 40 : case Kind::ARCSINE: rk = Kind::SINE; break;
421 : 47 : case Kind::ARCCOSINE: rk = Kind::COSINE; break;
422 : 46 : case Kind::ARCTANGENT: rk = Kind::TANGENT; break;
423 : 0 : case Kind::ARCCOSECANT: rk = Kind::COSECANT; break;
424 : 0 : case Kind::ARCSECANT: rk = Kind::SECANT; break;
425 : 0 : case Kind::ARCCOTANGENT: rk = Kind::COTANGENT; break;
426 : 0 : default: Unreachable() << "Unexpected kind " << k;
427 : : }
428 : 133 : Node invTerm = nm->mkNode(rk, var);
429 : 133 : lem = nm->mkNode(Kind::AND, rlem, mkEquality(invTerm, node[0]));
430 [ + + ]: 133 : if (!cond.isNull())
431 : : {
432 : 87 : lem = nm->mkNode(Kind::IMPLIES, cond, lem);
433 : : }
434 [ + - ]: 266 : Trace("arith-op-elim")
435 : 133 : << "Elimination lemma " << lem << " for " << node << std::endl;
436 : 133 : }
437 [ - + ][ - + ]: 228 : Assert(!lem.isNull());
[ - - ]
438 : : // the skolem lemma is for the function
439 : 228 : lems.emplace_back(lem, fun);
440 : 228 : return var;
441 : 228 : }
442 : 3 : case Kind::REAL_ALGEBRAIC_NUMBER:
443 : : {
444 : 3 : BoundVarManager* bvm = nm->getBoundVarManager();
445 : : Node v = bvm->mkBoundVar(
446 : 6 : BoundVarId::REAL_ALGEBRAIC_NUMBER_WITNESS, node, "i", nm->realType());
447 : 3 : Node w;
448 : : #ifdef CVC5_POLY_IMP
449 : 6 : w = PolyConverter::ran_to_node(
450 : 9 : node.getOperator().getConst<RealAlgebraicNumber>(), v);
451 : : #endif
452 : : // it should not be possible to define real algebraic numbers unless poly
453 : : // is enabled
454 [ - + ][ - + ]: 3 : Assert(!w.isNull());
[ - - ]
455 : 3 : return w;
456 : 3 : }
457 : : // these are handled by rewriting
458 : 848996 : default: break;
459 : : }
460 : 848996 : return node;
461 : : }
462 : :
463 : 4159 : Node OperatorElim::getAxiomFor(NodeManager* nm, const Node& n)
464 : : {
465 : 4159 : std::vector<std::pair<Node, Node>> klems;
466 : 4159 : bool wasNonLinear = false;
467 : 4159 : Node nn = eliminateOperators(nm, n, klems, false, wasNonLinear);
468 [ - + ]: 4159 : if (nn == n)
469 : : {
470 : 0 : return Node::null();
471 : : }
472 : 4159 : Node eqLem = n.eqNode(nn);
473 : 4159 : std::vector<Node> lemmas;
474 [ + + ]: 7524 : for (const std::pair<Node, Node>& kl : klems)
475 : : {
476 : 3365 : lemmas.emplace_back(kl.first);
477 : : }
478 [ + + ]: 4159 : if (!lemmas.empty())
479 : : {
480 : 3365 : Node axiom = nm->mkAnd(lemmas);
481 : 3365 : return nm->mkNode(Kind::AND, eqLem, axiom);
482 : 3365 : }
483 : 794 : return eqLem;
484 : 4159 : }
485 : :
486 : 2757 : Node OperatorElim::getArithSkolemApp(NodeManager* nm, Node n, SkolemId id)
487 : : {
488 : 2757 : SkolemManager* sm = nm->getSkolemManager();
489 : 2757 : Node skolem = sm->mkSkolemFunction(id);
490 : 2757 : Assert(skolem.getType().isFunction()
491 : : && skolem.getType().getNumChildren() == 2);
492 : 2757 : TypeNode argType = skolem.getType()[0];
493 [ + + ][ + + ]: 2757 : if (!argType.isInteger() && n.getType().isInteger())
[ + + ][ + + ]
[ - - ]
494 : : {
495 : 123 : n = nm->mkNode(Kind::TO_REAL, n);
496 : : }
497 : 2757 : skolem = nm->mkNode(Kind::APPLY_UF, skolem, n);
498 : 5514 : return skolem;
499 : 2757 : }
500 : :
501 : 5156 : SkolemLemma OperatorElim::mkSkolemLemma(const Node& lem,
502 : : const Node& k,
503 : : const Node& n)
504 : : {
505 : 5156 : TrustNode tlem;
506 [ + + ]: 5156 : if (d_env.isTheoryProofProducing())
507 : : {
508 : 2054 : tlem = TrustNode::mkTrustLemma(lem, this);
509 : 2054 : d_lemmaMap[lem] = n;
510 : : }
511 : : else
512 : : {
513 : 3102 : tlem = TrustNode::mkTrustLemma(lem, nullptr);
514 : : }
515 : 10312 : return SkolemLemma(tlem, k);
516 : 5156 : }
517 : :
518 : 2607 : std::shared_ptr<ProofNode> OperatorElim::getProofFor(Node f)
519 : : {
520 : : // This class provides proofs for two things:
521 : : // (1) rewrites n --> nn during preprocessing,
522 : : // (2) the axioms A added when rewriting n ---> nn.
523 : : // The proof rule ARITH_REDUCTION proves things of the form:
524 : : // (and (= n nn) A)
525 : : // where A may be omitted. We first determine which case we are in (whether
526 : : // being asked for a proof of a preprocessing rewrite or an axiom) and store
527 : : // the target term (n above) into tgt.
528 : 2607 : context::CDHashMap<Node, Node>::iterator it = d_lemmaMap.find(f);
529 : 2607 : Node tgt;
530 [ + + ]: 2607 : if (it == d_lemmaMap.end())
531 : : {
532 [ - + ]: 1835 : if (f.getKind() != Kind::EQUAL)
533 : : {
534 : 0 : DebugUnhandled() << "arith::OperatorElim could not prove " << f;
535 : : return nullptr;
536 : : }
537 : : // target is the left hand side.
538 : 1835 : tgt = f[0];
539 : : }
540 : : else
541 : : {
542 : : // target was stored in d_lemmaMap for an axiom.
543 : 772 : tgt = it->second;
544 : : }
545 : 5214 : CDProof cdp(d_env);
546 : 2607 : Node res = getAxiomFor(nodeManager(), tgt);
547 : 5214 : cdp.addStep(res, ProofRule::ARITH_REDUCTION, {}, {tgt});
548 : 2607 : bool success = false;
549 : : // If the axiom was an AND, then the fact in question should be one of the
550 : : // conjuncts, in which case we do an AND_ELIM step.
551 [ + + ]: 2607 : if (res.getKind() == Kind::AND)
552 : : {
553 [ - + ][ - + ]: 2166 : Assert(res.getNumChildren() == 2);
[ - - ]
554 [ + - ]: 2938 : for (size_t i = 0; i < 2; i++)
555 : : {
556 [ + + ]: 2938 : if (res[i] == f)
557 : : {
558 : 2166 : Node ni = nodeManager()->mkConstInt(i);
559 : 6498 : cdp.addStep(f, ProofRule::AND_ELIM, {res}, {ni});
560 : 2166 : success = true;
561 : 2166 : break;
562 : 2166 : }
563 : : }
564 : : }
565 : : else
566 : : {
567 : 441 : success = (res == f);
568 : : }
569 : 2607 : Assert(success) << "arith::OperatorElim could not prove " << f;
570 [ - + ]: 2607 : if (!success)
571 : : {
572 : 0 : return nullptr;
573 : : }
574 : 2607 : return cdp.getProofFor(f);
575 : 2607 : }
576 : :
577 : 104 : std::string OperatorElim::identify() const { return "arith::OperatorElim"; }
578 : :
579 : : } // namespace arith
580 : : } // namespace theory
581 : : } // namespace cvc5::internal
|
