1 /********************* */
2 /*! \file extf_solver.h
4 ** Top contributors (to current version):
5 ** Andrew Reynolds, Andres Noetzli
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 Solver for extended functions of theory of strings.
15 #include "cvc4_private.h"
17 #ifndef CVC4__THEORY__STRINGS__EXTF_SOLVER_H
18 #define CVC4__THEORY__STRINGS__EXTF_SOLVER_H
23 #include "context/cdo.h"
24 #include "expr/node.h"
25 #include "theory/ext_theory.h"
26 #include "theory/strings/base_solver.h"
27 #include "theory/strings/core_solver.h"
28 #include "theory/strings/inference_manager.h"
29 #include "theory/strings/sequences_stats.h"
30 #include "theory/strings/skolem_cache.h"
31 #include "theory/strings/solver_state.h"
32 #include "theory/strings/strings_rewriter.h"
33 #include "theory/strings/theory_strings_preprocess.h"
40 * Non-static information about an extended function t. This information is
41 * constructed and used during the check extended function evaluation
44 * In the following, we refer to the "context-dependent simplified form"
45 * of a term t to be the result of rewriting t * sigma, where sigma is a
46 * derivable substitution in the current context. For example, the
47 * context-depdendent simplified form of contains( x++y, "a" ) given
48 * sigma = { x -> "" } is contains(y,"a").
53 ExtfInfoTmp() : d_modelActive(true) {}
55 * If s is in d_ctn[true] (resp. d_ctn[false]), then contains( t, s )
56 * (resp. ~contains( t, s )) holds in the current context. The vector
57 * d_ctnFrom is the explanation for why this holds. For example,
58 * if d_ctn[false][i] is "A", then d_ctnFrom[false][i] might be
59 * t = x ++ y AND x = "" AND y = "B".
61 std::map
<bool, std::vector
<Node
> > d_ctn
;
62 std::map
<bool, std::vector
<Node
> > d_ctnFrom
;
64 * The constant that t is entailed to be equal to, or null if none exist.
68 * The explanation for why t is equal to its context-dependent simplified
71 std::vector
<Node
> d_exp
;
72 /** This flag is false if t is reduced in the model. */
77 * Extended function solver for the theory of strings. This manages extended
78 * functions for the theory of strings using a combination of context-dependent
79 * simplification (Reynolds et al CAV 2017) and lazy reductions.
83 typedef context::CDHashSet
<Node
, NodeHashFunction
> NodeSet
;
86 ExtfSolver(context::Context
* c
,
87 context::UserContext
* u
,
91 StringsRewriter
& rewriter
,
95 SequencesStatistics
& statistics
);
99 * Called when a shared term is added to theory of strings, this registers
100 * n with the extended theory utility for context-depdendent simplification.
102 void addSharedTerm(TNode n
);
103 /** check extended functions evaluation
105 * This applies "context-dependent simplification" for all active extended
106 * function terms in this SAT context. This infers facts of the form:
107 * x = c => f( t1 ... tn ) = c'
108 * where the rewritten form of f( t1...tn ) { x |-> c } is c', and x = c
109 * is a (tuple of) equalities that are asserted in this SAT context, and
110 * f( t1 ... tn ) is a term from this SAT context.
112 * For more details, this is steps 4 when effort=0 and step 6 when
113 * effort=1 from Strategy 1 in Reynolds et al, "Scaling up DPLL(T) String
114 * Solvers using Context-Dependent Simplification", CAV 2017. When called with
115 * effort=3, we apply context-dependent simplification based on model values.
117 void checkExtfEval(int effort
);
118 /** check extended function reductions
120 * This adds "reduction" lemmas for each active extended function in this SAT
121 * context. These are generally lemmas of the form:
122 * F[t1...tn,k] ^ f( t1 ... tn ) = k
123 * where f( t1 ... tn ) is an active extended function, k is a fresh constant
124 * and F is a formula that constrains k based on the definition of f.
126 * For more details, this is step 7 from Strategy 1 in Reynolds et al,
127 * CAV 2017. We stratify this in practice, where calling this with effort=1
128 * reduces some of the "easier" extended functions, and effort=2 reduces
131 void checkExtfReductions(int effort
);
132 /** get preprocess module */
133 StringsPreprocess
* getPreprocess() { return &d_preproc
; }
136 * Get the current substitution for term n.
138 * This method returns a term that n is currently equal to in the current
139 * context. It updates exp to contain an explanation of why it is currently
140 * equal to that term.
142 * The argument effort determines what kind of term to return, either
143 * a constant in the equivalence class of n (effort=0), the normal form of
144 * n (effort=1,2) or the model value of n (effort>=3). The latter is only
145 * valid at LAST_CALL effort. If a term of the above form cannot be returned,
146 * then n itself is returned.
148 Node
getCurrentSubstitutionFor(int effort
, Node n
, std::vector
<Node
>& exp
);
149 /** get mapping from extended functions to their information
151 * This information is valid during a full effort check after a call to
154 const std::map
<Node
, ExtfInfoTmp
>& getInfo() const;
155 //---------------------------------- information about ExtTheory
156 /** Are there any active extended functions? */
157 bool hasExtendedFunctions() const;
159 * Get the function applications of kind k that are active in the current
160 * context (see ExtTheory::getActive).
162 std::vector
<Node
> getActive(Kind k
) const;
163 //---------------------------------- end information about ExtTheory
167 * This is called when an extended function application n is not able to be
168 * simplified by context-depdendent simplification, and we are resorting to
169 * expanding n to its full semantics via a reduction. This method returns
170 * true if it successfully reduced n by some reduction. If so, it either
171 * caches that the reduction lemma was sent, or marks n as reduced in this
172 * SAT-context. The argument effort has the same meaning as in
173 * checkExtfReductions.
175 bool doReduction(int effort
, Node n
);
176 /** check extended function inferences
178 * This function makes additional inferences for n that do not contribute
179 * to its reduction, but may help show a refutation.
181 * This function is called when the context-depdendent simplified form of
182 * n is nr. The argument "in" is the information object for n. The argument
183 * "effort" has the same meaning as the effort argument of checkExtfEval.
185 void checkExtfInference(Node n
, Node nr
, ExtfInfoTmp
& in
, int effort
);
186 /** The solver state object */
187 SolverState
& d_state
;
188 /** The (custom) output channel of the theory of strings */
189 InferenceManager
& d_im
;
190 /** Reference to the term registry of theory of strings */
191 TermRegistry
& d_termReg
;
192 /** The theory rewriter for this theory. */
193 StringsRewriter
& d_rewriter
;
194 /** reference to the base solver, used for certain queries */
195 BaseSolver
& d_bsolver
;
196 /** reference to the core solver, used for certain queries */
197 CoreSolver
& d_csolver
;
198 /** the extended theory object for the theory of strings */
200 /** Reference to the statistics for the theory of strings/sequences. */
201 SequencesStatistics
& d_statistics
;
202 /** preprocessing utility, for performing strings reductions */
203 StringsPreprocess d_preproc
;
204 /** Common constants */
208 std::vector
<Node
> d_emptyVec
;
209 /** map extended functions to the above information */
210 std::map
<Node
, ExtfInfoTmp
> d_extfInfoTmp
;
211 /** any non-reduced extended functions exist? */
212 context::CDO
<bool> d_hasExtf
;
213 /** extended functions inferences cache */
214 NodeSet d_extfInferCache
;
215 /** The set of extended functions we have sent reduction lemmas for */
219 } // namespace strings
220 } // namespace theory
223 #endif /* CVC4__THEORY__STRINGS__EXTF_SOLVER_H */