mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-27 00:18:45 +00:00
Code Activity

reverse arguments

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-10-06 16:03:43 +01:00
parent e13d839e7c
commit c3f615dbfc
1 changed files with 4 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

5
src/tactic/core/dom_simplify_tactic.cpp
View file

@ -291,7 +291,7 @@ expr_ref dom_simplify_tactic::simplify_and_or(bool is_and, app * e) {
} \ } \
r = simplify(arg); \ r = simplify(arg); \
args.push_back(r); \ args.push_back(r); \
if (!assert_expr(simplify(arg), !is_and)) { \ if (!assert_expr(r, !is_and)) { \
r = is_and ? m.mk_false() : m.mk_true(); \ r = is_and ? m.mk_false() : m.mk_true(); \
return r; \ return r; \
} }
@ -304,6 +304,7 @@ expr_ref dom_simplify_tactic::simplify_and_or(bool is_and, app * e) {
expr* arg = e->get_arg(i); expr* arg = e->get_arg(i);
_SIMP_ARG(arg); _SIMP_ARG(arg);
} }
args.reverse();
} }
pop(scope_level() - old_lvl); pop(scope_level() - old_lvl);
r = is_and ? mk_and(args) : mk_or(args); r = is_and ? mk_and(args) : mk_or(args);
@ -338,6 +339,7 @@ void dom_simplify_tactic::simplify_goal(goal& g) {
if (i < sz - 1 && !m.is_true(r) && !m.is_false(r) && !g.dep(i) && !g.proofs_enabled() && !assert_expr(r, false)) { if (i < sz - 1 && !m.is_true(r) && !m.is_false(r) && !g.dep(i) && !g.proofs_enabled() && !assert_expr(r, false)) {
r = m.mk_false(); r = m.mk_false();
} }
CTRACE("simplify", r != g.form(i), tout << r << " " << mk_pp(g.form(i), m) << "\n";);
change |= r != g.form(i); change |= r != g.form(i);
proof* new_pr = 0; proof* new_pr = 0;
if (g.proofs_enabled()) { if (g.proofs_enabled()) {
@ -358,6 +360,7 @@ void dom_simplify_tactic::simplify_goal(goal& g) {
r = m.mk_false(); r = m.mk_false();
} }
change |= r != g.form(i); change |= r != g.form(i);
CTRACE("simplify", r != g.form(i), tout << r << " " << mk_pp(g.form(i), m) << "\n";);
proof* new_pr = 0; proof* new_pr = 0;
if (g.proofs_enabled()) { if (g.proofs_enabled()) {
new_pr = m.mk_modus_ponens(g.pr(i), m.mk_rewrite_star(g.form(i), r, 0, 0)); new_pr = m.mk_modus_ponens(g.pr(i), m.mk_rewrite_star(g.form(i), r, 0, 0));