diff --git a/src/api/api_ast.cpp b/src/api/api_ast.cpp index 944e447c6..db10c8bb3 100644 --- a/src/api/api_ast.cpp +++ b/src/api/api_ast.cpp @@ -641,6 +641,12 @@ extern "C" { else if (fid == mk_c(c)->get_fpa_fid() && k == ROUNDING_MODE_SORT) { return Z3_ROUNDING_MODE_SORT; } + else if (fid == mk_c(c)->get_seq_fid() && k == SEQ_SORT) { + return Z3_SEQ_SORT; + } + else if (fid == mk_c(c)->get_seq_fid() && k == RE_SORT) { + return Z3_RE_SORT; + } else { return Z3_UNKNOWN_SORT; } @@ -1108,6 +1114,32 @@ extern "C" { } } + if (mk_c(c)->get_seq_fid() == _d->get_family_id()) { + switch (_d->get_decl_kind()) { + case Z3_OP_SEQ_UNIT: return Z3_OP_SEQ_UNIT; + case Z3_OP_SEQ_EMPTY: return Z3_OP_SEQ_EMPTY; + case Z3_OP_SEQ_CONCAT: return Z3_OP_SEQ_CONCAT; + case Z3_OP_SEQ_PREFIX: return Z3_OP_SEQ_PREFIX; + case Z3_OP_SEQ_SUFFIX: return Z3_OP_SEQ_SUFFIX; + case Z3_OP_SEQ_CONTAINS: return Z3_OP_SEQ_CONTAINS; + case Z3_OP_SEQ_EXTRACT: return Z3_OP_SEQ_EXTRACT; + case Z3_OP_SEQ_REPLACE: return Z3_OP_SEQ_REPLACE; + case Z3_OP_SEQ_AT: return Z3_OP_SEQ_AT; + case Z3_OP_SEQ_LENGTH: return Z3_OP_SEQ_LENGTH; + case Z3_OP_SEQ_INDEX: return Z3_OP_SEQ_INDEX; + case Z3_OP_SEQ_TO_RE: return Z3_OP_SEQ_TO_RE; + case Z3_OP_SEQ_IN_RE: return Z3_OP_SEQ_IN_RE; + + case Z3_OP_RE_PLUS: return Z3_OP_RE_PLUS; + case Z3_OP_RE_STAR: return Z3_OP_RE_STAR; + case Z3_OP_RE_OPTION: return Z3_OP_RE_OPTION; + case Z3_OP_RE_CONCAT: return Z3_OP_RE_CONCAT; + case Z3_OP_RE_UNION: return Z3_OP_RE_UNION; + 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 9d0abe3a7..75782a28d 100644 --- a/src/api/api_context.cpp +++ b/src/api/api_context.cpp @@ -73,6 +73,7 @@ namespace api { m_datalog_util(m()), m_fpa_util(m()), m_dtutil(m()), + m_sutil(m()), m_last_result(m()), m_ast_trail(m()), m_replay_stack(), @@ -97,6 +98,7 @@ namespace api { m_dt_fid = m().mk_family_id("datatype"); 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_dt_plugin = static_cast(m().get_plugin(m_dt_fid)); if (!m_user_ref_count) { diff --git a/src/api/api_context.h b/src/api/api_context.h index 40b59d1b2..23c8d3fd2 100644 --- a/src/api/api_context.h +++ b/src/api/api_context.h @@ -25,6 +25,7 @@ Revision History: #include"api_util.h" #include"arith_decl_plugin.h" #include"bv_decl_plugin.h" +#include"seq_decl_plugin.h" #include"datatype_decl_plugin.h" #include"dl_decl_plugin.h" #include"fpa_decl_plugin.h" @@ -58,6 +59,7 @@ namespace api { datalog::dl_decl_util m_datalog_util; fpa_util m_fpa_util; datatype_util m_dtutil; + seq_util m_sutil; // Support for old solver API smt_params m_fparams; @@ -78,6 +80,7 @@ namespace api { family_id m_datalog_fid; family_id m_pb_fid; family_id m_fpa_fid; + family_id m_seq_fid; datatype_decl_plugin * m_dt_plugin; std::string m_string_buffer; // temporary buffer used to cache strings sent to the "external" world. @@ -121,6 +124,7 @@ namespace api { datalog::dl_decl_util & datalog_util() { return m_datalog_util; } fpa_util & fpautil() { return m_fpa_util; } datatype_util& dtutil() { return m_dtutil; } + seq_util& sutil() { return m_sutil; } 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; } @@ -129,6 +133,7 @@ namespace api { family_id get_datalog_fid() const { return m_datalog_fid; } 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; } 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_seq.cpp b/src/api/api_seq.cpp new file mode 100644 index 000000000..0949cc2e4 --- /dev/null +++ b/src/api/api_seq.cpp @@ -0,0 +1,151 @@ +/*++ +Copyright (c) 2016 Microsoft Corporation + +Module Name: + + api_seq.cpp + +Abstract: + + API for sequences and regular expressions. + +Author: + + Nikolaj Bjorner (nbjorner) 2016-01-02. + +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_seq_sort(Z3_context c, Z3_sort domain) { + Z3_TRY; + LOG_Z3_mk_seq_sort(c, domain); + RESET_ERROR_CODE(); + sort * ty = mk_c(c)->sutil().str.mk_seq(to_sort(domain)); + mk_c(c)->save_ast_trail(ty); + RETURN_Z3(of_sort(ty)); + Z3_CATCH_RETURN(0); + } + + Z3_sort Z3_API Z3_mk_re_sort(Z3_context c, Z3_sort domain) { + Z3_TRY; + LOG_Z3_mk_re_sort(c, domain); + RESET_ERROR_CODE(); + sort * ty = mk_c(c)->sutil().re.mk_re(to_sort(domain)); + mk_c(c)->save_ast_trail(ty); + RETURN_Z3(of_sort(ty)); + Z3_CATCH_RETURN(0); + } + + Z3_ast Z3_API Z3_mk_string(Z3_context c, Z3_string str) { + Z3_TRY; + LOG_Z3_mk_string(c, str); + RESET_ERROR_CODE(); + zstring s(str, zstring::ascii); + app* a = mk_c(c)->sutil().str.mk_string(s); + mk_c(c)->save_ast_trail(a); + RETURN_Z3(of_ast(a)); + Z3_CATCH_RETURN(0); + } + + Z3_sort Z3_API Z3_mk_string_sort(Z3_context c) { + Z3_TRY; + LOG_Z3_mk_string_sort(c); + RESET_ERROR_CODE(); + sort* ty = mk_c(c)->sutil().str.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_seq_sort(Z3_context c, Z3_sort s) { + Z3_TRY; + LOG_Z3_is_seq_sort(c, s); + RESET_ERROR_CODE(); + bool result = mk_c(c)->sutil().is_seq(to_sort(s)); + return result?Z3_TRUE:Z3_FALSE; + Z3_CATCH_RETURN(Z3_FALSE); + } + + Z3_bool Z3_API Z3_is_re_sort(Z3_context c, Z3_sort s) { + Z3_TRY; + LOG_Z3_is_re_sort(c, s); + RESET_ERROR_CODE(); + bool result = mk_c(c)->sutil().is_re(to_sort(s)); + return result?Z3_TRUE:Z3_FALSE; + Z3_CATCH_RETURN(Z3_FALSE); + } + + Z3_bool Z3_API Z3_is_string_sort(Z3_context c, Z3_sort s) { + Z3_TRY; + LOG_Z3_is_string_sort(c, s); + RESET_ERROR_CODE(); + bool result = mk_c(c)->sutil().is_string(to_sort(s)); + return result?Z3_TRUE:Z3_FALSE; + Z3_CATCH_RETURN(Z3_FALSE); + } + + Z3_bool Z3_API Z3_is_string(Z3_context c, Z3_ast s) { + Z3_TRY; + LOG_Z3_is_string(c, s); + RESET_ERROR_CODE(); + bool result = mk_c(c)->sutil().str.is_string(to_expr(s)); + return result?Z3_TRUE:Z3_FALSE; + Z3_CATCH_RETURN(Z3_FALSE); + } + + Z3_string Z3_API Z3_get_string(Z3_context c, Z3_ast s) { + Z3_TRY; + LOG_Z3_get_string(c, s); + RESET_ERROR_CODE(); + zstring str; + if (!mk_c(c)->sutil().str.is_string(to_expr(s), str)) { + SET_ERROR_CODE(Z3_INVALID_ARG); + return ""; + } + std::string result = str.encode(); + return mk_c(c)->mk_external_string(result); + Z3_CATCH_RETURN(""); + } + + Z3_ast Z3_API Z3_mk_seq_empty(Z3_context c, Z3_sort seq) { + Z3_TRY; + LOG_Z3_mk_seq_empty(c, seq); + RESET_ERROR_CODE(); + app* a = mk_c(c)->sutil().str.mk_empty(to_sort(seq)); + mk_c(c)->save_ast_trail(a); + RETURN_Z3(of_ast(a)); + Z3_CATCH_RETURN(0); + } + + MK_UNARY(Z3_mk_seq_unit, mk_c(c)->get_seq_fid(), OP_SEQ_UNIT, SKIP); + MK_NARY(Z3_mk_seq_concat, mk_c(c)->get_seq_fid(), OP_SEQ_CONCAT, SKIP); + MK_BINARY(Z3_mk_seq_prefix, mk_c(c)->get_seq_fid(), OP_SEQ_PREFIX, SKIP); + MK_BINARY(Z3_mk_seq_suffix, mk_c(c)->get_seq_fid(), OP_SEQ_SUFFIX, SKIP); + MK_BINARY(Z3_mk_seq_contains, mk_c(c)->get_seq_fid(), OP_SEQ_CONTAINS, SKIP); + MK_TERNARY(Z3_mk_seq_extract, mk_c(c)->get_seq_fid(), OP_SEQ_EXTRACT, SKIP); + MK_TERNARY(Z3_mk_seq_replace, mk_c(c)->get_seq_fid(), OP_SEQ_REPLACE, SKIP); + MK_BINARY(Z3_mk_seq_at, mk_c(c)->get_seq_fid(), OP_SEQ_AT, SKIP); + MK_UNARY(Z3_mk_seq_length, mk_c(c)->get_seq_fid(), OP_SEQ_LENGTH, SKIP); + //MK_BINARY(Z3_mk_seq_index, mk_c(c)->get_seq_fid(), OP_SEQ_INDEX, SKIP); + MK_UNARY(Z3_mk_seq_to_re, mk_c(c)->get_seq_fid(), OP_SEQ_TO_RE, SKIP); + MK_BINARY(Z3_mk_seq_in_re, mk_c(c)->get_seq_fid(), OP_SEQ_IN_RE, SKIP); + + + MK_UNARY(Z3_mk_re_plus, mk_c(c)->get_seq_fid(), OP_RE_PLUS, SKIP); + MK_UNARY(Z3_mk_re_star, mk_c(c)->get_seq_fid(), OP_RE_STAR, SKIP); + MK_UNARY(Z3_mk_re_option, mk_c(c)->get_seq_fid(), OP_RE_OPTION, SKIP); + MK_NARY(Z3_mk_re_union, mk_c(c)->get_seq_fid(), OP_RE_UNION, SKIP); + MK_NARY(Z3_mk_re_concat, mk_c(c)->get_seq_fid(), OP_RE_CONCAT, SKIP); + + + +}; diff --git a/src/api/api_util.h b/src/api/api_util.h index 9befd8849..3b7baeac0 100644 --- a/src/api/api_util.h +++ b/src/api/api_util.h @@ -135,6 +135,23 @@ Z3_ast Z3_API NAME(Z3_context c, Z3_ast n1, Z3_ast n2) { \ MK_BINARY_BODY(NAME, FID, OP, EXTRA_CODE); \ } +#define MK_TERNARY_BODY(NAME, FID, OP, EXTRA_CODE) \ + Z3_TRY; \ + RESET_ERROR_CODE(); \ + EXTRA_CODE; \ + expr * args[3] = { to_expr(n1), to_expr(n2), to_expr(n3) }; \ + ast* a = mk_c(c)->m().mk_app(FID, OP, 0, 0, 3, args); \ + mk_c(c)->save_ast_trail(a); \ + check_sorts(c, a); \ + RETURN_Z3(of_ast(a)); \ + Z3_CATCH_RETURN(0); + +#define MK_TERNARY(NAME, FID, OP, EXTRA_CODE) \ + Z3_ast Z3_API NAME(Z3_context c, Z3_ast n1, Z3_ast n2, Z3_ast n3) { \ + LOG_ ## NAME(c, n1, n2, n3); \ + MK_TERNARY_BODY(NAME, FID, OP, EXTRA_CODE); \ +} + #define MK_NARY(NAME, FID, OP, EXTRA_CODE) \ Z3_ast Z3_API NAME(Z3_context c, unsigned num_args, Z3_ast const* args) { \ Z3_TRY; \ diff --git a/src/api/python/z3.py b/src/api/python/z3.py index 864a92846..507e9bfee 100644 --- a/src/api/python/z3.py +++ b/src/api/python/z3.py @@ -930,6 +930,10 @@ def _to_expr_ref(a, ctx): return FiniteDomainRef(a, ctx) if sk == Z3_ROUNDING_MODE_SORT: return FPRMRef(a, ctx) + if sk == Z3_SEQ_SORT: + return SeqRef(a, ctx) + if sk == Z3_RE_SORT: + return ReRef(a, ctx) return ExprRef(a, ctx) def _coerce_expr_merge(s, a): @@ -3562,12 +3566,32 @@ def Concat(*args): 121 """ args = _get_args(args) + sz = len(args) + if __debug__: + _z3_assert(sz >= 2, "At least two arguments expected.") + + ctx = args[0].ctx + + if is_seq(args[0]): + if __debug__: + _z3_assert(all([is_seq(a) for a in args]), "All arguments must be sequence expressions.") + v = (Ast * sz)() + for i in range(sz): + v[i] = args[i].as_ast() + return SeqRef(Z3_mk_seq_concat(ctx.ref(), sz, v), ctx) + + if is_re(args[0]): + if __debug__: + _z3_assert(all([is_re(a) for a in args]), "All arguments must be regular expressions.") + v = (Ast * sz)() + for i in range(sz): + v[i] = args[i].as_ast() + return ReRef(Z3_mk_re_concat(ctx.ref(), sz, v), ctx) + if __debug__: _z3_assert(all([is_bv(a) for a in args]), "All arguments must be Z3 bit-vector expressions.") - _z3_assert(len(args) >= 2, "At least two arguments expected.") - ctx = args[0].ctx - r = args[0] - for i in range(len(args) - 1): + r = args[0] + for i in range(sz - 1): r = BitVecRef(Z3_mk_concat(ctx.ref(), r.as_ast(), args[i+1].as_ast()), ctx) return r @@ -7781,7 +7805,7 @@ def binary_interpolant(a,b,p=None,ctx=None): solver that determines satisfiability. x = Int('x') - print binary_interpolant(x<0,x>2) + print(binary_interpolant(x<0,x>2)) Not(x >= 0) """ f = And(Interpolant(a),b) @@ -7821,6 +7845,7 @@ def sequence_interpolant(v,p=None,ctx=None): f = And(Interpolant(f),v[i]) return tree_interpolant(f,p,ctx) + ######################################### # # Floating-Point Arithmetic @@ -8887,3 +8912,220 @@ def fpToIEEEBV(x): if __debug__: _z3_assert(is_fp(x), "First argument must be a Z3 floating-point expression") return BitVecRef(Z3_mk_fpa_to_ieee_bv(x.ctx_ref(), x.ast), x.ctx) + + + +######################################### +# +# Strings, Sequences and Regular expressions +# +######################################### + +class SeqSortRef(SortRef): + """Sequence sort.""" + + def is_string(self): + """Determine if sort is a string + >>> s = StringSort() + >>> s.is_string() + True + >>> s = SeqSort(IntSort()) + >>> s.is_string() + False + """ + return Z3_is_string_sort(self.ctx_ref(), self.ast) + +def StringSort(ctx=None): + """Create a string sort + >>> s = StringSort() + >>> print(s) + String + """ + ctx = _get_ctx(ctx) + return SeqSortRef(Z3_mk_string_sort(ctx.ref()), ctx) + + +def SeqSort(s): + """Create a sequence sort over elements provided in the argument + >>> s = SeqSort(IntSort()) + >>> s == Unit(IntVal(1)).sort() + True + """ + return SeqSortRef(Z3_mk_seq_sort(s.ctx_ref(), s.ast), s.ctx) + +class SeqRef(ExprRef): + """Sequence expression.""" + + def sort(self): + return SeqSortRef(Z3_get_sort(self.ctx_ref(), self.as_ast()), self.ctx) + + def __add__(self, other): + v = (Ast * 2)() + v[0] = self.as_ast() + v[1] = other.as_ast() + return SeqRef(Z3_mk_seq_concat(self.ctx_ref(), 2, v), self.ctx) + + def __getitem__(self, i): + return SeqRef(Z3_mk_seq_at(self.ctx_ref(), self.as_ast(), i.as_ast()), self.ctx) + + def is_string_sort(self): + return Z3_is_string_sort(self.ctx_ref(), Z3_get_sort(self.ctx_ref(), self.as_ast())) + + def is_string_value(self): + return Z3_is_string(self.ctx_ref(), self.as_ast()) + + def as_string(self): + """Return a string representation of sequence expression.""" + return Z3_ast_to_string(self.ctx_ref(), self.as_ast()) + + +def _coerce_seq(s, ctx=None): + if isinstance(s, str): + ctx = _get_ctx(ctx) + s = String(s, ctx) + return s + +def _get_ctx2(a, b): + if is_expr(a): + return a.ctx + if is_expr(b): + return b.ctx + return None + +def is_seq(a): + """Return `True` if `a` is a Z3 sequence expression.""" + return isinstance(a, SeqRef) + +def is_string_sort(a): + """Return `True` if `a` is a Z3 string expression.""" + return isinstance(a, SeqRef) and a.is_string_sort() + +def is_string_value(a): + """return 'True' if 'a' is a Z3 string constant expression.""" + return isinstance(a, SeqRef) and a.is_string_value() + +def String(s, ctx=None): + """create a string expression""" + ctx = _get_ctx(ctx) + return SeqRef(Z3_mk_string(ctx.ref(), s), ctx) + +def Empty(s): + """Create the empty sequence of the given sort + >>> e = Empty(StringSort()) + >>> print(e) + "" + >>> e2 = String("") + >>> print(e == e2) + True + >>> e3 = Empty(SeqSort(IntSort())) + >>> print(e3) + """ + return SeqRef(Z3_mk_seq_empty(s.ctx_ref(), s.as_ast()), s.ctx) + +def Unit(a): + """Create a singleton sequence""" + return SeqRef(Z3_mk_seq_unit(a.ctx_ref(), a.as_ast()), a.ctx) + +def PrefixOf(a, b): + """Check if 'a' is a prefix of 'b'""" + ctx = _get_ctx2(a, b) + a = _coerce_seq(a, ctx) + b = _coerce_seq(b, ctx) + return BoolRef(Z3_mk_seq_prefix(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx) + +def SuffixOf(a, b): + """Check if 'a' is a suffix of 'b'""" + ctx = _get_ctx2(a, b) + a = _coerce_seq(a, ctx) + b = _coerce_seq(b, ctx) + return BoolRef(Z3_mk_seq_suffix(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx) + +def Contains(a, b): + """Check if 'a' contains 'b'""" + ctx = _get_ctx2(a, b) + a = _coerce_seq(a, ctx) + b = _coerce_seq(b, ctx) + return BoolRef(Z3_mk_seq_contains(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx) + +#def Extract(a, offset, length): +# """Extract a sequence at offset with indicated length""" +# return SeqRef(Z3_mk_seq_extract(a.ctx_ref(), a.as_ast(), offset.as_ast()), length.ctx) + +def Replace(src, dst, s): + """Replace the first occurrence of 'src' by 'dst' in 's'""" + ctx = _get_ctx2(src, _get_ctx2(dst, s)) + src = _coerce_seq(src, ctx) + dst = _coerce_seq(dst, ctx) + s = _coerce_seq(s, ctx) + return SeqRef(Z3_mk_seq_replace(src.ctx_ref(), src.as_ast(), dst.as_ast()), s.ctx) + +def Length(s): + """Obtain the length of a sequence 's'""" + return ArithRef(Z3_mk_seq_length(s.ctx_ref(), s.as_ast(), s.ctx)) + +def Re(s, ctx=None): + """The regular expression that accepts sequence 's'""" + s = _coerce_seq(s, ctx) + return ReRef(Z3_mk_seq_to_re(s.ctx_ref(), s.as_ast()), s.ctx) + + + + +## Regular expressions + +class ReSortRef(SortRef): + """Regular expression sort.""" + + +def ReSort(s): + if is_ast(s): + return ReSortRef(Z3_mk_re_sort(s.ctx.ref(), s.as_ast()), ctx) + if s is None or isinstance(s, Context): + ctx = _get_ctx(s) + return ReSortRef(Z3_mk_re_sort(ctx.ref(), Z3_mk_string_sort(ctx.ref())), ctx) + raise Z3Exception("Regular expression sort constructor expects either a string or a context or no argument") + + +class ReRef(ExprRef): + """Regular expressions.""" + + def __add__(self, other): + v = (Ast * 2)() + v[0] = self.as_ast() + v[1] = other.as_ast() + return SeqRef(Z3_mk_re_union(self.ctx_ref(), 2, v), self.ctx) + + +def is_re(s): + return isinstance(s, ReRef) + +def InRe(s, re): + s = _coerce_seq(s, re.ctx) + return BoolRef(Z3_mk_seq_in_re(s.ctx_ref(), s.as_ast(), re.as_ast()), s.ctx) + +def Plus(re): + """Create the regular expression accepting one or more repetitions of argument. + >>> re = Plus(Re("a")) + >>> print(simplify(InRe("aa", re))) + True + >>> print(simplify(InRe("ab", re))) + False + >>> print(simplify(InRe("", re))) + False + """ + return ReRef(Z3_mk_re_plus(re.ctx_ref(), re.as_ast()), re.ctx) + +def Option(re): + return ReRef(Z3_mk_re_option(re.ctx_ref(), re.as_ast()), re.ctx) + +def Star(re): + """Create the regular expression accepting zero or more repetitions of argument. + >>> re = Star(Re("a")) + >>> print(simplify(InRe("aa", re))) + True + >>> print(simplify(InRe("ab", re))) + False + >>> print(simplify(InRe("", re))) + True + """ + return ReRef(Z3_mk_re_star(re.ctx_ref(), re.as_ast()), re.ctx) diff --git a/src/api/python/z3printer.py b/src/api/python/z3printer.py index adc203436..24d0359c9 100644 --- a/src/api/python/z3printer.py +++ b/src/api/python/z3printer.py @@ -570,6 +570,9 @@ class Formatter: def pp_algebraic(self, a): return to_format(a.as_decimal(self.precision)) + def pp_string(self, a): + return to_format(a.as_string()) + def pp_bv(self, a): return to_format(a.as_string()) @@ -875,6 +878,8 @@ class Formatter: return self.pp_fp_value(a) elif z3.is_fp(a): return self.pp_fp(a, d, xs) + elif z3.is_string_value(a): + return self.pp_string(a) elif z3.is_const(a): return self.pp_const(a) else: diff --git a/src/api/z3_api.h b/src/api/z3_api.h index a4a10bb85..e00134c06 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -161,6 +161,8 @@ typedef enum Z3_FINITE_DOMAIN_SORT, Z3_FLOATING_POINT_SORT, Z3_ROUNDING_MODE_SORT, + Z3_SEQ_SORT, + Z3_RE_SORT, Z3_UNKNOWN_SORT = 1000 } Z3_sort_kind; @@ -1098,7 +1100,7 @@ typedef enum { Z3_OP_PR_TH_LEMMA, Z3_OP_PR_HYPER_RESOLVE, - // Sequences + // Relational algebra Z3_OP_RA_STORE = 0x600, Z3_OP_RA_EMPTY, Z3_OP_RA_IS_EMPTY, @@ -1115,6 +1117,28 @@ typedef enum { Z3_OP_FD_CONSTANT, Z3_OP_FD_LT, + // Sequences + Z3_OP_SEQ_UNIT, + Z3_OP_SEQ_EMPTY, + Z3_OP_SEQ_CONCAT, + Z3_OP_SEQ_PREFIX, + Z3_OP_SEQ_SUFFIX, + Z3_OP_SEQ_CONTAINS, + Z3_OP_SEQ_EXTRACT, + Z3_OP_SEQ_REPLACE, + Z3_OP_SEQ_AT, + Z3_OP_SEQ_LENGTH, + Z3_OP_SEQ_INDEX, + Z3_OP_SEQ_TO_RE, + Z3_OP_SEQ_IN_RE, + + // regular expressions + Z3_OP_RE_PLUS, + Z3_OP_RE_STAR, + Z3_OP_RE_OPTION, + Z3_OP_RE_CONCAT, + Z3_OP_RE_UNION, + // Auxiliary Z3_OP_LABEL = 0x700, Z3_OP_LABEL_LIT, @@ -3093,6 +3117,213 @@ extern "C" { /*@}*/ + /** @name Sequences and regular expressions */ + /*@{*/ + + /** + \brief Create a sequence sort out of the sort for the elements. + + def_API('Z3_mk_seq_sort', SORT, (_in(CONTEXT), _in(SORT))) + */ + Z3_sort Z3_API Z3_mk_seq_sort(Z3_context c, Z3_sort s); + + /** + \brief Check if \c s is a sequence sort. + + def_API('Z3_is_seq_sort', BOOL, (_in(CONTEXT), _in(SORT))) + */ + Z3_bool Z3_API Z3_is_seq_sort(Z3_context c, Z3_sort s); + + /** + \brief Create a regular expression sort out of a sequence sort. + + def_API('Z3_mk_re_sort', SORT, (_in(CONTEXT), _in(SORT))) + */ + Z3_sort Z3_API Z3_mk_re_sort(Z3_context c, Z3_sort seq); + + /** + \brief Check if \c s is a regular expression sort. + + def_API('Z3_is_re_sort', BOOL, (_in(CONTEXT), _in(SORT))) + */ + Z3_bool Z3_API Z3_is_re_sort(Z3_context c, Z3_sort s); + + /** + \brief Create a sort for 8 bit strings. + + This function creates a sort for ASCII strings. + Each character is 8 bits. + + def_API('Z3_mk_string_sort', SORT ,(_in(CONTEXT), )) + */ + Z3_sort Z3_API Z3_mk_string_sort(Z3_context c); + + /** + \brief Check if \c s is a string sort. + + def_API('Z3_is_string_sort', BOOL, (_in(CONTEXT), _in(SORT))) + */ + Z3_bool Z3_API Z3_is_string_sort(Z3_context c, Z3_sort s); + + /** + \brief Create a string constant out of the string that is passed in + def_API('Z3_mk_string' ,AST ,(_in(CONTEXT), _in(STRING))) + */ + Z3_ast Z3_API Z3_mk_string(Z3_context c, Z3_string s); + + /** + \brief Determine if \c s is a string constant. + + def_API('Z3_is_string', BOOL, (_in(CONTEXT), _in(AST))) + */ + Z3_bool Z3_API Z3_is_string(Z3_context c, Z3_ast s); + + /** + \brief Retrieve the string constant stored in \c s. + + \pre Z3_is_string(c, s) + + def_API('Z3_get_string' ,STRING ,(_in(CONTEXT), _in(AST))) + */ + Z3_string Z3_API Z3_get_string(Z3_context c, Z3_ast s); + + /** + \brief Create an empty sequence of the sequence sort \c seq. + + \pre s is a sequence sort. + + def_API('Z3_mk_seq_empty' ,AST ,(_in(CONTEXT), _in(SORT))) + */ + Z3_ast Z3_API Z3_mk_seq_empty(Z3_context c, Z3_sort seq); + + /** + \brief Create a unit sequence of \c a. + + def_API('Z3_mk_seq_unit' ,AST ,(_in(CONTEXT), _in(AST))) + */ + Z3_ast Z3_API Z3_mk_seq_unit(Z3_context c, Z3_ast a); + + /** + \brief Concatenate sequences. + + \pre n > 0 + + def_API('Z3_mk_seq_concat' ,AST ,(_in(CONTEXT), _in(UINT), _in_array(1, AST))) + */ + Z3_ast Z3_API Z3_mk_seq_concat(Z3_context c, unsigned n, Z3_ast const args[]); + + /** + \brief Check if \c prefix is a prefix of \c s. + + \pre prefix and s are the same sequence sorts. + + def_API('Z3_mk_seq_prefix' ,AST ,(_in(CONTEXT), _in(AST), _in(AST))) + */ + Z3_ast Z3_API Z3_mk_seq_prefix(Z3_context c, Z3_ast prefix, Z3_ast s); + + /** + \brief Check if \c suffix is a suffix of \c s. + + \pre \c suffix and \c s are the same sequence sorts. + + def_API('Z3_mk_seq_suffix' ,AST ,(_in(CONTEXT), _in(AST), _in(AST))) + */ + Z3_ast Z3_API Z3_mk_seq_suffix(Z3_context c, Z3_ast suffix, Z3_ast s); + + /** + \brief Check if \c container contains \c containee. + + \pre \c container and \c containee are the same sequence sorts. + + def_API('Z3_mk_seq_contains' ,AST ,(_in(CONTEXT), _in(AST), _in(AST))) + */ + Z3_ast Z3_API Z3_mk_seq_contains(Z3_context c, Z3_ast container, Z3_ast containee); + + /** + \brief Extract subsequence starting at \c offset of \c length. + + def_API('Z3_mk_seq_extract' ,AST ,(_in(CONTEXT), _in(AST), _in(AST), _in(AST))) + */ + Z3_ast Z3_API Z3_mk_seq_extract(Z3_context c, Z3_ast s, Z3_ast offset, Z3_ast length); + + /** + \brief Replace the first occurrence of \c src with \c dst in \c s. + + def_API('Z3_mk_seq_replace' ,AST ,(_in(CONTEXT), _in(AST), _in(AST), _in(AST))) + */ + Z3_ast Z3_API Z3_mk_seq_replace(Z3_context c, Z3_ast src, Z3_ast dst, Z3_ast s); + + /** + \brief Retrieve from \s the unit sequence positioned at position \c index. + + def_API('Z3_mk_seq_at' ,AST ,(_in(CONTEXT), _in(AST), _in(AST))) + */ + Z3_ast Z3_API Z3_mk_seq_at(Z3_context c, Z3_ast s, Z3_ast index); + + /** + \brief Return the length of the sequence \c s. + + def_API('Z3_mk_seq_length' ,AST ,(_in(CONTEXT), _in(AST))) + */ + Z3_ast Z3_API Z3_mk_seq_length(Z3_context c, Z3_ast s); + + + /** + \brief Create a regular expression that accepts the sequence \c seq. + + def_API('Z3_mk_seq_to_re' ,AST ,(_in(CONTEXT), _in(AST))) + */ + Z3_ast Z3_API Z3_mk_seq_to_re(Z3_context c, Z3_ast seq); + + /** + \brief Check if \c seq is in the language generated by the regular expression \c re. + + def_API('Z3_mk_seq_in_re' ,AST ,(_in(CONTEXT), _in(AST), _in(AST))) + */ + Z3_ast Z3_API Z3_mk_seq_in_re(Z3_context c, Z3_ast seq, Z3_ast re); + + /** + \brief Create the regular language \c re+. + + def_API('Z3_mk_re_plus' ,AST ,(_in(CONTEXT), _in(AST))) + */ + Z3_ast Z3_API Z3_mk_re_plus(Z3_context c, Z3_ast re); + + /** + \brief Create the regular language \c re*. + + def_API('Z3_mk_re_star' ,AST ,(_in(CONTEXT), _in(AST))) + */ + Z3_ast Z3_API Z3_mk_re_star(Z3_context c, Z3_ast re); + + /** + \brief Create the regular language \c [re]. + + def_API('Z3_mk_re_option' ,AST ,(_in(CONTEXT), _in(AST))) + */ + Z3_ast Z3_API Z3_mk_re_option(Z3_context c, Z3_ast re); + + /** + \brief Create the union of the regular languages. + + \pre n > 0 + + def_API('Z3_mk_re_union' ,AST ,(_in(CONTEXT), _in(UINT), _in_array(1, AST))) + */ + Z3_ast Z3_API Z3_mk_re_union(Z3_context c, unsigned n, Z3_ast const args[]); + + /** + \brief Create the concatenation of the regular languages. + + \pre n > 0 + + def_API('Z3_mk_re_concat' ,AST ,(_in(CONTEXT), _in(UINT), _in_array(1, AST))) + */ + Z3_ast Z3_API Z3_mk_re_concat(Z3_context c, unsigned n, Z3_ast const args[]); + + /*@}*/ + + /** @name Quantifiers */ /*@{*/ /** diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp index c3f882e8d..44901b506 100644 --- a/src/ast/seq_decl_plugin.cpp +++ b/src/ast/seq_decl_plugin.cpp @@ -80,7 +80,6 @@ zstring zstring::replace(zstring const& src, zstring const& dst) const { return result; } -// TBD: SMT-LIB 2.5 strings don't have escape characters other than " static char* esc_table[32] = { "\\0", "^A", "^B", "^C", "^D", "^E", "^F", "\\a", "\\b", "\\t", "\\n", "\\v", "\\f", "\\r", "^N", "^O", "^P", "^Q", "^R", "^S", "^T", "^U", "^V","^W","^X","^Y","^Z","\\e","^\\","^]","^^","^_"}; @@ -404,14 +403,16 @@ sort * seq_decl_plugin::mk_sort(decl_kind k, unsigned num_parameters, parameter return m_string; } return m.mk_sort(symbol("Seq"), sort_info(m_family_id, SEQ_SORT, num_parameters, parameters)); - case RE_SORT: + case RE_SORT: { if (num_parameters != 1) { m.raise_exception("Invalid regex sort, expecting one parameter"); } if (!parameters[0].is_ast() || !is_sort(parameters[0].get_ast())) { m.raise_exception("invalid regex sort, parameter is not a sort"); } + sort * s = to_sort(parameters[0].get_ast()); return m.mk_sort(symbol("RegEx"), sort_info(m_family_id, RE_SORT, num_parameters, parameters)); + } case _STRING_SORT: return m_string; default: diff --git a/src/ast/seq_decl_plugin.h b/src/ast/seq_decl_plugin.h index d0a475b25..8cd67a406 100644 --- a/src/ast/seq_decl_plugin.h +++ b/src/ast/seq_decl_plugin.h @@ -215,14 +215,13 @@ public: str(seq_util& u): u(u), m(u.m), m_fid(u.m_fid) {} sort* mk_seq(sort* s) { parameter param(s); return m.mk_sort(m_fid, SEQ_SORT, 1, ¶m); } + sort* mk_string_sort() { return m.mk_sort(m_fid, _STRING_SORT, 0, 0); } app* mk_empty(sort* s) { return m.mk_const(m.mk_func_decl(m_fid, OP_SEQ_EMPTY, 0, 0, 0, (expr*const*)0, s)); } app* mk_string(zstring const& s); app* mk_string(symbol const& s) { return u.seq.mk_string(s); } app* mk_char(char ch); app* mk_concat(expr* a, expr* b) { expr* es[2] = { a, b }; return m.mk_app(m_fid, OP_SEQ_CONCAT, 2, es); } - app* mk_concat(expr* a, expr* b, expr* c) { - return mk_concat(a, mk_concat(b, c)); - } + app* mk_concat(expr* a, expr* b, expr* c) { return mk_concat(a, mk_concat(b, c)); } expr* mk_concat(unsigned n, expr* const* es) { if (n == 1) return es[0]; SASSERT(n > 1); return m.mk_app(m_fid, OP_SEQ_CONCAT, n, es); } app* mk_length(expr* a) { return m.mk_app(m_fid, OP_SEQ_LENGTH, 1, &a); } app* mk_substr(expr* a, expr* b, expr* c) { expr* es[3] = { a, b, c }; return m.mk_app(m_fid, OP_SEQ_EXTRACT, 3, es); } @@ -233,8 +232,6 @@ public: app* mk_unit(expr* u) { return m.mk_app(m_fid, OP_SEQ_UNIT, 1, &u); } app* mk_char(zstring const& s, unsigned idx); - - bool is_string(expr const * n) const { return is_app_of(n, m_fid, OP_STRING_CONST); } bool is_string(expr const* n, symbol& s) const { @@ -287,6 +284,8 @@ public: public: re(seq_util& u): m(u.m), m_fid(u.m_fid) {} + sort* mk_re(sort* seq) { parameter param(seq); return m.mk_sort(m_fid, RE_SORT, 1, ¶m); } + app* mk_to_re(expr* s) { return m.mk_app(m_fid, OP_SEQ_TO_RE, 1, &s); } app* mk_in_re(expr* s, expr* r) { return m.mk_app(m_fid, OP_SEQ_IN_RE, s, r); } app* mk_concat(expr* r1, expr* r2) { return m.mk_app(m_fid, OP_RE_CONCAT, r1, r2); } diff --git a/src/math/automata/automaton.h b/src/math/automata/automaton.h index 54cd02832..f64dfd205 100644 --- a/src/math/automata/automaton.h +++ b/src/math/automata/automaton.h @@ -292,6 +292,8 @@ public: // Generalized: // Src - E -> dst - t -> dst1 => Src - t -> dst1 if dst is final => each Src is final // + // src - e -> dst - ET -> dst1 => src - ET - dst1 if in_degree(dst) = 1, src != dst + // void compress() { for (unsigned i = 0; i < m_delta.size(); ++i) { for (unsigned j = 0; j < m_delta[i].size(); ++j) { @@ -326,6 +328,17 @@ public: add(move(m, src, dst1, t)); remove(dst, dst1, t); } + else if (1 == in_degree(dst) && (!is_final_state(dst) || is_final_state(src)) && init() != dst) { + moves const& mvs = m_delta[dst]; + moves mvs1; + for (unsigned k = 0; k < mvs.size(); ++k) { + mvs1.push_back(move(m, src, mvs[k].dst(), mvs[k].t())); + } + for (unsigned k = 0; k < mvs1.size(); ++k) { + remove(dst, mvs1[k].dst(), mvs1[k].t()); + add(mvs1[k]); + } + } else if (false && 1 == out_degree(dst) && all_epsilon_in(dst) && init() != dst && !is_final_state(dst)) { move const& mv = m_delta[dst][0]; T* t = mv.t(); @@ -364,7 +377,7 @@ public: } } } - + bool is_sequence(unsigned& length) const { if (is_final_state(m_init) && (out_degree(m_init) == 0 || (out_degree(m_init) == 1 && is_loop_state(m_init)))) { length = 0; @@ -466,6 +479,14 @@ public: } private: + void remove_dead_states() { + unsigned_vector remap; + for (unsigned i = 0; i < m_delta.size(); ++i) { + + } + } + + void add(move const& mv) { m_delta[mv.src()].push_back(mv); m_delta_inv[mv.dst()].push_back(mv); diff --git a/src/parsers/smt2/smt2scanner.cpp b/src/parsers/smt2/smt2scanner.cpp index ed16003c2..3664ed903 100644 --- a/src/parsers/smt2/smt2scanner.cpp +++ b/src/parsers/smt2/smt2scanner.cpp @@ -169,24 +169,16 @@ namespace smt2 { char c = curr(); if (c == EOF) throw scanner_exception("unexpected end of string", m_line, m_spos); - if (c == '\"') { + if (c == '\n') { + new_line(); + } + else if (c == '\"') { next(); if (curr() != '\"') { m_string.push_back(0); return STRING_TOKEN; } } - else if (c == '\n') { - new_line(); - } - else if (c == '\\') { - next(); - c = curr(); - if (c == EOF) - throw scanner_exception("unexpected end of string", m_line, m_spos); - if (c != '\\' && c != '\"') - throw scanner_exception("invalid escape sequence", m_line, m_spos); - } m_string.push_back(c); next(); } diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index c271e405e..1f3afa672 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -199,7 +199,7 @@ final_check_status theory_seq::final_check_eh() { TRACE("seq", tout << ">>solve_eqs\n";); return FC_CONTINUE; } - if (solve_nqs()) { + if (solve_nqs(0)) { ++m_stats.m_solve_nqs; TRACE("seq", tout << ">>solve_nqs\n";); return FC_CONTINUE; @@ -802,21 +802,20 @@ bool theory_seq::solve_binary_eq(expr* l, expr* r, dependency* dep) { return false; } -bool theory_seq::solve_nqs() { +bool theory_seq::solve_nqs(unsigned i) { bool change = false; context & ctx = get_context(); - for (unsigned i = 0; !ctx.inconsistent() && i < m_nqs.size(); ++i) { + for (; !ctx.inconsistent() && i < m_nqs.size(); ++i) { if (!m_nqs[i].is_solved()) { - change = solve_ne(i) || change; + solve_ne(i); } } - return change || ctx.inconsistent(); + return m_new_propagation || ctx.inconsistent(); } -bool theory_seq::solve_ne(unsigned idx) { +void theory_seq::solve_ne(unsigned idx) { context& ctx = get_context(); seq_rewriter rw(m); - bool change = false; ne const& n = m_nqs[idx]; TRACE("seq", display_disequation(tout, n);); @@ -827,7 +826,7 @@ bool theory_seq::solve_ne(unsigned idx) { case l_false: // mark as solved in mark_solved(idx); - return false; + return; case l_true: break; case l_undef: @@ -844,7 +843,7 @@ bool theory_seq::solve_ne(unsigned idx) { expr_ref rh = canonize(r, deps); if (!rw.reduce_eq(lh, rh, lhs, rhs)) { mark_solved(idx); - return change; + return; } else if (unchanged(l, lhs, r, rhs) ) { // continue @@ -870,11 +869,12 @@ bool theory_seq::solve_ne(unsigned idx) { switch (ctx.get_assignment(lit)) { case l_false: mark_solved(idx); - return false; + return; case l_true: break; case l_undef: ++num_undef_lits; + m_new_propagation = true; break; } } @@ -882,16 +882,14 @@ bool theory_seq::solve_ne(unsigned idx) { m_trail_stack.push(push_dep(*this, idx, deps)); erase_index(idx, i); --i; - change = true; } } if (num_undef_lits == 0 && n.m_lhs.empty()) { literal_vector lits(n.m_lits); lits.push_back(~mk_eq(n.m_l, n.m_r, false)); set_conflict(n.m_dep, lits); - return true; + SASSERT(m_new_propagation); } - return change; } @@ -986,7 +984,6 @@ void theory_seq::display(std::ostream & out) const { display_equations(out); } if (m_nqs.size() > 0) { - out << "Disequations:\n"; display_disequations(out); } if (!m_re2aut.empty()) { @@ -1017,8 +1014,13 @@ void theory_seq::display_equations(std::ostream& out) const { } void theory_seq::display_disequations(std::ostream& out) const { + bool first = true; for (unsigned i = 0; i < m_nqs.size(); ++i) { - display_disequation(out, m_nqs[i]); + if (!m_nqs[i].is_solved()) { + if (first) out << "Disequations:\n"; + first = false; + display_disequation(out, m_nqs[i]); + } } } @@ -1155,7 +1157,7 @@ app* theory_seq::mk_value(app* e) { unsigned sz; if (bv.is_numeral(result, val, sz) && sz == zstring().num_bits()) { unsigned v = val.get_unsigned(); - if ((0 <= v && v < 32) || v == 127) { + if ((0 <= v && v < 7) || (14 <= v && v < 32) || v == 127) { result = m_util.str.mk_unit(result); } else { @@ -1961,6 +1963,7 @@ void theory_seq::new_diseq_eh(theory_var v1, theory_var v2) { m_rewrite(eq); if (!m.is_false(eq)) { m_nqs.push_back(ne(e1, e2)); + solve_nqs(m_nqs.size() - 1); } // add solution for variable that is non-empty? } diff --git a/src/smt/theory_seq.h b/src/smt/theory_seq.h index 78eebe301..db5fa0f8b 100644 --- a/src/smt/theory_seq.h +++ b/src/smt/theory_seq.h @@ -357,8 +357,8 @@ namespace smt { bool is_binary_eq(expr* l, expr* r, expr*& x, ptr_vector& xunits, ptr_vector& yunits, expr*& y); bool solve_binary_eq(expr* l, expr* r, dependency* dep); - bool solve_nqs(); - bool solve_ne(unsigned i); + bool solve_nqs(unsigned i); + void solve_ne(unsigned i); bool unchanged(expr* e, expr_ref_vector& es) const { return es.size() == 1 && es[0] == e; } bool unchanged(expr* e, expr_ref_vector& es, expr* f, expr_ref_vector& fs) const { return