mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-10 19:27:06 +00:00
Code Activity

guard derivative code

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-05-23 16:02:10 -07:00
parent eb3f20832e
commit 24df35a83e
6 changed files with 94 additions and 14 deletions

1
src/smt/params/smt_params_helper.pyg
View file

@ -97,6 +97,7 @@ def_module_params(module_name='smt',
('seq.split_w_len', BOOL, True, 'enable splitting guided by length constraints'),
('seq.validate', BOOL, False, 'enable self-validation of theory axioms created by seq theory'),
('seq.use_derivatives', BOOL, False, 'dev flag (not for users) enable derivative based unfolding of regex'),
('seq.use_unicode', BOOL, False, 'dev flag (not for users) enable unicode semantics'),
('str.strong_arrangements', BOOL, True, 'assert equivalences instead of implications when generating string arrangement axioms'),
('str.aggressive_length_testing', BOOL, False, 'prioritize testing concrete length values over generating more options'),
('str.aggressive_value_testing', BOOL, False, 'prioritize testing concrete string constant values over generating more options'),

1
src/smt/params/theory_seq_params.cpp
View file

@ -22,4 +22,5 @@ void theory_seq_params::updt_params(params_ref const & _p) {
m_split_w_len = p.seq_split_w_len();
m_seq_validate = p.seq_validate();
m_seq_use_derivatives = p.seq_use_derivatives();
m_seq_use_unicode = p.seq_use_unicode();
}

4
src/smt/params/theory_seq_params.h
View file

@ -26,12 +26,14 @@ struct theory_seq_params {
bool m_split_w_len;
bool m_seq_validate;
bool m_seq_use_derivatives;
bool m_seq_use_unicode;
theory_seq_params(params_ref const & p = params_ref()):
m_split_w_len(true),
m_seq_validate(false),
m_seq_use_derivatives(false)
m_seq_use_derivatives(false),
m_seq_use_unicode(false)
{
updt_params(p);
}

62
src/smt/seq_regex.cpp
View file

@ -48,12 +48,29 @@ namespace smt {
}
return change;
}
/**
* Propagate the atom (str.in.re s r)
*
* Propagation implements the following inference rules
*
* (not (str.in.re s r)) => (str.in.re s (complement r))
* (str.in.re s r) => r != {}
*
* (str.in.re s r[if(c,r1,r2)]) & c => (str.in.re s r[r1])
* (str.in.re s r[if(c,r1,r2)]) & ~c => (str.in.re s r[r2])
* (str.in.re s r) & s = "" => nullable(r)
* s != "" => s = unit(head) ++ tail
* (str.in.re s r) & s != "" => (str.in.re tail D(head,r))
*/
bool seq_regex::propagate(literal lit) {
expr* s = nullptr, *r = nullptr;
expr* e = ctx.bool_var2expr(lit.var());
VERIFY(str().is_in_re(e, s, r));
TRACE("seq", tout << "propagate " << mk_pp(e, m) << "\n";);
// only positive assignments of membership propagation are relevant.
if (lit.sign() && sk().is_tail(s))
return true;
@ -72,8 +89,16 @@ namespace smt {
return true;
// TBD
// for !sk().is_tail(s):
// s in R => R != {}
// for !sk().is_tail(s): s in R => R != {}
if (false && !sk().is_tail(s)) {
expr_ref is_empty(m.mk_eq(r, re().mk_empty(m.get_sort(s))), m);
rewrite(is_empty);
literal is_emptyl = mk_literal(is_empty);
if (ctx.get_assignment(is_emptyl) != l_false) {
th.propagate_lit(nullptr, 1, &lit, ~is_emptyl);
return true;
}
}
if (block_unfolding(lit, s))
return true;
@ -131,9 +156,22 @@ namespace smt {
throw default_exception("unable to expand derivative");
th.add_axiom(is_empty, th.mk_eq(s, th.mk_concat(head, tail), false));
th.add_axiom(~lit, is_empty, th.mk_literal(re().mk_in_re(tail, d)));
TRACE("seq", tout << "head " << head << "\n";
tout << mk_pp(r, m) << "\n";);
return true;
}
/**
* Put a limit to the unfolding of s.
* TBD:
* Given an Regex R, we can compute the minimal length string accepted by R
* A strong analysis could compute the minimal length of s to be accepted by R
* For example if s = x + "abc" and R = .* ++ "def" . .**, then minimal length
* of s is 6.
* Limiting the depth of unfolding s below such lengths is not useful.
*/
bool seq_regex::block_unfolding(literal lit, expr* s) {
expr* t = nullptr;
unsigned i = 0;
@ -149,6 +187,10 @@ namespace smt {
return false;
}
/**
* Combine a conjunction of membership relations for the same string
* within the same Regex.
*/
bool seq_regex::coallesce_in_re(literal lit) {
// initially disable this
return false;
@ -190,15 +232,23 @@ namespace smt {
}
void seq_regex::propagate_is_empty(literal lit) {
void seq_regex::propagate_eq(expr* r1, expr* r2) {
// the dual version of unroll_non_empty, but
// skolem functions have to be eliminated or turned into
// universal quantifiers.
throw default_exception("emptiness checking of regex is TBD");
throw default_exception("emptiness checking for regex is TBD");
}
void seq_regex::propagate_is_nonempty(expr* r) {
sort* seq_sort = nullptr;
void seq_regex::propagate_ne(expr* r1, expr* r2) {
expr_ref r(m);
if (re().is_empty(r1))
std::swap(r1, r2);
if (re().is_empty(r2))
r = r1;
else
r = re().mk_union(re().mk_diff(r1, r2), re().mk_diff(r2, r1));
rewrite(r);
sort* seq_sort = nullptr;
VERIFY(u().is_re(r, seq_sort));
literal lit = ~th.mk_eq(r, re().mk_empty(seq_sort), false);
expr_mark seen;

9
src/smt/seq_regex.h
View file

@ -64,13 +64,18 @@ namespace smt {
seq_regex(theory_seq& th);
void push_scope() { m_to_propagate.push_scope(); }
void pop_scope(unsigned num_scopes) { m_to_propagate.pop_scope(num_scopes); }
bool propagate();
void propagate_in_re(literal lit);
void propagate_is_empty(literal lit);
void propagate_eq(expr* r1, expr* r2);
void propagate_ne(expr* r1, expr* r2);
void propagate_is_nonempty(expr* r);
};
};

31
src/smt/theory_seq.cpp
View file

@ -382,7 +382,7 @@ final_check_status theory_seq::final_check_eh() {
TRACEFIN("zero_length");
return FC_CONTINUE;
}
if (false && !m_unicode.final_check()) {
if (ctx.get_fparams().m_seq_use_unicode && !m_unicode.final_check()) {
return FC_CONTINUE;
}
if (get_fparams().m_split_w_len && len_based_split()) {
@ -1535,6 +1535,13 @@ bool theory_seq::internalize_term(app* term) {
return true;
}
if (ctx.get_fparams().m_seq_use_derivatives && m_util.str.is_in_re(term)) {
bool_var bv = ctx.mk_bool_var(term);
ctx.set_var_theory(bv, get_id());
ctx.mark_as_relevant(bv);
return true;
}
for (auto arg : *term) {
mk_var(ensure_enode(arg));
}
@ -2515,7 +2522,8 @@ void theory_seq::add_dependency(dependency*& dep, enode* a, enode* b) {
void theory_seq::propagate() {
// m_unicode.propagate();
if (ctx.get_fparams().m_seq_use_unicode)
m_unicode.propagate();
while (m_axioms_head < m_axioms.size() && !ctx.inconsistent()) {
expr_ref e(m);
e = m_axioms[m_axioms_head].get();
@ -3083,7 +3091,7 @@ void theory_seq::assign_eh(bool_var v, bool is_true) {
else if (m_util.str.is_nth_i(e) || m_util.str.is_nth_u(e)) {
// no-op
}
else if (false && m_util.is_char_le(e, e1, e2)) {
else if (ctx.get_fparams().m_seq_use_unicode && m_util.is_char_le(e, e1, e2)) {
theory_var v1 = get_th_var(ctx.get_enode(e1));
theory_var v2 = get_th_var(ctx.get_enode(e2));
if (is_true)
@ -3104,10 +3112,15 @@ void theory_seq::assign_eh(bool_var v, bool is_true) {
void theory_seq::new_eq_eh(theory_var v1, theory_var v2) {
enode* n1 = get_enode(v1);
enode* n2 = get_enode(v2);
if (false && m_util.is_char(n1->get_owner())) {
if (ctx.get_fparams().m_seq_use_unicode && m_util.is_char(n1->get_owner())) {
m_unicode.new_eq_eh(v1, v2);
return;
}
if (ctx.get_fparams().m_seq_use_derivatives && m_util.is_re(n1->get_owner())) {
m_regex.propagate_eq(n1->get_owner(), n2->get_owner());
return;
}
dependency* deps = m_dm.mk_leaf(assumption(n1, n2));
new_eq_eh(deps, n1, n2);
}
@ -3184,6 +3197,12 @@ void theory_seq::new_diseq_eh(theory_var v1, theory_var v2) {
expr_ref e2(n2->get_owner(), m);
SASSERT(n1->get_root() != n2->get_root());
if (m_util.is_re(n1->get_owner())) {
if (ctx.get_fparams().m_seq_use_derivatives) {
m_regex.propagate_ne(e1, e2);
return;
}
enode_pair_vector eqs;
literal_vector lits;
switch (regex_are_equal(e1, e2)) {
@ -3199,7 +3218,7 @@ void theory_seq::new_diseq_eh(theory_var v1, theory_var v2) {
throw default_exception("convert regular expressions into automata");
}
}
if (false && m_util.is_char(n1->get_owner())) {
if (ctx.get_fparams().m_seq_use_unicode && m_util.is_char(n1->get_owner())) {
m_unicode.new_diseq_eh(v1, v2);
return;
}
@ -3233,6 +3252,7 @@ void theory_seq::push_scope_eh() {
m_nqs.push_scope();
m_ncs.push_scope();
m_lts.push_scope();
m_regex.push_scope();
}
void theory_seq::pop_scope_eh(unsigned num_scopes) {
@ -3245,6 +3265,7 @@ void theory_seq::pop_scope_eh(unsigned num_scopes) {
m_nqs.pop_scope(num_scopes);
m_ncs.pop_scope(num_scopes);
m_lts.pop_scope(num_scopes);
m_regex.pop_scope(num_scopes);
m_rewrite.reset();
if (ctx.get_base_level() > ctx.get_scope_level() - num_scopes) {
m_replay.reset();