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 branch 'master' of https://github.com/Z3Prover/z3

Browse source
This commit is contained in:
Nikolaj Bjorner 2017-07-25 10:18:43 -07:00
parent 70f6280bf1 3865c45382
commit 9d6be286d0
2 changed files with 15 additions and 25 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/ast/ast_smt2_pp.cpp
View file

@ -429,7 +429,7 @@ format_ns::format * smt2_pp_environment::pp_sort(sort * s) {
if ((get_sutil().is_seq(s) || get_sutil().is_re(s)) && !get_sutil().is_string(s)) {
ptr_buffer<format> fs;
fs.push_back(pp_sort(to_sort(s->get_parameter(0).get_ast())));
return mk_seq1(m, fs.begin(), fs.end(), f2f(), get_sutil().is_seq(s)?"Seq":"Re");
return mk_seq1(m, fs.begin(), fs.end(), f2f(), get_sutil().is_seq(s)?"Seq":"RegEx");
}
#if 0
if (get_dtutil().is_datatype(s)) {

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) {