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