From 4140afa4cb276377f15aeb10dc945b5af450a3c7 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 11 Apr 2017 10:49:42 +0800 Subject: [PATCH] add regular expression membership for range of int.to.str functions. Issue #957 Signed-off-by: Nikolaj Bjorner --- src/ast/seq_decl_plugin.h | 1 + src/smt/theory_seq.cpp | 11 +++++++++++ 2 files changed, 12 insertions(+) diff --git a/src/ast/seq_decl_plugin.h b/src/ast/seq_decl_plugin.h index a7e534bbb..2882e905d 100644 --- a/src/ast/seq_decl_plugin.h +++ b/src/ast/seq_decl_plugin.h @@ -304,6 +304,7 @@ public: app* mk_to_re(expr* s) { return m.mk_app(m_fid, OP_SEQ_TO_RE, 1, &s); } app* mk_in_re(expr* s, expr* r) { return m.mk_app(m_fid, OP_SEQ_IN_RE, s, r); } + app* mk_range(expr* s1, expr* s2) { return m.mk_app(m_fid, OP_RE_RANGE, s1, s2); } app* mk_concat(expr* r1, expr* r2) { return m.mk_app(m_fid, OP_RE_CONCAT, r1, r2); } app* mk_union(expr* r1, expr* r2) { return m.mk_app(m_fid, OP_RE_UNION, r1, r2); } app* mk_inter(expr* r1, expr* r2) { return m.mk_app(m_fid, OP_RE_INTERSECT, r1, r2); } diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index 663d4cbe1..672d3c440 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -2345,6 +2345,17 @@ bool theory_seq::add_itos_axiom(expr* e) { return false; } add_axiom(mk_eq(e2, n, false)); + +#if 1 + expr_ref num_re(m), opt_re(m); + num_re = m_util.re.mk_range(m_util.str.mk_string(symbol("0")), m_util.str.mk_string(symbol("9"))); + num_re = m_util.re.mk_plus(num_re); + opt_re = m_util.re.mk_opt(m_util.re.mk_to_re(m_util.str.mk_string(symbol("-")))); + num_re = m_util.re.mk_concat(opt_re, num_re); + app_ref in_re(m_util.re.mk_in_re(e, num_re), m); + internalize_term(in_re); + propagate_in_re(in_re, true); +#endif m_trail_stack.push(push_replay(alloc(replay_axiom, m, e))); return true; }