1 /********************* */
4 ** Top contributors (to current version):
5 ** Andrew Reynolds, Tim King, Mathias Preiner
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2020 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.\endverbatim
12 ** \brief Extended theory interface.
14 ** This implements a generic module, used by theory solvers, for performing
15 ** "context-dependent simplification", as described in Reynolds et al
16 ** "Designing Theory Solvers with Extensions", FroCoS 2017.
18 ** At a high level, this technique implements a generic inference scheme based
19 ** on the combination of SAT-context-dependent equality reasoning and
20 ** SAT-context-indepedent rewriting.
22 ** As a simple example, say
23 ** (1) TheoryStrings tells us that the following facts hold in the SAT context:
24 ** x = "A" ^ str.contains( str.++( x, z ), "B" ) = true.
25 ** (2) The Rewriter tells us that:
26 ** str.contains( str.++( "A", z ), "B" ) ----> str.contains( z, "B" ).
27 ** From this, this class may infer that the following lemma is T-valid:
28 ** x = "A" ^ str.contains( str.++( x, z ), "B" ) => str.contains( z, "B" )
31 #include "cvc4_private.h"
33 #ifndef CVC4__THEORY__EXT_THEORY_H
34 #define CVC4__THEORY__EXT_THEORY_H
39 #include "context/cdhashmap.h"
40 #include "context/cdhashset.h"
41 #include "context/context.h"
42 #include "expr/node.h"
43 #include "theory/theory.h"
49 * A callback class for ExtTheory below. This class is responsible for
50 * determining how to apply context-dependent simplification.
52 class ExtTheoryCallback
55 virtual ~ExtTheoryCallback() {}
57 * Get current substitution at an effort
58 * @param effort The effort identifier
59 * @param vars The variables to get a substitution for
60 * @param subs The terms to substitute for variables, in order. This vector
61 * should be updated to one the same size as vars.
62 * @param exp The map containing the explanation for each variable. Together
63 * with subs, we have that:
64 * ( exp[vars[i]] => vars[i] = subs[i] ) holds for all i
65 * @return true if any (non-identity) substitution was added to subs.
67 virtual bool getCurrentSubstitution(int effort
,
68 const std::vector
<Node
>& vars
,
69 std::vector
<Node
>& subs
,
70 std::map
<Node
, std::vector
<Node
> >& exp
);
73 * Is extended function n reduced? This returns true if n is reduced to a
74 * form that requires no further interaction from the theory.
76 * @param effort The effort identifier
77 * @param n The term to reduce
78 * @param on The original form of n, before substitution
79 * @param exp The explanation of on = n
80 * @return true if n is reduced.
82 virtual bool isExtfReduced(int effort
,
85 std::vector
<Node
>& exp
);
88 * Get reduction for node n.
89 * If return value is true, then n is reduced.
90 * If satDep is updated to false, then n is reduced independent of the
91 * SAT context (e.g. by a lemma that persists at this
92 * user-context level).
93 * If nr is non-null, then ( n = nr ) should be added as a lemma by caller,
94 * and return value of this method should be true.
96 virtual bool getReduction(int effort
, Node n
, Node
& nr
, bool& satDep
);
99 /** Extended theory class
101 * This class is used for constructing generic extensions to theory solvers.
102 * In particular, it provides methods for "context-dependent simplification"
103 * and "model-based refinement". For details, see Reynolds et al "Design
104 * Theory Solvers with Extensions", FroCoS 2017.
107 * (1) A set of "extended function" kinds (d_extf_kind),
108 * (2) A database of active/inactive extended function terms (d_ext_func_terms)
109 * that have been registered to the class.
111 * This class has methods doInferences/doReductions, which send out lemmas
112 * based on the current set of active extended function terms. The former
113 * is based on context-dependent simplification, where this class asks the
114 * underlying theory for a "derivable substitution", whereby extended functions
119 typedef context::CDHashMap
<Node
, bool, NodeHashFunction
> NodeBoolMap
;
120 typedef context::CDHashSet
<Node
, NodeHashFunction
> NodeSet
;
125 * If cacheEnabled is false, we do not cache results of getSubstitutedTerm.
127 ExtTheory(ExtTheoryCallback
& p
,
129 context::UserContext
* u
,
131 bool cacheEnabled
= false);
132 virtual ~ExtTheory() {}
133 /** Tells this class to treat terms with Kind k as extended functions */
134 void addFunctionKind(Kind k
) { d_extf_kind
[k
] = true; }
135 /** Is kind k treated as an extended function by this class? */
136 bool hasFunctionKind(Kind k
) const
138 return d_extf_kind
.find(k
) != d_extf_kind
.end();
142 * Registers term n with this class. Adds n to the set of extended function
143 * terms known by this class (d_ext_func_terms) if n is an extended function,
144 * that is, if addFunctionKind( n.getKind() ) was called.
146 void registerTerm(Node n
);
147 /** register all subterms of n with this class */
148 void registerTermRec(Node n
);
149 /** set n as reduced/inactive
151 * If satDep = false, then n remains inactive in the duration of this
154 void markReduced(Node n
, bool satDep
= true);
156 * Mark that a and b are congruent terms. This sets b inactive, and sets a to
157 * inactive if b was inactive.
159 void markCongruent(Node a
, Node b
);
160 /** getSubstitutedTerms
162 * input : effort, terms
163 * output : sterms, exp, where ( exp[i] => terms[i] = sterms[i] ) for all i.
165 * For each i, sterms[i] = term[i] * sigma for some "derivable substitution"
166 * sigma. We obtain derivable substitutions and their explanations via calls
167 * to the underlying theory's Theory::getCurrentSubstitution method. This
170 * If useCache is true, we cache the result in d_gst_cache. This is a context
171 * independent cache that can be cleared using clearCache() below.
173 void getSubstitutedTerms(int effort
,
174 const std::vector
<Node
>& terms
,
175 std::vector
<Node
>& sterms
,
176 std::vector
<std::vector
<Node
> >& exp
,
177 bool useCache
= false);
179 * Same as above, but for a single term. We return the substituted form of
180 * term and add its explanation to exp.
182 Node
getSubstitutedTerm(int effort
,
184 std::vector
<Node
>& exp
,
185 bool useCache
= false);
186 /** clear the cache for getSubstitutedTerm */
190 * This function performs "context-dependent simplification". The method takes
192 * effort: an identifier used to determine which terms we reduce and the
193 * form of the derivable substitution we will use,
194 * terms: the set of terms to simplify,
195 * batch: if this flag is true, we send lemmas for all terms; if it is false
196 * we send a lemma for the first applicable term.
198 * Sends rewriting lemmas of the form ( exp => t = c ) where t is in terms
199 * and c is a constant, c = rewrite( t*sigma ) where exp |= sigma. These
200 * lemmas are determined by asking the underlying theory for a derivable
201 * substitution (through getCurrentSubstitution with getSubstitutedTerm)
202 * above, applying this substitution to terms in terms, rewriting
203 * the result and checking with the theory whether the resulting term is
204 * in reduced form (isExtfReduced).
206 * This method adds the extended terms that are still active to nred, and
207 * returns true if and only if a lemma of the above form was sent.
209 bool doInferences(int effort
,
210 const std::vector
<Node
>& terms
,
211 std::vector
<Node
>& nred
,
214 * Calls the above function, where terms is getActive(), the set of currently
217 bool doInferences(int effort
, std::vector
<Node
>& nred
, bool batch
= true);
220 * This method has the same interface as doInferences. In contrast to
221 * doInfereces, this method will send reduction lemmas of the form ( t = t' )
222 * where t is in terms and t' is an equivalent reduced term.
224 bool doReductions(int effort
,
225 const std::vector
<Node
>& terms
,
226 std::vector
<Node
>& nred
,
228 bool doReductions(int effort
, std::vector
<Node
>& nred
, bool batch
= true);
230 /** get the set of all extended function terms from d_ext_func_terms */
231 void getTerms(std::vector
<Node
>& terms
);
232 /** is there at least one active extended function term? */
233 bool hasActiveTerm() const;
234 /** is n an active extended function term? */
235 bool isActive(Node n
) const;
236 /** get the set of active terms from d_ext_func_terms */
237 std::vector
<Node
> getActive() const;
238 /** get the set of active terms from d_ext_func_terms of kind k */
239 std::vector
<Node
> getActive(Kind k
) const;
242 /** returns the set of variable subterms of n */
243 static std::vector
<Node
> collectVars(Node n
);
244 /** is n context dependent inactive? */
245 bool isContextIndependentInactive(Node n
) const;
246 /** do inferences internal */
247 bool doInferencesInternal(int effort
,
248 const std::vector
<Node
>& terms
,
249 std::vector
<Node
>& nred
,
252 /** send lemma on the output channel */
253 bool sendLemma(Node lem
, bool preprocess
= false);
254 /** reference to the callback */
255 ExtTheoryCallback
& d_parent
;
256 /** Reference to the output channel we are using */
257 OutputChannel
& d_out
;
260 /** extended function terms, map to whether they are active */
261 NodeBoolMap d_ext_func_terms
;
263 * The set of terms from d_ext_func_terms that are SAT-context-independent
264 * inactive. For instance, a term t is SAT-context-independent inactive if
265 * a reduction lemma of the form t = t' was added in this user-context level.
267 NodeSet d_ci_inactive
;
269 * Watched term for checking if any non-reduced extended functions exist.
270 * This is an arbitrary active member of d_ext_func_terms.
272 context::CDO
<Node
> d_has_extf
;
273 /** the set of kinds we are treated as extended functions */
274 std::map
<Kind
, bool> d_extf_kind
;
275 /** information for each term in d_ext_func_terms */
279 /** all variables in this term */
280 std::vector
<Node
> d_vars
;
282 std::map
<Node
, ExtfInfo
> d_extf_info
;
284 // cache of all lemmas sent
287 /** whether we enable caching for getSubstitutedTerm */
289 /** Substituted term info */
293 /** the substituted term */
295 /** an explanation */
296 std::vector
<Node
> d_exp
;
299 * This maps an (effort, term) to the information above. It is used as a
300 * cache for getSubstitutedTerm when d_cacheEnabled is true.
302 std::map
<int, std::map
<Node
, SubsTermInfo
> > d_gst_cache
;
305 } /* CVC4::theory namespace */
306 } /* CVC4 namespace */
308 #endif /* CVC4__THEORY__EXT_THEORY_H */