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

Line Exec Source
1
/*********************                                                        */
2
/*! \file normal_form.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Andres Noetzli, 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 Normal form datastructure for the theory of strings.
13
 **/
14
15
#include "cvc4_private.h"
16
17
#ifndef CVC4__THEORY__STRINGS__NORMAL_FORM_H
18
#define CVC4__THEORY__STRINGS__NORMAL_FORM_H
19
20
#include <map>
21
#include <vector>
22
#include "expr/node.h"
23
24
namespace CVC4 {
25
namespace theory {
26
namespace strings {
27
28
/** normal forms
29
 *
30
 * Stores information regarding the "normal form" of terms t in the current
31
 * context. Normal forms can be associated with terms, or with string
32
 * equivalence classes. For the latter, the normal form of an equivalence class
33
 * exists if exactly one unique normal form is associated to a subset of its
34
 * terms.
35
 *
36
 * In the following we use example where assertions are:
37
 *   { x = y, y = z, y = u ++ v, u = u1 ++ u2 }
38
 * and equivalence class [x] = { x, y, z, u ++ v }, whose normal form is
39
 *   (u1, u2, v)
40
 */
41
1096884
class NormalForm
42
{
43
 public:
44
394000
  NormalForm() : d_isRev(false) {}
45
  /**
46
   * The "base" of the normal form. This is some term in the equivalence
47
   * class of t that the normal form is based on. This is an arbitrary term
48
   * which is used as the reference point for explanations. In the above
49
   * running example, let us assume the base of [x] is y.
50
   */
51
  Node d_base;
52
  /** the normal form, (u1, u2, v), in the above example */
53
  std::vector<Node> d_nf;
54
  /** is the normal form d_nf stored in reverse order? */
55
  bool d_isRev;
56
  /**
57
   * The explanation for the normal form, this is a set of literals such that
58
   *   d_exp => d_base = d_nf
59
   * In the above example, this is the set of equalities
60
   *   { y = u ++ v, u = u1 ++ u2 }
61
   * If u ++ v was chosen as the base, then the first literal could be omitted.
62
   */
63
  std::vector<Node> d_exp;
64
  /**
65
   * Map from literals in the vector d_exp to integers indicating indices in
66
   * d_nf for which that literal L is relevant for explaining d_base = d_nf.
67
   *
68
   * In particular:
69
   * - false maps to an (ideally maximal) index relative to the start of d_nf
70
   * such that L is required for explaining why d_base has a prefix that
71
   * includes the term at that index,
72
   * - true maps to an (ideally maximal) index relative to the end of d_nf
73
   * such that L is required for explaining why d_base has a suffix that
74
   * includes the term at that index.
75
   * We call these the forward and backwards dependency indices.
76
   *
77
   * In the above example:
78
   *   y = u ++ v   : false -> 0, true -> 0
79
   *   u = u1 ++ u2 : false -> 0, true -> 1
80
   * When explaining y = u1 ++ u2 ++ v, the equality y = u ++ v is required
81
   * for explaining any prefix/suffix of y and its normal form. More
82
   * interestingly, the equality u = u1 ++ u2 is not required for explaining
83
   * that v is a suffix of y, since its reverse index in this map is 1,
84
   * indicating that "u2" is the first position in u1 ++ u2 ++ v that it is
85
   * required for explaining.
86
   *
87
   * This information is used to minimize explanations when conflicts arise,
88
   * thereby strengthening conflict clauses and lemmas.
89
   *
90
   * For example, say u ++ v = y = x = u ++ w and w and v are distinct
91
   * constants, using this dependency information, we could construct a
92
   * conflict:
93
   *   x = y ^ y = u ++ v ^ x = u ++ w
94
   * that does not include u = u1 ++ u2, because the conflict only pertains
95
   * to the last position in the normal form of y.
96
   */
97
  std::map<Node, std::map<bool, unsigned> > d_expDep;
98
  /** initialize
99
   *
100
   * Initialize the normal form with base node base. If base is not the empty
101
   * string, then d_nf is set to the singleton list containing base, otherwise
102
   * d_nf is empty.
103
   */
104
  void init(Node base);
105
  /** reverse the content of normal form d_nf
106
   *
107
   * This operation is done in contexts where the normal form is being scanned
108
   * in reverse order.
109
   */
110
  void reverse();
111
  /** split constant
112
   *
113
   * Splits the constant in d_nf at index to constants c1 and c2.
114
   *
115
   * Notice this function depends on whether the normal form has been reversed
116
   * d_isRev, as this impacts how the dependency indices are updated.
117
   */
118
  void splitConstant(unsigned index, Node c1, Node c2);
119
  /** add to explanation
120
   *
121
   * This adds exp to the explanation vector d_exp with new forward and
122
   * backwards dependency indices new_val and new_rev_val.
123
   *
124
   * If exp already has dependencies, we update the forward dependency
125
   * index to the minimum of the previous value and the new value, and
126
   * similarly update the backwards dependency index to the maximum.
127
   */
128
  void addToExplanation(Node exp, unsigned new_val, unsigned new_rev_val);
129
  /** get explanation
130
   *
131
   * This gets the explanation for the prefix (resp. suffix) of the normal
132
   * form up to index when d_isRev is false (resp. true). In particular;
133
   *
134
   * If index is -1, then this method adds all literals in d_exp to curr_exp.
135
   *
136
   * If index>=0, this method adds all literals in d_exp to curr_exp whose
137
   * forward (resp. backwards) dependency index is less than index
138
   * when isRev is false (resp. true).
139
   */
140
  void getExplanation(int index, std::vector<Node>& curr_exp);
141
142
  /**
143
   * Collects the constant string starting at a given index, i.e. concatenates
144
   * all the consecutive constant strings. If the normal form is reverse order,
145
   * this function searches backwards but the result will be in the original
146
   * order.
147
   *
148
   * @param index The index to start at, updated to point to the first
149
   *              non-constant component of the normal form or set equal to the
150
   *              size of the normal form if the remainder is all constants
151
   * @return The combined string constants
152
   */
153
  Node collectConstantStringAt(size_t& index);
154
155
  /** get explanation for prefix equality
156
   *
157
   * This adds to curr_exp the reason why the prefix of nfi up to index index_i
158
   * is equivalent to the prefix of nfj up to index_j. The values of
159
   * nfi.d_isRev and nfj.d_isRev affect how dependency indices are updated
160
   * during this call.
161
   */
162
  static void getExplanationForPrefixEq(NormalForm& nfi,
163
                                        NormalForm& nfj,
164
                                        int index_i,
165
                                        int index_j,
166
                                        std::vector<Node>& curr_exp);
167
};
168
169
}  // namespace strings
170
}  // namespace theory
171
}  // namespace CVC4
172
173
#endif /* CVC4__THEORY__STRINGS__NORMAL_FORM_H */