mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-13 12:28:44 +00:00
Code Activity

Z3str3: don't use arith_value::get_value in get_arith_value

Browse source
This commit is contained in:
Murphy Berzish 2018-10-02 12:28:53 -04:00
parent 03d9047490
commit 39fbf1e174
1 changed files with 18 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

21
src/smt/theory_str.cpp
View file

@ -4836,9 +4836,24 @@ namespace smt {
}
bool theory_str::get_arith_value(expr* e, rational& val) const {
arith_value v(get_context());
return v.get_value(e, val);
}
context& ctx = get_context();
ast_manager & m = get_manager();
if (!ctx.e_internalized(e)) {
return false;
}
// check root of the eqc for an integer constant
// if an integer constant exists in the eqc, it should be the root
enode * en_e = ctx.get_enode(e);
enode * root_e = en_e->get_root();
if (m_autil.is_numeral(root_e->get_owner(), val) && val.is_int()) {
TRACE("str", tout << mk_pp(e, m) << " ~= " << mk_pp(root_e->get_owner(), m) << std::endl;);
return true;
} else {
TRACE("str", tout << "root of eqc of " << mk_pp(e, m) << " is not a numeral" << std::endl;);
return false;
}
}
bool theory_str::lower_bound(expr* _e, rational& lo) {
if (opt_DisableIntegerTheoryIntegration) {