Branch data Line data Source code
1 : : /******************************************************************************
2 : : * This file is part of the cvc5 project.
3 : : *
4 : : * Copyright (c) 2009-2026 by the authors listed in the file AUTHORS
5 : : * in the top-level source directory and their institutional affiliations.
6 : : * All rights reserved. See the file COPYING in the top-level source
7 : : * directory for licensing information.
8 : : * ****************************************************************************
9 : : *
10 : : * Implementation of the solver state of the theory of strings.
11 : : */
12 : :
13 : : #include "theory/strings/solver_state.h"
14 : :
15 : : #include "theory/rewriter.h"
16 : : #include "theory/strings/model_cons.h"
17 : : #include "theory/strings/theory_strings_utils.h"
18 : : #include "theory/strings/word.h"
19 : : #include "util/rational.h"
20 : :
21 : : using namespace std;
22 : : using namespace cvc5::context;
23 : : using namespace cvc5::internal::kind;
24 : :
25 : : namespace cvc5::internal {
26 : : namespace theory {
27 : : namespace strings {
28 : :
29 : 51016 : SolverState::SolverState(Env& env, Valuation& v)
30 : : : TheoryState(env, v),
31 : 51016 : d_eeDisequalities(env.getContext()),
32 : 51016 : d_pendingConflictSet(env.getContext(), false),
33 : 51016 : d_pendingConflict(InferenceId::UNKNOWN),
34 : 102032 : d_modelCons(nullptr)
35 : : {
36 : 51016 : d_zero = nodeManager()->mkConstInt(Rational(0));
37 : 51016 : d_false = nodeManager()->mkConst(false);
38 : 51016 : }
39 : :
40 : 50668 : SolverState::~SolverState()
41 : : {
42 [ + + ]: 178809 : for (std::pair<const Node, EqcInfo*>& it : d_eqcInfo)
43 : : {
44 [ + - ]: 128141 : delete it.second;
45 : : }
46 : 50668 : }
47 : :
48 : 43324 : const context::CDList<Node>& SolverState::getDisequalityList() const
49 : : {
50 : 43324 : return d_eeDisequalities;
51 : : }
52 : :
53 : 373912 : void SolverState::addDisequality(TNode t1, TNode t2)
54 : : {
55 : 373912 : d_eeDisequalities.push_back(t1.eqNode(t2));
56 : 373912 : }
57 : :
58 : 7239180 : EqcInfo* SolverState::getOrMakeEqcInfo(Node eqc, bool doMake)
59 : : {
60 : 7239180 : std::map<Node, EqcInfo*>::iterator eqc_i = d_eqcInfo.find(eqc);
61 [ + + ]: 7239180 : if (eqc_i != d_eqcInfo.end())
62 : : {
63 : 5802430 : return eqc_i->second;
64 : : }
65 [ + + ]: 1436750 : if (doMake)
66 : : {
67 : 128141 : EqcInfo* ei = new EqcInfo(d_env.getContext());
68 : 128141 : d_eqcInfo[eqc] = ei;
69 : 128141 : return ei;
70 : : }
71 : 1308609 : return nullptr;
72 : : }
73 : :
74 : 16174 : TheoryModel* SolverState::getModel() { return d_valuation.getModel(); }
75 : :
76 : 3583903 : Node SolverState::getLengthExp(Node t,
77 : : std::vector<Node>& exp,
78 : : Node te,
79 : : bool minExp)
80 : : {
81 [ - + ][ - + ]: 3583903 : Assert(areEqual(t, te));
[ - - ]
82 : : // if we are minimizing explanations
83 [ + + ]: 3583903 : if (minExp)
84 : : {
85 : 1505663 : Node lt = nodeManager()->mkNode(Kind::STRING_LENGTH, te);
86 : 1505663 : lt = rewrite(lt);
87 [ + + ]: 1505663 : if (hasTerm(lt))
88 : : {
89 : : // use own length if it exists, leads to shorter explanation
90 : 1503137 : return lt;
91 : : }
92 [ + + ]: 1505663 : }
93 : 2080766 : EqcInfo* ei = getOrMakeEqcInfo(t, false);
94 [ + + ]: 2080766 : Node lengthTerm = ei ? ei->d_lengthTerm : Node::null();
95 : 2080766 : Node ret;
96 [ + + ]: 2080766 : if (lengthTerm.isNull())
97 : : {
98 : : // typically shouldn't be necessary
99 : 2524 : lengthTerm = te;
100 : : }
101 : : else
102 : : {
103 : 2078242 : lengthTerm = lengthTerm[0];
104 : : }
105 [ + - ]: 4161532 : Trace("strings") << "SolverState::getLengthTerm " << t << "/" << te << " is "
106 : 2080766 : << lengthTerm << std::endl;
107 [ + + ]: 2080766 : if (te != lengthTerm)
108 : : {
109 : 112681 : exp.push_back(te.eqNode(lengthTerm));
110 : : }
111 : 2080766 : return rewrite(nodeManager()->mkNode(Kind::STRING_LENGTH, lengthTerm));
112 : 2080766 : }
113 : :
114 : 3583899 : Node SolverState::getLength(Node t, std::vector<Node>& exp, bool minExp)
115 : : {
116 : 3583899 : return getLengthExp(t, exp, t, minExp);
117 : : }
118 : :
119 : 23165 : Node SolverState::explainNonEmpty(Node s)
120 : : {
121 [ - + ][ - + ]: 23165 : Assert(s.getType().isStringLike());
[ - - ]
122 : 23165 : Node emp = Word::mkEmptyWord(s.getType());
123 [ + + ]: 23165 : if (areDisequal(s, emp))
124 : : {
125 : 26086 : return s.eqNode(emp).negate();
126 : : }
127 : 10122 : Node sLen = nodeManager()->mkNode(Kind::STRING_LENGTH, s);
128 : 10122 : sLen = rewrite(sLen);
129 [ + + ]: 10122 : if (areDisequal(sLen, d_zero))
130 : : {
131 : 20236 : return sLen.eqNode(d_zero).negate();
132 : : }
133 : 4 : return Node::null();
134 : 23165 : }
135 : :
136 : 1781907 : bool SolverState::isEqualEmptyWord(Node s, Node& emps)
137 : : {
138 : 3563814 : Node sr = getRepresentative(s);
139 [ + + ]: 1781907 : if (sr.isConst())
140 : : {
141 [ + + ]: 335140 : if (Word::getLength(sr) == 0)
142 : : {
143 : 77250 : emps = sr;
144 : 77250 : return true;
145 : : }
146 : : }
147 : 1704657 : return false;
148 : 1781907 : }
149 : :
150 : 1150 : void SolverState::setPendingMergeConflict(Node conf, InferenceId id, bool rev)
151 : : {
152 [ + + ]: 1150 : if (d_pendingConflictSet.get())
153 : : {
154 : : // already set conflict
155 : 29 : return;
156 : : }
157 : 1121 : InferInfo iiPrefixConf(id);
158 : : // remember whether this was a prefix/suffix, which is used when looking
159 : : // if the explanation can be minimized
160 : 1121 : iiPrefixConf.d_idRev = rev;
161 : 1121 : iiPrefixConf.d_conc = d_false;
162 : 1121 : utils::flattenOp(Kind::AND, conf, iiPrefixConf.d_premises);
163 : 1121 : setPendingConflict(iiPrefixConf);
164 : 1121 : }
165 : :
166 : 1121 : void SolverState::setPendingConflict(InferInfo& ii)
167 : : {
168 [ + - ]: 1121 : if (!d_pendingConflictSet.get())
169 : : {
170 : 1121 : d_pendingConflict = ii;
171 : 1121 : d_pendingConflictSet.set(true);
172 : : }
173 : 1121 : }
174 : :
175 : 4379525 : bool SolverState::hasPendingConflict() const { return d_pendingConflictSet; }
176 : :
177 : 1111 : bool SolverState::getPendingConflict(InferInfo& ii) const
178 : : {
179 [ + - ]: 1111 : if (d_pendingConflictSet)
180 : : {
181 : 1111 : ii = d_pendingConflict;
182 : 1111 : return true;
183 : : }
184 : 0 : return false;
185 : : }
186 : :
187 : 11473 : std::pair<bool, Node> SolverState::entailmentCheck(options::TheoryOfMode mode,
188 : : TNode lit)
189 : : {
190 : 11473 : return d_valuation.entailmentCheck(mode, lit);
191 : : }
192 : :
193 : 36359 : void SolverState::separateByLengthTyped(
194 : : const std::vector<Node>& n,
195 : : std::map<TypeNode, std::vector<std::vector<Node>>>& cols,
196 : : std::map<TypeNode, std::vector<Node>>& lts)
197 : : {
198 : : // group terms by types
199 : 36359 : std::map<TypeNode, std::vector<Node>> tvecs;
200 [ + + ]: 188098 : for (const Node& eqc : n)
201 : : {
202 : 151739 : tvecs[eqc.getType()].push_back(eqc);
203 : : }
204 : : // separate for each type
205 [ + + ]: 43604 : for (const std::pair<const TypeNode, std::vector<Node>>& v : tvecs)
206 : : {
207 : 7245 : separateByLength(v.second, cols[v.first], lts[v.first]);
208 : : }
209 : 36359 : }
210 : :
211 : 9461 : void SolverState::separateByLength(const std::vector<Node>& n,
212 : : std::vector<std::vector<Node>>& cols,
213 : : std::vector<Node>& lts)
214 : : {
215 : 9461 : unsigned leqc_counter = 0;
216 : : // map (length, type) to an equivalence class identifier
217 : 9461 : std::map<Node, unsigned> eqc_to_leqc;
218 : : // backwards map
219 : 9461 : std::map<unsigned, Node> leqc_to_eqc;
220 : : // Collection of eqc for each identifier. Notice that some identifiers may
221 : : // not have an associated length in the mappings above, if the length of
222 : : // an equivalence class is unknown.
223 : 9461 : std::map<unsigned, std::vector<Node>> eqc_to_strings;
224 [ + + ]: 176216 : for (const Node& eqc : n)
225 : : {
226 [ - + ][ - + ]: 166755 : Assert(d_ee->getRepresentative(eqc) == eqc);
[ - - ]
227 : 166755 : EqcInfo* ei = getOrMakeEqcInfo(eqc, false);
228 [ + + ]: 166755 : Node lt = ei ? ei->d_lengthTerm : Node::null();
229 [ + + ]: 166755 : if (!lt.isNull())
230 : : {
231 : 333502 : Node r = d_ee->getRepresentative(lt);
232 [ + + ]: 166751 : if (eqc_to_leqc.find(r) == eqc_to_leqc.end())
233 : : {
234 : 35005 : eqc_to_leqc[r] = leqc_counter;
235 : 35005 : leqc_to_eqc[leqc_counter] = r;
236 : 35005 : leqc_counter++;
237 : : }
238 : 166751 : eqc_to_strings[eqc_to_leqc[r]].push_back(eqc);
239 : 166751 : }
240 : : else
241 : : {
242 : 4 : eqc_to_strings[leqc_counter].push_back(eqc);
243 : 4 : leqc_counter++;
244 : : }
245 : 166755 : }
246 [ + + ]: 44470 : for (const std::pair<const unsigned, std::vector<Node>>& p : eqc_to_strings)
247 : : {
248 [ - + ][ - + ]: 35009 : Assert(!p.second.empty());
[ - - ]
249 : 35009 : cols.emplace_back(p.second.begin(), p.second.end());
250 : 35009 : lts.push_back(leqc_to_eqc[p.first]);
251 : : }
252 : 9461 : }
253 : :
254 : 105132 : void SolverState::setModelConstructor(ModelCons* mc) { d_modelCons = mc; }
255 : :
256 : 17653 : ModelCons* SolverState::getModelConstructor() { return d_modelCons; }
257 : :
258 : : } // namespace strings
259 : : } // namespace theory
260 : : } // namespace cvc5::internal
|
