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 : : * AssertionPipeline stores a list of assertions modified by
11 : : * preprocessing passes.
12 : : */
13 : :
14 : : #include "preprocessing/assertion_pipeline.h"
15 : :
16 : : #include "expr/node_manager.h"
17 : : #include "options/smt_options.h"
18 : : #include "proof/lazy_proof.h"
19 : : #include "smt/logic_exception.h"
20 : : #include "smt/preprocess_proof_generator.h"
21 : : #include "theory/builtin/proof_checker.h"
22 : : #include "util/rational.h"
23 : :
24 : : namespace cvc5::internal {
25 : : namespace preprocessing {
26 : :
27 : 28208 : AssertionPipeline::AssertionPipeline(Env& env)
28 : : : EnvObj(env),
29 : 28208 : d_storeSubstsInAsserts(false),
30 : 28208 : d_pppg(nullptr),
31 : 28208 : d_conflict(false),
32 : 28208 : d_isRefutationUnsound(false),
33 : 28208 : d_isModelUnsound(false),
34 : 28208 : d_isNegated(false)
35 : : {
36 : 28208 : d_false = nodeManager()->mkConst(false);
37 : 28208 : }
38 : :
39 : 40239 : void AssertionPipeline::clear()
40 : : {
41 : 40239 : d_conflict = false;
42 : 40239 : d_isRefutationUnsound = false;
43 : 40239 : d_isModelUnsound = false;
44 : 40239 : d_isNegated = false;
45 : 40239 : d_nodes.clear();
46 : 40239 : d_iteSkolemMap.clear();
47 : 40239 : d_substsIndices.clear();
48 : 40239 : }
49 : :
50 : 541952 : void AssertionPipeline::push_back(
51 : : Node n, bool isInput, ProofGenerator* pgen, TrustId trustId, bool ensureRew)
52 : : {
53 [ + + ]: 541952 : if (d_conflict)
54 : : {
55 : : // if we are already in conflict, we skip. This is required to handle the
56 : : // case where "false" was already seen as an input assertion.
57 : 682 : return;
58 : : }
59 : : // If proof enabled, notify the preprocess proof generator.
60 : : // Note that if n is (and F1 ... Fn), below we instead add the assertions
61 : : // F1 .... Fn whose proofs are AND_ELIM steps given a proof of n. We do not
62 : : // add n as an assertion. However, we also remember the proof for n itself.
63 : : // The reason is that in rare cases we may relearn n (say via rewriting
64 : : // another assumption) which may lead to a cyclic proof if that rewriting
65 : : // depended on one of F1 ... Fn.
66 [ + + ]: 541270 : if (isProofEnabled())
67 : : {
68 [ + + ]: 301106 : if (!isInput)
69 : : {
70 : : // notice this is always called, regardless of whether pgen is nullptr
71 : 214060 : d_pppg->notifyNewAssert(n, pgen, trustId);
72 : : }
73 : : else
74 : : {
75 [ - + ][ - + ]: 87046 : Assert(pgen == nullptr);
[ - - ]
76 : : // n is an input assertion, whose proof should be ASSUME.
77 : 87046 : d_pppg->notifyInput(n);
78 : : }
79 : : }
80 [ + + ]: 541270 : if (n == d_false)
81 : : {
82 : 2779 : markConflict();
83 : : }
84 [ + + ]: 538491 : else if (n.getKind() == Kind::AND)
85 : : {
86 : : // Immediately miniscope top-level AND, which is important for minimizing
87 : : // dependencies in proofs. We add each conjunct seperately, justifying
88 : : // each with an AND_ELIM step.
89 : 13131 : std::vector<Node> conjs;
90 [ + + ]: 13131 : if (isProofEnabled())
91 : : {
92 [ + + ]: 7867 : if (!isInput)
93 : : {
94 [ + + ][ + - ]: 1674 : Assert(pgen != nullptr || trustId != TrustId::UNKNOWN_PREPROCESS_LEMMA);
[ - + ][ - + ]
[ - - ]
95 : 1674 : d_andElimEpg->addLazyStep(n, pgen, trustId);
96 : : }
97 : : }
98 : 13131 : std::vector<Node> toProcess;
99 : 13131 : toProcess.emplace_back(n);
100 : : do
101 : : {
102 : 337688 : Node nc = toProcess.back();
103 : 337688 : toProcess.pop_back();
104 [ + + ]: 337688 : if (nc.getKind() == Kind::AND)
105 : : {
106 [ + + ]: 54306 : if (isProofEnabled())
107 : : {
108 : 24398 : NodeManager* nm = nodeManager();
109 [ + + ]: 196385 : for (size_t j = 0, nchild = nc.getNumChildren(); j < nchild; j++)
110 : : {
111 : 171987 : size_t jj = (nchild - 1) - j;
112 : 171987 : Node in = nm->mkConstInt(Rational(jj));
113 : : // Never overwrite here. This is because the assumption we would
114 : : // overwrite might be at a lower user context. Overwriting the
115 : : // assumption can lead to open proofs in incremental mode.
116 : 515961 : d_andElimEpg->addStep(nc[jj],
117 : : ProofRule::AND_ELIM,
118 : : {nc},
119 : : {in},
120 : : false,
121 : : CDPOverwrite::NEVER);
122 : 171987 : toProcess.emplace_back(nc[jj]);
123 : 171987 : }
124 : : }
125 : : else
126 : : {
127 : 29908 : toProcess.insert(toProcess.end(), nc.rbegin(), nc.rend());
128 : : }
129 : : }
130 : : else
131 : : {
132 : 283382 : conjs.emplace_back(nc);
133 : : }
134 [ + + ]: 337688 : } while (!toProcess.empty());
135 : : // add each conjunct
136 [ + + ]: 296513 : for (const Node& nc : conjs)
137 : : {
138 [ + + ]: 283382 : push_back(nc,
139 : : false,
140 : 283382 : d_andElimEpg.get(),
141 : : TrustId::UNKNOWN_PREPROCESS_LEMMA,
142 : : ensureRew);
143 : : }
144 : 13131 : return;
145 : 13131 : }
146 : : else
147 : : {
148 : 525360 : d_nodes.push_back(n);
149 [ + + ]: 525360 : if (ensureRew)
150 : : {
151 : 7183 : ensureRewritten(d_nodes.size() - 1);
152 : : }
153 : : }
154 [ + - ]: 1056278 : Trace("assert-pipeline") << "Assertions: ...new assertion " << n
155 : 528139 : << ", isInput=" << isInput << std::endl;
156 : : }
157 : :
158 : 32924 : void AssertionPipeline::pushBackTrusted(TrustNode trn,
159 : : TrustId trustId,
160 : : bool ensureRew)
161 : : {
162 [ - + ][ - + ]: 32924 : Assert(trn.getKind() == TrustNodeKind::LEMMA);
[ - - ]
163 : : // push back what was proven
164 : 32924 : push_back(trn.getProven(), false, trn.getGenerator(), trustId, ensureRew);
165 : 32924 : }
166 : :
167 : 1274228 : void AssertionPipeline::replace(size_t i,
168 : : Node n,
169 : : ProofGenerator* pgen,
170 : : TrustId trustId)
171 : : {
172 [ - + ][ - + ]: 1274228 : Assert(i < d_nodes.size());
[ - - ]
173 [ + + ]: 1274228 : if (n == d_nodes[i])
174 : : {
175 : : // no change, skip
176 : 937872 : return;
177 : : }
178 [ + - ]: 672712 : Trace("assert-pipeline") << "Assertions: Replace " << d_nodes[i] << " with "
179 : 336356 : << n << std::endl;
180 [ + + ]: 336356 : if (isProofEnabled())
181 : : {
182 [ + + ][ + - ]: 181571 : Assert(pgen != nullptr || trustId != TrustId::UNKNOWN_PREPROCESS);
[ - + ][ - + ]
[ - - ]
183 : 181571 : d_pppg->notifyPreprocessed(d_nodes[i], n, pgen, trustId);
184 : : }
185 [ + + ]: 336356 : if (n == d_false)
186 : : {
187 : 3284 : markConflict();
188 : : }
189 : : else
190 : : {
191 : 333072 : d_nodes[i] = n;
192 : : }
193 : : }
194 : :
195 : 460 : void AssertionPipeline::removeIteSkolem(TNode skolem)
196 : : {
197 : 460 : for (IteSkolemMap::iterator it = d_iteSkolemMap.begin();
198 [ + + ]: 470 : it != d_iteSkolemMap.end();)
199 : : {
200 [ + + ]: 10 : if (it->second == skolem)
201 : : {
202 : 6 : it = d_iteSkolemMap.erase(it);
203 : : }
204 : : else
205 : : {
206 : 4 : ++it;
207 : : }
208 : : }
209 : 460 : }
210 : :
211 : 620868 : void AssertionPipeline::replaceTrusted(size_t i, TrustNode trn, TrustId trustId)
212 : : {
213 [ - + ][ - + ]: 620868 : Assert(i < d_nodes.size());
[ - - ]
214 [ + + ]: 620868 : if (trn.isNull())
215 : : {
216 : : // null trust node denotes no change, nothing to do
217 : 304787 : return;
218 : : }
219 [ - + ][ - + ]: 316081 : Assert(trn.getKind() == TrustNodeKind::REWRITE);
[ - - ]
220 [ - + ][ - + ]: 316081 : Assert(trn.getProven()[0] == d_nodes[i]);
[ - - ]
221 : 316081 : replace(i, trn.getNode(), trn.getGenerator(), trustId);
222 : : }
223 : :
224 : 21368 : void AssertionPipeline::ensureRewritten(size_t i)
225 : : {
226 [ - + ][ - + ]: 21368 : Assert(i < d_nodes.size());
[ - - ]
227 [ + + ]: 21368 : replace(i, rewrite(d_nodes[i]), d_rewpg.get());
228 : 21368 : }
229 : :
230 : 13902 : void AssertionPipeline::enableProofs(smt::PreprocessProofGenerator* pppg)
231 : : {
232 : 13902 : d_pppg = pppg;
233 [ + - ]: 13902 : if (d_andElimEpg == nullptr)
234 : : {
235 : 27804 : d_andElimEpg.reset(
236 : 27804 : new LazyCDProof(d_env, nullptr, userContext(), "AssertionsAndElim"));
237 : : }
238 [ + - ]: 13902 : if (d_rewpg == nullptr)
239 : : {
240 : 13902 : d_rewpg.reset(new RewriteProofGenerator(d_env));
241 : : }
242 : 13902 : }
243 : :
244 : 945063 : bool AssertionPipeline::isProofEnabled() const { return d_pppg != nullptr; }
245 : :
246 : 3219 : void AssertionPipeline::enableStoreSubstsInAsserts()
247 : : {
248 : 3219 : d_storeSubstsInAsserts = true;
249 : 3219 : d_nodes.push_back(nodeManager()->mkConst<bool>(true));
250 : 3219 : }
251 : :
252 : 27106 : void AssertionPipeline::disableStoreSubstsInAsserts()
253 : : {
254 : 27106 : d_storeSubstsInAsserts = false;
255 : 27106 : }
256 : :
257 : 1865 : void AssertionPipeline::addSubstitutionNode(Node n,
258 : : ProofGenerator* pg,
259 : : TrustId trustId)
260 : : {
261 [ - + ][ - + ]: 1865 : Assert(d_storeSubstsInAsserts);
[ - - ]
262 [ - + ][ - + ]: 1865 : Assert(n.getKind() == Kind::EQUAL);
[ - - ]
263 : 1865 : size_t prevNodeSize = d_nodes.size();
264 : : // ensure rewritten here
265 : 1865 : push_back(n, false, pg, trustId, true);
266 : : // remember this is a substitution index
267 [ + + ]: 3730 : for (size_t i = prevNodeSize, newSize = d_nodes.size(); i < newSize; i++)
268 : : {
269 : 1865 : d_substsIndices.insert(i);
270 : : }
271 : 1865 : }
272 : :
273 : 917826 : bool AssertionPipeline::isSubstsIndex(size_t i) const
274 : : {
275 : 917826 : return d_storeSubstsInAsserts
276 [ + + ][ + + ]: 917826 : && d_substsIndices.find(i) != d_substsIndices.end();
277 : : }
278 : :
279 : 6063 : void AssertionPipeline::markConflict()
280 : : {
281 : 6063 : d_conflict = true;
282 : 6063 : d_nodes.clear();
283 : 6063 : d_iteSkolemMap.clear();
284 : 6063 : d_nodes.push_back(d_false);
285 : 6063 : }
286 : :
287 : 65 : void AssertionPipeline::markRefutationUnsound()
288 : : {
289 : 65 : d_isRefutationUnsound = true;
290 : 65 : }
291 : :
292 : 0 : void AssertionPipeline::markModelUnsound() { d_isModelUnsound = true; }
293 : :
294 : 2 : void AssertionPipeline::markNegated()
295 : : {
296 [ + - ][ - + ]: 2 : if (d_isRefutationUnsound || d_isModelUnsound)
297 : : {
298 : : // disallow unintuitive uses of global negation.
299 : 0 : std::stringstream ss;
300 : : ss << "Cannot negate the preprocessed assertions when already marked as "
301 : 0 : "refutation or model unsound.";
302 : 0 : throw LogicException(ss.str());
303 : 0 : }
304 : 2 : d_isNegated = true;
305 : 2 : }
306 : :
307 : : } // namespace preprocessing
308 : : } // namespace cvc5::internal
|
