GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/arith/nl/transcendental/proof_checker.cpp Lines: 260 262 99.2 %
Date: 2021-03-23 Branches: 744 2284 32.6 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file proof_checker.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Gereon Kremer, Tim King
6
 ** This file is part of the CVC4 project.
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.\endverbatim
11
 **
12
 ** \brief Implementation of proof checker for transcendentals
13
 **/
14
15
#include "theory/arith/nl/transcendental/proof_checker.h"
16
17
#include "expr/sequence.h"
18
#include "theory/arith/arith_utilities.h"
19
#include "theory/arith/nl/transcendental/taylor_generator.h"
20
#include "theory/rewriter.h"
21
22
using namespace CVC4::kind;
23
24
namespace CVC4 {
25
namespace theory {
26
namespace arith {
27
namespace nl {
28
namespace transcendental {
29
30
namespace {
31
32
/**
33
 * Helper method to construct (t >= lb) AND (t <= up)
34
 */
35
56
Node mkBounds(TNode t, TNode lb, TNode ub)
36
{
37
56
  NodeManager* nm = NodeManager::currentNM();
38
224
  return nm->mkAnd(std::vector<Node>{nm->mkNode(Kind::GEQ, t, lb),
39
224
                                     nm->mkNode(Kind::LEQ, t, ub)});
40
}
41
42
/**
43
 * Helper method to construct a secant plane:
44
 * ((evall - evalu) / (l - u)) * (t - l) + evall
45
 */
46
48
Node mkSecant(TNode t, TNode l, TNode u, TNode evall, TNode evalu)
47
{
48
48
  NodeManager* nm = NodeManager::currentNM();
49
  return nm->mkNode(Kind::PLUS,
50
192
                    nm->mkNode(Kind::MULT,
51
192
                               nm->mkNode(Kind::DIVISION,
52
96
                                          nm->mkNode(Kind::MINUS, evall, evalu),
53
96
                                          nm->mkNode(Kind::MINUS, l, u)),
54
96
                               nm->mkNode(Kind::MINUS, t, l)),
55
144
                    evall);
56
}
57
58
}  // namespace
59
60
401
void TranscendentalProofRuleChecker::registerTo(ProofChecker* pc)
61
{
62
401
  pc->registerChecker(PfRule::ARITH_TRANS_PI, this);
63
401
  pc->registerChecker(PfRule::ARITH_TRANS_EXP_NEG, this);
64
401
  pc->registerChecker(PfRule::ARITH_TRANS_EXP_POSITIVITY, this);
65
401
  pc->registerChecker(PfRule::ARITH_TRANS_EXP_SUPER_LIN, this);
66
401
  pc->registerChecker(PfRule::ARITH_TRANS_EXP_ZERO, this);
67
401
  pc->registerChecker(PfRule::ARITH_TRANS_EXP_APPROX_ABOVE_POS, this);
68
401
  pc->registerChecker(PfRule::ARITH_TRANS_EXP_APPROX_ABOVE_NEG, this);
69
401
  pc->registerChecker(PfRule::ARITH_TRANS_EXP_APPROX_BELOW, this);
70
401
  pc->registerChecker(PfRule::ARITH_TRANS_SINE_BOUNDS, this);
71
401
  pc->registerChecker(PfRule::ARITH_TRANS_SINE_SHIFT, this);
72
401
  pc->registerChecker(PfRule::ARITH_TRANS_SINE_SYMMETRY, this);
73
401
  pc->registerChecker(PfRule::ARITH_TRANS_SINE_TANGENT_ZERO, this);
74
401
  pc->registerChecker(PfRule::ARITH_TRANS_SINE_TANGENT_PI, this);
75
401
  pc->registerChecker(PfRule::ARITH_TRANS_SINE_APPROX_BELOW_POS, this);
76
401
  pc->registerChecker(PfRule::ARITH_TRANS_SINE_APPROX_BELOW_NEG, this);
77
401
  pc->registerChecker(PfRule::ARITH_TRANS_SINE_APPROX_ABOVE_POS, this);
78
401
  pc->registerChecker(PfRule::ARITH_TRANS_SINE_APPROX_ABOVE_NEG, this);
79
401
}
80
81
339
Node TranscendentalProofRuleChecker::checkInternal(
82
    PfRule id, const std::vector<Node>& children, const std::vector<Node>& args)
83
{
84
339
  NodeManager* nm = NodeManager::currentNM();
85
678
  auto zero = nm->mkConst<Rational>(0);
86
678
  auto one = nm->mkConst<Rational>(1);
87
678
  auto mone = nm->mkConst<Rational>(-1);
88
678
  auto pi = nm->mkNullaryOperator(nm->realType(), Kind::PI);
89
678
  auto mpi = nm->mkNode(Kind::MULT, mone, pi);
90
339
  Trace("nl-trans-checker") << "Checking " << id << std::endl;
91
339
  Trace("nl-trans-checker") << "Children:" << std::endl;
92
339
  for (const auto& c : children)
93
  {
94
    Trace("nl-trans-checker") << "\t" << c << std::endl;
95
  }
96
339
  Trace("nl-trans-checker") << "Args:" << std::endl;
97
977
  for (const auto& a : args)
98
  {
99
638
    Trace("nl-trans-checker") << "\t" << a << std::endl;
100
  }
101
339
  if (id == PfRule::ARITH_TRANS_PI)
102
  {
103
16
    Assert(children.empty());
104
16
    Assert(args.size() == 2);
105
80
    return nm->mkAnd(std::vector<Node>{nm->mkNode(Kind::GEQ, pi, args[0]),
106
64
                                       nm->mkNode(Kind::LEQ, pi, args[1])});
107
  }
108
323
  else if (id == PfRule::ARITH_TRANS_EXP_NEG)
109
  {
110
18
    Assert(children.empty());
111
18
    Assert(args.size() == 1);
112
36
    Node e = nm->mkNode(Kind::EXPONENTIAL, args[0]);
113
    return nm->mkNode(
114
18
        EQUAL, nm->mkNode(LT, args[0], zero), nm->mkNode(LT, e, one));
115
  }
116
305
  else if (id == PfRule::ARITH_TRANS_EXP_POSITIVITY)
117
  {
118
18
    Assert(children.empty());
119
18
    Assert(args.size() == 1);
120
36
    Node e = nm->mkNode(Kind::EXPONENTIAL, args[0]);
121
18
    return nm->mkNode(GT, e, zero);
122
  }
123
287
  else if (id == PfRule::ARITH_TRANS_EXP_SUPER_LIN)
124
  {
125
18
    Assert(children.empty());
126
18
    Assert(args.size() == 1);
127
36
    Node e = nm->mkNode(Kind::EXPONENTIAL, args[0]);
128
    return nm->mkNode(OR,
129
36
                      nm->mkNode(LEQ, args[0], zero),
130
54
                      nm->mkNode(GT, e, nm->mkNode(PLUS, args[0], one)));
131
  }
132
269
  else if (id == PfRule::ARITH_TRANS_EXP_ZERO)
133
  {
134
18
    Assert(children.empty());
135
18
    Assert(args.size() == 1);
136
36
    Node e = nm->mkNode(Kind::EXPONENTIAL, args[0]);
137
18
    return nm->mkNode(EQUAL, args[0].eqNode(zero), e.eqNode(one));
138
  }
139
251
  else if (id == PfRule::ARITH_TRANS_EXP_APPROX_ABOVE_POS)
140
  {
141
19
    Assert(children.empty());
142
19
    Assert(args.size() == 4);
143
19
    Assert(args[0].isConst() && args[0].getKind() == Kind::CONST_RATIONAL
144
           && args[0].getConst<Rational>().isIntegral());
145
19
    Assert(args[1].getType().isReal());
146
19
    Assert(args[2].isConst() && args[2].getKind() == Kind::CONST_RATIONAL);
147
19
    Assert(args[3].isConst() && args[3].getKind() == Kind::CONST_RATIONAL);
148
    std::uint64_t d =
149
19
        args[0].getConst<Rational>().getNumerator().toUnsignedInt();
150
38
    Node t = args[1];
151
38
    Node l = args[2];
152
38
    Node u = args[3];
153
38
    TaylorGenerator tg;
154
38
    TaylorGenerator::ApproximationBounds bounds;
155
19
    tg.getPolynomialApproximationBounds(Kind::EXPONENTIAL, d / 2, bounds);
156
    Node evall = Rewriter::rewrite(
157
38
        bounds.d_upperPos.substitute(tg.getTaylorVariable(), l));
158
    Node evalu = Rewriter::rewrite(
159
38
        bounds.d_upperPos.substitute(tg.getTaylorVariable(), u));
160
38
    Node evalsecant = mkSecant(t, l, u, evall, evalu);
161
    Node lem = nm->mkNode(
162
        Kind::IMPLIES,
163
38
        mkBounds(t, l, u),
164
76
        nm->mkNode(Kind::LEQ, nm->mkNode(Kind::EXPONENTIAL, t), evalsecant));
165
19
    return Rewriter::rewrite(lem);
166
  }
167
232
  else if (id == PfRule::ARITH_TRANS_EXP_APPROX_ABOVE_NEG)
168
  {
169
5
    Assert(children.empty());
170
5
    Assert(args.size() == 4);
171
5
    Assert(args[0].isConst() && args[0].getKind() == Kind::CONST_RATIONAL
172
           && args[0].getConst<Rational>().isIntegral());
173
5
    Assert(args[1].getType().isReal());
174
5
    Assert(args[2].isConst() && args[2].getKind() == Kind::CONST_RATIONAL);
175
5
    Assert(args[3].isConst() && args[3].getKind() == Kind::CONST_RATIONAL);
176
    std::uint64_t d =
177
5
        args[0].getConst<Rational>().getNumerator().toUnsignedInt();
178
10
    Node t = args[1];
179
10
    Node l = args[2];
180
10
    Node u = args[3];
181
10
    TaylorGenerator tg;
182
10
    TaylorGenerator::ApproximationBounds bounds;
183
5
    tg.getPolynomialApproximationBounds(Kind::EXPONENTIAL, d / 2, bounds);
184
    Node evall = Rewriter::rewrite(
185
10
        bounds.d_upperNeg.substitute(tg.getTaylorVariable(), l));
186
    Node evalu = Rewriter::rewrite(
187
10
        bounds.d_upperNeg.substitute(tg.getTaylorVariable(), u));
188
10
    Node evalsecant = mkSecant(t, l, u, evall, evalu);
189
    Node lem = nm->mkNode(
190
        Kind::IMPLIES,
191
10
        mkBounds(t, l, u),
192
20
        nm->mkNode(Kind::LEQ, nm->mkNode(Kind::EXPONENTIAL, t), evalsecant));
193
5
    return Rewriter::rewrite(lem);
194
  }
195
227
  else if (id == PfRule::ARITH_TRANS_EXP_APPROX_BELOW)
196
  {
197
11
    Assert(children.empty());
198
11
    Assert(args.size() == 2);
199
11
    Assert(args[0].isConst() && args[0].getKind() == Kind::CONST_RATIONAL
200
           && args[0].getConst<Rational>().isIntegral());
201
11
    Assert(args[1].getType().isReal());
202
    std::uint64_t d =
203
11
        args[0].getConst<Rational>().getNumerator().toUnsignedInt();
204
22
    Node t = args[1];
205
22
    TaylorGenerator tg;
206
22
    TaylorGenerator::ApproximationBounds bounds;
207
11
    tg.getPolynomialApproximationBounds(Kind::EXPONENTIAL, d, bounds);
208
    Node eval =
209
22
        Rewriter::rewrite(bounds.d_lower.substitute(tg.getTaylorVariable(), t));
210
    return nm->mkNode(
211
11
        Kind::GEQ, std::vector<Node>{nm->mkNode(Kind::EXPONENTIAL, t), eval});
212
  }
213
216
  else if (id == PfRule::ARITH_TRANS_SINE_BOUNDS)
214
  {
215
40
    Assert(children.empty());
216
40
    Assert(args.size() == 1);
217
40
    Assert(args[0].getType().isReal());
218
80
    Node s = nm->mkNode(Kind::SINE, args[0]);
219
40
    return nm->mkNode(AND, nm->mkNode(LEQ, s, one), nm->mkNode(GEQ, s, mone));
220
  }
221
176
  else if (id == PfRule::ARITH_TRANS_SINE_SHIFT)
222
  {
223
24
    Assert(children.empty());
224
24
    Assert(args.size() == 3);
225
24
    const auto& x = args[0];
226
24
    const auto& y = args[1];
227
24
    const auto& s = args[2];
228
288
    return nm->mkAnd(std::vector<Node>{
229
96
        nm->mkAnd(std::vector<Node>{
230
48
            nm->mkNode(Kind::GEQ, y, nm->mkNode(Kind::MULT, mone, pi)),
231
48
            nm->mkNode(Kind::LEQ, y, pi)}),
232
        nm->mkNode(
233
            Kind::ITE,
234
96
            nm->mkAnd(std::vector<Node>{
235
48
                nm->mkNode(Kind::GEQ, x, nm->mkNode(Kind::MULT, mone, pi)),
236
                nm->mkNode(Kind::LEQ, x, pi),
237
48
            }),
238
48
            x.eqNode(y),
239
48
            x.eqNode(nm->mkNode(
240
                Kind::PLUS,
241
                y,
242
48
                nm->mkNode(Kind::MULT, nm->mkConst<Rational>(2), s, pi)))),
243
144
        nm->mkNode(Kind::SINE, y).eqNode(nm->mkNode(Kind::SINE, x))});
244
  }
245
152
  else if (id == PfRule::ARITH_TRANS_SINE_SYMMETRY)
246
  {
247
40
    Assert(children.empty());
248
40
    Assert(args.size() == 1);
249
40
    Assert(args[0].getType().isReal());
250
80
    Node s1 = nm->mkNode(Kind::SINE, args[0]);
251
    Node s2 = nm->mkNode(
252
80
        Kind::SINE, Rewriter::rewrite(nm->mkNode(Kind::MULT, mone, args[0])));
253
40
    return nm->mkNode(PLUS, s1, s2).eqNode(zero);
254
  }
255
112
  else if (id == PfRule::ARITH_TRANS_SINE_TANGENT_ZERO)
256
  {
257
40
    Assert(children.empty());
258
40
    Assert(args.size() == 1);
259
40
    Assert(args[0].getType().isReal());
260
80
    Node s = nm->mkNode(Kind::SINE, args[0]);
261
    return nm->mkNode(
262
        AND,
263
160
        nm->mkNode(
264
160
            IMPLIES, nm->mkNode(GT, args[0], zero), nm->mkNode(LT, s, args[0])),
265
160
        nm->mkNode(IMPLIES,
266
80
                   nm->mkNode(LT, args[0], zero),
267
200
                   nm->mkNode(GT, s, args[0])));
268
  }
269
72
  else if (id == PfRule::ARITH_TRANS_SINE_TANGENT_PI)
270
  {
271
40
    Assert(children.empty());
272
40
    Assert(args.size() == 1);
273
40
    Assert(args[0].getType().isReal());
274
80
    Node s = nm->mkNode(Kind::SINE, args[0]);
275
    return nm->mkNode(
276
        AND,
277
160
        nm->mkNode(IMPLIES,
278
80
                   nm->mkNode(GT, args[0], mpi),
279
80
                   nm->mkNode(GT, s, nm->mkNode(MINUS, mpi, args[0]))),
280
160
        nm->mkNode(IMPLIES,
281
80
                   nm->mkNode(LT, args[0], pi),
282
200
                   nm->mkNode(LT, s, nm->mkNode(MINUS, pi, args[0]))));
283
  }
284
32
  else if (id == PfRule::ARITH_TRANS_SINE_APPROX_ABOVE_NEG)
285
  {
286
12
    Assert(children.empty());
287
12
    Assert(args.size() == 6);
288
12
    Assert(args[0].isConst() && args[0].getKind() == Kind::CONST_RATIONAL
289
           && args[0].getConst<Rational>().isIntegral());
290
12
    Assert(args[1].getType().isReal());
291
12
    Assert(args[2].getType().isReal());
292
12
    Assert(args[3].getType().isReal());
293
12
    Assert(args[4].isConst() && args[4].getKind() == Kind::CONST_RATIONAL);
294
12
    Assert(args[5].isConst() && args[5].getKind() == Kind::CONST_RATIONAL);
295
    std::uint64_t d =
296
12
        args[0].getConst<Rational>().getNumerator().toUnsignedInt();
297
24
    Node t = args[1];
298
24
    Node lb = args[2];
299
24
    Node ub = args[3];
300
24
    Node l = args[4];
301
24
    Node u = args[5];
302
24
    TaylorGenerator tg;
303
24
    TaylorGenerator::ApproximationBounds bounds;
304
12
    tg.getPolynomialApproximationBounds(Kind::SINE, d / 2, bounds);
305
    Node evall = Rewriter::rewrite(
306
24
        bounds.d_upperNeg.substitute(tg.getTaylorVariable(), l));
307
    Node evalu = Rewriter::rewrite(
308
24
        bounds.d_upperNeg.substitute(tg.getTaylorVariable(), u));
309
    Node lem = nm->mkNode(
310
        Kind::IMPLIES,
311
24
        mkBounds(t, lb, ub),
312
48
        nm->mkNode(
313
96
            Kind::LEQ, nm->mkNode(Kind::SINE, t), mkSecant(t, lb, ub, l, u)));
314
12
    return Rewriter::rewrite(lem);
315
  }
316
20
  else if (id == PfRule::ARITH_TRANS_SINE_APPROX_ABOVE_POS)
317
  {
318
4
    Assert(children.empty());
319
4
    Assert(args.size() == 5);
320
4
    Assert(args[0].isConst() && args[0].getKind() == Kind::CONST_RATIONAL
321
           && args[0].getConst<Rational>().isIntegral());
322
4
    Assert(args[1].getType().isReal());
323
4
    Assert(args[2].getType().isReal());
324
4
    Assert(args[3].getType().isReal());
325
    std::uint64_t d =
326
4
        args[0].getConst<Rational>().getNumerator().toUnsignedInt();
327
8
    Node t = args[1];
328
8
    Node c = args[2];
329
8
    Node lb = args[3];
330
8
    Node ub = args[4];
331
8
    TaylorGenerator tg;
332
8
    TaylorGenerator::ApproximationBounds bounds;
333
4
    tg.getPolynomialApproximationBounds(Kind::SINE, d / 2, bounds);
334
    Node eval = Rewriter::rewrite(
335
8
        bounds.d_upperPos.substitute(tg.getTaylorVariable(), c));
336
    return Rewriter::rewrite(
337
16
        nm->mkNode(Kind::IMPLIES,
338
8
                   mkBounds(t, lb, ub),
339
12
                   nm->mkNode(Kind::LEQ, nm->mkNode(Kind::SINE, t), eval)));
340
  }
341
16
  else if (id == PfRule::ARITH_TRANS_SINE_APPROX_BELOW_POS)
342
  {
343
12
    Assert(children.empty());
344
12
    Assert(args.size() == 6);
345
12
    Assert(args[0].isConst() && args[0].getKind() == Kind::CONST_RATIONAL
346
           && args[0].getConst<Rational>().isIntegral());
347
12
    Assert(args[1].getType().isReal());
348
12
    Assert(args[2].getType().isReal());
349
12
    Assert(args[3].getType().isReal());
350
12
    Assert(args[4].isConst() && args[4].getKind() == Kind::CONST_RATIONAL);
351
12
    Assert(args[5].isConst() && args[5].getKind() == Kind::CONST_RATIONAL);
352
    std::uint64_t d =
353
12
        args[0].getConst<Rational>().getNumerator().toUnsignedInt();
354
24
    Node t = args[1];
355
24
    Node lb = args[2];
356
24
    Node ub = args[3];
357
24
    Node l = args[4];
358
24
    Node u = args[5];
359
24
    TaylorGenerator tg;
360
24
    TaylorGenerator::ApproximationBounds bounds;
361
12
    tg.getPolynomialApproximationBounds(Kind::SINE, d / 2, bounds);
362
    Node evall =
363
24
        Rewriter::rewrite(bounds.d_lower.substitute(tg.getTaylorVariable(), l));
364
    Node evalu =
365
24
        Rewriter::rewrite(bounds.d_lower.substitute(tg.getTaylorVariable(), u));
366
    Node lem = nm->mkNode(
367
        Kind::IMPLIES,
368
24
        mkBounds(t, lb, ub),
369
48
        nm->mkNode(
370
96
            Kind::GEQ, nm->mkNode(Kind::SINE, t), mkSecant(t, lb, ub, l, u)));
371
12
    return Rewriter::rewrite(lem);
372
  }
373
4
  else if (id == PfRule::ARITH_TRANS_SINE_APPROX_BELOW_NEG)
374
  {
375
4
    Assert(children.empty());
376
4
    Assert(args.size() == 5);
377
4
    Assert(args[0].isConst() && args[0].getKind() == Kind::CONST_RATIONAL
378
           && args[0].getConst<Rational>().isIntegral());
379
4
    Assert(args[1].getType().isReal());
380
4
    Assert(args[2].getType().isReal());
381
4
    Assert(args[3].getType().isReal());
382
    std::uint64_t d =
383
4
        args[0].getConst<Rational>().getNumerator().toUnsignedInt();
384
8
    Node t = args[1];
385
8
    Node c = args[2];
386
8
    Node lb = args[3];
387
8
    Node ub = args[4];
388
8
    TaylorGenerator tg;
389
8
    TaylorGenerator::ApproximationBounds bounds;
390
4
    tg.getPolynomialApproximationBounds(Kind::SINE, d / 2, bounds);
391
    Node eval =
392
8
        Rewriter::rewrite(bounds.d_lower.substitute(tg.getTaylorVariable(), c));
393
    return Rewriter::rewrite(
394
16
        nm->mkNode(Kind::IMPLIES,
395
8
                   mkBounds(t, lb, ub),
396
12
                   nm->mkNode(Kind::GEQ, nm->mkNode(Kind::SINE, t), eval)));
397
  }
398
  return Node::null();
399
}
400
401
}  // namespace transcendental
402
}  // namespace nl
403
}  // namespace arith
404
}  // namespace theory
405
26685
}  // namespace CVC4