mirror of
https://github.com/Z3Prover/z3
synced 2025-04-06 09:34:08 +00:00
Merge pull request #1336 from mtrberzi/clean-rewriter-patch
fix rewriter in theory_str
This commit is contained in:
commit
24a44a0b29
|
@ -166,14 +166,18 @@ namespace smt {
|
|||
}
|
||||
}
|
||||
|
||||
void theory_str::assert_axiom(expr * e) {
|
||||
void theory_str::assert_axiom(expr * _e) {
|
||||
if (opt_VerifyFinalCheckProgress) {
|
||||
finalCheckProgressIndicator = true;
|
||||
}
|
||||
|
||||
if (get_manager().is_true(e)) return;
|
||||
TRACE("str", tout << "asserting " << mk_ismt2_pp(e, get_manager()) << std::endl;);
|
||||
if (get_manager().is_true(_e)) return;
|
||||
context & ctx = get_context();
|
||||
ast_manager& m = get_manager();
|
||||
TRACE("str", tout << "asserting " << mk_ismt2_pp(_e, m) << std::endl;);
|
||||
expr_ref e(_e, m);
|
||||
//th_rewriter rw(m);
|
||||
//rw(e);
|
||||
if (!ctx.b_internalized(e)) {
|
||||
ctx.internalize(e, false);
|
||||
}
|
||||
|
@ -1422,104 +1426,6 @@ namespace smt {
|
|||
assert_axiom(finalAxiom);
|
||||
}
|
||||
|
||||
void theory_str::instantiate_axiom_Substr(enode * e) {
|
||||
context & ctx = get_context();
|
||||
ast_manager & m = get_manager();
|
||||
|
||||
app * expr = e->get_owner();
|
||||
if (axiomatized_terms.contains(expr)) {
|
||||
TRACE("str", tout << "already set up Substr axiom for " << mk_pp(expr, m) << std::endl;);
|
||||
return;
|
||||
}
|
||||
axiomatized_terms.insert(expr);
|
||||
|
||||
TRACE("str", tout << "instantiate Substr axiom for " << mk_pp(expr, m) << std::endl;);
|
||||
|
||||
expr_ref substrBase(expr->get_arg(0), m);
|
||||
expr_ref substrPos(expr->get_arg(1), m);
|
||||
expr_ref substrLen(expr->get_arg(2), m);
|
||||
SASSERT(substrBase);
|
||||
SASSERT(substrPos);
|
||||
SASSERT(substrLen);
|
||||
|
||||
expr_ref zero(m_autil.mk_numeral(rational::zero(), true), m);
|
||||
expr_ref minusOne(m_autil.mk_numeral(rational::minus_one(), true), m);
|
||||
SASSERT(zero);
|
||||
SASSERT(minusOne);
|
||||
|
||||
expr_ref_vector argumentsValid_terms(m);
|
||||
// pos >= 0
|
||||
argumentsValid_terms.push_back(m_autil.mk_ge(substrPos, zero));
|
||||
// pos < strlen(base)
|
||||
// --> pos + -1*strlen(base) < 0
|
||||
argumentsValid_terms.push_back(mk_not(m, m_autil.mk_ge(
|
||||
m_autil.mk_add(substrPos, m_autil.mk_mul(minusOne, substrLen)),
|
||||
zero)));
|
||||
|
||||
// len >= 0
|
||||
argumentsValid_terms.push_back(m_autil.mk_ge(substrLen, zero));
|
||||
|
||||
expr_ref argumentsValid(mk_and(argumentsValid_terms), m);
|
||||
SASSERT(argumentsValid);
|
||||
ctx.internalize(argumentsValid, false);
|
||||
|
||||
// (pos+len) >= strlen(base)
|
||||
// --> pos + len + -1*strlen(base) >= 0
|
||||
expr_ref lenOutOfBounds(m_autil.mk_ge(
|
||||
m_autil.mk_add(substrPos, substrLen, m_autil.mk_mul(minusOne, mk_strlen(substrBase))),
|
||||
zero), m);
|
||||
SASSERT(lenOutOfBounds);
|
||||
ctx.internalize(argumentsValid, false);
|
||||
|
||||
// Case 1: pos < 0 or pos >= strlen(base) or len < 0
|
||||
// ==> (Substr ...) = ""
|
||||
expr_ref case1_premise(mk_not(m, argumentsValid), m);
|
||||
SASSERT(case1_premise);
|
||||
ctx.internalize(case1_premise, false);
|
||||
expr_ref case1_conclusion(ctx.mk_eq_atom(expr, mk_string("")), m);
|
||||
SASSERT(case1_conclusion);
|
||||
ctx.internalize(case1_conclusion, false);
|
||||
expr_ref case1(rewrite_implication(case1_premise, case1_conclusion), m);
|
||||
SASSERT(case1);
|
||||
|
||||
// Case 2: (pos >= 0 and pos < strlen(base) and len >= 0) and (pos+len) >= strlen(base)
|
||||
// ==> base = t0.t1 AND len(t0) = pos AND (Substr ...) = t1
|
||||
expr_ref t0(mk_str_var("t0"), m);
|
||||
expr_ref t1(mk_str_var("t1"), m);
|
||||
expr_ref case2_conclusion(m.mk_and(
|
||||
ctx.mk_eq_atom(substrBase, mk_concat(t0,t1)),
|
||||
ctx.mk_eq_atom(mk_strlen(t0), substrPos),
|
||||
ctx.mk_eq_atom(expr, t1)), m);
|
||||
expr_ref case2(rewrite_implication(m.mk_and(argumentsValid, lenOutOfBounds), case2_conclusion), m);
|
||||
SASSERT(case2);
|
||||
|
||||
// Case 3: (pos >= 0 and pos < strlen(base) and len >= 0) and (pos+len) < strlen(base)
|
||||
// ==> base = t2.t3.t4 AND len(t2) = pos AND len(t3) = len AND (Substr ...) = t3
|
||||
|
||||
expr_ref t2(mk_str_var("t2"), m);
|
||||
expr_ref t3(mk_str_var("t3"), m);
|
||||
expr_ref t4(mk_str_var("t4"), m);
|
||||
expr_ref_vector case3_conclusion_terms(m);
|
||||
case3_conclusion_terms.push_back(ctx.mk_eq_atom(substrBase, mk_concat(t2, mk_concat(t3, t4))));
|
||||
case3_conclusion_terms.push_back(ctx.mk_eq_atom(mk_strlen(t2), substrPos));
|
||||
case3_conclusion_terms.push_back(ctx.mk_eq_atom(mk_strlen(t3), substrLen));
|
||||
case3_conclusion_terms.push_back(ctx.mk_eq_atom(expr, t3));
|
||||
expr_ref case3_conclusion(mk_and(case3_conclusion_terms), m);
|
||||
expr_ref case3(rewrite_implication(m.mk_and(argumentsValid, mk_not(m, lenOutOfBounds)), case3_conclusion), m);
|
||||
SASSERT(case3);
|
||||
|
||||
ctx.internalize(case1, false);
|
||||
ctx.internalize(case2, false);
|
||||
ctx.internalize(case3, false);
|
||||
|
||||
expr_ref finalAxiom(m.mk_and(case1, case2, case3), m);
|
||||
SASSERT(finalAxiom);
|
||||
assert_axiom(finalAxiom);
|
||||
}
|
||||
|
||||
#if 0
|
||||
// rewrite
|
||||
// requires to add th_rewriter to assert_axiom to enforce normal form.
|
||||
void theory_str::instantiate_axiom_Substr(enode * e) {
|
||||
context & ctx = get_context();
|
||||
ast_manager & m = get_manager();
|
||||
|
@ -1551,6 +1457,7 @@ namespace smt {
|
|||
argumentsValid_terms.push_back(mk_not(m, m_autil.mk_ge(
|
||||
m_autil.mk_add(substrPos, m_autil.mk_mul(minusOne, substrLen)),
|
||||
zero)));
|
||||
|
||||
// len >= 0
|
||||
argumentsValid_terms.push_back(m_autil.mk_ge(substrLen, zero));
|
||||
|
||||
|
@ -1564,7 +1471,7 @@ namespace smt {
|
|||
|
||||
// Case 1: pos < 0 or pos >= strlen(base) or len < 0
|
||||
// ==> (Substr ...) = ""
|
||||
expr_ref case1_premise(mk_not(m, argumentsValid), m);
|
||||
expr_ref case1_premise(m.mk_not(argumentsValid), m);
|
||||
expr_ref case1_conclusion(ctx.mk_eq_atom(expr, mk_string("")), m);
|
||||
expr_ref case1(m.mk_implies(case1_premise, case1_conclusion), m);
|
||||
|
||||
|
@ -1580,6 +1487,7 @@ namespace smt {
|
|||
|
||||
// Case 3: (pos >= 0 and pos < strlen(base) and len >= 0) and (pos+len) < strlen(base)
|
||||
// ==> base = t2.t3.t4 AND len(t2) = pos AND len(t3) = len AND (Substr ...) = t3
|
||||
|
||||
expr_ref t2(mk_str_var("t2"), m);
|
||||
expr_ref t3(mk_str_var("t3"), m);
|
||||
expr_ref t4(mk_str_var("t4"), m);
|
||||
|
@ -1589,13 +1497,24 @@ namespace smt {
|
|||
case3_conclusion_terms.push_back(ctx.mk_eq_atom(mk_strlen(t3), substrLen));
|
||||
case3_conclusion_terms.push_back(ctx.mk_eq_atom(expr, t3));
|
||||
expr_ref case3_conclusion(mk_and(case3_conclusion_terms), m);
|
||||
expr_ref case3(m.mk_implies(m.mk_and(argumentsValid, mk_not(m, lenOutOfBounds)), case3_conclusion), m);
|
||||
expr_ref case3(m.mk_implies(m.mk_and(argumentsValid, m.mk_not(lenOutOfBounds)), case3_conclusion), m);
|
||||
|
||||
assert_axiom(case1);
|
||||
assert_axiom(case2);
|
||||
assert_axiom(case3);
|
||||
{
|
||||
th_rewriter rw(m);
|
||||
|
||||
expr_ref case1_rw(case1, m);
|
||||
rw(case1_rw);
|
||||
assert_axiom(case1_rw);
|
||||
|
||||
expr_ref case2_rw(case2, m);
|
||||
rw(case2_rw);
|
||||
assert_axiom(case2_rw);
|
||||
|
||||
expr_ref case3_rw(case3, m);
|
||||
rw(case3_rw);
|
||||
assert_axiom(case3_rw);
|
||||
}
|
||||
}
|
||||
#endif
|
||||
|
||||
void theory_str::instantiate_axiom_Replace(enode * e) {
|
||||
context & ctx = get_context();
|
||||
|
@ -1636,13 +1555,17 @@ namespace smt {
|
|||
// false branch
|
||||
expr_ref elseBranch(ctx.mk_eq_atom(result, expr->get_arg(0)), m);
|
||||
|
||||
th_rewriter rw(m);
|
||||
|
||||
expr_ref breakdownAssert(m.mk_ite(condAst, m.mk_and(thenItems.size(), thenItems.c_ptr()), elseBranch), m);
|
||||
assert_axiom(breakdownAssert);
|
||||
|
||||
SASSERT(breakdownAssert);
|
||||
expr_ref breakdownAssert_rw(breakdownAssert, m);
|
||||
rw(breakdownAssert_rw);
|
||||
assert_axiom(breakdownAssert_rw);
|
||||
|
||||
expr_ref reduceToResult(ctx.mk_eq_atom(expr, result), m);
|
||||
assert_axiom(reduceToResult);
|
||||
expr_ref reduceToResult_rw(reduceToResult, m);
|
||||
rw(reduceToResult_rw);
|
||||
assert_axiom(reduceToResult_rw);
|
||||
}
|
||||
|
||||
void theory_str::instantiate_axiom_str_to_int(enode * e) {
|
||||
|
@ -4752,12 +4675,10 @@ namespace smt {
|
|||
bool theory_str::get_arith_value(expr* e, rational& val) const {
|
||||
context& ctx = get_context();
|
||||
ast_manager & m = get_manager();
|
||||
|
||||
// safety
|
||||
if (!ctx.e_internalized(e)) {
|
||||
// safety
|
||||
if (!ctx.e_internalized(e)) {
|
||||
return false;
|
||||
}
|
||||
|
||||
}
|
||||
// if an integer constant exists in the eqc, it should be the root
|
||||
enode * en_e = ctx.get_enode(e);
|
||||
enode * root_e = en_e->get_root();
|
||||
|
|
Loading…
Reference in a new issue