mirror of
https://github.com/Z3Prover/z3
synced 2025-07-23 12:48:53 +00:00
updates to mbqi
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
e8cabdc620
commit
402234757e
2 changed files with 114 additions and 114 deletions
|
@ -497,14 +497,14 @@ namespace spacer {
|
||||||
expr_ref bval (m);
|
expr_ref bval (m);
|
||||||
|
|
||||||
while (true) {
|
while (true) {
|
||||||
params_ref p;
|
params_ref p;
|
||||||
qe_lite qe(m, p, false);
|
qe_lite qe(m, p, false);
|
||||||
qe (vars, fml);
|
qe (vars, fml);
|
||||||
rw (fml);
|
rw (fml);
|
||||||
|
|
||||||
TRACE ("spacer_mbp",
|
TRACE ("spacer_mbp",
|
||||||
tout << "After qe_lite:\n";
|
tout << "After qe_lite:\n";
|
||||||
tout << mk_pp (fml, m) << "\n";
|
tout << mk_pp (fml, m) << "\n";
|
||||||
tout << "Vars:\n" << vars;);
|
tout << "Vars:\n" << vars;);
|
||||||
|
|
||||||
SASSERT (!m.is_false (fml));
|
SASSERT (!m.is_false (fml));
|
||||||
|
@ -572,21 +572,21 @@ namespace spacer {
|
||||||
// tout << "After second qelite: " <<
|
// tout << "After second qelite: " <<
|
||||||
// mk_pp (fml, m) << "\n";);
|
// mk_pp (fml, m) << "\n";);
|
||||||
|
|
||||||
if (use_native_mbp) {
|
if (use_native_mbp) {
|
||||||
qe::mbp mbp (m);
|
qe::mbp mbp (m);
|
||||||
expr_ref_vector fmls(m);
|
expr_ref_vector fmls(m);
|
||||||
flatten_and (fml, fmls);
|
flatten_and (fml, fmls);
|
||||||
|
|
||||||
mbp (true, arith_vars, *M.get (), fmls);
|
mbp (true, arith_vars, *M.get (), fmls);
|
||||||
fml = mk_and (fmls);
|
fml = mk_and (fmls);
|
||||||
SASSERT (arith_vars.empty ());
|
SASSERT (arith_vars.empty ());
|
||||||
} else {
|
} else {
|
||||||
scoped_no_proof _sp (m);
|
scoped_no_proof _sp (m);
|
||||||
spacer_qe::arith_project (*M.get (), arith_vars, fml);
|
spacer_qe::arith_project (*M.get (), arith_vars, fml);
|
||||||
}
|
}
|
||||||
|
|
||||||
TRACE ("spacer_mbp",
|
TRACE ("spacer_mbp",
|
||||||
tout << "Projected arith vars:\n" << mk_pp (fml, m) << "\n";
|
tout << "Projected arith vars:\n" << mk_pp (fml, m) << "\n";
|
||||||
tout << "Remaining arith vars:\n" << arith_vars << "\n";);
|
tout << "Remaining arith vars:\n" << arith_vars << "\n";);
|
||||||
SASSERT (!m.is_false (fml));
|
SASSERT (!m.is_false (fml));
|
||||||
}
|
}
|
||||||
|
@ -697,7 +697,7 @@ void expand_literals(ast_manager &m, expr_ref_vector& conjs)
|
||||||
}
|
}
|
||||||
|
|
||||||
namespace {
|
namespace {
|
||||||
class implicant_picker {
|
class implicant_picker {
|
||||||
model_evaluator_util &m_mev;
|
model_evaluator_util &m_mev;
|
||||||
ast_manager &m;
|
ast_manager &m;
|
||||||
arith_util m_arith;
|
arith_util m_arith;
|
||||||
|
@ -747,37 +747,37 @@ namespace {
|
||||||
out.push_back (res);
|
out.push_back (res);
|
||||||
}
|
}
|
||||||
|
|
||||||
void process_app(app *a, expr_ref_vector &out)
|
void process_app(app *a, expr_ref_vector &out)
|
||||||
{
|
{
|
||||||
if (m_visited.is_marked(a)) { return; }
|
if (m_visited.is_marked(a)) { return; }
|
||||||
SASSERT (m.is_bool (a));
|
SASSERT (m.is_bool (a));
|
||||||
expr_ref v(m);
|
expr_ref v(m);
|
||||||
m_mev.eval (a, v, false);
|
m_mev.eval (a, v, false);
|
||||||
|
|
||||||
if (!m.is_true(v) && !m.is_false(v)) { return; }
|
if (!m.is_true(v) && !m.is_false(v)) { return; }
|
||||||
|
|
||||||
expr *na, *f1, *f2, *f3;
|
expr *na, *f1, *f2, *f3;
|
||||||
|
|
||||||
if (a->get_family_id() != m.get_basic_family_id())
|
if (a->get_family_id() != m.get_basic_family_id())
|
||||||
{ add_literal(a, out); }
|
{ add_literal(a, out); }
|
||||||
else if (is_uninterp_const(a))
|
else if (is_uninterp_const(a))
|
||||||
{ add_literal(a, out); }
|
{ add_literal(a, out); }
|
||||||
else if (m.is_not(a, na) && m.is_not(na, na))
|
else if (m.is_not(a, na) && m.is_not(na, na))
|
||||||
{ m_todo.push_back(na); }
|
{ m_todo.push_back(na); }
|
||||||
else if (m.is_not(a, na))
|
else if (m.is_not(a, na))
|
||||||
{ m_todo.push_back(na); }
|
{ m_todo.push_back(na); }
|
||||||
else if (m.is_distinct(a)) {
|
else if (m.is_distinct(a)) {
|
||||||
if (m.is_false(v))
|
if (m.is_false(v))
|
||||||
m_todo.push_back
|
m_todo.push_back
|
||||||
(qe::project_plugin::pick_equality(m, *m_mev.get_model(), a));
|
(qe::project_plugin::pick_equality(m, *m_mev.get_model(), a));
|
||||||
else if (a->get_num_args() == 2)
|
else if (a->get_num_args() == 2)
|
||||||
{ add_literal(a, out); }
|
{ add_literal(a, out); }
|
||||||
else
|
else
|
||||||
m_todo.push_back(m.mk_distinct_expanded(a->get_num_args(),
|
m_todo.push_back(m.mk_distinct_expanded(a->get_num_args(),
|
||||||
a->get_args()));
|
a->get_args()));
|
||||||
} else if (m.is_and(a)) {
|
} else if (m.is_and(a)) {
|
||||||
if (m.is_true(v))
|
if (m.is_true(v))
|
||||||
{ m_todo.append(a->get_num_args(), a->get_args()); }
|
{ m_todo.append(a->get_num_args(), a->get_args()); }
|
||||||
else if (m.is_false(v)) {
|
else if (m.is_false(v)) {
|
||||||
for (unsigned i = 0, sz = a->get_num_args (); i < sz; ++i) {
|
for (unsigned i = 0, sz = a->get_num_args (); i < sz; ++i) {
|
||||||
if (m_mev.is_false(a->get_arg(i))) {
|
if (m_mev.is_false(a->get_arg(i))) {
|
||||||
|
@ -786,9 +786,9 @@ namespace {
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
} else if (m.is_or(a)) {
|
} else if (m.is_or(a)) {
|
||||||
if (m.is_false(v))
|
if (m.is_false(v))
|
||||||
{ m_todo.append(a->get_num_args(), a->get_args()); }
|
{ m_todo.append(a->get_num_args(), a->get_args()); }
|
||||||
else if (m.is_true(v)) {
|
else if (m.is_true(v)) {
|
||||||
for (unsigned i = 0, sz = a->get_num_args(); i < sz; ++i) {
|
for (unsigned i = 0, sz = a->get_num_args(); i < sz; ++i) {
|
||||||
if (m_mev.is_true(a->get_arg(i))) {
|
if (m_mev.is_true(a->get_arg(i))) {
|
||||||
|
@ -797,39 +797,39 @@ namespace {
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
} else if (m.is_iff(a, f1, f2) || m.is_eq(a, f1, f2) ||
|
} else if (m.is_iff(a, f1, f2) || m.is_eq(a, f1, f2) ||
|
||||||
(m.is_true(v) && m.is_not(a, na) && m.is_xor (na, f1, f2))) {
|
(m.is_true(v) && m.is_not(a, na) && m.is_xor (na, f1, f2))) {
|
||||||
if (!m.are_equal(f1, f2) && !m.are_distinct(f1, f2)) {
|
if (!m.are_equal(f1, f2) && !m.are_distinct(f1, f2)) {
|
||||||
if (m.is_bool(f1) &&
|
if (m.is_bool(f1) &&
|
||||||
(!is_uninterp_const(f1) || !is_uninterp_const(f2)))
|
(!is_uninterp_const(f1) || !is_uninterp_const(f2)))
|
||||||
{ m_todo.append(a->get_num_args(), a->get_args()); }
|
|
||||||
else
|
|
||||||
{ add_literal(a, out); }
|
|
||||||
}
|
|
||||||
} else if (m.is_ite(a, f1, f2, f3)) {
|
|
||||||
if (m.are_equal(f2, f3)) { m_todo.push_back(f2); }
|
|
||||||
else if (m_mev.is_true (f2) && m_mev.is_true (f3)) {
|
|
||||||
m_todo.push_back(f2);
|
|
||||||
m_todo.push_back(f3);
|
|
||||||
} else if (m_mev.is_false(f2) && m_mev.is_false(f3)) {
|
|
||||||
m_todo.push_back(f2);
|
|
||||||
m_todo.push_back(f3);
|
|
||||||
} else if (m_mev.is_true(f1)) {
|
|
||||||
m_todo.push_back(f1);
|
|
||||||
m_todo.push_back(f2);
|
|
||||||
} else if (m_mev.is_false(f1)) {
|
|
||||||
m_todo.push_back(f1);
|
|
||||||
m_todo.push_back(f3);
|
|
||||||
}
|
|
||||||
} else if (m.is_xor(a, f1, f2))
|
|
||||||
{ m_todo.append(a->get_num_args(), a->get_args()); }
|
{ m_todo.append(a->get_num_args(), a->get_args()); }
|
||||||
|
else
|
||||||
|
{ add_literal(a, out); }
|
||||||
|
}
|
||||||
|
} else if (m.is_ite(a, f1, f2, f3)) {
|
||||||
|
if (m.are_equal(f2, f3)) { m_todo.push_back(f2); }
|
||||||
|
else if (m_mev.is_true (f2) && m_mev.is_true (f3)) {
|
||||||
|
m_todo.push_back(f2);
|
||||||
|
m_todo.push_back(f3);
|
||||||
|
} else if (m_mev.is_false(f2) && m_mev.is_false(f3)) {
|
||||||
|
m_todo.push_back(f2);
|
||||||
|
m_todo.push_back(f3);
|
||||||
|
} else if (m_mev.is_true(f1)) {
|
||||||
|
m_todo.push_back(f1);
|
||||||
|
m_todo.push_back(f2);
|
||||||
|
} else if (m_mev.is_false(f1)) {
|
||||||
|
m_todo.push_back(f1);
|
||||||
|
m_todo.push_back(f3);
|
||||||
|
}
|
||||||
|
} else if (m.is_xor(a, f1, f2))
|
||||||
|
{ m_todo.append(a->get_num_args(), a->get_args()); }
|
||||||
else if (m.is_implies(a, f1, f2)) {
|
else if (m.is_implies(a, f1, f2)) {
|
||||||
if (m.is_true (v)) {
|
if (m.is_true (v)) {
|
||||||
if (m_mev.is_true(f2)) { m_todo.push_back(f2); }
|
if (m_mev.is_true(f2)) { m_todo.push_back(f2); }
|
||||||
else if (m_mev.is_false(f1)) { m_todo.push_back(f1); }
|
else if (m_mev.is_false(f1)) { m_todo.push_back(f1); }
|
||||||
} else if (m.is_false(v))
|
} else if (m.is_false(v))
|
||||||
{ m_todo.append(a->get_num_args(), a->get_args()); }
|
{ m_todo.append(a->get_num_args(), a->get_args()); }
|
||||||
} else if (m.is_true(a) || m.is_false(a)) { /* nothing */ }
|
} else if (m.is_true(a) || m.is_false(a)) { /* nothing */ }
|
||||||
else {
|
else {
|
||||||
verbose_stream () << "Unexpected expression: "
|
verbose_stream () << "Unexpected expression: "
|
||||||
<< mk_pp(a, m) << "\n";
|
<< mk_pp(a, m) << "\n";
|
||||||
|
@ -837,10 +837,10 @@ namespace {
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
void pick_literals(expr *e, expr_ref_vector &out)
|
void pick_literals(expr *e, expr_ref_vector &out)
|
||||||
{
|
{
|
||||||
SASSERT(m_todo.empty());
|
SASSERT(m_todo.empty());
|
||||||
if (m_visited.is_marked(e)) { return; }
|
if (m_visited.is_marked(e)) { return; }
|
||||||
SASSERT(is_app(e));
|
SASSERT(is_app(e));
|
||||||
|
|
||||||
m_todo.push_back(e);
|
m_todo.push_back(e);
|
||||||
|
@ -852,8 +852,8 @@ namespace {
|
||||||
} while (!m_todo.empty());
|
} while (!m_todo.empty());
|
||||||
}
|
}
|
||||||
|
|
||||||
bool pick_implicant(const expr_ref_vector &in, expr_ref_vector &out)
|
bool pick_implicant(const expr_ref_vector &in, expr_ref_vector &out)
|
||||||
{
|
{
|
||||||
m_visited.reset();
|
m_visited.reset();
|
||||||
expr_ref e(m);
|
expr_ref e(m);
|
||||||
e = mk_and (in);
|
e = mk_and (in);
|
||||||
|
@ -861,7 +861,7 @@ namespace {
|
||||||
|
|
||||||
for (unsigned i = 0, sz = in.size (); i < sz; ++i) {
|
for (unsigned i = 0, sz = in.size (); i < sz; ++i) {
|
||||||
if (is_true || m_mev.is_true(in.get(i)))
|
if (is_true || m_mev.is_true(in.get(i)))
|
||||||
{ pick_literals(in.get(i), out); }
|
{ pick_literals(in.get(i), out); }
|
||||||
}
|
}
|
||||||
|
|
||||||
m_visited.reset ();
|
m_visited.reset ();
|
||||||
|
@ -875,7 +875,7 @@ namespace {
|
||||||
void operator() (expr_ref_vector &in, expr_ref_vector& out)
|
void operator() (expr_ref_vector &in, expr_ref_vector& out)
|
||||||
{pick_implicant (in, out);}
|
{pick_implicant (in, out);}
|
||||||
};
|
};
|
||||||
}
|
}
|
||||||
|
|
||||||
void compute_implicant_literals (model_evaluator_util &mev, expr_ref_vector &formula,
|
void compute_implicant_literals (model_evaluator_util &mev, expr_ref_vector &formula,
|
||||||
expr_ref_vector &res)
|
expr_ref_vector &res)
|
||||||
|
@ -1178,9 +1178,9 @@ void ground_expr(expr *e, expr_ref &out, app_ref_vector &vars) {
|
||||||
expr *e1, *e2;
|
expr *e1, *e2;
|
||||||
if (m_array.is_select (n) && n->get_arg (1) != m_var) {
|
if (m_array.is_select (n) && n->get_arg (1) != m_var) {
|
||||||
m_res.push_back (n->get_arg (1));
|
m_res.push_back (n->get_arg (1));
|
||||||
} else if (m.is_eq(n, e1, e2)) {
|
} else if (m.is_eq(n, e1, e2)) {
|
||||||
if (e1 == m_var) { m_res.push_back(e2); }
|
if (e1 == m_var) { m_res.push_back(e2); }
|
||||||
else if (e2 == m_var) { m_res.push_back(e1); }
|
else if (e2 == m_var) { m_res.push_back(e1); }
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
};
|
};
|
||||||
|
@ -1206,7 +1206,7 @@ void ground_expr(expr *e, expr_ref &out, app_ref_vector &vars) {
|
||||||
tout << i << ": " << mk_pp (terms.get (i), m) << "\n";
|
tout << i << ": " << mk_pp (terms.get (i), m) << "\n";
|
||||||
);
|
);
|
||||||
|
|
||||||
for (unsigned i = 0, e = terms.size(); i < e; ++i) {
|
for (unsigned i = 0, e = terms.size(); i < e; ++i) {
|
||||||
expr* term = terms.get (i);
|
expr* term = terms.get (i);
|
||||||
expr_ref tval (m);
|
expr_ref tval (m);
|
||||||
mev.eval (term, tval, false);
|
mev.eval (term, tval, false);
|
||||||
|
|
|
@ -125,12 +125,12 @@ void project_plugin::push_back(expr_ref_vector& lits, expr* e) {
|
||||||
|
|
||||||
|
|
||||||
class mbp::impl {
|
class mbp::impl {
|
||||||
ast_manager& m;
|
ast_manager& m;
|
||||||
params_ref m_params;
|
params_ref m_params;
|
||||||
th_rewriter m_rw;
|
th_rewriter m_rw;
|
||||||
ptr_vector<project_plugin> m_plugins;
|
ptr_vector<project_plugin> m_plugins;
|
||||||
expr_mark m_visited;
|
expr_mark m_visited;
|
||||||
expr_mark m_bool_visited;
|
expr_mark m_bool_visited;
|
||||||
|
|
||||||
// parameters
|
// parameters
|
||||||
bool m_reduce_all_selects;
|
bool m_reduce_all_selects;
|
||||||
|
@ -280,33 +280,33 @@ class mbp::impl {
|
||||||
}
|
}
|
||||||
else {
|
else {
|
||||||
vars[j++] = var;
|
vars[j++] = var;
|
||||||
|
}
|
||||||
}
|
}
|
||||||
}
|
|
||||||
if (j == vars.size()) {
|
if (j == vars.size()) {
|
||||||
return;
|
return;
|
||||||
}
|
}
|
||||||
vars.shrink(j);
|
vars.shrink(j);
|
||||||
j = 0;
|
j = 0;
|
||||||
for (unsigned i = 0; i < fmls.size(); ++i) {
|
for (unsigned i = 0; i < fmls.size(); ++i) {
|
||||||
expr* fml = fmls[i].get();
|
expr* fml = fmls[i].get();
|
||||||
sub(fml, val);
|
sub(fml, val);
|
||||||
m_rw(val);
|
m_rw(val);
|
||||||
if (!m.is_true(val)) {
|
if (!m.is_true(val)) {
|
||||||
TRACE("qe", tout << mk_pp(fml, m) << " -> " << val << "\n";);
|
TRACE("qe", tout << mk_pp(fml, m) << " -> " << val << "\n";);
|
||||||
fmls[j++] = val;
|
fmls[j++] = val;
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
fmls.shrink(j);
|
fmls.shrink(j);
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
||||||
void subst_vars(model_evaluator& eval, app_ref_vector const& vars, expr_ref& fml) {
|
void subst_vars(model_evaluator& eval, app_ref_vector const& vars, expr_ref& fml) {
|
||||||
expr_safe_replace sub (m);
|
expr_safe_replace sub (m);
|
||||||
for (app * v : vars) {
|
for (app * v : vars) {
|
||||||
sub.insert(v, eval(v));
|
sub.insert(v, eval(v));
|
||||||
}
|
}
|
||||||
sub(fml);
|
sub(fml);
|
||||||
}
|
}
|
||||||
|
|
||||||
struct index_term_finder {
|
struct index_term_finder {
|
||||||
ast_manager& m;
|
ast_manager& m;
|
||||||
|
|
Loading…
Add table
Add a link
Reference in a new issue