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 "proof/proof_checker.h"
24 : : #include "proof/proof_node_manager.h"
25 : : #include "theory/output_channel.h"
26 : : #include "theory/quantifiers_engine.h"
27 : : #include "theory/rewriter.h"
28 : : #include "theory/substitutions.h"
29 : :
30 : : using namespace std;
31 : :
32 : : namespace cvc5::internal {
33 : : namespace theory {
34 : :
35 : 15 : const char* toString(ExtReducedId id)
36 : : {
37 [ + + ][ + + ]: 15 : switch (id)
[ + + ][ + + ]
[ + + ][ + + ]
[ + + ][ + - ]
[ - ]
38 : : {
39 : 1 : case ExtReducedId::NONE: return "NONE";
40 : 1 : case ExtReducedId::SR_CONST: return "SR_CONST";
41 : 1 : case ExtReducedId::REDUCTION: return "REDUCTION";
42 : 1 : case ExtReducedId::ARITH_SR_ZERO: return "ARITH_SR_ZERO";
43 : 1 : case ExtReducedId::ARITH_SR_LINEAR: return "ARITH_SR_LINEAR";
44 : 1 : case ExtReducedId::STRINGS_SR_CONST: return "STRINGS_SR_CONST";
45 : 1 : case ExtReducedId::STRINGS_NEG_CTN_DEQ: return "STRINGS_NEG_CTN_DEQ";
46 : 1 : case ExtReducedId::STRINGS_CTN_DECOMPOSE: return "STRINGS_CTN_DECOMPOSE";
47 : 1 : case ExtReducedId::STRINGS_REGEXP_INTER: return "STRINGS_REGEXP_INTER";
48 : 1 : case ExtReducedId::STRINGS_REGEXP_INTER_SUBSUME:
49 : 1 : return "STRINGS_REGEXP_INTER_SUBSUME";
50 : 1 : case ExtReducedId::STRINGS_REGEXP_INCLUDE: return "STRINGS_REGEXP_INCLUDE";
51 : 1 : case ExtReducedId::STRINGS_REGEXP_INCLUDE_NEG:
52 : 1 : return "STRINGS_REGEXP_INCLUDE_NEG";
53 : 1 : case ExtReducedId::STRINGS_REGEXP_RE_SYM_NF:
54 : 1 : return "STRINGS_REGEXP_RE_SYM_NF";
55 : 1 : case ExtReducedId::STRINGS_REGEXP_PDERIVATIVE:
56 : 1 : return "STRINGS_REGEXP_PDERIVATIVE";
57 : 1 : case ExtReducedId::STRINGS_NTH_REV: return "STRINGS_NTH_REV";
58 : 0 : case ExtReducedId::UNKNOWN: return "?";
59 : 0 : default: Unreachable(); return "?ExtReducedId?";
60 : : }
61 : : }
62 : :
63 : 15 : std::ostream& operator<<(std::ostream& out, ExtReducedId id)
64 : : {
65 : 15 : out << toString(id);
66 : 15 : return out;
67 : : }
68 : :
69 : 0 : bool ExtTheoryCallback::getCurrentSubstitution(
70 : : int effort,
71 : : const std::vector<Node>& vars,
72 : : std::vector<Node>& subs,
73 : : std::map<Node, std::vector<Node> >& exp)
74 : : {
75 : 0 : return false;
76 : : }
77 : 0 : bool ExtTheoryCallback::isExtfReduced(
78 : : int effort, Node n, Node on, std::vector<Node>& exp, ExtReducedId& id)
79 : : {
80 : 0 : id = ExtReducedId::SR_CONST;
81 : 0 : return n.isConst();
82 : : }
83 : 0 : bool ExtTheoryCallback::getReduction(int effort,
84 : : Node n,
85 : : Node& nr,
86 : : bool& isSatDep)
87 : : {
88 : 0 : return false;
89 : : }
90 : :
91 : 82380 : ExtTheory::ExtTheory(Env& env, ExtTheoryCallback& p, TheoryInferenceManager& im)
92 : : : EnvObj(env),
93 : : d_parent(p),
94 : : d_im(im),
95 : : d_ext_func_terms(context()),
96 : : d_extfExtReducedIdMap(context()),
97 : 164760 : d_ci_inactive(userContext()),
98 : : d_has_extf(context()),
99 : 82380 : d_lemmas(userContext())
100 : : {
101 : 82380 : d_true = nodeManager()->mkConst(true);
102 : 82380 : }
103 : :
104 : : // Gets all leaf terms in n.
105 : 35080 : std::vector<Node> ExtTheory::collectVars(Node n)
106 : : {
107 : 35080 : std::vector<Node> vars;
108 : 70160 : std::set<Node> visited;
109 : 70160 : std::vector<Node> worklist;
110 : 35080 : worklist.push_back(n);
111 [ + + ]: 228748 : while (!worklist.empty())
112 : : {
113 : 193668 : Node current = worklist.back();
114 : 193668 : worklist.pop_back();
115 [ + + ][ + + ]: 193668 : if (current.isConst() || visited.count(current) > 0)
[ + + ]
116 : : {
117 : 59718 : continue;
118 : : }
119 : 133950 : 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 [ + + ]: 133950 : if (current.getNumChildren() > 0)
124 : : {
125 : 78918 : worklist.insert(worklist.end(), current.begin(), current.end());
126 : : }
127 : : else
128 : : {
129 : 55032 : vars.push_back(current);
130 : : }
131 : : }
132 : 70160 : return vars;
133 : : }
134 : :
135 : : // do inferences
136 : 74812 : 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 [ + - ]: 149624 : Trace("extt-debug") << "getSubstitutedTerms for " << terms.size() << " / "
142 : 74812 : << d_ext_func_terms.size() << " extended functions."
143 : 74812 : << std::endl;
144 [ + + ]: 74812 : if (!terms.empty())
145 : : {
146 : : // all variables we need to find a substitution for
147 : 22374 : std::vector<Node> vars;
148 : 22374 : std::vector<Node> sub;
149 : 22374 : std::map<Node, std::vector<Node> > expc;
150 [ + + ]: 61059 : for (const Node& n : terms)
151 : : {
152 : : // do substitution, rewrite
153 : 49872 : std::map<Node, ExtfInfo>::iterator iti = d_extf_info.find(n);
154 [ - + ][ - + ]: 49872 : Assert(iti != d_extf_info.end());
[ - - ]
155 [ + + ]: 135056 : for (const Node& v : iti->second.d_vars)
156 : : {
157 [ + + ]: 85184 : if (std::find(vars.begin(), vars.end(), v) == vars.end())
158 : : {
159 : 45933 : vars.push_back(v);
160 : : }
161 : : }
162 : : }
163 : 11187 : bool useSubs = d_parent.getCurrentSubstitution(effort, vars, sub, expc);
164 : : // get the current substitution for all variables
165 [ + + ][ - + ]: 11187 : Assert(!useSubs || vars.size() == sub.size());
[ - + ][ - - ]
166 [ + + ]: 61059 : for (const Node& n : terms)
167 : : {
168 : 99744 : Node ns = n;
169 : 99744 : std::vector<Node> expn;
170 [ + + ]: 49872 : if (useSubs)
171 : : {
172 : : // do substitution
173 : 26270 : ns = n.substitute(vars.begin(), vars.end(), sub.begin(), sub.end());
174 [ + + ]: 26270 : if (ns != n)
175 : : {
176 : : // build explanation: explanation vars = sub for each vars in FV(n)
177 : 11976 : std::map<Node, ExtfInfo>::iterator iti = d_extf_info.find(n);
178 [ - + ][ - + ]: 11976 : Assert(iti != d_extf_info.end());
[ - - ]
179 [ + + ]: 34708 : for (const Node& v : iti->second.d_vars)
180 : : {
181 : 22732 : std::map<Node, std::vector<Node> >::iterator itx = expc.find(v);
182 [ + + ]: 22732 : if (itx != expc.end())
183 : : {
184 [ + + ]: 27292 : for (const Node& e : itx->second)
185 : : {
186 [ + - ]: 13646 : if (std::find(expn.begin(), expn.end(), e) == expn.end())
187 : : {
188 : 13646 : expn.push_back(e);
189 : : }
190 : : }
191 : : }
192 : : }
193 : : }
194 [ + - ]: 52540 : Trace("extt-debug") << " have " << n << " == " << ns
195 : 26270 : << ", exp size=" << expn.size() << "." << std::endl;
196 : : }
197 : : // add to vector
198 : 49872 : sterms.push_back(ns);
199 : 49872 : exp.push_back(expn);
200 : : }
201 : : }
202 : 74812 : }
203 : :
204 : 74812 : bool ExtTheory::doInferencesInternal(int effort,
205 : : const std::vector<Node>& terms,
206 : : std::vector<Node>& nred)
207 : : {
208 : 74812 : bool addedLemma = false;
209 : 149624 : std::vector<Node> sterms;
210 : 74812 : std::vector<std::vector<Node> > exp;
211 : 74812 : getSubstitutedTerms(effort, terms, sterms, exp);
212 : 74812 : NodeManager* nm = nodeManager();
213 [ + + ]: 124684 : for (unsigned i = 0, size = terms.size(); i < size; i++)
214 : : {
215 : 49872 : bool processed = false;
216 : : // if the substitution applied to terms[i] changed it
217 [ + + ]: 49872 : if (sterms[i] != terms[i])
218 : : {
219 : 23952 : 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 [ + + ]: 11976 : if (d_parent.isExtfReduced(effort, sr, terms[i], exp[i], id))
224 : : {
225 : 8602 : processed = true;
226 : 8602 : markInactive(terms[i], id);
227 : : // We have exp[i] => terms[i] = sr
228 : 17204 : Node eq = terms[i].eqNode(sr);
229 : 17204 : Node lem = eq;
230 [ + - ]: 8602 : if (!exp[i].empty())
231 : : {
232 : 8602 : Node antec = nm->mkAnd(exp[i]);
233 : 8602 : lem = nm->mkNode(Kind::IMPLIES, antec, eq);
234 : : }
235 : : // will be able to generate a proof for this
236 : 17204 : TrustNode trn = TrustNode::mkTrustLemma(lem, this);
237 : :
238 [ + - ]: 17204 : Trace("extt-debug") << "ExtTheory::doInferences : infer : " << eq
239 : 8602 : << " by " << exp[i] << std::endl;
240 [ + - ]: 8602 : Trace("extt-debug") << "...send lemma " << lem << std::endl;
241 [ + + ]: 8602 : if (sendLemma(trn, InferenceId::EXTT_SIMPLIFY))
242 : : {
243 [ + - ]: 6066 : Trace("extt-lemma")
244 : 0 : << "ExtTheory : substitution + rewrite lemma : " << lem
245 : 3033 : << std::endl;
246 : 3033 : addedLemma = true;
247 : : }
248 : : }
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 [ + - ]: 3374 : Trace("extt-nred") << "Non-reduced term : " << sr << std::endl;
255 : : }
256 : : }
257 : : else
258 : : {
259 [ + - ]: 37896 : Trace("extt-nred") << "Non-reduced term : " << sterms[i] << std::endl;
260 : : }
261 [ + + ]: 49872 : if (!processed)
262 : : {
263 : 41270 : nred.push_back(terms[i]);
264 : : }
265 : : }
266 : :
267 : 149624 : return addedLemma;
268 : : }
269 : :
270 : 8602 : bool ExtTheory::sendLemma(TrustNode lem, InferenceId id)
271 : : {
272 : 17204 : const Node& n = lem.getProven();
273 [ + + ]: 8602 : if (d_lemmas.find(n) == d_lemmas.end())
274 : : {
275 [ + + ]: 3514 : if (d_im.trustedLemma(lem, id))
276 : : {
277 : 3033 : d_lemmas.insert(n);
278 : 3033 : return true;
279 : : }
280 : : }
281 : 5569 : return false;
282 : : }
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 : 74812 : bool ExtTheory::doInferences(int effort, std::vector<Node>& nred)
296 : : {
297 : 149624 : std::vector<Node> terms = getActive();
298 : 149624 : return doInferencesInternal(effort, terms, nred);
299 : : }
300 : :
301 : : // Register term.
302 : 440866 : void ExtTheory::registerTerm(Node n)
303 : : {
304 [ + + ]: 440866 : if (d_extf_kind.find(n.getKind()) != d_extf_kind.end())
305 : : {
306 [ + + ]: 143523 : if (d_ext_func_terms.find(n) == d_ext_func_terms.end())
307 : : {
308 [ + - ]: 35080 : Trace("extt-debug") << "Found extended function : " << n << std::endl;
309 : 35080 : d_ext_func_terms[n] = true;
310 : 35080 : d_has_extf = n;
311 : 35080 : d_extf_info[n].d_vars = collectVars(n);
312 : : }
313 : : }
314 : 440866 : }
315 : :
316 : : // mark reduced
317 : 108443 : void ExtTheory::markInactive(Node n, ExtReducedId rid, bool satDep)
318 : : {
319 [ + - ]: 108443 : Trace("extt-debug") << "Mark reduced " << n << std::endl;
320 : 108443 : registerTerm(n);
321 [ - + ][ - + ]: 108443 : Assert(d_ext_func_terms.find(n) != d_ext_func_terms.end());
[ - - ]
322 : 108443 : d_ext_func_terms[n] = false;
323 : 108443 : d_extfExtReducedIdMap[n] = rid;
324 [ - + ]: 108443 : if (!satDep)
325 : : {
326 : 0 : d_ci_inactive[n] = rid;
327 : : }
328 : :
329 : : // update has_extf
330 [ + + ]: 108443 : if (d_has_extf.get() == n)
331 : : {
332 : 180935 : for (NodeBoolMap::iterator it = d_ext_func_terms.begin();
333 [ + + ]: 180935 : it != d_ext_func_terms.end();
334 : 167932 : ++it)
335 : : {
336 : : // if not already reduced
337 [ + + ][ + - ]: 167932 : if ((*it).second && !isContextIndependentInactive((*it).first))
[ + + ][ + + ]
[ - - ]
338 : : {
339 : 79752 : d_has_extf = (*it).first;
340 : : }
341 : : }
342 : : }
343 : 108443 : }
344 : :
345 : 1244620 : bool ExtTheory::isContextIndependentInactive(Node n) const
346 : : {
347 : 1244620 : ExtReducedId rid = ExtReducedId::UNKNOWN;
348 : 1244620 : return isContextIndependentInactive(n, rid);
349 : : }
350 : :
351 : 1842900 : bool ExtTheory::isContextIndependentInactive(Node n, ExtReducedId& rid) const
352 : : {
353 : 1842900 : NodeExtReducedIdMap::iterator it = d_ci_inactive.find(n);
354 [ - + ]: 1842900 : if (it != d_ci_inactive.end())
355 : : {
356 : 0 : rid = it->second;
357 : 0 : return true;
358 : : }
359 : 1842900 : return false;
360 : : }
361 : :
362 : 11307 : void ExtTheory::getTerms(std::vector<Node>& terms)
363 : : {
364 : 63672 : for (NodeBoolMap::iterator it = d_ext_func_terms.begin();
365 [ + + ]: 63672 : it != d_ext_func_terms.end();
366 : 52365 : ++it)
367 : : {
368 : 52365 : terms.push_back((*it).first);
369 : : }
370 : 11307 : }
371 : :
372 : 0 : bool ExtTheory::hasActiveTerm() const { return !d_has_extf.get().isNull(); }
373 : :
374 : 598281 : bool ExtTheory::isActive(Node n) const
375 : : {
376 : 598281 : ExtReducedId rid = ExtReducedId::UNKNOWN;
377 : 598281 : return isActive(n, rid);
378 : : }
379 : :
380 : 598281 : bool ExtTheory::isActive(Node n, ExtReducedId& rid) const
381 : : {
382 : 598281 : NodeBoolMap::const_iterator it = d_ext_func_terms.find(n);
383 [ + - ]: 598281 : if (it != d_ext_func_terms.end())
384 : : {
385 [ + - ]: 598281 : if ((*it).second)
386 : : {
387 : 598281 : return !isContextIndependentInactive(n, rid);
388 : : }
389 : 0 : NodeExtReducedIdMap::const_iterator itr = d_extfExtReducedIdMap.find(n);
390 : 0 : Assert(itr != d_extfExtReducedIdMap.end());
391 : 0 : rid = itr->second;
392 : 0 : return false;
393 : : }
394 : 0 : return false;
395 : : }
396 : :
397 : : // get active
398 : 269212 : std::vector<Node> ExtTheory::getActive() const
399 : : {
400 : 269212 : std::vector<Node> active;
401 : 1685630 : for (NodeBoolMap::iterator it = d_ext_func_terms.begin();
402 [ + + ]: 1685630 : it != d_ext_func_terms.end();
403 : 1416420 : ++it)
404 : : {
405 : : // if not already reduced
406 [ + + ][ + - ]: 1416420 : if ((*it).second && !isContextIndependentInactive((*it).first))
[ + + ][ + + ]
[ - - ]
407 : : {
408 : 1161160 : active.push_back((*it).first);
409 : : }
410 : : }
411 : 269212 : return active;
412 : : }
413 : :
414 : 32040 : std::vector<Node> ExtTheory::getActive(Kind k) const
415 : : {
416 : 32040 : std::vector<Node> active;
417 : 82392 : for (NodeBoolMap::iterator it = d_ext_func_terms.begin();
418 [ + + ]: 82392 : it != d_ext_func_terms.end();
419 : 50352 : ++it)
420 : : {
421 : : // if not already reduced
422 [ + + ]: 59952 : if ((*it).first.getKind() == k && (*it).second
423 [ + + ][ + - ]: 110304 : && !isContextIndependentInactive((*it).first))
[ + + ][ + + ]
[ - - ]
424 : : {
425 : 3707 : active.push_back((*it).first);
426 : : }
427 : : }
428 : 32040 : return active;
429 : : }
430 : :
431 : 522 : std::shared_ptr<ProofNode> ExtTheory::getProofFor(Node fact)
432 : : {
433 : 1566 : CDProof proof(d_env);
434 : 1044 : std::vector<Node> antec;
435 : 1044 : Node conc = fact;
436 [ + - ]: 522 : if (conc.getKind() == Kind::IMPLIES)
437 : : {
438 [ + + ]: 522 : if (conc[0].getKind() == Kind::AND)
439 : : {
440 : 72 : antec.insert(antec.end(), conc[0].begin(), conc[0].end());
441 : : }
442 : : else
443 : : {
444 : 450 : antec.push_back(conc[0]);
445 : : }
446 : 522 : conc = conc[1];
447 : : }
448 : 522 : ProofChecker* pc = d_env.getProofNodeManager()->getChecker();
449 : : Node res =
450 : 2088 : pc->checkDebug(ProofRule::MACRO_SR_PRED_INTRO, antec, {conc}, conc);
451 [ - + ]: 522 : if (res.isNull())
452 : : {
453 : 0 : Assert(false) << "ExtTheory failed to prove " << fact;
454 : : return nullptr;
455 : : }
456 : 1044 : proof.addStep(conc, ProofRule::MACRO_SR_PRED_INTRO, antec, {conc});
457 [ + - ]: 522 : if (!antec.empty())
458 : : {
459 : 1044 : 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 : 522 : return proof.getProofFor(fact);
467 : : }
468 : :
469 : 189 : std::string ExtTheory::identify() const { return "ExtTheory"; }
470 : :
471 : : } // namespace theory
472 : : } // namespace cvc5::internal
|
