mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
limit recursion depth of push_not() to 8 (#4917)
This commit is contained in:
parent
374ae52d70
commit
799de71a9f
|
@ -201,10 +201,10 @@ expr_ref mk_not(const expr_ref& e) {
|
|||
}
|
||||
|
||||
|
||||
expr_ref push_not(const expr_ref& e) {
|
||||
expr_ref push_not(const expr_ref& e, unsigned limit) {
|
||||
ast_manager& m = e.get_manager();
|
||||
if (!is_app(e)) {
|
||||
return expr_ref(m.mk_not(e), m);
|
||||
if (!is_app(e) || limit == 0) {
|
||||
return mk_not(e);
|
||||
}
|
||||
app* a = to_app(e);
|
||||
if (m.is_and(a)) {
|
||||
|
@ -213,7 +213,7 @@ expr_ref push_not(const expr_ref& e) {
|
|||
}
|
||||
expr_ref_vector args(m);
|
||||
for (expr* arg : *a) {
|
||||
args.push_back(push_not(expr_ref(arg, m)));
|
||||
args.push_back(push_not(expr_ref(arg, m), limit-1));
|
||||
}
|
||||
return mk_or(args);
|
||||
}
|
||||
|
@ -223,11 +223,11 @@ expr_ref push_not(const expr_ref& e) {
|
|||
}
|
||||
expr_ref_vector args(m);
|
||||
for (expr* arg : *a) {
|
||||
args.push_back(push_not(expr_ref(arg, m)));
|
||||
args.push_back(push_not(expr_ref(arg, m), limit-1));
|
||||
}
|
||||
return mk_and(args);
|
||||
}
|
||||
return expr_ref(mk_not(m, e), m);
|
||||
return mk_not(e);
|
||||
}
|
||||
|
||||
expr * expand_distinct(ast_manager & m, unsigned num_args, expr * const * args) {
|
||||
|
|
|
@ -141,7 +141,7 @@ inline app_ref mk_not(const app_ref& e) { return app_ref(e.m().mk_not(e), e.m())
|
|||
/**
|
||||
Negate and push over conjunction or disjunction.
|
||||
*/
|
||||
expr_ref push_not(const expr_ref& arg);
|
||||
expr_ref push_not(const expr_ref& arg, unsigned limit = 8);
|
||||
|
||||
/**
|
||||
Return the expression (and (not (= args[0] args[1])) (not (= args[0] args[2])) ... (not (= args[num_args-2] args[num_args-1])))
|
||||
|
|
Loading…
Reference in a new issue