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

Line Exec Source
1
/*********************                                                        */
2
/*! \file base_solver.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Andres Noetzli, Mudathir Mohamed
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 Base solver for term indexing and constant inference for the
13
 ** theory of strings.
14
 **/
15
16
#include "cvc4_private.h"
17
18
#ifndef CVC4__THEORY__STRINGS__BASE_SOLVER_H
19
#define CVC4__THEORY__STRINGS__BASE_SOLVER_H
20
21
#include "context/cdhashset.h"
22
#include "context/cdlist.h"
23
#include "theory/strings/infer_info.h"
24
#include "theory/strings/inference_manager.h"
25
#include "theory/strings/normal_form.h"
26
#include "theory/strings/skolem_cache.h"
27
#include "theory/strings/solver_state.h"
28
29
namespace CVC4 {
30
namespace theory {
31
namespace strings {
32
33
/** The base solver for the theory of strings
34
 *
35
 * This implements techniques for inferring when terms are congruent in the
36
 * current context, and techniques for inferring when equivalence classes
37
 * are equivalent to constants.
38
 */
39
class BaseSolver
40
{
41
  using NodeSet = context::CDHashSet<Node, NodeHashFunction>;
42
43
 public:
44
  BaseSolver(SolverState& s, InferenceManager& im);
45
  ~BaseSolver();
46
47
  //-----------------------inference steps
48
  /** check initial
49
   *
50
   * This function initializes term indices for each strings function symbol.
51
   * One key aspect of this construction is that concat terms are indexed by
52
   * their list of non-empty components. For example, if x = "" is an equality
53
   * asserted in this SAT context, then y ++ x ++ z may be indexed by (y,z).
54
   * This method may infer various facts while building these term indices, for
55
   * instance, based on congruence. An example would be inferring:
56
   *   y ++ x ++ z = y ++ z
57
   * if both terms are registered in this SAT context.
58
   *
59
   * This function should be called as a first step of any strategy.
60
   */
61
  void checkInit();
62
  /** check constant equivalence classes
63
   *
64
   * This function infers whether CONCAT terms can be simplified to constants.
65
   * For example, if x = "a" and y = "b" are equalities in the current SAT
66
   * context, then we may infer x ++ "c" ++ y is equivalent to "acb". In this
67
   * case, we infer the fact x ++ "c" ++ y = "acb".
68
   */
69
  void checkConstantEquivalenceClasses();
70
  /** check cardinality
71
   *
72
   * This function checks whether a cardinality inference needs to be applied
73
   * to a set of equivalence classes. For details, see Step 5 of the proof
74
   * procedure from Liang et al, CAV 2014.
75
   */
76
  void checkCardinality();
77
  //-----------------------end inference steps
78
79
  //-----------------------query functions
80
  /**
81
   * Is n congruent to another term in the current context that has not been
82
   * marked congruent? If so, we can ignore n.
83
   *
84
   * Note this and the functions in this block below are valid during a full
85
   * effort check after a call to checkInit.
86
   */
87
  bool isCongruent(Node n);
88
  /**
89
   * Get the constant that the equivalence class eqc is entailed to be equal
90
   * to, or null if none exist.
91
   */
92
  Node getConstantEqc(Node eqc);
93
  /**
94
   * Same as above, where the explanation for n = c is added to exp if c is
95
   * the (non-null) return value of this function, where n is a term in the
96
   * equivalence class of eqc.
97
   */
98
  Node explainConstantEqc(Node n, Node eqc, std::vector<Node>& exp);
99
  /**
100
   * Same as above, for "best content" terms.
101
   */
102
  Node explainBestContentEqc(Node n, Node eqc, std::vector<Node>& exp);
103
  /**
104
   * Get the set of equivalence classes of type string.
105
   */
106
  const std::vector<Node>& getStringEqc() const;
107
  //-----------------------end query functions
108
109
 private:
110
  /**
111
   * The information that we associated with each equivalence class.
112
   *
113
   * Example 1. Consider the equivalence class { r, x++"a"++y, x++z }, and
114
   * assume x = "" and y = "bb" in the current context. We have that
115
   *   d_bestContent = "abb",
116
   *   d_base = x++"a"++y
117
   *   d_exp = ( x = "" AND y = "bb" )
118
   *
119
   * Example 2. Consider the equivalence class { r, x++"a"++w++y, x++z }, and
120
   * assume x = "" and y = "bb" in the current context. We have that
121
   *   d_bestContent = "a" ++ w ++ "bb",
122
   *   d_bestScore = 3
123
   *   d_base = x++"a"++w++y
124
   *   d_exp = ( x = "" AND y = "bb" )
125
   *
126
   * This information is computed during checkInit and is used during various
127
   * inference schemas for deriving inferences.
128
   */
129
756032
  struct BaseEqcInfo
130
  {
131
    /**
132
     * Either a constant or a concatentation of constants and variables that
133
     * this equivalence class is entailed to be equal to. If it is a
134
     * concatenation, this is the concatenation that is currently known to have
135
     * the highest score (see `d_bestScore`).
136
     */
137
    Node d_bestContent;
138
    /**
139
     * The sum of the number of characters in the string literals of
140
     * `d_bestContent`.
141
     */
142
    size_t d_bestScore;
143
    /**
144
     * The term in the equivalence class that is entailed to be equal to
145
     * `d_bestContent`.
146
     */
147
    Node d_base;
148
    /** This term explains why `d_bestContent` is equal to `d_base`. */
149
    Node d_exp;
150
  };
151
152
  /**
153
   * A term index that considers terms modulo flattening and constant merging
154
   * for concatenation terms.
155
   */
156
2236132
  class TermIndex
157
  {
158
   public:
159
    /** Add n to this trie
160
     *
161
     * A term is indexed by flattening arguments of concatenation terms,
162
     * and replacing them by (non-empty) constants when possible, for example
163
     * if n is (str.++ x y z) and x = "abc" and y = "" are asserted, then n is
164
     * indexed by ("abc", z).
165
     *
166
     * index: the child of n we are currently processing,
167
     * s : reference to solver state,
168
     * er : the representative of the empty equivalence class.
169
     *
170
     * We store the vector of terms that n was indexed by in the vector c.
171
     */
172
    Node add(TNode n,
173
             unsigned index,
174
             const SolverState& s,
175
             Node er,
176
             std::vector<Node>& c);
177
    /** Clear this trie */
178
    void clear() { d_children.clear(); }
179
    /** The data at this node of the trie */
180
    Node d_data;
181
    /** The children of this node of the trie */
182
    std::map<TNode, TermIndex> d_children;
183
  };
184
  /**
185
   * This method is called as we are traversing the term index ti, where vecc
186
   * accumulates the list of constants in the path to ti. If ti has a non-null
187
   * data n, then we have inferred that d_data is equivalent to the
188
   * constant specified by vecc.
189
   *
190
   * @param ti The term index for string concatenations
191
   * @param vecc The list of constants in the path to ti
192
   * @param ensureConst If true, require that each element in the path is
193
   *                    constant
194
   * @param isConst If true, the path so far only includes constants
195
   */
196
  void checkConstantEquivalenceClasses(TermIndex* ti,
197
                                       std::vector<Node>& vecc,
198
                                       bool ensureConst = true,
199
                                       bool isConst = true);
200
  /**
201
   * Check cardinality for type tn. This adds a lemma corresponding to
202
   * cardinality for terms of type tn, if applicable.
203
   *
204
   * @param tn The string-like type of terms we are considering,
205
   * @param cols The list of collections of equivalence classes. This is a
206
   * partition of all string equivalence classes, grouped by those with equal
207
   * lengths.
208
   * @param lts The length of each of the collections in cols.
209
   */
210
  void checkCardinalityType(TypeNode tn,
211
                            std::vector<std::vector<Node> >& cols,
212
                            std::vector<Node>& lts);
213
  /** The solver state object */
214
  SolverState& d_state;
215
  /** The (custom) output channel of the theory of strings */
216
  InferenceManager& d_im;
217
  /** Commonly used constants */
218
  Node d_emptyString;
219
  Node d_false;
220
  /**
221
   * A congruence class is a set of terms f( t1 ), ..., f( tn ) where
222
   * t1 = ... = tn. Congruence classes are important since all but
223
   * one of the above terms (the representative of the congruence class)
224
   * can be ignored by the solver.
225
   *
226
   * This set contains a set of nodes that are not representatives of their
227
   * congruence class. This set is used to skip reasoning about terms in
228
   * various inference schemas implemented by this class.
229
   */
230
  NodeSet d_congruent;
231
  /**
232
   * Maps equivalence classes to their info, see description of `BaseEqcInfo`
233
   * for more information.
234
   */
235
  std::map<Node, BaseEqcInfo> d_eqcInfo;
236
  /** The list of equivalence classes of type string */
237
  std::vector<Node> d_stringsEqc;
238
  /** A term index for each type, function kind pair */
239
  std::map<TypeNode, std::map<Kind, TermIndex> > d_termIndex;
240
  /** the cardinality of the alphabet */
241
  uint32_t d_cardSize;
242
}; /* class BaseSolver */
243
244
}  // namespace strings
245
}  // namespace theory
246
}  // namespace CVC4
247
248
#endif /* CVC4__THEORY__STRINGS__BASE_SOLVER_H */