mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

fix theory of arithmetic complaints about wanting to write A > B

Browse source 
"what could possibly go wrong?"
This commit is contained in:
Murphy Berzish 2015-09-30 05:45:16 -04:00
parent ecb2116927
commit 5189c24d42
1 changed files with 14 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

17
src/smt/theory_str.cpp
View file

@ -274,7 +274,8 @@ app * theory_str::mk_nonempty_str_var() {
zero = m_autil.mk_numeral(rational(0), true);
SASSERT(zero);
// build LHS > RHS and assert
app * lhs_gt_rhs = m_autil.mk_gt(len_str, zero);
// we have to build !(LHS <= RHS) instead
app * lhs_gt_rhs = m.mk_not(m_autil.mk_le(len_str, zero));
SASSERT(lhs_gt_rhs);
assert_axiom(lhs_gt_rhs);
}
@ -1008,8 +1009,18 @@ void theory_str::process_concat_eq_type1(expr * concatAst1, expr * concatAst2) {
expr_ref x_plus_t1(m_autil.mk_add(mk_strlen(x), mk_strlen(t1)), mgr);
and_item[pos++] = ctx.mk_eq_atom(or_item[option], ctx.mk_eq_atom(mk_strlen(m), x_plus_t1));
and_item[pos++] = ctx.mk_eq_atom(or_item[option], m_autil.mk_gt(mk_strlen(m), mk_strlen(x)));
and_item[pos++] = ctx.mk_eq_atom(or_item[option], m_autil.mk_gt(mk_strlen(y), mk_strlen(n)));
// TODO these are crashing the solvers because the integer theory
// expects a constant on the right-hand side.
// The things we want to assert here are len(m) > len(x) and len(y) > len(n).
// We rewrite A > B as A-B > 0 and then as not(A-B <= 0),
// and then, *because we aren't allowed to use subtraction*,
// as not(A + -1*B <= 0)
and_item[pos++] = ctx.mk_eq_atom(or_item[option],
mgr.mk_not(m_autil.mk_le(m_autil.mk_add(mk_strlen(m),
m_autil.mk_mul(mk_int(-1), mk_strlen(x))), mk_int(0))) );
and_item[pos++] = ctx.mk_eq_atom(or_item[option],
mgr.mk_not(m_autil.mk_le(m_autil.mk_add(mk_strlen(y),
m_autil.mk_mul(mk_int(-1), mk_strlen(n))), mk_int(0))) );
option++;