GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/expr/proof.cpp Lines: 170 212 80.2 %
Date: 2021-03-23 Branches: 392 922 42.5 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file 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 proof
13
 **/
14
15
#include "expr/proof.h"
16
17
#include "expr/proof_checker.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
1062966
CDProof::CDProof(ProofNodeManager* pnm,
26
                 context::Context* c,
27
                 std::string name,
28
1062966
                 bool autoSymm)
29
    : d_manager(pnm),
30
      d_context(),
31
      d_nodes(c ? c : &d_context),
32
      d_name(name),
33
1062966
      d_autoSymm(autoSymm)
34
{
35
1062966
}
36
37
1063928
CDProof::~CDProof() {}
38
39
1972480
std::shared_ptr<ProofNode> CDProof::getProofFor(Node fact)
40
{
41
3944960
  std::shared_ptr<ProofNode> pf = getProofSymm(fact);
42
1972480
  if (pf != nullptr)
43
  {
44
1219434
    return pf;
45
  }
46
  // add as assumption
47
1506092
  std::vector<Node> pargs = {fact};
48
1506092
  std::vector<std::shared_ptr<ProofNode>> passume;
49
  std::shared_ptr<ProofNode> pfa =
50
1506092
      d_manager->mkNode(PfRule::ASSUME, passume, pargs, fact);
51
753046
  d_nodes.insert(fact, pfa);
52
753046
  return pfa;
53
}
54
55
29731306
std::shared_ptr<ProofNode> CDProof::getProof(Node fact) const
56
{
57
29731306
  NodeProofNodeMap::iterator it = d_nodes.find(fact);
58
29731306
  if (it != d_nodes.end())
59
  {
60
17404842
    return (*it).second;
61
  }
62
12326464
  return nullptr;
63
}
64
65
12240289
std::shared_ptr<ProofNode> CDProof::getProofSymm(Node fact)
66
{
67
12240289
  Trace("cdproof") << "CDProof::getProofSymm: " << fact << std::endl;
68
24480578
  std::shared_ptr<ProofNode> pf = getProof(fact);
69
12240289
  if (pf != nullptr && !isAssumption(pf.get()))
70
  {
71
4249461
    Trace("cdproof") << "...existing non-assume " << pf->getRule() << std::endl;
72
4249461
    return pf;
73
  }
74
7990828
  else if (!d_autoSymm)
75
  {
76
    Trace("cdproof") << "...not auto considering symmetry" << std::endl;
77
    return pf;
78
  }
79
15981656
  Node symFact = getSymmFact(fact);
80
7990828
  if (symFact.isNull())
81
  {
82
3433011
    Trace("cdproof") << "...no possible symm" << std::endl;
83
    // no symmetry possible, return original proof (possibly assumption)
84
3433011
    return pf;
85
  }
86
  // See if a proof exists for the opposite direction, if so, add the step.
87
  // Notice that SYMM is also disallowed.
88
9115634
  std::shared_ptr<ProofNode> pfs = getProof(symFact);
89
4557817
  if (pfs != nullptr)
90
  {
91
    // The symmetric fact exists, and the current one either does not, or is
92
    // an assumption. We make a new proof that applies SYMM to pfs.
93
773444
    std::vector<std::shared_ptr<ProofNode>> pschild;
94
596938
    pschild.push_back(pfs);
95
773444
    std::vector<Node> args;
96
596938
    if (pf == nullptr)
97
    {
98
420432
      Trace("cdproof") << "...fresh make symm" << std::endl;
99
      std::shared_ptr<ProofNode> psym =
100
840864
          d_manager->mkNode(PfRule::SYMM, pschild, args, fact);
101
420432
      Assert(psym != nullptr);
102
420432
      d_nodes.insert(fact, psym);
103
420432
      return psym;
104
    }
105
176506
    else if (!isAssumption(pfs.get()))
106
    {
107
      // if its not an assumption, make the connection
108
12
      Trace("cdproof") << "...update symm" << std::endl;
109
      // update pf
110
12
      bool sret = d_manager->updateNode(pf.get(), PfRule::SYMM, pschild, args);
111
12
      AlwaysAssert(sret);
112
    }
113
  }
114
  else
115
  {
116
7921758
    Trace("cdproof") << "...no symm, return "
117
3960879
                     << (pf == nullptr ? "null" : "non-null") << std::endl;
118
  }
119
  // return original proof (possibly assumption)
120
4137385
  return pf;
121
}
122
123
3411048
bool CDProof::addStep(Node expected,
124
                      PfRule id,
125
                      const std::vector<Node>& children,
126
                      const std::vector<Node>& args,
127
                      bool ensureChildren,
128
                      CDPOverwrite opolicy)
