mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
Merge branch 'master' of https://github.com/Z3Prover/z3 into HEAD
This commit is contained in:
commit
1c630ccc9a
|
@ -153,6 +153,11 @@ extern "C" {
|
|||
LOG_Z3_solver_set_params(c, s, p);
|
||||
RESET_ERROR_CODE();
|
||||
|
||||
symbol logic = to_param_ref(p).get_sym("smt.logic", symbol::null);
|
||||
if (logic != symbol::null) {
|
||||
to_solver(s)->m_logic = logic;
|
||||
}
|
||||
|
||||
if (to_solver(s)->m_solver) {
|
||||
bool old_model = to_solver(s)->m_params.get_bool("model", true);
|
||||
bool new_model = to_param_ref(p).get_bool("model", true);
|
||||
|
|
|
@ -3,6 +3,7 @@ def_module_params(module_name='smt',
|
|||
description='smt solver based on lazy smt',
|
||||
export=True,
|
||||
params=(('auto_config', BOOL, True, 'automatically configure solver'),
|
||||
('logic', SYMBOL, '', 'logic used to setup the SMT solver'),
|
||||
('random_seed', UINT, 0, 'random seed for the smt solver'),
|
||||
('relevancy', UINT, 2, 'relevancy propagation heuristic: 0 - disabled, 1 - relevancy is tracked by only affects quantifier instantiation, 2 - relevancy is tracked, and an atom is only asserted if it is relevant'),
|
||||
('macro_finder', BOOL, False, 'try to find universally quantified formulas that can be viewed as macros'),
|
||||
|
|
|
@ -34,7 +34,7 @@ struct interval {
|
|||
unsigned sz;
|
||||
bool tight;
|
||||
|
||||
explicit interval() : l(0), h(0), sz(0), tight(false) {}
|
||||
interval() {}
|
||||
interval(const rational& l, const rational& h, unsigned sz, bool tight = false) : l(l), h(h), sz(sz), tight(tight) {
|
||||
// canonicalize full set
|
||||
if (is_wrapped() && l == h + rational::one()) {
|
||||
|
@ -51,10 +51,11 @@ struct interval {
|
|||
|
||||
bool is_full() const { return l.is_zero() && h == uMaxInt(sz); }
|
||||
bool is_wrapped() const { return l > h; }
|
||||
bool is_singleton() const { return l == h; }
|
||||
|
||||
bool operator==(const interval& b) const {
|
||||
SASSERT(sz == b.sz);
|
||||
return l == b.l && h == b.h;
|
||||
return l == b.l && h == b.h && tight == b.tight;
|
||||
}
|
||||
bool operator!=(const interval& b) const { return !(*this == b); }
|
||||
|
||||
|
@ -79,7 +80,7 @@ struct interval {
|
|||
|
||||
/// return false if intersection is unsat
|
||||
bool intersect(const interval& b, interval& result) const {
|
||||
if (is_full() || (l == b.l && h == b.h)) {
|
||||
if (is_full() || *this == b) {
|
||||
result = b;
|
||||
return true;
|
||||
}
|
||||
|
@ -153,6 +154,8 @@ std::ostream& operator<<(std::ostream& o, const interval& I) {
|
|||
|
||||
class bv_bounds_simplifier : public ctx_simplify_tactic::simplifier {
|
||||
typedef obj_map<expr, interval> map;
|
||||
typedef obj_map<expr, bool> expr_set;
|
||||
typedef obj_map<expr, expr_set*> expr_list_map;
|
||||
|
||||
ast_manager& m;
|
||||
params_ref m_params;
|
||||
|
@ -160,6 +163,7 @@ class bv_bounds_simplifier : public ctx_simplify_tactic::simplifier {
|
|||
bv_util m_bv;
|
||||
vector<map> m_scopes;
|
||||
map *m_bound;
|
||||
expr_list_map m_expr_vars;
|
||||
|
||||
bool is_bound(expr *e, expr*& v, interval& b) {
|
||||
rational n;
|
||||
|
@ -209,6 +213,43 @@ class bv_bounds_simplifier : public ctx_simplify_tactic::simplifier {
|
|||
return false;
|
||||
}
|
||||
|
||||
expr_set* get_expr_vars(expr* t) {
|
||||
expr_set*& entry = m_expr_vars.insert_if_not_there2(t, 0)->get_data().m_value;
|
||||
if (entry)
|
||||
return entry;
|
||||
|
||||
expr_set* set = alloc(expr_set);
|
||||
entry = set;
|
||||
|
||||
if (!m_bv.is_numeral(t))
|
||||
set->insert(t, true);
|
||||
|
||||
if (!is_app(t))
|
||||
return set;
|
||||
|
||||
app* a = to_app(t);
|
||||
for (unsigned i = 0; i < a->get_num_args(); ++i) {
|
||||
expr_set* set_arg = get_expr_vars(a->get_arg(i));
|
||||
for (expr_set::iterator I = set_arg->begin(), E = set_arg->end(); I != E; ++I) {
|
||||
set->insert(I->m_key, true);
|
||||
}
|
||||
}
|
||||
return set;
|
||||
}
|
||||
|
||||
bool expr_has_bounds(expr* t) {
|
||||
app* a = to_app(t);
|
||||
if ((m_bv.is_bv_ule(t) || m_bv.is_bv_sle(t) || m.is_eq(t)) &&
|
||||
(m_bv.is_numeral(a->get_arg(0)) || m_bv.is_numeral(a->get_arg(1))))
|
||||
return true;
|
||||
|
||||
for (unsigned i = 0; i < a->get_num_args(); ++i) {
|
||||
if (expr_has_bounds(a->get_arg(i)))
|
||||
return true;
|
||||
}
|
||||
return false;
|
||||
}
|
||||
|
||||
public:
|
||||
|
||||
bv_bounds_simplifier(ast_manager& m, params_ref const& p) : m(m), m_params(p), m_bv(m) {
|
||||
|
@ -226,7 +267,11 @@ public:
|
|||
r.insert("propagate-eq", CPK_BOOL, "(default: false) propagate equalities from inequalities");
|
||||
}
|
||||
|
||||
virtual ~bv_bounds_simplifier() {}
|
||||
virtual ~bv_bounds_simplifier() {
|
||||
for (expr_list_map::iterator I = m_expr_vars.begin(), E = m_expr_vars.end(); I != E; ++I) {
|
||||
dealloc(I->m_value);
|
||||
}
|
||||
}
|
||||
|
||||
virtual bool assert_expr(expr * t, bool sign) {
|
||||
while (m.is_not(t, t)) {
|
||||
|
@ -250,10 +295,17 @@ public:
|
|||
|
||||
virtual bool simplify(expr* t, expr_ref& result) {
|
||||
expr* t1;
|
||||
interval b, ctx, intr;
|
||||
result = 0;
|
||||
bool sign = false;
|
||||
interval b;
|
||||
|
||||
if (m_bound->find(t, b) && b.is_singleton()) {
|
||||
result = m_bv.mk_numeral(b.l, m_bv.get_bv_size(t));
|
||||
return true;
|
||||
}
|
||||
|
||||
if (!m.is_bool(t))
|
||||
return false;
|
||||
|
||||
bool sign = false;
|
||||
while (m.is_not(t, t)) {
|
||||
sign = !sign;
|
||||
}
|
||||
|
@ -269,12 +321,15 @@ public:
|
|||
}
|
||||
}
|
||||
|
||||
interval ctx, intr;
|
||||
result = 0;
|
||||
|
||||
if (m_bound->find(t1, ctx)) {
|
||||
if (ctx.implies(b)) {
|
||||
result = m.mk_true();
|
||||
} else if (!b.intersect(ctx, intr)) {
|
||||
result = m.mk_false();
|
||||
} else if (m_propagate_eq && intr.l == intr.h) {
|
||||
} else if (m_propagate_eq && intr.is_singleton()) {
|
||||
result = m.mk_eq(t1, m_bv.mk_numeral(intr.l, m.get_sort(t1)));
|
||||
}
|
||||
} else if (b.is_full() && b.tight) {
|
||||
|
@ -287,6 +342,27 @@ public:
|
|||
return result != 0;
|
||||
}
|
||||
|
||||
virtual bool may_simplify(expr* t) {
|
||||
if (m_bv.is_numeral(t))
|
||||
return false;
|
||||
|
||||
expr_set* used_exprs = get_expr_vars(t);
|
||||
for (map::iterator I = m_bound->begin(), E = m_bound->end(); I != E; ++I) {
|
||||
if (I->m_value.is_singleton() && used_exprs->contains(I->m_key))
|
||||
return true;
|
||||
}
|
||||
|
||||
while (m.is_not(t, t));
|
||||
|
||||
expr* t1;
|
||||
interval b;
|
||||
// skip common case: single bound constraint without any context for simplification
|
||||
if (is_bound(t, t1, b)) {
|
||||
return m_bound->contains(t1);
|
||||
}
|
||||
return expr_has_bounds(t);
|
||||
}
|
||||
|
||||
virtual void push() {
|
||||
TRACE("bv", tout << "push\n";);
|
||||
unsigned sz = m_scopes.size();
|
||||
|
|
|
@ -331,17 +331,13 @@ struct ctx_simplify_tactic::imp {
|
|||
|
||||
void simplify(expr * t, expr_ref & r) {
|
||||
r = 0;
|
||||
if (m_depth >= m_max_depth || m_num_steps >= m_max_steps || !is_app(t)) {
|
||||
if (m_depth >= m_max_depth || m_num_steps >= m_max_steps || !is_app(t) || !m_simp->may_simplify(t)) {
|
||||
r = t;
|
||||
return;
|
||||
}
|
||||
checkpoint();
|
||||
TRACE("ctx_simplify_tactic_detail", tout << "processing: " << mk_bounded_pp(t, m) << "\n";);
|
||||
if (m_simp->simplify(t, r)) {
|
||||
SASSERT(r.get() != 0);
|
||||
return;
|
||||
}
|
||||
if (is_cached(t, r)) {
|
||||
if (is_cached(t, r) || m_simp->simplify(t, r)) {
|
||||
SASSERT(r.get() != 0);
|
||||
return;
|
||||
}
|
||||
|
|
|
@ -30,6 +30,7 @@ public:
|
|||
virtual ~simplifier() {}
|
||||
virtual bool assert_expr(expr * t, bool sign) = 0;
|
||||
virtual bool simplify(expr* t, expr_ref& result) = 0;
|
||||
virtual bool may_simplify(expr* t) { return true; }
|
||||
virtual void push() = 0;
|
||||
virtual void pop(unsigned num_scopes) = 0;
|
||||
virtual simplifier * translate(ast_manager & m) = 0;
|
||||
|
|
Loading…
Reference in a new issue