mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-06 14:13:23 +00:00
Code Activity

fix #3052: incorrect handling of ands simplified to false in dom-simplify

Browse source 
+ add support for not operations
This commit is contained in:
Nuno Lopes 2020-02-20 16:21:46 +00:00
parent 3bb05b5e01
commit c9be09b18c
2 changed files with 17 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -275,6 +275,9 @@ expr_ref dom_simplify_tactic::simplify_rec(expr * e0) {
else if (m.is_or(e)) { else if (m.is_or(e)) {
r = simplify_or(to_app(e)); r = simplify_or(to_app(e));
} }
else if (m.is_not(e)) {
r = simplify_not(to_app(e));
}
else { else {
for (expr * child : tree(e)) { for (expr * child : tree(e)) {
simplify_rec(child); simplify_rec(child);
@ -329,6 +332,7 @@ expr_ref dom_simplify_tactic::simplify_and_or(bool is_and, app * e) {
r = simplify_arg(arg); \ r = simplify_arg(arg); \
args.push_back(r); \ args.push_back(r); \
if (!assert_expr(r, !is_and)) { \ if (!assert_expr(r, !is_and)) { \
pop(scope_level() - old_lvl); \
r = is_and ? m.mk_false() : m.mk_true(); \ r = is_and ? m.mk_false() : m.mk_true(); \
return r; \ return r; \
} }
@ -345,10 +349,17 @@ expr_ref dom_simplify_tactic::simplify_and_or(bool is_and, app * e) {
} }
pop(scope_level() - old_lvl); pop(scope_level() - old_lvl);
r = is_and ? mk_and(args) : mk_or(args); return { is_and ? mk_and(args) : mk_or(args), m };
return r;
} }
expr_ref dom_simplify_tactic::simplify_not(app * e) {
expr *ee;
ENSURE(m.is_not(e, ee));
unsigned old_lvl = scope_level();
expr_ref t = simplify_rec(ee);
pop(scope_level() - old_lvl);
return mk_not(t);
}
bool dom_simplify_tactic::init(goal& g) { bool dom_simplify_tactic::init(goal& g) {

7
src/tactic/core/dom_simplify_tactic.h
View file

@ -105,9 +105,10 @@ class dom_simplify_tactic : public tactic {
expr_ref simplify_rec(expr* t); expr_ref simplify_rec(expr* t);
expr_ref simplify_arg(expr* t); expr_ref simplify_arg(expr* t);
expr_ref simplify_ite(app * ite); expr_ref simplify_ite(app * ite);
expr_ref simplify_and(app * ite) { return simplify_and_or(true, ite); } expr_ref simplify_and(app * e) { return simplify_and_or(true, e); }
expr_ref simplify_or(app * ite) { return simplify_and_or(false, ite); } expr_ref simplify_or(app * e) { return simplify_and_or(false, e); }
expr_ref simplify_and_or(bool is_and, app * ite); expr_ref simplify_and_or(bool is_and, app * e);
expr_ref simplify_not(app * e);
void simplify_goal(goal& g); void simplify_goal(goal& g);
bool is_subexpr(expr * a, expr * b); bool is_subexpr(expr * a, expr * b);