From ce53b368647c27176d87aa20b97414b7cc7eddf4 Mon Sep 17 00:00:00 2001 From: Murphy Berzish Date: Fri, 14 Oct 2016 12:34:11 -0400 Subject: [PATCH] theory_str API started --- src/api/api_ast.cpp | 16 ++++++++ src/api/api_context.cpp | 2 + src/api/api_context.h | 6 +++ src/api/api_str.cpp | 80 +++++++++++++++++++++++++++++++++++++ src/api/z3_api.h | 57 ++++++++++++++++++++++++++ src/ast/str_decl_plugin.cpp | 1 + src/ast/str_decl_plugin.h | 5 +++ 7 files changed, 167 insertions(+) create mode 100644 src/api/api_str.cpp diff --git a/src/api/api_ast.cpp b/src/api/api_ast.cpp index 1f16b2d35..7774efcd9 100644 --- a/src/api/api_ast.cpp +++ b/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; diff --git a/src/api/api_context.cpp b/src/api/api_context.cpp index bc48874a7..8fbb02598 100644 --- a/src/api/api_context.cpp +++ b/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(m().get_plugin(m_dt_fid)); install_tactics(*this); diff --git a/src/api/api_context.h b/src/api/api_context.h index fa6754120..0f2104a2b 100644 --- a/src/api/api_context.h +++ b/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; } diff --git a/src/api/api_str.cpp b/src/api/api_str.cpp new file mode 100644 index 000000000..a42600f2f --- /dev/null +++ b/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 +#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); + } + +}; diff --git a/src/api/z3_api.h b/src/api/z3_api.h index 114490015..7afba979e 100644 --- a/src/api/z3_api.h +++ b/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 */ /*@{*/ diff --git a/src/ast/str_decl_plugin.cpp b/src/ast/str_decl_plugin.cpp index 08358d46b..aa12e5946 100644 --- a/src/ast/str_decl_plugin.cpp +++ b/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(m.get_plugin(m.mk_family_id(symbol("str")))); + m_fid = m_plugin->get_family_id(); } diff --git a/src/ast/str_decl_plugin.h b/src/ast/str_decl_plugin.h index 5b0ca2a3a..aa8204459 100644 --- a/src/ast/str_decl_plugin.h +++ b/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); }