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

z3str3: add a method to rewrite-and-assert an axiom to reduce boilerplate

Browse source
This commit is contained in:
Murphy Berzish 2019-11-29 11:20:47 -05:00 • committed by Nikolaj Bjorner
parent b8f2cf5b0b
commit bf28b815fa
2 changed files with 24 additions and 14 deletions
Download patch file Download diff file Expand all files Collapse all files

36
src/smt/theory_str.cpp
View file

@ -225,7 +225,16 @@ namespace smt {
m_trail.push_back(e);
//TRACE("str", tout << "done asserting " << mk_ismt2_pp(e, get_manager()) << std::endl;);
}
void theory_str::assert_axiom_rw(expr * e) {
if (e == nullptr)
return;
context & ctx = get_context();
ast_manager & m = get_manager();
expr_ref _e(e, m);
ctx.get_rewriter()(_e);
assert_axiom(_e);
}
expr * theory_str::rewrite_implication(expr * premise, expr * conclusion) {
@ -3419,7 +3428,7 @@ namespace smt {
if (m_params.m_StrongArrangements) {
expr_ref ax_strong(ctx.mk_eq_atom(ax_l, ax_r), mgr);
assert_axiom(ax_strong);
assert_axiom_rw(ax_strong);
} else {
assert_implication(ax_l, ax_r);
}
@ -3482,7 +3491,7 @@ namespace smt {
if (m_params.m_StrongArrangements) {
expr_ref ax_strong(ctx.mk_eq_atom(ax_l, ax_r), mgr);
assert_axiom(ax_strong);
assert_axiom_rw(ax_strong);
} else {
assert_implication(ax_l, ax_r);
}
@ -3993,7 +4002,7 @@ namespace smt {
if (m_params.m_StrongArrangements) {
expr_ref implyLHS(ctx.mk_eq_atom(concatAst1, concatAst2), mgr);
expr_ref ax_strong(ctx.mk_eq_atom(implyLHS, implyR), mgr);
assert_axiom(ax_strong);
assert_axiom_rw(ax_strong);
} else {
assert_implication(ctx.mk_eq_atom(concatAst1, concatAst2), implyR);
}
@ -4184,8 +4193,7 @@ namespace smt {
if (m_params.m_StrongArrangements) {
expr_ref ax_strong(ctx.mk_eq_atom(ax_l, mk_and(r_items)), mgr);
ctx.get_rewriter()(ax_strong);
assert_axiom(ax_strong);
assert_axiom_rw(ax_strong);
} else {
assert_implication(ax_l, mk_and(r_items));
}
@ -4243,7 +4251,7 @@ namespace smt {
if (m_params.m_StrongArrangements) {
expr_ref ax_strong(ctx.mk_eq_atom(ax_l, ax_r), mgr);
assert_axiom(ax_strong);
assert_axiom_rw(ax_strong);
} else {
assert_implication(ax_l, ax_r);
}
@ -4357,7 +4365,7 @@ namespace smt {
if (m_params.m_StrongArrangements) {
expr_ref ax_lhs(ctx.mk_eq_atom(concatAst1, concatAst2), mgr);
expr_ref ax_strong(ctx.mk_eq_atom(ax_lhs, implyR), mgr);
assert_axiom(ax_strong);
assert_axiom_rw(ax_strong);
} else {
assert_implication(ctx.mk_eq_atom(concatAst1, concatAst2), implyR);
}
@ -4436,7 +4444,7 @@ namespace smt {
expr_ref implyR(ctx.mk_eq_atom(n, tmpAst), mgr);
if (m_params.m_StrongArrangements) {
expr_ref ax_strong(ctx.mk_eq_atom( ctx.mk_eq_atom(concatAst1, concatAst2), implyR ), mgr);
assert_axiom(ax_strong);
assert_axiom_rw(ax_strong);
} else {
assert_implication(ctx.mk_eq_atom(concatAst1, concatAst2), implyR);
}
@ -4448,7 +4456,7 @@ namespace smt {
if (m_params.m_StrongArrangements) {
expr_ref ax_strong(ctx.mk_eq_atom( ctx.mk_eq_atom(concatAst1, concatAst2), implyR ), mgr);
assert_axiom(ax_strong);
assert_axiom_rw(ax_strong);
} else {
assert_implication(ctx.mk_eq_atom(concatAst1, concatAst2), implyR);
}
@ -4461,7 +4469,7 @@ namespace smt {
expr_ref implyR(ctx.mk_eq_atom(y, tmpAst), mgr);
if (m_params.m_StrongArrangements) {
expr_ref ax_strong(ctx.mk_eq_atom( ctx.mk_eq_atom(concatAst1, concatAst2), implyR ), mgr);
assert_axiom(ax_strong);
assert_axiom_rw(ax_strong);
} else {
assert_implication(ctx.mk_eq_atom(concatAst1, concatAst2), implyR);
}
@ -4536,7 +4544,7 @@ namespace smt {
expr_ref implyR(ctx.mk_eq_atom(m, x_deltaStr), mgr);
if (m_params.m_StrongArrangements) {
expr_ref ax_strong(ctx.mk_eq_atom( ctx.mk_eq_atom(concatAst1, concatAst2), implyR ), mgr);
assert_axiom(ax_strong);
assert_axiom_rw(ax_strong);
} else {
assert_implication(ctx.mk_eq_atom(concatAst1, concatAst2), implyR);
}
@ -4547,7 +4555,7 @@ namespace smt {
expr_ref implyR(ctx.mk_eq_atom(x, m), mgr);
if (m_params.m_StrongArrangements) {
expr_ref ax_strong(ctx.mk_eq_atom( ctx.mk_eq_atom(concatAst1, concatAst2), implyR ), mgr);
assert_axiom(ax_strong);
assert_axiom_rw(ax_strong);
} else {
assert_implication(ctx.mk_eq_atom(concatAst1, concatAst2), implyR);
}
@ -4559,7 +4567,7 @@ namespace smt {
expr_ref implyR(ctx.mk_eq_atom(x, m_deltaStr), mgr);
if (m_params.m_StrongArrangements) {
expr_ref ax_strong(ctx.mk_eq_atom( ctx.mk_eq_atom(concatAst1, concatAst2), implyR ), mgr);
assert_axiom(ax_strong);
assert_axiom_rw(ax_strong);
} else {
assert_implication(ctx.mk_eq_atom(concatAst1, concatAst2), implyR);
}
@ -4799,7 +4807,7 @@ namespace smt {
if (m_params.m_StrongArrangements) {
expr_ref ax_strong(ctx.mk_eq_atom( ctx.mk_eq_atom(concatAst1, concatAst2), implyR ), mgr);
assert_axiom(ax_strong);
assert_axiom_rw(ax_strong);
} else {
assert_implication(ctx.mk_eq_atom(concatAst1, concatAst2), implyR);
}

2
src/smt/theory_str.h
View file

@ -489,6 +489,8 @@ protected:
void assert_axiom(expr * e);
void assert_implication(expr * premise, expr * conclusion);
expr * rewrite_implication(expr * premise, expr * conclusion);
// Use the rewriter to simplify an axiom, then assert it.
void assert_axiom_rw(expr * e);
expr * mk_string(zstring const& str);
expr * mk_string(const char * str);