129
{
130
6822096
  Trace("cdproof") << "CDProof::addStep: " << identify() << " : " << id << " "
131
3411048
                   << expected << ", ensureChildren = " << ensureChildren
132
3411048
                   << ", overwrite policy = " << opolicy << std::endl;
133
6822096
  Trace("cdproof-debug") << "CDProof::addStep: " << identify()
134
3411048
                         << " : children: " << children << "\n";
135
6822096
  Trace("cdproof-debug") << "CDProof::addStep: " << identify()
136
3411048
                         << " : args: " << args << "\n";
137
  // We must always provide expected to this method
138
3411048
  Assert(!expected.isNull());
139
140
6822096
  std::shared_ptr<ProofNode> pprev = getProofSymm(expected);
141
3411048
  if (pprev != nullptr)
142
  {
143
1040305
    if (!shouldOverwrite(pprev.get(), id, opolicy))
144
    {
145
      // we should not overwrite the current step
146
998473
      Trace("cdproof") << "...success, no overwrite" << std::endl;
147
998473
      return true;
148
    }
149
83664
    Trace("cdproof") << "existing proof " << pprev->getRule()
150
41832
                     << ", overwrite..." << std::endl;
151
    // we will overwrite the existing proof node by updating its contents below
152
  }
153
  // collect the child proofs, for each premise
154
4825150
  std::vector<std::shared_ptr<ProofNode>> pchildren;
155
7670206
  for (const Node& c : children)
156
  {
157
5257631
    Trace("cdproof") << "- get child " << c << std::endl;
158
10515262
    std::shared_ptr<ProofNode> pc = getProofSymm(c);
159
5257631
    if (pc == nullptr)
160
    {
161
1482019
      if (ensureChildren)
162
      {
163
        // failed to get a proof for a child, fail
164
        Trace("cdproof") << "...fail, no child" << std::endl;
165
        return false;
166
      }
167
1482019
      Trace("cdproof") << "--- add assume" << std::endl;
168
      // otherwise, we initialize it as an assumption
169
2964038
      std::vector<Node> pcargs = {c};
170
2964038
      std::vector<std::shared_ptr<ProofNode>> pcassume;
171
1482019
      pc = d_manager->mkNode(PfRule::ASSUME, pcassume, pcargs, c);
172
      // assumptions never fail to check
173
1482019
      Assert(pc != nullptr);
174
1482019
      d_nodes.insert(c, pc);
175
    }
176
5257631
    pchildren.push_back(pc);
177
  }
178
179
  // the user may have provided SYMM of an assumption
180
2412575
  if (id == PfRule::SYMM)
181
  {
182
36
    Assert(pchildren.size() == 1);
183
36
    if (isAssumption(pchildren[0].get()))
184
    {
185
      // the step we are constructing is a (symmetric fact of an) assumption, so
186
      // there is no use adding it to the proof.
187
36
      return true;
188
    }
189
  }
190
191
2412539
  bool ret = true;
192
  // create or update it
193
4825078
  std::shared_ptr<ProofNode> pthis;
194
2412539
  if (pprev == nullptr)
195
  {
196
2370707
    Trace("cdproof") << "  new node " << expected << "..." << std::endl;
197
2370707
    pthis = d_manager->mkNode(id, pchildren, args, expected);
198
2370707
    if (pthis == nullptr)
199
    {
200
      // failed to construct the node, perhaps due to a proof checking failure
201
      Trace("cdproof") << "...fail, proof checking" << std::endl;
202
      return false;
203
    }
204
2370707
    d_nodes.insert(expected, pthis);
205
  }
206
  else
207
  {
208
41832
    Trace("cdproof") << "  update node " << expected << "..." << std::endl;
209
    // update its value
210
41832
    pthis = pprev;
211
    // We return the value of updateNode here. This means this method may return
212
    // false if this call failed, regardless of whether we already have a proof
213
    // step for expected.
214
41832
    ret = d_manager->updateNode(pthis.get(), id, pchildren, args);
215
  }
216
2412539
  if (ret)
217
  {
218
    // the result of the proof node should be expected
219
2412539
    Assert(pthis->getResult() == expected);
220
221
    // notify new proof
222
2412539
    notifyNewProof(expected);
223
  }
224
225
2412539
  Trace("cdproof") << "...return " << ret << std::endl;
226
2412539
  return ret;
227
}
228
229
4010390
void CDProof::notifyNewProof(Node expected)
230
{
231
4010390
  if (!d_autoSymm)
232
  {
233
    return;
234
  }
235
  // ensure SYMM proof is also linked to an existing proof, if it is an
236
  // assumption.
237
8020780
  Node symExpected = getSymmFact(expected);
238
4010390
  if (!symExpected.isNull())
239
  {
240
1857469
    Trace("cdproof") << "  check connect symmetry " << symExpected << std::endl;
241
    // if it exists, we may need to update it
242
3714938
    std::shared_ptr<ProofNode> pfs = getProof(symExpected);
243
1857469
    if (pfs != nullptr)
244
    {
245
1279
      Trace("cdproof") << "  connect via getProofSymm method..." << std::endl;
246
      // call the get function with symmetry, which will do the update
247
1279
      std::shared_ptr<ProofNode> pfss = getProofSymm(symExpected);
248
    }
249
    else
250
    {
251
1856190
      Trace("cdproof") << "  no connect" << std::endl;
252
    }
253
  }
254
}
255
256
1171324
bool CDProof::addStep(Node expected,
257
                      const ProofStep& step,
258
                      bool ensureChildren,
259
                      CDPOverwrite opolicy)
