Branch data Line data Source code
1 : : /******************************************************************************
2 : : * Top contributors (to current version):
3 : : * Andrew Reynolds, Andres Noetzli, Aina Niemetz
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 : : * AssertionPipeline stores a list of assertions modified by
14 : : * preprocessing passes.
15 : : */
16 : :
17 : : #include "preprocessing/assertion_pipeline.h"
18 : :
19 : : #include "expr/node_manager.h"
20 : : #include "options/smt_options.h"
21 : : #include "proof/lazy_proof.h"
22 : : #include "smt/logic_exception.h"
23 : : #include "smt/preprocess_proof_generator.h"
24 : : #include "theory/builtin/proof_checker.h"
25 : : #include "util/rational.h"
26 : :
27 : : namespace cvc5::internal {
28 : : namespace preprocessing {
29 : :
30 : 51363 : AssertionPipeline::AssertionPipeline(Env& env)
31 : : : EnvObj(env),
32 : : d_storeSubstsInAsserts(false),
33 : : d_pppg(nullptr),
34 : : d_conflict(false),
35 : : d_isRefutationUnsound(false),
36 : : d_isModelUnsound(false),
37 : 51363 : d_isNegated(false)
38 : : {
39 : 51363 : d_false = nodeManager()->mkConst(false);
40 : 51363 : }
41 : :
42 : 64809 : void AssertionPipeline::clear()
43 : : {
44 : 64809 : d_conflict = false;
45 : 64809 : d_isRefutationUnsound = false;
46 : 64809 : d_isModelUnsound = false;
47 : 64809 : d_isNegated = false;
48 : 64809 : d_nodes.clear();
49 : 64809 : d_iteSkolemMap.clear();
50 : 64809 : d_substsIndices.clear();
51 : 64809 : }
52 : :
53 : 550266 : void AssertionPipeline::push_back(
54 : : Node n, bool isInput, ProofGenerator* pgen, TrustId trustId, bool ensureRew)
55 : : {
56 [ + + ]: 550266 : if (d_conflict)
57 : : {
58 : : // if we are already in conflict, we skip. This is required to handle the
59 : : // case where "false" was already seen as an input assertion.
60 : 4119 : return;
61 : : }
62 [ + + ]: 546147 : if (n == d_false)
63 : : {
64 : 6599 : markConflict();
65 : : }
66 [ + + ]: 539548 : else if (n.getKind() == Kind::AND)
67 : : {
68 : : // Immediately miniscope top-level AND, which is important for minimizing
69 : : // dependencies in proofs. We add each conjunct seperately, justifying
70 : : // each with an AND_ELIM step.
71 : 30116 : std::vector<Node> conjs;
72 [ + + ]: 15058 : if (isProofEnabled())
73 : : {
74 [ + + ]: 8530 : if (!isInput)
75 : : {
76 [ + + ][ - + ]: 1535 : Assert(pgen != nullptr || trustId != TrustId::UNKNOWN_PREPROCESS_LEMMA);
[ - + ][ - - ]
77 : 1535 : d_andElimEpg->addLazyStep(n, pgen, trustId);
78 : : }
79 : : }
80 : 15058 : std::vector<Node> toProcess;
81 : 15058 : toProcess.emplace_back(n);
82 : 280397 : do
83 : : {
84 : 590910 : Node nc = toProcess.back();
85 : 295455 : toProcess.pop_back();
86 [ + + ]: 295455 : if (nc.getKind() == Kind::AND)
87 : : {
88 [ + + ]: 58901 : if (isProofEnabled())
89 : : {
90 : 28001 : NodeManager* nm = nodeManager();
91 [ + + ]: 162829 : for (size_t j = 0, nchild = nc.getNumChildren(); j < nchild; j++)
92 : : {
93 : 134828 : size_t jj = (nchild-1)-j;
94 : 134828 : Node in = nm->mkConstInt(Rational(jj));
95 : : // Never overwrite here. This is because the assumption we would
96 : : // overwrite might be at a lower user context. Overwriting the
97 : : // assumption can lead to open proofs in incremental mode.
98 : 404484 : d_andElimEpg->addStep(nc[jj],
99 : : ProofRule::AND_ELIM,
100 : : {nc},
101 : : {in},
102 : : false,
103 : 269656 : CDPOverwrite::NEVER);
104 : 134828 : toProcess.emplace_back(nc[jj]);
105 : : }
106 : : }
107 : : else
108 : : {
109 : 30900 : toProcess.insert(toProcess.end(), nc.rbegin(), nc.rend());
110 : : }
111 : : }
112 : : else
113 : : {
114 : 236554 : conjs.emplace_back(nc);
115 : : }
116 [ + + ]: 295455 : } while (!toProcess.empty());
117 : : // add each conjunct
118 [ + + ]: 251612 : for (const Node& nc : conjs)
119 : : {
120 [ + + ]: 236554 : push_back(nc,
121 : : false,
122 : 236554 : d_andElimEpg.get(),
123 : : TrustId::UNKNOWN_PREPROCESS_LEMMA,
124 : : ensureRew);
125 : : }
126 : 15058 : return;
127 : : }
128 : : else
129 : : {
130 : 524490 : d_nodes.push_back(n);
131 [ + + ]: 524490 : if (ensureRew)
132 : : {
133 : 7695 : ensureRewritten(d_nodes.size() - 1);
134 : : }
135 : : }
136 [ + - ]: 1062180 : Trace("assert-pipeline") << "Assertions: ...new assertion " << n
137 : 531089 : << ", isInput=" << isInput << std::endl;
138 [ + + ]: 531089 : if (isProofEnabled())
139 : : {
140 [ + + ]: 284355 : if (!isInput)
141 : : {
142 : : // notice this is always called, regardless of whether pgen is nullptr
143 : 179126 : d_pppg->notifyNewAssert(n, pgen, trustId);
144 : : }
145 : : else
146 : : {
147 [ - + ][ - + ]: 105229 : Assert(pgen == nullptr);
[ - - ]
148 : : // n is an input assertion, whose proof should be ASSUME.
149 : 105229 : d_pppg->notifyInput(n);
150 : : }
151 : : }
152 : : }
153 : :
154 : 35408 : void AssertionPipeline::pushBackTrusted(TrustNode trn,
155 : : TrustId trustId,
156 : : bool ensureRew)
157 : : {
158 [ - + ][ - + ]: 35408 : Assert(trn.getKind() == TrustNodeKind::LEMMA);
[ - - ]
159 : : // push back what was proven
160 : 35408 : push_back(trn.getProven(), false, trn.getGenerator(), trustId, ensureRew);
161 : 35408 : }
162 : :
163 : 1282650 : void AssertionPipeline::replace(size_t i,
164 : : Node n,
165 : : ProofGenerator* pgen,
166 : : TrustId trustId)
167 : : {
168 [ - + ][ - + ]: 1282650 : Assert(i < d_nodes.size());
[ - - ]
169 [ + + ]: 1282650 : if (n == d_nodes[i])
170 : : {
171 : : // no change, skip
172 : 922770 : return;
173 : : }
174 [ + - ]: 719768 : Trace("assert-pipeline") << "Assertions: Replace " << d_nodes[i] << " with "
175 : 359884 : << n << std::endl;
176 [ + + ]: 359884 : if (isProofEnabled())
177 : : {
178 [ + + ][ - + ]: 207507 : Assert(pgen != nullptr || trustId != TrustId::UNKNOWN_PREPROCESS);
[ - + ][ - - ]
179 : 207507 : d_pppg->notifyPreprocessed(d_nodes[i], n, pgen, trustId);
180 : : }
181 [ + + ]: 359884 : if (n == d_false)
182 : : {
183 : 4224 : markConflict();
184 : : }
185 : : else
186 : : {
187 : 355660 : d_nodes[i] = n;
188 : : }
189 : : }
190 : :
191 : 620379 : void AssertionPipeline::replaceTrusted(size_t i, TrustNode trn, TrustId trustId)
192 : : {
193 [ - + ][ - + ]: 620379 : Assert(i < d_nodes.size());
[ - - ]
194 [ + + ]: 620379 : if (trn.isNull())
195 : : {
196 : : // null trust node denotes no change, nothing to do
197 : 283039 : return;
198 : : }
199 [ - + ][ - + ]: 337340 : Assert(trn.getKind() == TrustNodeKind::REWRITE);
[ - - ]
200 [ - + ][ - + ]: 337340 : Assert(trn.getProven()[0] == d_nodes[i]);
[ - - ]
201 : 337340 : replace(i, trn.getNode(), trn.getGenerator(), trustId);
202 : : }
203 : :
204 : 20862 : void AssertionPipeline::ensureRewritten(size_t i)
205 : : {
206 [ - + ][ - + ]: 20862 : Assert(i < d_nodes.size());
[ - - ]
207 [ + + ]: 20862 : replace(i, rewrite(d_nodes[i]), d_rewpg.get());
208 : 20862 : }
209 : :
210 : 18769 : void AssertionPipeline::enableProofs(smt::PreprocessProofGenerator* pppg)
211 : : {
212 : 18769 : d_pppg = pppg;
213 [ + - ]: 18769 : if (d_andElimEpg == nullptr)
214 : : {
215 : 37538 : d_andElimEpg.reset(
216 : 37538 : new LazyCDProof(d_env, nullptr, userContext(), "AssertionsAndElim"));
217 : : }
218 [ + - ]: 18769 : if (d_rewpg == nullptr)
219 : : {
220 : 18769 : d_rewpg.reset(new RewriteProofGenerator(d_env));
221 : : }
222 : 18769 : }
223 : :
224 : 964932 : bool AssertionPipeline::isProofEnabled() const { return d_pppg != nullptr; }
225 : :
226 : 3544 : void AssertionPipeline::enableStoreSubstsInAsserts()
227 : : {
228 : 3544 : d_storeSubstsInAsserts = true;
229 : 3544 : d_nodes.push_back(nodeManager()->mkConst<bool>(true));
230 : 3544 : }
231 : :
232 : 42723 : void AssertionPipeline::disableStoreSubstsInAsserts()
233 : : {
234 : 42723 : d_storeSubstsInAsserts = false;
235 : 42723 : }
236 : :
237 : 1885 : void AssertionPipeline::addSubstitutionNode(Node n,
238 : : ProofGenerator* pg,
239 : : TrustId trustId)
240 : : {
241 [ - + ][ - + ]: 1885 : Assert(d_storeSubstsInAsserts);
[ - - ]
242 [ - + ][ - + ]: 1885 : Assert(n.getKind() == Kind::EQUAL);
[ - - ]
243 : 1885 : size_t prevNodeSize = d_nodes.size();
244 : : // ensure rewritten here
245 : 1885 : push_back(n, false, pg, trustId, true);
246 : : // remember this is a substitution index
247 [ + + ]: 3770 : for (size_t i = prevNodeSize, newSize = d_nodes.size(); i < newSize; i++)
248 : : {
249 : 1885 : d_substsIndices.insert(i);
250 : : }
251 : 1885 : }
252 : :
253 : 901784 : bool AssertionPipeline::isSubstsIndex(size_t i) const
254 : : {
255 : 901784 : return d_storeSubstsInAsserts
256 [ + + ][ + + ]: 901784 : && d_substsIndices.find(i) != d_substsIndices.end();
257 : : }
258 : :
259 : 10823 : void AssertionPipeline::markConflict()
260 : : {
261 : 10823 : d_conflict = true;
262 : 10823 : d_nodes.clear();
263 : 10823 : d_iteSkolemMap.clear();
264 : 10823 : d_nodes.push_back(d_false);
265 : 10823 : }
266 : :
267 : 68 : void AssertionPipeline::markRefutationUnsound()
268 : : {
269 : 68 : d_isRefutationUnsound = true;
270 : 68 : }
271 : :
272 : 0 : void AssertionPipeline::markModelUnsound() { d_isModelUnsound = true; }
273 : :
274 : 2 : void AssertionPipeline::markNegated()
275 : : {
276 [ + - ][ - + ]: 2 : if (d_isRefutationUnsound || d_isModelUnsound)
277 : : {
278 : : // disallow unintuitive uses of global negation.
279 : 0 : std::stringstream ss;
280 : : ss << "Cannot negate the preprocessed assertions when already marked as "
281 : 0 : "refutation or model unsound.";
282 : 0 : throw LogicException(ss.str());
283 : : }
284 : 2 : d_isNegated = true;
285 : 2 : }
286 : :
287 : : } // namespace preprocessing
288 : : } // namespace cvc5::internal
|
