mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-05 17:14:07 +00:00
Code Activity

Merge branch 'master' of https://github.com/z3prover/z3

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-12-20 09:21:53 -08:00
parent 83b47f1859 be38b256c8
commit ad91748b5f
35 changed files with 401 additions and 623 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

26
src/api/api_solver.cpp
View file

@ -944,7 +944,7 @@ extern "C" {
Z3_TRY;
LOG_Z3_solver_propagate_register(c, s, e);
RESET_ERROR_CODE();
return to_solver_ref(s)->user_propagate_register(to_expr(e));
return to_solver_ref(s)->user_propagate_register_expr(to_expr(e));
Z3_CATCH_RETURN(0);
}
@ -964,4 +964,28 @@ extern "C" {
Z3_CATCH;
}
void Z3_API Z3_solver_propagate_created(Z3_context c, Z3_solver s, Z3_created_eh created_eh) {
Z3_TRY;
RESET_ERROR_CODE();
user_propagator::created_eh_t c = (void(*)(void*, user_propagator::callback*, expr*, unsigned))created_eh;
to_solver_ref(s)->user_propagate_register_created(c);
Z3_CATCH;
}
Z3_func_decl Z3_API Z3_solver_propagate_declare(Z3_context c, Z3_symbol name, unsigned n, Z3_sort* domain, Z3_sort range) {
Z3_TRY;
LOG_Z3_solver_propagate_declare(c, name, n, domain, range);
RESET_ERROR_CODE();
ast_manager& m = mk_c(c)->m();
family_id fid = m.mk_family_id(user_propagator::plugin::name());
if (!m.has_plugin(fid))
m.register_plugin(fid, alloc(user_propagator::plugin));
func_decl_info info(fid, user_propagator::plugin::kind_t::OP_USER_PROPAGATE);
func_decl* f = m.mk_func_decl(to_symbol(name), n, to_sorts(domain), to_sort(range), info);
mk_c(c)->save_ast_trail(f);
RETURN_Z3(of_func_decl(f));
Z3_CATCH_RETURN(nullptr);
}
};

33
src/api/c++/z3++.h
View file

