Branch data Line data Source code
1 : : /******************************************************************************
2 : : * Top contributors (to current version):
3 : : * Andrew Reynolds, Gereon Kremer, Tianyi Liang
4 : : *
5 : : * This file is part of the cvc5 project.
6 : : *
7 : : * Copyright (c) 2009-2025 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.
11 : : * ****************************************************************************
12 : : *
13 : : * Implementation of the solver state of the theory of strings.
14 : : */
15 : :
16 : : #include "theory/strings/solver_state.h"
17 : :
18 : : #include "theory/rewriter.h"
19 : : #include "theory/strings/model_cons.h"
20 : : #include "theory/strings/theory_strings_utils.h"
21 : : #include "theory/strings/word.h"
22 : : #include "util/rational.h"
23 : :
24 : : using namespace std;
25 : : using namespace cvc5::context;
26 : : using namespace cvc5::internal::kind;
27 : :
28 : : namespace cvc5::internal {
29 : : namespace theory {
30 : : namespace strings {
31 : :
32 : 51396 : SolverState::SolverState(Env& env, Valuation& v)
33 : : : TheoryState(env, v),
34 : : d_eeDisequalities(env.getContext()),
35 : 0 : d_pendingConflictSet(env.getContext(), false),
36 : : d_pendingConflict(InferenceId::UNKNOWN),
37 : 51396 : d_modelCons(nullptr)
38 : : {
39 : 51396 : d_zero = nodeManager()->mkConstInt(Rational(0));
40 : 51396 : d_false = nodeManager()->mkConst(false);
41 : 51396 : }
42 : :
43 : 51140 : SolverState::~SolverState()
44 : : {
45 [ + + ]: 178336 : for (std::pair<const Node, EqcInfo*>& it : d_eqcInfo)
46 : : {
47 [ + - ]: 127196 : delete it.second;
48 : : }
49 : 51140 : }
50 : :
51 : 37345 : const context::CDList<Node>& SolverState::getDisequalityList() const
52 : : {
53 : 37345 : return d_eeDisequalities;
54 : : }
55 : :
56 : 350430 : void SolverState::addDisequality(TNode t1, TNode t2)
57 : : {
58 : 350430 : d_eeDisequalities.push_back(t1.eqNode(t2));
59 : 350430 : }
60 : :
61 : 4783030 : EqcInfo* SolverState::getOrMakeEqcInfo(Node eqc, bool doMake)
62 : : {
63 : 4783030 : std::map<Node, EqcInfo*>::iterator eqc_i = d_eqcInfo.find(eqc);
64 [ + + ]: 4783030 : if (eqc_i != d_eqcInfo.end())
65 : : {
66 : 3415760 : return eqc_i->second;
67 : : }
68 [ + + ]: 1367270 : if (doMake)
69 : : {
70 : 127196 : EqcInfo* ei = new EqcInfo(d_env.getContext());
71 : 127196 : d_eqcInfo[eqc] = ei;
72 : 127196 : return ei;
73 : : }
74 : 1240070 : return nullptr;
75 : : }
76 : :
77 : 16285 : TheoryModel* SolverState::getModel() { return d_valuation.getModel(); }
78 : :
79 : 1616020 : Node SolverState::getLengthExp(Node t,
80 : : std::vector<Node>& exp,
81 : : Node te,
82 : : bool minExp)
83 : : {
84 [ - + ][ - + ]: 1616020 : Assert(areEqual(t, te));
[ - - ]
85 : : // if we are minimizing explanations
86 [ + + ]: 1616020 : if (minExp)
87 : : {
88 : 2991440 : Node lt = nodeManager()->mkNode(Kind::STRING_LENGTH, te);
89 : 1495720 : lt = rewrite(lt);
90 [ + + ]: 1495720 : if (hasTerm(lt))
91 : : {
92 : : // use own length if it exists, leads to shorter explanation
93 : 1493160 : return lt;
94 : : }
95 : : }
96 : 122865 : EqcInfo* ei = getOrMakeEqcInfo(t, false);
97 [ + + ]: 245730 : Node lengthTerm = ei ? ei->d_lengthTerm : Node::null();
98 : 122865 : Node ret;
99 [ + + ]: 122865 : if (lengthTerm.isNull())
100 : : {
101 : : // typically shouldn't be necessary
102 : 2533 : lengthTerm = te;
103 : : }
104 : : else
105 : : {
106 : 120332 : lengthTerm = lengthTerm[0];
107 : : }
108 [ + - ]: 245730 : Trace("strings") << "SolverState::getLengthTerm " << t << "/" << te << " is "
109 : 122865 : << lengthTerm << std::endl;
110 [ + + ]: 122865 : if (te != lengthTerm)
111 : : {
112 : 103610 : exp.push_back(te.eqNode(lengthTerm));
113 : : }
114 : 122865 : return rewrite(nodeManager()->mkNode(Kind::STRING_LENGTH, lengthTerm));
115 : : }
116 : :
117 : 1616020 : Node SolverState::getLength(Node t, std::vector<Node>& exp, bool minExp)
118 : : {
119 : 1616020 : return getLengthExp(t, exp, t, minExp);
120 : : }
121 : :
122 : 23481 : Node SolverState::explainNonEmpty(Node s)
123 : : {
124 [ - + ][ - + ]: 23481 : Assert(s.getType().isStringLike());
[ - - ]
125 : 46962 : Node emp = Word::mkEmptyWord(s.getType());
126 [ + + ]: 23481 : if (areDisequal(s, emp))
127 : : {
128 : 26526 : return s.eqNode(emp).negate();
129 : : }
130 : 30654 : Node sLen = nodeManager()->mkNode(Kind::STRING_LENGTH, s);
131 : 10218 : sLen = rewrite(sLen);
132 [ + + ]: 10218 : if (areDisequal(sLen, d_zero))
133 : : {
134 : 20428 : return sLen.eqNode(d_zero).negate();
135 : : }
136 : 4 : return Node::null();
137 : : }
138 : :
139 : 1585750 : bool SolverState::isEqualEmptyWord(Node s, Node& emps)
140 : : {
141 : 4757250 : Node sr = getRepresentative(s);
142 [ + + ]: 1585750 : if (sr.isConst())
143 : : {
144 [ + + ]: 247834 : if (Word::getLength(sr) == 0)
145 : : {
146 : 57529 : emps = sr;
147 : 57529 : return true;
148 : : }
149 : : }
150 : 1528220 : return false;
151 : : }
152 : :
153 : 1120 : void SolverState::setPendingMergeConflict(Node conf, InferenceId id, bool rev)
154 : : {
155 [ + + ]: 1120 : if (d_pendingConflictSet.get())
156 : : {
157 : : // already set conflict
158 : 28 : return;
159 : : }
160 : 2184 : InferInfo iiPrefixConf(id);
161 : : // remember whether this was a prefix/suffix, which is used when looking
162 : : // if the explanation can be minimized
163 : 1092 : iiPrefixConf.d_idRev = rev;
164 : 1092 : iiPrefixConf.d_conc = d_false;
165 : 1092 : utils::flattenOp(Kind::AND, conf, iiPrefixConf.d_premises);
166 : 1092 : setPendingConflict(iiPrefixConf);
167 : : }
168 : :
169 : 1092 : void SolverState::setPendingConflict(InferInfo& ii)
170 : : {
171 [ + - ]: 1092 : if (!d_pendingConflictSet.get())
172 : : {
173 : 1092 : d_pendingConflict = ii;
174 : 1092 : d_pendingConflictSet.set(true);
175 : : }
176 : 1092 : }
177 : :
178 : 4131150 : bool SolverState::hasPendingConflict() const { return d_pendingConflictSet; }
179 : :
180 : 1078 : bool SolverState::getPendingConflict(InferInfo& ii) const
181 : : {
182 [ + - ]: 1078 : if (d_pendingConflictSet)
183 : : {
184 : 1078 : ii = d_pendingConflict;
185 : 1078 : return true;
186 : : }
187 : 0 : return false;
188 : : }
189 : :
190 : 11624 : std::pair<bool, Node> SolverState::entailmentCheck(options::TheoryOfMode mode,
191 : : TNode lit)
192 : : {
193 : 11624 : return d_valuation.entailmentCheck(mode, lit);
194 : : }
195 : :
196 : 30683 : void SolverState::separateByLengthTyped(
197 : : const std::vector<Node>& n,
198 : : std::map<TypeNode, std::vector<std::vector<Node>>>& cols,
199 : : std::map<TypeNode, std::vector<Node>>& lts)
200 : : {
201 : : // group terms by types
202 : 61366 : std::map<TypeNode, std::vector<Node>> tvecs;
203 [ + + ]: 56429 : for (const Node& eqc : n)
204 : : {
205 : 25746 : tvecs[eqc.getType()].push_back(eqc);
206 : : }
207 : : // separate for each type
208 [ + + ]: 34122 : for (const std::pair<const TypeNode, std::vector<Node>>& v : tvecs)
209 : : {
210 : 3439 : separateByLength(v.second, cols[v.first], lts[v.first]);
211 : : }
212 : 30683 : }
213 : :
214 : 5595 : void SolverState::separateByLength(const std::vector<Node>& n,
215 : : std::vector<std::vector<Node>>& cols,
216 : : std::vector<Node>& lts)
217 : : {
218 : 5595 : unsigned leqc_counter = 0;
219 : : // map (length, type) to an equivalence class identifier
220 : 11190 : std::map<Node, unsigned> eqc_to_leqc;
221 : : // backwards map
222 : 11190 : std::map<unsigned, Node> leqc_to_eqc;
223 : : // Collection of eqc for each identifier. Notice that some identifiers may
224 : : // not have an associated length in the mappings above, if the length of
225 : : // an equivalence class is unknown.
226 : 11190 : std::map<unsigned, std::vector<Node> > eqc_to_strings;
227 [ + + ]: 46198 : for (const Node& eqc : n)
228 : : {
229 [ - + ][ - + ]: 40603 : Assert(d_ee->getRepresentative(eqc) == eqc);
[ - - ]
230 : 40603 : EqcInfo* ei = getOrMakeEqcInfo(eqc, false);
231 [ + + ]: 81206 : Node lt = ei ? ei->d_lengthTerm : Node::null();
232 [ + + ]: 40603 : if (!lt.isNull())
233 : : {
234 : 121797 : Node r = d_ee->getRepresentative(lt);
235 [ + + ]: 40599 : if (eqc_to_leqc.find(r) == eqc_to_leqc.end())
236 : : {
237 : 27421 : eqc_to_leqc[r] = leqc_counter;
238 : 27421 : leqc_to_eqc[leqc_counter] = r;
239 : 27421 : leqc_counter++;
240 : : }
241 : 40599 : eqc_to_strings[eqc_to_leqc[r]].push_back(eqc);
242 : : }
243 : : else
244 : : {
245 : 4 : eqc_to_strings[leqc_counter].push_back(eqc);
246 : 4 : leqc_counter++;
247 : : }
248 : : }
249 [ + + ]: 33020 : for (const std::pair<const unsigned, std::vector<Node> >& p : eqc_to_strings)
250 : : {
251 [ - + ][ - + ]: 27425 : Assert(!p.second.empty());
[ - - ]
252 : 27425 : cols.emplace_back(p.second.begin(), p.second.end());
253 : 27425 : lts.push_back(leqc_to_eqc[p.first]);
254 : : }
255 : 5595 : }
256 : :
257 : 93112 : void SolverState::setModelConstructor(ModelCons* mc) { d_modelCons = mc; }
258 : :
259 : 17645 : ModelCons* SolverState::getModelConstructor() { return d_modelCons; }
260 : :
261 : : } // namespace strings
262 : : } // namespace theory
263 : : } // namespace cvc5::internal
|
