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) 20092021 by the authors listed in the file AUTHORS 
8 

** in the toplevel source directory and their institutional affiliations. 
9 

** All rights reserved. See the file COPYING in the toplevel 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 

* nonconstant 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 */ 