GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/expr/proof_ensure_closed.cpp Lines: 12 76 15.8 %
Date: 2021-03-22 Branches: 18 410 4.4 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file proof_ensure_closed.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 debug checks for ensuring proofs are closed
13
 **/
14
15
#include "expr/proof_ensure_closed.h"
16
17
#include <sstream>
18
19
#include "expr/proof_generator.h"
20
#include "expr/proof_node.h"
21
#include "expr/proof_node_algorithm.h"
22
#include "options/proof_options.h"
23
#include "options/smt_options.h"
24
25
namespace CVC4 {
26
27
/**
28
 * Ensure closed with respect to assumptions, internal version, which
29
 * generalizes the check for a proof generator or a proof node.
30
 */
31
655157
void ensureClosedWrtInternal(Node proven,
32
                             ProofGenerator* pg,
33
                             ProofNode* pnp,
34
                             const std::vector<Node>& assumps,
35
                             const char* c,
36
                             const char* ctx,
37
                             bool reqGen)
38
{
39
655157
  if (!options::produceProofs())
40
  {
41
    // proofs not enabled, do not do check
42
969615
    return;
43
  }
44
340699
  bool isTraceDebug = Trace.isOn(c);
45
340699
  if (!options::proofEagerChecking() && !isTraceDebug)
46
  {
47
    // trace is off and proof new eager checking is off, do not do check
48
340699
    return;
49
  }
50
  std::stringstream sdiag;
51
  bool isTraceOn = Trace.isOn(c);
52
  if (!isTraceOn)
53
  {
54
    sdiag << ", use -t " << c << " for details";
55
  }
56
  bool dumpProofTraceOn = Trace.isOn("dump-proof-error");
57
  if (!dumpProofTraceOn)
58
  {
59
    sdiag << ", use -t dump-proof-error for details on proof";
60
  }
61
  // get the proof node in question, which is either provided or built by the
62
  // proof generator
63
  std::shared_ptr<ProofNode> pn;
64
  std::stringstream ss;
65
  if (pnp != nullptr)
66
  {
67
    Assert(pg == nullptr);
68
    ss << "ProofNode in context " << ctx;
69
  }
70
  else
71
  {
72
    ss << "ProofGenerator: " << (pg == nullptr ? "null" : pg->identify())
73
       << " in context " << ctx;
74
    if (pg == nullptr)
75
    {
76
      // only failure if flag is true
77
      if (reqGen)
78
      {
79
        Unreachable() << "...ensureClosed: no generator in context " << ctx
80
                      << sdiag.str();
81
      }
82
    }
83
    else
84
    {
85
      Assert(!proven.isNull());
86
      pn = pg->getProofFor(proven);
87
      pnp = pn.get();
88
    }
89
  }
90
  Trace(c) << "=== ensureClosed: " << ss.str() << std::endl;
91
  Trace(c) << "Proven: " << proven << std::endl;
92
  if (pnp == nullptr)
93
  {
94
    if (pg == nullptr)
95
    {
96
      // did not require generator
97
      Assert(!reqGen);
98
      Trace(c) << "...ensureClosed: no generator in context " << ctx
99
               << std::endl;
100
      return;
101
    }
102
  }
103
  // if we don't have a proof node, a generator failed
104
  if (pnp == nullptr)
105
  {
106
    Assert(pg != nullptr);
107
    AlwaysAssert(false) << "...ensureClosed: null proof from " << ss.str()
108
                        << sdiag.str();
109
  }
110
  std::vector<Node> fassumps;
111
  expr::getFreeAssumptions(pnp, fassumps);
112
  bool isClosed = true;
113
  std::stringstream ssf;
114
  for (const Node& fa : fassumps)
115
  {
116
    if (std::find(assumps.begin(), assumps.end(), fa) == assumps.end())
117
    {
118
      isClosed = false;
119
      ssf << "- " << fa << std::endl;
120
    }
121
  }
122
  if (!isClosed)
123
  {
124
    Trace(c) << "Free assumptions:" << std::endl;
125
    Trace(c) << ssf.str();
126
    if (!assumps.empty())
127
    {
128
      Trace(c) << "Expected assumptions:" << std::endl;
129
      for (const Node& a : assumps)
130
      {
131
        Trace(c) << "- " << a << std::endl;
132
      }
133
    }
134
    if (dumpProofTraceOn)
135
    {
136
      Trace("dump-proof-error") << " Proof: " << *pnp << std::endl;
137
    }
138
  }
139
  AlwaysAssert(isClosed) << "...ensureClosed: open proof from " << ss.str()
140
                         << sdiag.str();
141
  Trace(c) << "...ensureClosed: success" << std::endl;
142
  Trace(c) << "====" << std::endl;
143
}
144
145
655157
void pfgEnsureClosed(Node proven,
146
                     ProofGenerator* pg,
147
                     const char* c,
148
                     const char* ctx,
149
                     bool reqGen)
150
{
151
655157
  Assert(!proven.isNull());
152
  // proof generator may be null
153
1310314
  std::vector<Node> assumps;
154
655157
  ensureClosedWrtInternal(proven, pg, nullptr, assumps, c, ctx, reqGen);
155
655157
}
156
157
void pfgEnsureClosedWrt(Node proven,
158
                        ProofGenerator* pg,
159
                        const std::vector<Node>& assumps,
160
                        const char* c,
161
                        const char* ctx,
162
                        bool reqGen)
163
{
164
  Assert(!proven.isNull());
165
  // proof generator may be null
166
  ensureClosedWrtInternal(proven, pg, nullptr, assumps, c, ctx, reqGen);
167
}
168
169
void pfnEnsureClosed(ProofNode* pn, const char* c, const char* ctx)
170
{
171
  ensureClosedWrtInternal(Node::null(), nullptr, pn, {}, c, ctx, false);
172
}
173
174
void pfnEnsureClosedWrt(ProofNode* pn,
175
                        const std::vector<Node>& assumps,
176
                        const char* c,
177
                        const char* ctx)
178
{
179
  ensureClosedWrtInternal(Node::null(), nullptr, pn, assumps, c, ctx, false);
180
}
181
182
26676
}  // namespace CVC4