1 /********************* */
2 /*! \file solver_state.cpp
4 ** Top contributors (to current version):
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2019 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.\endverbatim
12 ** \brief Implementation of the solver state of the theory of strings.
15 #include "theory/strings/solver_state.h"
17 #include "theory/strings/theory_strings_utils.h"
18 #include "theory/strings/word.h"
21 using namespace CVC4::context
;
22 using namespace CVC4::kind
;
28 SolverState::SolverState(context::Context
* c
,
29 eq::EqualityEngine
& ee
,
38 d_zero
= NodeManager::currentNM()->mkConst(Rational(0));
41 SolverState::~SolverState()
43 for (std::pair
<const Node
, EqcInfo
*>& it
: d_eqcInfo
)
49 Node
SolverState::getRepresentative(Node t
) const
53 return d_ee
.getRepresentative(t
);
58 bool SolverState::hasTerm(Node a
) const { return d_ee
.hasTerm(a
); }
60 bool SolverState::areEqual(Node a
, Node b
) const
66 else if (hasTerm(a
) && hasTerm(b
))
68 return d_ee
.areEqual(a
, b
);
73 bool SolverState::areDisequal(Node a
, Node b
) const
79 else if (hasTerm(a
) && hasTerm(b
))
81 Node ar
= d_ee
.getRepresentative(a
);
82 Node br
= d_ee
.getRepresentative(b
);
83 return (ar
!= br
&& ar
.isConst() && br
.isConst())
84 || d_ee
.areDisequal(ar
, br
, false);
86 Node ar
= getRepresentative(a
);
87 Node br
= getRepresentative(b
);
88 return ar
!= br
&& ar
.isConst() && br
.isConst();
91 eq::EqualityEngine
* SolverState::getEqualityEngine() const { return &d_ee
; }
93 const context::CDList
<Node
>& SolverState::getDisequalityList() const
95 return d_eeDisequalities
;
98 void SolverState::eqNotifyNewClass(TNode t
)
100 Kind k
= t
.getKind();
101 if (k
== STRING_LENGTH
|| k
== STRING_TO_CODE
)
103 Node r
= d_ee
.getRepresentative(t
[0]);
104 EqcInfo
* ei
= getOrMakeEqcInfo(r
);
105 if (k
== STRING_LENGTH
)
107 ei
->d_lengthTerm
= t
[0];
111 ei
->d_codeTerm
= t
[0];
114 else if (t
.isConst())
116 EqcInfo
* ei
= getOrMakeEqcInfo(t
);
121 else if (k
== STRING_CONCAT
)
123 addEndpointsToEqcInfo(t
, t
, t
);
127 void SolverState::eqNotifyPreMerge(TNode t1
, TNode t2
)
129 EqcInfo
* e2
= getOrMakeEqcInfo(t2
, false);
132 EqcInfo
* e1
= getOrMakeEqcInfo(t1
);
133 // add information from e2 to e1
134 if (!e2
->d_lengthTerm
.get().isNull())
136 e1
->d_lengthTerm
.set(e2
->d_lengthTerm
);
138 if (!e2
->d_codeTerm
.get().isNull())
140 e1
->d_codeTerm
.set(e2
->d_codeTerm
);
142 if (!e2
->d_prefixC
.get().isNull())
144 setPendingConflictWhen(
145 e1
->addEndpointConst(e2
->d_prefixC
, Node::null(), false));
147 if (!e2
->d_suffixC
.get().isNull())
149 setPendingConflictWhen(
150 e1
->addEndpointConst(e2
->d_suffixC
, Node::null(), true));
152 if (e2
->d_cardinalityLemK
.get() > e1
->d_cardinalityLemK
.get())
154 e1
->d_cardinalityLemK
.set(e2
->d_cardinalityLemK
);
156 if (!e2
->d_normalizedLength
.get().isNull())
158 e1
->d_normalizedLength
.set(e2
->d_normalizedLength
);
163 void SolverState::eqNotifyDisequal(TNode t1
, TNode t2
, TNode reason
)
165 if (t1
.getType().isStringLike())
167 // store disequalities between strings, may need to check if their lengths
168 // are equal/disequal
169 d_eeDisequalities
.push_back(t1
.eqNode(t2
));
173 EqcInfo
* SolverState::getOrMakeEqcInfo(Node eqc
, bool doMake
)
175 std::map
<Node
, EqcInfo
*>::iterator eqc_i
= d_eqcInfo
.find(eqc
);
176 if (eqc_i
!= d_eqcInfo
.end())
178 return eqc_i
->second
;
182 EqcInfo
* ei
= new EqcInfo(d_context
);
189 TheoryModel
* SolverState::getModel() const { return d_valuation
.getModel(); }
191 void SolverState::addEndpointsToEqcInfo(Node t
, Node concat
, Node eqc
)
193 Assert(concat
.getKind() == STRING_CONCAT
194 || concat
.getKind() == REGEXP_CONCAT
);
195 EqcInfo
* ei
= nullptr;
197 for (unsigned r
= 0; r
< 2; r
++)
199 unsigned index
= r
== 0 ? 0 : concat
.getNumChildren() - 1;
200 Node c
= utils::getConstantComponent(concat
[index
]);
205 ei
= getOrMakeEqcInfo(eqc
);
207 Trace("strings-eager-pconf-debug")
208 << "New term: " << concat
<< " for " << t
<< " with prefix " << c
209 << " (" << (r
== 1) << ")" << std::endl
;
210 setPendingConflictWhen(ei
->addEndpointConst(t
, c
, r
== 1));
215 Node
SolverState::getLengthExp(Node t
, std::vector
<Node
>& exp
, Node te
)
217 Assert(areEqual(t
, te
));
218 Node lt
= utils::mkNLength(te
);
221 // use own length if it exists, leads to shorter explanation
224 EqcInfo
* ei
= getOrMakeEqcInfo(t
, false);
225 Node lengthTerm
= ei
? ei
->d_lengthTerm
: Node::null();
226 if (lengthTerm
.isNull())
228 // typically shouldnt be necessary
231 Debug("strings") << "SolverState::getLengthTerm " << t
<< " is " << lengthTerm
233 if (te
!= lengthTerm
)
235 exp
.push_back(te
.eqNode(lengthTerm
));
237 return Rewriter::rewrite(
238 NodeManager::currentNM()->mkNode(STRING_LENGTH
, lengthTerm
));
241 Node
SolverState::getLength(Node t
, std::vector
<Node
>& exp
)
243 return getLengthExp(t
, exp
, t
);
246 Node
SolverState::explainNonEmpty(Node s
)
248 Assert(s
.getType().isStringLike());
249 Node emp
= Word::mkEmptyWord(s
.getType());
250 if (areDisequal(s
, emp
))
252 return s
.eqNode(emp
).negate();
254 Node sLen
= utils::mkNLength(s
);
255 if (areDisequal(sLen
, d_zero
))
257 return sLen
.eqNode(d_zero
).negate();
262 void SolverState::setConflict() { d_conflict
= true; }
263 bool SolverState::isInConflict() const { return d_conflict
; }
265 void SolverState::setPendingConflictWhen(Node conf
)
267 if (!conf
.isNull() && d_pendingConflict
.get().isNull())
269 d_pendingConflict
= conf
;
273 Node
SolverState::getPendingConflict() const { return d_pendingConflict
; }
275 std::pair
<bool, Node
> SolverState::entailmentCheck(options::TheoryOfMode mode
,
278 return d_valuation
.entailmentCheck(mode
, lit
);
281 void SolverState::separateByLength(const std::vector
<Node
>& n
,
282 std::vector
<std::vector
<Node
> >& cols
,
283 std::vector
<Node
>& lts
)
285 unsigned leqc_counter
= 0;
286 std::map
<Node
, unsigned> eqc_to_leqc
;
287 std::map
<unsigned, Node
> leqc_to_eqc
;
288 std::map
<unsigned, std::vector
<Node
> > eqc_to_strings
;
289 NodeManager
* nm
= NodeManager::currentNM();
290 for (const Node
& eqc
: n
)
292 Assert(d_ee
.getRepresentative(eqc
) == eqc
);
293 EqcInfo
* ei
= getOrMakeEqcInfo(eqc
, false);
294 Node lt
= ei
? ei
->d_lengthTerm
: Node::null();
297 lt
= nm
->mkNode(STRING_LENGTH
, lt
);
298 Node r
= d_ee
.getRepresentative(lt
);
299 if (eqc_to_leqc
.find(r
) == eqc_to_leqc
.end())
301 eqc_to_leqc
[r
] = leqc_counter
;
302 leqc_to_eqc
[leqc_counter
] = r
;
305 eqc_to_strings
[eqc_to_leqc
[r
]].push_back(eqc
);
309 eqc_to_strings
[leqc_counter
].push_back(eqc
);
313 for (const std::pair
<const unsigned, std::vector
<Node
> >& p
: eqc_to_strings
)
315 cols
.push_back(std::vector
<Node
>());
316 cols
.back().insert(cols
.back().end(), p
.second
.begin(), p
.second
.end());
317 lts
.push_back(leqc_to_eqc
[p
.first
]);
321 } // namespace strings
322 } // namespace theory