GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/strings/extf_solver.h Lines: 4 4 100.0 %
Date: 2021-03-23 Branches: 1 2 50.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file extf_solver.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Andres Noetzli, Tim King
6
 ** This file is part of the CVC4 project.
7
 ** Copyright (c) 2009-2021 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
11
 **
12
 ** \brief Solver for extended functions of theory of strings.
13
 **/
14
15
#include "cvc4_private.h"
16
17
#ifndef CVC4__THEORY__STRINGS__EXTF_SOLVER_H
18
#define CVC4__THEORY__STRINGS__EXTF_SOLVER_H
19
20
#include <map>
21
#include <vector>
22
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"
34
35
namespace CVC4 {
36
namespace theory {
37
namespace strings {
38
39
/**
40
 * Non-static information about an extended function t. This information is
41
 * constructed and used during the check extended function evaluation
42
 * inference schema.
43
 *
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").
49
 */
50
245555
class ExtfInfoTmp
51
{
52
 public:
53
245555
  ExtfInfoTmp() : d_modelActive(true) {}
54
  /**
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".
60
   */
61
  std::map<bool, std::vector<Node> > d_ctn;
62
  std::map<bool, std::vector<Node> > d_ctnFrom;
63
  /**
64
   * The constant that t is entailed to be equal to, or null if none exist.
65
   */
66
  Node d_const;
67
  /**
68
   * The explanation for why t is equal to its context-dependent simplified
69
   * form.
70
   */
71
  std::vector<Node> d_exp;
72
  /** This flag is false if t is reduced in the model. */
73
  bool d_modelActive;
74
};
75
76
/**
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.
80
 */
81
class ExtfSolver
82
{
83
  typedef context::CDHashSet<Node, NodeHashFunction> NodeSet;
84
85
 public:
86
  ExtfSolver(SolverState& s,
87
             InferenceManager& im,
88
             TermRegistry& tr,
89
             StringsRewriter& rewriter,
90
             BaseSolver& bs,
91
             CoreSolver& cs,
92
             ExtTheory& et,
93
             SequencesStatistics& statistics);
94
  ~ExtfSolver();
95
  /** check extended functions evaluation
96
   *
97
   * This applies "context-dependent simplification" for all active extended
98
   * function terms in this SAT context. This infers facts of the form:
99
   *   x = c => f( t1 ... tn ) = c'
100
   * where the rewritten form of f( t1...tn ) { x |-> c } is c', and x = c
101
   * is a (tuple of) equalities that are asserted in this SAT context, and
102
   * f( t1 ... tn ) is a term from this SAT context.
103
   *
104
   * For more details, this is steps 4 when effort=0 and step 6 when
105
   * effort=1 from Strategy 1 in Reynolds et al, "Scaling up DPLL(T) String
106
   * Solvers using Context-Dependent Simplification", CAV 2017. When called with
107
   * effort=3, we apply context-dependent simplification based on model values.
108
   */
109
  void checkExtfEval(int effort);
110
  /** check extended function reductions
111
   *
112
   * This adds "reduction" lemmas for each active extended function in this SAT
113
   * context. These are generally lemmas of the form:
114
   *   F[t1...tn,k] ^ f( t1 ... tn ) = k
115
   * where f( t1 ... tn ) is an active extended function, k is a fresh constant
116
   * and F is a formula that constrains k based on the definition of f.
117
   *
118
   * For more details, this is step 7 from Strategy 1 in Reynolds et al,
119
   * CAV 2017. We stratify this in practice, where calling this with effort=1
120
   * reduces some of the "easier" extended functions, and effort=2 reduces
121
   * the rest.
122
   */
123
  void checkExtfReductions(int effort);
124
  /** get preprocess module */
125
  StringsPreprocess* getPreprocess() { return &d_preproc; }
126
127
  /**
128
   * Get the current substitution for term n.
129
   *
130
   * This method returns a term that n is currently equal to in the current
131
   * context. It updates exp to contain an explanation of why it is currently
132
   * equal to that term.
133
   *
134
   * The argument effort determines what kind of term to return, either
135
   * a constant in the equivalence class of n (effort=0), the normal form of
136
   * n (effort=1,2) or the model value of n (effort>=3). The latter is only
137
   * valid at LAST_CALL effort. If a term of the above form cannot be returned,
138
   * then n itself is returned.
139
   */
140
  Node getCurrentSubstitutionFor(int effort, Node n, std::vector<Node>& exp);
141
  /** get mapping from extended functions to their information
142
   *
143
   * This information is valid during a full effort check after a call to
144
   * checkExtfEval.
145
   */
146
  const std::map<Node, ExtfInfoTmp>& getInfo() const;
147
  //---------------------------------- information about ExtTheory
148
  /** Are there any active extended functions? */
149
  bool hasExtendedFunctions() const;
150
  /**
151
   * Get the function applications of kind k that are active in the current
152
   * context (see ExtTheory::getActive).
153
   */
154
  std::vector<Node> getActive(Kind k) const;
155
  //---------------------------------- end information about ExtTheory
156
 private:
157
  /** do reduction
158
   *
159
   * This is called when an extended function application n is not able to be
160
   * simplified by context-depdendent simplification, and we are resorting to
161
   * expanding n to its full semantics via a reduction. This method returns
162
   * true if it successfully reduced n by some reduction. If so, it either
163
   * caches that the reduction lemma was sent, or marks n as reduced in this
164
   * SAT-context. The argument effort has the same meaning as in
165
   * checkExtfReductions.
166
   */
167
  bool doReduction(int effort, Node n);
168
  /** check extended function inferences
169
   *
170
   * This function makes additional inferences for n that do not contribute
171
   * to its reduction, but may help show a refutation.
172
   *
173
   * This function is called when the context-depdendent simplified form of
174
   * n is nr. The argument "in" is the information object for n. The argument
175
   * "effort" has the same meaning as the effort argument of checkExtfEval.
176
   */
177
  void checkExtfInference(Node n, Node nr, ExtfInfoTmp& in, int effort);
178
  /** The solver state object */
179
  SolverState& d_state;
180
  /** The (custom) output channel of the theory of strings */
181
  InferenceManager& d_im;
182
  /** Reference to the term registry of theory of strings */
183
  TermRegistry& d_termReg;
184
  /** The theory rewriter for this theory. */
185
  StringsRewriter& d_rewriter;
186
  /** reference to the base solver, used for certain queries */
187
  BaseSolver& d_bsolver;
188
  /** reference to the core solver, used for certain queries */
189
  CoreSolver& d_csolver;
190
  /** the extended theory object for the theory of strings */
191
  ExtTheory& d_extt;
192
  /** Reference to the statistics for the theory of strings/sequences. */
193
  SequencesStatistics& d_statistics;
194
  /** preprocessing utility, for performing strings reductions */
195
  StringsPreprocess d_preproc;
196
  /** Common constants */
197
  Node d_true;
198
  Node d_false;
199
  /** Empty vector */
200
  std::vector<Node> d_emptyVec;
201
  /** map extended functions to the above information */
202
  std::map<Node, ExtfInfoTmp> d_extfInfoTmp;
203
  /** any non-reduced extended functions exist? */
204
  context::CDO<bool> d_hasExtf;
205
  /** extended functions inferences cache */
206
  NodeSet d_extfInferCache;
207
  /** The set of extended functions we have sent reduction lemmas for */
208
  NodeSet d_reduced;
209
};
210
211
/** An extended theory callback */
212
8994
class StringsExtfCallback : public ExtTheoryCallback
213
{
214
 public:
215
8997
  StringsExtfCallback() : d_esolver(nullptr) {}
216
  /**
217
   * Get current substitution based on the underlying extended function
218
   * solver.
219
   */
220
  bool getCurrentSubstitution(int effort,
221
                              const std::vector<Node>& vars,
222
                              std::vector<Node>& subs,
223
                              std::map<Node, std::vector<Node> >& exp) override;
224
  /** The extended function solver */
225
  ExtfSolver* d_esolver;
226
};
227
228
}  // namespace strings
229
}  // namespace theory
230
}  // namespace CVC4
231
232
#endif /* CVC4__THEORY__STRINGS__EXTF_SOLVER_H */