From d57c92f69e14db91d460e32b1430acf8c428adc2 Mon Sep 17 00:00:00 2001
From: Murphy Berzish <murphy.berzish@gmail.com>
Date: Thu, 20 Oct 2016 12:25:52 -0400
Subject: [PATCH] theory_str api: concat, length

---
 src/api/api_str.cpp |  3 +++
 src/api/z3_api.h    | 13 +++++++++++++
 2 files changed, 16 insertions(+)

diff --git a/src/api/api_str.cpp b/src/api/api_str.cpp
index a42600f2f..e28c6a501 100644
--- a/src/api/api_str.cpp
+++ b/src/api/api_str.cpp
@@ -77,4 +77,7 @@ extern "C" {
 		Z3_CATCH_RETURN(0);
 	}
 
+	MK_BINARY(Z3_mk_str_concat, mk_c(c)->get_str_fid(), OP_STRCAT, SKIP);
+	MK_UNARY(Z3_mk_str_length, mk_c(c)->get_str_fid(), OP_STRLEN, SKIP);
+
 };
diff --git a/src/api/z3_api.h b/src/api/z3_api.h
index 7afba979e..c938678d6 100644
--- a/src/api/z3_api.h
+++ b/src/api/z3_api.h
@@ -3200,6 +3200,19 @@ extern "C" {
     */
     Z3_ast Z3_API Z3_mk_str(Z3_context c, Z3_string str);
 
+    /**
+       \brief Create a string concatenation term.
+       def_API('Z3_mk_str_concat', AST, (_in(CONTEXT), _in(AST), _in(AST)))
+     */
+    Z3_ast Z3_API Z3_mk_str_concat(Z3_context c, Z3_ast s1, Z3_ast s2);
+
+    /**
+       \brief Create a string length term. (Integer representation)
+       def_API('Z3_mk_str_length', AST, (_in(CONTEXT), _in(AST)))
+     */
+    Z3_ast Z3_API Z3_mk_str_length(Z3_context c, Z3_ast s);
+
+
     /*@}*/
 
     /** @name Sequences and regular expressions */