260
{
261
3513972
  return addStep(expected,
262
1171324
                 step.d_rule,
263
                 step.d_children,
264
                 step.d_args,
265
                 ensureChildren,
266
2342648
                 opolicy);
267
}
268
269
26173
bool CDProof::addSteps(const ProofStepBuffer& psb,
270
                       bool ensureChildren,
271
                       CDPOverwrite opolicy)
272
{
273
26173
  const std::vector<std::pair<Node, ProofStep>>& steps = psb.getSteps();
274
52999
  for (const std::pair<Node, ProofStep>& ps : steps)
275
  {
276
26826
    if (!addStep(ps.first, ps.second, ensureChildren, opolicy))
277
    {
278
      return false;
279
    }
280
  }
281
26173
  return true;
282
}
283
284
1597851
bool CDProof::addProof(std::shared_ptr<ProofNode> pn,
285
                       CDPOverwrite opolicy,
286
                       bool doCopy)
287
{
288
1597851
  if (!doCopy)
289
  {
290
    // If we aren't doing a deep copy, we either store pn or link its top
291
    // node into the existing pointer
292
3195702
    Node curFact = pn->getResult();
293
3195702
    std::shared_ptr<ProofNode> cur = getProofSymm(curFact);
294
1597851
    if (cur == nullptr)
295
    {
296
      // Assert that the checker of this class agrees with (the externally
297
      // provided) pn. This ensures that if pn was checked by a different
298
      // checker than the one of the manager in this class, then it is double
299
      // checked here, so that this class maintains the invariant that all of
300
      // its nodes in d_nodes have been checked by the underlying checker.
301
1170584
      Assert(d_manager->getChecker() == nullptr
302
             || d_manager->getChecker()->check(pn.get(), curFact) == curFact);
303
      // just store the proof for fact
304
1170584
      d_nodes.insert(curFact, pn);
305
    }
306
427267
    else if (shouldOverwrite(cur.get(), pn->getRule(), opolicy))
307
    {
308
      // We update cur to have the structure of the top node of pn. Notice that
309
      // the interface to update this node will ensure that the proof apf is a
310
      // proof of the assumption. If it does not, then pn was wrong.
311
      if (!d_manager->updateNode(
312
              cur.get(), pn->getRule(), pn->getChildren(), pn->getArguments()))
313
      {
314
        return false;
315
      }
316
    }
317
    // also need to connect via SYMM if necessary
318
1597851
    notifyNewProof(curFact);
319
1597851
    return true;
320
  }
321
  std::unordered_map<ProofNode*, bool> visited;
322
  std::unordered_map<ProofNode*, bool>::iterator it;
323
  std::vector<ProofNode*> visit;
324
  ProofNode* cur;
325
  Node curFact;
326
  visit.push_back(pn.get());
327
  bool retValue = true;
328
  do
329
  {
330
    cur = visit.back();
331
    curFact = cur->getResult();
332
    visit.pop_back();
333
    it = visited.find(cur);
334
    if (it == visited.end())
335
    {
336
      // visit the children
337
      visited[cur] = false;
338
      visit.push_back(cur);
339
      const std::vector<std::shared_ptr<ProofNode>>& cs = cur->getChildren();
340
      for (const std::shared_ptr<ProofNode>& c : cs)
341
      {
342
        visit.push_back(c.get());
343
      }
344
    }
345
    else if (!it->second)
346
    {
347
      // we always call addStep, which may or may not overwrite the
348
      // current step
349
      std::vector<Node> pexp;
350
      const std::vector<std::shared_ptr<ProofNode>>& cs = cur->getChildren();
351
      for (const std::shared_ptr<ProofNode>& c : cs)
352
      {
353
        Assert(!c->getResult().isNull());
354
        pexp.push_back(c->getResult());
355
      }
356
      // can ensure children at this point
357
      bool res = addStep(
358
          curFact, cur->getRule(), pexp, cur->getArguments(), true, opolicy);
359
      // should always succeed
360
      Assert(res);
361
      retValue = retValue && res;
362
      visited[cur] = true;
363
    }
364
  } while (!visit.empty());
365
366
  return retValue;
367
}
368
369
597963
bool CDProof::hasStep(Node fact)
370
{
371
1195926
  std::shared_ptr<ProofNode> pf = getProof(fact);
372
597963
  if (pf != nullptr && !isAssumption(pf.get()))
373
  {
374
550196
    return true;
375
  }
376
47767
  else if (!d_autoSymm)
377
  {
378
    return false;
379
  }
380
95534
  Node symFact = getSymmFact(fact);
381
47767
  if (symFact.isNull())
382
  {
383
17981
    return false;
384
  }
385
29786
  pf = getProof(symFact);
386
29786
  if (pf != nullptr && !isAssumption(pf.get()))
387
  {
388
    return true;
389
  }
390
29786
  return false;
391
}
392
393
79395
ProofNodeManager* CDProof::getManager() const { return d_manager; }
394
395
1467572
bool CDProof::shouldOverwrite(ProofNode* pn, PfRule newId, CDPOverwrite opol)
396
{
397
1467572
  Assert(pn != nullptr);
398
  // we overwrite only if opol is CDPOverwrite::ALWAYS, or if
399
  // opol is CDPOverwrite::ASSUME_ONLY and the previously
400
  // provided proof pn was an assumption and the currently provided step is not
401
  return opol == CDPOverwrite::ALWAYS
402
1509404
         || (opol == CDPOverwrite::ASSUME_ONLY && isAssumption(pn)
403
1781222
             && newId != PfRule::ASSUME);
404
}
405
406
8238062
bool CDProof::isAssumption(ProofNode* pn)
407
{
408
8238062
  PfRule rule = pn->getRule();
409
8238062
  if (rule == PfRule::ASSUME)
410
  {
411
2047282
    return true;
412
  }
413
6190780
  else if (rule == PfRule::SYMM)
414
  {
415
353555
    const std::vector<std::shared_ptr<ProofNode>>& pc = pn->getChildren();
416
353555
    Assert(pc.size() == 1);
417
353555
    return pc[0]->getRule() == PfRule::ASSUME;
418
  }
419
5837225
  return false;
420
}
421
422
921608
bool CDProof::isSame(TNode f, TNode g)
423
{
424
921608
  if (f == g)
425
  {
426
532160
    return true;
427
  }
428
389448
  Kind fk = f.getKind();
429
389448
  Kind gk = g.getKind();
430
389448
  if (fk == EQUAL && gk == EQUAL && f[0] == g[1] && f[1] == g[0])
431
  {
432
    // symmetric equality
433
161342
    return true;
434
  }
435
271652
  if (fk == NOT && gk == NOT && f[0].getKind() == EQUAL
436
249181
      && g[0].getKind() == EQUAL && f[0][0] == g[0][1] && f[0][1] == g[0][0])
437
  {
438
    // symmetric disequality
439
2007
    return true;
440
  }
441
226099
  return false;
442
}
443
444
13484036
Node CDProof::getSymmFact(TNode f)
445
{
446
13484036
  bool polarity = f.getKind() != NOT;
447
26968072
  TNode fatom = polarity ? f : f[0];
448
13484036
  if (fatom.getKind() != EQUAL || fatom[0] == fatom[1])
449
  {
450
5924201
    return Node::null();
451
  }
452
15119670
  Node symFact = fatom[1].eqNode(fatom[0]);
453
7559835
  return polarity ? symFact : symFact.notNode();
454
}
455
456
12989681
std::string CDProof::identify() const { return d_name; }
457
458
26685
}  // namespace CVC4