mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-20 12:53:38 +00:00
Code Activity

Switched compute_implicant_literals to use new model API

Browse source
This commit is contained in:
Arie Gurfinkel 2018-06-16 13:43:30 -07:00
parent 60888a93eb
commit fffc8489bf
4 changed files with 188 additions and 182 deletions
Download patch file Download diff file Expand all files Collapse all files

5
src/api/api_qe.cpp
View file

@ -119,11 +119,8 @@ extern "C"
facts.push_back (to_expr (fml)); facts.push_back (to_expr (fml));
flatten_and (facts); flatten_and (facts);
spacer::model_evaluator_util mev (mk_c(c)->m());
mev.set_model (*model);
expr_ref_vector lits (mk_c(c)->m()); expr_ref_vector lits (mk_c(c)->m());
spacer::compute_implicant_literals (mev, facts, lits); spacer::compute_implicant_literals (*model, facts, lits);
expr_ref result (mk_c(c)->m ()); expr_ref result (mk_c(c)->m ());
result = mk_and (lits); result = mk_and (lits);

8
src/muz/spacer/spacer_context.cpp
View file

@ -366,7 +366,7 @@ pob *derivation::create_next_child ()
// get an implicant of the summary // get an implicant of the summary
expr_ref_vector u(m), lits (m); expr_ref_vector u(m), lits (m);
u.push_back (rf->get ()); u.push_back (rf->get ());
compute_implicant_literals (mev, u, lits); compute_implicant_literals (*model, u, lits);
expr_ref v(m); expr_ref v(m);
v = mk_and (lits); v = mk_and (lits);
@ -1172,7 +1172,7 @@ expr_ref pred_transformer::get_origin_summary (model_evaluator_util &mev,
// -- pick an implicant // -- pick an implicant
expr_ref_vector lits(m); expr_ref_vector lits(m);
compute_implicant_literals (mev, summary, lits); compute_implicant_literals (*mev.get_model(), summary, lits);
return mk_and(lits); return mk_and(lits);
} }
@ -3599,7 +3599,7 @@ reach_fact *pred_transformer::mk_rf (pob& n, model_evaluator_util &mev,
if (ctx.reach_dnf()) { if (ctx.reach_dnf()) {
expr_ref_vector u(m), lits(m); expr_ref_vector u(m), lits(m);
u.push_back (res); u.push_back (res);
compute_implicant_literals (mev, u, lits); compute_implicant_literals (*mev.get_model(), u, lits);
res = mk_and (lits); res = mk_and (lits);
} }
@ -3670,7 +3670,7 @@ bool context::create_children(pob& n, datalog::rule const& r,
forms.push_back(pt.get_transition(r)); forms.push_back(pt.get_transition(r));
forms.push_back(n.post()); forms.push_back(n.post());
compute_implicant_literals (mev, forms, lits); compute_implicant_literals (*mev.get_model(), forms, lits);
expr_ref phi = mk_and (lits); expr_ref phi = mk_and (lits);
// primed variables of the head // primed variables of the head

309
src/muz/spacer/spacer_util.cpp
View file

@ -405,67 +405,67 @@ namespace spacer {
namespace { namespace {
class implicant_picker { class implicant_picker {
model_evaluator_util &m_mev; model &m_model;
ast_manager &m; ast_manager &m;
arith_util m_arith; arith_util m_arith;
expr_ref_vector m_todo; expr_ref_vector m_todo;
expr_mark m_visited; expr_mark m_visited;
// add literal to the implicant
// applies lightweight normalization
void add_literal(expr *e, expr_ref_vector &out) {
SASSERT(m.is_bool(e));
void add_literal (expr *e, expr_ref_vector &out) { expr_ref res(m), v(m);
SASSERT (m.is_bool (e)); v = m_model(e);
// the literal must have a value
SASSERT(m.is_true(v) || m.is_false(v));
expr_ref res (m), v(m); res = m.is_false(v) ? m.mk_not(e) : e;
m_mev.eval (e, v, false);
SASSERT (m.is_true (v) || m.is_false (v));
res = m.is_false (v) ? m.mk_not (e) : e; if (m.is_distinct(res)) {
// --(distinct a b) == (not (= a b))
if (m.is_distinct (res)) {
// -- (distinct a b) == (not (= a b))
if (to_app(res)->get_num_args() == 2) { if (to_app(res)->get_num_args() == 2) {
res = m.mk_eq (to_app(res)->get_arg(0), to_app(res)->get_arg(1)); res = m.mk_eq(to_app(res)->get_arg(0),
res = m.mk_not (res); to_app(res)->get_arg(1));
res = m.mk_not(res);
} }
} }
expr *nres, *f1, *f2; expr *nres, *f1, *f2;
if (m.is_not(res, nres)) { if (m.is_not(res, nres)) {
// -- (not (xor a b)) == (= a b) // --(not (xor a b)) == (= a b)
if (m.is_xor(nres, f1, f2)) if (m.is_xor(nres, f1, f2))
{ res = m.mk_eq(f1, f2); } res = m.mk_eq(f1, f2);
// -- split arithmetic inequality // -- split arithmetic inequality
else if (m.is_eq (nres, f1, f2) && m_arith.is_int_real (f1)) { else if (m.is_eq(nres, f1, f2) && m_arith.is_int_real(f1)) {
expr_ref u(m); expr_ref u(m);
u = m_arith.mk_lt(f1, f2); u = m_arith.mk_lt(f1, f2);
if (m_mev.eval (u, v, false) && m.is_true (v)) res = m_model.is_true(u) ? u : m_arith.mk_lt(f2, f1);
{ res = u; }
else
{ res = m_arith.mk_lt(f2, f1); }
} }
} }
if (!m_mev.is_true (res)) { if (!m_model.is_true(res)) {
verbose_stream() << "Bad literal: " << mk_pp(res, m) << "\n"; verbose_stream() << "Bad literal: " << res << "\n";
} }
SASSERT (m_mev.is_true (res)); SASSERT(m_model.is_true(res));
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); v = m_model(a);
bool is_true = m.is_true(v); bool is_true = m.is_true(v);
if (!is_true && !m.is_false(v)) return; if (!is_true && !m.is_false(v)) return;
expr *na, *f1, *f2, *f3; expr *na, *f1, *f2, *f3;
if (m.is_true(a) || m.is_false(a)) { SASSERT(!m.is_false(a));
if (m.is_true(a)) {
// noop // noop
} }
else if (a->get_family_id() != m.get_basic_family_id()) { else if (a->get_family_id() != m.get_basic_family_id()) {
@ -479,14 +479,15 @@ namespace {
} }
else if (m.is_distinct(a)) { else if (m.is_distinct(a)) {
if (!is_true) { if (!is_true) {
f1 = qe::project_plugin::pick_equality(m, *m_mev.get_model(), a); f1 = qe::project_plugin::pick_equality(m, m_model, a);
m_todo.push_back(f1); m_todo.push_back(f1);
} }
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(), a->get_args())); m_todo.push_back(m.mk_distinct_expanded(a->get_num_args(),
a->get_args()));
} }
} }
else if (m.is_and(a)) { else if (m.is_and(a)) {
@ -494,8 +495,8 @@ namespace {
m_todo.append(a->get_num_args(), a->get_args()); m_todo.append(a->get_num_args(), a->get_args());
} }
else { else {
for (expr* e : *a) { for(expr* e : *a) {
if (m_mev.is_false(e)) { if (m_model.is_false(e)) {
m_todo.push_back(e); m_todo.push_back(e);
break; break;
} }
@ -506,17 +507,19 @@ namespace {
if (!is_true) if (!is_true)
m_todo.append(a->get_num_args(), a->get_args()); m_todo.append(a->get_num_args(), a->get_args());
else { else {
for (expr * e : *a) { for(expr * e : *a) {
if (m_mev.is_true(e)) { if (m_model.is_true(e)) {
m_todo.push_back(e); m_todo.push_back(e);
break; break;
} }
} }
} }
} }
else if (m.is_eq(a, f1, f2) || (is_true && m.is_not(a, na) && m.is_xor (na, f1, f2))) { else if (m.is_eq(a, f1, f2) ||
(is_true && 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) && (!is_uninterp_const(f1) || !is_uninterp_const(f2))) if (m.is_bool(f1) &&
(!is_uninterp_const(f1) || !is_uninterp_const(f2)))
m_todo.append(a->get_num_args(), a->get_args()); m_todo.append(a->get_num_args(), a->get_args());
else else
add_literal(a, out); add_literal(a, out);
@ -526,19 +529,19 @@ namespace {
if (m.are_equal(f2, f3)) { if (m.are_equal(f2, f3)) {
m_todo.push_back(f2); m_todo.push_back(f2);
} }
else if (m_mev.is_true (f2) && m_mev.is_true (f3)) { else if (m_model.is_true(f2) && m_model.is_true(f3)) {
m_todo.push_back(f2); m_todo.push_back(f2);
m_todo.push_back(f3); m_todo.push_back(f3);
} }
else if (m_mev.is_false(f2) && m_mev.is_false(f3)) { else if (m_model.is_false(f2) && m_model.is_false(f3)) {
m_todo.push_back(f2); m_todo.push_back(f2);
m_todo.push_back(f3); m_todo.push_back(f3);
} }
else if (m_mev.is_true(f1)) { else if (m_model.is_true(f1)) {
m_todo.push_back(f1); m_todo.push_back(f1);
m_todo.push_back(f2); m_todo.push_back(f2);
} }
else if (m_mev.is_false(f1)) { else if (m_model.is_false(f1)) {
m_todo.push_back(f1); m_todo.push_back(f1);
m_todo.push_back(f3); m_todo.push_back(f3);
} }
@ -548,16 +551,18 @@ namespace {
} }
else if (m.is_implies(a, f1, f2)) { else if (m.is_implies(a, f1, f2)) {
if (is_true) { if (is_true) {
if (m_mev.is_true(f2)) if (m_model.is_true(f2))
m_todo.push_back(f2); m_todo.push_back(f2);
else if (m_mev.is_false(f1)) else if (m_model.is_false(f1))
m_todo.push_back(f1); m_todo.push_back(f1);
} }
else else
m_todo.append(a->get_num_args(), a->get_args()); m_todo.append(a->get_num_args(), a->get_args());
} }
else { else {
IF_VERBOSE(0, verbose_stream () << "Unexpected expression: " << mk_pp(a, m) << "\n"); IF_VERBOSE(0,
verbose_stream() << "Unexpected expression: "
<< mk_pp(a, m) << "\n");
UNREACHABLE(); UNREACHABLE();
} }
} }
@ -574,70 +579,72 @@ namespace {
m_todo.pop_back(); m_todo.pop_back();
process_app(a, out); process_app(a, out);
m_visited.mark(a, true); m_visited.mark(a, true);
} 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();
bool is_true = m_mev.is_true (in); bool is_true = m_model.is_true(in);
for (expr* e : in) { for(expr* e : in) {
if (is_true || m_mev.is_true(e)) { if (is_true || m_model.is_true(e)) {
pick_literals(e, out); pick_literals(e, out);
} }
} }
m_visited.reset (); m_visited.reset();
return is_true; return is_true;
} }
public: public:
implicant_picker (model_evaluator_util &mev) : implicant_picker(model &mdl) :
m_mev (mev), m (m_mev.get_ast_manager ()), m_arith(m), m_todo(m) {} m_model(mdl), m(m_model.get_manager()), m_arith(m), m_todo(m) {}
void operator() (expr_ref_vector &in, expr_ref_vector& out) { void operator()(expr_ref_vector &in, expr_ref_vector& out) {
pick_implicant (in, out); model::scoped_model_completion _sc_(m_model, false);
pick_implicant(in, out);
} }
}; };
} }
void compute_implicant_literals (model_evaluator_util &mev, expr_ref_vector &formula, void compute_implicant_literals(model &mdl,
expr_ref_vector &formula,
expr_ref_vector &res) { expr_ref_vector &res) {
// flatten the formula and remove all trivial literals // flatten the formula and remove all trivial literals
// TBD: not clear why there is a dependence on it (other than // TBD: not clear why there is a dependence on it(other than
// not handling of Boolean constants by implicant_picker), however, // not handling of Boolean constants by implicant_picker), however,
// it was a source of a problem on a benchmark // it was a source of a problem on a benchmark
flatten_and(formula); flatten_and(formula);
if (formula.empty()) {return;} if (formula.empty()) {return;}
implicant_picker ipick (mev); implicant_picker ipick(mdl);
ipick (formula, res); ipick(formula, res);
} }
void simplify_bounds_old(expr_ref_vector& cube) { void simplify_bounds_old(expr_ref_vector& cube) {
ast_manager& m = cube.m(); ast_manager& m = cube.m();
scoped_no_proof _no_pf_(m); scoped_no_proof _no_pf_(m);
goal_ref g(alloc(goal, m, false, false, false)); goal_ref g(alloc(goal, m, false, false, false));
for (expr* c : cube) for(expr* c : cube)
g->assert_expr(c); g->assert_expr(c);
goal_ref_buffer result; goal_ref_buffer result;
tactic_ref simplifier = mk_arith_bounds_tactic(m); tactic_ref simplifier = mk_arith_bounds_tactic(m);
(*simplifier)(g, result); (*simplifier)(g, result);
SASSERT(result.size() == 1); SASSERT(result.size() == 1);
goal* r = result[0]; goal* r = result[0];
cube.reset(); cube.reset();
for (unsigned i = 0; i < r->size(); ++i) { for(unsigned i = 0; i < r->size(); ++i) {
cube.push_back(r->form(i)); cube.push_back(r->form(i));
} }
} }
void simplify_bounds_new (expr_ref_vector &cube) { void simplify_bounds_new(expr_ref_vector &cube) {
ast_manager &m = cube.m(); ast_manager &m = cube.m();
scoped_no_proof _no_pf_(m); scoped_no_proof _no_pf_(m);
goal_ref g(alloc(goal, m, false, false, false)); goal_ref g(alloc(goal, m, false, false, false));
for (expr* c : cube) for(expr* c : cube)
g->assert_expr(c); g->assert_expr(c);
goal_ref_buffer goals; goal_ref_buffer goals;
@ -645,12 +652,12 @@ namespace {
tactic_ref prop_bounds = mk_propagate_ineqs_tactic(m); tactic_ref prop_bounds = mk_propagate_ineqs_tactic(m);
tactic_ref t = and_then(prop_values.get(), prop_bounds.get()); tactic_ref t = and_then(prop_values.get(), prop_bounds.get());
(*t)(g, goals); (*t)(g, goals);
SASSERT(goals.size() == 1); SASSERT(goals.size() == 1);
g = goals[0]; g = goals[0];
cube.reset(); cube.reset();
for (unsigned i = 0; i < g->size(); ++i) { for(unsigned i = 0; i < g->size(); ++i) {
cube.push_back(g->form(i)); cube.push_back(g->form(i));
} }
} }
@ -664,86 +671,86 @@ namespace {
ast_manager &m; ast_manager &m;
arith_util m_util; arith_util m_util;
adhoc_rewriter_cfg (ast_manager &manager) : m(manager), m_util(m) {} adhoc_rewriter_cfg(ast_manager &manager) : m(manager), m_util(m) {}
bool is_le(func_decl const * n) const { return m_util.is_le(n); } bool is_le(func_decl const * n) const { return m_util.is_le(n); }
bool is_ge(func_decl const * n) const { return m_util.is_ge(n); } bool is_ge(func_decl const * n) const { return m_util.is_ge(n); }
br_status reduce_app (func_decl * f, unsigned num, expr * const * args, br_status reduce_app(func_decl * f, unsigned num, expr * const * args,
expr_ref & result, proof_ref & result_pr) { expr_ref & result, proof_ref & result_pr) {
expr * e; expr * e;
if (is_le(f)) if (is_le(f))
return mk_le_core (args[0], args[1], result); return mk_le_core(args[0], args[1], result);
if (is_ge(f)) if (is_ge(f))
return mk_ge_core (args[0], args[1], result); return mk_ge_core(args[0], args[1], result);
if (m.is_not(f) && m.is_not (args[0], e)) { if (m.is_not(f) && m.is_not(args[0], e)) {
result = e; result = e;
return BR_DONE; return BR_DONE;
} }
return BR_FAILED; return BR_FAILED;
} }
br_status mk_le_core (expr *arg1, expr * arg2, expr_ref & result) { br_status mk_le_core(expr *arg1, expr * arg2, expr_ref & result) {
// t <= -1 ==> t < 0 ==> ! (t >= 0) // t <= -1 ==> t < 0 ==> !(t >= 0)
if (m_util.is_int (arg1) && m_util.is_minus_one (arg2)) { if (m_util.is_int(arg1) && m_util.is_minus_one(arg2)) {
result = m.mk_not (m_util.mk_ge (arg1, mk_zero ())); result = m.mk_not(m_util.mk_ge(arg1, mk_zero()));
return BR_DONE; return BR_DONE;
} }
return BR_FAILED; return BR_FAILED;
} }
br_status mk_ge_core (expr * arg1, expr * arg2, expr_ref & result) { br_status mk_ge_core(expr * arg1, expr * arg2, expr_ref & result) {
// t >= 1 ==> t > 0 ==> ! (t <= 0) // t >= 1 ==> t > 0 ==> !(t <= 0)
if (m_util.is_int (arg1) && is_one (arg2)) { if (m_util.is_int(arg1) && is_one(arg2)) {
result = m.mk_not (m_util.mk_le (arg1, mk_zero ())); result = m.mk_not(m_util.mk_le(arg1, mk_zero()));
return BR_DONE; return BR_DONE;
} }
return BR_FAILED; return BR_FAILED;
} }
expr * mk_zero () {return m_util.mk_numeral (rational (0), true);} expr * mk_zero() {return m_util.mk_numeral(rational(0), true);}
bool is_one (expr const * n) const { bool is_one(expr const * n) const {
rational val; return m_util.is_numeral (n, val) && val.is_one (); rational val; return m_util.is_numeral(n, val) && val.is_one();
} }
}; };
void normalize (expr *e, expr_ref &out, void normalize(expr *e, expr_ref &out,
bool use_simplify_bounds, bool use_simplify_bounds,
bool use_factor_eqs) bool use_factor_eqs)
{ {
params_ref params; params_ref params;
// arith_rewriter // arith_rewriter
params.set_bool ("sort_sums", true); params.set_bool("sort_sums", true);
params.set_bool ("gcd_rounding", true); params.set_bool("gcd_rounding", true);
params.set_bool ("arith_lhs", true); params.set_bool("arith_lhs", true);
// poly_rewriter // poly_rewriter
params.set_bool ("som", true); params.set_bool("som", true);
params.set_bool ("flat", true); params.set_bool("flat", true);
// apply rewriter // apply rewriter
th_rewriter rw(out.m(), params); th_rewriter rw(out.m(), params);
rw (e, out); rw(e, out);
adhoc_rewriter_cfg adhoc_cfg(out.m ()); adhoc_rewriter_cfg adhoc_cfg(out.m());
rewriter_tpl<adhoc_rewriter_cfg> adhoc_rw (out.m (), false, adhoc_cfg); rewriter_tpl<adhoc_rewriter_cfg> adhoc_rw(out.m(), false, adhoc_cfg);
adhoc_rw (out.get (), out); adhoc_rw(out.get(), out);
if (out.m().is_and(out)) { if (out.m().is_and(out)) {
expr_ref_vector v(out.m()); expr_ref_vector v(out.m());
flatten_and (out, v); flatten_and(out, v);
if (v.size() > 1) { if (v.size() > 1) {
// sort arguments of the top-level and // sort arguments of the top-level and
std::stable_sort (v.c_ptr(), v.c_ptr() + v.size(), ast_lt_proc()); std::stable_sort(v.c_ptr(), v.c_ptr() + v.size(), ast_lt_proc());
if (use_simplify_bounds) { if (use_simplify_bounds) {
// remove redundant inequalities // remove redundant inequalities
simplify_bounds (v); simplify_bounds(v);
} }
if (use_factor_eqs) { if (use_factor_eqs) {
// -- refactor equivalence classes and choose a representative // -- refactor equivalence classes and choose a representative
qe::term_graph egraph(out.m()); qe::term_graph egraph(out.m());
egraph.add_lits (v); egraph.add_lits(v);
v.reset(); v.reset();
egraph.to_lits(v); egraph.to_lits(v);
} }
@ -755,10 +762,10 @@ namespace {
<< mk_and(v) << "\n";); << mk_and(v) << "\n";);
TRACE("spacer_normalize", TRACE("spacer_normalize",
qe::term_graph egraph(out.m()); qe::term_graph egraph(out.m());
for (expr* e : v) egraph.add_lit (to_app(e)); for(expr* e : v) egraph.add_lit(to_app(e));
tout << "Reduced app:\n" tout << "Reduced app:\n"
<< mk_pp(egraph.to_app(), out.m()) << "\n";); << mk_pp(egraph.to_app(), out.m()) << "\n";);
out = mk_and (v); out = mk_and(v);
} }
} }
} }
@ -768,34 +775,34 @@ namespace {
ast_manager &m; ast_manager &m;
arith_util m_arith; arith_util m_arith;
adhoc_rewriter_rpp (ast_manager &manager) : m(manager), m_arith(m) {} adhoc_rewriter_rpp(ast_manager &manager) : m(manager), m_arith(m) {}
bool is_le(func_decl const * n) const { return m_arith.is_le(n); } bool is_le(func_decl const * n) const { return m_arith.is_le(n); }
bool is_ge(func_decl const * n) const { return m_arith.is_ge(n); } bool is_ge(func_decl const * n) const { return m_arith.is_ge(n); }
bool is_lt(func_decl const * n) const { return m_arith.is_lt(n); } bool is_lt(func_decl const * n) const { return m_arith.is_lt(n); }
bool is_gt(func_decl const * n) const { return m_arith.is_gt(n); } bool is_gt(func_decl const * n) const { return m_arith.is_gt(n); }
bool is_zero (expr const * n) const {rational val; return m_arith.is_numeral(n, val) && val.is_zero();} bool is_zero(expr const * n) const {rational val; return m_arith.is_numeral(n, val) && val.is_zero();}
br_status reduce_app (func_decl * f, unsigned num, expr * const * args, br_status reduce_app(func_decl * f, unsigned num, expr * const * args,
expr_ref & result, proof_ref & result_pr) expr_ref & result, proof_ref & result_pr)
{ {
br_status st = BR_FAILED; br_status st = BR_FAILED;
expr *e1, *e2, *e3, *e4; expr *e1, *e2, *e3, *e4;
// rewrites (= (+ A (* -1 B)) 0) into (= A B) // rewrites(=(+ A(* -1 B)) 0) into(= A B)
if (m.is_eq (f) && is_zero (args [1]) && if (m.is_eq(f) && is_zero(args [1]) &&
m_arith.is_add (args[0], e1, e2) && m_arith.is_add(args[0], e1, e2) &&
m_arith.is_mul (e2, e3, e4) && m_arith.is_minus_one (e3)) { m_arith.is_mul(e2, e3, e4) && m_arith.is_minus_one(e3)) {
result = m.mk_eq (e1, e4); result = m.mk_eq(e1, e4);
return BR_DONE; return BR_DONE;
} }
// simplify normalized leq, where right side is different from 0 // simplify normalized leq, where right side is different from 0
// rewrites (<= (+ A (* -1 B)) C) into (<= A B+C) // rewrites(<=(+ A(* -1 B)) C) into(<= A B+C)
else if ((is_le(f) || is_lt(f) || is_ge(f) || is_gt(f)) && else if ((is_le(f) || is_lt(f) || is_ge(f) || is_gt(f)) &&
m_arith.is_add (args[0], e1, e2) && m_arith.is_add(args[0], e1, e2) &&
m_arith.is_mul (e2, e3, e4) && m_arith.is_minus_one (e3)) { m_arith.is_mul(e2, e3, e4) && m_arith.is_minus_one(e3)) {
expr_ref rhs(m); expr_ref rhs(m);
rhs = is_zero (args[1]) ? e4 : m_arith.mk_add(e4, args[1]); rhs = is_zero(args[1]) ? e4 : m_arith.mk_add(e4, args[1]);
if (is_le(f)) { if (is_le(f)) {
result = m_arith.mk_le(e1, rhs); result = m_arith.mk_le(e1, rhs);
@ -813,7 +820,7 @@ namespace {
{ UNREACHABLE(); } { UNREACHABLE(); }
} }
// simplify negation of ordering predicate // simplify negation of ordering predicate
else if (m.is_not (f)) { else if (m.is_not(f)) {
if (m_arith.is_lt(args[0], e1, e2)) { if (m_arith.is_lt(args[0], e1, e2)) {
result = m_arith.mk_ge(e1, e2); result = m_arith.mk_ge(e1, e2);
st = BR_DONE; st = BR_DONE;
@ -834,11 +841,11 @@ namespace {
mk_epp::mk_epp(ast *t, ast_manager &m, unsigned indent, mk_epp::mk_epp(ast *t, ast_manager &m, unsigned indent,
unsigned num_vars, char const * var_prefix) : unsigned num_vars, char const * var_prefix) :
mk_pp (t, m, m_epp_params, indent, num_vars, var_prefix), m_epp_expr(m) { mk_pp(t, m, m_epp_params, indent, num_vars, var_prefix), m_epp_expr(m) {
m_epp_params.set_uint("min_alias_size", UINT_MAX); m_epp_params.set_uint("min_alias_size", UINT_MAX);
m_epp_params.set_uint("max_depth", UINT_MAX); m_epp_params.set_uint("max_depth", UINT_MAX);
if (is_expr (m_ast)) { if (is_expr(m_ast)) {
rw(to_expr(m_ast), m_epp_expr); rw(to_expr(m_ast), m_epp_expr);
m_ast = m_epp_expr; m_ast = m_epp_expr;
} }
@ -858,11 +865,11 @@ namespace {
if (vars.size() < fv.size()) { if (vars.size() < fv.size()) {
vars.resize(fv.size()); vars.resize(fv.size());
} }
for (unsigned i = 0, sz = fv.size(); i < sz; ++i) { for(unsigned i = 0, sz = fv.size(); i < sz; ++i) {
sort *s = fv[i] ? fv[i] : m.mk_bool_sort(); sort *s = fv[i] ? fv[i] : m.mk_bool_sort();
vars[i] = mk_zk_const(m, i, s); vars[i] = mk_zk_const(m, i, s);
var_subst vs(m, false); var_subst vs(m, false);
vs(e, vars.size(), (expr * *) vars.c_ptr(), out); vs(e, vars.size(),(expr * *) vars.c_ptr(), out);
} }
} }
@ -872,75 +879,75 @@ namespace {
app_ref m_var; app_ref m_var;
expr_ref_vector &m_res; expr_ref_vector &m_res;
index_term_finder (ast_manager &mgr, app* v, expr_ref_vector &res) : m(mgr), m_array (m), m_var (v, m), m_res (res) {} index_term_finder(ast_manager &mgr, app* v, expr_ref_vector &res) : m(mgr), m_array(m), m_var(v, m), m_res(res) {}
void operator() (var *n) {} void operator()(var *n) {}
void operator() (quantifier *n) {} void operator()(quantifier *n) {}
void operator() (app *n) { void operator()(app *n) {
if (m_array.is_select (n) || m.is_eq(n)) { if (m_array.is_select(n) || m.is_eq(n)) {
unsigned i = 0; unsigned i = 0;
for (expr * arg : *n) { for(expr * arg : *n) {
if ((m.is_eq(n) || i > 0) && m_var != arg) m_res.push_back (arg); if ((m.is_eq(n) || i > 0) && m_var != arg) m_res.push_back(arg);
++i; ++i;
} }
} }
} }
}; };
bool mbqi_project_var (model_evaluator_util &mev, app* var, expr_ref &fml) { bool mbqi_project_var(model_evaluator_util &mev, app* var, expr_ref &fml) {
ast_manager &m = fml.get_manager (); ast_manager &m = fml.get_manager();
expr_ref val(m); expr_ref val(m);
mev.eval (var, val, false); mev.eval(var, val, false);
TRACE ("mbqi_project_verbose", TRACE("mbqi_project_verbose",
tout << "MBQI: var: " << mk_pp (var, m) << "\n" tout << "MBQI: var: " << mk_pp(var, m) << "\n"
<< "fml: " << fml << "\n";); << "fml: " << fml << "\n";);
expr_ref_vector terms (m); expr_ref_vector terms(m);
index_term_finder finder (m, var, terms); index_term_finder finder(m, var, terms);
for_each_expr (finder, fml); for_each_expr(finder, fml);
TRACE ("mbqi_project_verbose", TRACE("mbqi_project_verbose",
tout << "terms:\n" << terms << "\n";); tout << "terms:\n" << terms << "\n";);
for (expr * term : terms) { for(expr * term : terms) {
expr_ref tval (m); expr_ref tval(m);
mev.eval (term, tval, false); mev.eval(term, tval, false);
TRACE ("mbqi_project_verbose", TRACE("mbqi_project_verbose",
tout << "term: " << mk_pp (term, m) tout << "term: " << mk_pp(term, m)
<< " tval: " << tval << " tval: " << tval
<< " val: " << mk_pp (val, m) << "\n";); << " val: " << mk_pp(val, m) << "\n";);
// -- if the term does not contain an occurrence of var // -- if the term does not contain an occurrence of var
// -- and is in the same equivalence class in the model // -- and is in the same equivalence class in the model
if (tval == val && !occurs (var, term)) { if (tval == val && !occurs(var, term)) {
TRACE ("mbqi_project", TRACE("mbqi_project",
tout << "MBQI: replacing " << mk_pp (var, m) << " with " << mk_pp (term, m) << "\n";); tout << "MBQI: replacing " << mk_pp(var, m) << " with " << mk_pp(term, m) << "\n";);
expr_safe_replace sub(m); expr_safe_replace sub(m);
sub.insert (var, term); sub.insert(var, term);
sub (fml); sub(fml);
return true; return true;
} }
} }
TRACE ("mbqi_project", TRACE("mbqi_project",
tout << "MBQI: failed to eliminate " << mk_pp (var, m) << " from " << fml << "\n";); tout << "MBQI: failed to eliminate " << mk_pp(var, m) << " from " << fml << "\n";);
return false; return false;
} }
void mbqi_project (model &M, app_ref_vector &vars, expr_ref &fml) { void mbqi_project(model &M, app_ref_vector &vars, expr_ref &fml) {
ast_manager &m = fml.get_manager (); ast_manager &m = fml.get_manager();
model_evaluator_util mev(m); model_evaluator_util mev(m);
mev.set_model (M); mev.set_model(M);
expr_ref tmp(m); expr_ref tmp(m);
// -- evaluate to initialize mev cache // -- evaluate to initialize mev cache
mev.eval (fml, tmp, false); mev.eval(fml, tmp, false);
tmp.reset (); tmp.reset();
unsigned j = 0; unsigned j = 0;
for (app* v : vars) for(app* v : vars)
if (!mbqi_project_var (mev, v, fml)) if (!mbqi_project_var(mev, v, fml))
vars[j++] = v; vars[j++] = v;
vars.shrink(j); vars.shrink(j);
} }
@ -959,7 +966,7 @@ namespace {
for_each_expr(cs, fml); for_each_expr(cs, fml);
return false; return false;
} }
catch (found) { catch(found) {
return true; return true;
} }
} }
@ -970,8 +977,8 @@ namespace {
collect_indices(app_ref_vector& indices): m_indices(indices), a(indices.get_manager()) {} collect_indices(app_ref_vector& indices): m_indices(indices), a(indices.get_manager()) {}
void operator()(expr* n) {} void operator()(expr* n) {}
void operator()(app* n) { void operator()(app* n) {
if (a.is_select (n)) if (a.is_select(n))
for (unsigned i = 1; i < n->get_num_args(); ++i) for(unsigned i = 1; i < n->get_num_args(); ++i)
if (is_app(n->get_arg(i))) if (is_app(n->get_arg(i)))
m_indices.push_back(to_app(n->get_arg(i))); m_indices.push_back(to_app(n->get_arg(i)));
} }

4
src/muz/spacer/spacer_util.h
View file

@ -129,7 +129,9 @@ namespace spacer {
// TBD: sort out // TBD: sort out
void expand_literals(ast_manager &m, expr_ref_vector& conjs); void expand_literals(ast_manager &m, expr_ref_vector& conjs);
void compute_implicant_literals (model_evaluator_util &mev, expr_ref_vector &formula, expr_ref_vector &res); void compute_implicant_literals(model &mdl,
expr_ref_vector &formula,
expr_ref_vector &res);
void simplify_bounds (expr_ref_vector &lemmas); void simplify_bounds (expr_ref_vector &lemmas);
void normalize(expr *e, expr_ref &out, bool use_simplify_bounds = true, bool factor_eqs = false); void normalize(expr *e, expr_ref &out, bool use_simplify_bounds = true, bool factor_eqs = false);