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

disable breaking change to model generation

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-04-19 16:53:20 -07:00
parent eded7d023d
commit e1fa04b365
3 changed files with 48 additions and 21 deletions
Download patch file Download diff file Expand all files Collapse all files

36
src/ast/rewriter/seq_rewriter.cpp
View file

@ -257,6 +257,19 @@ eautomaton* re2automaton::operator()(expr* e) {
return r;
}
bool re2automaton::is_unit_char(expr* e, expr_ref& ch) {
zstring s;
expr* c = nullptr;
if (u.str.is_string(e, s) && s.length() == 1) {
ch = u.mk_char(s[0]);
return true;
}
if (u.str.is_unit(e, c)) {
ch = c;
return true;
}
return false;
}
eautomaton* re2automaton::re2aut(expr* e) {
SASSERT(u.is_re(e));
@ -287,15 +300,12 @@ eautomaton* re2automaton::re2aut(expr* e) {
return a.detach();
}
else if (u.re.is_range(e, e1, e2)) {
if (u.str.is_string(e1, s1) && u.str.is_string(e2, s2) &&
s1.length() == 1 && s2.length() == 1) {
unsigned start = s1[0];
unsigned stop = s2[0];
expr_ref _start(u.mk_char(start), m);
expr_ref _stop(u.mk_char(stop), m);
TRACE("seq", tout << "Range: " << start << " " << stop << "\n";);
expr_ref _start(m), _stop(m);
if (is_unit_char(e1, _start) &&
is_unit_char(e2, _stop)) {
TRACE("seq", tout << "Range: " << _start << " " << _stop << "\n";);
a = alloc(eautomaton, sm, sym_expr::mk_range(_start, _stop));
return a.detach();
return a.detach();
}
else {
TRACE("seq", tout << "Range expression is not handled: " << mk_pp(e, m) << "\n";);
@ -569,7 +579,11 @@ br_status seq_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con
case _OP_STRING_STRIDOF:
UNREACHABLE();
}
if (st != BR_FAILED && m().get_sort(result) != f->get_range()) {
std::cout << expr_ref(m().mk_app(f, num_args, args), m()) << " -> " << result << "\n";
}
CTRACE("seq_verbose", st != BR_FAILED, tout << expr_ref(m().mk_app(f, num_args, args), m()) << " -> " << result << "\n";);
SASSERT(st == BR_FAILED || m().get_sort(result) == f->get_range());
return st;
}
@ -1804,9 +1818,11 @@ br_status seq_rewriter::mk_str_in_regexp(expr* a, expr* b, expr_ref& result) {
TRACE("seq", tout << result << "\n";);
return BR_REWRITE_FULL;
}
br_status seq_rewriter::mk_str_to_regexp(expr* a, expr_ref& result) {
return BR_FAILED;
}
br_status seq_rewriter::mk_re_concat(expr* a, expr* b, expr_ref& result) {
if (m_util.re.is_full_seq(a) && m_util.re.is_full_seq(b)) {
result = a;
@ -1965,9 +1981,7 @@ br_status seq_rewriter::mk_re_inter(expr* a, expr* b, expr_ref& result) {
expr* ac = nullptr, *bc = nullptr;
if ((m_util.re.is_complement(a, ac) && ac == b) ||
(m_util.re.is_complement(b, bc) && bc == a)) {
sort* seq_sort = nullptr;
VERIFY(m_util.is_re(a, seq_sort));
result = m_util.re.mk_empty(seq_sort);
result = m_util.re.mk_empty(m().get_sort(a));
return BR_DONE;
}
return BR_FAILED;

1
src/ast/rewriter/seq_rewriter.h
View file

@ -89,6 +89,7 @@ class re2automaton {
scoped_ptr<boolean_algebra_t> m_ba;
scoped_ptr<symbolic_automata_t> m_sa;
bool is_unit_char(expr* e, expr_ref& ch);
eautomaton* re2aut(expr* e);
eautomaton* seq2aut(expr* e);
public:

32
src/smt/theory_seq.cpp
View file

@ -2388,7 +2388,7 @@ model_value_proc * theory_seq::mk_value(enode * n, model_generator & mg) {
// Shortcut for well-founded values to avoid some quadratic overhead
expr* x = nullptr, *y = nullptr, *z = nullptr;
if (m_util.str.is_concat(e, x, y) && m_util.str.is_unit(x, z) &&
if (false && m_util.str.is_concat(e, x, y) && m_util.str.is_unit(x, z) &&
ctx.e_internalized(z) && ctx.e_internalized(y)) {
sort* srt = m.get_sort(e);
seq_value_proc* sv = alloc(seq_value_proc, *this, n, srt);
@ -3466,15 +3466,23 @@ void theory_seq::new_eq_eh(theory_var v1, theory_var v2) {
new_eq_eh(deps, n1, n2);
}
lbool theory_seq::regex_are_equal(expr* r1, expr* r2) {
if (r1 == r2) {
lbool theory_seq::regex_are_equal(expr* _r1, expr* _r2) {
if (_r1 == _r2) {
return l_true;
}
expr_ref r1(_r1, m);
expr_ref r2(_r2, m);
m_rewrite(r1);
m_rewrite(r2);
if (r1 == r2)
return l_true;
expr* d1 = m_util.re.mk_inter(r1, m_util.re.mk_complement(r2));
expr* d2 = m_util.re.mk_inter(r2, m_util.re.mk_complement(r1));
expr_ref diff(m_util.re.mk_union(d1, d2), m);
m_rewrite(diff);
eautomaton* aut = get_automaton(diff);
if (!aut) {
std::cout << diff << "\n";
return l_undef;
}
else if (aut->is_empty()) {
@ -3487,26 +3495,28 @@ lbool theory_seq::regex_are_equal(expr* r1, expr* r2) {
void theory_seq::new_eq_eh(dependency* deps, enode* n1, enode* n2) {
TRACE("seq", tout << mk_bounded_pp(n1->get_owner(), m) << " = " << mk_bounded_pp(n2->get_owner(), m) << "\n";);
if (n1 != n2 && m_util.is_seq(n1->get_owner())) {
expr* e1 = n1->get_owner();
expr* e2 = n2->get_owner();
TRACE("seq", tout << mk_bounded_pp(e1, m) << " = " << mk_bounded_pp(e2, m) << "\n";);
if (n1 != n2 && m_util.is_seq(e1)) {
theory_var v1 = n1->get_th_var(get_id());
theory_var v2 = n2->get_th_var(get_id());
if (m_find.find(v1) == m_find.find(v2)) {
return;
}
m_find.merge(v1, v2);
expr_ref o1(n1->get_owner(), m);
expr_ref o2(n2->get_owner(), m);
expr_ref o1(e1, m);
expr_ref o2(e2, m);
TRACE("seq", tout << mk_bounded_pp(o1, m) << " = " << mk_bounded_pp(o2, m) << "\n";);
m_eqs.push_back(mk_eqdep(o1, o2, deps));
solve_eqs(m_eqs.size()-1);
enforce_length_coherence(n1, n2);
}
else if (n1 != n2 && m_util.is_re(n1->get_owner())) {
else if (n1 != n2 && m_util.is_re(e1)) {
// create an expression for the symmetric difference and imply it is empty.
enode_pair_vector eqs;
literal_vector lits;
switch (regex_are_equal(n1->get_owner(), n2->get_owner())) {
switch (regex_are_equal(e1, e2)) {
case l_true:
break;
case l_false:
@ -3515,7 +3525,9 @@ void theory_seq::new_eq_eh(dependency* deps, enode* n1, enode* n2) {
set_conflict(eqs, lits);
break;
default:
throw default_exception("convert regular expressions into automata");
std::stringstream strm;
strm << "could not decide equality over: " << mk_pp(e1, m) << "\n" << mk_pp(e2, m) << "\n";
throw default_exception(strm.str());
}
}
}