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 debug checks for ensuring proofs are closed.
11 : : */
12 : :
13 : : #include "proof/proof_ensure_closed.h"
14 : :
15 : : #include <sstream>
16 : :
17 : : #include "options/proof_options.h"
18 : : #include "options/smt_options.h"
19 : : #include "proof/proof_generator.h"
20 : : #include "proof/proof_node.h"
21 : : #include "proof/proof_node_algorithm.h"
22 : :
23 : : namespace cvc5::internal {
24 : :
25 : : /**
26 : : * Ensure closed with respect to assumptions, internal version, which
27 : : * generalizes the check for a proof generator or a proof node.
28 : : */
29 : 2613611 : void ensureClosedWrtInternal(const Options& opts,
30 : : Node proven,
31 : : ProofGenerator* pg,
32 : : ProofNode* pnp,
33 : : const std::vector<Node>& assumps,
34 : : const char* c,
35 : : const char* ctx,
36 : : bool reqGen)
37 : : {
38 [ + + ]: 2613611 : if (!opts.smt.produceProofs)
39 : : {
40 : : // proofs not enabled, do not do check
41 : 2589405 : return;
42 : : }
43 : 2514781 : bool isTraceDebug = TraceIsOn(c);
44 [ + + ][ + - ]: 2514781 : if (opts.proof.proofCheck != options::ProofCheckMode::EAGER && !isTraceDebug)
45 : : {
46 : : // trace is off and proof new eager checking is off, do not do check
47 : 2490495 : return;
48 : : }
49 : 24286 : std::stringstream sdiag;
50 : 24286 : bool isTraceOn = TraceIsOn(c);
51 [ + - ]: 24286 : if (!isTraceOn)
52 : : {
53 : 24286 : sdiag << ", use -t " << c << " for details";
54 : : }
55 : 24286 : bool dumpProofTraceOn = TraceIsOn("dump-proof-error");
56 [ + - ]: 24286 : if (!dumpProofTraceOn)
57 : : {
58 : 24286 : sdiag << ", use -t dump-proof-error for details on proof";
59 : : }
60 : : // get the proof node in question, which is either provided or built by the
61 : : // proof generator
62 : 24286 : std::shared_ptr<ProofNode> pn;
63 : 24286 : std::stringstream ss;
64 [ + + ]: 24286 : if (pnp != nullptr)
65 : : {
66 [ - + ][ - + ]: 7 : Assert(pg == nullptr);
[ - - ]
67 : 7 : ss << "ProofNode in context " << ctx;
68 : : }
69 : : else
70 : : {
71 [ + + ][ - - ]: 48558 : ss << "ProofGenerator: " << (pg == nullptr ? "null" : pg->identify())
72 [ + + ]: 48558 : << " in context " << ctx;
73 [ + + ]: 24279 : if (pg == nullptr)
74 : : {
75 : : // only failure if flag is true
76 [ - + ]: 80 : if (reqGen)
77 : : {
78 : 0 : Unreachable() << "...ensureClosed: no generator in context " << ctx
79 : 0 : << sdiag.str();
80 : : }
81 : : }
82 : : else
83 : : {
84 [ - + ][ - + ]: 24199 : Assert(!proven.isNull());
[ - - ]
85 : 24199 : pn = pg->getProofFor(proven);
86 : 24199 : pnp = pn.get();
87 : : }
88 : : }
89 [ + - ][ - + ]: 24286 : Trace(c) << "=== ensureClosed: " << ss.str() << std::endl;
[ - - ]
90 [ + - ]: 24286 : Trace(c) << "Proven: " << proven << std::endl;
91 [ + + ]: 24286 : if (pnp == nullptr)
92 : : {
93 [ + - ]: 80 : if (pg == nullptr)
94 : : {
95 : : // did not require generator
96 [ - + ][ - + ]: 80 : Assert(!reqGen);
[ - - ]
97 [ + - ]: 160 : Trace(c) << "...ensureClosed: no generator in context " << ctx
98 : 80 : << std::endl;
99 : 80 : return;
100 : : }
101 : : }
102 : : // if we don't have a proof node, a generator failed
103 [ - + ]: 24206 : if (pnp == nullptr)
104 : : {
105 : 0 : Assert(pg != nullptr);
106 : 0 : AlwaysAssert(false) << "...ensureClosed: null proof from " << ss.str()
107 : 0 : << sdiag.str();
108 : : }
109 : 24206 : std::vector<Node> fassumps;
110 : 24206 : expr::getFreeAssumptions(pnp, fassumps);
111 : 24206 : bool isClosed = true;
112 : 24206 : std::stringstream ssf;
113 [ + + ]: 24223 : for (const Node& fa : fassumps)
114 : : {
115 [ - + ]: 17 : if (std::find(assumps.begin(), assumps.end(), fa) == assumps.end())
116 : : {
117 : 0 : isClosed = false;
118 : 0 : ssf << "- " << fa << std::endl;
119 : : }
120 : : }
121 [ - + ]: 24206 : if (!isClosed)
122 : : {
123 [ - - ]: 0 : Trace(c) << "Free assumptions:" << std::endl;
124 : 0 : Trace(c) << ssf.str();
125 [ - - ]: 0 : if (!assumps.empty())
126 : : {
127 [ - - ]: 0 : Trace(c) << "Expected assumptions:" << std::endl;
128 [ - - ]: 0 : for (const Node& a : assumps)
129 : : {
130 [ - - ]: 0 : Trace(c) << "- " << a << std::endl;
131 : : }
132 : : }
133 [ - - ]: 0 : if (dumpProofTraceOn)
134 : : {
135 [ - - ]: 0 : Trace("dump-proof-error") << " Proof: " << *pnp << std::endl;
136 : : }
137 : : }
138 : 48412 : AlwaysAssert(isClosed) << "...ensureClosed: open proof from " << ss.str()
139 [ - + ][ - + ]: 24206 : << sdiag.str();
[ - - ]
140 [ + - ]: 24206 : Trace(c) << "...ensureClosed: success" << std::endl;
141 [ + - ]: 24206 : Trace(c) << "====" << std::endl;
142 [ + + ][ + + ]: 24446 : }
[ + + ]
143 : :
144 : 2613604 : void pfgEnsureClosed(const Options& opts,
145 : : Node proven,
146 : : ProofGenerator* pg,
147 : : const char* c,
148 : : const char* ctx,
149 : : bool reqGen)
150 : : {
151 [ - + ][ - + ]: 2613604 : Assert(!proven.isNull());
[ - - ]
152 : : // proof generator may be null
153 : 2613604 : std::vector<Node> assumps;
154 : 2613604 : ensureClosedWrtInternal(opts, proven, pg, nullptr, assumps, c, ctx, reqGen);
155 : 2613604 : }
156 : :
157 : 0 : void pfgEnsureClosedWrt(const Options& opts,
158 : : Node proven,
159 : : ProofGenerator* pg,
160 : : const std::vector<Node>& assumps,
161 : : const char* c,
162 : : const char* ctx,
163 : : bool reqGen)
164 : : {
165 : 0 : Assert(!proven.isNull());
166 : : // proof generator may be null
167 : 0 : ensureClosedWrtInternal(opts, proven, pg, nullptr, assumps, c, ctx, reqGen);
168 : 0 : }
169 : :
170 : 0 : void pfnEnsureClosed(const Options& opts,
171 : : ProofNode* pn,
172 : : const char* c,
173 : : const char* ctx)
174 : : {
175 : 0 : ensureClosedWrtInternal(opts, Node::null(), nullptr, pn, {}, c, ctx, false);
176 : 0 : }
177 : :
178 : 7 : void pfnEnsureClosedWrt(const Options& opts,
179 : : ProofNode* pn,
180 : : const std::vector<Node>& assumps,
181 : : const char* c,
182 : : const char* ctx)
183 : : {
184 : 7 : ensureClosedWrtInternal(
185 : 14 : opts, Node::null(), nullptr, pn, assumps, c, ctx, false);
186 : 7 : }
187 : :
188 : : } // namespace cvc5::internal
|
