From ff47c8632b9a6c212f68fe3e0968eaef379d4321 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 17 Aug 2017 20:28:49 -0700 Subject: [PATCH 1/7] remove reinterpret cast occurrences that require disabling strict alias analysis #987 #1210 Signed-off-by: Nikolaj Bjorner --- src/ast/ast.cpp | 8 ++++---- src/ast/ast.h | 16 +++++++--------- src/muz/spacer/spacer_sym_mux.cpp | 6 ++---- src/util/array_map.h | 5 +---- src/util/optional.h | 19 ++++++++++--------- 5 files changed, 24 insertions(+), 30 deletions(-) diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp index a1efed19e..f347a8e49 100644 --- a/src/ast/ast.cpp +++ b/src/ast/ast.cpp @@ -35,7 +35,7 @@ Revision History: parameter::~parameter() { if (m_kind == PARAM_RATIONAL) { - reinterpret_cast(m_rational)->~rational(); + dealloc(m_rational); } } @@ -50,14 +50,14 @@ parameter& parameter::operator=(parameter const& other) { return *this; } if (m_kind == PARAM_RATIONAL) { - reinterpret_cast(m_rational)->~rational(); + dealloc(m_rational); } m_kind = other.m_kind; switch(other.m_kind) { case PARAM_INT: m_int = other.get_int(); break; case PARAM_AST: m_ast = other.get_ast(); break; - case PARAM_SYMBOL: new (m_symbol) symbol(other.get_symbol()); break; - case PARAM_RATIONAL: new (m_rational) rational(other.get_rational()); break; + case PARAM_SYMBOL: m_symbol = other.m_symbol; break; + case PARAM_RATIONAL: m_rational = alloc(rational, other.get_rational()); break; case PARAM_DOUBLE: m_dval = other.m_dval; break; case PARAM_EXTERNAL: m_ext_id = other.m_ext_id; break; default: diff --git a/src/ast/ast.h b/src/ast/ast.h index 3a3f08df2..e6beec7e6 100644 --- a/src/ast/ast.h +++ b/src/ast/ast.h @@ -102,8 +102,8 @@ private: union { int m_int; // for PARAM_INT ast* m_ast; // for PARAM_AST - char m_symbol[sizeof(symbol)]; // for PARAM_SYMBOL - char m_rational[sizeof(rational)]; // for PARAM_RATIONAL + void const* m_symbol; // for PARAM_SYMBOL + rational* m_rational; // for PARAM_RATIONAL double m_dval; // for PARAM_DOUBLE (remark: this is not used in float_decl_plugin) unsigned m_ext_id; // for PARAM_EXTERNAL }; @@ -114,12 +114,10 @@ public: explicit parameter(int val): m_kind(PARAM_INT), m_int(val) {} explicit parameter(unsigned val): m_kind(PARAM_INT), m_int(val) {} explicit parameter(ast * p): m_kind(PARAM_AST), m_ast(p) {} - explicit parameter(symbol const & s): m_kind(PARAM_SYMBOL) { new (m_symbol) symbol(s); } - explicit parameter(rational const & r): m_kind(PARAM_RATIONAL) { new (m_rational) rational(r); } + explicit parameter(symbol const & s): m_kind(PARAM_SYMBOL), m_symbol(s.c_ptr()) {} + explicit parameter(rational const & r): m_kind(PARAM_RATIONAL), m_rational(alloc(rational, r)) {} explicit parameter(double d):m_kind(PARAM_DOUBLE), m_dval(d) {} - explicit parameter(const char *s):m_kind(PARAM_SYMBOL) { - new (m_symbol) symbol(s); - } + explicit parameter(const char *s):m_kind(PARAM_SYMBOL), m_symbol(symbol(s).c_ptr()) {} explicit parameter(unsigned ext_id, bool):m_kind(PARAM_EXTERNAL), m_ext_id(ext_id) {} parameter(parameter const&); @@ -156,8 +154,8 @@ public: int get_int() const { SASSERT(is_int()); return m_int; } ast * get_ast() const { SASSERT(is_ast()); return m_ast; } - symbol const & get_symbol() const { SASSERT(is_symbol()); return *(reinterpret_cast(m_symbol)); } - rational const & get_rational() const { SASSERT(is_rational()); return *(reinterpret_cast(m_rational)); } + symbol get_symbol() const { SASSERT(is_symbol()); return symbol::mk_symbol_from_c_ptr(m_symbol); } + rational const & get_rational() const { SASSERT(is_rational()); return *m_rational; } double get_double() const { SASSERT(is_double()); return m_dval; } unsigned get_ext_id() const { SASSERT(is_external()); return m_ext_id; } diff --git a/src/muz/spacer/spacer_sym_mux.cpp b/src/muz/spacer/spacer_sym_mux.cpp index da8f8eeca..c311d9990 100644 --- a/src/muz/spacer/spacer_sym_mux.cpp +++ b/src/muz/spacer/spacer_sym_mux.cpp @@ -32,10 +32,8 @@ using namespace spacer; sym_mux::sym_mux(ast_manager & m, const std::vector & suffixes) : m(m), m_ref_holder(m), m_next_sym_suffix_idx(0), m_suffixes(suffixes) { - unsigned suf_sz = m_suffixes.size(); - for (unsigned i = 0; i < suf_sz; ++i) { - symbol suff_sym = symbol(m_suffixes[i].c_str()); - m_used_suffixes.insert(suff_sym); + for (std::string const& s : m_suffixes) { + m_used_suffixes.insert(symbol(s.c_str())); } } diff --git a/src/util/array_map.h b/src/util/array_map.h index c5163715e..f3f99d015 100644 --- a/src/util/array_map.h +++ b/src/util/array_map.h @@ -63,10 +63,7 @@ class array_map { } void really_flush() { - typename vector >::iterator it = m_map.begin(); - typename vector >::iterator end = m_map.end(); - for (; it != end; ++it) { - optional & e = *it; + for (optional & e : m_map) { if (e) { m_plugin.del_eh(e->m_key, e->m_data); e.set_invalid(); diff --git a/src/util/optional.h b/src/util/optional.h index 22757f3bd..eeff35260 100644 --- a/src/util/optional.h +++ b/src/util/optional.h @@ -23,24 +23,25 @@ Revision History: template class optional { - char m_obj[sizeof(T)]; + T* m_obj; char m_initialized; void construct(const T & val) { m_initialized = 1; - new (reinterpret_cast(m_obj)) T(val); + m_obj = alloc(T, val); } void destroy() { if (m_initialized == 1) { - reinterpret_cast(m_obj)->~T(); + dealloc(m_obj); + m_obj = 0; } m_initialized = 0; } public: optional(): - m_initialized(0) {} + m_obj(0), m_initialized(0) {} explicit optional(const T & val) { construct(val); @@ -65,7 +66,7 @@ public: T * get() const { if (m_initialized == 1) { - return reinterpret_cast(m_obj); + return m_obj; } else { return 0; @@ -80,22 +81,22 @@ public: T * operator->() { SASSERT(m_initialized==1); - return reinterpret_cast(m_obj); + return m_obj; } T const * operator->() const { SASSERT(m_initialized==1); - return reinterpret_cast(m_obj); + return m_obj; } const T & operator*() const { SASSERT(m_initialized==1); - return *reinterpret_cast(m_obj); + return *m_obj; } T & operator*() { SASSERT(m_initialized==1); - return *reinterpret_cast(m_obj); + return *m_obj; } optional & operator=(const T & val) { From e1d08e95268684a0c65316906c1ad24e15d27754 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 17 Aug 2017 20:41:29 -0700 Subject: [PATCH 2/7] remove reinterpret cast occurrences that require disabling strict alias analysis #987 #1210 Signed-off-by: Nikolaj Bjorner --- CMakeLists.txt | 4 ---- scripts/mk_util.py | 8 ++++---- 2 files changed, 4 insertions(+), 8 deletions(-) diff --git a/CMakeLists.txt b/CMakeLists.txt index a3ed2a312..715679957 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -234,22 +234,18 @@ if ("${CMAKE_SYSTEM_NAME}" STREQUAL "Linux") if ("${TARGET_ARCHITECTURE}" STREQUAL "x86_64") list(APPEND Z3_COMPONENT_CXX_DEFINES "-D_USE_THREAD_LOCAL") endif() - z3_add_cxx_flag("-fno-strict-aliasing" REQUIRED) elseif ("${CMAKE_SYSTEM_NAME}" STREQUAL "Darwin") # Does OSX really not need any special flags? message(STATUS "Platform: Darwin") elseif ("${CMAKE_SYSTEM_NAME}" MATCHES "FreeBSD") message(STATUS "Platform: FreeBSD") list(APPEND Z3_COMPONENT_CXX_DEFINES "-D_FREEBSD_") - z3_add_cxx_flag("-fno-strict-aliasing" REQUIRED) elseif ("${CMAKE_SYSTEM_NAME}" MATCHES "OpenBSD") message(STATUS "Platform: OpenBSD") list(APPEND Z3_COMPONENT_CXX_DEFINES "-D_OPENBSD_") - z3_add_cxx_flag("-fno-strict-aliasing" REQUIRED) elseif (CYGWIN) message(STATUS "Platform: Cygwin") list(APPEND Z3_COMPONENT_CXX_DEFINES "-D_CYGWIN") - z3_add_cxx_flag("-fno-strict-aliasing" REQUIRED) elseif (WIN32) message(STATUS "Platform: Windows") list(APPEND Z3_COMPONENT_CXX_DEFINES "-D_WINDOWS") diff --git a/scripts/mk_util.py b/scripts/mk_util.py index d2e3d6b4c..24f22d8ee 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -2443,26 +2443,26 @@ def mk_config(): SO_EXT = '.dylib' SLIBFLAGS = '-dynamiclib' elif sysname == 'Linux': - CXXFLAGS = '%s -fno-strict-aliasing -D_LINUX_' % CXXFLAGS + CXXFLAGS = '%s -D_LINUX_' % CXXFLAGS OS_DEFINES = '-D_LINUX_' SO_EXT = '.so' LDFLAGS = '%s -lrt' % LDFLAGS SLIBFLAGS = '-shared' SLIBEXTRAFLAGS = '%s -lrt' % SLIBEXTRAFLAGS elif sysname == 'FreeBSD': - CXXFLAGS = '%s -fno-strict-aliasing -D_FREEBSD_' % CXXFLAGS + CXXFLAGS = '%s -D_FREEBSD_' % CXXFLAGS OS_DEFINES = '-D_FREEBSD_' SO_EXT = '.so' LDFLAGS = '%s -lrt' % LDFLAGS SLIBFLAGS = '-shared' SLIBEXTRAFLAGS = '%s -lrt' % SLIBEXTRAFLAGS elif sysname == 'OpenBSD': - CXXFLAGS = '%s -fno-strict-aliasing -D_OPENBSD_' % CXXFLAGS + CXXFLAGS = '%s -D_OPENBSD_' % CXXFLAGS OS_DEFINES = '-D_OPENBSD_' SO_EXT = '.so' SLIBFLAGS = '-shared' elif sysname[:6] == 'CYGWIN': - CXXFLAGS = '%s -D_CYGWIN -fno-strict-aliasing' % CXXFLAGS + CXXFLAGS = '%s -D_CYGWIN' % CXXFLAGS OS_DEFINES = '-D_CYGWIN' SO_EXT = '.dll' SLIBFLAGS = '-shared' From 66b24a6c18b26dcbf8762c73d25908caaab04617 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 17 Aug 2017 21:00:14 -0700 Subject: [PATCH 3/7] change typename to class in optional to deal with compilation Signed-off-by: Nikolaj Bjorner --- src/muz/rel/dl_interval_relation.cpp | 1 - src/util/optional.h | 2 +- 2 files changed, 1 insertion(+), 2 deletions(-) diff --git a/src/muz/rel/dl_interval_relation.cpp b/src/muz/rel/dl_interval_relation.cpp index ccb7b728b..e14d242bb 100644 --- a/src/muz/rel/dl_interval_relation.cpp +++ b/src/muz/rel/dl_interval_relation.cpp @@ -18,7 +18,6 @@ Revision History: --*/ #include "util/debug.h" -#include "util/optional.h" #include "ast/ast_pp.h" #include "muz/rel/dl_interval_relation.h" #include "muz/rel/dl_relation_manager.h" diff --git a/src/util/optional.h b/src/util/optional.h index eeff35260..5b3753ac6 100644 --- a/src/util/optional.h +++ b/src/util/optional.h @@ -21,7 +21,7 @@ Revision History: #ifndef OPTIONAL_H_ #define OPTIONAL_H_ -template +template class optional { T* m_obj; char m_initialized; From ee00852151f6e0b34f244878eaa5643a42ec3335 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 17 Aug 2017 21:09:23 -0700 Subject: [PATCH 4/7] fix compilation of tests Signed-off-by: Nikolaj Bjorner --- src/test/optional.cpp | 1 + 1 file changed, 1 insertion(+) diff --git a/src/test/optional.cpp b/src/test/optional.cpp index 46dfef82c..2ef922444 100644 --- a/src/test/optional.cpp +++ b/src/test/optional.cpp @@ -18,6 +18,7 @@ Revision History: --*/ #include "util/trace.h" #include "util/debug.h" +#include "util/memory_manager.h" #include "util/optional.h" static void tst1() { From 112fa16bc0fa516b1c6acb51db6db7fd98fbff64 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 18 Aug 2017 09:19:38 -0700 Subject: [PATCH 5/7] fix #1217 Signed-off-by: Nikolaj Bjorner --- src/smt/theory_arith_int.h | 4 +- src/smt/theory_arith_nl.h | 84 ++++++++++++-------------------------- 2 files changed, 29 insertions(+), 59 deletions(-) diff --git a/src/smt/theory_arith_int.h b/src/smt/theory_arith_int.h index 4150ecc1c..d93e062f4 100644 --- a/src/smt/theory_arith_int.h +++ b/src/smt/theory_arith_int.h @@ -239,7 +239,7 @@ namespace smt { for (; it != end; ++it) { theory_var b = it->get_base_var(); if (b == null_theory_var) { - TRACE("theory_arith_int", display_row(tout << "null: ", *it, true); ); + TRACE("arith_int", display_row(tout << "null: ", *it, true); ); continue; } bool is_tight = false; @@ -257,7 +257,7 @@ namespace smt { const_coeff = u->get_value().get_rational(); } if (!is_tight) { - TRACE("theory_arith_int", + TRACE("arith_int", display_row(tout << "!tight: ", *it, true); display_var(tout, b); ); diff --git a/src/smt/theory_arith_nl.h b/src/smt/theory_arith_nl.h index b4d30d639..9649440d2 100644 --- a/src/smt/theory_arith_nl.h +++ b/src/smt/theory_arith_nl.h @@ -681,8 +681,7 @@ namespace smt { SASSERT(is_pure_monomial(var2expr(v))); expr * m = var2expr(v); rational val(1), v_val; - for (unsigned i = 0; i < to_app(m)->get_num_args(); i++) { - expr * arg = to_app(m)->get_arg(i); + for (expr* arg : *to_app(m)) { theory_var curr = expr2var(arg); SASSERT(curr != null_theory_var); v_val = get_value(curr, computed_epsilon); @@ -742,7 +741,6 @@ namespace smt { continue; bool computed_epsilon = false; bool r = check_monomial_assignment(v, computed_epsilon); - SASSERT(!computed_epsilon); // integer variables do not use epsilon if (!r) { expr * m = get_enode(v)->get_owner(); SASSERT(is_pure_monomial(m)); @@ -1249,11 +1247,9 @@ namespace smt { } // Update the number of occurrences in the result vector. - typename var2num_occs::iterator it2 = m_var2num_occs.begin(); - typename var2num_occs::iterator end2 = m_var2num_occs.end(); - for (; it2 != end2; ++it2) { - if ((*it2).m_value > 1) - varinfo.push_back(var_num_occs((*it2).m_key, (*it2).m_value)); + for (auto const& vn : m_var2num_occs) { + if (vn.m_value > 1) + varinfo.push_back(var_num_occs(vn.m_key, vn.m_value)); } } @@ -1265,18 +1261,16 @@ namespace smt { SASSERT(!p.empty()); TRACE("p2expr_bug", display_coeff_exprs(tout, p);); ptr_buffer args; - sbuffer::const_iterator it = p.begin(); - sbuffer::const_iterator end = p.end(); - for (; it != end; ++it) { - rational const & c = it->first; - expr * var = it->second; + for (coeff_expr const& ce : p) { + rational const & c = ce.first; + expr * var = ce.second; if (!c.is_one()) { rational c2; expr * m = 0; if (m_util.is_numeral(var, c2)) - m = m_util.mk_numeral(c*c2, m_util.is_int(var)); + m = m_util.mk_numeral(c*c2, m_util.is_int(var) && c.is_int() && c2.is_int()); else - m = m_util.mk_mul(m_util.mk_numeral(c, m_util.is_int(var)), var); + m = m_util.mk_mul(m_util.mk_numeral(c, c.is_int() && m_util.is_int(var)), var); m_nl_new_exprs.push_back(m); args.push_back(m); } @@ -1453,8 +1447,7 @@ namespace smt { SASSERT(is_pure_monomial(m)); unsigned idx = 0; ptr_buffer new_args; - for (unsigned i = 0; i < to_app(m)->get_num_args(); i++) { - expr * arg = to_app(m)->get_arg(i); + for (expr * arg : *to_app(m)) { if (arg == var) { if (idx < d) idx++; @@ -1487,17 +1480,15 @@ namespace smt { tout << "min_degree: " << d << "\n";); sbuffer e; // monomials/x^d where var occurs with degree d sbuffer r; // rest - sbuffer::const_iterator it = p.begin(); - sbuffer::const_iterator end = p.end(); - for (; it != end; ++it) { - expr * m = it->second; + for (auto const& kv : p) { + expr * m = kv.second; expr * f = factor(m, var, d); if (get_degree_of(m, var) == d) { - e.push_back(coeff_expr(it->first, f)); + e.push_back(coeff_expr(kv.first, f)); } else { SASSERT(get_degree_of(m, var) > d); - r.push_back(coeff_expr(it->first, f)); + r.push_back(coeff_expr(kv.first, f)); } } expr * s = cross_nested(e, 0); @@ -1623,16 +1614,12 @@ namespace smt { return true; std::stable_sort(varinfo.begin(), varinfo.end(), var_num_occs_lt()); TRACE("cross_nested", tout << "var num occs:\n"; - sbuffer::const_iterator it = varinfo.begin(); - sbuffer::const_iterator end = varinfo.end(); - for (; it != end ; ++it) { - tout << mk_bounded_pp(it->first, get_manager()) << " -> " << it->second << "\n"; + for (auto const& kv : varinfo) { + tout << mk_bounded_pp(kv.first, get_manager()) << " -> " << kv.second << "\n"; }); - sbuffer::const_iterator it = varinfo.begin(); - sbuffer::const_iterator end = varinfo.end(); - for (; it != end; ++it) { + for (auto const& kv : varinfo) { m_nl_new_exprs.reset(); - expr * var = it->first; + expr * var = kv.first; expr * cn = cross_nested(p, var); // Remark: cn may not be well-sorted because, since a row may contain mixed integer/real monomials. // This is not really a problem, since evaluate_as_interval will work even if cn is not well-sorted. @@ -1731,10 +1718,7 @@ namespace smt { */ template bool theory_arith::is_cross_nested_consistent(svector const & nl_cluster) { - svector::const_iterator it = nl_cluster.begin(); - svector::const_iterator end = nl_cluster.end(); - for (; it != end; ++it) { - theory_var v = *it; + for (theory_var v : nl_cluster) { if (!is_base(v)) continue; m_stats.m_nl_cross_nested++; @@ -1765,10 +1749,7 @@ namespace smt { template void theory_arith::init_grobner_var_order(svector const & nl_cluster, grobner & gb) { // Initialize variable order - svector::const_iterator it = nl_cluster.begin(); - svector::const_iterator end = nl_cluster.end(); - for (; it != end; ++it) { - theory_var v = *it; + for (theory_var v : nl_cluster) { expr * var = var2expr(v); if (is_fixed(v)) { @@ -1905,10 +1886,7 @@ namespace smt { template void theory_arith::init_grobner(svector const & nl_cluster, grobner & gb) { init_grobner_var_order(nl_cluster, gb); - svector::const_iterator it = nl_cluster.begin(); - svector::const_iterator end = nl_cluster.end(); - for (; it != end; ++it) { - theory_var v = *it; + for (theory_var v : nl_cluster) { if (is_base(v)) { row const & r = m_rows[get_var_row(v)]; add_row_to_gb(r, gb); @@ -2296,10 +2274,7 @@ namespace smt { eqs.reset(); gb.get_equations(eqs); TRACE("grobner_bug", tout << "after gb\n";); - ptr_vector::const_iterator it = eqs.begin(); - ptr_vector::const_iterator end = eqs.end(); - for (; it != end; ++it) { - grobner::equation * eq = *it; + for (grobner::equation* eq : eqs) { TRACE("grobner_bug", gb.display_equation(tout, *eq);); if (is_inconsistent(eq, gb)) return GB_PROGRESS; @@ -2310,9 +2285,7 @@ namespace smt { // then assert bounds for x, and continue gb_result result = GB_FAIL; if (m_params.m_nl_arith_gb_eqs) { - it = eqs.begin(); - for (; it != end; ++it) { - grobner::equation * eq = *it; + for (grobner::equation* eq : eqs) { if (!eq->is_linear_combination()) { TRACE("non_linear", tout << "processing new equality:\n"; gb.display_equation(tout, *eq);); TRACE("non_linear_bug", tout << "processing new equality:\n"; gb.display_equation(tout, *eq);); @@ -2331,9 +2304,8 @@ namespace smt { // I only consider linear equations... (HACK) // Moreover, I do not change the weight of a variable more than once in this loop. bool modified = false; - it = eqs.begin(); - for (; it != end; ++it) { - grobner::equation const * eq = *it; + + for (grobner::equation const* eq : eqs) { unsigned num_monomials = eq->get_num_monomials(); CTRACE("grobner_bug", num_monomials <= 0, gb.display_equation(tout, *eq);); if (num_monomials == 0) @@ -2370,13 +2342,11 @@ namespace smt { bool theory_arith::max_min_nl_vars() { var_set already_found; svector vars; - for (unsigned j = 0; j < m_nl_monomials.size(); ++j) { - theory_var v = m_nl_monomials[j]; + for (theory_var v : m_nl_monomials) { mark_var(v, vars, already_found); expr * n = var2expr(v); SASSERT(is_pure_monomial(n)); - for (unsigned i = 0; i < to_app(n)->get_num_args(); i++) { - expr * curr = to_app(n)->get_arg(i); + for (expr * curr : *to_app(n)) { theory_var v = expr2var(curr); SASSERT(v != null_theory_var); mark_var(v, vars, already_found); From 6feb7ba79599fd3155ab4d4ee213c584c609c280 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 18 Aug 2017 14:27:46 -0700 Subject: [PATCH 6/7] :q add sequences to ML API Signed-off-by: Nikolaj Bjorner --- src/api/ml/z3.ml | 38 ++++++++++++++++ src/api/ml/z3.mli | 109 ++++++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 147 insertions(+) diff --git a/src/api/ml/z3.ml b/src/api/ml/z3.ml index 41d2226c5..c4a4da00c 100644 --- a/src/api/ml/z3.ml +++ b/src/api/ml/z3.ml @@ -1215,6 +1215,44 @@ struct let mk_numeral ctx v size = Z3native.mk_numeral ctx v (mk_sort ctx size) end +module Seq = +struct + let mk_seq_sort = Z3native.mk_seq_sort + let is_seq_sort = Z3native.is_seq_sort + let mk_re_sort = Z3native.mk_re_sort + let is_re_sort = Z3native.is_re_sort + let mk_string_sort = Z3native.mk_string_sort + let is_string_sort = Z3native.is_string_sort + let mk_string = Z3native.mk_string + let is_string = Z3native.is_string + let get_string = Z3native.get_string + let mk_seq_empty = Z3native.mk_seq_empty + let mk_seq_unit = Z3native.mk_seq_unit + let mk_seq_concat ctx args = Z3native.mk_seq_concat ctx (List.length args) args + let mk_seq_prefix = Z3native.mk_seq_prefix + let mk_seq_suffix = Z3native.mk_seq_suffix + let mk_seq_contains = Z3native.mk_seq_contains + let mk_seq_extract = Z3native.mk_seq_extract + let mk_seq_replace = Z3native.mk_seq_replace + let mk_seq_at = Z3native.mk_seq_at + let mk_seq_length = Z3native.mk_seq_length + let mk_seq_index = Z3native.mk_seq_index + let mk_str_to_int = Z3native.mk_str_to_int + let mk_int_to_str = Z3native.mk_int_to_str + let mk_seq_to_re = Z3native.mk_seq_to_re + let mk_seq_in_re = Z3native.mk_seq_in_re + let mk_re_plus = Z3native.mk_re_plus + let mk_re_star = Z3native.mk_re_star + let mk_re_option = Z3native.mk_re_option + let mk_re_union ctx args = Z3native.mk_re_union ctx (List.length args) args + let mk_re_concat ctx args = Z3native.mk_re_concat ctx (List.length args) args + let mk_re_range = Z3native.mk_re_range + let mk_re_loop = Z3native.mk_re_loop + let mk_re_intersect = Z3native.mk_re_intersect + let mk_re_complement = Z3native.mk_re_complement + let mk_re_empty = Z3native.mk_re_empty + let mk_re_full = Z3native.mk_re_full +end module FloatingPoint = struct diff --git a/src/api/ml/z3.mli b/src/api/ml/z3.mli index 818a635f7..7b561f878 100644 --- a/src/api/ml/z3.mli +++ b/src/api/ml/z3.mli @@ -1825,6 +1825,115 @@ sig val mk_numeral : context -> string -> int -> Expr.expr end +(** Sequences, Strings and Regular Expressions **) +module Seq : +sig + val mk_seq_sort : context -> Sort.sort -> Sort.sort + + (* test if sort is a sequence sort *) + val is_seq_sort : context -> Sort.sort -> bool + + (* create regular expression sorts over sequences of the argument sort *) + val mk_re_sort : context -> Sort.sort -> Sort.sort + + (* test if sort is a regular expression sort *) + val is_re_sort : context -> Sort.sort -> bool + + (* create string sort *) + val mk_string_sort : context -> Sort.sort + + (* test if sort is a string sort (a sequence of 8-bit bit-vectors) *) + val is_string_sort : context -> Sort.sort -> bool + + (* create a string literal *) + val mk_string : context -> string -> Expr.expr + + (* test if expression is a string *) + val is_string : context -> Expr.expr -> bool + + (* retrieve string from string Expr.expr *) + val get_string : context -> Expr.expr -> string + + (* the empty sequence over base sort *) + val mk_seq_empty : context -> Sort.sort -> Expr.expr + + (* a unit sequence *) + val mk_seq_unit : context -> Expr.expr -> Expr.expr + + (* sequence concatenation *) + val mk_seq_concat : context -> Expr.expr list -> Expr.expr + + (* predicate if the first argument is a prefix of the second *) + val mk_seq_prefix : context -> Expr.expr -> Expr.expr -> Expr.expr + + (* predicate if the first argument is a suffix of the second *) + val mk_seq_suffix : context -> Expr.expr -> Expr.expr -> Expr.expr + + (* predicate if the first argument contains the second *) + val mk_seq_contains : context -> Expr.expr -> Expr.expr -> Expr.expr + + (* extract sub-sequence starting at index given by second argument and of length provided by third argument *) + val mk_seq_extract : context -> Expr.expr -> Expr.expr -> Expr.expr -> Expr.expr + + (* replace first occurrence of second argument by third *) + val mk_seq_replace : context -> Expr.expr -> Expr.expr -> Expr.expr -> Expr.expr + + (* a unit sequence at index provided by second argument *) + val mk_seq_at : context -> Expr.expr -> Expr.expr -> Expr.expr + + (* length of a sequence *) + val mk_seq_length : context -> Expr.expr -> Expr.expr + + (* index of the first occurrence of the second argument in the first *) + val mk_seq_index : context -> Expr.expr -> Expr.expr -> Expr.expr -> Expr.expr + + (* retrieve integer expression encoded in string *) + val mk_str_to_int : context -> Expr.expr -> Expr.expr + + (* convert an integer expression to a string *) + val mk_int_to_str : context -> Expr.expr -> Expr.expr + + (* create regular expression that accepts the argument sequence *) + val mk_seq_to_re : context -> Expr.expr -> Expr.expr + + (* regular expression membership predicate *) + val mk_seq_in_re : context -> Expr.expr -> Expr.expr -> Expr.expr + + (* regular expression plus *) + val mk_re_plus : context -> Expr.expr -> Expr.expr + + (* regular expression star *) + val mk_re_star : context -> Expr.expr -> Expr.expr + + (* optional regular expression *) + val mk_re_option : context -> Expr.expr -> Expr.expr + + (* union of regular expressions *) + val mk_re_union : context -> Expr.expr list -> Expr.expr + + (* concatenation of regular expressions* ) + val mk_re_concat : context -> Expr.expr list -> Expr.expr + + (* regular expression for the range between two characters *) + val mk_re_range : context -> Expr.expr -> Expr.expr -> Expr.expr + + (* bounded loop regular expression *) + val mk_re_loop : context -> Expr.expr -> int -> int -> Expr.expr + + (* intersection of regular expressions *) + val mk_re_intersect : context -> int -> Expr.expr list -> Expr.expr + + (* the regular expression complement *) + val mk_re_complement : context -> Expr.expr -> Expr.expr + + (* the regular expression that accepts no sequences *) + val mk_re_empty : context -> Sort.sort -> Expr.expr + + (* the regular expression that accepts all sequences *) + val mk_re_full : context -> Sort.sort -> Expr.expr + +end + (** Floating-Point Arithmetic *) module FloatingPoint : sig From aa81d58bb0fe632a8832ec8f5a9abbd86753bf07 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 18 Aug 2017 14:29:53 -0700 Subject: [PATCH 7/7] add sequences to ML API #1214 Signed-off-by: Nikolaj Bjorner --- src/api/ml/z3.mli | 1 + 1 file changed, 1 insertion(+) diff --git a/src/api/ml/z3.mli b/src/api/ml/z3.mli index 7b561f878..0207a53ed 100644 --- a/src/api/ml/z3.mli +++ b/src/api/ml/z3.mli @@ -1828,6 +1828,7 @@ end (** Sequences, Strings and Regular Expressions **) module Seq : sig + (* create a sequence sort *) val mk_seq_sort : context -> Sort.sort -> Sort.sort (* test if sort is a sequence sort *)