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

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

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2017-07-31 20:18:53 +01:00
parent 507356c7bf d130ae2e4f
commit bbf0ebcb74
12 changed files with 99 additions and 63 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/ast/ast.h
View file

@ -2021,8 +2021,8 @@ public:
app * mk_not(expr * n) { return mk_app(m_basic_family_id, OP_NOT, n); }
app * mk_distinct(unsigned num_args, expr * const * args);
app * mk_distinct_expanded(unsigned num_args, expr * const * args);
app * mk_true() { return m_true; }
app * mk_false() { return m_false; }
app * mk_true() const { return m_true; }
app * mk_false() const { return m_false; }
app * mk_bool_val(bool b) { return b?m_true:m_false; }
app * mk_interp(expr * arg) { return mk_app(m_basic_family_id, OP_INTERP, arg); }

4
src/ast/proof_checker/proof_checker.cpp
View file

@ -1299,7 +1299,7 @@ bool proof_checker::check_arith_literal(bool is_pos, app* lit0, rational const&
is_pos = !is_pos;
}
if (!a.is_le(lit) && !a.is_lt(lit) && !a.is_ge(lit) && !a.is_gt(lit) && !m.is_eq(lit)) {
IF_VERBOSE(0, verbose_stream() << mk_pp(lit, m) << "\n";);
IF_VERBOSE(2, verbose_stream() << "Not arith literal: " << mk_pp(lit, m) << "\n";);
return false;
}
SASSERT(lit->get_num_args() == 2);
@ -1363,7 +1363,7 @@ bool proof_checker::check_arith_literal(bool is_pos, app* lit0, rational const&
rw(sum);
}
IF_VERBOSE(0, verbose_stream() << coeff << "\n" << mk_pp(lit0, m) << "\n" << mk_pp(sum, m) << "\n";);
IF_VERBOSE(2, verbose_stream() << "coeff,lit,sum " << coeff << "\n" << mk_pp(lit0, m) << "\n" << mk_pp(sum, m) << "\n";);
#endif
return true;

80
src/ast/rewriter/quant_hoist.cpp
View file

