GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/expr/proof_checker.cpp Lines: 92 162 56.8 %
Date: 2021-03-23 Branches: 131 626 20.9 %

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 proof checker
13
 **/
14
15
#include "expr/proof_checker.h"
16
17
#include "expr/proof_node.h"
18
#include "expr/skolem_manager.h"
19
#include "options/proof_options.h"
20
#include "smt/smt_statistics_registry.h"
21
22
using namespace CVC4::kind;
23
24
namespace CVC4 {
25
26
4886178
Node ProofRuleChecker::check(PfRule id,
27
                             const std::vector<Node>& children,
28
                             const std::vector<Node>& args)
29
{
30
  // call instance-specific checkInternal method
31
4886178
  return checkInternal(id, children, args);
32
}
33
34
885643
bool ProofRuleChecker::getUInt32(TNode n, uint32_t& i)
35
{
36
  // must be a non-negative integer constant that fits an unsigned int
37
2656929
  if (n.isConst() && n.getType().isInteger()
38
885643
      && n.getConst<Rational>().sgn() >= 0
39
2656929
      && n.getConst<Rational>().getNumerator().fitsUnsignedInt())
40
  {
41
885643
    i = n.getConst<Rational>().getNumerator().toUnsignedInt();
42
885643
    return true;
43
  }
44
  return false;
45
}
46
47
1041
bool ProofRuleChecker::getBool(TNode n, bool& b)
48
{
49
1041
  if (n.isConst() && n.getType().isBoolean())
50
  {
51
1041
    b = n.getConst<bool>();
52
1041
    return true;
53
  }
54
  return false;
55
}
56
57
461854
bool ProofRuleChecker::getKind(TNode n, Kind& k)
58
{
59
  uint32_t i;
60
461854
  if (!getUInt32(n, i))
61
  {
62
    return false;
63
  }
64
461854
  k = static_cast<Kind>(i);
65
461854
  return true;
66
}
67
68
475200
Node ProofRuleChecker::mkKindNode(Kind k)
69
{
70
475200
  if (k == UNDEFINED_KIND)
71
  {
72
    // UNDEFINED_KIND is negative, hence return null to avoid cast
73
    return Node::null();
74
  }
75
475200
  return NodeManager::currentNM()->mkConst(Rational(static_cast<uint32_t>(k)));
76
}
77
78
962
ProofCheckerStatistics::ProofCheckerStatistics()
79
    : d_ruleChecks("ProofCheckerStatistics::ruleChecks"),
80
962
    d_totalRuleChecks("ProofCheckerStatistics::totalRuleChecks", 0)
81
{
82
962
  smtStatisticsRegistry()->registerStat(&d_ruleChecks);
83
962
  smtStatisticsRegistry()->registerStat(&d_totalRuleChecks);
84
962
}
85
86
1924
ProofCheckerStatistics::~ProofCheckerStatistics()
87
{
88
962
  smtStatisticsRegistry()->unregisterStat(&d_ruleChecks);
89
962
  smtStatisticsRegistry()->unregisterStat(&d_totalRuleChecks);
90
962
}
91
92
1170584
Node ProofChecker::check(ProofNode* pn, Node expected)
93
{
94
1170584
  return check(pn->getRule(), pn->getChildren(), pn->getArguments(), expected);
95
}
96
97
15481039
Node ProofChecker::check(
98
    PfRule id,
99
    const std::vector<std::shared_ptr<ProofNode>>& children,
100
    const std::vector<Node>& args,
101
    Node expected)
102
{
103
  // optimization: immediately return for ASSUME
104
15481039
  if (id == PfRule::ASSUME)
105
  {
106
10704634
    Assert(children.empty());
107
10704634
    Assert(args.size() == 1 && args[0].getType().isBoolean());
108
10704634
    Assert(expected.isNull() || expected == args[0]);
109
10704634
    return expected;
110
  }
111
  // record stat
112
4776405
  d_stats.d_ruleChecks << id;
113
4776405
  ++d_stats.d_totalRuleChecks;
114
4776405
  Trace("pfcheck") << "ProofChecker::check: " << id << std::endl;
115
9552810
  std::vector<Node> cchildren;
116
21096100
  for (const std::shared_ptr<ProofNode>& pc : children)
117
  {
118
16319695
    Assert(pc != nullptr);
119
32639390
    Node cres = pc->getResult();
120
16319695
    if (cres.isNull())
121
    {
122
      Trace("pfcheck") << "ProofChecker::check: failed child" << std::endl;
123
      Unreachable()
124
          << "ProofChecker::check: child proof was invalid (null conclusion)"
125
          << std::endl;
126
      // should not have been able to create such a proof node
127
      return Node::null();
128
    }
129
16319695
    cchildren.push_back(cres);
130
16319695
    if (Trace.isOn("pfcheck"))
131
    {
132
      std::stringstream ssc;
133
      pc->printDebug(ssc);
134
      Trace("pfcheck") << "     child: " << ssc.str() << " : " << cres
135
                       << std::endl;
136
    }
137
  }
138
4776405
  Trace("pfcheck") << "      args: " << args << std::endl;
139
4776405
  Trace("pfcheck") << "  expected: " << expected << std::endl;
140
9552810
  std::stringstream out;
141
  // we use trusted (null) checkers here, since we want the proof generation to
142
  // proceed without failing here. We always enable output since a failure
143
  // implies that we will exit with the error message below.
144
9552810
  Node res = checkInternal(id, cchildren, args, expected, out, true, true);
145
4776405
  if (res.isNull())
146
  {
147
    Trace("pfcheck") << "ProofChecker::check: failed" << std::endl;
148
    Unreachable() << "ProofChecker::check: failed, " << out.str() << std::endl;
149
    // it did not match the given expectation, fail
150
    return Node::null();
151
  }
152
4776405
  Trace("pfcheck") << "ProofChecker::check: success!" << std::endl;
153
4776405
  return res;
154
}
155
156
109773
Node ProofChecker::checkDebug(PfRule id,
157
                              const std::vector<Node>& cchildren,
158
                              const std::vector<Node>& args,
159
                              Node expected,
160
                              const char* traceTag)
161
{
162
219546
  std::stringstream out;
163
109773
  bool traceEnabled = Trace.isOn(traceTag);
164
  // Since we are debugging, we want to treat trusted (null) checkers as
165
  // a failure. We only enable output if the trace is enabled for efficiency.
166
  Node res =
167
109773
      checkInternal(id, cchildren, args, expected, out, false, traceEnabled);
168
109773
  if (traceEnabled)
169
  {
170
    Trace(traceTag) << "ProofChecker::checkDebug: " << id;
171
    if (res.isNull())
172
    {
173
      Trace(traceTag) << " failed, " << out.str() << std::endl;
174
    }
175
    else
176
    {
177
      Trace(traceTag) << " success" << std::endl;
178
    }
179
    Trace(traceTag) << "cchildren: " << cchildren << std::endl;
180
    Trace(traceTag) << "     args: " << args << std::endl;
181
  }
182
219546
  return res;
183
}
184
185
4886178
Node ProofChecker::checkInternal(PfRule id,
186
                                 const std::vector<Node>& cchildren,
187
                                 const std::vector<Node>& args,
188
                                 Node expected,
189
                                 std::stringstream& out,
190
                                 bool useTrustedChecker,
191
                                 bool enableOutput)
192
{
193
4886178
  std::map<PfRule, ProofRuleChecker*>::iterator it = d_checker.find(id);
194
4886178
  if (it == d_checker.end())
195
  {
196
    // no checker for the rule
197
    if (enableOutput)
198
    {
199
      out << "no checker for rule " << id << std::endl;
200
    }
201
    return Node::null();
202
  }
203
4886178
  else if (it->second == nullptr)
204
  {
205
    if (useTrustedChecker)
206
    {
207
      Notice() << "ProofChecker::check: trusting PfRule " << id << std::endl;
208
      // trusted checker
209
      return expected;
210
    }
211
    else
212
    {
213
      if (enableOutput)
214
      {
215
        out << "trusted checker for rule " << id << std::endl;
216
      }
217
      return Node::null();
218
    }
219
  }
220
  // check it with the corresponding checker
221
9772356
  Node res = it->second->check(id, cchildren, args);
222
4886178
  if (!expected.isNull())
223
  {
224
7950488
    Node expectedw = expected;
225
3975244
    if (res != expectedw)
226
    {
227
      if (enableOutput)
228
      {
229
        out << "result does not match expected value." << std::endl
230
            << "    PfRule: " << id << std::endl;
231
        for (const Node& c : cchildren)
232
        {
233
          out << "     child: " << c << std::endl;
234
        }
235
        for (const Node& a : args)
236
        {
237
          out << "       arg: " << a << std::endl;
238
        }
239
        out << "    result: " << res << std::endl
240
            << "  expected: " << expected << std::endl;
241
      }
242
      // it did not match the given expectation, fail
243
      return Node::null();
244
    }
245
  }
246
  // fails if pedantic level is not met
247
4886178
  if (options::proofEagerChecking())
248
  {
249
    std::stringstream serr;
250
    if (isPedanticFailure(id, serr, enableOutput))
251
    {
252
      if (enableOutput)
253
      {
254
        out << serr.str() << std::endl;
255
        if (Trace.isOn("proof-pedantic"))
256
        {
257
          Trace("proof-pedantic")
258
              << "Failed pedantic check for " << id << std::endl;
259
          Trace("proof-pedantic") << "Expected: " << expected << std::endl;
260
          out << "Expected: " << expected << std::endl;
261
        }
262
      }
263
      return Node::null();
264
    }
265
  }
266
4886178
  return res;
267
}
268
269
127871
void ProofChecker::registerChecker(PfRule id, ProofRuleChecker* psc)
270
{
271
127871
  std::map<PfRule, ProofRuleChecker*>::iterator it = d_checker.find(id);
272
127871
  if (it != d_checker.end())
273
  {
274
    // checker is already provided
275
    Notice() << "ProofChecker::registerChecker: checker already exists for "
276
             << id << std::endl;
277
    return;
278
  }
279
127871
  d_checker[id] = psc;
280
}
281
282
13468
void ProofChecker::registerTrustedChecker(PfRule id,
283
                                          ProofRuleChecker* psc,
284
                                          uint32_t plevel)
285
{
286
13468
  AlwaysAssert(plevel <= 10) << "ProofChecker::registerTrustedChecker: "
287
                                "pedantic level must be 0-10, got "
288
                             << plevel << " for " << id;
289
13468
  registerChecker(id, psc);
290
  // overwrites if already there
291
13468
  if (d_plevel.find(id) != d_plevel.end())
292
  {
293
    Notice() << "ProofChecker::registerTrustedRule: already provided pedantic "
294
                "level for "
295
             << id << std::endl;
296
  }
297
13468
  d_plevel[id] = plevel;
298
13468
}
299
300
131927
ProofRuleChecker* ProofChecker::getCheckerFor(PfRule id)
301
{
302
131927
  std::map<PfRule, ProofRuleChecker*>::const_iterator it = d_checker.find(id);
303
131927
  if (it == d_checker.end())
304
  {
305
    return nullptr;
306
  }
307
131927
  return it->second;
308
}
309
310
1815616
uint32_t ProofChecker::getPedanticLevel(PfRule id) const
311
{
312
1815616
  std::map<PfRule, uint32_t>::const_iterator itp = d_plevel.find(id);
313
1815616
  if (itp != d_plevel.end())
314
  {
315
6612
    return itp->second;
316
  }
317
1809004
  return 0;
318
}
319
320
1815616
bool ProofChecker::isPedanticFailure(PfRule id,
321
                                     std::ostream& out,
322
                                     bool enableOutput) const
323
{
324
1815616
  if (d_pclevel == 0)
325
  {
326
1815616
    return false;
327
  }
328
  std::map<PfRule, uint32_t>::const_iterator itp = d_plevel.find(id);
329
  if (itp != d_plevel.end())
330
  {
331
    if (itp->second <= d_pclevel)
332
    {
333
      if (enableOutput)
334
      {
335
        out << "pedantic level for " << id << " not met (rule level is "
336
            << itp->second << " which is at or below the pedantic level "
337
            << d_pclevel << ")";
338
        bool pedanticTraceEnabled = Trace.isOn("proof-pedantic");
339
        if (!pedanticTraceEnabled)
340
        {
341
          out << ", use -t proof-pedantic for details";
342
        }
343
      }
344
      return true;
345
    }
346
  }
347
  return false;
348
}
349
350
26685
}  // namespace CVC4