GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/trust_node.cpp Lines: 48 62 77.4 %
Date: 2021-03-23 Branches: 70 202 34.7 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file trust_node.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 the trust node utility
13
 **/
14
15
#include "theory/trust_node.h"
16
17
#include "expr/proof_ensure_closed.h"
18
#include "expr/proof_generator.h"
19
20
namespace CVC4 {
21
namespace theory {
22
23
const char* toString(TrustNodeKind tnk)
24
{
25
  switch (tnk)
26
  {
27
    case TrustNodeKind::CONFLICT: return "CONFLICT";
28
    case TrustNodeKind::LEMMA: return "LEMMA";
29
    case TrustNodeKind::PROP_EXP: return "PROP_EXP";
30
    case TrustNodeKind::REWRITE: return "REWRITE";
31
    default: return "?";
32
  }
33
}
34
35
std::ostream& operator<<(std::ostream& out, TrustNodeKind tnk)
36
{
37
  out << toString(tnk);
38
  return out;
39
}
40
41
303920
TrustNode TrustNode::mkTrustConflict(Node conf, ProofGenerator* g)
42
{
43
607840
  Node ckey = getConflictProven(conf);
44
  // if a generator is provided, should confirm that it can prove it
45
303920
  Assert(g == nullptr || g->hasProofFor(ckey));
46
607840
  return TrustNode(TrustNodeKind::CONFLICT, ckey, g);
47
}
48
49
1723867
TrustNode TrustNode::mkTrustLemma(Node lem, ProofGenerator* g)
50
{
51
3447734
  Node lkey = getLemmaProven(lem);
52
  // if a generator is provided, should confirm that it can prove it
53
1723867
  Assert(g == nullptr || g->hasProofFor(lkey));
54
3447734
  return TrustNode(TrustNodeKind::LEMMA, lkey, g);
55
}
56
57
556725
TrustNode TrustNode::mkTrustPropExp(TNode lit, Node exp, ProofGenerator* g)
58
{
59
1113450
  Node pekey = getPropExpProven(lit, exp);
60
556725
  Assert(g == nullptr || g->hasProofFor(pekey));
61
1113450
  return TrustNode(TrustNodeKind::PROP_EXP, pekey, g);
62
}
63
64
1964934
TrustNode TrustNode::mkTrustRewrite(TNode n, Node nr, ProofGenerator* g)
65
{
66
3929868
  Node rkey = getRewriteProven(n, nr);
67
1964934
  Assert(g == nullptr || g->hasProofFor(rkey));
68
3929868
  return TrustNode(TrustNodeKind::REWRITE, rkey, g);
69
}
70
71
4285718
TrustNode TrustNode::null()
72
{
73
4285718
  return TrustNode(TrustNodeKind::INVALID, Node::null());
74
}
75
76
8835164
TrustNode::TrustNode(TrustNodeKind tnk, Node p, ProofGenerator* g)
77
8835164
    : d_tnk(tnk), d_proven(p), d_gen(g)
78
{
79
  // does not make sense to provide null node with generator
80
8835164
  Assert(!d_proven.isNull() || d_gen == nullptr);
81
8835164
}
82
83
2690724
TrustNodeKind TrustNode::getKind() const { return d_tnk; }
84
85
6813218
Node TrustNode::getNode() const
86
{
87
6813218
  switch (d_tnk)
88
  {
89
    // the node of lemma is the node itself
90
2550198
    case TrustNodeKind::LEMMA: return d_proven;
91
    // the node of the rewrite is the right hand side of EQUAL
92
2480596
    case TrustNodeKind::REWRITE: return d_proven[1];
93
    // the node of an explained propagation is the antecendant of an IMPLIES
94
    // the node of a conflict is underneath a NOT
95
1782424
    default: return d_proven[0];
96
  }
97
}
98
99
2975601
Node TrustNode::getProven() const { return d_proven; }
100
101
1524210
ProofGenerator* TrustNode::getGenerator() const { return d_gen; }
102
103
7436219
bool TrustNode::isNull() const { return d_proven.isNull(); }
104
105
76882
std::shared_ptr<ProofNode> TrustNode::toProofNode() const
106
{
107
76882
  if (d_gen == nullptr)
108
  {
109
627
    return nullptr;
110
  }
111
76255
  return d_gen->getProofFor(d_proven);
112
}
113
114
319228
Node TrustNode::getConflictProven(Node conf) { return conf.notNode(); }
115
116
1925787
Node TrustNode::getLemmaProven(Node lem) { return lem; }
117
118
628482
Node TrustNode::getPropExpProven(TNode lit, Node exp)
119
{
120
628482
  return NodeManager::currentNM()->mkNode(kind::IMPLIES, exp, lit);
121
}
122
123
1964934
Node TrustNode::getRewriteProven(TNode n, Node nr) { return n.eqNode(nr); }
124
125
545226
void TrustNode::debugCheckClosed(const char* c,
126
                                 const char* ctx,
127
                                 bool reqNullGen)
128
{
129
545226
  pfgEnsureClosed(d_proven, d_gen, c, ctx, reqNullGen);
130
545226
}
131
132
61736
std::string TrustNode::identifyGenerator() const
133
{
134
61736
  if (d_gen == nullptr)
135
  {
136
1359
    return "null";
137
  }
138
60377
  return d_gen->identify();
139
}
140
141
std::ostream& operator<<(std::ostream& out, TrustNode n)
142
{
143
  out << "(" << n.getKind() << " " << n.getProven() << " "
144
      << n.identifyGenerator() << ")";
145
  return out;
146
}
147
148
}  // namespace theory
149
26685
}  // namespace CVC4