1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
|
/********************* */
/*! \file base_solver.h
** \verbatim
** Top contributors (to current version):
** Andrew Reynolds
** This file is part of the CVC4 project.
** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
** in the top-level source directory) and their institutional affiliations.
** All rights reserved. See the file COPYING in the top-level source
** directory for licensing information.\endverbatim
**
** \brief Base solver for term indexing and constant inference for the
** theory of strings.
**/
#include "cvc4_private.h"
#ifndef CVC4__THEORY__STRINGS__BASE_SOLVER_H
#define CVC4__THEORY__STRINGS__BASE_SOLVER_H
#include "context/cdhashset.h"
#include "context/cdlist.h"
#include "theory/strings/infer_info.h"
#include "theory/strings/inference_manager.h"
#include "theory/strings/normal_form.h"
#include "theory/strings/skolem_cache.h"
#include "theory/strings/solver_state.h"
namespace CVC4 {
namespace theory {
namespace strings {
/** The base solver for the theory of strings
*
* This implements techniques for inferring when terms are congruent in the
* current context, and techniques for inferring when equivalence classes
* are equivalent to constants.
*/
class BaseSolver
{
using NodeSet = context::CDHashSet<Node, NodeHashFunction>;
public:
BaseSolver(context::Context* c,
context::UserContext* u,
SolverState& s,
InferenceManager& im);
~BaseSolver();
//-----------------------inference steps
/** check initial
*
* This function initializes term indices for each strings function symbol.
* One key aspect of this construction is that concat terms are indexed by
* their list of non-empty components. For example, if x = "" is an equality
* asserted in this SAT context, then y ++ x ++ z may be indexed by (y,z).
* This method may infer various facts while building these term indices, for
* instance, based on congruence. An example would be inferring:
* y ++ x ++ z = y ++ z
* if both terms are registered in this SAT context.
*
* This function should be called as a first step of any strategy.
*/
void checkInit();
/** check constant equivalence classes
*
* This function infers whether CONCAT terms can be simplified to constants.
* For example, if x = "a" and y = "b" are equalities in the current SAT
* context, then we may infer x ++ "c" ++ y is equivalent to "acb". In this
* case, we infer the fact x ++ "c" ++ y = "acb".
*/
void checkConstantEquivalenceClasses();
//-----------------------end inference steps
//-----------------------query functions
/**
* Is n congruent to another term in the current context that has not been
* marked congruent? If so, we can ignore n.
*
* Note this and the functions in this block below are valid during a full
* effort check after a call to checkInit.
*/
bool isCongruent(Node n);
/**
* Get the constant that the equivalence class eqc is entailed to be equal
* to, or null if none exist.
*/
Node getConstantEqc(Node eqc);
/**
* Same as above, where the explanation for n = c is added to exp if c is
* the (non-null) return value of this function, where n is a term in the
* equivalence class of eqc.
*/
Node explainConstantEqc(Node n, Node eqc, std::vector<Node>& exp);
/**
* Get the set of equivalence classes of type string.
*/
const std::vector<Node>& getStringEqc() const;
//-----------------------end query functions
private:
/**
* A term index that considers terms modulo flattening and constant merging
* for concatenation terms.
*/
class TermIndex
{
public:
/** Add n to this trie
*
* A term is indexed by flattening arguments of concatenation terms,
* and replacing them by (non-empty) constants when possible, for example
* if n is (str.++ x y z) and x = "abc" and y = "" are asserted, then n is
* indexed by ("abc", z).
*
* index: the child of n we are currently processing,
* s : reference to solver state,
* er : the representative of the empty equivalence class.
*
* We store the vector of terms that n was indexed by in the vector c.
*/
Node add(TNode n,
unsigned index,
const SolverState& s,
Node er,
std::vector<Node>& c);
/** Clear this trie */
void clear() { d_children.clear(); }
/** The data at this node of the trie */
Node d_data;
/** The children of this node of the trie */
std::map<TNode, TermIndex> d_children;
};
/**
* This method is called as we are traversing the term index ti, where vecc
* accumulates the list of constants in the path to ti. If ti has a non-null
* data n, then we have inferred that d_data is equivalent to the
* constant specified by vecc.
*/
void checkConstantEquivalenceClasses(TermIndex* ti, std::vector<Node>& vecc);
/** The solver state object */
SolverState& d_state;
/** The (custom) output channel of the theory of strings */
InferenceManager& d_im;
/** Commonly used constants */
Node d_emptyString;
Node d_false;
/**
* A congruence class is a set of terms f( t1 ), ..., f( tn ) where
* t1 = ... = tn. Congruence classes are important since all but
* one of the above terms (the representative of the congruence class)
* can be ignored by the solver.
*
* This set contains a set of nodes that are not representatives of their
* congruence class. This set is used to skip reasoning about terms in
* various inference schemas implemnted by this class.
*/
NodeSet d_congruent;
/**
* The following three vectors are used for tracking constants that each
* equivalence class is entailed to be equal to.
* - The map d_eqcToConst maps (representatives) r of equivalence classes to
* the constant that that equivalence class is entailed to be equal to,
* - The term d_eqcToConstBase[r] is the term in the equivalence class r
* that is entailed to be equal to the constant d_eqcToConst[r],
* - The term d_eqcToConstExp[r] is the explanation of why
* d_eqcToConstBase[r] is equal to d_eqcToConst[r].
*
* For example, consider the equivalence class { r, x++"a"++y, x++z }, and
* assume x = "" and y = "bb" in the current context. We have that
* d_eqcToConst[r] = "abb",
* d_eqcToConstBase[r] = x++"a"++y
* d_eqcToConstExp[r] = ( x = "" AND y = "bb" )
*
* This information is computed during checkInit and is used during various
* inference schemas for deriving inferences.
*/
std::map<Node, Node> d_eqcToConst;
std::map<Node, Node> d_eqcToConstBase;
std::map<Node, Node> d_eqcToConstExp;
/** The list of equivalence classes of type string */
std::vector<Node> d_stringsEqc;
/** A term index for each function kind */
std::map<Kind, TermIndex> d_termIndex;
}; /* class BaseSolver */
} // namespace strings
} // namespace theory
} // namespace CVC4
#endif /* CVC4__THEORY__STRINGS__BASE_SOLVER_H */
|
