From 9dd8ebb474aa291c494f31625a602d429579c376 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 27 May 2020 10:10:13 -0700
Subject: [PATCH] fix build

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/ast/rewriter/arith_rewriter.cpp | 13 ++++++++++---
 src/ast/rewriter/arith_rewriter.h   |  5 +++--
 src/smt/seq_regex.cpp               | 26 ++++++++++----------------
 3 files changed, 23 insertions(+), 21 deletions(-)

diff --git a/src/ast/rewriter/arith_rewriter.cpp b/src/ast/rewriter/arith_rewriter.cpp
index 860ad2a48..471cb7643 100644
--- a/src/ast/rewriter/arith_rewriter.cpp
+++ b/src/ast/rewriter/arith_rewriter.cpp
@@ -22,6 +22,13 @@ Notes:
 #include "math/polynomial/algebraic_numbers.h"
 #include "ast/ast_pp.h"
 
+seq_util& arith_rewriter_core::seq() {
+    if (!m_seq) {
+        m_seq = alloc(seq_util, m());
+    }
+    return *m_seq;
+}
+
 void arith_rewriter::updt_local_params(params_ref const & _p) {
     arith_rewriter_params p(_p);
     m_arith_lhs       = p.arith_lhs();
@@ -247,10 +254,10 @@ bool arith_rewriter::is_non_negative(expr* e) {
         unsigned pu;
         return m_util.is_power(e, n, p) && m_util.is_unsigned(p, pu) && (pu % 2 == 0);
     };
-    if (m_seq.str.is_length(e))
-        return true;
     if (is_even_power(e)) 
         return true;
+    if (seq().str.is_length(e))
+        return true;
     if (!m_util.is_mul(e)) 
         return false;
     expr_mark mark;
@@ -260,7 +267,7 @@ bool arith_rewriter::is_non_negative(expr* e) {
     for (expr* arg : args) {
         if (is_even_power(arg))
             continue;
-        if (m_seq.str.is_length(e))
+        if (seq().str.is_length(e))
             continue;
         if (m_util.is_numeral(arg, r)) {
             if (r.is_neg()) 
diff --git a/src/ast/rewriter/arith_rewriter.h b/src/ast/rewriter/arith_rewriter.h
index 06a565bb3..479180e00 100644
--- a/src/ast/rewriter/arith_rewriter.h
+++ b/src/ast/rewriter/arith_rewriter.h
@@ -27,13 +27,14 @@ class arith_rewriter_core {
 protected:
     typedef rational numeral;
     arith_util  m_util;
-    seq_util    m_seq;
+    scoped_ptr<seq_util> m_seq;
     bool        m_expand_power;
     bool        m_mul2power;
     bool        m_expand_tan;
     
     ast_manager & m() const { return m_util.get_manager(); }
     family_id get_fid() const { return m_util.get_family_id(); }
+    seq_util& seq();
     
     bool is_numeral(expr * n) const { return m_util.is_numeral(n); }
     bool is_numeral(expr * n, numeral & r) const { return m_util.is_numeral(n, r); }
@@ -45,7 +46,7 @@ protected:
     bool use_power() const { return m_mul2power && !m_expand_power; }
     decl_kind power_decl_kind() const { return OP_POWER; }
 public:
-    arith_rewriter_core(ast_manager & m):m_util(m), m_seq(m) {}
+    arith_rewriter_core(ast_manager & m):m_util(m) {}
     bool is_zero(expr * n) const { return m_util.is_zero(n); }
 };
 
diff --git a/src/smt/seq_regex.cpp b/src/smt/seq_regex.cpp
index 89f6978ac..fb15721d4 100644
--- a/src/smt/seq_regex.cpp
+++ b/src/smt/seq_regex.cpp
@@ -309,7 +309,7 @@ namespace smt {
     /**
      * is_non_empty(r, u) => nullable or not c_i or is_non_empty(r_i, u union r)
      *
-     * for each (c_i, r_i) in cofactors
+     * for each (c_i, r_i) in cofactors (min-terms)
      *
      * is_non_empty(r_i, u union r) := false if r_i in u
      *
@@ -327,24 +327,23 @@ namespace smt {
         if (!d)
             throw default_exception("derivative was not defined");
         literal_vector lits;
+        lits.push_back(~lit);
+        if (null_lit != false_literal) 
+            lits.push_back(null_lit);
         expr_ref_pair_vector cofactors(m);
         seq_rw().get_cofactors(d, cofactors);
         for (auto const& p : cofactors) {
+            if (is_member(p.second, u))
+                continue;
             expr_ref cond(p.first, m);
             seq_rw().elim_condition(hd, cond);
             rewrite(cond);
             if (m.is_false(cond))
                 continue;            
-            lits.reset();
-            lits.push_back(~lit);
-            if (!m.is_true(cond)) 
-                lits.push_back(~th.mk_literal(cond));
-            if (null_lit != false_literal) 
-                lits.push_back(null_lit);
-            if (!is_member(p.second, u))
-                lits.push_back(th.mk_literal(sk().mk_is_non_empty(p.second, re().mk_union(u, r))));
-            th.add_axiom(lits);
+            expr_ref next_non_empty = sk().mk_is_non_empty(p.second, re().mk_union(u, r));
+            lits.push_back(th.mk_literal(next_non_empty));
         }
+        th.add_axiom(lits);
     }
 
 
@@ -384,15 +383,10 @@ namespace smt {
                 continue;
             lits.reset();
             lits.push_back(~lit);
-            expr_ref is_empty1 = sk().mk_is_non_empty(p.second, re().mk_union(u, r));
-            // TBD: triple check soundness here.
-            // elim_condition(x, x = 'a') = true
-            // forall x . x = 'a' => is_empty(r, u)
-            // <=> 
-            // is_empty(r, u)
             if (!m.is_true(cond)) {
                 lits.push_back(th.mk_literal(mk_forall(m, hd, mk_not(m, cond))));
             }
+            expr_ref is_empty1 = sk().mk_is_non_empty(p.second, re().mk_union(u, r));    
             lits.push_back(th.mk_literal(is_empty1)); 
             th.add_axiom(lits);
         }