mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 18:31:49 +00:00
Code Activity

Merge pull request #1147 from mtrberzi/fix-get-arith-value

Browse source 
Improved theory_arith integration in theory_str::get_arith_value()
This commit is contained in:
Nikolaj Bjorner 2017-07-24 21:21:45 -07:00 committed by GitHub
parent 741f940119 7ddb940f77
commit 3865c45382
1 changed files with 14 additions and 24 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

38
src/smt/theory_str.cpp
View file

@ -4653,34 +4653,24 @@ namespace smt {
}
bool theory_str::get_arith_value(expr* e, rational& val) const {
if (opt_DisableIntegerTheoryIntegration) {
TRACE("str", tout << "WARNING: integer theory integration disabled" << std::endl;);
return false;
}
context& ctx = get_context();
ast_manager & m = get_manager();
theory_mi_arith* tha = get_th_arith(ctx, m_autil.get_family_id(), e);
if (!tha) {
// safety
if (!ctx.e_internalized(e)) {
return false;
}
// 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;
}
TRACE("str", tout << "checking eqc of " << mk_pp(e, m) << " for arithmetic value" << std::endl;);
expr_ref _val(m);
enode * en_e = ctx.get_enode(e);
enode * it = en_e;
do {
if (m_autil.is_numeral(it->get_owner(), val) && val.is_int()) {
// found an arithmetic term
TRACE("str", tout << mk_pp(it->get_owner(), m) << " is an integer ( ~= " << val << " )"
<< std::endl;);
return true;
} else {
TRACE("str", tout << mk_pp(it->get_owner(), m) << " not a numeral" << std::endl;);
}
it = it->get_next();
} while (it != en_e);
TRACE("str", tout << "no arithmetic values found in eqc" << std::endl;);
return false;
}
bool theory_str::lower_bound(expr* _e, rational& lo) {