mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-02 09:20:22 +00:00
Code Activity

don't rewrite on every axiom in theory_str

Browse source
This commit is contained in:
Murphy Berzish 2017-09-07 14:06:37 -04:00
parent 10cd396ae3
commit 4e4c72580b
1 changed files with 17 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

22
src/smt/theory_str.cpp
View file

@ -176,8 +176,8 @@ namespace smt {
ast_manager& m = get_manager(); ast_manager& m = get_manager();
TRACE("str", tout << "asserting " << mk_ismt2_pp(_e, m) << std::endl;); TRACE("str", tout << "asserting " << mk_ismt2_pp(_e, m) << std::endl;);
expr_ref e(_e, m); expr_ref e(_e, m);
th_rewriter rw(m); //th_rewriter rw(m);
rw(e); //rw(e);
if (!ctx.b_internalized(e)) { if (!ctx.b_internalized(e)) {
ctx.internalize(e, false); ctx.internalize(e, false);
} }
@ -1491,9 +1491,21 @@ namespace smt {
expr_ref case3_conclusion(mk_and(case3_conclusion_terms), m); expr_ref case3_conclusion(mk_and(case3_conclusion_terms), m);
expr_ref case3(m.mk_implies(m.mk_and(argumentsValid, m.mk_not(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); th_rewriter rw(m);
assert_axiom(case3);
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);
}
} }
void theory_str::instantiate_axiom_Replace(enode * e) { void theory_str::instantiate_axiom_Replace(enode * e) {