Branch data Line data Source code
1 : : /******************************************************************************
2 : : * Top contributors (to current version):
3 : : * Andrew Reynolds, Tim King, Mathias Preiner
4 : : *
5 : : * This file is part of the cvc5 project.
6 : : *
7 : : * Copyright (c) 2009-2025 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 : : * At a high level, this technique implements a generic inference scheme based
20 : : * on the combination of SAT-context-dependent equality reasoning and
21 : : * SAT-context-indepedent rewriting.
22 : : *
23 : : * As a simple example, say
24 : : * (1) TheoryStrings tells us that the following facts hold in the SAT context:
25 : : * x = "A" ^ str.contains( str.++( x, z ), "B" ) = true.
26 : : * (2) The Rewriter tells us that:
27 : : * str.contains( str.++( "A", z ), "B" ) ----> str.contains( z, "B" ).
28 : : * From this, this class may infer that the following lemma is T-valid:
29 : : * x = "A" ^ str.contains( str.++( x, z ), "B" ) => str.contains( z, "B" )
30 : : */
31 : :
32 : : #include "cvc5_private.h"
33 : :
34 : : #ifndef CVC5__THEORY__EXT_THEORY_H
35 : : #define CVC5__THEORY__EXT_THEORY_H
36 : :
37 : : #include <map>
38 : :
39 : : #include "context/cdhashmap.h"
40 : : #include "context/cdhashset.h"
41 : : #include "context/cdo.h"
42 : : #include "context/context.h"
43 : : #include "expr/node.h"
44 : : #include "proof/proof.h"
45 : : #include "smt/env_obj.h"
46 : : #include "theory/theory_inference_manager.h"
47 : :
48 : : namespace cvc5::internal {
49 : : namespace theory {
50 : :
51 : : class OutputChannel;
52 : :
53 : : /** Reasons for why a term was marked reduced */
54 : : enum class ExtReducedId
55 : : {
56 : : // the extended function is not marked reduced
57 : : NONE,
58 : : // the extended function substitutes+rewrites to a constant
59 : : SR_CONST,
60 : : // the extended function was reduced by the callback
61 : : REDUCTION,
62 : : // the extended function substitutes+rewrites to zero
63 : : ARITH_SR_ZERO,
64 : : // the extended function substitutes+rewrites to a linear (non-zero) term
65 : : ARITH_SR_LINEAR,
66 : : // an extended string function substitutes+rewrites to a constant
67 : : STRINGS_SR_CONST,
68 : : // a negative str.contains was reduced to a disequality
69 : : STRINGS_NEG_CTN_DEQ,
70 : : // a str.contains was subsumed by another based on a decomposition
71 : : STRINGS_CTN_DECOMPOSE,
72 : : // reduced via an intersection inference
73 : : STRINGS_REGEXP_INTER,
74 : : // subsumed due to intersection reasoning
75 : : STRINGS_REGEXP_INTER_SUBSUME,
76 : : // subsumed due to RE inclusion reasoning for positive memberships
77 : : STRINGS_REGEXP_INCLUDE,
78 : : // subsumed due to RE inclusion reasoning for negative memberships
79 : : STRINGS_REGEXP_INCLUDE_NEG,
80 : : // satisfied due to normal form substitution into re memberships
81 : : STRINGS_REGEXP_RE_SYM_NF,
82 : : // satisfied due to partial derivative computation
83 : : STRINGS_REGEXP_PDERIVATIVE,
84 : : // reduction for seq.nth over seq.rev
85 : : STRINGS_NTH_REV,
86 : : // the reason for the reduction is unknown
87 : : UNKNOWN,
88 : : };
89 : : /**
90 : : * Converts an ext reduced identifier to a string.
91 : : *
92 : : * @param id The ext reduced identifier
93 : : * @return The name of the ext reduced identifier
94 : : */
95 : : const char* toString(ExtReducedId id);
96 : :
97 : : /**
98 : : * Writes an ext reduced identifier to a stream.
99 : : *
100 : : * @param out The stream to write to
101 : : * @param id The ext reduced identifier to write to the stream
102 : : * @return The stream
103 : : */
104 : : std::ostream& operator<<(std::ostream& out, ExtReducedId id);
105 : :
106 : : /**
107 : : * A callback class for ExtTheory below. This class is responsible for
108 : : * determining how to apply context-dependent simplification.
109 : : */
110 : : class ExtTheoryCallback
111 : : {
112 : : public:
113 : 83097 : virtual ~ExtTheoryCallback() {}
114 : : /*
115 : : * Get current substitution at an effort
116 : : * @param effort The effort identifier
117 : : * @param vars The variables to get a substitution for
118 : : * @param subs The terms to substitute for variables, in order. This vector
119 : : * should be updated to one the same size as vars.
120 : : * @param exp The map containing the explanation for each variable. Together
121 : : * with subs, we have that:
122 : : * ( exp[vars[i]] => vars[i] = subs[i] ) holds for all i
123 : : * @return true if any (non-identity) substitution was added to subs.
124 : : */
125 : : virtual bool getCurrentSubstitution(int effort,
126 : : const std::vector<Node>& vars,
127 : : std::vector<Node>& subs,
128 : : std::map<Node, std::vector<Node> >& exp);
129 : :
130 : : /*
131 : : * Is extended function n reduced? This returns true if n is reduced to a
132 : : * form that requires no further interaction from the theory.
133 : : *
134 : : * @param effort The effort identifier
135 : : * @param n The term to reduce
136 : : * @param on The original form of n, before substitution
137 : : * @param exp The explanation of on = n
138 : : * @param id If this method returns true, then id is updated to the reason
139 : : * why n was reduced.
140 : : * @return true if n is reduced.
141 : : */
142 : : virtual bool isExtfReduced(
143 : : int effort, Node n, Node on, std::vector<Node>& exp, ExtReducedId& id);
144 : :
145 : : /**
146 : : * Get reduction for node n.
147 : : * If return value is true, then n is reduced.
148 : : * If satDep is updated to false, then n is reduced independent of the
149 : : * SAT context (e.g. by a lemma that persists at this
150 : : * user-context level).
151 : : * If nr is non-null, then ( n = nr ) should be added as a lemma by caller,
152 : : * and return value of this method should be true.
153 : : */
154 : : virtual bool getReduction(int effort, Node n, Node& nr, bool& satDep);
155 : : };
156 : :
157 : : /** Extended theory class
158 : : *
159 : : * This class is used for constructing generic extensions to theory solvers.
160 : : * In particular, it provides methods for "context-dependent simplification"
161 : : * and "model-based refinement". For details, see Reynolds et al "Design
162 : : * Theory Solvers with Extensions", FroCoS 2017.
163 : : *
164 : : * It maintains:
165 : : * (1) A set of "extended function" kinds (d_extf_kind),
166 : : * (2) A database of active/inactive extended function terms (d_ext_func_terms)
167 : : * that have been registered to the class.
168 : : *
169 : : * This class has methods doInferences/doReductions, which send out lemmas
170 : : * based on the current set of active extended function terms. The former
171 : : * is based on context-dependent simplification, where this class asks the
172 : : * underlying theory for a "derivable substitution", whereby extended functions
173 : : * may be reducable.
174 : : */
175 : : class ExtTheory : protected EnvObj, public ProofGenerator
176 : : {
177 : : using NodeBoolMap = context::CDHashMap<Node, bool>;
178 : : using NodeExtReducedIdMap = context::CDHashMap<Node, ExtReducedId>;
179 : : using NodeSet = context::CDHashSet<Node>;
180 : :
181 : : public:
182 : : /** constructor
183 : : *
184 : : * If cacheEnabled is false, we do not cache results of getSubstitutedTerm.
185 : : */
186 : : ExtTheory(Env& env, ExtTheoryCallback& p, TheoryInferenceManager& im);
187 : 83097 : virtual ~ExtTheory() {}
188 : : /** Tells this class to treat terms with Kind k as extended functions */
189 : 1211980 : void addFunctionKind(Kind k) { d_extf_kind[k] = true; }
190 : : /** Is kind k treated as an extended function by this class? */
191 : 887113 : bool hasFunctionKind(Kind k) const
192 : : {
193 : 887113 : return d_extf_kind.find(k) != d_extf_kind.end();
194 : : }
195 : : /** register term
196 : : *
197 : : * Registers term n with this class. Adds n to the set of extended function
198 : : * terms known by this class (d_ext_func_terms) if n is an extended function,
199 : : * that is, if addFunctionKind( n.getKind() ) was called.
200 : : */
201 : : void registerTerm(Node n);
202 : : /** set n as reduced/inactive
203 : : *
204 : : * If satDep = false, then n remains inactive in the duration of this
205 : : * user-context level
206 : : */
207 : : void markInactive(Node n, ExtReducedId rid, bool satDep = true);
208 : : /** getSubstitutedTerms
209 : : *
210 : : * input : effort, terms
211 : : * output : sterms, exp, where ( exp[i] => terms[i] = sterms[i] ) for all i.
212 : : *
213 : : * For each i, sterms[i] = term[i] * sigma for some "derivable substitution"
214 : : * sigma. We obtain derivable substitutions and their explanations via calls
215 : : * to the underlying theory's Theory::getCurrentSubstitution method.
216 : : */
217 : : void getSubstitutedTerms(int effort,
218 : : const std::vector<Node>& terms,
219 : : std::vector<Node>& sterms,
220 : : std::vector<std::vector<Node> >& exp);
221 : : /** doInferences
222 : : *
223 : : * This function performs "context-dependent simplification". The method takes
224 : : * as input:
225 : : * effort: an identifier used to determine which terms we reduce and the
226 : : * form of the derivable substitution we will use,
227 : : * terms: the set of terms to simplify
228 : : *
229 : : * Sends rewriting lemmas of the form ( exp => t = c ) where t is in terms
230 : : * and c is a constant, c = rewrite( t*sigma ) where exp |= sigma. These
231 : : * lemmas are determined by asking the underlying theory for a derivable
232 : : * substitution (through getCurrentSubstitution with getSubstitutedTerm)
233 : : * above, applying this substitution to terms in terms, rewriting
234 : : * the result and checking with the theory whether the resulting term is
235 : : * in reduced form (isExtfReduced).
236 : : *
237 : : * This method adds the extended terms that are still active to nred, and
238 : : * returns true if and only if a lemma of the above form was sent.
239 : : */
240 : : bool doInferences(int effort,
241 : : const std::vector<Node>& terms,
242 : : std::vector<Node>& nred);
243 : : /**
244 : : * Calls the above function, where terms is getActive(), the set of currently
245 : : * active terms.
246 : : */
247 : : bool doInferences(int effort, std::vector<Node>& nred);
248 : :
249 : : /** get the set of all extended function terms from d_ext_func_terms */
250 : : void getTerms(std::vector<Node>& terms);
251 : : /** is there at least one active extended function term? */
252 : : bool hasActiveTerm() const;
253 : : /** is n an active extended function term? */
254 : : bool isActive(Node n) const;
255 : : /**
256 : : * Same as above, but rid is updated to the reason if this method returns
257 : : * false.
258 : : */
259 : : bool isActive(Node n, ExtReducedId& rid) const;
260 : : /** get the set of active terms from d_ext_func_terms */
261 : : std::vector<Node> getActive() const;
262 : : /** get the set of active terms from d_ext_func_terms of kind k */
263 : : std::vector<Node> getActive(Kind k) const;
264 : :
265 : : /**
266 : : * Get proof for a lemma sent via this class, which is of the form
267 : : * (t1 = s1 ^ ... ^ tn = sn) => (t = s)
268 : : * where the conclusion can be shown via substitution + rewriting.
269 : : */
270 : : std::shared_ptr<ProofNode> getProofFor(Node fact) override;
271 : : /** identify */
272 : : std::string identify() const override;
273 : :
274 : : private:
275 : : /** returns the set of variable subterms of n */
276 : : static std::vector<Node> collectVars(Node n);
277 : : /** is n context dependent inactive? */
278 : : bool isContextIndependentInactive(Node n) const;
279 : : /**
280 : : * Same as above, but rid is updated to the reason if this method returns
281 : : * true.
282 : : */
283 : : bool isContextIndependentInactive(Node n, ExtReducedId& rid) const;
284 : : /** do inferences internal */
285 : : bool doInferencesInternal(int effort,
286 : : const std::vector<Node>& terms,
287 : : std::vector<Node>& nred);
288 : : /** send lemma on the output channel */
289 : : bool sendLemma(TrustNode lem, InferenceId id);
290 : : /** reference to the callback */
291 : : ExtTheoryCallback& d_parent;
292 : : /** inference manager used to send lemmas */
293 : : TheoryInferenceManager& d_im;
294 : : /** the true node */
295 : : Node d_true;
296 : : /** extended function terms, map to whether they are active */
297 : : NodeBoolMap d_ext_func_terms;
298 : : /** mapping to why extended function terms are inactive */
299 : : NodeExtReducedIdMap d_extfExtReducedIdMap;
300 : : /**
301 : : * The set of terms from d_ext_func_terms that are SAT-context-independent
302 : : * inactive. For instance, a term t is SAT-context-independent inactive if
303 : : * a reduction lemma of the form t = t' was added in this user-context level.
304 : : */
305 : : NodeExtReducedIdMap d_ci_inactive;
306 : : /**
307 : : * Watched term for checking if any non-reduced extended functions exist.
308 : : * This is an arbitrary active member of d_ext_func_terms.
309 : : */
310 : : context::CDO<Node> d_has_extf;
311 : : /** the set of kinds we are treated as extended functions */
312 : : std::map<Kind, bool> d_extf_kind;
313 : : /** information for each term in d_ext_func_terms */
314 : : class ExtfInfo
315 : : {
316 : : public:
317 : : /** all variables in this term */
318 : : std::vector<Node> d_vars;
319 : : };
320 : : std::map<Node, ExtfInfo> d_extf_info;
321 : :
322 : : // cache of all lemmas sent
323 : : NodeSet d_lemmas;
324 : : };
325 : :
326 : : } // namespace theory
327 : : } // namespace cvc5::internal
328 : :
329 : : #endif /* CVC5__THEORY__EXT_THEORY_H */
|
