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