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-2024 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 : 48984 : 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 : 48984 : d_isNegated(false)
38 : : {
39 : 48984 : d_false = nodeManager()->mkConst(false);
40 : 48984 : }
41 : :
42 : 64498 : void AssertionPipeline::clear()
43 : : {
44 : 64498 : d_conflict = false;
45 : 64498 : d_isRefutationUnsound = false;
46 : 64498 : d_isModelUnsound = false;
47 : 64498 : d_isNegated = false;
48 : 64498 : d_nodes.clear();
49 : 64498 : d_iteSkolemMap.clear();
50 : 64498 : d_substsIndices.clear();
51 : 64498 : }
52 : :
53 : 593054 : void AssertionPipeline::push_back(Node n,
54 : : bool isInput,
55 : : ProofGenerator* pgen)
56 : : {
57 [ + + ]: 593054 : if (d_conflict)
58 : : {
59 : : // if we are already in conflict, we skip. This is required to handle the
60 : : // case where "false" was already seen as an input assertion.
61 : 3694 : return;
62 : : }
63 [ + + ]: 589360 : if (n == d_false)
64 : : {
65 : 6459 : markConflict();
66 : : }
67 [ + + ]: 582901 : else if (n.getKind() == Kind::AND)
68 : : {
69 : : // Immediately miniscope top-level AND, which is important for minimizing
70 : : // dependencies in proofs. We add each conjunct seperately, justifying
71 : : // each with an AND_ELIM step.
72 : 28750 : std::vector<Node> conjs;
73 [ + + ]: 14375 : if (isProofEnabled())
74 : : {
75 [ + + ]: 8351 : if (!isInput)
76 : : {
77 : 1065 : d_andElimEpg->addLazyStep(n, pgen, TrustId::PREPROCESS_LEMMA);
78 : : }
79 : : }
80 : 14375 : std::vector<Node> toProcess;
81 : 14375 : toProcess.emplace_back(n);
82 : 276826 : do
83 : : {
84 : 582402 : Node nc = toProcess.back();
85 : 291201 : toProcess.pop_back();
86 [ + + ]: 291201 : if (nc.getKind() == Kind::AND)
87 : : {
88 [ + + ]: 57818 : if (isProofEnabled())
89 : : {
90 : 27180 : NodeManager* nm = nodeManager();
91 [ + + ]: 159551 : for (size_t j = 0, nchild = nc.getNumChildren(); j < nchild; j++)
92 : : {
93 : 132371 : size_t jj = (nchild-1)-j;
94 : 132371 : Node in = nm->mkConstInt(Rational(jj));
95 : 397113 : d_andElimEpg->addStep(nc[jj], ProofRule::AND_ELIM, {nc}, {in});
96 : 132371 : toProcess.emplace_back(nc[jj]);
97 : : }
98 : : }
99 : : else
100 : : {
101 : 30638 : toProcess.insert(toProcess.end(), nc.rbegin(), nc.rend());
102 : : }
103 : : }
104 : : else
105 : : {
106 : 233383 : conjs.emplace_back(nc);
107 : : }
108 [ + + ]: 291201 : } while (!toProcess.empty());
109 : : // add each conjunct
110 [ + + ]: 247758 : for (const Node& nc : conjs)
111 : : {
112 [ + + ]: 233383 : push_back(nc, false, d_andElimEpg.get());
113 : : }
114 : 14375 : return;
115 : : }
116 : : else
117 : : {
118 : 568526 : d_nodes.push_back(n);
119 : : }
120 [ + - ]: 1149970 : Trace("assert-pipeline") << "Assertions: ...new assertion " << n
121 : 574985 : << ", isInput=" << isInput << std::endl;
122 [ + + ]: 574985 : if (isProofEnabled())
123 : : {
124 [ + + ]: 324892 : if (!isInput)
125 : : {
126 : : // notice this is always called, regardless of whether pgen is nullptr
127 : 220740 : d_pppg->notifyNewAssert(n, pgen);
128 : : }
129 : : else
130 : : {
131 [ - + ][ - + ]: 104152 : Assert(pgen == nullptr);
[ - - ]
132 : : // n is an input assertion, whose proof should be ASSUME.
133 : 104152 : d_pppg->notifyInput(n);
134 : : }
135 : : }
136 : : }
137 : :
138 : 28510 : void AssertionPipeline::pushBackTrusted(TrustNode trn)
139 : : {
140 [ - + ][ - + ]: 28510 : Assert(trn.getKind() == TrustNodeKind::LEMMA);
[ - - ]
141 : : // push back what was proven
142 : 28510 : push_back(trn.getProven(), false, trn.getGenerator());
143 : 28510 : }
144 : :
145 : 1292270 : void AssertionPipeline::replace(size_t i, Node n, ProofGenerator* pgen)
146 : : {
147 [ - + ][ - + ]: 1292270 : Assert(i < d_nodes.size());
[ - - ]
148 [ + + ]: 1292270 : if (n == d_nodes[i])
149 : : {
150 : : // no change, skip
151 : 953352 : return;
152 : : }
153 [ + - ]: 677842 : Trace("assert-pipeline") << "Assertions: Replace " << d_nodes[i] << " with "
154 : 338921 : << n << std::endl;
155 [ + + ]: 338921 : if (isProofEnabled())
156 : : {
157 : 195687 : d_pppg->notifyPreprocessed(d_nodes[i], n, pgen);
158 : : }
159 [ + + ]: 338921 : if (n == d_false)
160 : : {
161 : 3379 : markConflict();
162 : : }
163 : : else
164 : : {
165 : 335542 : d_nodes[i] = n;
166 : : }
167 : : }
168 : :
169 : 601912 : void AssertionPipeline::replaceTrusted(size_t i, TrustNode trn)
170 : : {
171 [ - + ][ - + ]: 601912 : Assert(i < d_nodes.size());
[ - - ]
172 [ + + ]: 601912 : if (trn.isNull())
173 : : {
174 : : // null trust node denotes no change, nothing to do
175 : 280965 : return;
176 : : }
177 [ - + ][ - + ]: 320947 : Assert(trn.getKind() == TrustNodeKind::REWRITE);
[ - - ]
178 [ - + ][ - + ]: 320947 : Assert(trn.getProven()[0] == d_nodes[i]);
[ - - ]
179 : 320947 : replace(i, trn.getNode(), trn.getGenerator());
180 : : }
181 : :
182 : 17053 : void AssertionPipeline::enableProofs(smt::PreprocessProofGenerator* pppg)
183 : : {
184 : 17053 : d_pppg = pppg;
185 [ + - ]: 17053 : if (d_andElimEpg == nullptr)
186 : : {
187 : 34106 : d_andElimEpg.reset(
188 : 34106 : new LazyCDProof(d_env, nullptr, userContext(), "AssertionsAndElim"));
189 : : }
190 : 17053 : }
191 : :
192 : 986099 : bool AssertionPipeline::isProofEnabled() const { return d_pppg != nullptr; }
193 : :
194 : 4188 : void AssertionPipeline::enableStoreSubstsInAsserts()
195 : : {
196 : 4188 : d_storeSubstsInAsserts = true;
197 : 4188 : d_nodes.push_back(nodeManager()->mkConst<bool>(true));
198 : 4188 : }
199 : :
200 : 40016 : void AssertionPipeline::disableStoreSubstsInAsserts()
201 : : {
202 : 40016 : d_storeSubstsInAsserts = false;
203 : 40016 : }
204 : :
205 : 2306 : void AssertionPipeline::addSubstitutionNode(Node n, ProofGenerator* pg)
206 : : {
207 [ - + ][ - + ]: 2306 : Assert(d_storeSubstsInAsserts);
[ - - ]
208 [ - + ][ - + ]: 2306 : Assert(n.getKind() == Kind::EQUAL);
[ - - ]
209 : 2306 : size_t prevNodeSize = d_nodes.size();
210 : 2306 : push_back(n, false, pg);
211 : : // remember this is a substitution index
212 [ + + ]: 4612 : for (size_t i = prevNodeSize, newSize = d_nodes.size(); i < newSize; i++)
213 : : {
214 : : // ensure rewritten
215 : 2306 : replace(i, rewrite(d_nodes[i]));
216 : 2306 : d_substsIndices.insert(i);
217 : : }
218 : 2306 : }
219 : :
220 : 888525 : bool AssertionPipeline::isSubstsIndex(size_t i) const
221 : : {
222 : 888525 : return d_storeSubstsInAsserts
223 [ + + ][ + + ]: 888525 : && d_substsIndices.find(i) != d_substsIndices.end();
224 : : }
225 : :
226 : 9838 : void AssertionPipeline::markConflict()
227 : : {
228 : 9838 : d_conflict = true;
229 : 9838 : d_nodes.clear();
230 : 9838 : d_iteSkolemMap.clear();
231 : 9838 : d_nodes.push_back(d_false);
232 : 9838 : }
233 : :
234 : 43 : void AssertionPipeline::markRefutationUnsound()
235 : : {
236 : 43 : d_isRefutationUnsound = true;
237 : 43 : }
238 : :
239 : 0 : void AssertionPipeline::markModelUnsound() { d_isModelUnsound = true; }
240 : :
241 : 2 : void AssertionPipeline::markNegated()
242 : : {
243 [ + - ][ - + ]: 2 : if (d_isRefutationUnsound || d_isModelUnsound)
244 : : {
245 : : // disallow unintuitive uses of global negation.
246 : 0 : std::stringstream ss;
247 : : ss << "Cannot negate the preprocessed assertions when already marked as "
248 : 0 : "refutation or model unsound.";
249 : 0 : throw LogicException(ss.str());
250 : : }
251 : 2 : d_isNegated = true;
252 : 2 : }
253 : :
254 : : } // namespace preprocessing
255 : : } // namespace cvc5::internal
|
