GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/strings/theory_strings.h Lines: 32 32 100.0 %
Date: 2021-03-23 Branches: 69 132 52.3 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file theory_strings.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Tianyi Liang, Mathias Preiner
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 Theory of strings
13
 **
14
 ** Theory of strings.
15
 **/
16
17
#include "cvc4_private.h"
18
19
#ifndef CVC4__THEORY__STRINGS__THEORY_STRINGS_H
20
#define CVC4__THEORY__STRINGS__THEORY_STRINGS_H
21
22
#include <climits>
23
#include <deque>
24
25
#include "context/cdhashset.h"
26
#include "context/cdlist.h"
27
#include "expr/node_trie.h"
28
#include "theory/ext_theory.h"
29
#include "theory/strings/base_solver.h"
30
#include "theory/strings/core_solver.h"
31
#include "theory/strings/eager_solver.h"
32
#include "theory/strings/extf_solver.h"
33
#include "theory/strings/infer_info.h"
34
#include "theory/strings/inference_manager.h"
35
#include "theory/strings/normal_form.h"
36
#include "theory/strings/proof_checker.h"
37
#include "theory/strings/regexp_elim.h"
38
#include "theory/strings/regexp_operation.h"
39
#include "theory/strings/regexp_solver.h"
40
#include "theory/strings/sequences_stats.h"
41
#include "theory/strings/solver_state.h"
42
#include "theory/strings/strategy.h"
43
#include "theory/strings/strings_fmf.h"
44
#include "theory/strings/strings_rewriter.h"
45
#include "theory/strings/term_registry.h"
46
#include "theory/theory.h"
47
#include "theory/uf/equality_engine.h"
48
49
namespace CVC4 {
50
namespace theory {
51
namespace strings {
52
53
/**
54
 * A theory solver for strings. At a high level, the solver implements
55
 * techniques described in:
56
 * - Liang et al, CAV 2014,
57
 * - Reynolds et al, CAV 2017,
58
 * - Reynolds et al, IJCAR 2020.
59
 * Its rewriter is described in:
60
 * - Reynolds et al, CAV 2019.
61
 */
62
class TheoryStrings : public Theory {
63
  friend class InferenceManager;
64
  typedef context::CDHashSet<Node, NodeHashFunction> NodeSet;
65
  typedef context::CDHashSet<TypeNode, TypeNodeHashFunction> TypeNodeSet;
66
 public:
67
  TheoryStrings(context::Context* c,
68
                context::UserContext* u,
69
                OutputChannel& out,
70
                Valuation valuation,
71
                const LogicInfo& logicInfo,
72
                ProofNodeManager* pnm);
73
  ~TheoryStrings();
74
  //--------------------------------- initialization
75
  /** get the official theory rewriter of this theory */
76
  TheoryRewriter* getTheoryRewriter() override;
77
  /**
78
   * Returns true if we need an equality engine. If so, we initialize the
79
   * information regarding how it should be setup. For details, see the
80
   * documentation in Theory::needsEqualityEngine.
81
   */
82
  bool needsEqualityEngine(EeSetupInfo& esi) override;
83
  /** finish initialization */
84
  void finishInit() override;
85
  //--------------------------------- end initialization
86
  /** Identify this theory */
87
  std::string identify() const override;
88
  /** Explain */
89
  TrustNode explain(TNode literal) override;
90
  /** presolve */
91
  void presolve() override;
92
  /** shutdown */
93
8988
  void shutdown() override {}
94
  /** preregister term */
95
  void preRegisterTerm(TNode n) override;
96
  /** Expand definition */
97
  TrustNode expandDefinition(Node n) override;
98
  //--------------------------------- standard check
99
  /** Do we need a check call at last call effort? */
100
  bool needsCheckLastEffort() override;
101
  bool preNotifyFact(TNode atom,
102
                     bool pol,
103
                     TNode fact,
104
                     bool isPrereg,
105
                     bool isInternal) override;
106
  void notifyFact(TNode atom, bool pol, TNode fact, bool isInternal) override;
107
  /** Post-check, called after the fact queue of the theory is processed. */
108
  void postCheck(Effort level) override;
109
  //--------------------------------- end standard check
110
  /** propagate method */
111
  bool propagateLit(TNode literal);
112
  /** Conflict when merging two constants */
113
  void conflict(TNode a, TNode b);
114
  /** called when a new equivalence class is created */
115
  void eqNotifyNewClass(TNode t);
116
  /** preprocess rewrite */
117
  TrustNode ppRewrite(TNode atom, std::vector<SkolemLemma>& lems) override;
118
  /** Collect model values in m based on the relevant terms given by termSet */
119
  bool collectModelValues(TheoryModel* m,
120
                          const std::set<Node>& termSet) override;
121
122
 private:
123
  /** NotifyClass for equality engine */
124
8994
  class NotifyClass : public eq::EqualityEngineNotify {
125
  public:
126
8997
   NotifyClass(TheoryStrings& ts) : d_str(ts), d_eagerSolver(ts.d_eagerSolver)
127
   {
128
8997
   }
129
294369
   bool eqNotifyTriggerPredicate(TNode predicate, bool value) override
130
   {
131
588738
     Debug("strings") << "NotifyClass::eqNotifyTriggerPredicate(" << predicate
132
294369
                      << ", " << (value ? "true" : "false") << ")" << std::endl;
133
294369
     if (value)
134
     {
135
160833
       return d_str.propagateLit(predicate);
136
     }
137
133536
     return d_str.propagateLit(predicate.notNode());
138
    }
139
320531
    bool eqNotifyTriggerTermEquality(TheoryId tag,
140
                                     TNode t1,
141
                                     TNode t2,
142
                                     bool value) override
143
    {
144
320531
      Debug("strings") << "NotifyClass::eqNotifyTriggerTermMerge(" << tag << ", " << t1 << ", " << t2 << ")" << std::endl;
145
320531
      if (value) {
146
242426
        return d_str.propagateLit(t1.eqNode(t2));
147
      }
148
78105
      return d_str.propagateLit(t1.eqNode(t2).notNode());
149
    }
150
645
    void eqNotifyConstantTermMerge(TNode t1, TNode t2) override
151
    {
152
645
      Debug("strings") << "NotifyClass::eqNotifyConstantTermMerge(" << t1 << ", " << t2 << ")" << std::endl;
153
645
      d_str.conflict(t1, t2);
154
645
    }
155
83840
    void eqNotifyNewClass(TNode t) override
156
    {
157
83840
      Debug("strings") << "NotifyClass::eqNotifyNewClass(" << t << std::endl;
158
83840
      d_str.eqNotifyNewClass(t);
159
83840
    }
160
809569
    void eqNotifyMerge(TNode t1, TNode t2) override
161
    {
162
1619138
      Debug("strings") << "NotifyClass::eqNotifyMerge(" << t1 << ", " << t2
163
809569
                       << std::endl;
164
809569
      d_eagerSolver.eqNotifyMerge(t1, t2);
165
809569
    }
166
127964
    void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) override
167
    {
168
127964
      Debug("strings") << "NotifyClass::eqNotifyDisequal(" << t1 << ", " << t2 << ", " << reason << std::endl;
169
127964
      d_eagerSolver.eqNotifyDisequal(t1, t2, reason);
170
127964
    }
171
172
   private:
173
    /** The theory of strings object to notify */
174
    TheoryStrings& d_str;
175
    /** The eager solver of the theory of strings */
176
    EagerSolver& d_eagerSolver;
177
  };/* class TheoryStrings::NotifyClass */
178
  /** compute care graph */
179
  void computeCareGraph() override;
180
  /**
181
   * Are x and y shared terms that are not equal? This is used for constructing
182
   * the care graph in the above function.
183
   */
184
  bool areCareDisequal(TNode x, TNode y);
185
  /** Add care pairs */
186
  void addCarePairs(TNodeTrie* t1,
187
                    TNodeTrie* t2,
188
                    unsigned arity,
189
                    unsigned depth);
190
  /** Collect model info for type tn
191
   *
192
   * Assigns model values (in m) to all relevant terms of the string-like type
193
   * tn in the current context, which are stored in repSet. Furthermore,
194
   * col is a partition of repSet where equivalence classes are grouped into
195
   * sets having equal length, where these lengths are stored in lts.
196
   *
197
   * Returns false if a conflict is discovered while doing this assignment.
198
   */
199
  bool collectModelInfoType(
200
      TypeNode tn,
201
      const std::unordered_set<Node, NodeHashFunction>& repSet,
202
      std::vector<std::vector<Node> >& col,
203
      std::vector<Node>& lts,
204
      TheoryModel* m);
205
206
  /** assert pending fact
207
   *
208
   * This asserts atom with polarity to the equality engine of this class,
209
   * where exp is the explanation of why (~) atom holds.
210
   *
211
   * This call may trigger further initialization steps involving the terms
212
   * of atom, including calls to registerTerm.
213
   */
214
  void assertPendingFact(Node atom, bool polarity, Node exp);
215
  //-----------------------inference steps
216
  /** check register terms pre-normal forms
217
   *
218
   * This calls registerTerm(n,2) on all non-congruent strings in the
219
   * equality engine of this class.
220
   */
221
  void checkRegisterTermsPreNormalForm();
222
  /** check codes
223
   *
224
   * This inference schema ensures that constraints between str.code terms
225
   * are satisfied by models that correspond to extensions of the current
226
   * assignment. In particular, this method ensures that str.code can be
227
   * given an interpretation that is injective for string arguments with length
228
   * one. It may add lemmas of the form:
229
   *   str.code(x) == -1 V str.code(x) != str.code(y) V x == y
230
   */
231
  void checkCodes();
232
  /** check register terms for normal forms
233
   *
234
   * This calls registerTerm(str.++(t1, ..., tn ), 3) on the normal forms
235
   * (t1, ..., tn) of all string equivalence classes { s1, ..., sm } such that
236
   * there does not exist a term of the form str.len(si) in the current context.
237
   */
238
  void checkRegisterTermsNormalForms();
239
  //-----------------------end inference steps
240
  /** run the given inference step */
241
  void runInferStep(InferStep s, int effort);
242
  /** run strategy for effort e */
243
  void runStrategy(Theory::Effort e);
244
  /** print strings equivalence classes for debugging */
245
  std::string debugPrintStringsEqc();
246
  /** Commonly used constants */
247
  Node d_true;
248
  Node d_false;
249
  Node d_zero;
250
  Node d_one;
251
  Node d_neg_one;
252
  /** the cardinality of the alphabet */
253
  uint32_t d_cardSize;
254
  /** The notify class */
255
  NotifyClass d_notify;
256
  /**
257
   * Statistics for the theory of strings/sequences. All statistics for these
258
   * theories is collected in this object.
259
   */
260
  SequencesStatistics d_statistics;
261
  /** The solver state object */
262
  SolverState d_state;
263
  /** The eager solver */
264
  EagerSolver d_eagerSolver;
265
  /** The term registry for this theory */
266
  TermRegistry d_termReg;
267
  /** The extended theory callback */
268
  StringsExtfCallback d_extTheoryCb;
269
  /** Extended theory, responsible for context-dependent simplification. */
270
  ExtTheory d_extTheory;
271
  /** The (custom) output channel of the theory of strings */
272
  InferenceManager d_im;
273
  /** The theory rewriter for this theory. */
274
  StringsRewriter d_rewriter;
275
  /** The proof rule checker */
276
  StringProofRuleChecker d_sProofChecker;
277
  /**
278
   * The base solver, responsible for reasoning about congruent terms and
279
   * inferring constants for equivalence classes.
280
   */
281
  BaseSolver d_bsolver;
282
  /**
283
   * The core solver, responsible for reasoning about string concatenation
284
   * with length constraints.
285
   */
286
  CoreSolver d_csolver;
287
  /**
288
   * Extended function solver, responsible for reductions and simplifications
289
   * involving extended string functions.
290
   */
291
  ExtfSolver d_esolver;
292
  /** regular expression solver module */
293
  RegExpSolver d_rsolver;
294
  /** regular expression elimination module */
295
  RegExpElimination d_regexp_elim;
296
  /** Strings finite model finding decision strategy */
297
  StringsFmf d_stringsFmf;
298
  /** The representation of the strategy */
299
  Strategy d_strat;
300
};/* class TheoryStrings */
301
302
}/* CVC4::theory::strings namespace */
303
}/* CVC4::theory namespace */
304
}/* CVC4 namespace */
305
306
#endif /* CVC4__THEORY__STRINGS__THEORY_STRINGS_H */