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) 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 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 nonempty 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 (nonnull) 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 (nonempty) 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 nonnull 
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 stringlike 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 */ 