Merge pull request #988 from mtrberzi/theory_str-frontend

Frontend changes for theory_str

src/ast/ast.cpp

@@ -17,6 +17,7 @@ Revision History:
 
 --*/
 #include<sstream>
+#include<cstring>
 #include"ast.h"
 #include"ast_pp.h"
 #include"ast_ll_pp.h"

src/ast/ast.h

@@ -117,6 +117,9 @@ public:
     explicit parameter(symbol const & s): m_kind(PARAM_SYMBOL) { new (m_symbol) symbol(s); }
     explicit parameter(rational const & r): m_kind(PARAM_RATIONAL) { new (m_rational) rational(r); }
     explicit parameter(double d):m_kind(PARAM_DOUBLE), m_dval(d) {}
+    explicit parameter(const char *s):m_kind(PARAM_SYMBOL) {
+        new (m_symbol) symbol(s);
+    }
     explicit parameter(unsigned ext_id, bool):m_kind(PARAM_EXTERNAL), m_ext_id(ext_id) {}
     parameter(parameter const&);
 

src/ast/rewriter/seq_rewriter.cpp

@@ -329,7 +329,8 @@ br_status seq_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con
     switch(f->get_decl_kind()) {
 
     case OP_SEQ_UNIT:
-        return BR_FAILED;
+        SASSERT(num_args == 1);
+        return mk_seq_unit(args[0], result);
     case OP_SEQ_EMPTY:
         return BR_FAILED;
     case OP_RE_PLUS:
@@ -351,7 +352,8 @@ br_status seq_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con
         SASSERT(num_args == 2);
         return mk_re_union(args[0], args[1], result);
     case OP_RE_RANGE:
-        return BR_FAILED;    
+        SASSERT(num_args == 2);
+        return mk_re_range(args[0], args[1], result);
     case OP_RE_INTERSECT:
         SASSERT(num_args == 2);
         return mk_re_inter(args[0], args[1], result);
@@ -434,6 +436,33 @@ br_status seq_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con
     return BR_FAILED;
 }
 
+/*
+ * (seq.unit (_ BitVector 8)) ==> String constant
+ */
+br_status seq_rewriter::mk_seq_unit(expr* e, expr_ref& result) {
+    sort * s = m().get_sort(e);
+    bv_util bvu(m());
+
+    if (is_sort_of(s, bvu.get_family_id(), BV_SORT)) {
+        // specifically we want (_ BitVector 8)
+        rational n_val;
+        unsigned int n_size;
+        if (bvu.is_numeral(e, n_val, n_size)) {
+            if (n_size == 8) {
+                // convert to string constant
+                char ch = (char)n_val.get_int32();
+                TRACE("seq", tout << "rewrite seq.unit of 8-bit value " << n_val.to_string() << " to string constant \"" << ch << "\"" << std::endl;);
+                char s_tmp[2] = {ch, '\0'};
+                symbol s(s_tmp);
+                result = m_util.str.mk_string(s);
+                return BR_DONE;
+            }
+        }
+    }
+
+    return BR_FAILED;
+}
+
 /*
    string + string = string
    a + (b + c) = (a + b) + c
@@ -1401,6 +1430,39 @@ br_status seq_rewriter::mk_re_star(expr* a, expr_ref& result) {
     return BR_FAILED;
 }
 
+/*
+ * (re.range c_1 c_n) = (re.union (str.to.re c1) (str.to.re c2) ... (str.to.re cn))
+ */
+br_status seq_rewriter::mk_re_range(expr* lo, expr* hi, expr_ref& result) {
+    TRACE("seq", tout << "rewrite re.range [" << mk_pp(lo, m()) << " " << mk_pp(hi, m()) << "]\n";);
+    zstring str_lo, str_hi;
+    if (m_util.str.is_string(lo, str_lo) && m_util.str.is_string(hi, str_hi)) {
+        if (str_lo.length() == 1 && str_hi.length() == 1) {
+            unsigned int c1 = str_lo[0];
+            unsigned int c2 = str_hi[0];
+            if (c1 > c2) {
+                // exchange c1 and c2
+                unsigned int tmp = c1;
+                c2 = c1;
+                c1 = tmp;
+            }
+            zstring s(c1);
+            expr_ref acc(m_util.re.mk_to_re(m_util.str.mk_string(s)), m());
+            for (unsigned int ch = c1 + 1; ch <= c2; ++ch) {
+                zstring s_ch(ch);
+                expr_ref acc2(m_util.re.mk_to_re(m_util.str.mk_string(s_ch)), m());
+                acc = m_util.re.mk_union(acc, acc2);
+            }
+            result = acc;
+            return BR_REWRITE2;
+        } else {
+            m().raise_exception("string constants in re.range must have length 1");
+        }
+    }
+
+    return BR_FAILED;
+}
+
 /*
    emp+ = emp
    all+ = all
@@ -1430,9 +1492,9 @@ br_status seq_rewriter::mk_re_plus(expr* a, expr_ref& result) {
         return BR_DONE;
     }
 
-    return BR_FAILED;
-//  result = m_util.re.mk_concat(a, m_util.re.mk_star(a));
-//  return BR_REWRITE2;
+    //return BR_FAILED;
+    result = m_util.re.mk_concat(a, m_util.re.mk_star(a));
+    return BR_REWRITE2;
 }
 
 br_status seq_rewriter::mk_re_opt(expr* a, expr_ref& result) {

src/ast/rewriter/seq_rewriter.h

@@ -98,6 +98,7 @@ class seq_rewriter {
     re2automaton   m_re2aut;
     expr_ref_vector m_es, m_lhs, m_rhs;
 
+    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);
     br_status mk_seq_extract(expr* a, expr* b, expr* c, expr_ref& result);
@@ -119,6 +120,7 @@ class seq_rewriter {
     br_status mk_re_plus(expr* a, expr_ref& result);
     br_status mk_re_opt(expr* a, expr_ref& result);
     br_status mk_re_loop(unsigned num_args, expr* const* args, expr_ref& result);
+    br_status mk_re_range(expr* lo, expr* hi, expr_ref& result);
 
     bool set_empty(unsigned sz, expr* const* es, bool all, expr_ref_vector& lhs, expr_ref_vector& rhs);
     bool is_subsequence(unsigned n, expr* const* l, unsigned m, expr* const* r, 

src/ast/seq_decl_plugin.cpp

@@ -831,7 +831,9 @@ void seq_decl_plugin::get_sort_names(svector<builtin_name> & sort_names, symbol
     init();
     sort_names.push_back(builtin_name("Seq",   SEQ_SORT));
     sort_names.push_back(builtin_name("RegEx", RE_SORT));
+    // SMT-LIB 2.5 compatibility
     sort_names.push_back(builtin_name("String", _STRING_SORT));
+    sort_names.push_back(builtin_name("StringSequence", _STRING_SORT));
 }
 
 app* seq_decl_plugin::mk_string(symbol const& s) {

src/ast/seq_decl_plugin.h

@@ -273,6 +273,15 @@ public:
         bool is_in_re(expr const* n)    const { return is_app_of(n, m_fid, OP_SEQ_IN_RE); }
         bool is_unit(expr const* n)     const { return is_app_of(n, m_fid, OP_SEQ_UNIT); }
 
+        bool is_string_term(expr const * n) const {
+            sort * s = get_sort(n);
+            return u.is_string(s);
+        }
+
+        bool is_non_string_sequence(expr const * n) const {
+            sort * s = get_sort(n);
+            return (u.is_seq(s) && !u.is_string(s));
+        }
 
         MATCH_BINARY(is_concat);
         MATCH_UNARY(is_length);