mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-27 10:55:50 +00:00
Code Activity

lifting iff to binary

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-09-27 03:45:45 -07:00
parent 1dcbd2d86c
commit 6c71baf77b
5 changed files with 51 additions and 31 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/sat/smt/euf_solver.cpp
View file

@ -488,10 +488,8 @@ namespace euf {
return sat::check_result::CR_CONTINUE;
if (m_qsolver)
apply_solver(m_qsolver);
if (num_nodes < m_egraph.num_nodes()) {
IF_VERBOSE(1, verbose_stream() << "new nodes created, but not detected\n");
if (num_nodes < m_egraph.num_nodes())
return sat::check_result::CR_CONTINUE;
}
TRACE("after_search", s().display(tout););
if (give_up)
return sat::check_result::CR_GIVEUP;

65
src/sat/smt/q_ematch.cpp
View file

@ -427,33 +427,11 @@ namespace q {
expr_ref body(mk_not(m, q->get_expr()), m);
q = m.update_quantifier(q, forall_k, body);
}
expr_ref_vector ors(m);
expr_ref_vector ors(m);
flatten_or(q->get_expr(), ors);
for (expr* arg : ors) {
bool sign = m.is_not(arg, arg);
expr* l, *r;
if (m.is_distinct(arg) && to_app(arg)->get_num_args() == 2) {
l = to_app(arg)->get_arg(0);
r = to_app(arg)->get_arg(1);
sign = !sign;
}
else if (!m.is_eq(arg, l, r) || is_ground(arg)) {
l = arg;
r = sign ? m.mk_false() : m.mk_true();
sign = false;
}
if (m.is_true(l) || m.is_false(l))
std::swap(l, r);
if (sign && m.is_false(r)) {
r = m.mk_true();
sign = false;
}
else if (sign && m.is_true(r)) {
r = m.mk_false();
sign = false;
}
cl->m_lits.push_back(lit(expr_ref(l, m), expr_ref(r, m), sign));
}
for (expr* arg : ors)
cl->m_lits.push_back(clausify_literal(arg));
if (q->get_num_patterns() == 0) {
expr_ref tmp(m);
m_infer_patterns(q, tmp);
@ -468,6 +446,41 @@ namespace q {
return cl;
}
lit ematch::clausify_literal(expr* arg) {
bool sign = m.is_not(arg, arg);
expr* _l, *_r;
expr_ref l(m), r(m);
// convert into equality or equivalence
if (m.is_distinct(arg) && to_app(arg)->get_num_args() == 2) {
l = to_app(arg)->get_arg(0);
r = to_app(arg)->get_arg(1);
sign = !sign;
}
else if (!is_ground(arg) && m.is_eq(arg, _l, _r)) {
l = _l;
r = _r;
}
else {
l = arg;
r = sign ? m.mk_false() : m.mk_true();
sign = false;
}
// convert Boolean disequalities into equality
if (m.is_true(l) || m.is_false(l))
std::swap(l, r);
if (sign && m.is_false(r)) {
r = m.mk_true();
sign = false;
}
else if (sign && m.is_true(r)) {
r = m.mk_false();
sign = false;
}
return lit(l, r, sign);
}
/**
* Attach ground subterms of patterns so they appear shared.
*/

1
src/sat/smt/q_ematch.h
View file

@ -112,6 +112,7 @@ namespace q {
void attach_ground_pattern_terms(expr* pat);
clause* clausify(quantifier* q);
lit clausify_literal(expr* arg);
fingerprint* add_fingerprint(clause& c, binding& b, unsigned max_generation);
void set_tmp_binding(fingerprint& fp);

4
src/sat/smt/q_eval.cpp
View file

@ -171,10 +171,10 @@ namespace q {
}
euf::enode* eval::operator()(unsigned n, euf::enode* const* binding, expr* e, euf::enode_pair_vector& evidence) {
if (is_ground(e))
return ctx.get_egraph().find(e);
if (m_mark.is_marked(e))
return m_eval[e->get_id()];
if (is_ground(e))
return ctx.get_egraph().find(e);
ptr_buffer<expr> todo;
ptr_buffer<euf::enode> args;
todo.push_back(e);

8
src/sat/smt/q_solver.cpp
View file

@ -232,6 +232,14 @@ namespace q {
else
UNREACHABLE();
expr* a, *b;
if (m_expanded.size() == 1 && m.is_iff(m_expanded.get(0), a, b)) {
expr_ref f1(m.mk_implies(a, b), m);
expr_ref f2(m.mk_implies(b, a), m);
m_expanded.reset();
m_expanded.push_back(f1);
m_expanded.push_back(f2);
}
if (m_expanded.size() > 1) {
for (unsigned i = m_expanded.size(); i-- > 0; ) {
expr_ref tmp(m.update_quantifier(q, m_expanded.get(i)), m);