From 5bbf05c93c3b3d65b58c2a56d2cc45cfd01ad34b Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 18 May 2020 19:35:31 -0700 Subject: [PATCH] kleene Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/seq_rewriter.cpp | 10 ++++++++++ src/ast/rewriter/seq_rewriter.h | 2 ++ 2 files changed, 12 insertions(+) diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index b1f08c2b1..add6b6afd 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -1983,6 +1983,16 @@ bool seq_rewriter::get_head_tail(expr* s, expr_ref& head, expr_ref& tail) { return false; } +expr_ref seq_rewriter::kleene_and(expr* cond, expr* r) { + expr* re_empty = m_util.re.mk_empty(m().get_sort(r)); + return expr_ref(m().mk_ite(cond, r, re_empty), m()); +} + +expr_ref seq_rewriter::kleene_predicate(expr* cond, sort* seq_sort) { + expr* re_with_empty = m_util.re.mk_to_re(m_util.str.mk_empty(seq_sort)); + return kleene_and(cond, re_with_empty); +} + expr_ref seq_rewriter::is_nullable(expr* r) { SASSERT(m_util.is_re(r)); expr* r1 = nullptr, *r2 = nullptr; diff --git a/src/ast/rewriter/seq_rewriter.h b/src/ast/rewriter/seq_rewriter.h index c2cf2cab8..7b79d714c 100644 --- a/src/ast/rewriter/seq_rewriter.h +++ b/src/ast/rewriter/seq_rewriter.h @@ -134,6 +134,8 @@ class seq_rewriter { bool get_head_tail(expr* e, expr_ref& head, expr_ref& tail); expr_ref is_nullable(expr* r); + expr_ref kleene_and(expr* cond, expr* r); + expr_ref kleene_predicate(expr* cond, sort* seq_sort); br_status mk_seq_unit(expr* e, expr_ref& result); br_status mk_seq_concat(expr* a, expr* b, expr_ref& result);