From 8ed86d2f19a074dd68d10ca5832a4cfa18351cbb Mon Sep 17 00:00:00 2001
From: Murphy Berzish <murphy.berzish@gmail.com>
Date: Tue, 29 Sep 2015 18:02:05 -0400
Subject: [PATCH] add concatenation axiom

---
 src/smt/theory_str.cpp | 16 ++++++++++++++--
 src/smt/theory_str.h   |  1 +
 2 files changed, 15 insertions(+), 2 deletions(-)

diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp
index f9fb7e3a4..ea7b84d62 100644
--- a/src/smt/theory_str.cpp
+++ b/src/smt/theory_str.cpp
@@ -142,7 +142,7 @@ app * theory_str::mk_concat(app * e1, app * e2) {
 }
 
 bool theory_str::can_propagate() {
-    return !m_basicstr_axiom_todo.empty() || !m_str_eq_todo.empty();
+    return !m_basicstr_axiom_todo.empty() || !m_str_eq_todo.empty() || !m_concat_axiom_todo.empty();
 }
 
 void theory_str::propagate() {
@@ -160,6 +160,11 @@ void theory_str::propagate() {
             handle_equality(lhs->get_owner(), rhs->get_owner());
         }
         m_str_eq_todo.reset();
+
+        for (unsigned i = 0; i < m_concat_axiom_todo.empty(); ++i) {
+            instantiate_concat_axiom(m_concat_axiom_todo[i]);
+        }
+        m_concat_axiom_todo.reset();
     }
 }
 
@@ -167,7 +172,6 @@ void theory_str::propagate() {
  * Instantiate an axiom of the following form:
  * Length(Concat(x, y)) = Length(x) + Length(y)
  */
-// TODO this isn't used yet
 void theory_str::instantiate_concat_axiom(enode * cat) {
     SASSERT(is_concat(cat));
     app * a_cat = cat->get_owner();
@@ -321,6 +325,7 @@ void theory_str::reset_eh() {
     TRACE("t_str", tout << "resetting" << std::endl;);
     m_basicstr_axiom_todo.reset();
     m_str_eq_todo.reset();
+    m_concat_axiom_todo.reset();
     pop_scope_eh(0);
 }
 
@@ -767,6 +772,8 @@ void theory_str::handle_equality(expr * lhs, expr * rhs) {
         }
     }
 
+    // TODO simplify_parent over eqc
+
     // TODO regex unroll? (much later)
 }
 
@@ -785,6 +792,11 @@ void theory_str::set_up_axioms(expr * ex) {
         enode * n = ctx.get_enode(ex);
         SASSERT(n);
         m_basicstr_axiom_todo.push_back(n);
+
+        // if additionally ex is a concatenation, set up concatenation axioms
+        if (is_app(ex) && is_concat(to_app(ex))) {
+            m_concat_axiom_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 ea6ec8551..458287392 100644
--- a/src/smt/theory_str.h
+++ b/src/smt/theory_str.h
@@ -57,6 +57,7 @@ namespace smt {
 
         ptr_vector<enode> m_basicstr_axiom_todo;
         svector<std::pair<enode*,enode*> > m_str_eq_todo;
+        ptr_vector<enode> m_concat_axiom_todo;
 
         int tmpXorVarCount;
         std::map<std::pair<expr*, expr*>, std::map<int, expr*> > varForBreakConcat;