From f8d328b1fb9fe0785886d8eef768e55fa1ba744a Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 18 May 2020 19:10:00 -0700
Subject: [PATCH] add nullable, get-head-tail with Caleb

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/ast/ast_util.h                |  2 +
 src/ast/rewriter/seq_rewriter.cpp | 73 +++++++++++++++++++++++++++++++
 src/ast/rewriter/seq_rewriter.h   |  3 ++
 3 files changed, 78 insertions(+)

diff --git a/src/ast/ast_util.h b/src/ast/ast_util.h
index 72ae3e74b..c48a55146 100644
--- a/src/ast/ast_util.h
+++ b/src/ast/ast_util.h
@@ -102,6 +102,7 @@ expr * get_clause_literal(ast_manager & m, expr * cls, unsigned idx);
  */
 expr * mk_and(ast_manager & m, unsigned num_args, expr * const * args);
 app  * mk_and(ast_manager & m, unsigned num_args, app * const * args);
+inline expr * mk_and(ast_manager & m, expr* a, expr* b) { expr* args[2] = { a, b }; return mk_and(m, 2, args); }
 inline app_ref mk_and(app_ref_vector const& args) { return app_ref(mk_and(args.get_manager(), args.size(), args.c_ptr()), args.get_manager()); }
 inline expr_ref mk_and(expr_ref_vector const& args) { return expr_ref(mk_and(args.get_manager(), args.size(), args.c_ptr()), args.get_manager()); }
 
@@ -123,6 +124,7 @@ app_ref operator+(expr_ref& a, expr_ref& b);
  */
 expr * mk_or(ast_manager & m, unsigned num_args, expr * const * args);
 app  * mk_or(ast_manager & m, unsigned num_args, app * const * args);
+inline expr * mk_or(ast_manager & m, expr* a, expr* b) { expr* args[2] = { a, b }; return mk_or(m, 2, args); }
 inline app_ref mk_or(app_ref_vector const& args) { return app_ref(mk_or(args.get_manager(), args.size(), args.c_ptr()), args.get_manager()); }
 inline expr_ref mk_or(expr_ref_vector const& args) { return expr_ref(mk_or(args.get_manager(), args.size(), args.c_ptr()), args.get_manager()); }
 
diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp
index f363b58e6..cc2b309f5 100644
--- a/src/ast/rewriter/seq_rewriter.cpp
+++ b/src/ast/rewriter/seq_rewriter.cpp
@@ -1963,6 +1963,79 @@ bool seq_rewriter::is_sequence(expr* e, expr_ref_vector& seq) {
     return true;
 }
 
+bool seq_rewriter::get_head_tail(expr* s, expr_ref& head, expr_ref& tail) {
+    expr* h = nullptr, *t = nullptr;
+    zstring s1;
+    if (m_util.str.is_unit(s, h)) {
+        head = h;
+        tail = m_util.str.mk_empty(m().get_sort(s));
+        return true;
+    }
+    if (m_util.str.is_string(s, s1) && s1.length() > 0) {
+        head = m_util.str.mk_string(s1.extract(0, 1));
+        tail = m_util.str.mk_string(s1.extract(1, s1.length()));
+        return true;    
+    }
+    if (m_util.str.is_concat(s, h, t) && get_head_tail(h, head, tail)) {
+        tail = m_util.str.mk_concat(tail, t);
+        return true;
+    }
+    return false;
+}
+
+expr_ref seq_rewriter::is_nullable(expr* r) {
+    SASSERT(m_util.is_re(r));
+    expr* r1 = nullptr, *r2 = nullptr;
+    unsigned lo = 0, hi = 0;
+    if (m_util.re.is_concat(r, r1, r2)) {
+        return expr_ref(mk_and(m(), is_nullable(r1), is_nullable(r2)), m());
+    }
+    if (m_util.re.is_union(r, r1, r2)) {
+        return expr_ref(mk_or(m(), is_nullable(r1), is_nullable(r2)), m());
+    }
+    if (m_util.re.is_intersection(r, r1, r2)) {
+        return expr_ref(mk_and(m(), is_nullable(r1), is_nullable(r2)), m());
+    }
+    if (m_util.re.is_star(r) || 
+             m_util.re.is_opt(r) ||
+             m_util.re.is_full_seq(r)) {
+        return expr_ref(m().mk_true(), m());
+    }
+    if (m_util.re.is_full_char(r) ||
+             m_util.re.is_empty(r) ||
+             m_util.re.is_of_pred(r)) {
+        return expr_ref(m().mk_false(), m());
+    }
+    if (m_util.re.is_plus(r, r1)) {
+        return is_nullable(r1);
+    }
+    if (m_util.re.is_range(r, r1, r2)) {
+        if (m_util.is_const_char(r1, lo) && m_util.is_const_char(r2, hi)) {
+            return expr_ref(m().mk_bool_val(lo > hi), m());
+        }
+        else {
+            return expr_ref(m_util.mk_lt(r2, r1), m());
+        }
+    }
+    if (m_util.re.is_complement(r, r1)) {
+        return expr_ref(mk_not(m(), is_nullable(r1)), m());
+    }
+    if (m_util.re.is_loop(r, r1, lo) || m_util.re.is_loop(r, r1, lo, hi)) {
+        if (lo == 0) {
+            return expr_ref(m().mk_true(), m());
+        }
+        else if (hi == 0) {
+            return expr_ref(m().mk_false(), m());
+        }
+        else {
+            return is_nullable(r1);
+        }
+    }
+    sort* seq_sort = nullptr;
+    VERIFY(m_util.is_re(r, seq_sort));
+    return expr_ref(m_util.re.mk_in_re(m_util.str.mk_empty(seq_sort), r), m());
+}
+
 br_status seq_rewriter::mk_str_in_regexp(expr* a, expr* b, expr_ref& result) {
     if (m_util.re.is_empty(b)) {
         result = m().mk_false();
diff --git a/src/ast/rewriter/seq_rewriter.h b/src/ast/rewriter/seq_rewriter.h
index b52167f9d..c2cf2cab8 100644
--- a/src/ast/rewriter/seq_rewriter.h
+++ b/src/ast/rewriter/seq_rewriter.h
@@ -132,6 +132,9 @@ class seq_rewriter {
     }
     length_comparison compare_lengths(unsigned sza, expr* const* as, unsigned szb, expr* const* bs);
 
+    bool get_head_tail(expr* e, expr_ref& head, expr_ref& tail);
+    expr_ref is_nullable(expr* r);
+
     br_status mk_seq_unit(expr* e, expr_ref& result);
     br_status mk_seq_concat(expr* a, expr* b, expr_ref& result);
     br_status mk_seq_length(expr* a, expr_ref& result);