GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/expr/lazy_proof_chain.cpp Lines: 113 151 74.8 %
Date: 2021-03-23 Branches: 167 518 32.2 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file lazy_proof_chain.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Haniel Barbosa, Andrew Reynolds, Gereon Kremer
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 lazy proof utility
13
 **/
14
15
#include "expr/lazy_proof_chain.h"
16
17
#include "expr/proof.h"
18
#include "expr/proof_ensure_closed.h"
19
#include "expr/proof_node.h"
20
#include "expr/proof_node_algorithm.h"
21
#include "expr/proof_node_manager.h"
22
#include "options/proof_options.h"
23
24
namespace CVC4 {
25
26
4624
LazyCDProofChain::LazyCDProofChain(ProofNodeManager* pnm,
27
                                   bool cyclic,
28
                                   context::Context* c,
29
                                   ProofGenerator* defGen,
30
4624
                                   bool defRec)
31
    : d_manager(pnm),
32
      d_cyclic(cyclic),
33
      d_defRec(defRec),
34
      d_context(),
35
      d_gens(c ? c : &d_context),
36
4624
      d_defGen(defGen)
37
{
38
4624
}
39
40
6548
LazyCDProofChain::~LazyCDProofChain() {}
41
42
const std::map<Node, std::shared_ptr<ProofNode>> LazyCDProofChain::getLinks()
43
    const
44
{
45
  std::map<Node, std::shared_ptr<ProofNode>> links;
46
  for (const std::pair<const Node, ProofGenerator* const>& link : d_gens)
47
  {
48
    Assert(link.second);
49
    std::shared_ptr<ProofNode> pfn = link.second->getProofFor(link.first);
50
    Assert(pfn);
51
    links[link.first] = pfn;
52
  }
53
  return links;
54
}
55
56
21980
std::shared_ptr<ProofNode> LazyCDProofChain::getProofFor(Node fact)
57
{
58
43960
  Trace("lazy-cdproofchain")
59
21980
      << "LazyCDProofChain::getProofFor " << fact << "\n";
60
  // which facts have had proofs retrieved for. This is maintained to avoid
61
  // cycles. It also saves the proof node of the fact
62
  std::unordered_map<Node, std::shared_ptr<ProofNode>, NodeHashFunction>
63
43960
      toConnect;
64
  // leaves of proof node links in the chain, i.e. assumptions, yet to be
65
  // expanded
66
  std::unordered_map<Node,
67
                     std::vector<std::shared_ptr<ProofNode>>,
68
                     NodeHashFunction>
69
43960
      assumptionsToExpand;
70
  // invariant of the loop below, the first iteration notwhistanding:
71
  //   visit = domain(assumptionsToExpand) \ domain(toConnect)
72
43960
  std::vector<Node> visit{fact};
73
43960
  std::unordered_map<Node, bool, NodeHashFunction> visited;
74
43960
  Node cur;
75
1121930
  do
76
  {
77
1143910
    cur = visit.back();
78
1143910
    visit.pop_back();
79
1143910
    auto itVisited = visited.find(cur);
80
    // pre-traversal
81
1143910
    if (itVisited == visited.end())
82
    {
83
514076
      Trace("lazy-cdproofchain")
84
257038
          << "LazyCDProofChain::getProofFor: check " << cur << "\n";
85
257038
      Assert(toConnect.find(cur) == toConnect.end());
86
257038
      bool rec = true;
87
257038
      ProofGenerator* pg = getGeneratorForInternal(cur, rec);
88
409177
      if (!pg)
89
      {
90
304278
        Trace("lazy-cdproofchain")
91
152139
            << "LazyCDProofChain::getProofFor: nothing to do\n";
92
        // nothing to do for this fact, it'll be a leaf in the final proof
93
        // node, don't post-traverse.
94
152139
        visited[cur] = true;
95
310966
        continue;
96
      }
97
209798
      Trace("lazy-cdproofchain")
98
209798
          << "LazyCDProofChain::getProofFor: Call generator " << pg->identify()
99
104899
          << " for chain link " << cur << "\n";
100
203110
      std::shared_ptr<ProofNode> curPfn = pg->getProofFor(cur);
101
106217
      if (curPfn == nullptr)
102
      {
103
2636
        Trace("lazy-cdproofchain")
104
1318
            << "LazyCDProofChain::getProofFor: No proof found, skip\n";
105
1318
        visited[cur] = true;
106
1318
        continue;
107
      }
108
      // map node whose proof node must be expanded to the respective poof node
109
103581
      toConnect[cur] = curPfn;
110
108951
      if (!rec)
111
      {
112
        // we don't want to recursively connect this proof
113
5370
        visited[cur] = true;
114
5370
        continue;
115
      }
116
196422
      Trace("lazy-cdproofchain-debug")
117
98211
          << "LazyCDProofChain::getProofFor: stored proof: " << *curPfn.get()
118
98211
          << "\n";
119
      // retrieve free assumptions and their respective proof nodes
120
196422
      std::map<Node, std::vector<std::shared_ptr<ProofNode>>> famap;
121
98211
      expr::getFreeAssumptionsMap(curPfn, famap);
122
98211
      if (Trace.isOn("lazy-cdproofchain"))
123
      {
124
        Trace("lazy-cdproofchain")
125
            << "LazyCDProofChain::getProofFor: free assumptions:\n";
126
        for (auto fap : famap)
127
        {
128
          Trace("lazy-cdproofchain")
129
              << "LazyCDProofChain::getProofFor:  - " << fap.first << "\n";
130
        }
131
      }
132
      // mark for post-traversal if we are controlling cycles
133
98211
      if (d_cyclic)
134
      {
135
196422
        Trace("lazy-cdproofchain") << "LazyCDProofChain::getProofFor: marking "
136
98211
                                   << cur << " for cycle check\n";
137
98211
        visit.push_back(cur);
138
98211
        visited[cur] = false;
139
      }
140
      else
141
      {
142
        visited[cur] = true;
143
      }
144
      // enqueue free assumptions to process
145
1037646
      for (const std::pair<const Node, std::vector<std::shared_ptr<ProofNode>>>&
146
98211
               fap : famap)
147
      {
148
        // check cycles
149
1037646
        if (d_cyclic)
150
        {
151
          // cycles are assumptions being *currently* expanded and seen again,
152
          // i.e. in toConnect and not yet post-visited
153
1037646
          auto itToConnect = toConnect.find(fap.first);
154
1051573
          if (itToConnect != toConnect.end() && !visited[fap.first])
155
          {
156
            // Since we have a cycle with an assumption, this fact will be an
157
            // assumption in the final proof node produced by this
158
            // method. Thus we erase it as something to be connected, which
159
            // will keep it as an assumption.
160
27854
            Trace("lazy-cdproofchain") << "LazyCDProofChain::getProofFor: "
161
13927
                                          "removing cyclic assumption "
162
13927
                                       << fap.first << " from expansion\n";
163
13927
            continue;
164
          }
165
        }
166
        // We always add assumptions to visit so that their last seen occurrence
167
        // is expanded (rather than the first seen occurrence, if we were not
168
        // adding assumptions, say, in assumptionsToExpand). This is so because
169
        // in the case where we are checking cycles this is necessary (and
170
        // harmless when we are not). For example the cycle
171
        //
172
        //                 a2
173
        //                ...
174
        //               ----
175
        //                a1
176
        //               ...
177
        //             --------
178
        //   a0   a1    a2
179
        //       ...
180
        //  ---------------
181
        //       n
182
        //
183
        // in which a2 has a1 as an assumption, which has a2 an assumption,
184
        // would not be captured if we did not revisit a1, which is an
185
        // assumption of n and this already occur in assumptionsToExpand when
186
        // it shows up again as an assumption of a2.
187
1023719
        visit.push_back(fap.first);
188
        // add assumption proof nodes to be updated
189
2047438
        assumptionsToExpand[fap.first].insert(
190
2047438
            assumptionsToExpand[fap.first].end(),
191
            fap.second.begin(),
192
3071157
            fap.second.end());
193
      }
194
98211
      if (d_cyclic)
195
      {
196
98211
        Trace("lazy-cdproofchain") << push;
197
98211
        Trace("lazy-cdproofchain-debug") << push;
198
      }
199
    }
200
886872
    else if (!itVisited->second)
201
    {
202
98211
      visited[cur] = true;
203
98211
      Trace("lazy-cdproofchain") << pop;
204
98211
      Trace("lazy-cdproofchain-debug") << pop;
205
196422
      Trace("lazy-cdproofchain")
206
98211
          << "LazyCDProofChain::getProofFor: post-visited " << cur << "\n";
207
    }
208
    else
209
    {
210
1577322
      Trace("lazy-cdproofchain")
211
788661
          << "LazyCDProofChain::getProofFor: already fully processed " << cur
212
788661
          << "\n";
213
    }
214
1143910
  } while (!visit.empty());
215
  // expand all assumptions marked to be connected
216
103581
  for (const std::pair<const Node, std::shared_ptr<ProofNode>>& npfn :
217
21980
       toConnect)
218
  {
219
103581
    auto it = assumptionsToExpand.find(npfn.first);
220
124957
    if (it == assumptionsToExpand.end())
221
    {
222
21376
      Assert(npfn.first == fact);
223
21376
      continue;
224
    }
225
82205
    Assert(npfn.second);
226
164410
    Trace("lazy-cdproofchain")
227
82205
        << "LazyCDProofChain::getProofFor: expand assumption " << npfn.first
228
82205
        << "\n";
229
164410
    Trace("lazy-cdproofchain-debug")
230
82205
        << "LazyCDProofChain::getProofFor: ...expand to " << *npfn.second.get()
231
82205
        << "\n";
232
    // update each assumption proof node
233
311441
    for (std::shared_ptr<ProofNode> pfn : it->second)
234
    {
235
229236
      d_manager->updateNode(pfn.get(), npfn.second.get());
236
    }
237
  }
238
  // final proof of fact
239
21980
  auto it = toConnect.find(fact);
240
21980
  if (it == toConnect.end())
241
  {
242
604
    return nullptr;
243
  }
244
21376
  return it->second;
245
}
246
247
717802
void LazyCDProofChain::addLazyStep(Node expected, ProofGenerator* pg)
248
{
249
717802
  Assert(pg != nullptr);
250
1435604
  Trace("lazy-cdproofchain") << "LazyCDProofChain::addLazyStep: " << expected
251
717802
                             << " set to generator " << pg->identify() << "\n";
252
  // note this will replace the generator for expected, if any
253
717802
  d_gens.insert(expected, pg);
254
717802
}
255
256
void LazyCDProofChain::addLazyStep(Node expected,
257
                                   ProofGenerator* pg,
258
                                   const std::vector<Node>& assumptions,
259
                                   const char* ctx)
260
{
261
  Assert(pg != nullptr);
262
  Trace("lazy-cdproofchain") << "LazyCDProofChain::addLazyStep: " << expected
263
                             << " set to generator " << pg->identify() << "\n";
264
  // note this will rewrite the generator for expected, if any
265
  d_gens.insert(expected, pg);
266
  // check if chain is closed if options::proofEagerChecking() is on
267
  if (options::proofEagerChecking())
268
  {
269
    Trace("lazy-cdproofchain")
270
        << "LazyCDProofChain::addLazyStep: Checking closed proof...\n";
271
    std::shared_ptr<ProofNode> pfn = pg->getProofFor(expected);
272
    std::vector<Node> allowedLeaves{assumptions.begin(), assumptions.end()};
273
    // add all current links in the chain
274
    for (const std::pair<const Node, ProofGenerator* const>& link : d_gens)
275
    {
276
      allowedLeaves.push_back(link.first);
277
    }
278
    if (Trace.isOn("lazy-cdproofchain"))
279
    {
280
      Trace("lazy-cdproofchain") << "Checking relative to leaves...\n";
281
      for (const Node& n : allowedLeaves)
282
      {
283
        Trace("lazy-cdproofchain") << "  - " << n << "\n";
284
      }
285
      Trace("lazy-cdproofchain") << "\n";
286
    }
287
    pfnEnsureClosedWrt(pfn.get(), allowedLeaves, "lazy-cdproofchain", ctx);
288
  }
289
}
290
291
bool LazyCDProofChain::hasGenerator(Node fact) const
292
{
293
  return d_gens.find(fact) != d_gens.end();
294
}
295
296
ProofGenerator* LazyCDProofChain::getGeneratorFor(Node fact)
297
{
298
  bool rec = true;
299
  return getGeneratorForInternal(fact, rec);
300
}
301
302
257038
ProofGenerator* LazyCDProofChain::getGeneratorForInternal(Node fact, bool& rec)
303
{
304
257038
  auto it = d_gens.find(fact);
305
257038
  if (it != d_gens.end())
306
  {
307
85977
    return (*it).second;
308
  }
309
  // otherwise, if no explicit generators, we use the default one
310
171061
  if (d_defGen != nullptr)
311
  {
312
18922
    rec = d_defRec;
313
18922
    return d_defGen;
314
  }
315
152139
  return nullptr;
316
}
317
318
32803
std::string LazyCDProofChain::identify() const { return "LazyCDProofChain"; }
319
320
26685
}  // namespace CVC4