hoisting out blocker for empty

#5693
Z3Prover · Dec 13, 2021 · 9ec0f94 · 9ec0f94
1 parent fcdf8d4
commit 9ec0f94
Show file tree

Hide file tree

Showing 2 changed files with 33 additions and 18 deletions.
diff --git a/src/smt/seq_regex.cpp b/src/smt/seq_regex.cpp
@@ -235,6 +235,31 @@ namespace smt {
 
     }
 
+    bool seq_regex::block_if_empty(expr* r, literal lit) {
+        auto info = re().get_info(r);
+
+        //if the minlength of the regex is UINT_MAX then the regex is a deadend
+        if (re().is_empty(r) || info.min_length == UINT_MAX) {
+            STRACE("seq_regex_brief", tout << "(empty) ";);
+            th.add_axiom(~lit);
+            return true;
+        }
+
+        if (info.interpreted) {
+            std::cout << "recur: " << r->get_id() << "\n";
+            std::cout << mk_pp(r, m) << "\n";
+            update_state_graph(r);
+
+            if (m_state_graph.is_dead(get_state_id(r))) {
+                STRACE("seq_regex_brief", tout << "(dead) ";);
+                th.add_axiom(~lit);
+                return true;
+            }
+        }
+        return false;
+    }
+
+
     /**
      * Propagate the atom (accept s i r)
      *
@@ -271,24 +296,8 @@ namespace smt {
                                        << "PA(" << mk_pp(s, m) << "@" << idx
                                        << "," << state_str(r) << ") ";);
 
-        auto info = re().get_info(r);
-
-        //if the minlength of the regex is UINT_MAX then the regex is a deadend
-        if (re().is_empty(r) || info.min_length == UINT_MAX) {
-            STRACE("seq_regex_brief", tout << "(empty) ";);
-            th.add_axiom(~lit);
+        if (block_if_empty(r, lit))
             return;
-        }
-
-        if (info.interpreted) {
-            update_state_graph(r);
-
-            if (m_state_graph.is_dead(get_state_id(r))) {
-                STRACE("seq_regex_brief", tout << "(dead) ";);
-                th.add_axiom(~lit);
-                return;
-            }
-        }
 
         if (block_unfolding(lit, idx)) {
             STRACE("seq_regex_brief", tout << "(blocked) ";);
@@ -544,6 +553,10 @@ namespace smt {
         expr* e = ctx.bool_var2expr(lit.var()), *r = nullptr, *u = nullptr, *n = nullptr;
         VERIFY(sk().is_is_non_empty(e, r, u, n));
 
+        if (block_if_empty(r, lit))
+            return;
+
+
         TRACE("seq_regex", tout << "propagate nonempty: " << mk_pp(e, m) << std::endl;);
         STRACE("seq_regex_brief", tout
             << std::endl << "PNE(" << expr_id_str(e) << "," << state_str(r)
@@ -553,6 +566,7 @@ namespace smt {
         if (m.is_true(is_nullable)) 
             return;
 
+
         literal null_lit = th.mk_literal(is_nullable);
         expr_ref hd = mk_first(r, n);
         expr_ref d(m);
@@ -845,7 +859,6 @@ namespace smt {
         return m_state_to_expr.get(id - 1);
     }
 
-
     bool seq_regex::can_be_in_cycle(expr *r1, expr *r2) {
         // TBD: This can be used to optimize the state graph:
         // return false here if it is known that r1 -> r2 can never be

diff --git a/src/smt/seq_regex.h b/src/smt/seq_regex.h
@@ -184,6 +184,8 @@ namespace smt {
             }
         }
 
+        bool block_if_empty(expr* r, literal lit);
+
     public:
 
         seq_regex(theory_seq& th);