basic infrastructure for string rewriting

src/ast/rewriter/rewriter.txt

@@ -7,6 +7,8 @@ The following classes implement theory specific rewriting rules:
   - array_rewriter
   - datatype_rewriter
   - fpa_rewriter
+  - seq_rewriter
+  - str_rewriter
 
 Each of them provide the method
     br_status mk_app_core(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result)

src/ast/rewriter/str_rewriter.cpp

@@ -0,0 +1,66 @@
+/*++
+Copyright (c) 2016 Microsoft Corporation
+
+Module Name:
+
+    str_rewriter.cpp
+
+Abstract:
+
+    AST rewriting rules for string terms.
+
+Author:
+
+    Murphy Berzish
+
+Notes:
+
+--*/
+
+#include"str_rewriter.h"
+#include"arith_decl_plugin.h"
+#include"ast_pp.h"
+#include"ast_util.h"
+#include"well_sorted.h"
+
+br_status str_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) {
+    SASSERT(f->get_family_id() == get_fid());
+
+    TRACE("t_str_rw", tout << "rewrite app: " << f->get_name() << std::endl;);
+
+    switch(f->get_decl_kind()) {
+    default:
+        return BR_FAILED;
+    }
+}
+
+br_status str_rewriter::mk_eq_core(expr * l, expr * r, expr_ref & result) {
+    // from seq_rewriter
+    expr_ref_vector lhs(m()), rhs(m()), res(m());
+    bool changed = false;
+    if (!reduce_eq(l, r, lhs, rhs, changed)) {
+        result = m().mk_false();
+        return BR_DONE;
+    }
+    if (!changed) {
+        return BR_FAILED;
+    }
+    for (unsigned i = 0; i < lhs.size(); ++i) {
+        res.push_back(m().mk_eq(lhs[i].get(), rhs[i].get()));
+    }
+    result = mk_and(res);
+    return BR_REWRITE3;
+}
+
+bool str_rewriter::reduce_eq(expr * l, expr * r, expr_ref_vector & lhs, expr_ref_vector & rhs, bool & change) {
+    // TODO inspect seq_rewriter::reduce_eq()
+    change = false;
+    return true;
+}
+
+bool str_rewriter::reduce_eq(expr_ref_vector& ls, expr_ref_vector& rs, expr_ref_vector& lhs, expr_ref_vector& rhs, bool& change) {
+    // TODO inspect seq_rewriter::reduce_eq()
+    change = false;
+    return true;
+}
+

src/ast/rewriter/str_rewriter.h

@@ -0,0 +1,46 @@
+/*++
+Copyright (c) 2016 Microsoft Corporation
+
+Module Name:
+
+    str_rewriter.h
+
+Abstract:
+
+    AST rewriting rules for string terms.
+
+Author:
+
+    Murphy Berzish
+
+Notes:
+
+--*/
+
+#include"str_decl_plugin.h"
+#include"arith_decl_plugin.h"
+#include"rewriter_types.h"
+#include"params.h"
+
+class str_rewriter {
+    str_util m_strutil;
+    arith_util m_autil;
+
+public:
+    str_rewriter(ast_manager & m, params_ref const & p = params_ref()) :
+        m_strutil(m), m_autil(m) {
+    }
+
+    ast_manager & m() const { return m_strutil.get_manager(); }
+    family_id get_fid() const { return m_strutil.get_family_id(); }
+
+    void updt_params(params_ref const & p) {}
+    static void get_param_descrs(param_descrs & r) {}
+
+    br_status mk_app_core(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result);
+    br_status mk_eq_core(expr * lhs, expr * rhs, expr_ref & result);
+
+    bool reduce_eq(expr * l, expr * r, expr_ref_vector & lhs, expr_ref_vector & rhs, bool & change);
+    bool reduce_eq(expr_ref_vector& ls, expr_ref_vector& rs, expr_ref_vector& lhs, expr_ref_vector& rhs, bool& change);
+
+};

src/ast/rewriter/th_rewriter.cpp

@@ -27,6 +27,7 @@ Notes:
 #include"dl_rewriter.h"
 #include"pb_rewriter.h"
 #include"seq_rewriter.h"
+#include"str_rewriter.h"
 #include"rewriter_def.h"
 #include"expr_substitution.h"
 #include"ast_smt2_pp.h"
@@ -45,6 +46,7 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
     dl_rewriter         m_dl_rw;
     pb_rewriter         m_pb_rw;
     seq_rewriter        m_seq_rw;
+    str_rewriter        m_str_rw;
     arith_util          m_a_util;
     bv_util             m_bv_util;
     unsigned long long  m_max_memory; // in bytes
@@ -79,6 +81,7 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
         m_ar_rw.updt_params(p);
         m_f_rw.updt_params(p);
         m_seq_rw.updt_params(p);
+        m_str_rw.updt_params(p);
         updt_local_params(p);
     }
 
@@ -179,6 +182,8 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
                     st = m_ar_rw.mk_eq_core(args[0], args[1], result);
                 else if (s_fid == m_seq_rw.get_fid())
                     st = m_seq_rw.mk_eq_core(args[0], args[1], result);
+                else if (s_fid == m_str_rw.get_fid())
+                    st = m_str_rw.mk_eq_core(args[0], args[1], result);
                 
                 if (st != BR_FAILED)
                     return st;
@@ -207,6 +212,8 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
             return m_pb_rw.mk_app_core(f, num, args, result);
         if (fid == m_seq_rw.get_fid())
             return m_seq_rw.mk_app_core(f, num, args, result);
+        if (fid == m_str_rw.get_fid())
+            return m_str_rw.mk_app_core(f, num, args, result);
         return BR_FAILED;
     }
 
@@ -665,6 +672,7 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
         m_dl_rw(m),
         m_pb_rw(m),
         m_seq_rw(m),
+        m_str_rw(m),
         m_a_util(m),
         m_bv_util(m),
         m_used_dependencies(m),