limit recursion depth of push_not() to 8 (#4917)

Z3Prover · Dec 29, 2020 · 799de71 · 799de71
1 parent 374ae52
commit 799de71
Show file tree

Hide file tree

Showing 2 changed files with 7 additions and 7 deletions.
diff --git a/src/ast/ast_util.cpp b/src/ast/ast_util.cpp
@@ -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) {

diff --git a/src/ast/ast_util.h b/src/ast/ast_util.h
@@ -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])))