@ -334,6 +334,7 @@ namespace z3 {
func_decl recfun(char const * name, sort const & d1, sort const & d2, sort const & range);
void recdef(func_decl, expr_vector const& args, expr const& body);
func_decl user_propagate_function(symbol const& name, sort_vector const& domain, sort const& range);
expr constant(symbol const & name, sort const & s);
expr constant(char const * name, sort const & s);
@ -3424,6 +3425,14 @@ namespace z3 {
Z3_add_rec_def(f.ctx(), f, vars.size(), vars.ptr(), body);
}
inline func_decl context::user_propagate_function(symbol const& name, sort_vector const& domain, sort const& range) {
check_context(domain, range);
array<Z3_sort> domain1(domain);
Z3_func_decl f = Z3_solver_propagate_declare(range.ctx(), name, domain1.size(), domain1.ptr(), range);
check_error();
return func_decl(*this, f);
}
inline expr context::constant(symbol const & name, sort const & s) {
Z3_ast r = Z3_mk_const(m_ctx, name, s);
check_error();
@ -3877,10 +3886,12 @@ namespace z3 {
typedef std::function<void(unsigned, expr const&)> fixed_eh_t;
typedef std::function<void(void)> final_eh_t;
typedef std::function<void(unsigned, unsigned)> eq_eh_t;
typedef std::function<void(unsigned, expr const&)> created_eh_t;
final_eh_t m_final_eh;
eq_eh_t m_eq_eh;
fixed_eh_t m_fixed_eh;
created_eh_t m_created_eh;
solver* s;
Z3_context c;
Z3_solver_callback cb { nullptr };
@ -3929,6 +3940,14 @@ namespace z3 {
static_cast<user_propagator_base*>(p)->m_final_eh();
}
static void created_eh(void* _p, Z3_solver_callback cb, Z3_ast _e, unsigned id) {
user_propagator_base* p = static_cast<user_propagator_base*>(_p);
scoped_cb _cb(p, cb);
scoped_context ctx(p->ctx());
expr e(ctx(), _e);
static_cast<user_propagator_base*>(p)->m_created_eh(id, e);
}
public:
user_propagator_base(Z3_context c) : s(nullptr), c(c) {}
@ -4008,6 +4027,18 @@ namespace z3 {
Z3_solver_propagate_final(ctx(), *s, final_eh);
}
void register_created(created_eh_t& c) {
assert(s);
m_created_eh = c;
Z3_solver_propagate_created(ctx(), *s, created_eh);
}
void register_created() {
m_created_eh = [this](unsigned id, expr const& e) {
created(id, e);
};
Z3_solver_propagate_created(ctx(), *s, created_eh);
}
virtual void fixed(unsigned /*id*/, expr const& /*e*/) { }
@ -4015,6 +4046,8 @@ namespace z3 {
virtual void final() { }
virtual void created(unsigned /*id*/, expr const& /*e*/) {}
/**
\brief tracks \c e by a unique identifier that is returned by the call.

19
src/api/z3_api.h
View file

@ -1430,6 +1430,7 @@ typedef void* Z3_fresh_eh(void* ctx, Z3_context new_context);
typedef void Z3_fixed_eh(void* ctx, Z3_solver_callback cb, unsigned id, Z3_ast value);
typedef void Z3_eq_eh(void* ctx, Z3_solver_callback cb, unsigned x, unsigned y);
typedef void Z3_final_eh(void* ctx, Z3_solver_callback cb);
typedef void Z3_created_eh(void* ctx, Z3_solver_callback cb, Z3_ast e, unsigned id);
/**
@ -6676,6 +6677,24 @@ extern "C" {
*/
void Z3_API Z3_solver_propagate_diseq(Z3_context c, Z3_solver s, Z3_eq_eh eq_eh);
/**
* \brief register a callback when a new expression with a registered function is used by the solver
* The registered function appears at the top level and is created using \ref Z3_propagate_solver_declare.
*/
void Z3_API Z3_solver_propagate_created(Z3_context c, Z3_solver s, Z3_created_eh created_eh);
/**
Create uninterpreted function declaration for the user propagator.
When expressions using the function are created by the solver invoke a callback
to \ref \Z3_solver_progate_created with arguments
1. context and callback solve
2. declared_expr: expression using function that was used as the top-level symbol
3. declared_id: a unique identifier (unique within the current scope) to track the expression.
def_API('Z3_solver_propagate_declare', FUNC_DECL, (_in(CONTEXT), _in(SYMBOL), _in(UINT), _in_array(2, SORT), _in(SORT)))
*/
Z3_func_decl Z3_API Z3_solver_propagate_declare(Z3_context c, Z3_symbol name, unsigned n, Z3_sort* domain, Z3_sort range);
/**
\brief register an expression to propagate on with the solver.
Only expressions of type Bool and type Bit-Vector can be registered for propagation.

2
src/ast/ast.h
View file

@ -845,7 +845,7 @@ class quantifier : public expr {
char m_patterns_decls[0];
static unsigned get_obj_size(unsigned num_decls, unsigned num_patterns, unsigned num_no_patterns) {
return sizeof(quantifier) + num_decls * (sizeof(sort *) + sizeof(symbol)) + (num_patterns + num_no_patterns) * sizeof(expr*);
return (unsigned)(sizeof(quantifier) + num_decls * (sizeof(sort *) + sizeof(symbol)) + (num_patterns + num_no_patterns) * sizeof(expr*));
}
quantifier(quantifier_kind k, unsigned num_decls, sort * const * decl_sorts, symbol const * decl_names, expr * body, sort* s,

2
src/ast/recfun_decl_plugin.h
View file

@ -305,7 +305,7 @@ namespace recfun {
m_pred(pred), m_cdef(&d), m_args(args) {}
body_expansion(body_expansion const & from):
m_pred(from.m_pred), m_cdef(from.m_cdef), m_args(from.m_args) {}
body_expansion(body_expansion && from) :
body_expansion(body_expansion && from) noexcept :
m_pred(from.m_pred), m_cdef(from.m_cdef), m_args(std::move(from.m_args)) {}
std::ostream& display(std::ostream& out) const;

2
src/ast/rewriter/maximize_ac_sharing.h
View file

@ -46,7 +46,7 @@ class maximize_ac_sharing : public default_rewriter_cfg {
entry(func_decl * d = nullptr, expr * arg1 = nullptr, expr * arg2 = nullptr):m_decl(d), m_arg1(arg1), m_arg2(arg2) {
SASSERT((d == 0 && arg1 == 0 && arg2 == 0) || (d != 0 && arg1 != 0 && arg2 != 0));
if (arg1->get_id() > arg2->get_id())
if (arg1 && arg2 && arg1->get_id() > arg2->get_id())
std::swap(m_arg1, m_arg2);
}

313
src/ast/rewriter/seq_rewriter.cpp
View file

@ -2857,7 +2857,7 @@ br_status seq_rewriter::mk_re_reverse(expr* r, expr_ref& result) {
return BR_REWRITE2;
}
else if (re().is_loop(r, r1, lo, hi)) {
result = re().mk_loop(re().mk_reverse(r1), lo, hi);
result = re().mk_loop_proper(re().mk_reverse(r1), lo, hi);
return BR_REWRITE2;
}
else if (re().is_reverse(r, r1)) {
@ -3184,7 +3184,7 @@ void seq_rewriter::mk_antimirov_deriv_rec(expr* e, expr* r, expr* path, expr_ref
if ((lo == 0 && hi == 0) || hi < lo)
result = nothing();
else
result = mk_antimirov_deriv_concat(mk_antimirov_deriv(e, r1, path), re().mk_loop(r1, (lo == 0 ? 0 : lo - 1), hi - 1));
result = mk_antimirov_deriv_concat(mk_antimirov_deriv(e, r1, path), re().mk_loop_proper(r1, (lo == 0 ? 0 : lo - 1), hi - 1));
}
else if (re().is_opt(r, r1))
result = mk_antimirov_deriv(e, r1, path);
@ -3350,6 +3350,8 @@ expr_ref seq_rewriter::mk_regex_inter_normalize(expr* r1, expr* r2) {
SASSERT(m_util.is_re(r1));
SASSERT(m_util.is_re(r2));
expr_ref result(m());
if (re().is_epsilon(r2))
std::swap(r1, r2);
std::function<bool(expr*, expr*&, expr*&)> test = [&](expr* t, expr*& a, expr*& b) { return re().is_intersection(t, a, b); };
std::function<expr* (expr*, expr*)> compose = [&](expr* r1, expr* r2) { return re().mk_inter(r1, r2); };
if (r1 == r2 || re().is_empty(r1) || re().is_full_seq(r2))
@ -3368,9 +3370,8 @@ expr_ref seq_rewriter::mk_regex_inter_normalize(expr* r1, expr* r2) {
result = r2;
else if (re().is_dot_plus(r2) && re().get_info(r1).min_length > 0)
result = r1;
else {
result = merge_regex_sets(r1, r2, re().mk_empty(r1->get_sort()), test, compose);
}
else
result = merge_regex_sets(r1, r2, re().mk_empty(r1->get_sort()), test, compose);
return result;
}
@ -3380,7 +3381,6 @@ expr_ref seq_rewriter::merge_regex_sets(expr* r1, expr* r2, expr* unit,
sort* seq_sort;
expr_ref result(unit, m());
expr_ref_vector prefix(m());
expr* a, * ar1, * b, * br1;
VERIFY(m_util.is_re(r1, seq_sort));
SASSERT(m_util.is_re(r2));
SASSERT(r2->get_sort() == r1->get_sort());
@ -3414,6 +3414,7 @@ expr_ref seq_rewriter::merge_regex_sets(expr* r1, expr* r2, expr* unit,
if (are_complements(ar, br))
return expr_ref(unit, m());
expr* a, * ar1, * b, * br1;
if (test(br, b, br1) && !test(ar, a, ar1))
std::swap(ar, br);
@ -3505,7 +3506,7 @@ expr_ref seq_rewriter::mk_regex_reverse(expr* r) {
else if (re().is_loop(r, r1, lo))
result = re().mk_loop(mk_regex_reverse(r1), lo);
else if (re().is_loop(r, r1, lo, hi))
result = re().mk_loop(mk_regex_reverse(r1), lo, hi);
result = re().mk_loop_proper(mk_regex_reverse(r1), lo, hi);
else if (re().is_opt(r, r1))
result = re().mk_opt(mk_regex_reverse(r1));
else if (re().is_complement(r, r1))
@ -3518,8 +3519,9 @@ expr_ref seq_rewriter::mk_regex_reverse(expr* r) {
}
expr_ref seq_rewriter::mk_regex_concat(expr* r, expr* s) {
sort* seq_sort = nullptr;
sort* seq_sort = nullptr, * ele_sort = nullptr;
VERIFY(m_util.is_re(r, seq_sort));
VERIFY(u().is_seq(seq_sort, ele_sort));
SASSERT(r->get_sort() == s->get_sort());
expr_ref result(m());
expr* r1, * r2;
@ -3529,11 +3531,30 @@ expr_ref seq_rewriter::mk_regex_concat(expr* r, expr* s) {
result = r;
else if (re().is_full_seq(r) && re().is_full_seq(s))
result = r;
else if (re().is_full_char(r) && re().is_full_seq(s))
// ..* = .+
result = re().mk_plus(re().mk_full_char(ele_sort));
else if (re().is_full_seq(r) && re().is_full_char(s))
// .*. = .+
result = re().mk_plus(re().mk_full_char(ele_sort));
else if (re().is_concat(r, r1, r2))
//create the resulting concatenation in right-associative form
// create the resulting concatenation in right-associative form except for the following case
// TODO: maintain the followig invariant for A ++ B{m,n} + C
// concat(concat(A, B{m,n}), C) (if A != () and C != ())
// concat(B{m,n}, C) (if A == () and C != ())
// where A, B, C are regexes
// Using & below for Intersection and | for Union
// In other words, do not make A ++ B{m,n} into right-assoc form, but keep B{m,n} at the top
// This will help to identify this situation in the merge routine:
// concat(concat(A, B{0,m}), C) | concat(concat(A, B{0,n}), C)
// simplies to
// concat(concat(A, B{0,max(m,n)}), C)
// analogously:
// concat(concat(A, B{0,m}), C) & concat(concat(A, B{0,n}), C)
// simplies to
// concat(concat(A, B{0,min(m,n)}), C)
result = mk_regex_concat(r1, mk_regex_concat(r2, s));
else {
//TODO: perhaps simplifiy some further cases such as .*. = ..* = .*.+ = .+.* = .+
result = re().mk_concat(r, s);
}
return result;
@ -3567,15 +3588,7 @@ expr_ref seq_rewriter::mk_in_antimirov_rec(expr* s, expr* d) {
*/
expr_ref seq_rewriter::simplify_path(expr* elem, expr* path) {
expr_ref result(path, m());
expr* h = nullptr, * t = nullptr;
if (m().is_and(path, h, t)) {
if (m().is_true(h))
result = simplify_path(elem, t);
else if (m().is_true(t))
result = simplify_path(elem, h);
else
elim_condition(elem, result);
}
elim_condition(elem, result);
return result;
}
@ -4028,7 +4041,7 @@ expr_ref seq_rewriter::mk_derivative_rec(expr* ele, expr* r) {
return result;
}
else {
return mk_der_concat(result, re().mk_loop(r1, lo, hi));
return mk_der_concat(result, re().mk_loop_proper(r1, lo, hi));
}
}
else if (re().is_full_seq(r) ||
@ -4524,7 +4537,7 @@ br_status seq_rewriter::mk_re_concat(expr* a, expr* b, expr_ref& result) {
unsigned lo1, hi1, lo2, hi2;
if (re().is_loop(a, a1, lo1, hi1) && lo1 <= hi1 && re().is_loop(b, b1, lo2, hi2) && lo2 <= hi2 && a1 == b1) {
result = re().mk_loop(a1, lo1 + lo2, hi1 + hi2);
result = re().mk_loop_proper(a1, lo1 + lo2, hi1 + hi2);
return BR_DONE;
}
if (re().is_loop(a, a1, lo1) && re().is_loop(b, b1, lo2) && a1 == b1) {
@ -4632,79 +4645,13 @@ br_status seq_rewriter::mk_re_union0(expr* a, expr* b, expr_ref& result) {
return BR_FAILED;
}
/*
(a + a) = a
(a + eps) = a
(eps + a) = a
*/
/* Creates a normalized union. */
br_status seq_rewriter::mk_re_union(expr* a, expr* b, expr_ref& result) {
br_status st = mk_re_union0(a, b, result);
if (st != BR_FAILED)
return st;
auto mk_full = [&]() { return re().mk_full_seq(a->get_sort()); };
if (are_complements(a, b)) {
result = mk_full();
return BR_DONE;
}
//just keep the union normalized
result = mk_regex_union_normalize(a, b);
return BR_DONE;
expr* a1 = nullptr, *a2 = nullptr;
expr* b1 = nullptr, *b2 = nullptr;
// ensure union is right-associative
// and swap-sort entries
if (re().is_union(a, a1, a2)) {
result = re().mk_union(a1, re().mk_union(a2, b));
return BR_REWRITE2;
}
auto get_id = [&](expr* e) { re().is_complement(e, e); return e->get_id(); };
if (re().is_union(b, b1, b2)) {
if (is_subset(a, b1)) {
result = b;
return BR_DONE;
}
if (is_subset(b1, a)) {
result = re().mk_union(a, b2);
return BR_REWRITE1;
}
if (are_complements(a, b1)) {
result = mk_full();
return BR_DONE;
}
if (get_id(a) > get_id(b1)) {
result = re().mk_union(b1, re().mk_union(a, b2));
return BR_REWRITE2;
}
}
else {
if (is_subset(a, b)) {
result = b;
return BR_DONE;
}
if (is_subset(b, a)) {
result = a;
return BR_DONE;
}
if (get_id(a) > get_id(b)) {
result = re().mk_union(b, a);
return BR_DONE;
}
}
return BR_FAILED;
}
/*
comp(intersect e1 e2) -> union comp(e1) comp(e2)
comp(union e1 e2) -> intersect comp(e1) comp(e2)
comp(none) -> all
comp(all) -> none
comp(comp(e1)) -> e1
comp(epsilon) -> .+
*/
/* Creates a normalized complement */
br_status seq_rewriter::mk_re_complement(expr* a, expr_ref& result) {
expr *e1 = nullptr, *e2 = nullptr;
if (re().is_intersection(a, e1, e2)) {
@ -4759,84 +4706,10 @@ br_status seq_rewriter::mk_re_inter0(expr* a, expr* b, expr_ref& result) {
return BR_FAILED;
}
/**
(r n r) = r
(emp n r) = emp
(r n emp) = emp
(all n r) = r
(r n all) = r
(r n comp(r)) = emp
(comp(r) n r) = emp
(r n to_re(s)) = ite (s in r) to_re(s) emp
(to_re(s) n r) = "
*/
/* Creates a normalized intersection. */
br_status seq_rewriter::mk_re_inter(expr* a, expr* b, expr_ref& result) {
br_status st = mk_re_inter0(a, b, result);
if (st != BR_FAILED)
return st;
auto mk_empty = [&]() { return re().mk_empty(a->get_sort()); };
if (are_complements(a, b)) {
result = mk_empty();
return BR_DONE;
}
// intersect and normalize
result = mk_regex_inter_normalize(a, b);
return BR_DONE;
expr* a1 = nullptr, *a2 = nullptr;
expr* b1 = nullptr, *b2 = nullptr;
// the following rewrite rules do not seem to
// do the right thing when it comes to normalizing
// ensure intersection is right-associative
// and swap-sort entries
if (re().is_intersection(a, a1, a2)) {
result = re().mk_inter(a1, re().mk_inter(a2, b));
return BR_REWRITE2;
}
auto get_id = [&](expr* e) { re().is_complement(e, e); return e->get_id(); };
if (re().is_intersection(b, b1, b2)) {
if (is_subset(b1, a)) {
result = b;
return BR_DONE;
}
if (is_subset(a, b1)) {
result = re().mk_inter(a, b2);
return BR_REWRITE1;
}
if (are_complements(a, b1)) {
result = mk_empty();
return BR_DONE;
}
if (get_id(a) > get_id(b1)) {
result = re().mk_inter(b1, re().mk_inter(a, b2));
return BR_REWRITE2;
}
}
else {
if (get_id(a) > get_id(b)) {
result = re().mk_inter(b, a);
return BR_DONE;
}
if (is_subset(a, b)) {
result = a;
return BR_DONE;
}
if (is_subset(b, a)) {
result = b;
return BR_DONE;
}
}
if (re().is_to_re(b))
std::swap(a, b);
expr* s = nullptr;
if (re().is_to_re(a, s)) {
result = m().mk_ite(re().mk_in_re(s, b), a, re().mk_empty(a->get_sort()));
return BR_REWRITE2;
}
return BR_FAILED;
}
br_status seq_rewriter::mk_re_diff(expr* a, expr* b, expr_ref& result) {
@ -4874,7 +4747,7 @@ br_status seq_rewriter::mk_re_loop(func_decl* f, unsigned num_args, expr* const*
}
// (loop (loop a l l) h h) = (loop a l*h l*h)
if (re().is_loop(args[0], a, lo, hi) && np == 2 && lo == hi && lo2 == hi2) {
result = re().mk_loop(a, lo2 * lo, hi2 * hi);
result = re().mk_loop_proper(a, lo2 * lo, hi2 * hi);
return BR_REWRITE1;
}
// (loop a 1 1) = a
@ -4901,7 +4774,7 @@ br_status seq_rewriter::mk_re_loop(func_decl* f, unsigned num_args, expr* const*
case 3:
if (m_autil.is_numeral(args[1], n1) && n1.is_unsigned() &&
m_autil.is_numeral(args[2], n2) && n2.is_unsigned()) {
result = re().mk_loop(args[0], n1.get_unsigned(), n2.get_unsigned());
result = re().mk_loop_proper(args[0], n1.get_unsigned(), n2.get_unsigned());
return BR_REWRITE1;
}
break;
@ -4913,7 +4786,7 @@ br_status seq_rewriter::mk_re_loop(func_decl* f, unsigned num_args, expr* const*
br_status seq_rewriter::mk_re_power(func_decl* f, expr* a, expr_ref& result) {
unsigned p = f->get_parameter(0).get_int();
result = re().mk_loop(a, p, p);
result = re().mk_loop_proper(a, p, p);
return BR_REWRITE1;
}
@ -5080,74 +4953,68 @@ void seq_rewriter::intersect(unsigned lo, unsigned hi, svector<std::pair<unsigne
*/
void seq_rewriter::elim_condition(expr* elem, expr_ref& cond) {
expr_ref_vector conds(m());
expr_ref_vector conds_range(m());
flatten_and(cond, conds);
expr* lhs = nullptr, *rhs = nullptr, *e1 = nullptr;
bool all_ranges = false;
if (u().is_char(elem)) {
all_ranges = true;
unsigned ch = 0, ch2 = 0;
svector<std::pair<unsigned, unsigned>> ranges, ranges1;
ranges.push_back(std::make_pair(0, u().max_char()));
auto exclude_char = [&](unsigned ch) {
if (ch == 0) {
intersect(1, u().max_char(), ranges);
}
else if (ch == u().max_char()) {
intersect(0, ch-1, ranges);
auto exclude_range = [&](unsigned lower, unsigned upper) {
SASSERT(lower <= upper);
if (lower == 0) {
if (upper == u().max_char())
ranges.reset();
else
intersect(upper + 1, u().max_char(), ranges);
}
else if (upper == u().max_char())
intersect(0, lower - 1, ranges);
else {
// not(lower <= e <= upper) iff ((0 <= e <= lower-1) or (upper+1 <= e <= max))
// Note that this transformation is correct only when lower <= upper
ranges1.reset();
ranges1.append(ranges);
intersect(0, ch - 1, ranges);
intersect(ch + 1, u().max_char(), ranges1);
intersect(0, lower - 1, ranges);
intersect(upper + 1, u().max_char(), ranges1);
ranges.append(ranges1);
}
};
bool all_ranges = true;
bool negated = false;
for (expr* e : conds) {
if (m().is_eq(e, lhs, rhs) && elem == lhs && u().is_const_char(rhs, ch)) {
intersect(ch, ch, ranges);
if (u().is_char_const_range(elem, e, ch, ch2, negated)) {
if (ch > ch2) {
if (negated)
// !(ch <= elem <= ch2) is trivially true
continue;
else
// (ch <= elem <= ch2) is trivially false
ranges.reset();
}
else if (negated)
exclude_range(ch, ch2);
else
intersect(ch, ch2, ranges);
conds_range.push_back(e);
}
else if (m().is_eq(e, lhs, rhs) && elem == rhs && u().is_const_char(lhs, ch)) {
intersect(ch, ch, ranges);
}
else if (u().is_char_le(e, lhs, rhs) && elem == lhs && u().is_const_char(rhs, ch)) {
intersect(0, ch, ranges);
}
else if (u().is_char_le(e, lhs, rhs) && elem == rhs && u().is_const_char(lhs, ch)) {
intersect(ch, u().max_char(), ranges);
}
else if (m().is_not(e, e1) && m().is_eq(e1, lhs, rhs) && elem == lhs && u().is_const_char(rhs, ch)) {
exclude_char(ch);
}
else if (m().is_not(e, e1) && m().is_eq(e1, lhs, rhs) && elem == rhs && u().is_const_char(lhs, ch)) {
exclude_char(ch);
}
else if (m().is_not(e, e1) && u().is_char_le(e1, lhs, rhs) && elem == lhs && u().is_const_char(rhs, ch)) {
// not (e <= ch)
if (ch == u().max_char())
ranges.reset();
else
intersect(ch+1, u().max_char(), ranges);
}
else if (m().is_not(e, e1) && u().is_char_le(e1, lhs, rhs) && elem == rhs && u().is_const_char(lhs, ch)) {
// not (ch <= e)
if (ch == 0)
ranges.reset();
else
intersect(0, ch-1, ranges);
}
else if (m().is_true(e) || (m().is_eq(e, lhs, rhs) && lhs == rhs)) {
// trivially true
// trivially true conditions
else if (m().is_true(e) || (m().is_eq(e, lhs, rhs) && lhs == rhs))
continue;
}
else if (m().is_not(e, e1) && m().is_eq(e1, lhs, rhs) && u().is_const_char(lhs, ch) && u().is_const_char(rhs, ch2) && ch != ch2) {
// trivially true
else if (m().is_not(e, e1) && m().is_eq(e1, lhs, rhs) && u().is_const_char(lhs, ch) && u().is_const_char(rhs, ch2) && ch != ch2)
continue;
}
else if (m().is_false(e) || (m().is_not(e, e1) && m().is_eq(e1, lhs, rhs) && lhs == rhs)) {
// trivially false
cond = m().mk_false();
return;
}
else if (u().is_char_le(e, lhs, rhs) && u().is_const_char(lhs, ch) && u().is_const_char(rhs, ch2) && ch <= ch2)
continue;
else if (m().is_not(e, e1) && u().is_char_le(e1, lhs, rhs) && u().is_const_char(lhs, ch) && u().is_const_char(rhs, ch2) && ch > ch2)
continue;
// trivially false conditions
else if (m().is_false(e) || (m().is_not(e, e1) && m().is_eq(e1, lhs, rhs) && lhs == rhs))
ranges.reset();
else if (u().is_char_le(e, lhs, rhs) && u().is_const_char(lhs, ch) && u().is_const_char(rhs, ch2) && ch > ch2)
ranges.reset();
else if (m().is_not(e, e1) && u().is_char_le(e1, lhs, rhs) && u().is_const_char(lhs, ch) && u().is_const_char(rhs, ch2) && ch <= ch2)
ranges.reset();
else {
all_ranges = false;
break;
@ -5164,6 +5031,7 @@ void seq_rewriter::elim_condition(expr* elem, expr_ref& cond) {
cond = m().mk_true();
return;
}
conds.set(conds_range);
}
}
@ -5186,6 +5054,15 @@ void seq_rewriter::elim_condition(expr* elem, expr_ref& cond) {
cond = m().mk_and(m().mk_eq(elem, solution), cond);
}
}
else if (all_ranges) {
if (conds.empty())
// all ranges were removed as trivially true
cond = m().mk_true();
else if (conds.size() == 1)
cond = conds.get(0);
else
cond = m().mk_and(conds);
}
}

10
src/ast/rewriter/seq_rewriter.h
View file

@ -223,11 +223,6 @@ class seq_rewriter {
expr_ref merge_regex_sets(expr* r1, expr* r2, expr* unit, std::function<bool(expr*, expr*&, expr*&)>& decompose, std::function<expr* (expr*, expr*)>& compose);
// Apply simplifications and keep the representation normalized
// Assuming r1 and r2 are normalized
expr_ref mk_regex_union_normalize(expr* r1, expr* r2);
expr_ref mk_regex_inter_normalize(expr* r1, expr* r2);
// elem is (:var 0) and path a condition that may have (:var 0) as a free variable
// simplify path, e.g., (:var 0) = 'a' & (:var 0) = 'b' is simplified to false
expr_ref simplify_path(expr* elem, expr* path);
@ -423,5 +418,10 @@ public:
// heuristic elimination of element from condition that comes form a derivative.
// special case optimization for conjunctions of equalities, disequalities and ranges.
void elim_condition(expr* elem, expr_ref& cond);
/* Apply simplifications to the union to keep the union normalized (r1 and r2 are not normalized)*/
expr_ref mk_regex_union_normalize(expr* r1, expr* r2);
/* Apply simplifications to the intersection to keep it normalized (r1 and r2 are not normalized)*/
expr_ref mk_regex_inter_normalize(expr* r1, expr* r2);
};

50
src/ast/seq_decl_plugin.cpp
View file

@ -831,6 +831,39 @@ app* seq_util::mk_lt(expr* ch1, expr* ch2) const {
return m.mk_not(mk_le(ch2, ch1));
}
bool seq_util::is_char_const_range(expr const* x, expr* e, unsigned& l, unsigned& u, bool& negated) const {
expr* a, * b, * e0, * e1, * e2, * lb, * ub;
e1 = e;
negated = (m.is_not(e, e1)) ? true : false;
if (m.is_eq(e1, a, b) && (a == x && is_const_char(b, l))) {
u = l;
return true;
}
if (is_char_le(e1, a, b) && a == x && is_const_char(b, u)) {
// (x <= u)
l = 0;
return true;
}
if (is_char_le(e1, a, b) && b == x && is_const_char(a, l)) {
// (l <= x)
u = max_char();
return true;
}
if (m.is_and(e1, e0, e2) && is_char_le(e0, lb, a) && a == x && is_const_char(lb, l) &&
is_char_le(e2, b, ub) && b == x && is_const_char(ub, u))
// (l <= x) & (x <= u)
return true;
if (m.is_eq(e1, a, b) && b == x && is_const_char(a, l)) {
u = l;
return true;
}
if (m.is_and(e1, e0, e2) && is_char_le(e0, a, ub) && a == x && is_const_char(ub, u) &&
is_char_le(e2, lb, b) && b == x && is_const_char(lb, l))
// (x <= u) & (l <= x)
return true;
return false;
}
bool seq_util::str::is_string(func_decl const* f, zstring& s) const {
if (is_string(f)) {
s = f->get_parameter(0).get_zstring();
@ -1030,6 +1063,23 @@ app* seq_util::rex::mk_loop(expr* r, unsigned lo, unsigned hi) {
return m.mk_app(m_fid, OP_RE_LOOP, 2, params, 1, &r);
}
expr* seq_util::rex::mk_loop_proper(expr* r, unsigned lo, unsigned hi)
{
if (lo == 0 && hi == 0) {
sort* seq_sort = nullptr;
VERIFY(u.is_re(r, seq_sort));
// avoid creating a loop with both bounds 0
// such an expression is invalid as a loop
// it is BY DEFINITION = epsilon
return mk_epsilon(seq_sort);
}
if (lo == 1 && hi == 1)
// do not create a loop unless it actually is a loop
return r;
parameter params[2] = { parameter(lo), parameter(hi) };
return m.mk_app(m_fid, OP_RE_LOOP, 2, params, 1, &r);
}
app* seq_util::rex::mk_loop(expr* r, expr* lo) {
expr* rs[2] = { r, lo };
return m.mk_app(m_fid, OP_RE_LOOP, 0, nullptr, 2, rs);

7
src/ast/seq_decl_plugin.h
View file

@ -252,6 +252,12 @@ public:
unsigned max_char() const { return seq.max_char(); }
unsigned num_bits() const { return seq.num_bits(); }
/*
e has a form that is equivalent to l <= x <= u (then negated = false)
or e is equivalent to !(l <= x <= u) (then negated = true)
*/
bool is_char_const_range(expr const* x, expr * e, unsigned& l, unsigned& u, bool& negated) const;
app* mk_skolem(symbol const& name, unsigned n, expr* const* args, sort* range);
bool is_skolem(expr const* e) const { return is_app_of(e, m_fid, _OP_SEQ_SKOLEM); }
@ -498,6 +504,7 @@ public:
app* mk_opt(expr* r) { return m.mk_app(m_fid, OP_RE_OPTION, r); }
app* mk_loop(expr* r, unsigned lo);
app* mk_loop(expr* r, unsigned lo, unsigned hi);
expr* mk_loop_proper(expr* r, unsigned lo, unsigned hi);
app* mk_loop(expr* r, expr* lo);
app* mk_loop(expr* r, expr* lo, expr* hi);
app* mk_full_char(sort* s);

24
src/cmd_context/pdecl.cpp
View file

@ -416,9 +416,9 @@ void psort_builtin_decl::display(std::ostream & out) const {
void ptype::display(std::ostream & out, pdatatype_decl const * const * dts) const {
switch (kind()) {
case PTR_PSORT: get_psort()->display(out); break;
case PTR_REC_REF: out << dts[get_idx()]->get_name(); break;
case PTR_MISSING_REF: out << get_missing_ref(); break;
case ptype_kind::PTR_PSORT: get_psort()->display(out); break;
case ptype_kind::PTR_REC_REF: out << dts[get_idx()]->get_name(); break;
case ptype_kind::PTR_MISSING_REF: out << get_missing_ref(); break;
}
}
@ -426,19 +426,19 @@ paccessor_decl::paccessor_decl(unsigned id, unsigned num_params, pdecl_manager &
pdecl(id, num_params),
m_name(n),
m_type(r) {
if (m_type.kind() == PTR_PSORT) {
if (m_type.kind() == ptype_kind::PTR_PSORT) {
m.inc_ref(r.get_psort());
}
}
void paccessor_decl::finalize(pdecl_manager & m) {
if (m_type.kind() == PTR_PSORT) {
if (m_type.kind() == ptype_kind::PTR_PSORT) {
m.lazy_dec_ref(m_type.get_psort());
}
}
bool paccessor_decl::has_missing_refs(symbol & missing) const {
if (m_type.kind() == PTR_MISSING_REF) {
if (m_type.kind() == ptype_kind::PTR_MISSING_REF) {
missing = m_type.get_missing_ref();
return true;
}
@ -446,14 +446,14 @@ bool paccessor_decl::has_missing_refs(symbol & missing) const {
}
bool paccessor_decl::fix_missing_refs(dictionary<int> const & symbol2idx, symbol & missing) {
TRACE("fix_missing_refs", tout << "m_type.kind(): " << m_type.kind() << "\n";
if (m_type.kind() == PTR_MISSING_REF) tout << m_type.get_missing_ref() << "\n";);
if (m_type.kind() != PTR_MISSING_REF)
TRACE("fix_missing_refs", tout << "m_type.kind(): " << (int)m_type.kind() << "\n";
if (m_type.kind() == ptype_kind::PTR_MISSING_REF) tout << m_type.get_missing_ref() << "\n";);
if (m_type.kind() != ptype_kind::PTR_MISSING_REF)
return true;
int idx;
if (symbol2idx.find(m_type.get_missing_ref(), idx)) {
m_type = ptype(idx);
SASSERT(m_type.kind() == PTR_REC_REF);
SASSERT(m_type.kind() == ptype_kind::PTR_REC_REF);
return true;
}
missing = m_type.get_missing_ref();
@ -462,8 +462,8 @@ bool paccessor_decl::fix_missing_refs(dictionary<int> const & symbol2idx, symbol
accessor_decl * paccessor_decl::instantiate_decl(pdecl_manager & m, unsigned n, sort * const * s) {
switch (m_type.kind()) {
case PTR_REC_REF: return mk_accessor_decl(m.m(), m_name, type_ref(m_type.get_idx()));
case PTR_PSORT: return mk_accessor_decl(m.m(), m_name, type_ref(m_type.get_psort()->instantiate(m, n, s)));
case ptype_kind::PTR_REC_REF: return mk_accessor_decl(m.m(), m_name, type_ref(m_type.get_idx()));
case ptype_kind::PTR_PSORT: return mk_accessor_decl(m.m(), m_name, type_ref(m_type.get_psort()->instantiate(m, n, s)));
default:
// missing refs must have been eliminated.
UNREACHABLE();

16
src/cmd_context/pdecl.h
View file

@ -157,7 +157,7 @@ class pdatatype_decl;
class pconstructor_decl;
class paccessor_decl;
enum ptype_kind {
enum class ptype_kind {
PTR_PSORT, // psort
PTR_REC_REF, // recursive reference
PTR_MISSING_REF // a symbol, it is useful for building parsers.
@ -171,14 +171,14 @@ class ptype {
};
symbol m_missing_ref;
public:
ptype():m_kind(PTR_PSORT), m_sort(nullptr) {}
ptype(int idx):m_kind(PTR_REC_REF), m_idx(idx) {}
ptype(psort * s):m_kind(PTR_PSORT), m_sort(s) {}
ptype(symbol const & s):m_kind(PTR_MISSING_REF), m_missing_ref(s) {}
ptype():m_kind(ptype_kind::PTR_PSORT), m_sort(nullptr) {}
ptype(int idx):m_kind(ptype_kind::PTR_REC_REF), m_idx(idx) {}
ptype(psort * s):m_kind(ptype_kind::PTR_PSORT), m_sort(s) {}
ptype(symbol const & s):m_kind(ptype_kind::PTR_MISSING_REF), m_sort(nullptr), m_missing_ref(s) {}
ptype_kind kind() const { return m_kind; }
psort * get_psort() const { SASSERT(kind() == PTR_PSORT); return m_sort; }
int get_idx() const { SASSERT(kind() == PTR_REC_REF); return m_idx; }
symbol const & get_missing_ref() const { SASSERT(kind() == PTR_MISSING_REF); return m_missing_ref; }
psort * get_psort() const { SASSERT(kind() == ptype_kind::PTR_PSORT); return m_sort; }
int get_idx() const { SASSERT(kind() == ptype_kind::PTR_REC_REF); return m_idx; }
symbol const & get_missing_ref() const { SASSERT(kind() == ptype_kind::PTR_MISSING_REF); return m_missing_ref; }
void display(std::ostream & out, pdatatype_decl const * const * dts) const;
};

4
src/sat/sat_solver/inc_sat_solver.cpp
View file

@ -683,8 +683,8 @@ public:
ensure_euf()->user_propagate_register_diseq(diseq_eh);
}
unsigned user_propagate_register(expr* e) override {
return ensure_euf()->user_propagate_register(e);
unsigned user_propagate_register_expr(expr* e) override {
return ensure_euf()->user_propagate_register_expr(e);
}
private:

2
src/sat/smt/euf_solver.h
View file

@ -425,7 +425,7 @@ namespace euf {
check_for_user_propagator();
m_user_propagator->register_diseq(diseq_eh);
}
unsigned user_propagate_register(expr* e) {
unsigned user_propagate_register_expr(expr* e) {
check_for_user_propagator();
return m_user_propagator->add_expr(e);
}

4
src/smt/params/preprocessor_params.cpp
View file

@ -40,8 +40,8 @@ void preprocessor_params::display(std::ostream & out) const {
pattern_inference_params::display(out);
bit_blaster_params::display(out);
DISPLAY_PARAM(m_lift_ite);
DISPLAY_PARAM(m_ng_lift_ite);
DISPLAY_PARAM((int)m_lift_ite);
DISPLAY_PARAM((int)m_ng_lift_ite);
DISPLAY_PARAM(m_pull_cheap_ite);
DISPLAY_PARAM(m_pull_nested_quantifiers);
DISPLAY_PARAM(m_eliminate_term_ite);

6
src/smt/params/preprocessor_params.h
View file

@ -21,7 +21,7 @@ Revision History:
#include "params/pattern_inference_params.h"
#include "params/bit_blaster_params.h"
enum lift_ite_kind {
enum class lift_ite_kind {
LI_NONE,
LI_CONSERVATIVE,
LI_FULL
@ -50,8 +50,8 @@ struct preprocessor_params : public pattern_inference_params,
public:
preprocessor_params(params_ref const & p = params_ref()):
m_lift_ite(LI_NONE),
m_ng_lift_ite(LI_NONE),
m_lift_ite(lift_ite_kind::LI_NONE),
m_ng_lift_ite(lift_ite_kind::LI_NONE),
m_pull_cheap_ite(false),
m_pull_nested_quantifiers(false),
m_eliminate_term_ite(false),

10
src/smt/smt_context.h
View file

@ -1723,24 +1723,18 @@ namespace smt {
m_user_propagator->register_diseq(diseq_eh);
}
unsigned user_propagate_register(expr* e) {
unsigned user_propagate_register_expr(expr* e) {
if (!m_user_propagator)
throw default_exception("user propagator must be initialized");
return m_user_propagator->add_expr(e);
}
void user_propagate_register_created(user_propagator::register_created_eh_t& r) {
void user_propagate_register_created(user_propagator::created_eh_t& r) {
if (!m_user_propagator)
throw default_exception("user propagator must be initialized");
m_user_propagator->register_created(r);
}
func_decl* user_propagate_declare(symbol const& name, unsigned n, sort* const* domain, sort* range) {
if (!m_user_propagator)
throw default_exception("user propagator must be initialized");
return m_user_propagator->declare(name, n, domain, range);
}
bool watches_fixed(enode* n) const;
void assign_fixed(enode* n, expr* val, unsigned sz, literal const* explain);

322
src/smt/smt_kernel.cpp
View file

@ -32,31 +32,11 @@ namespace smt {
m_kernel(m, fp, p),
m_params(p) {
}
static void copy(imp& src, imp& dst) {
context::copy(src.m_kernel, dst.m_kernel);
}
smt_params & fparams() {
return m_kernel.get_fparams();
}
params_ref const & params() {
return m_params;
}
ast_manager & m() const {
return m_kernel.get_manager();
}
bool set_logic(symbol logic) {
return m_kernel.set_logic(logic);
}
void set_progress_callback(progress_callback * callback) {
return m_kernel.set_progress_callback(callback);
}
void display(std::ostream & out) const {
// m_kernel.display(out); <<< for external users it is just junk
// TODO: it will be replaced with assertion_stack.display
@ -67,195 +47,7 @@ namespace smt {
out << "\n " << mk_ismt2_pp(f, m(), 2);
}
out << ")";
}
void assert_expr(expr * e) {
TRACE("smt_kernel", tout << "assert:\n" << mk_ismt2_pp(e, m()) << "\n";);
m_kernel.assert_expr(e);
}
void assert_expr(expr * e, proof * pr) {
m_kernel.assert_expr(e, pr);
}
unsigned size() const {
return m_kernel.get_num_asserted_formulas();
}
void get_formulas(ptr_vector<expr>& fmls) const {
m_kernel.get_asserted_formulas(fmls);
}
expr* get_formula(unsigned i) const {
return m_kernel.get_asserted_formula(i);
}
void push() {
TRACE("smt_kernel", tout << "push()\n";);
m_kernel.push();
}
void pop(unsigned num_scopes) {
TRACE("smt_kernel", tout << "pop()\n";);
m_kernel.pop(num_scopes);
}
unsigned get_scope_level() const {
return m_kernel.get_scope_level();
}
lbool setup_and_check() {
return m_kernel.setup_and_check();
}
bool inconsistent() {
return m_kernel.inconsistent();
}
lbool check(unsigned num_assumptions, expr * const * assumptions) {
return m_kernel.check(num_assumptions, assumptions);
}
lbool check(expr_ref_vector const& cube, vector<expr_ref_vector> const& clause) {
return m_kernel.check(cube, clause);
}
lbool get_consequences(expr_ref_vector const& assumptions, expr_ref_vector const& vars, expr_ref_vector& conseq, expr_ref_vector& unfixed) {
return m_kernel.get_consequences(assumptions, vars, conseq, unfixed);
}
lbool preferred_sat(expr_ref_vector const& asms, vector<expr_ref_vector>& cores) {
return m_kernel.preferred_sat(asms, cores);
}
lbool find_mutexes(expr_ref_vector const& vars, vector<expr_ref_vector>& mutexes) {
return m_kernel.find_mutexes(vars, mutexes);
}
void get_model(model_ref & m) {
m_kernel.get_model(m);
}
proof * get_proof() {
return m_kernel.get_proof();
}
unsigned get_unsat_core_size() const {
return m_kernel.get_unsat_core_size();
}
expr * get_unsat_core_expr(unsigned idx) const {
return m_kernel.get_unsat_core_expr(idx);
}
void get_levels(ptr_vector<expr> const& vars, unsigned_vector& depth) {
m_kernel.get_levels(vars, depth);
}
expr_ref_vector get_trail() {
return m_kernel.get_trail();
}
failure last_failure() const {
return m_kernel.get_last_search_failure();
}
std::string last_failure_as_string() const {
return m_kernel.last_failure_as_string();
}
void set_reason_unknown(char const* msg) {
m_kernel.set_reason_unknown(msg);
}
void get_assignments(expr_ref_vector & result) {
m_kernel.get_assignments(result);
}
void get_relevant_labels(expr * cnstr, buffer<symbol> & result) {
m_kernel.get_relevant_labels(cnstr, result);
}
void get_relevant_labeled_literals(bool at_lbls, expr_ref_vector & result) {
m_kernel.get_relevant_labeled_literals(at_lbls, result);
}
void get_relevant_literals(expr_ref_vector & result) {
m_kernel.get_relevant_literals(result);
}
void get_guessed_literals(expr_ref_vector & result) {
m_kernel.get_guessed_literals(result);
}
expr_ref next_cube() {
lookahead lh(m_kernel);
return lh.choose();
}
expr_ref_vector cubes(unsigned depth) {
lookahead lh(m_kernel);
return lh.choose_rec(depth);
}
void collect_statistics(::statistics & st) const {
m_kernel.collect_statistics(st);
}
void reset_statistics() {
}
void display_statistics(std::ostream & out) const {
m_kernel.display_statistics(out);
}
void display_istatistics(std::ostream & out) const {
m_kernel.display_istatistics(out);
}
bool canceled() {
return m_kernel.get_cancel_flag();
}
void updt_params(params_ref const & p) {
m_kernel.updt_params(p);
}
void user_propagate_init(
void* ctx,
user_propagator::push_eh_t& push_eh,
user_propagator::pop_eh_t& pop_eh,
user_propagator::fresh_eh_t& fresh_eh) {
m_kernel.user_propagate_init(ctx, push_eh, pop_eh, fresh_eh);
}
void user_propagate_register_final(user_propagator::final_eh_t& final_eh) {
m_kernel.user_propagate_register_final(final_eh);
}
void user_propagate_register_fixed(user_propagator::fixed_eh_t& fixed_eh) {
m_kernel.user_propagate_register_fixed(fixed_eh);
}
void user_propagate_register_eq(user_propagator::eq_eh_t& eq_eh) {
m_kernel.user_propagate_register_eq(eq_eh);
}
void user_propagate_register_diseq(user_propagator::eq_eh_t& diseq_eh) {
m_kernel.user_propagate_register_diseq(diseq_eh);
}
unsigned user_propagate_register(expr* e) {
return m_kernel.user_propagate_register(e);
}
void user_propagate_register_created(user_propagator::register_created_eh_t& r) {
m_kernel.user_propagate_register_created(r);
}
func_decl* user_propagate_declare(symbol const& name, unsigned n, sort* const* domain, sort* range) {
return m_kernel.user_propagate_declare(name, n, domain, range);
}
}
};
@ -268,147 +60,148 @@ namespace smt {
}
ast_manager & kernel::m() const {
return m_imp->m();
return m_imp->m_kernel.get_manager();
}
void kernel::copy(kernel& src, kernel& dst) {
imp::copy(*src.m_imp, *dst.m_imp);
context::copy(src.m_imp->m_kernel, dst.m_imp->m_kernel);
}
bool kernel::set_logic(symbol logic) {
return m_imp->set_logic(logic);
return m_imp->m_kernel.set_logic(logic);
}
void kernel::set_progress_callback(progress_callback * callback) {
m_imp->set_progress_callback(callback);
m_imp->m_kernel.set_progress_callback(callback);
}
void kernel::assert_expr(expr * e) {
m_imp->assert_expr(e);
m_imp->m_kernel.assert_expr(e);
}
void kernel::assert_expr(expr_ref_vector const& es) {
for (unsigned i = 0; i < es.size(); ++i) {
m_imp->assert_expr(es[i]);
}
for (unsigned i = 0; i < es.size(); ++i)
m_imp->m_kernel.assert_expr(es[i]);
}
void kernel::assert_expr(expr * e, proof * pr) {
m_imp->assert_expr(e, pr);
m_imp->m_kernel.assert_expr(e, pr);
}
unsigned kernel::size() const {
return m_imp->size();
return m_imp->m_kernel.get_num_asserted_formulas();
}
expr* kernel::get_formula(unsigned i) const {
return m_imp->get_formula(i);
return m_imp->m_kernel.get_asserted_formula(i);
}
void kernel::push() {
m_imp->push();
m_imp->m_kernel.push();
}
void kernel::pop(unsigned num_scopes) {
m_imp->pop(num_scopes);
m_imp->m_kernel.pop(num_scopes);
}
unsigned kernel::get_scope_level() const {
return m_imp->get_scope_level();
return m_imp->m_kernel.get_scope_level();
}
void kernel::reset() {
ast_manager & _m = m();
smt_params & fps = m_imp->fparams();
params_ref ps = m_imp->params();
smt_params& fps = m_imp->m_kernel.get_fparams();
params_ref ps = m_imp->m_params;
m_imp->~imp();
m_imp = new (m_imp) imp(_m, fps, ps);
}
bool kernel::inconsistent() {
return m_imp->inconsistent();
return m_imp->m_kernel.inconsistent();
}
lbool kernel::setup_and_check() {
return m_imp->setup_and_check();
return m_imp->m_kernel.setup_and_check();
}
lbool kernel::check(unsigned num_assumptions, expr * const * assumptions) {
lbool r = m_imp->check(num_assumptions, assumptions);
lbool r = m_imp->m_kernel.check(num_assumptions, assumptions);
TRACE("smt_kernel", tout << "check result: " << r << "\n";);
return r;
}
lbool kernel::check(expr_ref_vector const& cube, vector<expr_ref_vector> const& clauses) {
return m_imp->check(cube, clauses);
return m_imp->m_kernel.check(cube, clauses);
}
lbool kernel::get_consequences(expr_ref_vector const& assumptions, expr_ref_vector const& vars, expr_ref_vector& conseq, expr_ref_vector& unfixed) {
return m_imp->get_consequences(assumptions, vars, conseq, unfixed);
return m_imp->m_kernel.get_consequences(assumptions, vars, conseq, unfixed);
}
lbool kernel::preferred_sat(expr_ref_vector const& asms, vector<expr_ref_vector>& cores) {
return m_imp->preferred_sat(asms, cores);
return m_imp->m_kernel.preferred_sat(asms, cores);
}
lbool kernel::find_mutexes(expr_ref_vector const& vars, vector<expr_ref_vector>& mutexes) {
return m_imp->find_mutexes(vars, mutexes);
return m_imp->m_kernel.find_mutexes(vars, mutexes);
}
void kernel::get_model(model_ref & m) {
m_imp->get_model(m);
m_imp->m_kernel.get_model(m);
}
proof * kernel::get_proof() {
return m_imp->get_proof();
return m_imp->m_kernel.get_proof();
}
unsigned kernel::get_unsat_core_size() const {
return m_imp->get_unsat_core_size();
return m_imp->m_kernel.get_unsat_core_size();
}
expr * kernel::get_unsat_core_expr(unsigned idx) const {
return m_imp->get_unsat_core_expr(idx);
return m_imp->m_kernel.get_unsat_core_expr(idx);
}
failure kernel::last_failure() const {
return m_imp->last_failure();
return m_imp->m_kernel.get_last_search_failure();
}
std::string kernel::last_failure_as_string() const {
return m_imp->last_failure_as_string();
return m_imp->m_kernel.last_failure_as_string();
}
void kernel::set_reason_unknown(char const* msg) {
m_imp->set_reason_unknown(msg);
m_imp->m_kernel.set_reason_unknown(msg);
}
void kernel::get_assignments(expr_ref_vector & result) {
m_imp->get_assignments(result);
m_imp->m_kernel.get_assignments(result);
}
void kernel::get_relevant_labels(expr * cnstr, buffer<symbol> & result) {
m_imp->get_relevant_labels(cnstr, result);
m_imp->m_kernel.get_relevant_labels(cnstr, result);
}
void kernel::get_relevant_labeled_literals(bool at_lbls, expr_ref_vector & result) {
m_imp->get_relevant_labeled_literals(at_lbls, result);
m_imp->m_kernel.get_relevant_labeled_literals(at_lbls, result);
}
void kernel::get_relevant_literals(expr_ref_vector & result) {
m_imp->get_relevant_literals(result);
m_imp->m_kernel.get_relevant_literals(result);
}
void kernel::get_guessed_literals(expr_ref_vector & result) {
m_imp->get_guessed_literals(result);
m_imp->m_kernel.get_guessed_literals(result);
}
expr_ref kernel::next_cube() {
return m_imp->next_cube();
lookahead lh(m_imp->m_kernel);
return lh.choose();
}
expr_ref_vector kernel::cubes(unsigned depth) {
return m_imp->cubes(depth);
lookahead lh(m_imp->m_kernel);
return lh.choose_rec(depth);
}
std::ostream& kernel::display(std::ostream & out) const {
@ -417,27 +210,26 @@ namespace smt {
}
void kernel::collect_statistics(::statistics & st) const {
m_imp->collect_statistics(st);
m_imp->m_kernel.collect_statistics(st);
}
void kernel::reset_statistics() {
m_imp->reset_statistics();
}
void kernel::display_statistics(std::ostream & out) const {
m_imp->display_statistics(out);
m_imp->m_kernel.display_statistics(out);
}
void kernel::display_istatistics(std::ostream & out) const {
m_imp->display_istatistics(out);
m_imp->m_kernel.display_istatistics(out);
}
bool kernel::canceled() const {
return m_imp->canceled();
return m_imp->m_kernel.get_cancel_flag();
}
void kernel::updt_params(params_ref const & p) {
return m_imp->updt_params(p);
return m_imp->m_kernel.updt_params(p);
}
void kernel::collect_param_descrs(param_descrs & d) {
@ -449,11 +241,11 @@ namespace smt {
}
void kernel::get_levels(ptr_vector<expr> const& vars, unsigned_vector& depth) {
m_imp->get_levels(vars, depth);
m_imp->m_kernel.get_levels(vars, depth);
}
expr_ref_vector kernel::get_trail() {
return m_imp->get_trail();
return m_imp->m_kernel.get_trail();
}
void kernel::user_propagate_init(
@ -461,35 +253,31 @@ namespace smt {
user_propagator::push_eh_t& push_eh,
user_propagator::pop_eh_t& pop_eh,
user_propagator::fresh_eh_t& fresh_eh) {
m_imp->user_propagate_init(ctx, push_eh, pop_eh, fresh_eh);
m_imp->m_kernel.user_propagate_init(ctx, push_eh, pop_eh, fresh_eh);
}
void kernel::user_propagate_register_fixed(user_propagator::fixed_eh_t& fixed_eh) {
m_imp->user_propagate_register_fixed(fixed_eh);
m_imp->m_kernel.user_propagate_register_fixed(fixed_eh);
}
void kernel::user_propagate_register_final(user_propagator::final_eh_t& final_eh) {
m_imp->user_propagate_register_final(final_eh);
m_imp->m_kernel.user_propagate_register_final(final_eh);
}
void kernel::user_propagate_register_eq(user_propagator::eq_eh_t& eq_eh) {
m_imp->user_propagate_register_eq(eq_eh);
m_imp->m_kernel.user_propagate_register_eq(eq_eh);
}
void kernel::user_propagate_register_diseq(user_propagator::eq_eh_t& diseq_eh) {
m_imp->user_propagate_register_diseq(diseq_eh);
m_imp->m_kernel.user_propagate_register_diseq(diseq_eh);
}
unsigned kernel::user_propagate_register(expr* e) {
return m_imp->user_propagate_register(e);
unsigned kernel::user_propagate_register_expr(expr* e) {
return m_imp->m_kernel.user_propagate_register_expr(e);
}
void kernel::user_propagate_register_created(user_propagator::register_created_eh_t& r) {
m_imp->user_propagate_register_created(r);
}
func_decl* kernel::user_propagate_declare(symbol const& name, unsigned n, sort* const* domain, sort* range) {
return m_imp->user_propagate_declare(name, n, domain, range);
void kernel::user_propagate_register_created(user_propagator::created_eh_t& r) {
m_imp->m_kernel.user_propagate_register_created(r);
}
};

6
src/smt/smt_kernel.h
View file

@ -301,11 +301,9 @@ namespace smt {
void user_propagate_register_diseq(user_propagator::eq_eh_t& diseq_eh);
unsigned user_propagate_register(expr* e);
unsigned user_propagate_register_expr(expr* e);
void user_propagate_register_created(user_propagator::register_created_eh_t& r);
func_decl* user_propagate_declare(symbol const& name, unsigned n, sort* const* domain, sort* range);
void user_propagate_register_created(user_propagator::created_eh_t& r);
/**
\brief Return a reference to smt::context.

8
src/smt/smt_setup.cpp
View file

@ -643,8 +643,8 @@ namespace smt {
// It destroys the existing patterns.
// m_params.m_macro_finder = true;
if (m_params.m_ng_lift_ite == LI_NONE)
m_params.m_ng_lift_ite = LI_CONSERVATIVE;
if (m_params.m_ng_lift_ite == lift_ite_kind::LI_NONE)
m_params.m_ng_lift_ite = lift_ite_kind::LI_CONSERVATIVE;
TRACE("setup", tout << "max_eager_multipatterns: " << m_params.m_qi_max_eager_multipatterns << "\n";);
m_context.register_plugin(alloc(smt::theory_i_arith, m_context));
setup_arrays();
@ -668,8 +668,8 @@ namespace smt {
m_params.m_qi_lazy_threshold = 20;
//
m_params.m_macro_finder = true;
if (m_params.m_ng_lift_ite == LI_NONE)
m_params.m_ng_lift_ite = LI_CONSERVATIVE;
if (m_params.m_ng_lift_ite == lift_ite_kind::LI_NONE)
m_params.m_ng_lift_ite = lift_ite_kind::LI_CONSERVATIVE;
m_params.m_pi_max_multi_patterns = 10; //<< it was used for SMT-COMP
m_params.m_array_lazy_ieq = true;
m_params.m_array_lazy_ieq_delay = 4;

11
src/smt/smt_solver.cpp
View file

@ -200,7 +200,6 @@ namespace {
return m_context.check(num_assumptions, assumptions);
}
lbool check_sat_cc_core(expr_ref_vector const& cube, vector<expr_ref_vector> const& clauses) override {
return m_context.check(cube, clauses);
}
@ -237,18 +236,14 @@ namespace {
m_context.user_propagate_register_diseq(diseq_eh);
}
unsigned user_propagate_register(expr* e) override {
return m_context.user_propagate_register(e);
unsigned user_propagate_register_expr(expr* e) override {
return m_context.user_propagate_register_expr(e);
}
void user_propagate_register_created(user_propagator::register_created_eh_t& c) override {
void user_propagate_register_created(user_propagator::created_eh_t& c) override {
m_context.user_propagate_register_created(c);
}
func_decl* user_propagate_declare(symbol const& name, unsigned n, sort* const* domain, sort* range) {
return m_context.user_propagate_declare(name, n, domain, range);
}
struct scoped_minimize_core {
smt_solver& s;
expr_ref_vector m_assumptions;

14
src/smt/tactic/smt_tactic_core.cpp
View file

@ -319,7 +319,7 @@ public:
user_propagator::final_eh_t m_final_eh;
user_propagator::eq_eh_t m_eq_eh;
user_propagator::eq_eh_t m_diseq_eh;
user_propagator::register_created_eh_t m_created_eh;
user_propagator::created_eh_t m_created_eh;
expr_ref_vector m_vars;
unsigned_vector m_var2internal;
@ -333,7 +333,7 @@ public:
user_propagator::final_eh_t i_final_eh;
user_propagator::eq_eh_t i_eq_eh;
user_propagator::eq_eh_t i_diseq_eh;
user_propagator::register_created_eh_t i_created_eh;
user_propagator::created_eh_t i_created_eh;
struct callback : public user_propagator::callback {
@ -449,7 +449,7 @@ public:
unsigned i = 0;
for (expr* v : m_vars) {
unsigned j = m_ctx->user_propagate_register(v);
unsigned j = m_ctx->user_propagate_register_expr(v);
m_var2internal.setx(i, j, 0);
m_internal2var.setx(j, i, 0);
++i;
@ -493,16 +493,12 @@ public:
m_diseq_eh = diseq_eh;
}
unsigned user_propagate_register(expr* e) override {
unsigned user_propagate_register_expr(expr* e) override {
m_vars.push_back(e);
return m_vars.size() - 1;
}
func_decl* user_propagate_declare(symbol const& name, unsigned n, sort* const* domain, sort* range) override {
return m_ctx->user_propagate_declare(name, n, domain, range);
}
void user_propagate_register_created(user_propagator::register_created_eh_t& created_eh) override {
void user_propagate_register_created(user_propagator::created_eh_t& created_eh) override {
m_ctx->user_propagate_register_created(created_eh);
}
};

12
src/smt/theory_user_propagator.cpp
View file

@ -23,7 +23,7 @@ Author:
using namespace smt;
theory_user_propagator::theory_user_propagator(context& ctx):
theory(ctx, ctx.get_manager().mk_family_id("user_propagator"))
theory(ctx, ctx.get_manager().mk_family_id(user_propagator::plugin::name()))
{}
theory_user_propagator::~theory_user_propagator() {
@ -173,16 +173,6 @@ void theory_user_propagator::propagate() {
m_qhead = qhead;
}
func_decl* theory_user_propagator::declare(symbol const& name, unsigned n, sort* const* domain, sort* range) {
if (!m_created_eh)
throw default_exception("event handler for dynamic expressions has to be registered before functions can be created");
// ensure that declaration plugin is registered with m.
if (!m.has_plugin(get_id()))
m.register_plugin(get_id(), alloc(user_propagator::plugin));
func_decl_info info(get_id(), user_propagator::plugin::kind_t::OP_USER_PROPAGATE);
return m.mk_func_decl(name, n, domain, range, info);
}
bool theory_user_propagator::internalize_atom(app* atom, bool gate_ctx) {
return internalize_term(atom);

7
src/smt/theory_user_propagator.h
View file

@ -56,7 +56,7 @@ namespace smt {
user_propagator::fixed_eh_t m_fixed_eh;
user_propagator::eq_eh_t m_eq_eh;
user_propagator::eq_eh_t m_diseq_eh;
user_propagator::register_created_eh_t m_created_eh;
user_propagator::created_eh_t m_created_eh;
user_propagator::context_obj* m_api_context = nullptr;
unsigned m_qhead = 0;
@ -96,8 +96,7 @@ namespace smt {
void register_fixed(user_propagator::fixed_eh_t& fixed_eh) { m_fixed_eh = fixed_eh; }
void register_eq(user_propagator::eq_eh_t& eq_eh) { m_eq_eh = eq_eh; }
void register_diseq(user_propagator::eq_eh_t& diseq_eh) { m_diseq_eh = diseq_eh; }
void register_created(user_propagator::register_created_eh_t& created_eh) { m_created_eh = created_eh; }
func_decl* declare(symbol const& name, unsigned n, sort* const* domain, sort* range);
void register_created(user_propagator::created_eh_t& created_eh) { m_created_eh = created_eh; }
bool has_fixed() const { return (bool)m_fixed_eh; }
@ -123,7 +122,7 @@ namespace smt {
void collect_statistics(::statistics & st) const override;
model_value_proc * mk_value(enode * n, model_generator & mg) override { return nullptr; }
void init_model(model_generator & m) override {}
bool include_func_interp(func_decl* f) override { return false; }
bool include_func_interp(func_decl* f) override { return true; }
bool can_propagate() override;
void propagate() override;
void display(std::ostream& out) const override {}

14
src/solver/assertions/asserted_formulas.cpp
View file

@ -71,12 +71,12 @@ asserted_formulas::asserted_formulas(ast_manager & m, smt_params & sp, params_re
void asserted_formulas::setup() {
switch (m_smt_params.m_lift_ite) {
case LI_FULL:
m_smt_params.m_ng_lift_ite = LI_NONE;
case lift_ite_kind::LI_FULL:
m_smt_params.m_ng_lift_ite = lift_ite_kind::LI_NONE;
break;
case LI_CONSERVATIVE:
if (m_smt_params.m_ng_lift_ite == LI_CONSERVATIVE)
m_smt_params.m_ng_lift_ite = LI_NONE;
case lift_ite_kind::LI_CONSERVATIVE:
if (m_smt_params.m_ng_lift_ite == lift_ite_kind::LI_CONSERVATIVE)
m_smt_params.m_ng_lift_ite = lift_ite_kind::LI_NONE;
break;
default:
break;
@ -281,8 +281,8 @@ void asserted_formulas::reduce() {
if (!invoke(m_reduce_asserted_formulas)) return;
if (!invoke(m_pull_nested_quantifiers)) return;
if (!invoke(m_lift_ite)) return;
m_lift_ite.m_functor.set_conservative(m_smt_params.m_lift_ite == LI_CONSERVATIVE);
m_ng_lift_ite.m_functor.set_conservative(m_smt_params.m_ng_lift_ite == LI_CONSERVATIVE);
m_lift_ite.m_functor.set_conservative(m_smt_params.m_lift_ite == lift_ite_kind::LI_CONSERVATIVE);
m_ng_lift_ite.m_functor.set_conservative(m_smt_params.m_ng_lift_ite == lift_ite_kind::LI_CONSERVATIVE);
if (!invoke(m_ng_lift_ite)) return;
if (!invoke(m_elim_term_ite)) return;
if (!invoke(m_refine_inj_axiom)) return;

6
src/solver/assertions/asserted_formulas.h
View file

@ -154,7 +154,7 @@ class asserted_formulas {
public:
elim_term_ite_fn(asserted_formulas& af): simplify_fmls(af, "elim-term-ite"), m_elim(af.m, af.m_defined_names) {}
void simplify(justified_expr const& j, expr_ref& n, proof_ref& p) override { m_elim(j.get_fml(), n, p); }
bool should_apply() const override { return af.m_smt_params.m_eliminate_term_ite && af.m_smt_params.m_lift_ite != LI_FULL; }
bool should_apply() const override { return af.m_smt_params.m_eliminate_term_ite && af.m_smt_params.m_lift_ite != lift_ite_kind::LI_FULL; }
void post_op() override { af.m_formulas.append(m_elim.new_defs()); af.reduce_and_solve(); m_elim.reset(); }
void push() { m_elim.push(); }
void pop(unsigned n) { m_elim.pop(n); }
@ -187,8 +187,8 @@ class asserted_formulas {
MK_SIMPLIFIERF(cheap_quant_fourier_motzkin, elim_bounds_rw, "cheap-fourier-motzkin", af.m_smt_params.m_eliminate_bounds && af.has_quantifiers(), true);
MK_SIMPLIFIERF(elim_bvs_from_quantifiers, bv_elim_rw, "eliminate-bit-vectors-from-quantifiers", af.m_smt_params.m_bb_quantifiers, true);
MK_SIMPLIFIERF(apply_bit2int, bit2int, "propagate-bit-vector-over-integers", af.m_smt_params.m_simplify_bit2int, true);
MK_SIMPLIFIERF(lift_ite, push_app_ite_rw, "lift-ite", af.m_smt_params.m_lift_ite != LI_NONE, true);
MK_SIMPLIFIERF(ng_lift_ite, ng_push_app_ite_rw, "lift-ite", af.m_smt_params.m_ng_lift_ite != LI_NONE, true);
MK_SIMPLIFIERF(lift_ite, push_app_ite_rw, "lift-ite", af.m_smt_params.m_lift_ite != lift_ite_kind::LI_NONE, true);
MK_SIMPLIFIERF(ng_lift_ite, ng_push_app_ite_rw, "lift-ite", af.m_smt_params.m_ng_lift_ite != lift_ite_kind::LI_NONE, true);
reduce_asserted_formulas_fn m_reduce_asserted_formulas;

4
src/solver/tactic2solver.cpp
View file

@ -108,8 +108,8 @@ public:
m_tactic->user_propagate_register_diseq(diseq_eh);
}
unsigned user_propagate_register(expr* e) override {
return m_tactic->user_propagate_register(e);
unsigned user_propagate_register_expr(expr* e) override {
return m_tactic->user_propagate_register_expr(e);
}
void user_propagate_clear() override {

2
src/tactic/core/elim_uncnstr_tactic.cpp
View file

@ -892,7 +892,7 @@ public:
m_num_elim_apps = 0;
}
unsigned user_propagate_register(expr* e) override {
unsigned user_propagate_register_expr(expr* e) override {
m_nonvars.insert(e);
return 0;
}

4
src/tactic/core/reduce_args_tactic.cpp
View file

@ -78,7 +78,7 @@ public:
void operator()(goal_ref const & g, goal_ref_buffer & result) override;
void cleanup() override;
unsigned user_propagate_register(expr* e) override;
unsigned user_propagate_register_expr(expr* e) override;
void user_propagate_clear() override;
};
@ -502,7 +502,7 @@ void reduce_args_tactic::cleanup() {
m_imp->m_vars.append(vars);
}
unsigned reduce_args_tactic::user_propagate_register(expr* e) {
unsigned reduce_args_tactic::user_propagate_register_expr(expr* e) {
m_imp->m_vars.push_back(e);
return 0;
}

2
src/tactic/tactic.h
View file

@ -85,7 +85,7 @@ public:
throw default_exception("tactic does not support user propagation");
}
unsigned user_propagate_register(expr* e) override { return 0; }
unsigned user_propagate_register_expr(expr* e) override { return 0; }
virtual char const* name() const = 0;
protected:

14
src/tactic/tactical.cpp
View file

@ -190,9 +190,9 @@ public:
m_t2->user_propagate_register_diseq(diseq_eh);
}
unsigned user_propagate_register(expr* e) override {
m_t1->user_propagate_register(e);
return m_t2->user_propagate_register(e);
unsigned user_propagate_register_expr(expr* e) override {
m_t1->user_propagate_register_expr(e);
return m_t2->user_propagate_register_expr(e);
}
void user_propagate_clear() override {
@ -200,14 +200,10 @@ public:
m_t2->user_propagate_clear();
}
void user_propagate_register_created(user_propagator::register_created_eh_t& created_eh) override {
void user_propagate_register_created(user_propagator::created_eh_t& created_eh) override {
m_t2->user_propagate_register_created(created_eh);
}
func_decl* user_propagate_declare(symbol const& name, unsigned n, sort* const* domain, sort* range) override {
return m_t2->user_propagate_declare(name, n, domain, range);
}
};
tactic * and_then(tactic * t1, tactic * t2) {
@ -833,7 +829,7 @@ public:
void reset() override { m_t->reset(); }
void set_logic(symbol const& l) override { m_t->set_logic(l); }
void set_progress_callback(progress_callback * callback) override { m_t->set_progress_callback(callback); }
unsigned user_propagate_register(expr* e) override { return m_t->user_propagate_register(e); }
unsigned user_propagate_register_expr(expr* e) override { return m_t->user_propagate_register_expr(e); }
void user_propagate_clear() override { m_t->user_propagate_clear(); }
protected:

20
src/tactic/user_propagator_base.h
View file

@ -23,12 +23,14 @@ namespace user_propagator {
typedef std::function<void*(void*, ast_manager&, context_obj*&)> fresh_eh_t;
typedef std::function<void(void*)> push_eh_t;
typedef std::function<void(void*,unsigned)> pop_eh_t;
typedef std::function<void(void*, callback*, expr*, unsigned)> register_created_eh_t;
typedef std::function<void(void*, callback*, expr*, unsigned)> created_eh_t;
class plugin : public decl_plugin {
public:
static symbol name() { return symbol("user_propagator"); }
enum kind_t { OP_USER_PROPAGATE };
virtual ~plugin() {}
@ -79,23 +81,11 @@ namespace user_propagator {
throw default_exception("user-propagators are only supported on the SMT solver");
}
virtual unsigned user_propagate_register(expr* e) {
virtual unsigned user_propagate_register_expr(expr* e) {
throw default_exception("user-propagators are only supported on the SMT solver");
}
/**
* Create uninterpreted function for the user propagator.
* When expressions using the function are assigned values, generate a callback
* into a register_declared_eh(user_ctx, solver_ctx, declared_expr, declare_id) with arguments
* 1. context and callback context
* 2. declared_expr: expression using function that was declared at top.
* 3. declared_id: a unique identifier (unique within the current scope) to track the expression.
*/
virtual func_decl* user_propagate_declare(symbol const& name, unsigned n, sort* const* domain, sort* range) {
throw default_exception("user-propagators are only supported on the SMT solver");
}
virtual void user_propagate_register_created(register_created_eh_t& r) {
virtual void user_propagate_register_created(created_eh_t& r) {
throw default_exception("user-propagators are only supported on the SMT solver");
}

26
src/util/state_graph.cpp
View file

@ -445,7 +445,7 @@ bool state_graph::write_dgml() {
}
r = m_state_ufind.next(r);
} while (r != s);
dgml << " Category=\"State\">" << std::endl;
dgml << " Category=\"State\" Group=\"Collapsed\">" << std::endl;
if (m_dead.contains(s))
dgml << "<Category Ref=\"Dead\"/>" << std::endl;
if (m_live.contains(s))
@ -453,18 +453,35 @@ bool state_graph::write_dgml() {
if (m_unexplored.contains(s))
dgml << "<Category Ref=\"Unexplored\"/>" << std::endl;
dgml << "</Node>" << std::endl;
dgml << "<Node Id=\"" << s << "info\" Label=\"";
r = s;
dgml << s << "=";
m_state_pp.pp_state_label(dgml, r);
do {
if (r != s) {
dgml << "&#13;" << r << "=";
m_state_pp.pp_state_label(dgml, r);
}
r = m_state_ufind.next(r);
} while (r != s);
dgml << "\"" << std::endl;
dgml << " Category=\"StateInfo\">" << std::endl;
dgml << "</Node>" << std::endl;
}
}
dgml << "</Nodes>" << std::endl;
dgml << "<Links>" << std::endl;
for (auto s : m_seen) {
if (m_state_ufind.is_root(s))
if (m_state_ufind.is_root(s)) {
for (auto t : m_targets[s]) {
dgml << "<Link Source=\"" << s << "\" Target=\"" << t << "\" Category=\"Transition\">" << std::endl;
if (!m_sources_maybecycle[t].contains(s))
dgml << "<Category Ref=\"Noncycle\"/>" << std::endl;
dgml << "</Link>" << std::endl;
}
dgml << "<Link Source=\"" << s << "\" Target=\"" << s << "info\" Category=\"Contains\">" << std::endl;
dgml << "</Link>" << std::endl;
}
}
dgml << "</Links>" << std::endl;
dgml << "<Categories>" << std::endl
@ -494,6 +511,11 @@ bool state_graph::write_dgml() {
<< "<Setter Property=\"Stroke\" Value=\"black\"/>" << std::endl
<< "<Setter Property=\"Background\" Value=\"white\"/>" << std::endl
<< "<Setter Property=\"MinWidth\" Value=\"0\"/>" << std::endl
<< "<Setter Property=\"FontSize\" Value=\"12\"/>" << std::endl
<< "</Style>" << std::endl
<< "<Style TargetType=\"Node\" GroupLabel=\"StateInfo\" ValueLabel=\"True\">" << std::endl
<< "<Setter Property=\"Stroke\" Value=\"white\"/>" << std::endl
<< "<Setter Property=\"FontSize\" Value=\"24\"/>" << std::endl
<< "</Style>" << std::endl
<< "<Style TargetType=\"Link\" GroupLabel=\"Transition\" ValueLabel=\"True\">" << std::endl
<< "<Condition Expression=\"HasCategory('Transition')\"/>" << std::endl

8
src/util/zstring.cpp
View file

@ -87,12 +87,12 @@ zstring::zstring(char const* s) {
string_encoding zstring::get_encoding() {
if (gparams::get_value("encoding") == "unicode")
return unicode;
return string_encoding::unicode;
if (gparams::get_value("encoding") == "bmp")
return bmp;
return string_encoding::bmp;
if (gparams::get_value("encoding") == "ascii")
return ascii;
return unicode;
return string_encoding::ascii;
return string_encoding::unicode;
}
bool zstring::well_formed() const {

14
src/util/zstring.h
View file

@ -21,7 +21,7 @@ Author:
#include "util/buffer.h"
#include "util/rational.h"
enum string_encoding {
enum class string_encoding {
ascii, // exactly 8 bits
unicode,
bmp // basic multilingual plane; exactly 16 bits
@ -41,22 +41,22 @@ public:
static unsigned ascii_num_bits() { return 8; }
static unsigned max_char() {
switch (get_encoding()) {
case unicode:
case string_encoding::unicode:
return unicode_max_char();
case bmp:
case string_encoding::bmp:
return bmp_max_char();
case ascii:
case string_encoding::ascii:
return ascii_max_char();
}
return unicode_max_char();
}
static unsigned num_bits() {
switch (get_encoding()) {
case unicode:
case string_encoding::unicode:
return unicode_num_bits();
case bmp:
case string_encoding::bmp:
return bmp_num_bits();
case ascii:
case string_encoding::ascii:
return ascii_num_bits();
}
return unicode_num_bits();