GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/arith/proof_checker.cpp Lines: 110 186 59.1 %
Date: 2021-03-22 Branches: 238 934 25.5 %

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