Branch data Line data Source code
1 : : /******************************************************************************
2 : : * Top contributors (to current version):
3 : : * Andrew Reynolds, Tim King, Gereon Kremer
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 : : * Extended theory interface.
14 : : *
15 : : * This implements a generic module, used by theory solvers, for performing
16 : : * "context-dependent simplification", as described in Reynolds et al
17 : : * "Designing Theory Solvers with Extensions", FroCoS 2017.
18 : : */
19 : :
20 : : #include "theory/ext_theory.h"
21 : :
22 : : #include "base/check.h"
23 : : #include "theory/output_channel.h"
24 : : #include "theory/quantifiers_engine.h"
25 : : #include "theory/rewriter.h"
26 : : #include "theory/substitutions.h"
27 : :
28 : : using namespace std;
29 : :
30 : : namespace cvc5::internal {
31 : : namespace theory {
32 : :
33 : 15 : const char* toString(ExtReducedId id)
34 : : {
35 [ + + ][ + + ]: 15 : switch (id)
[ + + ][ + + ]
[ + + ][ + + ]
[ + + ][ + - ]
[ - ]
36 : : {
37 : 1 : case ExtReducedId::NONE: return "NONE";
38 : 1 : case ExtReducedId::SR_CONST: return "SR_CONST";
39 : 1 : case ExtReducedId::REDUCTION: return "REDUCTION";
40 : 1 : case ExtReducedId::ARITH_SR_ZERO: return "ARITH_SR_ZERO";
41 : 1 : case ExtReducedId::ARITH_SR_LINEAR: return "ARITH_SR_LINEAR";
42 : 1 : case ExtReducedId::STRINGS_SR_CONST: return "STRINGS_SR_CONST";
43 : 1 : case ExtReducedId::STRINGS_NEG_CTN_DEQ: return "STRINGS_NEG_CTN_DEQ";
44 : 1 : case ExtReducedId::STRINGS_CTN_DECOMPOSE: return "STRINGS_CTN_DECOMPOSE";
45 : 1 : case ExtReducedId::STRINGS_REGEXP_INTER: return "STRINGS_REGEXP_INTER";
46 : 1 : case ExtReducedId::STRINGS_REGEXP_INTER_SUBSUME:
47 : 1 : return "STRINGS_REGEXP_INTER_SUBSUME";
48 : 1 : case ExtReducedId::STRINGS_REGEXP_INCLUDE: return "STRINGS_REGEXP_INCLUDE";
49 : 1 : case ExtReducedId::STRINGS_REGEXP_INCLUDE_NEG:
50 : 1 : return "STRINGS_REGEXP_INCLUDE_NEG";
51 : 1 : case ExtReducedId::STRINGS_REGEXP_RE_SYM_NF:
52 : 1 : return "STRINGS_REGEXP_RE_SYM_NF";
53 : 1 : case ExtReducedId::STRINGS_REGEXP_PDERIVATIVE:
54 : 1 : return "STRINGS_REGEXP_PDERIVATIVE";
55 : 1 : case ExtReducedId::STRINGS_NTH_REV: return "STRINGS_NTH_REV";
56 : 0 : case ExtReducedId::UNKNOWN: return "?";
57 : 0 : default: Unreachable(); return "?ExtReducedId?";
58 : : }
59 : : }
60 : :
61 : 15 : std::ostream& operator<<(std::ostream& out, ExtReducedId id)
62 : : {
63 : 15 : out << toString(id);
64 : 15 : return out;
65 : : }
66 : :
67 : 0 : bool ExtTheoryCallback::getCurrentSubstitution(
68 : : int effort,
69 : : const std::vector<Node>& vars,
70 : : std::vector<Node>& subs,
71 : : std::map<Node, std::vector<Node> >& exp)
72 : : {
73 : 0 : return false;
74 : : }
75 : 0 : bool ExtTheoryCallback::isExtfReduced(
76 : : int effort, Node n, Node on, std::vector<Node>& exp, ExtReducedId& id)
77 : : {
78 : 0 : id = ExtReducedId::SR_CONST;
79 : 0 : return n.isConst();
80 : : }
81 : 0 : bool ExtTheoryCallback::getReduction(int effort,
82 : : Node n,
83 : : Node& nr,
84 : : bool& isSatDep)
85 : : {
86 : 0 : return false;
87 : : }
88 : :
89 : 81314 : ExtTheory::ExtTheory(Env& env, ExtTheoryCallback& p, TheoryInferenceManager& im)
90 : : : EnvObj(env),
91 : : d_parent(p),
92 : : d_im(im),
93 : : d_ext_func_terms(context()),
94 : : d_extfExtReducedIdMap(context()),
95 : 162628 : d_ci_inactive(userContext()),
96 : : d_has_extf(context()),
97 : 81314 : d_lemmas(userContext())
98 : : {
99 : 81314 : d_true = nodeManager()->mkConst(true);
100 : 81314 : }
101 : :
102 : : // Gets all leaf terms in n.
103 : 36248 : std::vector<Node> ExtTheory::collectVars(Node n)
104 : : {
105 : 36248 : std::vector<Node> vars;
106 : 72496 : std::set<Node> visited;
107 : 72496 : std::vector<Node> worklist;
108 : 36248 : worklist.push_back(n);
109 [ + + ]: 236418 : while (!worklist.empty())
110 : : {
111 : 200170 : Node current = worklist.back();
112 : 200170 : worklist.pop_back();
113 [ + + ][ + + ]: 200170 : if (current.isConst() || visited.count(current) > 0)
[ + + ]
114 : : {
115 : 60040 : continue;
116 : : }
117 : 140130 : visited.insert(current);
118 : : // Treat terms not belonging to this theory as leaf
119 : : // note : chould include terms not belonging to this theory
120 : : // (commented below)
121 [ + + ]: 140130 : if (current.getNumChildren() > 0)
122 : : {
123 : 81994 : worklist.insert(worklist.end(), current.begin(), current.end());
124 : : }
125 : : else
126 : : {
127 : 58136 : vars.push_back(current);
128 : : }
129 : : }
130 : 72496 : return vars;
131 : : }
132 : :
133 : 0 : Node ExtTheory::getSubstitutedTerm(int effort,
134 : : Node term,
135 : : std::vector<Node>& exp)
136 : : {
137 : 0 : std::vector<Node> terms;
138 : 0 : terms.push_back(term);
139 : 0 : std::vector<Node> sterms;
140 : 0 : std::vector<std::vector<Node> > exps;
141 : 0 : getSubstitutedTerms(effort, terms, sterms, exps);
142 : 0 : Assert(sterms.size() == 1);
143 : 0 : Assert(exps.size() == 1);
144 : 0 : exp.insert(exp.end(), exps[0].begin(), exps[0].end());
145 : 0 : return sterms[0];
146 : : }
147 : :
148 : : // do inferences
149 : 74386 : void ExtTheory::getSubstitutedTerms(int effort,
150 : : const std::vector<Node>& terms,
151 : : std::vector<Node>& sterms,
152 : : std::vector<std::vector<Node> >& exp)
153 : : {
154 [ + - ]: 148772 : Trace("extt-debug") << "getSubstitutedTerms for " << terms.size() << " / "
155 : 74386 : << d_ext_func_terms.size() << " extended functions."
156 : 74386 : << std::endl;
157 [ + + ]: 74386 : if (!terms.empty())
158 : : {
159 : : // all variables we need to find a substitution for
160 : 24392 : std::vector<Node> vars;
161 : 24392 : std::vector<Node> sub;
162 : 24392 : std::map<Node, std::vector<Node> > expc;
163 [ + + ]: 79248 : for (const Node& n : terms)
164 : : {
165 : : // do substitution, rewrite
166 : 67052 : std::map<Node, ExtfInfo>::iterator iti = d_extf_info.find(n);
167 [ - + ][ - + ]: 67052 : Assert(iti != d_extf_info.end());
[ - - ]
168 [ + + ]: 184613 : for (const Node& v : iti->second.d_vars)
169 : : {
170 [ + + ]: 117561 : if (std::find(vars.begin(), vars.end(), v) == vars.end())
171 : : {
172 : 55939 : vars.push_back(v);
173 : : }
174 : : }
175 : : }
176 : 12196 : bool useSubs = d_parent.getCurrentSubstitution(effort, vars, sub, expc);
177 : : // get the current substitution for all variables
178 [ + + ][ - + ]: 12196 : Assert(!useSubs || vars.size() == sub.size());
[ - + ][ - - ]
179 [ + + ]: 79248 : for (const Node& n : terms)
180 : : {
181 : 134104 : Node ns = n;
182 : 134104 : std::vector<Node> expn;
183 [ + + ]: 67052 : if (useSubs)
184 : : {
185 : : // do substitution
186 : 38508 : ns = n.substitute(vars.begin(), vars.end(), sub.begin(), sub.end());
187 [ + + ]: 38508 : if (ns != n)
188 : : {
189 : : // build explanation: explanation vars = sub for each vars in FV(n)
190 : 18433 : std::map<Node, ExtfInfo>::iterator iti = d_extf_info.find(n);
191 [ - + ][ - + ]: 18433 : Assert(iti != d_extf_info.end());
[ - - ]
192 [ + + ]: 53854 : for (const Node& v : iti->second.d_vars)
193 : : {
194 : 35421 : std::map<Node, std::vector<Node> >::iterator itx = expc.find(v);
195 [ + + ]: 35421 : if (itx != expc.end())
196 : : {
197 [ + + ]: 42750 : for (const Node& e : itx->second)
198 : : {
199 [ + - ]: 21375 : if (std::find(expn.begin(), expn.end(), e) == expn.end())
200 : : {
201 : 21375 : expn.push_back(e);
202 : : }
203 : : }
204 : : }
205 : : }
206 : : }
207 [ + - ]: 77016 : Trace("extt-debug") << " have " << n << " == " << ns
208 : 38508 : << ", exp size=" << expn.size() << "." << std::endl;
209 : : }
210 : : // add to vector
211 : 67052 : sterms.push_back(ns);
212 : 67052 : exp.push_back(expn);
213 : : }
214 : : }
215 : 74386 : }
216 : :
217 : 74386 : bool ExtTheory::doInferencesInternal(int effort,
218 : : const std::vector<Node>& terms,
219 : : std::vector<Node>& nred,
220 : : bool isRed)
221 : : {
222 : 74386 : bool addedLemma = false;
223 [ - + ]: 74386 : if (isRed)
224 : : {
225 [ - - ]: 0 : for (const Node& n : terms)
226 : : {
227 : 0 : Node nr;
228 : : // note: could do reduction with substitution here
229 : 0 : bool satDep = false;
230 [ - - ]: 0 : if (!d_parent.getReduction(effort, n, nr, satDep))
231 : : {
232 : 0 : nred.push_back(n);
233 : : }
234 : : else
235 : : {
236 : 0 : if (!nr.isNull() && n != nr)
237 : : {
238 : 0 : Node lem = nodeManager()->mkNode(Kind::EQUAL, n, nr);
239 [ - - ]: 0 : if (sendLemma(lem, InferenceId::EXTT_SIMPLIFY))
240 : : {
241 [ - - ]: 0 : Trace("extt-lemma")
242 : 0 : << "ExtTheory : reduction lemma : " << lem << std::endl;
243 : 0 : addedLemma = true;
244 : : }
245 : : }
246 : 0 : markInactive(n, ExtReducedId::REDUCTION, satDep);
247 : : }
248 : : }
249 : : }
250 : : else
251 : : {
252 : 148772 : std::vector<Node> sterms;
253 : 148772 : std::vector<std::vector<Node> > exp;
254 : 74386 : getSubstitutedTerms(effort, terms, sterms, exp);
255 : 148772 : std::map<Node, unsigned> sterm_index;
256 : 74386 : NodeManager* nm = nodeManager();
257 [ + + ]: 141438 : for (unsigned i = 0, size = terms.size(); i < size; i++)
258 : : {
259 : 67052 : bool processed = false;
260 [ + + ]: 67052 : if (sterms[i] != terms[i])
261 : : {
262 : 36866 : Node sr = rewrite(sterms[i]);
263 : : // ask the theory if this term is reduced, e.g. is it constant or it
264 : : // is a non-extf term.
265 : : ExtReducedId id;
266 [ + + ]: 18433 : if (d_parent.isExtfReduced(effort, sr, terms[i], exp[i], id))
267 : : {
268 : 15461 : processed = true;
269 : 15461 : markInactive(terms[i], id);
270 : : // We have exp[i] => terms[i] = sr, convert this to a clause.
271 : : // This ensures the proof infrastructure can process this as a
272 : : // normal theory lemma.
273 : 30922 : Node eq = terms[i].eqNode(sr);
274 : 30922 : Node lem = eq;
275 [ + - ]: 15461 : if (!exp[i].empty())
276 : : {
277 : 15461 : std::vector<Node> eei;
278 [ + + ]: 32921 : for (const Node& e : exp[i])
279 : : {
280 : 17460 : eei.push_back(e.negate());
281 : : }
282 : 15461 : eei.push_back(eq);
283 : 15461 : lem = nm->mkNode(Kind::OR, eei);
284 : : }
285 : :
286 [ + - ]: 30922 : Trace("extt-debug") << "ExtTheory::doInferences : infer : " << eq
287 : 15461 : << " by " << exp[i] << std::endl;
288 [ + - ]: 15461 : Trace("extt-debug") << "...send lemma " << lem << std::endl;
289 [ + + ]: 15461 : if (sendLemma(lem, InferenceId::EXTT_SIMPLIFY))
290 : : {
291 [ + - ]: 10364 : Trace("extt-lemma")
292 : 0 : << "ExtTheory : substitution + rewrite lemma : " << lem
293 : 5182 : << std::endl;
294 : 5182 : addedLemma = true;
295 : : }
296 : : }
297 : : else
298 : : {
299 : : // check if we have already reduced this
300 : 2972 : std::map<Node, unsigned>::iterator itsi = sterm_index.find(sr);
301 [ + + ]: 2972 : if (itsi == sterm_index.end())
302 : : {
303 : 2752 : sterm_index[sr] = i;
304 : : }
305 : : else
306 : : {
307 : : // unsigned j = itsi->second;
308 : : // note : can add (non-reducing) lemma :
309 : : // exp[j] ^ exp[i] => sterms[i] = sterms[j]
310 : : }
311 : :
312 [ + - ]: 2972 : Trace("extt-nred") << "Non-reduced term : " << sr << std::endl;
313 : : }
314 : : }
315 : : else
316 : : {
317 [ + - ]: 48619 : Trace("extt-nred") << "Non-reduced term : " << sterms[i] << std::endl;
318 : : }
319 [ + + ]: 67052 : if (!processed)
320 : : {
321 : 51591 : nred.push_back(terms[i]);
322 : : }
323 : : }
324 : : }
325 : 74386 : return addedLemma;
326 : : }
327 : :
328 : 15461 : bool ExtTheory::sendLemma(Node lem, InferenceId id)
329 : : {
330 [ + + ]: 15461 : if (d_lemmas.find(lem) == d_lemmas.end())
331 : : {
332 [ + - ]: 5182 : if (d_im.lemma(lem, id))
333 : : {
334 : 5182 : d_lemmas.insert(lem);
335 : 5182 : return true;
336 : : }
337 : : }
338 : 10279 : return false;
339 : : }
340 : :
341 : 0 : bool ExtTheory::doInferences(int effort,
342 : : const std::vector<Node>& terms,
343 : : std::vector<Node>& nred)
344 : : {
345 [ - - ]: 0 : if (!terms.empty())
346 : : {
347 : 0 : return doInferencesInternal(effort, terms, nred, false);
348 : : }
349 : 0 : return false;
350 : : }
351 : :
352 : 74386 : bool ExtTheory::doInferences(int effort, std::vector<Node>& nred)
353 : : {
354 : 148772 : std::vector<Node> terms = getActive();
355 : 148772 : return doInferencesInternal(effort, terms, nred, false);
356 : : }
357 : :
358 : 0 : bool ExtTheory::doReductions(int effort,
359 : : const std::vector<Node>& terms,
360 : : std::vector<Node>& nred)
361 : : {
362 [ - - ]: 0 : if (!terms.empty())
363 : : {
364 : 0 : return doInferencesInternal(effort, terms, nred, true);
365 : : }
366 : 0 : return false;
367 : : }
368 : :
369 : 0 : bool ExtTheory::doReductions(int effort, std::vector<Node>& nred)
370 : : {
371 : 0 : const std::vector<Node> terms = getActive();
372 : 0 : return doInferencesInternal(effort, terms, nred, true);
373 : : }
374 : :
375 : : // Register term.
376 : 447991 : void ExtTheory::registerTerm(Node n)
377 : : {
378 [ + + ]: 447991 : if (d_extf_kind.find(n.getKind()) != d_extf_kind.end())
379 : : {
380 [ + + ]: 153248 : if (d_ext_func_terms.find(n) == d_ext_func_terms.end())
381 : : {
382 [ + - ]: 36248 : Trace("extt-debug") << "Found extended function : " << n << std::endl;
383 : 36248 : d_ext_func_terms[n] = true;
384 : 36248 : d_has_extf = n;
385 : 36248 : d_extf_info[n].d_vars = collectVars(n);
386 : : }
387 : : }
388 : 447991 : }
389 : :
390 : : // mark reduced
391 : 117000 : void ExtTheory::markInactive(Node n, ExtReducedId rid, bool satDep)
392 : : {
393 [ + - ]: 117000 : Trace("extt-debug") << "Mark reduced " << n << std::endl;
394 : 117000 : registerTerm(n);
395 [ - + ][ - + ]: 117000 : Assert(d_ext_func_terms.find(n) != d_ext_func_terms.end());
[ - - ]
396 : 117000 : d_ext_func_terms[n] = false;
397 : 117000 : d_extfExtReducedIdMap[n] = rid;
398 [ - + ]: 117000 : if (!satDep)
399 : : {
400 : 0 : d_ci_inactive[n] = rid;
401 : : }
402 : :
403 : : // update has_extf
404 [ + + ]: 117000 : if (d_has_extf.get() == n)
405 : : {
406 : 189369 : for (NodeBoolMap::iterator it = d_ext_func_terms.begin();
407 [ + + ]: 189369 : it != d_ext_func_terms.end();
408 : 176021 : ++it)
409 : : {
410 : : // if not already reduced
411 [ + + ][ + - ]: 176021 : if ((*it).second && !isContextIndependentInactive((*it).first))
[ + + ][ + + ]
[ - - ]
412 : : {
413 : 82834 : d_has_extf = (*it).first;
414 : : }
415 : : }
416 : : }
417 : 117000 : }
418 : :
419 : 964110 : bool ExtTheory::isContextIndependentInactive(Node n) const
420 : : {
421 : 964110 : ExtReducedId rid = ExtReducedId::UNKNOWN;
422 : 964110 : return isContextIndependentInactive(n, rid);
423 : : }
424 : :
425 : 1387050 : bool ExtTheory::isContextIndependentInactive(Node n, ExtReducedId& rid) const
426 : : {
427 : 1387050 : NodeExtReducedIdMap::iterator it = d_ci_inactive.find(n);
428 [ - + ]: 1387050 : if (it != d_ci_inactive.end())
429 : : {
430 : 0 : rid = it->second;
431 : 0 : return true;
432 : : }
433 : 1387050 : return false;
434 : : }
435 : :
436 : 12315 : void ExtTheory::getTerms(std::vector<Node>& terms)
437 : : {
438 : 82970 : for (NodeBoolMap::iterator it = d_ext_func_terms.begin();
439 [ + + ]: 82970 : it != d_ext_func_terms.end();
440 : 70655 : ++it)
441 : : {
442 : 70655 : terms.push_back((*it).first);
443 : : }
444 : 12315 : }
445 : :
446 : 0 : bool ExtTheory::hasActiveTerm() const { return !d_has_extf.get().isNull(); }
447 : :
448 : 422937 : bool ExtTheory::isActive(Node n) const
449 : : {
450 : 422937 : ExtReducedId rid = ExtReducedId::UNKNOWN;
451 : 422937 : return isActive(n, rid);
452 : : }
453 : :
454 : 422937 : bool ExtTheory::isActive(Node n, ExtReducedId& rid) const
455 : : {
456 : 422937 : NodeBoolMap::const_iterator it = d_ext_func_terms.find(n);
457 [ + - ]: 422937 : if (it != d_ext_func_terms.end())
458 : : {
459 [ + - ]: 422937 : if ((*it).second)
460 : : {
461 : 422937 : return !isContextIndependentInactive(n, rid);
462 : : }
463 : 0 : NodeExtReducedIdMap::const_iterator itr = d_extfExtReducedIdMap.find(n);
464 : 0 : Assert(itr != d_extfExtReducedIdMap.end());
465 : 0 : rid = itr->second;
466 : 0 : return false;
467 : : }
468 : 0 : return false;
469 : : }
470 : :
471 : : // get active
472 : 260136 : std::vector<Node> ExtTheory::getActive() const
473 : : {
474 : 260136 : std::vector<Node> active;
475 : 1392690 : for (NodeBoolMap::iterator it = d_ext_func_terms.begin();
476 [ + + ]: 1392690 : it != d_ext_func_terms.end();
477 : 1132550 : ++it)
478 : : {
479 : : // if not already reduced
480 [ + + ][ + - ]: 1132550 : if ((*it).second && !isContextIndependentInactive((*it).first))
[ + + ][ + + ]
[ - - ]
481 : : {
482 : 876861 : active.push_back((*it).first);
483 : : }
484 : : }
485 : 260136 : return active;
486 : : }
487 : :
488 : 31503 : std::vector<Node> ExtTheory::getActive(Kind k) const
489 : : {
490 : 31503 : std::vector<Node> active;
491 : 86259 : for (NodeBoolMap::iterator it = d_ext_func_terms.begin();
492 [ + + ]: 86259 : it != d_ext_func_terms.end();
493 : 54756 : ++it)
494 : : {
495 : : // if not already reduced
496 [ + + ]: 65232 : if ((*it).first.getKind() == k && (*it).second
497 [ + + ][ + - ]: 119988 : && !isContextIndependentInactive((*it).first))
[ + + ][ + + ]
[ - - ]
498 : : {
499 : 4415 : active.push_back((*it).first);
500 : : }
501 : : }
502 : 31503 : return active;
503 : : }
504 : :
505 : : } // namespace theory
506 : : } // namespace cvc5::internal
|