@ -41,9 +41,9 @@ public:
m_rewriter(m)
{}
void operator()(expr* fml, app_ref_vector& vars, bool& is_fa, expr_ref& result) {
void operator()(expr* fml, app_ref_vector& vars, bool& is_fa, expr_ref& result, bool use_fresh, bool rewrite_ok) {
quantifier_type qt = Q_none_pos;
pull_quantifier(fml, qt, vars, result);
pull_quantifier(fml, qt, vars, result, use_fresh, rewrite_ok);
TRACE("qe_verbose",
tout << mk_pp(fml, m) << "\n";
tout << mk_pp(result, m) << "\n";);
@ -51,36 +51,38 @@ public:
is_fa = (Q_forall_pos == qt);
}
void pull_exists(expr* fml, app_ref_vector& vars, expr_ref& result) {
void pull_exists(expr* fml, app_ref_vector& vars, expr_ref& result, bool use_fresh, bool rewrite_ok) {
quantifier_type qt = Q_exists_pos;
pull_quantifier(fml, qt, vars, result);
pull_quantifier(fml, qt, vars, result, use_fresh, rewrite_ok);
TRACE("qe_verbose",
tout << mk_pp(fml, m) << "\n";
tout << mk_pp(result, m) << "\n";);
}
void pull_quantifier(bool is_forall, expr_ref& fml, app_ref_vector& vars) {
void pull_quantifier(bool is_forall, expr_ref& fml, app_ref_vector& vars, bool use_fresh, bool rewrite_ok) {
quantifier_type qt = is_forall?Q_forall_pos:Q_exists_pos;
expr_ref result(m);
pull_quantifier(fml, qt, vars, result);
pull_quantifier(fml, qt, vars, result, use_fresh, rewrite_ok);
TRACE("qe_verbose",
tout << mk_pp(fml, m) << "\n";
tout << mk_pp(result, m) << "\n";);
fml = result;
}
void extract_quantifier(quantifier* q, app_ref_vector& vars, expr_ref& result) {
void extract_quantifier(quantifier* q, app_ref_vector& vars, expr_ref& result, bool use_fresh) {
unsigned nd = q->get_num_decls();
for (unsigned i = 0; i < nd; ++i) {
sort* s = q->get_decl_sort(i);
app* a = m.mk_fresh_const(q->get_decl_name(i).str().c_str(), s);
symbol const& sym = q->get_decl_name (i);
app* a = use_fresh ? m.mk_fresh_const(sym.str ().c_str (), s)
: m.mk_const (sym, s);
vars.push_back(a);
}
expr * const * exprs = (expr* const*) (vars.c_ptr() + vars.size()- nd);
instantiate(m, q, exprs, result);
}
unsigned pull_quantifier(bool is_forall, expr_ref& fml, ptr_vector<sort>* sorts, svector<symbol>* names) {
unsigned pull_quantifier(bool is_forall, expr_ref& fml, ptr_vector<sort>* sorts, svector<symbol>* names, bool use_fresh, bool rewrite_ok) {
unsigned index = var_counter().get_next_var(fml);
while (is_quantifier(fml) && (is_forall == to_quantifier(fml)->is_forall())) {
quantifier* q = to_quantifier(fml);
@ -97,7 +99,7 @@ public:
return index;
}
app_ref_vector vars(m);
pull_quantifier(is_forall, fml, vars);
pull_quantifier(is_forall, fml, vars, use_fresh, rewrite_ok);
if (vars.empty()) {
return index;
}
@ -192,7 +194,7 @@ private:
}
void pull_quantifier(expr* fml, quantifier_type& qt, app_ref_vector& vars, expr_ref& result) {
void pull_quantifier(expr* fml, quantifier_type& qt, app_ref_vector& vars, expr_ref& result, bool use_fresh, bool rewrite_ok) {
if (!has_quantifiers(fml)) {
result = fml;
@ -209,38 +211,48 @@ private:
if (m.is_and(fml)) {
num_args = a->get_num_args();
for (unsigned i = 0; i < num_args; ++i) {
pull_quantifier(a->get_arg(i), qt, vars, tmp);
pull_quantifier(a->get_arg(i), qt, vars, tmp, use_fresh, rewrite_ok);
args.push_back(tmp);
}
if (rewrite_ok) {
m_rewriter.mk_and(args.size(), args.c_ptr(), result);
}
else {
result = m.mk_and (args.size (), args.c_ptr ());
}
}
else if (m.is_or(fml)) {
num_args = to_app(fml)->get_num_args();
for (unsigned i = 0; i < num_args; ++i) {
pull_quantifier(to_app(fml)->get_arg(i), qt, vars, tmp);
pull_quantifier(to_app(fml)->get_arg(i), qt, vars, tmp, use_fresh, rewrite_ok);
args.push_back(tmp);
}
if (rewrite_ok) {
m_rewriter.mk_or(args.size(), args.c_ptr(), result);
}
else {
result = m.mk_or (args.size (), args.c_ptr ());
}
}
else if (m.is_not(fml)) {
pull_quantifier(to_app(fml)->get_arg(0), negate(qt), vars, tmp);
pull_quantifier(to_app(fml)->get_arg(0), negate(qt), vars, tmp, use_fresh, rewrite_ok);
negate(qt);
result = m.mk_not(tmp);
}
else if (m.is_implies(fml, t1, t2)) {
pull_quantifier(t1, negate(qt), vars, tmp);
pull_quantifier(t1, negate(qt), vars, tmp, use_fresh, rewrite_ok);
negate(qt);
pull_quantifier(t2, qt, vars, result);
pull_quantifier(t2, qt, vars, result, use_fresh, rewrite_ok);
result = m.mk_implies(tmp, result);
}
else if (m.is_ite(fml, t1, t2, t3)) {
expr_ref tt1(m), tt2(m), tt3(m), ntt1(m), nt1(m);
pull_quantifier(t2, qt, vars, tt2);
pull_quantifier(t3, qt, vars, tt3);
pull_quantifier(t2, qt, vars, tt2, use_fresh, rewrite_ok);
pull_quantifier(t3, qt, vars, tt3, use_fresh, rewrite_ok);
if (has_quantifiers(t1)) {
pull_quantifier(t1, qt, vars, tt1);
pull_quantifier(t1, qt, vars, tt1, use_fresh, rewrite_ok);
nt1 = m.mk_not(t1);
pull_quantifier(nt1, qt, vars, ntt1);
pull_quantifier(nt1, qt, vars, ntt1, use_fresh, rewrite_ok);
result = m.mk_and(m.mk_or(ntt1, tt2), m.mk_or(tt1, tt3));
}
else {
@ -249,12 +261,12 @@ private:
}
else if ((m.is_eq(fml, t1, t2) && m.is_bool(t1)) || m.is_iff(fml, t1, t2)) {
expr_ref tt1(m), tt2(m), ntt1(m), ntt2(m), nt1(m), nt2(m);
pull_quantifier(t1, qt, vars, tt1);
pull_quantifier(t2, qt, vars, tt2);
pull_quantifier(t1, qt, vars, tt1, use_fresh, rewrite_ok);
pull_quantifier(t2, qt, vars, tt2, use_fresh, rewrite_ok);
nt1 = m.mk_not(t1);
nt2 = m.mk_not(t2);
pull_quantifier(nt1, qt, vars, ntt1);
pull_quantifier(nt2, qt, vars, ntt2);
pull_quantifier(nt1, qt, vars, ntt1, use_fresh, rewrite_ok);
pull_quantifier(nt2, qt, vars, ntt2, use_fresh, rewrite_ok);
result = m.mk_and(m.mk_or(ntt1, tt2), m.mk_or(ntt2, tt1));
}
else {
@ -271,8 +283,8 @@ private:
break;
}
set_quantifier_type(qt, q->is_forall());
extract_quantifier(q, vars, tmp);
pull_quantifier(tmp, qt, vars, result);
extract_quantifier(q, vars, tmp, use_fresh);
pull_quantifier(tmp, qt, vars, result, use_fresh, rewrite_ok);
break;
}
case AST_VAR:
@ -295,18 +307,18 @@ quantifier_hoister::~quantifier_hoister() {
dealloc(m_impl);
}
void quantifier_hoister::operator()(expr* fml, app_ref_vector& vars, bool& is_fa, expr_ref& result) {
(*m_impl)(fml, vars, is_fa, result);
void quantifier_hoister::operator()(expr* fml, app_ref_vector& vars, bool& is_fa, expr_ref& result, bool use_fresh, bool rewrite_ok) {
(*m_impl)(fml, vars, is_fa, result, use_fresh, rewrite_ok);
}
void quantifier_hoister::pull_exists(expr* fml, app_ref_vector& vars, expr_ref& result) {
m_impl->pull_exists(fml, vars, result);
void quantifier_hoister::pull_exists(expr* fml, app_ref_vector& vars, expr_ref& result, bool use_fresh, bool rewrite_ok) {
m_impl->pull_exists(fml, vars, result, use_fresh, rewrite_ok);
}
void quantifier_hoister::pull_quantifier(bool is_forall, expr_ref& fml, app_ref_vector& vars) {
m_impl->pull_quantifier(is_forall, fml, vars);
void quantifier_hoister::pull_quantifier(bool is_forall, expr_ref& fml, app_ref_vector& vars, bool use_fresh, bool rewrite_ok) {
m_impl->pull_quantifier(is_forall, fml, vars, use_fresh, rewrite_ok);
}
unsigned quantifier_hoister::pull_quantifier(bool is_forall, expr_ref& fml, ptr_vector<sort>* sorts, svector<symbol>* names) {
return m_impl->pull_quantifier(is_forall, fml, sorts, names);
unsigned quantifier_hoister::pull_quantifier(bool is_forall, expr_ref& fml, ptr_vector<sort>* sorts, svector<symbol>* names, bool use_fresh, bool rewrite_ok) {
return m_impl->pull_quantifier(is_forall, fml, sorts, names, use_fresh, rewrite_ok);
}

8
src/ast/rewriter/quant_hoist.h
View file

@ -43,14 +43,14 @@ public:
or, and, implies, ite (then and else branch only).
*/
void operator()(expr* fml, app_ref_vector& vars, bool& is_fa, expr_ref& result);
void operator()(expr* fml, app_ref_vector& vars, bool& is_fa, expr_ref& result, bool use_fresh = true, bool rewrite_ok = true);
/**
\brief Pull top-most existential quantifier up.
The list of variables is empty if there are no top-level existential quantifier.
*/
void pull_exists(expr* fml, app_ref_vector& vars, expr_ref& result);
void pull_exists(expr* fml, app_ref_vector& vars, expr_ref& result, bool use_fresh = true, bool rewrite_ok = true);
/**
@ -58,7 +58,7 @@ public:
The list of variables is empty if there are no top-level universal/existential quantifier.
*/
void pull_quantifier(bool is_forall, expr_ref& fml, app_ref_vector& vars);
void pull_quantifier(bool is_forall, expr_ref& fml, app_ref_vector& vars, bool use_fresh = true, bool rewrite_ok = true);
/**
\brief Pull top-most universal (is_forall true) or existential (is_forall=false) quantifier up.
@ -66,7 +66,7 @@ public:
Return index of maximal variable.
*/
unsigned pull_quantifier(bool is_forall, expr_ref& fml, ptr_vector<sort>* sorts, svector<symbol>* names);
unsigned pull_quantifier(bool is_forall, expr_ref& fml, ptr_vector<sort>* sorts, svector<symbol>* names, bool use_fresh = true, bool rewrite_ok = true);
};

2
src/cmd_context/eval_cmd.cpp
View file

@ -58,6 +58,8 @@ public:
virtual void execute(cmd_context & ctx) {
if (!ctx.is_model_available())
throw cmd_exception("model is not available");
if (!m_target)
throw cmd_exception("no arguments passed to eval");
model_ref md;
unsigned index = m_params.get_uint("model_index", 0);
check_sat_result * last_result = ctx.get_check_sat_result();

15
src/qe/qe_lite.cpp
View file

@ -2342,6 +2342,7 @@ private:
elim_star m_elim_star;
th_rewriter m_rewriter;
bool m_use_array_der;
bool has_unique_non_ground(expr_ref_vector const& fmls, unsigned& index) {
index = fmls.size();
if (index <= 1) {
@ -2359,13 +2360,14 @@ private:
}
public:
impl(ast_manager & m, params_ref const & p):
impl(ast_manager & m, params_ref const & p, bool use_array_der):
m(m),
m_der(m, p),
m_fm(m),
m_array_der(m),
m_elim_star(*this),
m_rewriter(m) {}
m_rewriter(m),
m_use_array_der(use_array_der) {}
void operator()(app_ref_vector& vars, expr_ref& fml) {
if (vars.empty()) {
@ -2445,14 +2447,15 @@ public:
m_array_der.set_is_variable_proc(is_var);
m_der(fmls);
m_fm(fmls);
m_array_der(fmls);
// AG: disalble m_array_der() since it interferes with other array handling
if (m_use_array_der) m_array_der(fmls);
TRACE("qe_lite", for (unsigned i = 0; i < fmls.size(); ++i) tout << mk_pp(fmls[i].get(), m) << "\n";);
}
};
qe_lite::qe_lite(ast_manager & m, params_ref const & p) {
m_impl = alloc(impl, m, p);
qe_lite::qe_lite(ast_manager & m, params_ref const & p, bool use_array_der) {
m_impl = alloc(impl, m, p, use_array_der);
}
qe_lite::~qe_lite() {
@ -2484,7 +2487,7 @@ class qe_lite_tactic : public tactic {
imp(ast_manager& m, params_ref const & p):
m(m),
m_qe(m, p)
m_qe(m, p, true)
{}
void checkpoint() {

5
src/qe/qe_lite.h
View file

@ -31,7 +31,10 @@ class qe_lite {
class impl;
impl * m_impl;
public:
qe_lite(ast_manager & m, params_ref const & p);
/**
use_array_der controls whether equalities over array reads are simplified
*/
qe_lite(ast_manager& m, params_ref const & p, bool use_array_der = true);
~qe_lite();

11
src/smt/smt_context.cpp
View file

@ -2406,7 +2406,7 @@ namespace smt {
if (m_manager.has_trace_stream())
m_manager.trace_stream() << "[pop] " << num_scopes << " " << m_scope_lvl << "\n";
TRACE("context", tout << "backtracking: " << num_scopes << "\n";);
TRACE("context", tout << "backtracking: " << num_scopes << " from " << m_scope_lvl << "\n";);
TRACE("pop_scope_detail", display(tout););
SASSERT(num_scopes > 0);
SASSERT(num_scopes <= m_scope_lvl);
@ -2901,10 +2901,10 @@ namespace smt {
}
push_scope();
m_base_scopes.push_back(base_scope());
base_scope & bs = m_base_scopes.back();
bs.m_lemmas_lim = m_lemmas.size();
bs.m_inconsistent = inconsistent();
bs.m_simp_qhead_lim = m_simp_qhead;
base_scope & bs = m_base_scopes.back();
bs.m_lemmas_lim = m_lemmas.size();
bs.m_inconsistent = inconsistent();
bs.m_simp_qhead_lim = m_simp_qhead;
m_base_lvl++;
m_search_lvl++; // Not really necessary. But, it is useful to enforce the invariant m_search_lvl >= m_base_lvl
SASSERT(m_base_lvl <= m_scope_lvl);
@ -2912,6 +2912,7 @@ namespace smt {
void context::pop(unsigned num_scopes) {
SASSERT (num_scopes > 0);
if (num_scopes > m_scope_lvl) return;
pop_to_base_lvl();
pop_scope(num_scopes);
}

1
src/smt/smt_justification.h
View file

@ -181,6 +181,7 @@ namespace smt {
enode * m_node2;
public:
eq_propagation_justification(enode * n1, enode * n2):m_node1(n1), m_node2(n2) {
SASSERT(n1 != n2);
}
virtual void get_antecedents(conflict_resolution & cr);

15
src/smt/smt_model_finder.cpp
View file

@ -760,7 +760,7 @@ namespace smt {
ptr_vector<expr> const & exceptions = n->get_exceptions();
ptr_vector<node> const & avoid_set = n->get_avoid_set();
obj_map<expr, unsigned> const & elems = s->get_elems();
SASSERT(!elems.empty());
if (elems.empty()) return;
if (!exceptions.empty() || !avoid_set.empty()) {
ptr_buffer<expr> ex_vals;
collect_exceptions_values(n, ex_vals);
@ -927,15 +927,14 @@ namespace smt {
ptr_buffer<expr> values;
get_instantiation_set_values(n, values);
sort * s = n->get_sort();
expr * else_val = eval(n->get_else(), true);
func_decl * p = m_manager.mk_fresh_func_decl(1, &s, s);
func_decl * p = m_manager.mk_fresh_func_decl(1, &s, s);
func_interp * pi = alloc(func_interp, m_manager, 1);
pi->set_else(else_val);
m_model->register_aux_decl(p, pi);
ptr_buffer<expr>::const_iterator it = values.begin();
ptr_buffer<expr>::const_iterator end = values.end();
for (; it != end; ++it) {
expr * v = *it;
if (n->get_else()) {
expr * else_val = eval(n->get_else(), true);
pi->set_else(else_val);
}
for (expr * v : values) {
pi->insert_new_entry(&v, v);
}
n->set_proj(p);

3
src/smt/theory_seq.cpp
View file

@ -1681,6 +1681,7 @@ bool theory_seq::solve_binary_eq(expr_ref_vector const& ls, expr_ref_vector cons
bool has_conflict = false;
for (unsigned j = 0; !has_conflict && j < sz; ++j) {
unsigned j1 = (offset + j) % sz;
if (xs[j] == ys[j1]) continue;
literal eq = mk_eq(xs[j], ys[j1], false);
switch (ctx.get_assignment(eq)) {
case l_false:
@ -1891,7 +1892,7 @@ bool theory_seq::solve_ne(unsigned idx) {
new_ls.push_back(ls);
new_rs.push_back(rs);
}
else {
else if (nl != nr) {
literal lit(mk_eq(nl, nr, false));
ctx.mark_as_relevant(lit);
new_lits.push_back(lit);

14
src/util/ref.h
View file

@ -50,6 +50,7 @@ public:
inc_ref();
}
ref (ref && r): m_ptr (r.detach ()) {}
~ref() {
dec_ref();
}
@ -89,6 +90,14 @@ public:
return *this;
}
ref & operator=(ref &&r) {
if (this != &r) {
dec_ref ();
m_ptr = r.detach ();
}
return *this;
}
void reset() {
dec_ref();
m_ptr = 0;
@ -107,6 +116,11 @@ public:
friend bool operator!=(const ref & r1, const ref & r2) {
return r1.m_ptr != r2.m_ptr;
}
friend void swap (ref &r1, ref &r2) {
T* tmp = r1.m_ptr;
r1.m_ptr = r2.m_ptr;
r2.m_ptr = tmp;
}
};
/**