Branch data Line data Source code
1 : : /******************************************************************************
2 : : * Top contributors (to current version):
3 : : * Andrew Reynolds, Daniel Larraz
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 : : * Conflict processor module
14 : : */
15 : :
16 : : #include "theory/conflict_processor.h"
17 : :
18 : : #include "expr/node_algorithm.h"
19 : : #include "expr/skolem_manager.h"
20 : : #include "options/smt_options.h"
21 : : #include "options/theory_options.h"
22 : : #include "theory/strings/regexp_eval.h"
23 : : #include "theory/theory_engine.h"
24 : :
25 : : using namespace cvc5::internal::kind;
26 : :
27 : : namespace cvc5::internal {
28 : : namespace theory {
29 : :
30 : 8 : ConflictProcessor::ConflictProcessor(Env& env, bool useExtRewriter)
31 : 8 : : EnvObj(env), d_useExtRewriter(useExtRewriter), d_stats(statisticsRegistry())
32 : : {
33 : 8 : NodeManager* nm = env.getNodeManager();
34 : 8 : d_true = nm->mkConst(true);
35 : 8 : d_false = nm->mkConst(false);
36 : 8 : }
37 : :
38 : 154 : TrustNode ConflictProcessor::processLemma(const TrustNode& lem)
39 : : {
40 : 154 : ++d_stats.d_initLemmas;
41 : 308 : Node lemma = lem.getProven();
42 : 154 : lemma = rewrite(lemma);
43 : : // do not use compression, because we will erase substitutions below
44 : 308 : SubstitutionMap s(nullptr, false);
45 : 308 : std::map<Node, Node> varToExp;
46 : 308 : std::vector<Node> tgtLits;
47 : : // decompose lemma into AND( s ) => OR( tgtLits )
48 : 154 : decomposeLemma(lemma, s, varToExp, tgtLits);
49 : : // if we didn't infer a substitution, we are done
50 [ + + ]: 154 : if (s.empty())
51 : : {
52 [ + - ]: 138 : Trace("confp-nprocess") << "...no substitution for " << lemma << std::endl;
53 : 138 : return TrustNode::null();
54 : : }
55 : 16 : ++d_stats.d_lemmas;
56 [ + - ]: 16 : Trace("confp") << "Decomposed " << lemma << std::endl;
57 [ + - ][ - + ]: 16 : Trace("confp") << "- Substitution: " << s.toString() << std::endl;
[ - - ]
58 [ + - ]: 16 : Trace("confp") << "- Target: " << tgtLits << std::endl;
59 : : // Check if the substitution implies one of the tgtLit. If so, store in
60 : : // tgtLit. If we find a single one, then we can ignore the others in tgtLits.
61 : 32 : Node tgtLit;
62 : 32 : std::vector<Node> tgtLitsNc;
63 : : // Maps evaluated literals to their source.
64 : 32 : std::map<Node, Node> evMap;
65 : 16 : std::map<Node, Node>::iterator itm;
66 [ + + ]: 48 : for (const Node& tlit : tgtLits)
67 : : {
68 : 40 : Node ev = evaluateSubstitution(s, tlit);
69 [ + - ]: 40 : Trace("confp-debug") << "eval " << tlit << " is " << ev << std::endl;
70 [ + + ]: 40 : if (ev == d_true)
71 : : {
72 : : // For example, for lemma (=> (= x 0) (or (= (* x y) 0) (= z 0))), we have
73 : : // that (= (* x y) 0) evaluates to true under substitution {x->0}, hence
74 : : // only this literal needs to be included amongst the target literals,
75 : : // e.g. (= z 0) can be dropped.
76 : 8 : tgtLit = tlit;
77 : 8 : break;
78 : : }
79 [ + + ]: 32 : else if (ev == d_false)
80 : : {
81 [ + - ]: 8 : Trace("confp-debug") << "...filter implied " << tlit << std::endl;
82 : 8 : continue;
83 : : }
84 : : // If we evaluated the literal.
85 [ + - ]: 24 : if (!ev.isNull())
86 : : {
87 : 24 : itm = evMap.find(ev);
88 [ - + ]: 24 : if (itm != evMap.end())
89 : : {
90 : : // The literal evaluated to the same thing as something else.
91 : : // For example, for lemma (=> (= x 0) (or (= y x) (= y 0)))
92 : : // (= y x) and (= y 0) both evaluate to (= y 0), hence one of these
93 : : // literals can be droped.
94 [ - - ]: 0 : Trace("confp-debug") << "...filter duplicate " << tlit << std::endl;
95 : 0 : continue;
96 : : }
97 : : // look for negation
98 : 24 : Node evn = ev.negate();
99 : 24 : itm = evMap.find(evn);
100 [ - + ]: 24 : if (itm != evMap.end())
101 : : {
102 : 0 : tgtLitsNc.clear();
103 : : // The literal evaluated to the negation of something else.
104 : : // For example, for lemma
105 : : // (=> (= x 0) (or (not (= y x)) (= y 0) (= z 0)))
106 : : // (not (= y x)) and (= y 0) evaluate to the negation of one another,
107 : : // hence, only these two literals are required to be in the lemma and
108 : : // all others (e.g. (= z 0)) can be dropped.
109 [ - - ]: 0 : Trace("confp-debug") << "...contradiction " << itm->second << " and "
110 : 0 : << tlit << std::endl;
111 : 0 : tgtLitsNc.push_back(itm->second);
112 : 0 : tgtLitsNc.push_back(tlit);
113 : 0 : break;
114 : : }
115 : : }
116 : 24 : tgtLitsNc.push_back(tlit);
117 : 24 : evMap[ev] = tlit;
118 : : }
119 : 16 : bool minimized = false;
120 : 32 : std::vector<Node> auxExplain;
121 : : // If we did not find a target literal.
122 [ + + ]: 16 : if (tgtLit.isNull())
123 : : {
124 [ + - ]: 8 : Trace("confp-debug") << "No target for " << lemma << std::endl;
125 : : // If we filtered any literals (either by redundancy checking or by
126 : : // inferring a conflict).
127 [ + - ]: 8 : if (tgtLitsNc.size() < tgtLits.size())
128 : : {
129 : 8 : minimized = true;
130 [ + - ]: 16 : Trace("confp") << "...SUCCESS (filtered "
131 : 0 : << (tgtLits.size() - tgtLitsNc.size()) << "/"
132 : 8 : << tgtLits.size() << ")" << std::endl;
133 : : }
134 : : else
135 : : {
136 [ - - ]: 0 : Trace("confp") << "...FAIL (no target)" << std::endl;
137 : 0 : return TrustNode::null();
138 : : }
139 : : // just take the OR as target
140 : 8 : tgtLit = nodeManager()->mkOr(tgtLitsNc);
141 : : }
142 : : else
143 : : {
144 [ - + ]: 8 : if (tgtLits.size() > 1)
145 : : {
146 : : // we are minimized if there were multiple target literals and we found a
147 : : // single one that sufficed
148 : 0 : minimized = true;
149 [ - - ]: 0 : Trace("confp") << "...SUCCESS (target out of " << tgtLits.size() << ")"
150 : 0 : << std::endl;
151 [ - - ]: 0 : Trace("confp") << "Target suffices " << tgtLit
152 : 0 : << " for more than one disjunct" << std::endl;
153 : : }
154 : : // The substitution s only applies when we found a target literal, so we
155 : : // only minimize in the case where tgtLit is not null.
156 : 16 : std::unordered_map<Node, Node> smap = s.getSubstitutions();
157 [ - + ]: 8 : if (smap.size() > 1)
158 : : {
159 : 0 : std::vector<Node> toErase;
160 : : // For each substitution, see if we can drop it while maintaining the
161 : : // invariant that the target literal still evaluates to true.
162 : : // For example, the lemma (=> (and (= x 1) (= y 0)) (> x 0)) can be
163 : : // minimized to (=> (= x 1) (> x 0)) noting that (> x 0) simplifies to
164 : : // true under substitution { x -> 1, y -> 0 }, and moreover still simplifies
165 : : // to true under { x -> 1 }.
166 [ - - ]: 0 : for (std::pair<const Node, Node>& ss : smap)
167 : : {
168 : : // try eliminating the substitution
169 : 0 : Node v = ss.first;
170 : 0 : s.eraseSubstitution(v);
171 [ - - ]: 0 : Trace("confp") << "--- try substitution without " << v << std::endl;
172 : 0 : Node ev = evaluateSubstitution(s, tgtLit);
173 [ - - ]: 0 : if (ev==d_true)
174 : : {
175 : 0 : toErase.push_back(v);
176 : : }
177 : : else
178 : : {
179 [ - - ]: 0 : Trace("confp") << "...did not work on " << tgtLit << std::endl;
180 : : // add it back
181 : 0 : s.addSubstitution(v, ss.second);
182 : : }
183 : : }
184 [ - - ]: 0 : if (!toErase.empty())
185 : : {
186 [ - - ]: 0 : if (TraceIsOn("confp"))
187 : : {
188 [ - - ]: 0 : if (!minimized)
189 : : {
190 [ - - ]: 0 : Trace("confp") << "...SUCCESS (min subs " << toErase.size() << "/"
191 : 0 : << smap.size() << ")" << std::endl;
192 : : }
193 : : }
194 : : // If we erased any literals from the substitution, we have minimized
195 : : // the lemma.
196 : 0 : minimized = true;
197 [ - - ]: 0 : for (const Node& v : toErase)
198 : : {
199 : : // Erase the literal for the explanation of the substitution.
200 : 0 : varToExp.erase(v);
201 [ - - ]: 0 : Trace("confp") << "Substitution is unnecessary for " << v
202 : 0 : << std::endl;
203 : : }
204 : : }
205 : : }
206 : : }
207 : :
208 : : // If we minimized at all, we replace the the lemma with a stronger
209 : : // version.
210 [ + + ]: 16 : if (minimized)
211 : : {
212 : 8 : ++d_stats.d_minLemmas;
213 : 8 : NodeManager* nm = nodeManager();
214 : 16 : std::vector<Node> clause;
215 [ + + ]: 24 : for (std::pair<const Node, Node>& e : varToExp)
216 : : {
217 [ - + ]: 16 : if (e.second.getKind() == Kind::AND)
218 : : {
219 [ - - ]: 0 : for (const Node& ec : e.second)
220 : : {
221 : 0 : clause.push_back(ec.negate());
222 : : }
223 : : }
224 : : else
225 : : {
226 : 16 : clause.push_back(e.second.negate());
227 : : }
228 : : }
229 : 8 : clause.insert(clause.end(), auxExplain.begin(), auxExplain.end());
230 [ + - ]: 8 : if (tgtLit.getKind() == Kind::OR)
231 : : {
232 : 8 : clause.insert(clause.end(), tgtLit.begin(), tgtLit.end());
233 : : }
234 : : else
235 : : {
236 : 0 : clause.push_back(tgtLit);
237 : : }
238 : 8 : Node genLem = nm->mkOr(clause);
239 [ + - ]: 8 : Trace("confp") << "...processed lemma is " << genLem << std::endl;
240 : 8 : return TrustNode::mkTrustLemma(genLem);
241 : : }
242 : :
243 [ + - ]: 8 : Trace("confp") << "...FAIL (no minimize)" << std::endl;
244 : 8 : return TrustNode::null();
245 : : }
246 : :
247 : 154 : void ConflictProcessor::decomposeLemma(const Node& lem,
248 : : SubstitutionMap& s,
249 : : std::map<Node, Node>& varToExp,
250 : : std::vector<Node>& tgtLits) const
251 : : {
252 : : // visit is implicitly negated
253 : 308 : std::unordered_set<TNode> visited;
254 : 308 : std::vector<TNode> visit;
255 : 308 : std::unordered_set<Node> keep;
256 : 308 : TNode cur;
257 : : Kind k;
258 : 154 : visit.push_back(lem);
259 : 252 : do
260 : : {
261 : 406 : cur = visit.back();
262 : 406 : visit.pop_back();
263 [ + - ]: 406 : if (visited.find(cur) == visited.end())
264 : : {
265 : 406 : visited.insert(cur);
266 : 406 : k = cur.getKind();
267 [ + + ][ + + ]: 406 : if (k == Kind::OR || k == Kind::IMPLIES)
268 : : {
269 : : // all children are entailed
270 [ + + ]: 254 : for (size_t i = 0, nargs = cur.getNumChildren(); i < nargs; i++)
271 : : {
272 [ + + ][ + + ]: 172 : if (k == Kind::IMPLIES && i == 0)
273 : : {
274 : 8 : Node cc = cur[0].negate();
275 : 8 : keep.insert(cc);
276 : 8 : visit.push_back(cc);
277 : : }
278 : : else
279 : : {
280 : 164 : visit.push_back(cur[i]);
281 : : }
282 : : }
283 : 82 : continue;
284 : : }
285 [ + + ]: 324 : else if (k == Kind::NOT)
286 : : {
287 : 162 : k = cur[0].getKind();
288 [ + + ]: 162 : if (k == Kind::EQUAL)
289 : : {
290 : : // maybe substitution?
291 : 80 : Node vtmp;
292 : 80 : Node ctmp;
293 [ + + ]: 80 : if (isAssignEq(s, cur[0], vtmp, ctmp))
294 : : {
295 [ - + ][ - + ]: 24 : Assert(!s.hasSubstitution(vtmp));
[ - - ]
296 : : // use as a substitution
297 : 24 : s.addSubstitution(vtmp, ctmp);
298 : 24 : varToExp[vtmp] = cur[0];
299 : 24 : continue;
300 : : }
301 : : }
302 [ + + ]: 82 : else if (k == Kind::AND)
303 : : {
304 : : // negations of children of AND are entailed
305 [ + + ]: 104 : for (const Node& c : cur[0])
306 : : {
307 : 80 : Node cn = c.negate();
308 : 80 : keep.insert(cn);
309 : 80 : visit.push_back(cn);
310 : : }
311 : 24 : continue;
312 : : }
313 : : }
314 : : // otherwise, take this as a target literal
315 : 276 : tgtLits.push_back(cur);
316 : : }
317 [ + + ]: 406 : } while (!visit.empty());
318 : 154 : }
319 : :
320 : 40 : Node ConflictProcessor::evaluateSubstitutionLit(const SubstitutionMap& s,
321 : : const Node& tgtLit) const
322 : : {
323 [ + - ]: 40 : Trace("confp-subs-debug") << "...try " << tgtLit << std::endl;
324 : 40 : Node ev = s.apply(tgtLit);
325 [ + - ]: 40 : Trace("confp-subs-debug") << "...apply " << ev << std::endl;
326 : : // use the extended rewriter if option is set
327 [ - + ]: 40 : if (d_useExtRewriter)
328 : : {
329 : 0 : ev = extendedRewrite(ev);
330 : : }
331 : : else
332 : : {
333 : 40 : ev = rewrite(ev);
334 : : // also try the extended equality rewriter
335 [ + + ]: 40 : if (ev.getKind() == Kind::EQUAL)
336 : : {
337 : 8 : ev = rewriteEqualityExt(ev);
338 : : }
339 : : }
340 [ + - ]: 40 : Trace("confp-subs-debug") << "...rewrite " << ev << std::endl;
341 : 40 : return ev;
342 : : }
343 : :
344 : 40 : Node ConflictProcessor::evaluateSubstitution(const SubstitutionMap& s,
345 : : const Node& tgt) const
346 : : {
347 : 40 : bool polarity = true;
348 : 80 : Node tgtAtom = tgt;
349 [ + + ]: 40 : if (tgtAtom.getKind() == Kind::NOT)
350 : : {
351 : 32 : tgtAtom = tgtAtom[0];
352 : 32 : polarity = !polarity;
353 : : }
354 : : // Optimize for OR and AND.
355 : 40 : Kind k = tgtAtom.getKind();
356 [ + - ][ - + ]: 40 : if (k == Kind::OR || k == Kind::AND)
357 : : {
358 : 0 : bool hasNonConst = false;
359 [ - - ]: 0 : for (const Node& n : tgtAtom)
360 : : {
361 : 0 : Node sn = evaluateSubstitutionLit(s, n);
362 [ - - ]: 0 : if (!sn.isConst())
363 : : {
364 : : // failure if all children must be a given value
365 [ - - ]: 0 : if (polarity == (k == Kind::AND))
366 : : {
367 : : // we don't bother computing the rest
368 : 0 : return Node::null();
369 : : }
370 : 0 : hasNonConst = true;
371 : : }
372 [ - - ]: 0 : else if (sn.getConst<bool>() == (k == Kind::OR))
373 : : {
374 : : // short circuits to value
375 [ - - ][ - - ]: 0 : return polarity ? sn : (k == Kind::OR ? d_false : d_true);
376 : : }
377 : : }
378 : : // if non-constant, we don't bother computing
379 : 0 : return hasNonConst ? Node::null() : (k == Kind::OR ? d_true : d_false);
380 : : }
381 : : // otherwise, rewrite
382 : 80 : Node ret = evaluateSubstitutionLit(s, tgtAtom);
383 [ + + ]: 40 : if (!polarity)
384 : : {
385 : 48 : return ret.isConst() ? (ret.getConst<bool>() ? d_false : d_true)
386 [ + + ][ + + ]: 48 : : ret.negate();
387 : : }
388 : 8 : return ret;
389 : : }
390 : :
391 : 8 : ConflictProcessor::Statistics::Statistics(StatisticsRegistry& sr)
392 : 8 : : d_initLemmas(sr.registerInt("ConflictProcessor::init_lemmas")),
393 : 8 : d_lemmas(sr.registerInt("ConflictProcessor::lemmas")),
394 : 8 : d_minLemmas(sr.registerInt("ConflictProcessor::min_lemmas"))
395 : : {
396 : 8 : }
397 : :
398 : 80 : bool ConflictProcessor::isAssignEq(const SubstitutionMap& s,
399 : : const Node& n,
400 : : Node& v,
401 : : Node& c) const
402 : : {
403 [ - + ][ - + ]: 80 : Assert(n.getKind() == Kind::EQUAL);
[ - - ]
404 [ + + ]: 208 : for (size_t i = 0; i < 2; i++)
405 : : {
406 : 152 : if (!n[i].isVar() || s.hasSubstitution(n[i]))
407 : : {
408 : 128 : continue;
409 : : }
410 : : // otherwise check cyclic
411 : 48 : Node ns = s.apply(n[1 - i]);
412 [ - + ]: 24 : if (expr::hasSubterm(ns, n[i]))
413 : : {
414 : 0 : continue;
415 : : }
416 : 24 : v = n[i];
417 : 24 : c = n[1 - i];
418 : 24 : return true;
419 : : }
420 : 56 : return false;
421 : : }
422 : :
423 : : } // namespace theory
424 : : } // namespace cvc5::internal
|
