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 : : * The distinct extension of TheoryUF.
11 : : */
12 : :
13 : : #include "theory/uf/distinct_extension.h"
14 : :
15 : : #include "options/smt_options.h"
16 : : #include "proof/proof.h"
17 : : #include "proof/proof_generator.h"
18 : : #include "proof/proof_node_algorithm.h"
19 : : #include "proof/proof_node_manager.h"
20 : : #include "theory/uf/theory_uf_rewriter.h"
21 : :
22 : : namespace cvc5::internal {
23 : : namespace theory {
24 : : namespace uf {
25 : :
26 : : /**
27 : : * A proof generator for lemmas added by the distinct extension
28 : : */
29 : : class DistinctProofGenerator : protected EnvObj, public ProofGenerator
30 : : {
31 : : public:
32 : 8696 : DistinctProofGenerator(Env& env) : EnvObj(env) {}
33 : 17392 : virtual ~DistinctProofGenerator() {}
34 : : /**
35 : : * Proves false from an element equality and a distinct constraint, as
36 : : * described below. This is used both for giving proofs of lemmas and
37 : : * conflicts.
38 : : */
39 : 2416 : std::shared_ptr<ProofNode> getConflictProof(Node eeq, Node distinct)
40 : : {
41 : 4832 : CDProof cdp(d_env);
42 : 2416 : std::vector<Node> cpremises;
43 [ + + ]: 82920 : for (const Node& e : distinct)
44 : : {
45 [ + + ]: 80504 : if (e == eeq[0])
46 : : {
47 : 2416 : cpremises.push_back(eeq);
48 : : }
49 : : else
50 : : {
51 : : // otherwise will be refl
52 : 78088 : cpremises.push_back(Node::null());
53 : : }
54 : 80504 : }
55 : : // ------ -----
56 : : // a = c b = b c = c
57 : : // ------------------------- cong -------------------
58 : : // dist(a,b,c) = dist(c,b,c) dist(c,b,c) = false
59 : : // ----------------------------------------------------
60 : : // dist(a,b,c) dist(a,b,c) = false
61 : : // --------------------------------
62 : : // false
63 : : // --------------------- scope {a=c,dist(a,b,c)}
64 : : // ~(a=c ^ dist(a,b,c))
65 : 2416 : Node ceq = expr::proveCong(d_env, &cdp, distinct, cpremises);
66 : 2416 : Assert(ceq.getKind() == Kind::EQUAL && ceq[0] != ceq[1]);
67 [ + - ]: 2416 : Trace("distinct-pf") << "...prove by congruence " << ceq << std::endl;
68 : : // dist(c,b,c) = false
69 : 2416 : Node falsen = nodeManager()->mkConst(false);
70 : 2416 : Node eq = ceq[1].eqNode(falsen);
71 : 2416 : cdp.addTheoryRewriteStep(eq, ProofRewriteRule::DISTINCT_FALSE);
72 : : // dist(a,b,c) = false
73 : 2416 : Node eq2 = ceq[0].eqNode(falsen);
74 [ + + ][ - - ]: 7248 : cdp.addStep(eq2, ProofRule::TRANS, {ceq, eq}, {});
75 : : // false
76 [ + + ][ - - ]: 7248 : cdp.addStep(falsen, ProofRule::EQ_RESOLVE, {distinct, eq2}, {});
77 : 4832 : return cdp.getProofFor(falsen);
78 : 2416 : }
79 : : /**
80 : : * Get proof for, which expects lemmas of the form
81 : : * (not (and (= x y) (distinct ... x ... y ...))), or
82 : : * (=> B (distinct ....)) where B is the result of expanding distinct.
83 : : */
84 : 20 : std::shared_ptr<ProofNode> getProofFor(Node fact) override
85 : : {
86 [ + - ]: 20 : Trace("distinct-pf") << "Get proof for: " << fact << std::endl;
87 [ + - ][ + + ]: 36 : if (fact.getKind() == Kind::NOT && fact[0].getKind() == Kind::AND
[ - - ]
88 : 36 : && fact[0].getNumChildren() == 2 && fact[0][0].getKind() == Kind::EQUAL
89 : 36 : && fact[0][1].getKind() == Kind::DISTINCT)
90 : : {
91 : 16 : Node eq = fact[0][0];
92 : 16 : Node distinct = fact[0][1];
93 : 32 : std::shared_ptr<ProofNode> pfn = getConflictProof(eq, distinct);
94 : 64 : std::vector<Node> assumps{eq, distinct};
95 : 16 : return d_env.getProofNodeManager()->mkScope(pfn, assumps);
96 : 16 : }
97 : 12 : else if (fact.getKind() == Kind::IMPLIES
98 [ + - ][ + - ]: 4 : && fact[1].getKind() == Kind::DISTINCT)
[ + - ][ + - ]
[ - - ]
99 : : {
100 : 4 : Node atom = fact[1];
101 : 4 : Node batom = TheoryUfRewriter::blastDistinct(nodeManager(), atom);
102 [ + - ]: 4 : if (batom == fact[0])
103 : : {
104 : 8 : CDProof cdp(d_env);
105 : 4 : Node eq = atom.eqNode(batom);
106 : 4 : cdp.addTheoryRewriteStep(eq, ProofRewriteRule::DISTINCT_ELIM);
107 : 8 : Node eqs = eq[1].eqNode(eq[0]);
108 : : // eqs proven via eq based on auto-symm handling in CDProof
109 [ + + ][ - - ]: 12 : cdp.addStep(atom, ProofRule::EQ_RESOLVE, {batom, eqs}, {});
110 : : // ----------------
111 : : // B B = dist(a,b,c)
112 : : // ------------------
113 : : // dist(a,b,c)
114 : : // ---------------- scope {B}
115 : : // B => dist(a,b,c)
116 : : // where B is the result of eliminating distinct.
117 : 4 : std::shared_ptr<ProofNode> pfn = cdp.getProofFor(fact[1]);
118 : 12 : std::vector<Node> assumps{fact[0]};
119 : 4 : return d_env.getProofNodeManager()->mkScope(pfn, assumps);
120 : 4 : }
121 [ - + ][ - + ]: 8 : }
122 : 0 : CDProof cdp(d_env);
123 : 0 : cdp.addTrustedStep(fact, TrustId::UF_DISTINCT, {}, {});
124 : 0 : return cdp.getProofFor(fact);
125 : 0 : }
126 : : /** identify */
127 : 0 : std::string identify() const override { return "DistinctProofGenerator"; }
128 : : };
129 : :
130 : 28708 : DistinctExtension::DistinctExtension(Env& env,
131 : : TheoryState& state,
132 : 28708 : TheoryInferenceManager& im)
133 : : : EnvObj(env),
134 : 28708 : d_state(state),
135 : 28708 : d_im(im),
136 : 28708 : d_ndistinct(context()),
137 : 28708 : d_negDistinct(context()),
138 : 28708 : d_negDistinctIndex(context(), 0),
139 : 28708 : d_posDistinct(context()),
140 [ + + ]: 37404 : d_dproof(d_env.isTheoryProofProducing()
141 : 8696 : ? new DistinctProofGenerator(d_env)
142 : : : nullptr),
143 : 46100 : d_epg(d_env.isTheoryProofProducing()
144 : 17392 : ? new EagerProofGenerator(d_env, context(), "DistinctEpg")
145 : : : nullptr),
146 : 86124 : d_pendingConflict(context())
147 : : {
148 : 28708 : d_false = nodeManager()->mkConst(false);
149 : 28708 : }
150 : :
151 : 34999 : bool DistinctExtension::needsCheckLastEffort()
152 : : {
153 : 34999 : return d_negDistinctIndex.get() < d_negDistinct.size()
154 [ + + ][ + + ]: 34999 : || !d_posDistinct.empty();
155 : : }
156 : :
157 : 17084 : void DistinctExtension::assertDistinct(TNode atom, bool pol, TNode fact)
158 : : {
159 : : // since we do not do congruence over distinct, we need to add all
160 : : // children of distinct as terms to the equality engine. This ensures that
161 : : // the model will assign values to them, which may be used during the check
162 : : // method of this class.
163 [ + + ]: 165208 : for (const Node& nc : atom)
164 : : {
165 : 148124 : d_state.addTerm(nc);
166 : 148124 : }
167 [ + + ]: 17084 : if (pol)
168 : : {
169 : 583 : d_posDistinct.push_back(fact);
170 : 583 : std::unordered_map<Node, Node> reps;
171 : 583 : std::unordered_map<Node, Node>::iterator itr;
172 : 583 : bool isConflict = false;
173 : : // see if we are in conflict, which is the case if for
174 : : // distinct(t1...tn) it is already the case that ti=tj for some i,j.
175 [ + + ]: 11401 : for (const Node& nc : atom)
176 : : {
177 : 21636 : Node ncr = d_state.getRepresentative(nc);
178 : 10818 : itr = reps.find(ncr);
179 [ + - ]: 10818 : if (itr == reps.end())
180 : : {
181 : 10818 : reps[ncr] = nc;
182 : 10818 : continue;
183 : : }
184 : 0 : isConflict = true;
185 : : // otherwise already a conflict
186 : 0 : Node eq = itr->second.eqNode(nc);
187 [ - - ]: 0 : if (d_env.isTheoryProofProducing())
188 : : {
189 : 0 : std::shared_ptr<ProofNode> pfn = d_dproof->getConflictProof(eq, fact);
190 : 0 : d_epg->setProofFor(d_false, pfn);
191 : 0 : }
192 : 0 : d_im.conflictExp(InferenceId::UF_DISTINCT_DEQ, {eq, fact}, d_epg.get());
193 : 0 : break;
194 [ + - ][ + - ]: 21636 : }
195 [ + - ]: 583 : if (!isConflict)
196 : : {
197 [ + + ]: 11401 : for (const std::pair<const Node, Node>& p : reps)
198 : : {
199 [ + - ]: 21636 : Trace("uf-lazy-distinct")
200 : 10818 : << "Watch " << p.first << " distinct (" << fact << ")" << std::endl;
201 : 10818 : size_t ndprev = d_ndistinct[p.first];
202 : 10818 : d_ndistinct[p.first] = ndprev + 1;
203 : : // Ensure the non-context dependent list has the right size in
204 : : // case we backtracked. This is tracked via d_ndistinct.
205 : 10818 : std::vector<Node>& ndlist = d_eqcToDistinct[p.first];
206 : 10818 : ndlist.resize(ndprev);
207 : 10818 : ndlist.emplace_back(fact);
208 : : // also carry the member
209 : 10818 : std::vector<Node>& ndmem = d_eqcToDMem[p.first];
210 : 10818 : ndmem.resize(ndprev);
211 : 10818 : ndmem.emplace_back(p.second);
212 : : }
213 : : }
214 : 583 : }
215 : : else
216 : : {
217 : : // otherwise track that the negated distinct term
218 : 16501 : d_negDistinct.push_back(fact);
219 : : }
220 : 17084 : }
221 : :
222 : 9806833 : void DistinctExtension::eqNotifyMerge(TNode t1, TNode t2)
223 : : {
224 : : // Must ensure we track distinct constraints, moving those from t2 into t1.
225 : : // If the same distinct constraint is in both, we are in conflict.
226 : 9806833 : NodeUIntMap::iterator it2 = d_ndistinct.find(t2);
227 [ + + ]: 9806833 : if (it2 != d_ndistinct.end())
228 : : {
229 [ + - ]: 6915 : Trace("uf-lazy-distinct") << "merge " << t1 << " and " << t2 << std::endl;
230 : 6915 : NodeUIntMap::iterator it1 = d_ndistinct.find(t1);
231 : 6915 : std::vector<Node>& d1 = d_eqcToDistinct[t1];
232 : 6915 : std::vector<Node>& d1m = d_eqcToDMem[t1];
233 : 6915 : std::vector<Node>& d2 = d_eqcToDistinct[t2];
234 : : // the iterator up to which d2 is valid
235 : 6915 : std::vector<Node>::iterator d2e = d2.begin() + it2->second;
236 [ + + ]: 6915 : if (it1 != d_ndistinct.end())
237 : : {
238 : : // ensure the list of distinct constraints in t1 is resized now
239 : 4505 : d1.resize(it1->second);
240 : 4505 : d1m.resize(it1->second);
241 [ + - ]: 9010 : Trace("uf-lazy-distinct")
242 : 0 : << "...looking for conflicts in intersection of # terms = "
243 : 4505 : << it1->second << " and " << it2->second << std::endl;
244 : : // check for conflicts, in particular if any distinct constraint
245 : : // associated with the first equivalence class is also associated with
246 : : // the second equivalence class.
247 [ + - ]: 4505 : for (size_t i = 0; i < it1->second; i++)
248 : : {
249 : 4505 : Node d = d1[i];
250 [ - + ][ - + ]: 4505 : Assert(d.getKind() == Kind::DISTINCT);
[ - - ]
251 [ + - ]: 4505 : Trace("uf-lazy-distinct") << "...check " << d << std::endl;
252 : 4505 : std::vector<Node>::iterator itd1 = std::find(d2.begin(), d2e, d);
253 [ + - ]: 4505 : if (itd1 != d2e)
254 : : {
255 : : // conflict
256 : 4505 : size_t i2 = std::distance(d2.begin(), itd1);
257 [ - + ][ - + ]: 4505 : Assert(i < d_eqcToDMem[t1].size());
[ - - ]
258 [ - + ][ - + ]: 4505 : Assert(i2 < d_eqcToDMem[t2].size());
[ - - ]
259 : 9010 : Node eq = d_eqcToDMem[t1][i].eqNode(d_eqcToDMem[t2][i2]);
260 [ - + ][ - + ]: 4505 : Assert(d_state.areEqual(d_eqcToDMem[t1][i], d_eqcToDMem[t2][i2]));
[ - - ]
261 [ + - ]: 9010 : Trace("uf-lazy-distinct")
262 : 4505 : << "...conflict " << eq << " " << d << std::endl;
263 : 18020 : std::vector<Node> exp{eq, d};
264 : 4505 : d_pendingConflict = nodeManager()->mkAnd(exp);
265 : 4505 : return;
266 : 4505 : }
267 [ - - ]: 0 : Trace("uf-lazy-distinct") << "...no conflict" << std::endl;
268 [ - + ]: 4505 : }
269 : : }
270 : : else
271 : : {
272 : 2410 : d1.clear();
273 : 2410 : d1m.clear();
274 : : }
275 : : // append lists
276 : 2410 : d1.insert(d1.end(), d2.begin(), d2e);
277 : 2410 : std::vector<Node>& d2m = d_eqcToDMem[t2];
278 : 2410 : d1m.insert(d1m.end(), d2m.begin(), d2m.begin() + it2->second);
279 : : }
280 : : }
281 : :
282 : 2455831 : void DistinctExtension::check(Theory::Effort level)
283 : : {
284 [ + + ]: 2455831 : if (!d_pendingConflict.get().isNull())
285 : : {
286 : 4226 : Node conf = d_pendingConflict.get();
287 : 4226 : std::vector<Node> exp(conf.begin(), conf.end());
288 [ + + ]: 4226 : if (d_env.isTheoryProofProducing())
289 : : {
290 [ - + ][ - + ]: 2400 : Assert(exp.size() == 2);
[ - - ]
291 : : std::shared_ptr<ProofNode> pfn =
292 : 4800 : d_dproof->getConflictProof(exp[0], exp[1]);
293 : 2400 : d_epg->setProofFor(d_false, pfn);
294 : 2400 : }
295 [ + + ]: 4226 : d_im.conflictExp(InferenceId::UF_DISTINCT_DEQ, exp, d_epg.get());
296 : 4226 : return;
297 : 4226 : }
298 [ + + ]: 2451605 : if (level != Theory::Effort::EFFORT_LAST_CALL)
299 : : {
300 : 2447576 : return;
301 : : }
302 : 4029 : TheoryModel* tm = d_state.getModel();
303 : 4029 : bool addedLemma = false;
304 : : // Check negated distinct. We first check if the negated distinct constraint
305 : : // is satisfied in this SAT context, which is the case if for
306 : : // distinct(t1...tn), we have that the equality engine has ti=tj for some
307 : : // i != j. If not, we reduce the negated distinct based on the method
308 : : // TheoryUfRewriter::blastDistinct.
309 : 4029 : size_t nnd = d_negDistinct.size();
310 [ + + ]: 4100 : for (size_t i = d_negDistinctIndex.get(); i < nnd; i++)
311 : : {
312 : 71 : Node ndistinct = d_negDistinct[i];
313 : 71 : Assert(ndistinct.getKind() == Kind::NOT
314 : : && ndistinct[0].getKind() == Kind::DISTINCT);
315 : : // check if satisfied
316 : 71 : Node atom = ndistinct[0];
317 : 71 : std::unordered_set<Node> reps;
318 : 71 : bool isSat = false;
319 [ + + ]: 371 : for (size_t j = 0, nterms = atom.getNumChildren(); j < nterms; j++)
320 : : {
321 : 720 : Node ncr = d_state.getRepresentative(atom[j]);
322 [ + + ]: 360 : if (!reps.insert(ncr).second)
323 : : {
324 : 60 : isSat = true;
325 : 60 : break;
326 : : }
327 [ + + ]: 360 : }
328 [ + + ]: 71 : if (!isSat)
329 : : {
330 : 11 : Node batom = TheoryUfRewriter::blastDistinct(nodeManager(), atom);
331 : 22 : Node lem = nodeManager()->mkNode(Kind::IMPLIES, batom, atom);
332 [ + + ]: 11 : TrustNode tlem = TrustNode::mkTrustLemma(lem, d_dproof.get());
333 [ + - ]: 11 : if (d_im.trustedLemma(tlem, InferenceId::UF_NOT_DISTINCT_ELIM))
334 : : {
335 : 11 : addedLemma = true;
336 : : }
337 : 11 : }
338 : : // otherwise we determined that we are SAT in the remainder of this
339 : : // SAT context (due to looking up representatives, instead of model values)
340 : : // meaning that we don't need to check this constraint again in this
341 : : // SAT context.
342 : 71 : }
343 : 4029 : d_negDistinctIndex = nnd;
344 [ + + ]: 4029 : if (addedLemma)
345 : : {
346 : 11 : return;
347 : : }
348 : : // Note that it still may the case that we have a (distinct t1 ... tn)
349 : : // constraint where ti and tj were assigned the same value in the model,
350 : : // but the UF theory was not informed of ti = tj. This is because we
351 : : // do not insist that distinct induces care pairs in theory combination.
352 : : // Thus we must double check that all values are distinct in the model.
353 : : // If not, then we add the lemma (~distinct(t1,...,tn) or ti != tj) for
354 : : // each pair of terms that have equal values.
355 [ + + ]: 4808 : for (const Node& atom : d_posDistinct)
356 : : {
357 [ - + ][ - + ]: 790 : Assert(atom.getKind() == Kind::DISTINCT);
[ - - ]
358 : : // ensure the positive distinct are satisfied in model
359 : 790 : std::unordered_map<Node, Node> vals;
360 : 790 : std::unordered_map<Node, Node>::iterator itr;
361 [ + + ]: 14324 : for (const Node& nc : atom)
362 : : {
363 : 13534 : Node ncr = tm->getValue(nc);
364 : 13534 : itr = vals.find(ncr);
365 [ + + ]: 13534 : if (itr == vals.end())
366 : : {
367 : 12803 : vals[ncr] = nc;
368 : 12803 : continue;
369 : : }
370 : 731 : Node eq = itr->second.eqNode(nc);
371 : 2924 : Node lem = nodeManager()->mkNode(Kind::AND, {eq, atom}).notNode();
372 [ + + ]: 731 : TrustNode tlem = TrustNode::mkTrustLemma(lem, d_dproof.get());
373 : 731 : d_im.trustedLemma(tlem, InferenceId::UF_DISTINCT_DEQ_MODEL);
374 [ + + ][ + + ]: 26337 : }
375 : 790 : }
376 : : }
377 : :
378 : : } // namespace uf
379 : : } // namespace theory
380 : : } // namespace cvc5::internal
|
