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
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
|
/********************* */
/*! \file solver_state.h
** \verbatim
** Top contributors (to current version):
** Andrew Reynolds, Tianyi Liang, Morgan Deters
** This file is part of the CVC4 project.
** Copyright (c) 2009-2020 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 The solver state of the theory of strings
**/
#include "cvc4_private.h"
#ifndef CVC4__THEORY__STRINGS__SOLVER_STATE_H
#define CVC4__THEORY__STRINGS__SOLVER_STATE_H
#include <map>
#include "context/context.h"
#include "expr/node.h"
#include "theory/theory_model.h"
#include "theory/uf/equality_engine.h"
#include "theory/valuation.h"
#include "theory/strings/eqc_info.h"
namespace CVC4 {
namespace theory {
namespace strings {
/**
* Solver state for strings.
*
* The purpose of this class is track and provide query functions for the state
* of the assertions for the theory of strings. This includes:
* (1) Equality queries via the equality engine,
* (2) Whether the set of assertions is in conflict.
* (3) Equivalence class information as in the class above.
*/
class SolverState
{
typedef context::CDList<Node> NodeList;
public:
SolverState(context::Context* c,
context::UserContext* u,
Valuation& v);
~SolverState();
/**
* Finish initialize, ee is a pointer to the official equality engine
* of theory of strings.
*/
void finishInit(eq::EqualityEngine* ee);
/** Get the SAT context */
context::Context* getSatContext() const;
/** Get the user context */
context::UserContext* getUserContext() const;
//-------------------------------------- equality information
/**
* Get the representative of t in the equality engine of this class, or t
* itself if it is not registered as a term.
*/
Node getRepresentative(Node t) const;
/** Is t registered as a term in the equality engine of this class? */
bool hasTerm(Node a) const;
/**
* Are a and b equal according to the equality engine of this class? Also
* returns true if a and b are identical.
*/
bool areEqual(Node a, Node b) const;
/**
* Are a and b disequal according to the equality engine of this class? Also
* returns true if the representative of a and b are distinct constants.
*/
bool areDisequal(Node a, Node b) const;
/** get equality engine */
eq::EqualityEngine* getEqualityEngine() const;
/**
* Get the list of disequalities that are currently asserted to the equality
* engine.
*/
const context::CDList<Node>& getDisequalityList() const;
//-------------------------------------- end equality information
//-------------------------------------- notifications for equalities
/** called when a new equivalence class is created */
void eqNotifyNewClass(TNode t);
/** called when two equivalence classes merge */
void eqNotifyMerge(TNode t1, TNode t2);
/** called when two equivalence classes are made disequal */
void eqNotifyDisequal(TNode t1, TNode t2, TNode reason);
//-------------------------------------- end notifications for equalities
//------------------------------------------ conflicts
/**
* Set that the current state of the solver is in conflict. This should be
* called immediately after a call to conflict(...) on the output channel of
* the theory of strings.
*/
void setConflict();
/** Are we currently in conflict? */
bool isInConflict() const;
/** set pending conflict
*
* If conf is non-null, this is called when conf is a conjunction of literals
* that hold in the current context that are unsatisfiable. It is set as the
* "pending conflict" to be processed as a conflict lemma on the output
* channel of this class. It is not sent out immediately since it may require
* explanation from the equality engine, and may be called at any time, e.g.
* during a merge operation, when the equality engine is not in a state to
* provide explanations.
*/
void setPendingConflictWhen(Node conf);
/** get the pending conflict, or null if none exist */
Node getPendingConflict() const;
//------------------------------------------ end conflicts
/** get length with explanation
*
* If possible, this returns an arithmetic term that exists in the current
* context that is equal to the length of te, or otherwise returns the
* length of t. It adds to exp literals that hold in the current context that
* explain why that term is equal to the length of t. For example, if
* we have assertions:
* len( x ) = 5 ^ z = x ^ x = y,
* then getLengthExp( z, exp, y ) returns len( x ) and adds { z = x } to
* exp. On the other hand, getLengthExp( z, exp, x ) returns len( x ) and
* adds nothing to exp.
*/
Node getLengthExp(Node t, std::vector<Node>& exp, Node te);
/** shorthand for getLengthExp(t, exp, t) */
Node getLength(Node t, std::vector<Node>& exp);
/** explain non-empty
*
* This returns an explanation of why string-like term is non-empty in the
* current context, if such an explanation exists. Otherwise, this returns
* the null node.
*
* Note that an explanation is a (conjunction of) literals that currently hold
* in the equality engine.
*/
Node explainNonEmpty(Node s);
/**
* Is equal empty word? Returns true if s is equal to the empty word (of
* its type). If this method returns true, it updates emps to be that word.
* This is an optimization so that the relevant empty word does not need to
* be constructed to check if s is equal to the empty word.
*/
bool isEqualEmptyWord(Node s, Node& emps);
/**
* Get the above information for equivalence class eqc. If doMake is true,
* we construct a new information class if one does not exist. The term eqc
* should currently be a representative of the equality engine of this class.
*/
EqcInfo* getOrMakeEqcInfo(Node eqc, bool doMake = true);
/** Get pointer to the model object of the Valuation object */
TheoryModel* getModel() const;
/** add endpoints to eqc info
*
* This method is called when term t is the explanation for why equivalence
* class eqc may have a constant endpoint due to a concatentation term concat.
* For example, we may call this method on:
* t := (str.++ x y), concat := (str.++ x y), eqc
* for some eqc that is currently equal to t. Another example is:
* t := (str.in.re z (re.++ r s)), concat := (re.++ r s), eqc
* for some eqc that is currently equal to z.
*/
void addEndpointsToEqcInfo(Node t, Node concat, Node eqc);
/** Entailment check
*
* This calls entailmentCheck on the Valuation object of theory of strings.
*/
std::pair<bool, Node> entailmentCheck(options::TheoryOfMode mode, TNode lit);
/** Separate by length
*
* Separate the string representatives in argument n into a partition cols
* whose collections have equal length. The i^th vector in cols has length
* lts[i] for all elements in col. These vectors are furthmore separated
* by string-like type.
*/
void separateByLength(
const std::vector<Node>& n,
std::map<TypeNode, std::vector<std::vector<Node>>>& cols,
std::map<TypeNode, std::vector<Node>>& lts);
private:
/** Common constants */
Node d_zero;
/** Pointer to the SAT context object used by the theory of strings. */
context::Context* d_context;
/** Pointer to the user context object used by the theory of strings. */
context::UserContext* d_ucontext;
/** Pointer to equality engine of the theory of strings. */
eq::EqualityEngine* d_ee;
/**
* The (SAT-context-dependent) list of disequalities that have been asserted
* to the equality engine above.
*/
NodeList d_eeDisequalities;
/** Reference to the valuation of the theory of strings */
Valuation& d_valuation;
/** Are we in conflict? */
context::CDO<bool> d_conflict;
/** The pending conflict if one exists */
context::CDO<Node> d_pendingConflict;
/** Map from representatives to their equivalence class information */
std::map<Node, EqcInfo*> d_eqcInfo;
}; /* class TheoryStrings */
} // namespace strings
} // namespace theory
} // namespace CVC4
#endif /* CVC4__THEORY__STRINGS__SOLVER_STATE_H */
|
