GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/builtin/proof_checker.cpp Lines: 182 271 67.2 %
Date: 2021-03-23 Branches: 312 1057 29.5 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file proof_checker.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds
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 equality proof checker
13
 **/
14
15
#include "theory/builtin/proof_checker.h"
16
17
#include "expr/skolem_manager.h"
18
#include "smt/term_formula_removal.h"
19
#include "theory/evaluator.h"
20
#include "theory/rewriter.h"
21
#include "theory/theory.h"
22
23
using namespace CVC4::kind;
24
25
namespace CVC4 {
26
namespace theory {
27
28
const char* toString(MethodId id)
29
{
30
  switch (id)
31
  {
32
    case MethodId::RW_REWRITE: return "RW_REWRITE";
33
    case MethodId::RW_EXT_REWRITE: return "RW_EXT_REWRITE";
34
    case MethodId::RW_REWRITE_EQ_EXT: return "RW_REWRITE_EQ_EXT";
35
    case MethodId::RW_EVALUATE: return "RW_EVALUATE";
36
    case MethodId::RW_IDENTITY: return "RW_IDENTITY";
37
    case MethodId::RW_REWRITE_THEORY_PRE: return "RW_REWRITE_THEORY_PRE";
38
    case MethodId::RW_REWRITE_THEORY_POST: return "RW_REWRITE_THEORY_POST";
39
    case MethodId::SB_DEFAULT: return "SB_DEFAULT";
40
    case MethodId::SB_LITERAL: return "SB_LITERAL";
41
    case MethodId::SB_FORMULA: return "SB_FORMULA";
42
    default: return "MethodId::Unknown";
43
  };
44
}
45
46
std::ostream& operator<<(std::ostream& out, MethodId id)
47
{
48
  out << toString(id);
49
  return out;
50
}
51
52
178960
Node mkMethodId(MethodId id)
53
{
54
178960
  return NodeManager::currentNM()->mkConst(Rational(static_cast<uint32_t>(id)));
55
}
56
57
namespace builtin {
58
59
962
void BuiltinProofRuleChecker::registerTo(ProofChecker* pc)
60
{
61
962
  pc->registerChecker(PfRule::ASSUME, this);
62
962
  pc->registerChecker(PfRule::SCOPE, this);
63
962
  pc->registerChecker(PfRule::SUBS, this);
64
962
  pc->registerChecker(PfRule::REWRITE, this);
65
962
  pc->registerChecker(PfRule::EVALUATE, this);
66
962
  pc->registerChecker(PfRule::MACRO_SR_EQ_INTRO, this);
67
962
  pc->registerChecker(PfRule::MACRO_SR_PRED_INTRO, this);
68
962
  pc->registerChecker(PfRule::MACRO_SR_PRED_ELIM, this);
69
962
  pc->registerChecker(PfRule::MACRO_SR_PRED_TRANSFORM, this);
70
962
  pc->registerChecker(PfRule::THEORY_REWRITE, this);
71
962
  pc->registerChecker(PfRule::REMOVE_TERM_FORMULA_AXIOM, this);
72
  // trusted rules
73
962
  pc->registerTrustedChecker(PfRule::THEORY_LEMMA, this, 1);
74
962
  pc->registerTrustedChecker(PfRule::PREPROCESS, this, 3);
75
962
  pc->registerTrustedChecker(PfRule::PREPROCESS_LEMMA, this, 3);
76
962
  pc->registerTrustedChecker(PfRule::THEORY_PREPROCESS, this, 3);
77
962
  pc->registerTrustedChecker(PfRule::THEORY_PREPROCESS_LEMMA, this, 3);
78
962
  pc->registerTrustedChecker(PfRule::THEORY_EXPAND_DEF, this, 3);
79
962
  pc->registerTrustedChecker(PfRule::WITNESS_AXIOM, this, 3);
80
962
  pc->registerTrustedChecker(PfRule::TRUST_REWRITE, this, 1);
81
962
  pc->registerTrustedChecker(PfRule::TRUST_SUBS, this, 1);
82
962
  pc->registerTrustedChecker(PfRule::TRUST_SUBS_MAP, this, 1);
83
962
}
84
85
1138505
Node BuiltinProofRuleChecker::applySubstitutionRewrite(
86
    Node n, const std::vector<Node>& exp, MethodId ids, MethodId idr)
87
{
88
2277010
  Node nks = applySubstitution(n, exp, ids);
89
2277010
  return applyRewrite(nks, idr);
90
}
91
92
1284331
Node BuiltinProofRuleChecker::applyRewrite(Node n, MethodId idr)
93
{
94
2568662
  Trace("builtin-pfcheck-debug")
95
1284331
      << "applyRewrite (" << idr << "): " << n << std::endl;
96
1284331
  if (idr == MethodId::RW_REWRITE)
97
  {
98
1284238
    return Rewriter::rewrite(n);
99
  }
100
93
  if (idr == MethodId::RW_EXT_REWRITE)
101
  {
102
    return d_ext_rewriter.extendedRewrite(n);
103
  }
104
93
  if (idr == MethodId::RW_REWRITE_EQ_EXT)
105
  {
106
93
    return Rewriter::rewriteEqualityExt(n);
107
  }
108
  if (idr == MethodId::RW_EVALUATE)
109
  {
110
    Evaluator eval;
111
    return eval.eval(n, {}, {}, false);
112
  }
113
  if (idr == MethodId::RW_IDENTITY)
114
  {
115
    // does nothing
116
    return n;
117
  }
118
  // unknown rewriter
119
  Assert(false) << "BuiltinProofRuleChecker::applyRewrite: no rewriter for "
120
                << idr << std::endl;
121
  return n;
122
}
123
124
2369032
bool BuiltinProofRuleChecker::getSubstitutionForLit(Node exp,
125
                                                    TNode& var,
126
                                                    TNode& subs,
127
                                                    MethodId ids)
128
{
129
2369032
  if (ids == MethodId::SB_DEFAULT)
130
  {
131
2334348
    if (exp.getKind() != EQUAL)
132
    {
133
      return false;
134
    }
135
2334348
    var = exp[0];
136
2334348
    subs = exp[1];
137
  }
138
34684
  else if (ids == MethodId::SB_LITERAL)
139
  {
140
34684
    bool polarity = exp.getKind() != NOT;
141
34684
    var = polarity ? exp : exp[0];
142
34684
    subs = NodeManager::currentNM()->mkConst(polarity);
143
  }
144
  else if (ids == MethodId::SB_FORMULA)
145
  {
146
    var = exp;
147
    subs = NodeManager::currentNM()->mkConst(true);
148
  }
149
  else
150
  {
151
    Assert(false) << "BuiltinProofRuleChecker::applySubstitution: no "
152
                     "substitution for "
153
                  << ids << std::endl;
154
    return false;
155
  }
156
2369032
  return true;
157
}
158
159
2369032
bool BuiltinProofRuleChecker::getSubstitutionFor(Node exp,
160
                                                 std::vector<TNode>& vars,
161
                                                 std::vector<TNode>& subs,
162
                                                 std::vector<TNode>& from,
163
                                                 MethodId ids)
164
{
165
4738064
  TNode v;
166
4738064
  TNode s;
167
2369032
  if (exp.getKind() == AND && ids == MethodId::SB_DEFAULT)
168
  {
169
    for (const Node& ec : exp)
170
    {
171
      // non-recursive, do not use nested AND
172
      if (!getSubstitutionForLit(ec, v, s, ids))
173
      {
174
        return false;
175
      }
176
      vars.push_back(v);
177
      subs.push_back(s);
178
      from.push_back(ec);
179
    }
180
    return true;
181
  }
182
2369032
  bool ret = getSubstitutionForLit(exp, v, s, ids);
183
2369032
  vars.push_back(v);
184
2369032
  subs.push_back(s);
185
2369032
  from.push_back(exp);
186
2369032
  return ret;
187
}
188
189
2258619
Node BuiltinProofRuleChecker::applySubstitution(Node n, Node exp, MethodId ids)
190
{
191
4517238
  std::vector<TNode> vars;
192
4517238
  std::vector<TNode> subs;
193
4517238
  std::vector<TNode> from;
194
2258619
  if (!getSubstitutionFor(exp, vars, subs, from, ids))
195
  {
196
    return Node::null();
197
  }
198
4517238
  Node ns = n;
199
  // apply substitution one at a time, in reverse order
200
4517238
  for (size_t i = 0, nvars = vars.size(); i < nvars; i++)
201
  {
202
4517238
    TNode v = vars[nvars - 1 - i];
203
4517238
    TNode s = subs[nvars - 1 - i];
204
4517238
    Trace("builtin-pfcheck-debug")
205
2258619
        << "applySubstitution (" << ids << "): " << v << " -> " << s
206
2258619
        << " (from " << exp << ")" << std::endl;
207
2258619
    ns = ns.substitute(v, s);
208
  }
209
2258619
  return ns;
210
}
211
212
1150972
Node BuiltinProofRuleChecker::applySubstitution(Node n,
213
                                                const std::vector<Node>& exp,
214
                                                MethodId ids)
215
{
216
2301944
  Node curr = n;
217
  // apply substitution one at a time, in reverse order
218
3409591
  for (size_t i = 0, nexp = exp.size(); i < nexp; i++)
219
  {
220
2258619
    if (exp[nexp - 1 - i].isNull())
221
    {
222
      return Node::null();
223
    }
224
2258619
    curr = applySubstitution(curr, exp[nexp - 1 - i], ids);
225
2258619
    if (curr.isNull())
226
    {
227
      break;
228
    }
229
  }
230
1150972
  return curr;
231
}
232
233
23777
bool BuiltinProofRuleChecker::getMethodId(TNode n, MethodId& i)
234
{
235
  uint32_t index;
236
23777
  if (!getUInt32(n, index))
237
  {
238
    return false;
239
  }
240
23777
  i = static_cast<MethodId>(index);
241
23777
  return true;
242
}
243
244
1034187
Node BuiltinProofRuleChecker::checkInternal(PfRule id,
245
                                            const std::vector<Node>& children,
246
                                            const std::vector<Node>& args)
247
{
248
1034187
  NodeManager * nm = NodeManager::currentNM();
249
  // compute what was proven
250
1034187
  if (id == PfRule::ASSUME)
251
  {
252
    Assert(children.empty());
253
    Assert(args.size() == 1);
254
    Assert(args[0].getType().isBoolean());
255
    return args[0];
256
  }
257
1034187
  else if (id == PfRule::SCOPE)
258
  {
259
195500
    Assert(children.size() == 1);
260
195500
    if (args.empty())
261
    {
262
      // no antecedant
263
      return children[0];
264
    }
265
391000
    Node ant = nm->mkAnd(args);
266
    // if the conclusion is false, its the negated antencedant only
267
195500
    if (children[0].isConst() && !children[0].getConst<bool>())
268
    {
269
85630
      return ant.notNode();
270
    }
271
109870
    return nm->mkNode(IMPLIES, ant, children[0]);
272
  }
273
838687
  else if (id == PfRule::SUBS)
274
  {
275
    Assert(children.size() > 0);
276
    Assert(1 <= args.size() && args.size() <= 2);
277
    MethodId ids = MethodId::SB_DEFAULT;
278
    if (args.size() == 2 && !getMethodId(args[1], ids))
279
    {
280
      return Node::null();
281
    }
282
    std::vector<Node> exp;
283
    for (size_t i = 0, nchild = children.size(); i < nchild; i++)
284
    {
285
      exp.push_back(children[i]);
286
    }
287
    Node res = applySubstitution(args[0], exp, ids);
288
    if (res.isNull())
289
    {
290
      return Node::null();
291
    }
292
    return args[0].eqNode(res);
293
  }
294
838687
  else if (id == PfRule::REWRITE)
295
  {
296
13899
    Assert(children.empty());
297
13899
    Assert(1 <= args.size() && args.size() <= 2);
298
13899
    MethodId idr = MethodId::RW_REWRITE;
299
13899
    if (args.size() == 2 && !getMethodId(args[1], idr))
300
    {
301
      return Node::null();
302
    }
303
27798
    Node res = applyRewrite(args[0], idr);
304
13899
    if (res.isNull())
305
    {
306
      return Node::null();
307
    }
308
13899
    return args[0].eqNode(res);
309
  }
310
824788
  else if (id == PfRule::EVALUATE)
311
  {
312
    Assert(children.empty());
313
    Assert(args.size() == 1);
314
    Node res = applyRewrite(args[0], MethodId::RW_EVALUATE);
315
    if (res.isNull())
316
    {
317
      return Node::null();
318
    }
319
    return args[0].eqNode(res);
320
  }
321
824788
  else if (id == PfRule::MACRO_SR_EQ_INTRO)
322
  {
323
48446
    Assert(1 <= args.size() && args.size() <= 3);
324
    MethodId ids, idr;
325
48446
    if (!getMethodIds(args, ids, idr, 1))
326
    {
327
      return Node::null();
328
    }
329
96892
    Node res = applySubstitutionRewrite(args[0], children, ids, idr);
330
48446
    if (res.isNull())
331
    {
332
      return Node::null();
333
    }
334
48446
    return args[0].eqNode(res);
335
  }
336
776342
  else if (id == PfRule::MACRO_SR_PRED_INTRO)
337
  {
338
59832
    Trace("builtin-pfcheck") << "Check " << id << " " << children.size() << " "
339
29916
                             << args[0] << std::endl;
340
29916
    Assert(1 <= args.size() && args.size() <= 3);
341
    MethodId ids, idr;
342
29916
    if (!getMethodIds(args, ids, idr, 1))
343
    {
344
      return Node::null();
345
    }
346
59832
    Node res = applySubstitutionRewrite(args[0], children, ids, idr);
347
29916
    if (res.isNull())
348
    {
349
      return Node::null();
350
    }
351
29916
    Trace("builtin-pfcheck") << "Result is " << res << std::endl;
352
59832
    Trace("builtin-pfcheck") << "Witness form is "
353
29916
                             << SkolemManager::getOriginalForm(res) << std::endl;
354
    // **** NOTE: can rewrite the witness form here. This enables certain lemmas
355
    // to be provable, e.g. (= k t) where k is a purification Skolem for t.
356
29916
    res = Rewriter::rewrite(SkolemManager::getOriginalForm(res));
357
29916
    if (!res.isConst() || !res.getConst<bool>())
358
    {
359
      Trace("builtin-pfcheck")
360
          << "Failed to rewrite to true, res=" << res << std::endl;
361
      return Node::null();
362
    }
363
29916
    Trace("builtin-pfcheck") << "...success" << std::endl;
364
29916
    return args[0];
365
  }
366
746426
  else if (id == PfRule::MACRO_SR_PRED_ELIM)
367
  {
368
16654
    Trace("builtin-pfcheck") << "Check " << id << " " << children.size() << " "
369
8327
                             << args.size() << std::endl;
370
8327
    Assert(children.size() >= 1);
371
8327
    Assert(args.size() <= 2);
372
16654
    std::vector<Node> exp;
373
8327
    exp.insert(exp.end(), children.begin() + 1, children.end());
374
    MethodId ids, idr;
375
8327
    if (!getMethodIds(args, ids, idr, 0))
376
    {
377
      return Node::null();
378
    }
379
16654
    Node res1 = applySubstitutionRewrite(children[0], exp, ids, idr);
380
8327
    Trace("builtin-pfcheck") << "Returned " << res1 << std::endl;
381
8327
    return res1;
382
  }
383
738099
  else if (id == PfRule::MACRO_SR_PRED_TRANSFORM)
384
  {
385
1051816
    Trace("builtin-pfcheck") << "Check " << id << " " << children.size() << " "
386
525908
                             << args.size() << std::endl;
387
525908
    Assert(children.size() >= 1);
388
525908
    Assert(1 <= args.size() && args.size() <= 3);
389
525908
    Assert(args[0].getType().isBoolean());
390
    MethodId ids, idr;
391
525908
    if (!getMethodIds(args, ids, idr, 1))
392
    {
393
      return Node::null();
394
    }
395
1051816
    std::vector<Node> exp;
396
525908
    exp.insert(exp.end(), children.begin() + 1, children.end());
397
1051816
    Node res1 = applySubstitutionRewrite(children[0], exp, ids, idr);
398
1051816
    Node res2 = applySubstitutionRewrite(args[0], exp, ids, idr);
399
    // if not already equal, do rewriting
400
525908
    if (res1 != res2)
401
    {
402
      // can rewrite the witness forms
403
578
      res1 = Rewriter::rewrite(SkolemManager::getOriginalForm(res1));
404
578
      res2 = Rewriter::rewrite(SkolemManager::getOriginalForm(res2));
405
578
      if (res1.isNull() || res1 != res2)
406
      {
407
108
        Trace("builtin-pfcheck") << "Failed to match results" << std::endl;
408
108
        Trace("builtin-pfcheck-debug") << res1 << " vs " << res2 << std::endl;
409
108
        return Node::null();
410
      }
411
    }
412
525800
    return args[0];
413
  }
414
212191
  else if (id == PfRule::REMOVE_TERM_FORMULA_AXIOM)
415
  {
416
4764
    Assert(children.empty());
417
4764
    Assert(args.size() == 1);
418
4764
    return RemoveTermFormulas::getAxiomFor(args[0]);
419
  }
420
207427
  else if (id == PfRule::PREPROCESS || id == PfRule::PREPROCESS_LEMMA
421
206834
           || id == PfRule::THEORY_PREPROCESS
422
205796
           || id == PfRule::THEORY_PREPROCESS_LEMMA
423
205547
           || id == PfRule::THEORY_EXPAND_DEF || id == PfRule::WITNESS_AXIOM
424
205524
           || id == PfRule::THEORY_LEMMA || id == PfRule::THEORY_REWRITE
425
40
           || id == PfRule::TRUST_REWRITE || id == PfRule::TRUST_SUBS
426
1
           || id == PfRule::TRUST_SUBS_MAP)
427
  {
428
    // "trusted" rules
429
207427
    Assert(!args.empty());
430
207427
    Assert(args[0].getType().isBoolean());
431
207427
    return args[0];
432
  }
433
434
  // no rule
435
  return Node::null();
436
}
437
438
612597
bool BuiltinProofRuleChecker::getMethodIds(const std::vector<Node>& args,
439
                                           MethodId& ids,
440
                                           MethodId& idr,
441
                                           size_t index)
442
{
443
612597
  ids = MethodId::SB_DEFAULT;
444
612597
  idr = MethodId::RW_REWRITE;
445
612597
  if (args.size() > index)
446
  {
447
11088
    if (!getMethodId(args[index], ids))
448
    {
449
      Trace("builtin-pfcheck")
450
          << "Failed to get id from " << args[index] << std::endl;
451
      return false;
452
    }
453
  }
454
612597
  if (args.size() > index + 1)
455
  {
456
55
    if (!getMethodId(args[index + 1], idr))
457
    {
458
      Trace("builtin-pfcheck")
459
          << "Failed to get id from " << args[index + 1] << std::endl;
460
      return false;
461
    }
462
  }
463
612597
  return true;
464
}
465
466
25779
void BuiltinProofRuleChecker::addMethodIds(std::vector<Node>& args,
467
                                           MethodId ids,
468
                                           MethodId idr)
469
{
470
25779
  bool ndefRewriter = (idr != MethodId::RW_REWRITE);
471
25779
  if (ids != MethodId::SB_DEFAULT || ndefRewriter)
472
  {
473
31
    args.push_back(mkMethodId(ids));
474
  }
475
25779
  if (ndefRewriter)
476
  {
477
31
    args.push_back(mkMethodId(idr));
478
  }
479
25779
}
480
481
bool BuiltinProofRuleChecker::getTheoryId(TNode n, TheoryId& tid)
482
{
483
  uint32_t i;
484
  if (!getUInt32(n, i))
485
  {
486
    return false;
487
  }
488
  tid = static_cast<TheoryId>(i);
489
  return true;
490
}
491
492
177588
Node BuiltinProofRuleChecker::mkTheoryIdNode(TheoryId tid)
493
{
494
  return NodeManager::currentNM()->mkConst(
495
177588
      Rational(static_cast<uint32_t>(tid)));
496
}
497
498
}  // namespace builtin
499
}  // namespace theory
500
26685
}  // namespace CVC4