mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
seq API, tuning
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner
parent
8e80fb830b
commit
a3c4972c85
|
|
@ -205,6 +205,18 @@ namespace z3 {
|
|||
\brief Return the Bit-vector sort of size \c sz. That is, the sort for bit-vectors of size \c sz.
|
||||
*/
|
||||
sort bv_sort(unsigned sz);
|
||||
/**
|
||||
\brief Return the sort for ASCII strings.
|
||||
*/
|
||||
sort string_sort();
|
||||
/**
|
||||
\brief Return a sequence sort over base sort \c s.
|
||||
*/
|
||||
sort seq_sort(sort& s);
|
||||
/**
|
||||
\brief Return a regular expression sort over sequences \c seq_sort.
|
||||
*/
|
||||
sort re_sort(sort& seq_sort);
|
||||
/**
|
||||
\brief Return an array sort for arrays from \c d to \c r.
|
||||
|
||||
|
|
@ -261,6 +273,9 @@ namespace z3 {
|
|||
expr bv_val(__uint64 n, unsigned sz);
|
||||
expr bv_val(char const * n, unsigned sz);
|
||||
|
||||
expr string_val(char const* s);
|
||||
expr string_val(std::string const& s);
|
||||
|
||||
expr num_val(int n, sort const & s);
|
||||
|
||||
/**
|
||||
|
|
@ -425,6 +440,14 @@ namespace z3 {
|
|||
\brief Return true if this sort is a Relation sort.
|
||||
*/
|
||||
bool is_relation() const { return sort_kind() == Z3_RELATION_SORT; }
|
||||
/**
|
||||
\brief Return true if this sort is a Sequence sort.
|
||||
*/
|
||||
bool is_seq() const { return sort_kind() == Z3_SEQ_SORT; }
|
||||
/**
|
||||
\brief Return true if this sort is a regular expression sort.
|
||||
*/
|
||||
bool is_re() const { return sort_kind() == Z3_RE_SORT; }
|
||||
/**
|
||||
\brief Return true if this sort is a Finite domain sort.
|
||||
*/
|
||||
|
|
@ -532,6 +555,15 @@ namespace z3 {
|
|||
\brief Return true if this is a Relation expression.
|
||||
*/
|
||||
bool is_relation() const { return get_sort().is_relation(); }
|
||||
/**
|
||||
\brief Return true if this is a sequence expression.
|
||||
*/
|
||||
bool is_seq() const { return get_sort().is_seq(); }
|
||||
/**
|
||||
\brief Return true if this is a regular expression.
|
||||
*/
|
||||
bool is_re() const { return get_sort().is_re(); }
|
||||
|
||||
/**
|
||||
\brief Return true if this is a Finite-domain expression.
|
||||
|
||||
|
|
@ -663,6 +695,7 @@ namespace z3 {
|
|||
|
||||
friend expr distinct(expr_vector const& args);
|
||||
friend expr concat(expr const& a, expr const& b);
|
||||
friend expr concat(expr_vector const& args);
|
||||
|
||||
friend expr operator==(expr const & a, expr const & b);
|
||||
friend expr operator==(expr const & a, int b);
|
||||
|
|
@ -728,10 +761,50 @@ namespace z3 {
|
|||
friend expr operator|(int a, expr const & b);
|
||||
|
||||
friend expr operator~(expr const & a);
|
||||
expr extract(unsigned hi, unsigned lo) const { Z3_ast r = Z3_mk_extract(ctx(), hi, lo, *this); return expr(ctx(), r); }
|
||||
expr extract(unsigned hi, unsigned lo) const { Z3_ast r = Z3_mk_extract(ctx(), hi, lo, *this); ctx().check_error(); return expr(ctx(), r); }
|
||||
unsigned lo() const { assert (is_app() && Z3_get_decl_num_parameters(ctx(), decl()) == 2); return static_cast<unsigned>(Z3_get_decl_int_parameter(ctx(), decl(), 1)); }
|
||||
unsigned hi() const { assert (is_app() && Z3_get_decl_num_parameters(ctx(), decl()) == 2); return static_cast<unsigned>(Z3_get_decl_int_parameter(ctx(), decl(), 0)); }
|
||||
|
||||
/**
|
||||
\brief sequence and regular expression operations.
|
||||
+ is overloaeded as sequence concatenation and regular expression union.
|
||||
concat is overloaded to handle sequences and regular expressions
|
||||
*/
|
||||
expr extract(expr const& offset, expr const& length) const {
|
||||
check_context(*this, offset); check_context(offset, length);
|
||||
Z3_ast r = Z3_mk_seq_extract(ctx(), *this, offset, length); check_error(); return expr(ctx(), r);
|
||||
}
|
||||
expr replace(expr const& src, expr const& dst) const {
|
||||
check_context(*this, src); check_context(src, dst);
|
||||
Z3_ast r = Z3_mk_seq_replace(ctx(), *this, src, dst);
|
||||
check_error();
|
||||
return expr(ctx(), r);
|
||||
}
|
||||
expr unit() const {
|
||||
Z3_ast r = Z3_mk_seq_unit(ctx(), *this);
|
||||
check_error();
|
||||
return expr(ctx(), r);
|
||||
}
|
||||
expr contains(expr const& s) {
|
||||
check_context(*this, s);
|
||||
Z3_ast r = Z3_mk_seq_contains(ctx(), *this, s);
|
||||
check_error();
|
||||
return expr(ctx(), r);
|
||||
}
|
||||
expr at(expr const& index) const {
|
||||
check_context(*this, index);
|
||||
Z3_ast r = Z3_mk_seq_at(ctx(), *this, index);
|
||||
check_error();
|
||||
return expr(ctx(), r);
|
||||
}
|
||||
expr length() const {
|
||||
Z3_ast r = Z3_mk_seq_length(ctx(), *this);
|
||||
check_error();
|
||||
return expr(ctx(), r);
|
||||
}
|
||||
|
||||
|
||||
|
||||
/**
|
||||
\brief Return a simplified version of this expression.
|
||||
*/
|
||||
|
|
@ -835,6 +908,13 @@ namespace z3 {
|
|||
else if (a.is_bv() && b.is_bv()) {
|
||||
r = Z3_mk_bvadd(a.ctx(), a, b);
|
||||
}
|
||||
else if (a.is_seq() && b.is_seq()) {
|
||||
return concat(a, b);
|
||||
}
|
||||
else if (a.is_re() && b.is_re()) {
|
||||
Z3_ast _args[2] = { a, b };
|
||||
r = Z3_mk_re_union(a.ctx(), 2, _args);
|
||||
}
|
||||
else {
|
||||
// operator is not supported by given arguments.
|
||||
assert(false);
|
||||
|
|
@ -1219,11 +1299,48 @@ namespace z3 {
|
|||
|
||||
inline expr concat(expr const& a, expr const& b) {
|
||||
check_context(a, b);
|
||||
Z3_ast r = Z3_mk_concat(a.ctx(), a, b);
|
||||
Z3_ast r;
|
||||
if (Z3_is_seq_sort(a.ctx(), a.get_sort())) {
|
||||
Z3_ast _args[2] = { a, b };
|
||||
r = Z3_mk_seq_concat(a.ctx(), 2, _args);
|
||||
}
|
||||
else if (Z3_is_re_sort(a.ctx(), a.get_sort())) {
|
||||
Z3_ast _args[2] = { a, b };
|
||||
r = Z3_mk_re_concat(a.ctx(), 2, _args);
|
||||
}
|
||||
else {
|
||||
r = Z3_mk_concat(a.ctx(), a, b);
|
||||
}
|
||||
a.ctx().check_error();
|
||||
return expr(a.ctx(), r);
|
||||
}
|
||||
|
||||
inline expr concat(expr_vector const& args) {
|
||||
Z3_ast r;
|
||||
assert(args.size() > 0);
|
||||
if (args.size() == 1) {
|
||||
return args[0];
|
||||
}
|
||||
context& ctx = args[0].ctx();
|
||||
array<Z3_ast> _args(args);
|
||||
if (Z3_is_seq_sort(ctx, args[0].get_sort())) {
|
||||
r = Z3_mk_seq_concat(ctx, _args.size(), _args.ptr());
|
||||
}
|
||||
else if (Z3_is_re_sort(ctx, args[0].get_sort())) {
|
||||
r = Z3_mk_re_concat(ctx, _args.size(), _args.ptr());
|
||||
}
|
||||
else {
|
||||
r = _args[args.size()-1];
|
||||
for (unsigned i = args.size()-1; i > 0; ) {
|
||||
--i;
|
||||
r = Z3_mk_concat(ctx, _args[i], r);
|
||||
ctx.check_error();
|
||||
}
|
||||
}
|
||||
ctx.check_error();
|
||||
return expr(ctx, r);
|
||||
}
|
||||
|
||||
class func_entry : public object {
|
||||
Z3_func_entry m_entry;
|
||||
void init(Z3_func_entry e) {
|
||||
|
|
@ -1762,6 +1879,10 @@ namespace z3 {
|
|||
inline sort context::int_sort() { Z3_sort s = Z3_mk_int_sort(m_ctx); check_error(); return sort(*this, s); }
|
||||
inline sort context::real_sort() { Z3_sort s = Z3_mk_real_sort(m_ctx); check_error(); return sort(*this, s); }
|
||||
inline sort context::bv_sort(unsigned sz) { Z3_sort s = Z3_mk_bv_sort(m_ctx, sz); check_error(); return sort(*this, s); }
|
||||
inline sort context::string_sort() { Z3_sort s = Z3_mk_string_sort(m_ctx); check_error(); return sort(*this, s); }
|
||||
inline sort context::seq_sort(sort& s) { Z3_sort r = Z3_mk_seq_sort(m_ctx, s); check_error(); return sort(*this, r); }
|
||||
inline sort context::re_sort(sort& s) { Z3_sort r = Z3_mk_re_sort(m_ctx, s); check_error(); return sort(*this, r); }
|
||||
|
||||
inline sort context::array_sort(sort d, sort r) { Z3_sort s = Z3_mk_array_sort(m_ctx, d, r); check_error(); return sort(*this, s); }
|
||||
inline sort context::enumeration_sort(char const * name, unsigned n, char const * const * enum_names, func_decl_vector & cs, func_decl_vector & ts) {
|
||||
array<Z3_symbol> _enum_names(n);
|
||||
|
|
@ -1885,6 +2006,9 @@ namespace z3 {
|
|||
inline expr context::bv_val(__uint64 n, unsigned sz) { Z3_ast r = Z3_mk_unsigned_int64(m_ctx, n, bv_sort(sz)); check_error(); return expr(*this, r); }
|
||||
inline expr context::bv_val(char const * n, unsigned sz) { Z3_ast r = Z3_mk_numeral(m_ctx, n, bv_sort(sz)); check_error(); return expr(*this, r); }
|
||||
|
||||
inline expr context::string_val(char const* s) { Z3_ast r = Z3_mk_string(m_ctx, s); check_error(); return expr(*this, r); }
|
||||
inline expr context::string_val(std::string const& s) { Z3_ast r = Z3_mk_string(m_ctx, s.c_str()); check_error(); return expr(*this, r); }
|
||||
|
||||
inline expr context::num_val(int n, sort const & s) { Z3_ast r = Z3_mk_int(m_ctx, n, s); check_error(); return expr(*this, r); }
|
||||
|
||||
inline expr func_decl::operator()(unsigned n, expr const * args) const {
|
||||
|
|
@ -2017,6 +2141,62 @@ namespace z3 {
|
|||
d.check_error();
|
||||
return expr(d.ctx(), r);
|
||||
}
|
||||
|
||||
// sequence and regular expression operations.
|
||||
// union is +
|
||||
// concat is overloaded to handle sequences and regular expressions
|
||||
|
||||
inline expr empty(sort const& s) {
|
||||
Z3_ast r = Z3_mk_seq_empty(s.ctx(), s);
|
||||
s.check_error();
|
||||
return expr(s.ctx(), r);
|
||||
}
|
||||
inline expr suffixof(expr const& a, expr const& b) {
|
||||
check_context(a, b);
|
||||
Z3_ast r = Z3_mk_seq_suffix(a.ctx(), a, b);
|
||||
a.check_error();
|
||||
return expr(a.ctx(), r);
|
||||
}
|
||||
inline expr prefixof(expr const& a, expr const& b) {
|
||||
check_context(a, b);
|
||||
Z3_ast r = Z3_mk_seq_prefix(a.ctx(), a, b);
|
||||
a.check_error();
|
||||
return expr(a.ctx(), r);
|
||||
}
|
||||
inline expr indexof(expr const& s, expr const& substr, expr const& offset) {
|
||||
check_context(s, substr); check_context(s, offset);
|
||||
Z3_ast r = Z3_mk_seq_index(s.ctx(), s, substr, offset);
|
||||
s.check_error();
|
||||
return expr(s.ctx(), r);
|
||||
}
|
||||
inline expr to_re(expr const& s) {
|
||||
Z3_ast r = Z3_mk_seq_to_re(s.ctx(), s);
|
||||
s.check_error();
|
||||
return expr(s.ctx(), r);
|
||||
}
|
||||
inline expr in_re(expr const& s, expr const& re) {
|
||||
check_context(s, re);
|
||||
Z3_ast r = Z3_mk_seq_in_re(s.ctx(), s, re);
|
||||
s.check_error();
|
||||
return expr(s.ctx(), r);
|
||||
}
|
||||
inline expr plus(expr const& re) {
|
||||
Z3_ast r = Z3_mk_re_plus(re.ctx(), re);
|
||||
re.check_error();
|
||||
return expr(re.ctx(), r);
|
||||
}
|
||||
inline expr option(expr const& re) {
|
||||
Z3_ast r = Z3_mk_re_option(re.ctx(), re);
|
||||
re.check_error();
|
||||
return expr(re.ctx(), r);
|
||||
}
|
||||
inline expr star(expr const& re) {
|
||||
Z3_ast r = Z3_mk_re_star(re.ctx(), re);
|
||||
re.check_error();
|
||||
return expr(re.ctx(), r);
|
||||
}
|
||||
|
||||
|
||||
inline expr interpolant(expr const& a) {
|
||||
return expr(a.ctx(), Z3_mk_interpolant(a.ctx(), a));
|
||||
}
|
||||
|
|
|
|||
|
|
@ -292,7 +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
|
||||
// src - e -> dst - ET -> Dst1 => src - ET -> Dst1 if in_degree(dst) = 1, src != dst
|
||||
// Src - E -> dst - et -> dst1 => Src - et -> dst1 if out_degree(dst) = 1, src != dst
|
||||
//
|
||||
void compress() {
|
||||
for (unsigned i = 0; i < m_delta.size(); ++i) {
|
||||
|
|
@ -339,24 +340,42 @@ public:
|
|||
add(mvs1[k]);
|
||||
}
|
||||
}
|
||||
else if (false && 1 == out_degree(dst) && all_epsilon_in(dst) && init() != dst && !is_final_state(dst)) {
|
||||
//
|
||||
// Src - E -> dst - et -> dst1 => Src - et -> dst1 if out_degree(dst) = 1, src != dst
|
||||
//
|
||||
else if (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();
|
||||
unsigned dst1 = mv.dst();
|
||||
T* t = mv.t();
|
||||
unsigned_vector src0s;
|
||||
moves const& mvs = m_delta_inv[dst];
|
||||
moves mvs1;
|
||||
for (unsigned k = 0; k < mvs.size(); ++k) {
|
||||
SASSERT(mvs[k].is_epsilon());
|
||||
src0s.push_back(mvs[k].src());
|
||||
mvs1.push_back(move(m, mvs[k].src(), dst1, t));
|
||||
}
|
||||
for (unsigned k = 0; k < src0s.size(); ++k) {
|
||||
remove(src0s[k], dst, 0);
|
||||
add(move(m, src0s[i], dst1, t));
|
||||
for (unsigned k = 0; k < mvs1.size(); ++k) {
|
||||
remove(mvs1[k].src(), dst, 0);
|
||||
add(mvs1[k]);
|
||||
}
|
||||
remove(dst, dst1, t);
|
||||
--j;
|
||||
continue;
|
||||
}
|
||||
//
|
||||
// Src1 - ET -> src - e -> dst => Src1 - ET -> dst if out_degree(src) = 1, src != init()
|
||||
//
|
||||
else if (1 == out_degree(src) && init() != src && (!is_final_state(src) || is_final_state(dst))) {
|
||||
moves const& mvs = m_delta_inv[src];
|
||||
moves mvs1;
|
||||
for (unsigned k = 0; k < mvs.size(); ++k) {
|
||||
mvs1.push_back(move(m, mvs[k].src(), dst, mvs[k].t()));
|
||||
}
|
||||
for (unsigned k = 0; k < mvs1.size(); ++k) {
|
||||
remove(mvs1[k].src(), src, mvs1[k].t());
|
||||
add(mvs1[k]);
|
||||
}
|
||||
}
|
||||
else {
|
||||
continue;
|
||||
}
|
||||
|
|
@ -482,7 +501,7 @@ private:
|
|||
void remove_dead_states() {
|
||||
unsigned_vector remap;
|
||||
for (unsigned i = 0; i < m_delta.size(); ++i) {
|
||||
|
||||
|
||||
}
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -373,14 +373,12 @@ bool theory_seq::propagate_length_coherence(expr* e) {
|
|||
expr_ref high1(m_autil.mk_le(m_util.str.mk_length(e), m_autil.mk_numeral(hi, true)), m);
|
||||
expr_ref high2(m_autil.mk_le(m_util.str.mk_length(seq), m_autil.mk_numeral(hi-lo, true)), m);
|
||||
add_axiom(~mk_literal(high1), mk_literal(high2));
|
||||
m_trail_stack.push(push_replay(alloc(replay_length_coherence, m, e)));
|
||||
}
|
||||
|
||||
m_trail_stack.push(push_replay(alloc(replay_length_coherence, m, e)));
|
||||
return true;
|
||||
}
|
||||
|
||||
bool theory_seq::check_length_coherence() {
|
||||
bool coherent = true;
|
||||
obj_hashtable<expr>::iterator it = m_length.begin(), end = m_length.end();
|
||||
for (; it != end; ++it) {
|
||||
expr* e = *it;
|
||||
|
|
@ -398,7 +396,7 @@ bool theory_seq::check_length_coherence() {
|
|||
return false;
|
||||
}
|
||||
}
|
||||
return coherent;
|
||||
return true;
|
||||
}
|
||||
|
||||
/*
|
||||
|
|
@ -890,6 +888,23 @@ void theory_seq::solve_ne(unsigned idx) {
|
|||
set_conflict(n.m_dep, lits);
|
||||
SASSERT(m_new_propagation);
|
||||
}
|
||||
if (num_undef_lits == 0 && n.m_lhs.size() == 1) {
|
||||
expr* l = n.m_lhs[0];
|
||||
expr* r = n.m_rhs[0];
|
||||
if (m_util.str.is_empty(r)) {
|
||||
std::swap(l, r);
|
||||
}
|
||||
if (m_util.str.is_empty(l) && is_var(r)) {
|
||||
literal lit = ~mk_eq_empty(r);
|
||||
if (ctx.get_assignment(lit) == l_true) {
|
||||
expr_ref head(m), tail(m);
|
||||
mk_decompose(r, head, tail);
|
||||
expr_ref conc(m_util.str.mk_concat(head, tail), m);
|
||||
propagate_is_conc(r, conc);
|
||||
}
|
||||
m_new_propagation = true;
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
|
|
@ -2171,6 +2186,15 @@ bool theory_seq::add_accept2step(expr* acc) {
|
|||
break;
|
||||
}
|
||||
}
|
||||
if (has_undef && mvs.size() == 1) {
|
||||
literal lit = lits.back();
|
||||
lits.pop_back();
|
||||
for (unsigned i = 0; i < lits.size(); ++i) {
|
||||
lits[i].neg();
|
||||
}
|
||||
propagate_lit(0, lits.size(), lits.c_ptr(), lit);
|
||||
return false;
|
||||
}
|
||||
if (has_undef) {
|
||||
return true;
|
||||
}
|
||||
|
|
|
|||
Loading…
Reference in a new issue