GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/expr/proof_node_updater.cpp Lines: 96 130 73.8 %
Date: 2021-03-22 Branches: 124 354 35.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file proof_node_updater.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Haniel Barbosa
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 a utility for updating proof nodes
13
 **/
14
15
#include "expr/proof_node_updater.h"
16
17
#include "expr/lazy_proof.h"
18
#include "expr/proof_ensure_closed.h"
19
#include "expr/proof_node_algorithm.h"
20
#include "expr/proof_node_manager.h"
21
22
namespace CVC4 {
23
24
2890
ProofNodeUpdaterCallback::ProofNodeUpdaterCallback() {}
25
2890
ProofNodeUpdaterCallback::~ProofNodeUpdaterCallback() {}
26
27
bool ProofNodeUpdaterCallback::update(Node res,
28
                                      PfRule id,
29
                                      const std::vector<Node>& children,
30
                                      const std::vector<Node>& args,
31
                                      CDProof* cdp,
32
                                      bool& continueUpdate)
33
{
34
  return false;
35
}
36
37
4216
ProofNodeUpdater::ProofNodeUpdater(ProofNodeManager* pnm,
38
                                   ProofNodeUpdaterCallback& cb,
39
                                   bool mergeSubproofs,
40
4216
                                   bool autoSym)
41
    : d_pnm(pnm),
42
      d_cb(cb),
43
      d_debugFreeAssumps(false),
44
      d_mergeSubproofs(mergeSubproofs),
45
4216
      d_autoSym(autoSym)
46
{
47
4216
}
48
49
4584
void ProofNodeUpdater::process(std::shared_ptr<ProofNode> pf)
50
{
51
4584
  if (d_debugFreeAssumps)
52
  {
53
    if (Trace.isOn("pfnu-debug"))
54
    {
55
      Trace("pfnu-debug2") << "Initial proof: " << *pf.get() << std::endl;
56
      Trace("pfnu-debug") << "ProofNodeUpdater::process" << std::endl;
57
      Trace("pfnu-debug") << "Expected free assumptions: " << std::endl;
58
      for (const Node& fa : d_freeAssumps)
59
      {
60
        Trace("pfnu-debug") << "- " << fa << std::endl;
61
      }
62
      std::vector<Node> assump;
63
      expr::getFreeAssumptions(pf.get(), assump);
64
      Trace("pfnu-debug") << "Current free assumptions: " << std::endl;
65
      for (const Node& fa : assump)
66
      {
67
        Trace("pfnu-debug") << "- " << fa << std::endl;
68
      }
69
    }
70
  }
71
9168
  std::vector<std::shared_ptr<ProofNode>> traversing;
72
4584
  processInternal(pf, d_freeAssumps, traversing);
73
4584
}
74
75
47296
void ProofNodeUpdater::processInternal(
76
    std::shared_ptr<ProofNode> pf,
77
    const std::vector<Node>& fa,
78
    std::vector<std::shared_ptr<ProofNode>>& traversing)
79
{
80
47296
  Trace("pf-process") << "ProofNodeUpdater::process" << std::endl;
81
94592
  std::unordered_map<std::shared_ptr<ProofNode>, bool> visited;
82
47296
  std::unordered_map<std::shared_ptr<ProofNode>, bool>::iterator it;
83
94592
  std::vector<std::shared_ptr<ProofNode>> visit;
84
94592
  std::shared_ptr<ProofNode> cur;
85
47296
  visit.push_back(pf);
86
47296
  std::map<Node, std::shared_ptr<ProofNode>>::iterator itc;
87
  // A cache from formulas to proof nodes that are in the current scope.
88
  // Notice that we make a fresh recursive call to process if the current
89
  // rule is SCOPE below.
90
94592
  std::map<Node, std::shared_ptr<ProofNode>> resCache;
91
94592
  Node res;
92
10408007
  do
93
  {
94
10455303
    cur = visit.back();
95
10455303
    visit.pop_back();
96
10455303
    it = visited.find(cur);
97
10455303
    res = cur->getResult();
98
10455303
    if (it == visited.end())
99
    {
100
4472886
      if (d_mergeSubproofs)
101
      {
102
2133560
        itc = resCache.find(res);
103
2518362
        if (itc != resCache.end())
104
        {
105
          // already have a proof, merge it into this one
106
384802
          visited[cur] = true;
107
384802
          d_pnm->updateNode(cur.get(), itc->second.get());
108
1201552
          continue;
109
        }
110
      }
111
      // run update to a fixed point
112
4088084
      bool continueUpdate = true;
113
4241678
      while (runUpdate(cur, fa, continueUpdate) && continueUpdate)
114
      {
115
76797
        Trace("pf-process-debug") << "...updated proof." << std::endl;
116
      }
117
4088084
      visited[cur] = !continueUpdate;
118
4477320
      if (!continueUpdate)
119
      {
120
        // no further changes should be made to cur according to the callback
121
778472
        Trace("pf-process-debug")
122
389236
            << "...marked to not continue update." << std::endl;
123
389236
        runFinalize(cur, fa, resCache);
124
389236
        continue;
125
      }
126
3698848
      traversing.push_back(cur);
127
3698848
      visit.push_back(cur);
128
3698848
      if (d_mergeSubproofs)
129
      {
130
        // If we are not the top-level proof, we were a scope, or became a
131
        // scope after updating, we need to make a separate recursive call to
132
        // this method. This is not necessary if we are not merging subproofs.
133
1748758
        if (cur->getRule() == PfRule::SCOPE && cur != pf)
134
        {
135
85424
          std::vector<Node> nfa;
136
          // if we are debugging free assumptions, update the set
137
42712
          if (d_debugFreeAssumps)
138
          {
139
            nfa.insert(nfa.end(), fa.begin(), fa.end());
140
            const std::vector<Node>& args = cur->getArguments();
141
            nfa.insert(nfa.end(), args.begin(), args.end());
142
            Trace("pfnu-debug2")
143
                << "Process new scope with " << args << std::endl;
144
          }
145
          // Process in new call separately, since we should not cache
146
          // the results of proofs that have a different scope.
147
42712
          processInternal(cur, nfa, traversing);
148
42712
          continue;
149
        }
150
      }
151
3656136
      const std::vector<std::shared_ptr<ProofNode>>& ccp = cur->getChildren();
152
      // now, process children
153
10365295
      for (const std::shared_ptr<ProofNode>& cp : ccp)
154
      {
155
20127477
        if (std::find(traversing.begin(), traversing.end(), cp)
156
20127477
            != traversing.end())
157
        {
158
          Unhandled()
159
              << "ProofNodeUpdater::processInternal: cyclic proof! (use "
160
                 "--proof-eager-checking)"
161
              << std::endl;
162
        }
163
6709159
        visit.push_back(cp);
164
      }
165
    }
166
5982417
    else if (!it->second)
167
    {
168
3698848
      Assert(!traversing.empty());
169
3698848
      traversing.pop_back();
170
3698848
      visited[cur] = true;
171
      // finalize the node
172
3698848
      runFinalize(cur, fa, resCache);
173
    }
174
10455303
  } while (!visit.empty());
175
47296
  Trace("pf-process") << "ProofNodeUpdater::process: finished" << std::endl;
176
47296
}
177
178
4164881
bool ProofNodeUpdater::runUpdate(std::shared_ptr<ProofNode> cur,
179
                                 const std::vector<Node>& fa,
180
                                 bool& continueUpdate)
181
{
182
  // should it be updated?
183
4164881
  if (!d_cb.shouldUpdate(cur, continueUpdate))
184
  {
185
3440734
    return false;
186
  }
187
724147
  PfRule id = cur->getRule();
188
  // use CDProof to open a scope for which the callback updates
189
1448294
  CDProof cpf(d_pnm, nullptr, "ProofNodeUpdater::CDProof", d_autoSym);
190
724147
  const std::vector<std::shared_ptr<ProofNode>>& cc = cur->getChildren();
191
1448294
  std::vector<Node> ccn;
192
1176639
  for (const std::shared_ptr<ProofNode>& cp : cc)
193
  {
194
904984
    Node cpres = cp->getResult();
195
452492
    ccn.push_back(cpres);
196
    // store in the proof
197
452492
    cpf.addProof(cp);
198
  }
199
1448294
  Trace("pf-process-debug")
200
724147
      << "Updating (" << cur->getRule() << ")..." << std::endl;
201
1448294
  Node res = cur->getResult();
202
  // only if the callback updated the node
203
724147
  if (d_cb.update(res, id, ccn, cur->getArguments(), &cpf, continueUpdate))
204
  {
205
932066
    std::shared_ptr<ProofNode> npn = cpf.getProofFor(res);
206
932066
    std::vector<Node> fullFa;
207
466033
    if (d_debugFreeAssumps)
208
    {
209
      expr::getFreeAssumptions(cur.get(), fullFa);
210
      Trace("pfnu-debug") << "Original proof : " << *cur << std::endl;
211
    }
212
    // then, update the original proof node based on this one
213
466033
    Trace("pf-process-debug") << "Update node..." << std::endl;
214
466033
    d_pnm->updateNode(cur.get(), npn.get());
215
466033
    Trace("pf-process-debug") << "...update node finished." << std::endl;
216
466033
    if (d_debugFreeAssumps)
217
    {
218
      fullFa.insert(fullFa.end(), fa.begin(), fa.end());
219
      // We have that npn is a node we occurring the final updated version of
220
      // the proof. We can now debug based on the expected set of free
221
      // assumptions.
222
      Trace("pfnu-debug") << "Ensure update closed..." << std::endl;
223
      pfnEnsureClosedWrt(
224
          npn.get(), fullFa, "pfnu-debug", "ProofNodeUpdater:postupdate");
225
    }
226
466033
    Trace("pf-process-debug") << "..finished" << std::endl;
227
466033
    return true;
228
  }
229
258114
  Trace("pf-process-debug") << "..finished" << std::endl;
230
258114
  return false;
231
}
232
233
4088084
void ProofNodeUpdater::runFinalize(
234
    std::shared_ptr<ProofNode> cur,
235
    const std::vector<Node>& fa,
236
    std::map<Node, std::shared_ptr<ProofNode>>& resCache)
237
{
238
4088084
  if (d_mergeSubproofs)
239
  {
240
3497516
    Node res = cur->getResult();
241
    // cache result if we are merging subproofs
242
1748758
    resCache[res] = cur;
243
  }
244
4088084
  if (d_debugFreeAssumps)
245
  {
246
    // We have that npn is a node we occurring the final updated version of
247
    // the proof. We can now debug based on the expected set of free
248
    // assumptions.
249
    Trace("pfnu-debug") << "Ensure update closed..." << std::endl;
250
    pfnEnsureClosedWrt(
251
        cur.get(), fa, "pfnu-debug", "ProofNodeUpdater:finalize");
252
  }
253
4088084
}
254
255
void ProofNodeUpdater::setDebugFreeAssumptions(
256
    const std::vector<Node>& freeAssumps)
257
{
258
  d_freeAssumps.clear();
259
  d_freeAssumps.insert(
260
      d_freeAssumps.end(), freeAssumps.begin(), freeAssumps.end());
261
  d_debugFreeAssumps = true;
262
}
263
264
26676
}  // namespace CVC4