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 : : * Extended theory interface.
11 : : *
12 : : * This implements a generic module, used by theory solvers, for performing
13 : : * "context-dependent simplification", as described in Reynolds et al
14 : : * "Designing Theory Solvers with Extensions", FroCoS 2017.
15 : : */
16 : :
17 : : #include "theory/ext_theory.h"
18 : :
19 : : #include "base/check.h"
20 : : #include "proof/proof_checker.h"
21 : : #include "proof/proof_node_manager.h"
22 : : #include "theory/output_channel.h"
23 : : #include "theory/quantifiers_engine.h"
24 : : #include "theory/rewriter.h"
25 : : #include "theory/substitutions.h"
26 : :
27 : : using namespace std;
28 : :
29 : : namespace cvc5::internal {
30 : : namespace theory {
31 : :
32 : 15 : const char* toString(ExtReducedId id)
33 : : {
34 [ + + ][ + + ]: 15 : switch (id)
[ + + ][ + + ]
[ + + ][ + + ]
[ + + ][ + - ]
[ - ]
35 : : {
36 : 1 : case ExtReducedId::NONE: return "NONE";
37 : 1 : case ExtReducedId::SR_CONST: return "SR_CONST";
38 : 1 : case ExtReducedId::REDUCTION: return "REDUCTION";
39 : 1 : case ExtReducedId::ARITH_SR_ZERO: return "ARITH_SR_ZERO";
40 : 1 : case ExtReducedId::ARITH_SR_LINEAR: return "ARITH_SR_LINEAR";
41 : 1 : case ExtReducedId::STRINGS_SR_CONST: return "STRINGS_SR_CONST";
42 : 1 : case ExtReducedId::STRINGS_NEG_CTN_DEQ: return "STRINGS_NEG_CTN_DEQ";
43 : 1 : case ExtReducedId::STRINGS_CTN_DECOMPOSE: return "STRINGS_CTN_DECOMPOSE";
44 : 1 : case ExtReducedId::STRINGS_REGEXP_INTER: return "STRINGS_REGEXP_INTER";
45 : 1 : case ExtReducedId::STRINGS_REGEXP_INTER_SUBSUME:
46 : 1 : return "STRINGS_REGEXP_INTER_SUBSUME";
47 : 1 : case ExtReducedId::STRINGS_REGEXP_INCLUDE: return "STRINGS_REGEXP_INCLUDE";
48 : 1 : case ExtReducedId::STRINGS_REGEXP_INCLUDE_NEG:
49 : 1 : return "STRINGS_REGEXP_INCLUDE_NEG";
50 : 1 : case ExtReducedId::STRINGS_REGEXP_RE_SYM_NF:
51 : 1 : return "STRINGS_REGEXP_RE_SYM_NF";
52 : 1 : case ExtReducedId::STRINGS_REGEXP_PDERIVATIVE:
53 : 1 : return "STRINGS_REGEXP_PDERIVATIVE";
54 : 1 : case ExtReducedId::STRINGS_NTH_REV: return "STRINGS_NTH_REV";
55 : 0 : case ExtReducedId::UNKNOWN: return "?";
56 : 0 : default: Unreachable(); return "?ExtReducedId?";
57 : : }
58 : : }
59 : :
60 : 15 : std::ostream& operator<<(std::ostream& out, ExtReducedId id)
61 : : {
62 : 15 : out << toString(id);
63 : 15 : return out;
64 : : }
65 : :
66 : 0 : bool ExtTheoryCallback::getCurrentSubstitution(
67 : : CVC5_UNUSED int effort,
68 : : CVC5_UNUSED const std::vector<Node>& vars,
69 : : CVC5_UNUSED std::vector<Node>& subs,
70 : : CVC5_UNUSED std::map<Node, std::vector<Node> >& exp)
71 : : {
72 : 0 : return false;
73 : : }
74 : 0 : bool ExtTheoryCallback::isExtfReduced(CVC5_UNUSED int effort,
75 : : Node n,
76 : : CVC5_UNUSED Node on,
77 : : CVC5_UNUSED std::vector<Node>& exp,
78 : : ExtReducedId& id)
79 : : {
80 : 0 : id = ExtReducedId::SR_CONST;
81 : 0 : return n.isConst();
82 : : }
83 : 0 : bool ExtTheoryCallback::getReduction(CVC5_UNUSED int effort,
84 : : CVC5_UNUSED Node n,
85 : : CVC5_UNUSED Node& nr,
86 : : CVC5_UNUSED bool& isSatDep)
87 : : {
88 : 0 : return false;
89 : : }
90 : :
91 : 43629 : ExtTheory::ExtTheory(Env& env, ExtTheoryCallback& p, TheoryInferenceManager& im)
92 : : : EnvObj(env),
93 : 43629 : d_parent(p),
94 : 43629 : d_im(im),
95 : 43629 : d_ext_func_terms(context()),
96 : 43629 : d_extfExtReducedIdMap(context()),
97 : 43629 : d_ci_inactive(userContext()),
98 : 43629 : d_has_extf(context()),
99 : 87258 : d_lemmas(userContext())
100 : : {
101 : 43629 : d_true = nodeManager()->mkConst(true);
102 : 43629 : }
103 : :
104 : : // Gets all leaf terms in n.
105 : 39709 : std::vector<Node> ExtTheory::collectVars(Node n)
106 : : {
107 : 39709 : std::vector<Node> vars;
108 : 39709 : std::set<Node> visited;
109 : 39709 : std::vector<Node> worklist;
110 : 39709 : worklist.push_back(n);
111 [ + + ]: 261006 : while (!worklist.empty())
112 : : {
113 : 221297 : Node current = worklist.back();
114 : 221297 : worklist.pop_back();
115 [ + + ][ + + ]: 221297 : if (current.isConst() || visited.count(current) > 0)
[ + + ]
116 : : {
117 : 69583 : continue;
118 : : }
119 : 151714 : visited.insert(current);
120 : : // Treat terms not belonging to this theory as leaf
121 : : // note : chould include terms not belonging to this theory
122 : : // (commented below)
123 [ + + ]: 151714 : if (current.getNumChildren() > 0)
124 : : {
125 : 88663 : worklist.insert(worklist.end(), current.begin(), current.end());
126 : : }
127 : : else
128 : : {
129 : 63051 : vars.push_back(current);
130 : : }
131 [ + + ]: 221297 : }
132 : 79418 : return vars;
133 : 39709 : }
134 : :
135 : : // do inferences
136 : 70485 : void ExtTheory::getSubstitutedTerms(int effort,
137 : : const std::vector<Node>& terms,
138 : : std::vector<Node>& sterms,
139 : : std::vector<std::vector<Node> >& exp)
140 : : {
141 [ + - ]: 140970 : Trace("extt-debug") << "getSubstitutedTerms for " << terms.size() << " / "
142 : 70485 : << d_ext_func_terms.size() << " extended functions."
143 : 70485 : << std::endl;
144 [ + + ]: 70485 : if (!terms.empty())
145 : : {
146 : : // all variables we need to find a substitution for
147 : 13249 : std::vector<Node> vars;
148 : 13249 : std::vector<Node> sub;
149 : 13249 : std::map<Node, std::vector<Node> > expc;
150 [ + + ]: 85159 : for (const Node& n : terms)
151 : : {
152 : : // do substitution, rewrite
153 : 71910 : std::map<Node, ExtfInfo>::iterator iti = d_extf_info.find(n);
154 [ - + ][ - + ]: 71910 : Assert(iti != d_extf_info.end());
[ - - ]
155 [ + + ]: 198965 : for (const Node& v : iti->second.d_vars)
156 : : {
157 [ + + ]: 127055 : if (std::find(vars.begin(), vars.end(), v) == vars.end())
158 : : {
159 : 55997 : vars.push_back(v);
160 : : }
161 : : }
162 : : }
163 : 13249 : bool useSubs = d_parent.getCurrentSubstitution(effort, vars, sub, expc);
164 : : // get the current substitution for all variables
165 [ + + ][ + - ]: 13249 : Assert(!useSubs || vars.size() == sub.size());
[ - + ][ - + ]
[ - - ]
166 [ + + ]: 85159 : for (const Node& n : terms)
167 : : {
168 : 71910 : Node ns = n;
169 : 71910 : std::vector<Node> expn;
170 [ + + ]: 71910 : if (useSubs)
171 : : {
172 : : // do substitution
173 : 38399 : ns = n.substitute(vars.begin(), vars.end(), sub.begin(), sub.end());
174 [ + + ]: 38399 : if (ns != n)
175 : : {
176 : : // build explanation: explanation vars = sub for each vars in FV(n)
177 : 17024 : std::map<Node, ExtfInfo>::iterator iti = d_extf_info.find(n);
178 [ - + ][ - + ]: 17024 : Assert(iti != d_extf_info.end());
[ - - ]
179 [ + + ]: 50469 : for (const Node& v : iti->second.d_vars)
180 : : {
181 : 33445 : std::map<Node, std::vector<Node> >::iterator itx = expc.find(v);
182 [ + + ]: 33445 : if (itx != expc.end())
183 : : {
184 [ + + ]: 39954 : for (const Node& e : itx->second)
185 : : {
186 [ + - ]: 19977 : if (std::find(expn.begin(), expn.end(), e) == expn.end())
187 : : {
188 : 19977 : expn.push_back(e);
189 : : }
190 : : }
191 : : }
192 : : }
193 : : }
194 [ + - ]: 76798 : Trace("extt-debug") << " have " << n << " == " << ns
195 : 38399 : << ", exp size=" << expn.size() << "." << std::endl;
196 : : }
197 : : // add to vector
198 : 71910 : sterms.push_back(ns);
199 : 71910 : exp.push_back(expn);
200 : 71910 : }
201 : 13249 : }
202 : 70485 : }
203 : :
204 : 70485 : bool ExtTheory::doInferencesInternal(int effort,
205 : : const std::vector<Node>& terms,
206 : : std::vector<Node>& nred)
207 : : {
208 : 70485 : bool addedLemma = false;
209 : 70485 : std::vector<Node> sterms;
210 : 70485 : std::vector<std::vector<Node> > exp;
211 : 70485 : getSubstitutedTerms(effort, terms, sterms, exp);
212 : 70485 : NodeManager* nm = nodeManager();
213 [ + + ]: 142395 : for (unsigned i = 0, size = terms.size(); i < size; i++)
214 : : {
215 : 71910 : bool processed = false;
216 : : // if the substitution applied to terms[i] changed it
217 [ + + ]: 71910 : if (sterms[i] != terms[i])
218 : : {
219 : 17024 : Node sr = rewrite(sterms[i]);
220 : : // ask the theory if this term is reduced, e.g. is it constant or it
221 : : // is a non-extf term.
222 : : ExtReducedId id;
223 [ + + ]: 17024 : if (d_parent.isExtfReduced(effort, sr, terms[i], exp[i], id))
224 : : {
225 : 12691 : processed = true;
226 : 12691 : markInactive(terms[i], id);
227 : : // We have exp[i] => terms[i] = sr
228 : 12691 : Node eq = terms[i].eqNode(sr);
229 : 12691 : Node lem = eq;
230 [ + - ]: 12691 : if (!exp[i].empty())
231 : : {
232 : 12691 : Node antec = nm->mkAnd(exp[i]);
233 : 12691 : lem = nm->mkNode(Kind::IMPLIES, antec, eq);
234 : 12691 : }
235 : : // will be able to generate a proof for this
236 : 12691 : TrustNode trn = TrustNode::mkTrustLemma(lem, this);
237 : :
238 [ + - ]: 25382 : Trace("extt-debug") << "ExtTheory::doInferences : infer : " << eq
239 : 12691 : << " by " << exp[i] << std::endl;
240 [ + - ]: 12691 : Trace("extt-debug") << "...send lemma " << lem << std::endl;
241 [ + + ]: 12691 : if (sendLemma(trn, InferenceId::EXTT_SIMPLIFY))
242 : : {
243 [ + - ]: 9404 : Trace("extt-lemma")
244 : 0 : << "ExtTheory : substitution + rewrite lemma : " << lem
245 : 4702 : << std::endl;
246 : 4702 : addedLemma = true;
247 : : }
248 : 12691 : }
249 : : else
250 : : {
251 : : // note : can add (non-reducing) lemma :
252 : : // exp[j] ^ exp[i] => sterms[i] = sterms[j]
253 : : // if there are any duplicates, but we do not do this currently.
254 [ + - ]: 4333 : Trace("extt-nred") << "Non-reduced term : " << sr << std::endl;
255 : : }
256 : 17024 : }
257 : : else
258 : : {
259 [ + - ]: 54886 : Trace("extt-nred") << "Non-reduced term : " << sterms[i] << std::endl;
260 : : }
261 [ + + ]: 71910 : if (!processed)
262 : : {
263 : 59219 : nred.push_back(terms[i]);
264 : : }
265 : : }
266 : :
267 : 70485 : return addedLemma;
268 : 70485 : }
269 : :
270 : 12691 : bool ExtTheory::sendLemma(TrustNode lem, InferenceId id)
271 : : {
272 : 12691 : const Node& n = lem.getProven();
273 [ + + ]: 12691 : if (d_lemmas.find(n) == d_lemmas.end())
274 : : {
275 [ + + ]: 5685 : if (d_im.trustedLemma(lem, id))
276 : : {
277 : 4702 : d_lemmas.insert(n);
278 : 4702 : return true;
279 : : }
280 : : }
281 : 7989 : return false;
282 : 12691 : }
283 : :
284 : 0 : bool ExtTheory::doInferences(int effort,
285 : : const std::vector<Node>& terms,
286 : : std::vector<Node>& nred)
287 : : {
288 [ - - ]: 0 : if (!terms.empty())
289 : : {
290 : 0 : return doInferencesInternal(effort, terms, nred);
291 : : }
292 : 0 : return false;
293 : : }
294 : :
295 : 70485 : bool ExtTheory::doInferences(int effort, std::vector<Node>& nred)
296 : : {
297 : 70485 : std::vector<Node> terms = getActive();
298 : 140970 : return doInferencesInternal(effort, terms, nred);
299 : 70485 : }
300 : :
301 : : // Register term.
302 : 534874 : void ExtTheory::registerTerm(Node n)
303 : : {
304 [ + + ]: 534874 : if (d_extf_kind.find(n.getKind()) != d_extf_kind.end())
305 : : {
306 [ + + ]: 195630 : if (d_ext_func_terms.find(n) == d_ext_func_terms.end())
307 : : {
308 [ + - ]: 39709 : Trace("extt-debug") << "Found extended function : " << n << std::endl;
309 : 39709 : d_ext_func_terms[n] = true;
310 : 39709 : d_has_extf = n;
311 : 39709 : d_extf_info[n].d_vars = collectVars(n);
312 : : }
313 : : }
314 : 534874 : }
315 : :
316 : : // mark reduced
317 : 155921 : void ExtTheory::markInactive(Node n, ExtReducedId rid, bool satDep)
318 : : {
319 [ + - ]: 155921 : Trace("extt-debug") << "Mark reduced " << n << std::endl;
320 : 155921 : registerTerm(n);
321 [ - + ][ - + ]: 155921 : Assert(d_ext_func_terms.find(n) != d_ext_func_terms.end());
[ - - ]
322 : 155921 : d_ext_func_terms[n] = false;
323 : 155921 : d_extfExtReducedIdMap[n] = rid;
324 [ - + ]: 155921 : if (!satDep)
325 : : {
326 : 0 : d_ci_inactive[n] = rid;
327 : : }
328 : :
329 : : // update has_extf
330 [ + + ]: 155921 : if (d_has_extf.get() == n)
331 : : {
332 : 18748 : for (NodeBoolMap::iterator it = d_ext_func_terms.begin();
333 [ + + ]: 269518 : it != d_ext_func_terms.end();
334 : 250770 : ++it)
335 : : {
336 : : // if not already reduced
337 [ + + ][ + - ]: 250770 : if ((*it).second && !isContextIndependentInactive((*it).first))
[ + + ][ + + ]
[ - - ]
338 : : {
339 : 124895 : d_has_extf = (*it).first;
340 : : }
341 : : }
342 : : }
343 : 155921 : }
344 : :
345 : 1552733 : bool ExtTheory::isContextIndependentInactive(Node n) const
346 : : {
347 : 1552733 : ExtReducedId rid = ExtReducedId::UNKNOWN;
348 : 1552733 : return isContextIndependentInactive(n, rid);
349 : : }
350 : :
351 : 2273226 : bool ExtTheory::isContextIndependentInactive(Node n, ExtReducedId& rid) const
352 : : {
353 : 2273226 : NodeExtReducedIdMap::iterator it = d_ci_inactive.find(n);
354 [ - + ]: 2273226 : if (it != d_ci_inactive.end())
355 : : {
356 : 0 : rid = it->second;
357 : 0 : return true;
358 : : }
359 : 2273226 : return false;
360 : : }
361 : :
362 : 13363 : void ExtTheory::getTerms(std::vector<Node>& terms)
363 : : {
364 : 13363 : for (NodeBoolMap::iterator it = d_ext_func_terms.begin();
365 [ + + ]: 88345 : it != d_ext_func_terms.end();
366 : 74982 : ++it)
367 : : {
368 : 74982 : terms.push_back((*it).first);
369 : : }
370 : 13363 : }
371 : :
372 : 0 : bool ExtTheory::hasActiveTerm() const { return !d_has_extf.get().isNull(); }
373 : :
374 : 720626 : bool ExtTheory::isActive(Node n) const
375 : : {
376 : 720626 : ExtReducedId rid = ExtReducedId::UNKNOWN;
377 : 720626 : return isActive(n, rid);
378 : : }
379 : :
380 : 720626 : bool ExtTheory::isActive(Node n, ExtReducedId& rid) const
381 : : {
382 : 720626 : NodeBoolMap::const_iterator it = d_ext_func_terms.find(n);
383 [ + - ]: 720626 : if (it != d_ext_func_terms.end())
384 : : {
385 [ + + ]: 720626 : if ((*it).second)
386 : : {
387 : 720493 : return !isContextIndependentInactive(n, rid);
388 : : }
389 : 133 : NodeExtReducedIdMap::const_iterator itr = d_extfExtReducedIdMap.find(n);
390 [ - + ][ - + ]: 133 : Assert(itr != d_extfExtReducedIdMap.end());
[ - - ]
391 : 133 : rid = itr->second;
392 : 133 : return false;
393 : : }
394 : 0 : return false;
395 : : }
396 : :
397 : : // get active
398 : 264329 : std::vector<Node> ExtTheory::getActive() const
399 : : {
400 : 264329 : std::vector<Node> active;
401 : 264329 : for (NodeBoolMap::iterator it = d_ext_func_terms.begin();
402 [ + + ]: 2039167 : it != d_ext_func_terms.end();
403 : 1774838 : ++it)
404 : : {
405 : : // if not already reduced
406 [ + + ][ + - ]: 1774838 : if ((*it).second && !isContextIndependentInactive((*it).first))
[ + + ][ + + ]
[ - - ]
407 : : {
408 : 1424355 : active.push_back((*it).first);
409 : : }
410 : : }
411 : 264329 : return active;
412 : 0 : }
413 : :
414 : 26132 : std::vector<Node> ExtTheory::getActive(Kind k) const
415 : : {
416 : 26132 : std::vector<Node> active;
417 : 26132 : for (NodeBoolMap::iterator it = d_ext_func_terms.begin();
418 [ + + ]: 77332 : it != d_ext_func_terms.end();
419 : 51200 : ++it)
420 : : {
421 : : // if not already reduced
422 [ + + ]: 60370 : if ((*it).first.getKind() == k && (*it).second
423 [ + + ][ + - ]: 111570 : && !isContextIndependentInactive((*it).first))
[ + + ][ + + ]
[ - - ]
424 : : {
425 : 3483 : active.push_back((*it).first);
426 : : }
427 : : }
428 : 26132 : return active;
429 : 0 : }
430 : :
431 : 1318 : std::shared_ptr<ProofNode> ExtTheory::getProofFor(Node fact)
432 : : {
433 : 2636 : CDProof proof(d_env);
434 : 1318 : std::vector<Node> antec;
435 : 1318 : Node conc = fact;
436 [ + - ]: 1318 : if (conc.getKind() == Kind::IMPLIES)
437 : : {
438 [ + + ]: 1318 : if (conc[0].getKind() == Kind::AND)
439 : : {
440 : 284 : antec.insert(antec.end(), conc[0].begin(), conc[0].end());
441 : : }
442 : : else
443 : : {
444 : 1034 : antec.push_back(conc[0]);
445 : : }
446 : 1318 : conc = conc[1];
447 : : }
448 : 1318 : ProofChecker* pc = d_env.getProofNodeManager()->getChecker();
449 : : Node res =
450 : 5272 : pc->checkDebug(ProofRule::MACRO_SR_PRED_INTRO, antec, {conc}, conc);
451 [ - + ]: 1318 : if (res.isNull())
452 : : {
453 : 0 : DebugUnhandled() << "ExtTheory failed to prove " << fact;
454 : : return nullptr;
455 : : }
456 : 2636 : proof.addStep(conc, ProofRule::MACRO_SR_PRED_INTRO, antec, {conc});
457 [ + - ]: 1318 : if (!antec.empty())
458 : : {
459 : 2636 : proof.addStep(fact, ProofRule::SCOPE, {conc}, antec);
460 : : }
461 : : // t1 = s1 ... tn = sn
462 : : // -------------------- MACRO_SR_PRED_INTRO {t}
463 : : // t = s
464 : : // ----------------------------------- SCOPE {t1 = s1 ... tn = sn}
465 : : // (t1 = s1 ^ ... ^ tn = sn) => (t = s).
466 : 1318 : return proof.getProofFor(fact);
467 : 1318 : }
468 : :
469 : 758 : std::string ExtTheory::identify() const { return "ExtTheory"; }
470 : :
471 : : } // namespace theory
472 : : } // namespace cvc5::internal
|
