mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

modify theory_str::get_value() to check EQC for a numeral

Browse source 
Instead of asking the arithmetic theory for the current assignment,
we return the (unique) numeral in the equivalence class of the term
whose length we want to know.

This is because the arithmetic theory may return a default / internal
value that doesn't correspond to anything actually asserted by the core solver.
This commit is contained in:
Murphy Berzish 2016-08-02 16:44:54 -04:00
parent 45c4954959
commit 3c2fe497de
1 changed files with 4 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

8
src/smt/theory_str.cpp
View file

@ -3832,13 +3832,13 @@ bool theory_str::get_value(expr* e, rational& val) const {
enode * en_e = ctx.get_enode(e);
enode * it = en_e;
do {
if (tha->get_value(it, _val)) {
if (m_autil.is_numeral(it->get_owner(), val) && val.is_int()) {
// found an arithmetic term
TRACE("t_str_int", tout << "get_value[" << mk_pp(it->get_owner(), m) << "] = " << mk_pp(_val, m)
TRACE("t_str_int", tout << mk_pp(it->get_owner(), m) << " is an integer ( ~= " << val << " )"
<< std::endl;);
return m_autil.is_numeral(_val, val) && val.is_int();
return true;
} else {
TRACE("t_str_int", tout << "get_value[" << mk_pp(it->get_owner(), m) << "] not found" << std::endl;);
TRACE("t_str_int", tout << mk_pp(it->get_owner(), m) << " not a numeral" << std::endl;);
}
it = it->get_next();
} while (it != en_e);