decl and rewriter for string StartsWith

src/ast/rewriter/str_rewriter.cpp

@@ -42,24 +42,30 @@ br_status str_rewriter::mk_str_CharAt(expr * arg0, expr * arg1, expr_ref & resul
         result = m_strutil.mk_string(resultStr);
         return BR_DONE;
     } else {
-        // TODO if we ever figure out how to assert axioms in here, add this code
+        // TODO if we ever figure out how to assert axioms in here, add the axiom code from Z3str2's strAstReduce.cpp
         return BR_FAILED;
-        /*
-        Z3_ast ts0 = my_mk_internal_string_var(t);
-        Z3_ast ts1 = my_mk_internal_string_var(t);
-        Z3_ast ts2 = my_mk_internal_string_var(t);
+    }
+}
 
-        Z3_ast cond = mk_2_and(t, Z3_mk_ge(ctx, args[1], mk_int(ctx, 0)), Z3_mk_lt(ctx, args[1], mk_length(t, args[0])));
-
-        Z3_ast and_item[3];
-        and_item[0] = Z3_mk_eq(ctx, args[0], mk_concat(t, ts0, mk_concat(t, ts1, ts2)));
-        and_item[1] = Z3_mk_eq(ctx, args[1], mk_length(t, ts0));
-        and_item[2] = Z3_mk_eq(ctx, mk_length(t, ts1), mk_int(ctx, 1));
-        Z3_ast thenBranch = Z3_mk_and(ctx, 3, and_item);
-        Z3_ast elseBranch = Z3_mk_eq(ctx, ts1, my_mk_str_value(t, ""));
-        breakdownAssert = Z3_mk_ite(ctx, cond, thenBranch, elseBranch);
-        return ts1;
-        */
+br_status str_rewriter::mk_str_StartsWith(expr * haystack, expr * needle, expr_ref & result) {
+    TRACE("t_str_rw", tout << "rewrite (StartsWith " << mk_pp(haystack, m()) << " " << mk_pp(needle, m()) << ")" << std::endl;);
+    if (m_strutil.is_string(haystack) && m_strutil.is_string(needle)) {
+        TRACE("t_str_rw", tout << "evaluating constant StartsWith predicate" << std::endl;);
+        std::string haystackStr = m_strutil.get_string_constant_value(haystack);
+        std::string needleStr = m_strutil.get_string_constant_value(needle);
+        if (haystackStr.length() < needleStr.length()) {
+            result = m().mk_false();
+            return BR_DONE;
+        } else {
+            if (haystackStr.substr(0, needleStr.length()) == needleStr) {
+                result = m().mk_true();
+            } else {
+                result = m().mk_false();
+            }
+            return BR_DONE;
+        }
+    } else {
+        return BR_FAILED;
     }
 }
 
@@ -73,6 +79,9 @@ br_status str_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con
     case OP_STR_CHARAT:
         SASSERT(num_args == 2);
         return mk_str_CharAt(args[0], args[1], result);
+    case OP_STR_STARTSWITH:
+        SASSERT(num_args == 2);
+        return mk_str_StartsWith(args[0], args[1], result);
     default:
         return BR_FAILED;
     }

src/ast/rewriter/str_rewriter.h

@@ -41,6 +41,7 @@ public:
     br_status mk_eq_core(expr * lhs, expr * rhs, expr_ref & result);
 
     br_status mk_str_CharAt(expr * arg0, expr * arg1, expr_ref & result);
+    br_status mk_str_StartsWith(expr * haystack, expr * needle, 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/str_decl_plugin.cpp

@@ -27,6 +27,7 @@ str_decl_plugin::str_decl_plugin():
     m_concat_decl(0),
     m_length_decl(0),
     m_charat_decl(0),
+    m_startswith_decl(0),
     m_arith_plugin(0),
     m_arith_fid(0),
     m_int_sort(0){
@@ -41,6 +42,7 @@ void str_decl_plugin::finalize(void) {
     DEC_REF(m_concat_decl);
     DEC_REF(m_length_decl);
     DEC_REF(m_charat_decl);
+    DEC_REF(m_startswith_decl);
     DEC_REF(m_int_sort);
 }
 
@@ -60,6 +62,8 @@ void str_decl_plugin::set_manager(ast_manager * m, family_id id) {
     m_manager->inc_ref(m_int_sort);
     sort * i = m_int_sort;
 
+    sort* boolT = m_manager->mk_bool_sort();
+
 #define MK_OP(FIELD, NAME, KIND, SORT)                                                  \
     FIELD = m->mk_func_decl(symbol(NAME), SORT, SORT, SORT, func_decl_info(id, KIND));  \
     m->inc_ref(FIELD)
@@ -71,6 +75,9 @@ void str_decl_plugin::set_manager(ast_manager * m, family_id id) {
 
     m_charat_decl = m->mk_func_decl(symbol("CharAt"), s, i, s, func_decl_info(id, OP_STR_CHARAT));
     m_manager->inc_ref(m_charat_decl);
+
+    m_startswith_decl = m->mk_func_decl(symbol("StartsWith"), s, s, boolT, func_decl_info(id, OP_STR_STARTSWITH));
+    m_manager->inc_ref(m_startswith_decl);
 }
 
 decl_plugin * str_decl_plugin::mk_fresh() {
@@ -89,6 +96,7 @@ func_decl * str_decl_plugin::mk_func_decl(decl_kind k) {
     case OP_STRCAT: return m_concat_decl;
     case OP_STRLEN: return m_length_decl;
     case OP_STR_CHARAT: return m_charat_decl;
+    case OP_STR_STARTSWITH: return m_startswith_decl;
     default: return 0;
     }
 }
@@ -146,6 +154,7 @@ void str_decl_plugin::get_op_names(svector<builtin_name> & op_names, symbol cons
     op_names.push_back(builtin_name("Concat", OP_STRCAT));
     op_names.push_back(builtin_name("Length", OP_STRLEN));
     op_names.push_back(builtin_name("CharAt", OP_STR_CHARAT));
+    op_names.push_back(builtin_name("StartsWith", OP_STR_STARTSWITH));
 }
 
 void str_decl_plugin::get_sort_names(svector<builtin_name> & sort_names, symbol const & logic) {

src/ast/str_decl_plugin.h

@@ -32,6 +32,7 @@ enum str_op_kind {
     OP_STRLEN,
     // higher-level string functions -- these are reduced to basic operations
     OP_STR_CHARAT,
+    OP_STR_STARTSWITH,
     // end
     LAST_STR_OP
 };
@@ -43,7 +44,9 @@ protected:
 
     func_decl * m_concat_decl;
     func_decl * m_length_decl;
+
     func_decl * m_charat_decl;
+    func_decl * m_startswith_decl;
 
     arith_decl_plugin * m_arith_plugin;
     family_id           m_arith_fid;