theory_str Substr support WIP

src/ast/str_decl_plugin.cpp

@@ -33,6 +33,7 @@ str_decl_plugin::str_decl_plugin():
     m_indexof_decl(0),
     m_indexof2_decl(0),
     m_lastindexof_decl(0),
+    m_substr_decl(0),
     m_arith_plugin(0),
     m_arith_fid(0),
     m_int_sort(0){
@@ -53,6 +54,7 @@ void str_decl_plugin::finalize(void) {
     DEC_REF(m_indexof_decl);
     DEC_REF(m_indexof2_decl);
     DEC_REF(m_lastindexof_decl);
+    DEC_REF(m_substr_decl);
     DEC_REF(m_int_sort);
 }
 
@@ -106,6 +108,12 @@ void str_decl_plugin::set_manager(ast_manager * m, family_id id) {
 
     m_lastindexof_decl = m->mk_func_decl(symbol("LastIndexof"), s, s, i, func_decl_info(id, OP_STR_LASTINDEXOF));
     m_manager->inc_ref(m_lastindexof_decl);
+
+    {
+        sort * d[3] = {s, i, i };
+        m_substr_decl = m->mk_func_decl(symbol("Substring"), 3, d, s, func_decl_info(id, OP_STR_SUBSTR));
+        m_manager->inc_ref(m_substr_decl);
+    }
 }
 
 decl_plugin * str_decl_plugin::mk_fresh() {
@@ -130,6 +138,7 @@ func_decl * str_decl_plugin::mk_func_decl(decl_kind k) {
     case OP_STR_INDEXOF: return m_indexof_decl;
     case OP_STR_INDEXOF2: return m_indexof2_decl;
     case OP_STR_LASTINDEXOF: return m_lastindexof_decl;
+    case OP_STR_SUBSTR: return m_substr_decl;
     default: return 0;
     }
 }
@@ -193,6 +202,7 @@ void str_decl_plugin::get_op_names(svector<builtin_name> & op_names, symbol cons
     op_names.push_back(builtin_name("Indexof", OP_STR_INDEXOF));
     op_names.push_back(builtin_name("Indexof2", OP_STR_INDEXOF2));
     op_names.push_back(builtin_name("LastIndexof", OP_STR_LASTINDEXOF));
+    op_names.push_back(builtin_name("Substring", OP_STR_SUBSTR));
 }
 
 void str_decl_plugin::get_sort_names(svector<builtin_name> & sort_names, symbol const & logic) {

src/ast/str_decl_plugin.h

@@ -38,6 +38,7 @@ enum str_op_kind {
     OP_STR_INDEXOF,
     OP_STR_INDEXOF2,
     OP_STR_LASTINDEXOF,
+    OP_STR_SUBSTR,
     // end
     LAST_STR_OP
 };
@@ -57,6 +58,7 @@ protected:
     func_decl * m_indexof_decl;
     func_decl * m_indexof2_decl;
     func_decl * m_lastindexof_decl;
+    func_decl * m_substr_decl;
 
     arith_decl_plugin * m_arith_plugin;
     family_id           m_arith_fid;

src/smt/theory_str.cpp

@@ -612,6 +612,7 @@ bool theory_str::can_propagate() {
     return !m_basicstr_axiom_todo.empty() || !m_str_eq_todo.empty() || !m_concat_axiom_todo.empty()
             || !m_axiom_CharAt_todo.empty() || !m_axiom_StartsWith_todo.empty() || !m_axiom_EndsWith_todo.empty()
             || !m_axiom_Contains_todo.empty() || !m_axiom_Indexof_todo.empty() || !m_axiom_Indexof2_todo.empty() || !m_axiom_LastIndexof_todo.empty()
+            || !m_axiom_Substr_todo.empty()
             ;
 }
 
@@ -670,6 +671,11 @@ void theory_str::propagate() {
             instantiate_axiom_LastIndexof(m_axiom_LastIndexof_todo[i]);
         }
         m_axiom_LastIndexof_todo.reset();
+
+        for (unsigned i = 0; i < m_axiom_Substr_todo.size(); ++i) {
+            instantiate_axiom_Substr(m_axiom_Substr_todo[i]);
+        }
+        m_axiom_Substr_todo.reset();
     }
 }
 
