From c5ffb012dd3d69c768133221fb391855a9773581 Mon Sep 17 00:00:00 2001
From: Murphy Berzish <murphy.berzish@gmail.com>
Date: Tue, 14 Jun 2016 16:16:39 -0400
Subject: [PATCH] axioms for StartsWith; WIP as I need to fix an infinite
 recursion bug

---
 src/smt/theory_str.cpp | 53 +++++++++++++++++++++++++++++++++++++++++-
 src/smt/theory_str.h   |  4 ++++
 2 files changed, 56 insertions(+), 1 deletion(-)

diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp
index fe8f12e81..b87881ea6 100644
--- a/src/smt/theory_str.cpp
+++ b/src/smt/theory_str.cpp
@@ -568,7 +568,7 @@ expr * theory_str::mk_concat(expr * n1, expr * n2) {
 
 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_CharAt_todo.empty() || !m_axiom_StartsWith_todo.empty()
             ;
 }
 
@@ -597,6 +597,10 @@ void theory_str::propagate() {
             instantiate_axiom_CharAt(m_axiom_CharAt_todo[i]);
         }
         m_axiom_CharAt_todo.reset();
+
+        for (unsigned i = 0; i < m_axiom_StartsWith_todo.size(); ++i) {
+            instantiate_axiom_StartsWith(m_axiom_StartsWith_todo[i]);
+        }
     }
 }
 
@@ -783,6 +787,39 @@ void theory_str::instantiate_axiom_CharAt(enode * e) {
     assert_axiom(finalAxiom);
 }
 
+void theory_str::instantiate_axiom_StartsWith(enode * e) {
+    context & ctx = get_context();
+    ast_manager & m = get_manager();
+    app * expr = e->get_owner();
+
+    TRACE("t_str_detail", tout << "instantiate StartsWith 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_vector innerItems(m);
+    innerItems.push_back(ctx.mk_eq_atom(expr->get_arg(0), mk_concat(ts0, ts1)));
+    innerItems.push_back(ctx.mk_eq_atom(mk_strlen(ts0), mk_strlen(expr->get_arg(1))));
+    innerItems.push_back(m.mk_ite(ctx.mk_eq_atom(ts0, expr->get_arg(1)), expr, m.mk_not(expr)));
+    expr_ref then1(m.mk_and(innerItems.size(), innerItems.c_ptr()), m);
+    SASSERT(then1);
+
+    // the top-level condition is Length(arg0) >= Length(arg1).
+    // of course, the integer theory is not so accommodating
+    expr_ref topLevelCond(
+            m_autil.mk_ge(
+                    m_autil.mk_add(
+                            mk_strlen(expr->get_arg(0)), m_autil.mk_mul(mk_int(-1), mk_strlen(expr->get_arg(1)))),
+                    mk_int(0))
+            , m);
+    SASSERT(topLevelCond);
+
+    expr_ref finalAxiom(m.mk_ite(topLevelCond, then1, m.mk_not(expr)), 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);
@@ -3491,6 +3528,7 @@ void theory_str::set_up_axioms(expr * ex) {
 
     sort * ex_sort = m.get_sort(ex);
     sort * str_sort = m.mk_sort(get_family_id(), STRING_SORT);
+    sort * bool_sort = m.mk_bool_sort();
 
     if (ex_sort == str_sort) {
         TRACE("t_str_detail", tout << "setting up axioms for " << mk_ismt2_pp(ex, get_manager()) <<
@@ -3526,6 +3564,19 @@ void theory_str::set_up_axioms(expr * ex) {
                 TRACE("t_str_detail", tout << "variable " << mk_ismt2_pp(ap, get_manager()) << " is #" << v << std::endl;);
             }
         }
+    } else if (ex_sort == bool_sort) {
+        TRACE("t_str_detail", tout << "setting up axioms for " << mk_ismt2_pp(ex, get_manager()) <<
+                ": expr is of sort Bool" << std::endl;);
+        // set up axioms for boolean terms
+        enode * n = ctx.get_enode(ex);
+        SASSERT(n);
+
+        if (is_app(ex)) {
+            app * ap = to_app(ex);
+            if (is_StartsWith(ap)) {
+                m_axiom_StartsWith_todo.push_back(n);
+            }
+        }
     } else {
         TRACE("t_str_detail", tout << "setting up axioms for " << mk_ismt2_pp(ex, get_manager()) <<
                 ": expr is of wrong sort, ignoring" << std::endl;);
diff --git a/src/smt/theory_str.h b/src/smt/theory_str.h
index c86328d30..6c332dbd4 100644
--- a/src/smt/theory_str.h
+++ b/src/smt/theory_str.h
@@ -108,6 +108,7 @@ namespace smt {
 
         // enode lists for term-specific axioms
         ptr_vector<enode> m_axiom_CharAt_todo;
+        ptr_vector<enode> m_axiom_StartsWith_todo;
 
         int tmpStringVarCount;
         int tmpXorVarCount;
@@ -172,11 +173,14 @@ namespace smt {
         bool is_strlen(enode const * n) const { return is_strlen(n->get_owner()); }
         bool is_CharAt(app const * a) const { return a->is_app_of(get_id(), OP_STR_CHARAT); }
         bool is_CharAt(enode const * n) const { return is_CharAt(n->get_owner()); }
+        bool is_StartsWith(app const * a) const { return a->is_app_of(get_id(), OP_STR_STARTSWITH); }
+        bool is_StartsWith(enode const * n) const { return is_StartsWith(n->get_owner()); }
         void instantiate_concat_axiom(enode * cat);
         void instantiate_basic_string_axioms(enode * str);
         void instantiate_str_eq_length_axiom(enode * lhs, enode * rhs);
 
         void instantiate_axiom_CharAt(enode * e);
+        void instantiate_axiom_StartsWith(enode * e);
 
         void set_up_axioms(expr * ex);
         void handle_equality(expr * lhs, expr * rhs);