GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/expr/lazy_proof.cpp Lines: 94 97 96.9 %
Date: 2021-03-22 Branches: 169 352 48.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file lazy_proof.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 lazy proof utility
13
 **/
14
15
#include "expr/lazy_proof.h"
16
17
#include "expr/proof_ensure_closed.h"
18
#include "expr/proof_node.h"
19
#include "expr/proof_node_manager.h"
20
21
using namespace CVC4::kind;
22
23
namespace CVC4 {
24
25
219412
LazyCDProof::LazyCDProof(ProofNodeManager* pnm,
26
                         ProofGenerator* dpg,
27
                         context::Context* c,
28
219412
                         std::string name)
29
219412
    : CDProof(pnm, c, name), d_gens(c ? c : &d_context), d_defaultGen(dpg)
30
{
31
219412
}
32
33
260585
LazyCDProof::~LazyCDProof() {}
34
35
1369689
std::shared_ptr<ProofNode> LazyCDProof::getProofFor(Node fact)
36
{
37
1369689
  Trace("lazy-cdproof") << "LazyCDProof::mkLazyProof " << fact << std::endl;
38
  // make the proof, which should always be non-null, since we construct an
39
  // assumption in the worst case.
40
1369689
  std::shared_ptr<ProofNode> opf = CDProof::getProofFor(fact);
41
1369689
  Assert(opf != nullptr);
42
1369689
  if (!hasGenerators())
43
  {
44
596758
    Trace("lazy-cdproof") << "...no generators, finished" << std::endl;
45
    // optimization: no generators, we are done
46
596758
    return opf;
47
  }
48
  // otherwise, we traverse the proof opf and fill in the ASSUME leafs that
49
  // have generators
50
1545862
  std::unordered_set<ProofNode*> visited;
51
772931
  std::unordered_set<ProofNode*>::iterator it;
52
1545862
  std::vector<ProofNode*> visit;
53
  ProofNode* cur;
54
772931
  visit.push_back(opf.get());
55
24666784
  do
56
  {
57
25439715
    cur = visit.back();
58
25439715
    visit.pop_back();
59
25439715
    it = visited.find(cur);
60
61
25439715
    if (it == visited.end())
62
    {
63
10447957
      visited.insert(cur);
64
20895914
      Node cfact = cur->getResult();
65
10447957
      if (getProof(cfact).get() != cur)
66
      {
67
        // We don't own this proof, skip it. This is to ensure that this method
68
        // is idempotent, since it may be the case that a previous call to
69
        // getProofFor connected a proof from a proof generator as a child of
70
        // a ProofNode in the range of the map in CDProof. Thus, this ensures
71
        // we don't touch such proofs.
72
241827
        Trace("lazy-cdproof") << "...skip unowned proof" << std::endl;
73
      }
74
10206130
      else if (cur->getRule() == PfRule::ASSUME)
75
      {
76
937311
        bool isSym = false;
77
937311
        ProofGenerator* pg = getGeneratorFor(cfact, isSym);
78
937311
        if (pg != nullptr)
79
        {
80
1579970
          Trace("lazy-cdproof")
81
1579970
              << "LazyCDProof: Call generator " << pg->identify()
82
789985
              << " for assumption " << cfact << std::endl;
83
1579970
          Node cfactGen = isSym ? CDProof::getSymmFact(cfact) : cfact;
84
789985
          Assert(!cfactGen.isNull());
85
          // Do not use the addProofTo interface, instead use the update node
86
          // interface, since this ensures that we don't take ownership for
87
          // the current proof. Instead, it is only linked, and ignored on
88
          // future calls to getProofFor due to the check above.
89
1579970
          std::shared_ptr<ProofNode> pgc = pg->getProofFor(cfactGen);
90
          // If the proof was null, then the update is not performed. This is
91
          // not considered an error, since this behavior is equivalent to
92
          // if pg had provided the proof (ASSUME cfactGen). Ensuring the
93
          // proper behavior wrt closed proofs should be done outside this
94
          // method.
95
789985
          if (pgc != nullptr)
96
          {
97
1579970
            Trace("lazy-cdproof-gen")
98
789985
                << "LazyCDProof: stored proof: " << *pgc.get() << std::endl;
99
100
789985
            if (isSym)
101
            {
102
8662
              d_manager->updateNode(cur, PfRule::SYMM, {pgc}, {});
103
            }
104
            else
105
            {
106
781323
              d_manager->updateNode(cur, pgc.get());
107
            }
108
1579970
            Trace("lazy-cdproof") << "LazyCDProof: Successfully added fact for "
109
789985
                                  << cfactGen << std::endl;
110
          }
111
        }
112
        else
113
        {
114
294652
          Trace("lazy-cdproof") << "LazyCDProof: " << identify()
115
147326
                                << " : No generator for " << cfact << std::endl;
116
        }
117
        // Notice that we do not traverse the proofs that have been generated
118
        // lazily by the proof generators here.  In other words, we assume that
119
        // the proofs from provided proof generators are final and need
120
        // no further modification by this class.
121
      }
122
      else
123
      {
124
9268819
        const std::vector<std::shared_ptr<ProofNode>>& cc = cur->getChildren();
125
33935603
        for (const std::shared_ptr<ProofNode>& cp : cc)
126
        {
127
24666784
          visit.push_back(cp.get());
128
        }
129
      }
130
    }
131
25439715
  } while (!visit.empty());
132
  // we have now updated the ASSUME leafs of opf, return it
133
772931
  Trace("lazy-cdproof") << "...finished" << std::endl;
134
772931
  Assert(opf->getResult() == fact);
135
772931
  return opf;
136
}
137
138
2100861
void LazyCDProof::addLazyStep(Node expected,
139
                              ProofGenerator* pg,
140
                              PfRule idNull,
141
                              bool isClosed,
142
                              const char* ctx,
143
                              bool forceOverwrite)
144
{
145
2100861
  if (pg == nullptr)
146
  {
147
    // null generator, should have given a proof rule
148
74
    if (idNull == PfRule::ASSUME)
149
    {
150
      Unreachable() << "LazyCDProof::addLazyStep: " << identify()
151
                    << ": failed to provide proof generator for " << expected;
152
      return;
153
    }
154
148
    Trace("lazy-cdproof") << "LazyCDProof::addLazyStep: " << expected
155
74
                          << " set (trusted) step " << idNull << "\n";
156
74
    addStep(expected, idNull, {}, {expected});
157
74
    return;
158
  }
159
4201574
  Trace("lazy-cdproof") << "LazyCDProof::addLazyStep: " << expected
160
2100787
                        << " set to generator " << pg->identify() << "\n";
161
2100787
  if (!forceOverwrite)
162
  {
163
2100787
    NodeProofGeneratorMap::const_iterator it = d_gens.find(expected);
164
2100787
    if (it != d_gens.end())
165
    {
166
      // don't overwrite something that is already there
167
1171905
      return;
168
    }
169
  }
170
  // just store now
171
928882
  d_gens.insert(expected, pg);
172
  // debug checking
173
928882
  if (isClosed)
174
  {
175
95902
    Trace("lazy-cdproof-debug") << "Checking closed..." << std::endl;
176
95902
    pfgEnsureClosed(expected, pg, "lazy-cdproof-debug", ctx);
177
  }
178
}
179
180
937311
ProofGenerator* LazyCDProof::getGeneratorFor(Node fact,
181
                                             bool& isSym)
182
{
183
937311
  isSym = false;
184
937311
  NodeProofGeneratorMap::const_iterator it = d_gens.find(fact);
185
937311
  if (it != d_gens.end())
186
  {
187
108843
    return (*it).second;
188
  }
189
1656936
  Node factSym = CDProof::getSymmFact(fact);
190
  // could be symmetry
191
828468
  if (factSym.isNull())
192
  {
193
    // can't be symmetry, return the default generator
194
220953
    return d_defaultGen;
195
  }
196
607515
  it = d_gens.find(factSym);
197
607515
  if (it != d_gens.end())
198
  {
199
8662
    isSym = true;
200
8662
    return (*it).second;
201
  }
202
  // return the default generator
203
598853
  return d_defaultGen;
204
}
205
206
1369689
bool LazyCDProof::hasGenerators() const
207
{
208
1369689
  return !d_gens.empty() || d_defaultGen != nullptr;
209
}
210
211
43099
bool LazyCDProof::hasGenerator(Node fact) const
212
{
213
43099
  if (d_defaultGen != nullptr)
214
  {
215
    return true;
216
  }
217
43099
  NodeProofGeneratorMap::const_iterator it = d_gens.find(fact);
218
43099
  if (it != d_gens.end())
219
  {
220
1634
    return true;
221
  }
222
  // maybe there is a symmetric fact?
223
82930
  Node factSym = CDProof::getSymmFact(fact);
224
41465
  if (!factSym.isNull())
225
  {
226
25955
    it = d_gens.find(factSym);
227
  }
228
41465
  return it != d_gens.end();
229
}
230
231
26676
}  // namespace CVC4