@@ -1150,6 +1156,42 @@ void theory_str::instantiate_axiom_LastIndexof(enode * e) {
     assert_axiom(finalAxiom);
 }
 
+void theory_str::instantiate_axiom_Substr(enode * e) {
+    context & ctx = get_context();
+    ast_manager & m = get_manager();
+
+    app * expr = e->get_owner();
+    if (axiomatized_terms.contains(expr)) {
+        TRACE("t_str_detail", tout << "already set up Substr axiom for " << mk_pp(expr, m) << std::endl;);
+        return;
+    }
+    axiomatized_terms.insert(expr);
+
+    TRACE("t_str_detail", tout << "instantiate Substr axiom for " << mk_pp(expr, m) << std::endl;);
+
+    expr_ref ts0(mk_str_var("ts0"), m);
+    expr_ref ts1(mk_str_var("ts1"), m);
+    expr_ref ts2(mk_str_var("ts2"), m);
+
+    expr_ref ts0_contains_ts1(mk_contains(expr->get_arg(0), ts1), m);
+
+    expr_ref_vector and_item(m);
+    and_item.push_back(ts0_contains_ts1);
+    and_item.push_back(ctx.mk_eq_atom(expr->get_arg(0), mk_concat(ts0, mk_concat(ts1, ts2))));
+    and_item.push_back(ctx.mk_eq_atom(expr->get_arg(1), mk_strlen(ts0)));
+    and_item.push_back(ctx.mk_eq_atom(expr->get_arg(2), mk_strlen(ts1)));
+
+    expr_ref breakdownAssert(m.mk_and(and_item.size(), and_item.c_ptr()), m);
+    SASSERT(breakdownAssert);
+
+    expr_ref reduceToVar(ctx.mk_eq_atom(expr, ts1), m);
+    SASSERT(reduceToVar);
+
+    expr_ref finalAxiom(m.mk_and(breakdownAssert, reduceToVar), m);
+    SASSERT(finalAxiom);
+    assert_axiom(finalAxiom);
+}
+
 void theory_str::attach_new_th_var(enode * n) {
     context & ctx = get_context();
     theory_var v = mk_var(n);

src/smt/theory_str.h

@@ -115,6 +115,7 @@ namespace smt {
         ptr_vector<enode> m_axiom_Indexof_todo;
         ptr_vector<enode> m_axiom_Indexof2_todo;
         ptr_vector<enode> m_axiom_LastIndexof_todo;
+        ptr_vector<enode> m_axiom_Substr_todo;
 
         // hashtable of all exprs for which we've already set up term-specific axioms --
         // this prevents infinite recursive descent with respect to axioms that
@@ -199,6 +200,8 @@ namespace smt {
         bool is_Indexof2(enode const * n) const { return is_Indexof2(n->get_owner()); }
         bool is_LastIndexof(app const * a) const { return a->is_app_of(get_id(), OP_STR_LASTINDEXOF); }
         bool is_LastIndexof(enode const * n) const { return is_LastIndexof(n->get_owner()); }
+        bool is_Substr(app const * a) const { return a->is_app_of(get_id(), OP_STR_SUBSTR); }
+        bool is_Substr(enode const * n) const { return is_Substr(n->get_owner()); }
 
         void instantiate_concat_axiom(enode * cat);
         void instantiate_basic_string_axioms(enode * str);
@@ -211,6 +214,7 @@ namespace smt {
         void instantiate_axiom_Indexof(enode * e);
         void instantiate_axiom_Indexof2(enode * e);
         void instantiate_axiom_LastIndexof(enode * e);
+        void instantiate_axiom_Substr(enode * e);
 
         void set_up_axioms(expr * ex);
         void handle_equality(expr * lhs, expr * rhs);