mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 18:31:49 +00:00
Code Activity

ensure also negative lt are constrained

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-06-30 07:44:06 +03:00
parent 1f0d162b7f
commit 85b0722df0
3 changed files with 25 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -518,6 +518,10 @@ br_status seq_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con
SASSERT(num_args == 2);
st = mk_str_in_regexp(args[0], args[1], result);
break;
case OP_STRING_LE:
SASSERT(num_args == 2);
st = mk_str_le(args[0], args[1], result);
break;
case OP_STRING_CONST:
return BR_FAILED;
case OP_STRING_ITOS:
@ -1237,6 +1241,11 @@ br_status seq_rewriter::mk_seq_suffix(expr* a, expr* b, expr_ref& result) {
return BR_FAILED;
}
br_status seq_rewriter::mk_str_le(expr* a, expr* b, expr_ref& result) {
result = m.mk_not(m_util.str.mk_lex_lt(b, a));
return BR_DONE;
}
br_status seq_rewriter::mk_str_itos(expr* a, expr_ref& result) {
rational r;
if (m_autil.is_numeral(a, r)) {

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

@ -124,6 +124,7 @@ class seq_rewriter {
br_status mk_str_stoi(expr* a, expr_ref& result);
br_status mk_str_in_regexp(expr* a, expr* b, expr_ref& result);
br_status mk_str_to_regexp(expr* a, expr_ref& result);
br_status mk_str_le(expr* a, expr* b, expr_ref& result);
br_status mk_re_concat(expr* a, expr* b, expr_ref& result);
br_status mk_re_union(expr* a, expr* b, expr_ref& result);
br_status mk_re_inter(expr* a, expr* b, expr_ref& result);

19
src/smt/theory_seq.cpp
View file

@ -5923,6 +5923,9 @@ void theory_seq::propagate_not_suffix(expr* e) {
e1 < e2 => e1 = empty or e1 = xcy
e1 < e2 => e1 = empty or c < d
e1 < e2 => e2 = xdz
!(e1 < e2) => e1 = e2 or e2 = empty or e2 = xcy
!(e1 < e2) => e1 = e2 or e2 = empty or c < d
!(e1 < e2) => e1 = e2 or e1 = xdz
e1 < e2 or e1 = e2 or e2 < e1
!(e1 = e2) or !(e1 < e2)
@ -5941,15 +5944,23 @@ void theory_seq::add_lt_axiom(expr* n) {
expr_ref z = mk_skolem(symbol("str.lt.z"), e1, e2);
expr_ref c = mk_skolem(symbol("str.lt.c"), e1, e2, nullptr, nullptr, char_sort);
expr_ref d = mk_skolem(symbol("str.lt.d"), e1, e2, nullptr, nullptr, char_sort);
expr_ref xcy(mk_concat(x, m_util.str.mk_unit(c), y), m);
expr_ref xdz(mk_concat(x, m_util.str.mk_unit(d), z), m);
expr_ref empty_string(m_util.str.mk_empty(s), m);
literal emp1 = mk_eq(e1, empty_string, false);
literal emp2 = mk_eq(e2, empty_string, false);
literal eq = mk_eq(e1, e2, false);
literal xcy = mk_eq(e1, mk_concat(x, m_util.str.mk_unit(c), y), false);
literal xdz = mk_eq(e2, mk_concat(x, m_util.str.mk_unit(d), z), false);
literal e1xcy = mk_eq(e1, xcy, false);
literal e2xdz = mk_eq(e2, xdz, false);
literal e2xcy = mk_eq(e2, xcy, false);
literal e1xdz = mk_eq(e1, xdz, false);
literal ltcd = mk_literal(m_util.mk_lt(c, d));
add_axiom(~lt, xdz);
add_axiom(~lt, emp1, xcy);
add_axiom(~lt, e2xdz);
add_axiom(~lt, emp1, e1xcy);
add_axiom(~lt, emp1, ltcd);
add_axiom(lt, eq, e1xdz);
add_axiom(lt, eq, emp2, ltcd);
add_axiom(lt, eq, emp2, e2xcy);
if (e1->get_id() <= e2->get_id()) {
literal gt = mk_literal(m_util.str.mk_lex_lt(e2, e1));
add_axiom(lt, eq, gt);