From 7f0d9157ac9ec470f958902401e957e72871f177 Mon Sep 17 00:00:00 2001
From: Murphy Berzish <murphy.berzish@gmail.com>
Date: Sun, 6 Sep 2015 21:47:57 -0400
Subject: [PATCH] at least for now, Concat is no longer associative this means
 that we'll always have (Concat a b) instead of variadic forms

---
 src/ast/str_decl_plugin.cpp | 31 ++++++++++++++++++++-----------
 src/ast/str_decl_plugin.h   |  2 ++
 2 files changed, 22 insertions(+), 11 deletions(-)

diff --git a/src/ast/str_decl_plugin.cpp b/src/ast/str_decl_plugin.cpp
index eb309ecf0..70c8a6ebe 100644
--- a/src/ast/str_decl_plugin.cpp
+++ b/src/ast/str_decl_plugin.cpp
@@ -41,16 +41,11 @@ void str_decl_plugin::set_manager(ast_manager * m, family_id id) {
     m->inc_ref(m_str_decl);
     sort * s = m_str_decl;
 
-#define MK_AC_OP(FIELD, NAME, KIND, SORT) {                             \
-        func_decl_info info(id, KIND);                                  \
-        info.set_associative();                                         \
-        info.set_flat_associative();                                    \
-        info.set_commutative();                                         \
-        FIELD = m->mk_func_decl(symbol(NAME), SORT, SORT, SORT, info);  \
-        m->inc_ref(FIELD);                                              \
-    }
+#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)
 
-    MK_AC_OP(m_concat_decl, "Concat", OP_STRCAT, s);
+    MK_OP(m_concat_decl, "Concat", OP_STRCAT, s);
 }
 
 decl_plugin * str_decl_plugin::mk_fresh() {
@@ -64,10 +59,24 @@ sort * str_decl_plugin::mk_sort(decl_kind k, unsigned num_parameters, parameter
     }
 }
 
+func_decl * str_decl_plugin::mk_func_decl(decl_kind k) {
+    switch(k) {
+    case OP_STRCAT: return m_concat_decl;
+    default: return 0;
+    }
+}
+
 func_decl * str_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters,
                                          unsigned arity, sort * const * domain, sort * range) {
-    /* TODO */
-    m_manager->raise_exception("str_decl_plugin::mk_func_decl() not yet implemented"); return 0;
+    if (k == OP_STR) {
+        m_manager->raise_exception("OP_STR not yet implemented in mk_func_decl!");
+        return 0;
+    }
+    if (arity == 0) {
+        m_manager->raise_exception("no arguments supplied to string operator");
+        return 0;
+    }
+    return mk_func_decl(k);
 }
 
 app * str_decl_plugin::mk_string(const char * val) {
diff --git a/src/ast/str_decl_plugin.h b/src/ast/str_decl_plugin.h
index 16e1ef4a3..d190e9ff7 100644
--- a/src/ast/str_decl_plugin.h
+++ b/src/ast/str_decl_plugin.h
@@ -38,6 +38,8 @@ protected:
     func_decl * m_concat_decl;
 
     virtual void set_manager(ast_manager * m, family_id id);
+
+    func_decl * mk_func_decl(decl_kind k);
 public:
     str_decl_plugin();
     virtual ~str_decl_plugin();