mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 02:15:19 +00:00
Code Activity

fix various nullability checks in seq_regex

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-06-03 12:28:32 -07:00
parent 377dbad3b9
commit 3a7df2c6ef
4 changed files with 22 additions and 16 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/muz/transforms/dl_mk_array_blast.cpp
View file

@ -324,7 +324,6 @@ namespace datalog {
}
scoped_ptr<rule_set> rules = alloc(rule_set, m_ctx);
rules->inherit_predicates(source);
rule_set::iterator it = source.begin(), end = source.end();
bool change = false;
for (rule* r : source) {
if (m_ctx.canceled())

4
src/nlsat/nlsat_solver.cpp
View file

@ -1967,7 +1967,9 @@ namespace nlsat {
bool resolve(clause const & conflict) {
clause const * conflict_clause = &conflict;
m_lemma_assumptions = nullptr;
start:
std::cout << "resolve\n";
start:
std::cout << "start\n";
SASSERT(check_marks());
TRACE("nlsat_proof", tout << "STARTING RESOLUTION\n";);
TRACE("nlsat_proof_sk", tout << "STARTING RESOLUTION\n";);

11
src/qe/qe_arith_plugin.cpp
View file

@ -2412,24 +2412,21 @@ public:
}
bool update_bounds(contains_app& contains_x, expr* fml) {
bounds_proc* bounds = nullptr;
if (m_bounds_cache.find(contains_x.x(), fml, bounds)) {
bounds_proc* _bounds = nullptr;
if (m_bounds_cache.find(contains_x.x(), fml, _bounds)) {
return true;
}
bounds = alloc(bounds_proc, m_util);
scoped_ptr<bounds_proc> bounds = alloc(bounds_proc, m_util);
if (!update_bounds(*bounds, contains_x, fml, m_ctx.pos_atoms(), true)) {
dealloc(bounds);
return false;
}
if (!update_bounds(*bounds, contains_x, fml, m_ctx.neg_atoms(), false)) {
dealloc(bounds);
return false;
}
m_trail.push_back(contains_x.x());
m_trail.push_back(fml);
m_bounds_cache.insert(contains_x.x(), fml, bounds);
m_bounds_cache.insert(contains_x.x(), fml, bounds.detach());
return true;
}
};

22
src/smt/seq_regex.cpp
View file

@ -195,11 +195,22 @@ namespace smt {
VERIFY(sk().is_accept(e, s, i, idx, r));
expr_ref is_nullable(m), d(r, m);
TRACE("seq", tout << "propagate " << mk_pp(e, m) << "\n";);
if (block_unfolding(lit, idx))
return true;
literal_vector conds;
conds.push_back(~lit);
if (!unfold_cofactors(d, conds))
return false;
if (re().is_empty(d)) {
th.add_axiom(conds);
return true;
}
// s in R & len(s) <= i => nullable(R)
literal len_s_le_i = th.m_ax.mk_le(th.mk_len(s), idx);
switch (ctx.get_assignment(len_s_le_i)) {
@ -207,25 +218,22 @@ namespace smt {
ctx.mark_as_relevant(len_s_le_i);
return false;
case l_true:
is_nullable = seq_rw().is_nullable(r);
is_nullable = seq_rw().is_nullable(d);
rewrite(is_nullable);
th.add_axiom(~lit, ~len_s_le_i, th.mk_literal(is_nullable));
conds.push_back(~len_s_le_i);
conds.push_back(th.mk_literal(is_nullable));
th.add_axiom(conds);
return true;
case l_false:
break;
}
literal_vector conds;
if (!unfold_cofactors(d, conds))
return false;
// (accept s i R) & len(s) > i => (accept s (+ i 1) D(nth(s, i), R)) or conds
expr_ref head = th.mk_nth(s, i);
d = re().mk_derivative(head, r);
rewrite(d);
literal acc_next = th.mk_literal(sk().mk_accept(s, a().mk_int(idx + 1), d));
conds.push_back(~lit);
conds.push_back(len_s_le_i);
conds.push_back(acc_next);
th.add_axiom(conds);