mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 10:25:18 +00:00
Code Activity

seq API

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2016-01-02 22:52:28 -08:00
parent 5e553a4dc1
commit e10ecad5dc
14 changed files with 745 additions and 44 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

32
src/api/api_ast.cpp
View file

@ -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;

2
src/api/api_context.cpp
View file

@ -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<datatype_decl_plugin*>(m().get_plugin(m_dt_fid));
if (!m_user_ref_count) {

5
src/api/api_context.h
View file

@ -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; }

151
src/api/api_seq.cpp Normal file
View file

@ -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<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_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);
};

17
src/api/api_util.h
View file

@ -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; \

252
src/api/python/z3.py
View file

@ -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)

5
src/api/python/z3printer.py
View file

@ -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:

233
src/api/z3_api.h
View file

@ -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 */
/*@{*/
/**

5
src/ast/seq_decl_plugin.cpp
View file

@ -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:

9
src/ast/seq_decl_plugin.h
View file

@ -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, &param); }
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, &param); }
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); }

23
src/math/automata/automaton.h
View file

@ -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);

16
src/parsers/smt2/smt2scanner.cpp
View file

@ -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();
}

35
src/smt/theory_seq.cpp
View file

@ -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?
}

4
src/smt/theory_seq.h
View file

@ -357,8 +357,8 @@ namespace smt {
bool is_binary_eq(expr* l, expr* r, expr*& x, ptr_vector<expr>& xunits, ptr_vector<expr>& 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