theory_str API started

src/api/api_ast.cpp

@@ -647,6 +647,12 @@ extern "C" {
         else if (fid == mk_c(c)->get_seq_fid() && k == RE_SORT) {
             return Z3_RE_SORT;
         }
+        else if (fid == mk_c(c)->get_str_fid() && k == STRING_SORT) {
+        	return Z3_STRING_SORT;
+        }
+        else if (fid == mk_c(c)->get_str_fid() && k == REGEX_SORT) {
+        	return Z3_REGEX_SORT;
+        }
         else {
             return Z3_UNKNOWN_SORT;
         }
@@ -1139,6 +1145,16 @@ extern "C" {
             }
         }
 
+        if (mk_c(c)->get_str_fid() == _d->get_family_id()) {
+        	switch (_d->get_decl_kind()) {
+        	// TODO(z3str2) add others
+        	case OP_STRCAT: return Z3_OP_STR_CONCAT;
+        	case OP_STRLEN: return Z3_OP_STR_LENGTH;
+        	default:
+        		return Z3_OP_UNINTERPRETED;
+        	}
+        }
+
         if (mk_c(c)->get_fpa_fid() == _d->get_family_id()) {
             switch (_d->get_decl_kind()) {
             case OP_FPA_RM_NEAREST_TIES_TO_EVEN: return Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN;

src/api/api_context.cpp

@@ -74,6 +74,7 @@ namespace api {
         m_fpa_util(m()),
         m_dtutil(m()),
         m_sutil(m()),
+		m_strutil(m()),
         m_last_result(m()),
         m_ast_trail(m()),
         m_pmanager(m_limit) {
@@ -98,6 +99,7 @@ namespace api {
         m_datalog_fid = m().mk_family_id("datalog_relation");
         m_fpa_fid   = m().mk_family_id("fpa");
         m_seq_fid   = m().mk_family_id("seq");
+        m_str_fid   = m().mk_family_id("str");
         m_dt_plugin = static_cast<datatype_decl_plugin*>(m().get_plugin(m_dt_fid));
     
         install_tactics(*this);

src/api/api_context.h

@@ -26,6 +26,7 @@ Revision History:
 #include"arith_decl_plugin.h"
 #include"bv_decl_plugin.h"
 #include"seq_decl_plugin.h"
+#include"str_decl_plugin.h"
 #include"datatype_decl_plugin.h"
 #include"dl_decl_plugin.h"
 #include"fpa_decl_plugin.h"
@@ -61,6 +62,8 @@ namespace api {
         datatype_util              m_dtutil;
         seq_util                   m_sutil;
 
+        str_util                   m_strutil;
+
         // Support for old solver API
         smt_params                 m_fparams;
         // -------------------------------
@@ -79,6 +82,7 @@ namespace api {
         family_id                  m_pb_fid;
         family_id                  m_fpa_fid;
         family_id                  m_seq_fid;
+        family_id                  m_str_fid;
         datatype_decl_plugin *     m_dt_plugin;
         
         std::string                m_string_buffer; // temporary buffer used to cache strings sent to the "external" world.
@@ -123,6 +127,7 @@ namespace api {
         fpa_util & fpautil() { return m_fpa_util; }
         datatype_util& dtutil() { return m_dtutil; }
         seq_util& sutil() { return m_sutil; }
+        str_util& strutil() { return m_strutil; }
         family_id get_basic_fid() const { return m_basic_fid; }
         family_id get_array_fid() const { return m_array_fid; }
         family_id get_arith_fid() const { return m_arith_fid; }
@@ -132,6 +137,7 @@ namespace api {
         family_id get_pb_fid() const { return m_pb_fid; }
         family_id get_fpa_fid() const { return m_fpa_fid; }
         family_id get_seq_fid() const { return m_seq_fid; }
+        family_id get_str_fid() const { return m_str_fid; }
         datatype_decl_plugin * get_dt_plugin() const { return m_dt_plugin; }
 
         Z3_error_code get_error_code() const { return m_error_code; }

src/api/api_str.cpp

@@ -0,0 +1,80 @@
+/*++
+Copyright (c) 2016 Microsoft Corporation
+
+Module Name:
+
+    api_str.cpp
+
+Abstract:
+
+    API for strings and regular expressions (Z3str2 implementation).
+
+Author:
+
+    Murphy Berzish (mtrberzi) 2016-10-03.
+
+Revision History:
+
+--*/
+#include<iostream>
+#include"z3.h"
+#include"api_log_macros.h"
+#include"api_context.h"
+#include"api_util.h"
+#include"ast_pp.h"
+
+extern "C" {
+
+	Z3_sort Z3_API Z3_mk_str_sort(Z3_context c) {
+		Z3_TRY;
+		LOG_Z3_mk_str_sort(c);
+		RESET_ERROR_CODE();
+		sort * ty = mk_c(c)->strutil().mk_string_sort();
+		mk_c(c)->save_ast_trail(ty);
+		RETURN_Z3(of_sort(ty));
+		Z3_CATCH_RETURN(0);
+	}
+
+	Z3_bool Z3_API Z3_is_str_sort(Z3_context c, Z3_sort s) {
+		Z3_TRY;
+		LOG_Z3_is_str_sort(c, s);
+		RESET_ERROR_CODE();
+		bool result = mk_c(c)->strutil().is_str_sort(to_sort(s));
+		return result?Z3_TRUE:Z3_FALSE;
+		Z3_CATCH_RETURN(Z3_FALSE);
+	}
+
+	Z3_bool Z3_API Z3_is_str(Z3_context c, Z3_ast s) {
+		Z3_TRY;
+		LOG_Z3_is_str(c, s);
+		RESET_ERROR_CODE();
+		bool result = mk_c(c)->strutil().is_string(to_expr(s));
+		return result ? Z3_TRUE : Z3_FALSE;
+		Z3_CATCH_RETURN(Z3_FALSE);
+	}
+
+	Z3_string Z3_API Z3_get_str(Z3_context c, Z3_ast s) {
+		Z3_TRY;
+		LOG_Z3_get_str(c, s);
+		RESET_ERROR_CODE();
+		if (!mk_c(c)->strutil().is_string(to_expr(s))) {
+			SET_ERROR_CODE(Z3_INVALID_ARG);
+			return "";
+		}
+		std::string result = mk_c(c)->strutil().get_string_constant_value(to_expr(s));
+		return mk_c(c)->mk_external_string(result);
+		Z3_CATCH_RETURN("");
+	}
+
+	Z3_ast Z3_API Z3_mk_str(Z3_context c, Z3_string str) {
+		Z3_TRY;
+		LOG_Z3_mk_str(c, str);
+		RESET_ERROR_CODE();
+		std::string s(str);
+		app * a = mk_c(c)->strutil().mk_string(str);
+		mk_c(c)->save_ast_trail(a);
+		RETURN_Z3(of_ast(a));
+		Z3_CATCH_RETURN(0);
+	}
+
+};

src/api/z3_api.h

@@ -165,6 +165,8 @@ typedef enum
     Z3_ROUNDING_MODE_SORT,
     Z3_SEQ_SORT,
     Z3_RE_SORT,
+	Z3_STRING_SORT,
+	Z3_REGEX_SORT,
     Z3_UNKNOWN_SORT = 1000
 } Z3_sort_kind;
 
@@ -1150,6 +1152,10 @@ typedef enum {
     Z3_OP_RE_CONCAT,
     Z3_OP_RE_UNION,
 
+	// theory_str
+	Z3_OP_STR_CONCAT,
+	Z3_OP_STR_LENGTH,
+
     // Auxiliary
     Z3_OP_LABEL = 0x700,
     Z3_OP_LABEL_LIT,
@@ -3145,6 +3151,57 @@ extern "C" {
 
     /*@}*/
 
+    /** @name Strings and regular expressions (Z3str2 implementation) */
+    /*@{*/
+
+    /**
+     \brief Create a string sort for 8-bit ASCII strings.
+
+     This function creates a sort for ASCII strings.
+     Each character is 8 bits.
+
+     def_API('Z3_mk_str_sort', SORT, (_in(CONTEXT), ))
+     */
+    Z3_sort Z3_API Z3_mk_str_sort(Z3_context c);
+
+    /**
+      \brief Check if \c s is a string sort.
+
+      def_API('Z3_is_str_sort', BOOL, (_in(CONTEXT), _in(SORT)))
+     */
+
+    Z3_bool Z3_API Z3_is_str_sort(Z3_context c, Z3_sort s);
+
+    /**
+      \brief Determine if \c s is a string constant.
+
+      def_API('Z3_is_str', BOOL, (_in(CONTEXT), _in(AST)))
+     */
+
+    Z3_bool Z3_API Z3_is_str(Z3_context c, Z3_ast s);
+
+    /**
+      \brief Retrieve the string constant stored in \c s.
+
+      \pre Z3_is_str(c, s)
+
+      def_API('Z3_get_str', STRING, (_in(CONTEXT), _in(AST)))
+     */
+
+    Z3_string Z3_API Z3_get_str(Z3_context c, Z3_ast s);
+
+    /**
+       \brief Create a string constant.
+
+       \param c logical context.
+       \param str The ASCII representation of the string constant.
+
+       def_API('Z3_mk_str', AST, (_in(CONTEXT), _in(STRING)))
+    */
+    Z3_ast Z3_API Z3_mk_str(Z3_context c, Z3_string str);
+
+    /*@}*/
+
     /** @name Sequences and regular expressions */
     /*@{*/
 

src/ast/str_decl_plugin.cpp

@@ -322,4 +322,5 @@ str_util::str_util(ast_manager &m) :
     m_manager(m) {
     SASSERT(m.has_plugin(symbol("str")));
     m_plugin = static_cast<str_decl_plugin*>(m.get_plugin(m.mk_family_id(symbol("str"))));
+    m_fid = m_plugin->get_family_id();
 }

src/ast/str_decl_plugin.h

@@ -120,6 +120,8 @@ public:
     family_id get_fid() const { return m_afid; }
     family_id get_family_id() const { return get_fid(); }
 
+    bool is_str_sort(sort* s) const { return is_sort_of(s, m_afid, STRING_SORT); }
+
     bool is_string(expr const * n, const char ** val) const;
     bool is_string(expr const * n) const;
 
@@ -135,11 +137,14 @@ public:
 class str_util : public str_recognizers {
     ast_manager & m_manager;
     str_decl_plugin * m_plugin;
+    family_id m_fid;
 public:
     str_util(ast_manager & m);
     ast_manager & get_manager() const { return m_manager; }
     str_decl_plugin & plugin() { return *m_plugin; }
 
+    sort* mk_string_sort() const { return get_manager().mk_sort(m_fid, STRING_SORT, 0, 0); }
+
     app * mk_string(const char * val) {
         return m_plugin->mk_string(val);
     }