Branch data Line data Source code
1 : : /******************************************************************************
2 : : * This file is part of the cvc5 project.
3 : : *
4 : : * Copyright (c) 2009-2026 by the authors listed in the file AUTHORS
5 : : * in the top-level source directory and their institutional affiliations.
6 : : * All rights reserved. See the file COPYING in the top-level source
7 : : * directory for licensing information.
8 : : * ****************************************************************************
9 : : *
10 : : * Implementation of the trust node utility.
11 : : */
12 : :
13 : : #include "proof/trust_node.h"
14 : :
15 : : #include "proof/proof_ensure_closed.h"
16 : : #include "proof/proof_generator.h"
17 : :
18 : : namespace cvc5::internal {
19 : :
20 : 0 : const char* toString(TrustNodeKind tnk)
21 : : {
22 [ - - ][ - - ]: 0 : switch (tnk)
[ - ]
23 : : {
24 : 0 : case TrustNodeKind::CONFLICT: return "CONFLICT";
25 : 0 : case TrustNodeKind::LEMMA: return "LEMMA";
26 : 0 : case TrustNodeKind::PROP_EXP: return "PROP_EXP";
27 : 0 : case TrustNodeKind::REWRITE: return "REWRITE";
28 : 0 : default: return "?";
29 : : }
30 : : }
31 : :
32 : 0 : std::ostream& operator<<(std::ostream& out, TrustNodeKind tnk)
33 : : {
34 : 0 : out << toString(tnk);
35 : 0 : return out;
36 : : }
37 : :
38 : 421220 : TrustNode TrustNode::mkTrustConflict(Node conf, ProofGenerator* g)
39 : : {
40 : 421220 : Node ckey = getConflictProven(conf);
41 : : // if a generator is provided, should confirm that it can prove it
42 : 421220 : Assert(g == nullptr || g->hasProofFor(ckey));
43 : 842440 : return TrustNode(TrustNodeKind::CONFLICT, ckey, g);
44 : 421220 : }
45 : :
46 : 6388056 : TrustNode TrustNode::mkTrustLemma(Node lem, ProofGenerator* g)
47 : : {
48 : 6388056 : Node lkey = getLemmaProven(lem);
49 : : // if a generator is provided, should confirm that it can prove it
50 : 6388056 : Assert(g == nullptr || g->hasProofFor(lkey));
51 : 12776112 : return TrustNode(TrustNodeKind::LEMMA, lkey, g);
52 : 6388056 : }
53 : :
54 : 1392301 : TrustNode TrustNode::mkTrustPropExp(TNode lit, Node exp, ProofGenerator* g)
55 : : {
56 : 2784602 : Node pekey = getPropExpProven(lit, exp);
57 : 1392301 : Assert(g == nullptr || g->hasProofFor(pekey));
58 : 2784602 : return TrustNode(TrustNodeKind::PROP_EXP, pekey, g);
59 : 1392301 : }
60 : :
61 : 7069727 : TrustNode TrustNode::mkTrustRewrite(TNode n, Node nr, ProofGenerator* g)
62 : : {
63 : 14139454 : Node rkey = getRewriteProven(n, nr);
64 : 7069727 : Assert(g == nullptr || g->hasProofFor(rkey));
65 : 14139454 : return TrustNode(TrustNodeKind::REWRITE, rkey, g);
66 : 7069727 : }
67 : :
68 : 8554 : TrustNode TrustNode::mkReplaceGenTrustNode(const TrustNode& orig,
69 : : ProofGenerator* g)
70 : : {
71 : 17108 : return TrustNode(orig.getKind(), orig.getProven(), g);
72 : : }
73 : :
74 : 3 : TrustNode TrustNode::mkTrustNode(TrustNodeKind tnk, Node p, ProofGenerator* g)
75 : : {
76 : 3 : return TrustNode(tnk, p, g);
77 : : }
78 : :
79 : 17462924 : TrustNode TrustNode::null()
80 : : {
81 : 34925848 : return TrustNode(TrustNodeKind::INVALID, Node::null());
82 : : }
83 : :
84 : 32742785 : TrustNode::TrustNode(TrustNodeKind tnk, Node p, ProofGenerator* g)
85 : 32742785 : : d_tnk(tnk), d_proven(p), d_gen(g)
86 : : {
87 : : // does not make sense to provide null node with generator
88 [ + + ][ + - ]: 32742785 : Assert(!d_proven.isNull() || d_gen == nullptr);
[ - + ][ - + ]
[ - - ]
89 : 32742785 : }
90 : :
91 : 9212180 : TrustNodeKind TrustNode::getKind() const { return d_tnk; }
92 : :
93 : 14840386 : Node TrustNode::getNode() const
94 : : {
95 [ + + ][ + ]: 14840386 : switch (d_tnk)
96 : : {
97 : : // the node of lemma is the node itself
98 : 5348004 : case TrustNodeKind::LEMMA: return d_proven;
99 : : // the node of the rewrite is the right hand side of EQUAL
100 : 7344831 : case TrustNodeKind::REWRITE: return d_proven[1];
101 : : // the node of an explained propagation is the antecendant of an IMPLIES
102 : : // the node of a conflict is underneath a NOT
103 : 2147551 : default: return d_proven[0];
104 : : }
105 : : }
106 : :
107 : 12296384 : Node TrustNode::getProven() const { return d_proven; }
108 : :
109 : 6246058 : ProofGenerator* TrustNode::getGenerator() const { return d_gen; }
110 : :
111 : 23458283 : bool TrustNode::isNull() const { return d_proven.isNull(); }
112 : :
113 : 499595 : std::shared_ptr<ProofNode> TrustNode::toProofNode() const
114 : : {
115 [ + + ]: 499595 : if (d_gen == nullptr)
116 : : {
117 : 856 : return nullptr;
118 : : }
119 : 498739 : return d_gen->getProofFor(d_proven);
120 : : }
121 : :
122 : 495035 : Node TrustNode::getConflictProven(Node conf) { return conf.notNode(); }
123 : :
124 : 8727560 : Node TrustNode::getLemmaProven(Node lem) { return lem; }
125 : :
126 : 1718782 : Node TrustNode::getPropExpProven(TNode lit, Node exp)
127 : : {
128 : 1718782 : return NodeManager::mkNode(Kind::IMPLIES, exp, lit);
129 : : }
130 : :
131 : 7069727 : Node TrustNode::getRewriteProven(TNode n, Node nr) { return n.eqNode(nr); }
132 : :
133 : 1371053 : void TrustNode::debugCheckClosed(const Options& opts,
134 : : const char* c,
135 : : const char* ctx,
136 : : bool reqNullGen)
137 : : {
138 : 1371053 : pfgEnsureClosed(opts, d_proven, d_gen, c, ctx, reqNullGen);
139 : 1371053 : }
140 : :
141 : 0 : std::string TrustNode::identifyGenerator() const
142 : : {
143 [ - - ]: 0 : if (d_gen == nullptr)
144 : : {
145 : 0 : return "null";
146 : : }
147 : 0 : return d_gen->identify();
148 : : }
149 : :
150 : 0 : std::ostream& operator<<(std::ostream& out, TrustNode n)
151 : : {
152 : 0 : out << "(" << n.getKind() << " " << n.getProven() << " "
153 : 0 : << n.identifyGenerator() << ")";
154 : 0 : return out;
155 : : }
156 : :
157 : : } // namespace cvc5::internal
|
