mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-28 03:15:50 +00:00
Code Activity

change to iterative unfolding left build broken for some time

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-05-26 21:25:53 -07:00
parent 9764007c97
commit 94ffd63b51
3 changed files with 11 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/ast/seq_decl_plugin.h
View file

@ -250,7 +250,7 @@ public:
#if Z3_USE_UNICODE
bool is_char_le(expr const* e) const { return is_app_of(e, m_fid, OP_CHAR_LE); }
#else
bool is_char_le(expr const* e) const { return false; }
bool is_char_le(expr const* e) const { return bv().is_bv_ule(e) && is_char(to_app(e)->get_arg(0)); }
#endif
app* mk_char(unsigned ch) const;
app* mk_le(expr* ch1, expr* ch2) const;

11
src/smt/seq_regex.cpp
View file

@ -337,9 +337,9 @@ namespace smt {
continue;
lits.reset();
lits.push_back(~lit);
if (!m.is_true(cond))
if (!m.is_true(cond))
lits.push_back(~th.mk_literal(cond));
if (false_literal != null_lit)
if (null_lit != false_literal)
lits.push_back(null_lit);
if (!is_member(p.second, u))
lits.push_back(th.mk_literal(sk().mk_is_non_empty(p.second, re().mk_union(u, r))));
@ -385,8 +385,13 @@ namespace smt {
lits.reset();
lits.push_back(~lit);
expr_ref is_empty1 = sk().mk_is_non_empty(p.second, re().mk_union(u, r));
// TBD: triple check soundness here.
// elim_condition(x, x = 'a') = true
// forall x . x = 'a' => is_empty(r, u)
// <=>
// is_empty(r, u)
if (!m.is_true(cond)) {
lits.push_back(th.mk_literal(mk_forall(m, hd, m.mk_not(cond))));
lits.push_back(th.mk_literal(mk_forall(m, hd, mk_not(m, cond))));
}
lits.push_back(th.mk_literal(is_empty1));
th.add_axiom(lits);

3
src/smt/theory_seq.cpp
View file

@ -3509,7 +3509,8 @@ bool theory_seq::should_research(expr_ref_vector & unsat_core) {
if (k_min < UINT_MAX) {
m_max_unfolding_depth++;
k_min *= 2;
k_min = std::max(m_util.str.min_length(s_min), k_min);
if (m_util.is_seq(s_min))
k_min = std::max(m_util.str.min_length(s_min), k_min);
IF_VERBOSE(1, verbose_stream() << "(smt.seq :increase-length " << mk_pp(s_min, m) << " " << k_min << ")\n");
add_length_limit(s_min, k_min, false);
return true;