mirror of
https://github.com/Z3Prover/z3
synced 2025-04-07 18:05:21 +00:00
fixes to bv/dual-solver,
This commit is contained in:
parent
a4354c960c
commit
89ffb45c4f
|
@ -245,7 +245,7 @@ public:
|
|||
bool is_unsigned(expr const * n, unsigned& u) const {
|
||||
rational val;
|
||||
bool is_int = true;
|
||||
return is_numeral(n, val, is_int) && is_int && val.is_unsigned(), u = val.get_unsigned(), true;
|
||||
return is_numeral(n, val, is_int) && is_int && val.is_unsigned() && (u = val.get_unsigned(), true);
|
||||
}
|
||||
bool is_numeral(expr const * n, rational & val, bool & is_int) const;
|
||||
bool is_numeral(expr const * n, rational & val) const { bool is_int; return is_numeral(n, val, is_int); }
|
||||
|
|
|
@ -95,7 +95,7 @@ unmerge(a,a')
|
|||
- n1 is reinserted. It used to be a root.
|
||||
|
||||
|
||||
--*/
|
||||
*/
|
||||
|
||||
#include "ast/euf/euf_egraph.h"
|
||||
#include "ast/ast_pp.h"
|
||||
|
@ -317,11 +317,22 @@ namespace euf {
|
|||
|
||||
void egraph::set_merge_enabled(enode* n, bool enable_merge) {
|
||||
if (enable_merge != n->merge_enabled()) {
|
||||
toggle_merge_enabled(n);
|
||||
m_updates.push_back(update_record(n, update_record::toggle_merge()));
|
||||
n->set_merge_enabled(enable_merge);
|
||||
}
|
||||
}
|
||||
|
||||
void egraph::toggle_merge_enabled(enode* n) {
|
||||
bool enable_merge = !n->merge_enabled();
|
||||
n->set_merge_enabled(enable_merge);
|
||||
if (n->num_args() > 0) {
|
||||
if (enable_merge)
|
||||
insert_table(n);
|
||||
else
|
||||
m_table.erase(n);
|
||||
}
|
||||
}
|
||||
|
||||
void egraph::set_value(enode* n, lbool value) {
|
||||
force_push();
|
||||
TRACE("euf", tout << bpp(n) << "\n";);
|
||||
|
@ -362,7 +373,7 @@ namespace euf {
|
|||
undo_node();
|
||||
break;
|
||||
case update_record::tag_t::is_toggle_merge:
|
||||
p.r1->set_merge_enabled(!p.r1->merge_enabled());
|
||||
toggle_merge_enabled(p.r1);
|
||||
break;
|
||||
case update_record::tag_t::is_set_parent:
|
||||
undo_eq(p.r1, p.n1, p.r2_num_parents);
|
||||
|
@ -520,6 +531,12 @@ namespace euf {
|
|||
for (enode* c : enode_class(r1))
|
||||
c->m_root = r1;
|
||||
|
||||
for (enode* p : enode_parents(r1))
|
||||
if (p->merge_enabled() && !p->is_cgr() && !p->m_cg) {
|
||||
std::cout << bpp(p) << "\n";
|
||||
SASSERT(false);
|
||||
}
|
||||
|
||||
for (enode* p : enode_parents(r1))
|
||||
if (p->merge_enabled() && (p->is_cgr() || !p->congruent(p->m_cg)))
|
||||
insert_table(p);
|
||||
|
|
|
@ -196,6 +196,7 @@ namespace euf {
|
|||
void push_to_lca(enode* a, enode* lca);
|
||||
void push_congruence(enode* n1, enode* n2, bool commutative);
|
||||
void push_todo(enode* n);
|
||||
void toggle_merge_enabled(enode* n);
|
||||
|
||||
enode_bool_pair insert_table(enode* p);
|
||||
|
||||
|
|
|
@ -138,7 +138,7 @@ namespace euf {
|
|||
bool is_cgr() const { return this == m_cg; }
|
||||
bool commutative() const { return m_commutative; }
|
||||
void mark_interpreted() { SASSERT(num_args() == 0); m_interpreted = true; }
|
||||
bool merge_enabled() { return m_merge_enabled; }
|
||||
bool merge_enabled() const { return m_merge_enabled; }
|
||||
|
||||
enode* get_arg(unsigned i) const { SASSERT(i < num_args()); return m_args[i]; }
|
||||
unsigned hash() const { return m_expr->hash(); }
|
||||
|
|
|
@ -1192,10 +1192,10 @@ namespace lp {
|
|||
|
||||
impq lar_solver::get_tv_ivalue(tv const& t) const {
|
||||
if (t.is_var())
|
||||
return get_ivalue(t.column());
|
||||
return get_column_value(t.column());
|
||||
impq r;
|
||||
for (const auto& p : get_term(t))
|
||||
r += p.coeff() * get_ivalue(p.column());
|
||||
r += p.coeff() * get_column_value(p.column());
|
||||
return r;
|
||||
}
|
||||
|
||||
|
@ -1317,9 +1317,8 @@ namespace lp {
|
|||
|
||||
void lar_solver::mark_rows_for_bound_prop(lpvar j) {
|
||||
auto& column = A_r().m_columns[j];
|
||||
for (auto const& r : column) {
|
||||
m_rows_with_changed_bounds.insert(r.var());
|
||||
}
|
||||
for (auto const& r : column)
|
||||
m_rows_with_changed_bounds.insert(r.var());
|
||||
}
|
||||
|
||||
|
||||
|
|
|
@ -638,7 +638,7 @@ public:
|
|||
inline const static_matrix<mpq, impq> & A_r() const { return m_mpq_lar_core_solver.m_r_A; }
|
||||
// columns
|
||||
bool column_is_int(column_index const& j) const { return column_is_int((unsigned)j); }
|
||||
const impq& get_ivalue(column_index const& j) const { return get_column_value(j); }
|
||||
// const impq& get_ivalue(column_index const& j) const { return get_column_value(j); }
|
||||
const impq& get_column_value(column_index const& j) const { return m_mpq_lar_core_solver.m_r_x[j]; }
|
||||
inline
|
||||
var_index external_to_local(unsigned j) const {
|
||||
|
|
|
@ -51,7 +51,6 @@ namespace arith {
|
|||
|
||||
solver::~solver() {
|
||||
del_bounds(0);
|
||||
std::for_each(m_internalize_states.begin(), m_internalize_states.end(), delete_proc<internalize_state>());
|
||||
}
|
||||
|
||||
void solver::asserted(literal l) {
|
||||
|
|
|
@ -111,7 +111,7 @@ namespace arith {
|
|||
m_to_ensure_var.reset();
|
||||
}
|
||||
};
|
||||
ptr_vector<internalize_state> m_internalize_states;
|
||||
scoped_ptr_vector<internalize_state> m_internalize_states;
|
||||
unsigned m_internalize_head{ 0 };
|
||||
|
||||
class scoped_internalize_state {
|
||||
|
|
|
@ -223,6 +223,9 @@ namespace array {
|
|||
args1.push_back(k);
|
||||
args2.push_back(k);
|
||||
}
|
||||
std::cout << "e1: " << mk_pp(e1, m) << "\n";
|
||||
std::cout << "e2: " << mk_pp(e2, m) << "\n";
|
||||
std::cout << "funcs: " << funcs << "\n";
|
||||
expr_ref sel1(a.mk_select(args1), m);
|
||||
expr_ref sel2(a.mk_select(args2), m);
|
||||
literal lit1 = eq_internalize(e1, e2);
|
||||
|
@ -521,13 +524,11 @@ namespace array {
|
|||
for (unsigned i = 0; i < num_vars; i++) {
|
||||
euf::enode * n = var2enode(i);
|
||||
|
||||
if (!a.is_array(n->get_expr())) {
|
||||
continue;
|
||||
}
|
||||
if (!is_array(n))
|
||||
continue;
|
||||
euf::enode * r = n->get_root();
|
||||
if (r->is_marked1()) {
|
||||
continue;
|
||||
}
|
||||
if (r->is_marked1())
|
||||
continue;
|
||||
// arrays used as indices in other arrays have to be treated as shared issue #3532, #3529
|
||||
if (ctx.is_shared(r) || is_select_arg(r))
|
||||
roots.push_back(r->get_th_var(get_id()));
|
||||
|
|
|
@ -86,6 +86,7 @@ namespace array {
|
|||
}
|
||||
|
||||
void solver::internalize_ext(euf::enode* n) {
|
||||
SASSERT(is_array(n->get_arg(0)));
|
||||
push_axiom(extensionality_axiom(n->get_arg(0), n->get_arg(1)));
|
||||
}
|
||||
|
||||
|
|
|
@ -165,7 +165,10 @@ namespace array {
|
|||
|
||||
void solver::new_diseq_eh(euf::th_eq const& eq) {
|
||||
force_push();
|
||||
push_axiom(extensionality_axiom(var2enode(eq.v1()), var2enode(eq.v2())));
|
||||
euf::enode* n1 = var2enode(eq.v1());
|
||||
euf::enode* n2 = var2enode(eq.v2());
|
||||
if (is_array(n1))
|
||||
push_axiom(extensionality_axiom(n1, n2));
|
||||
}
|
||||
|
||||
bool solver::unit_propagate() {
|
||||
|
|
|
@ -158,6 +158,7 @@ namespace array {
|
|||
void collect_shared_vars(sbuffer<theory_var>& roots);
|
||||
bool add_interface_equalities();
|
||||
bool is_select_arg(euf::enode* r);
|
||||
bool is_array(euf::enode* n) const { return a.is_array(n->get_expr()); }
|
||||
|
||||
// solving
|
||||
void add_parent_select(theory_var v_child, euf::enode* select);
|
||||
|
|
|
@ -176,10 +176,10 @@ namespace bv {
|
|||
args[i] = arg_value;
|
||||
expr_ref r(m.mk_app(n->get_decl(), args), m);
|
||||
set_delay_internalize(r, internalize_mode::init_bits_only_i); // do not bit-blast this multiplier.
|
||||
args[i] = n->get_arg(i);
|
||||
std::cout << "@" << s().scope_lvl() << "\n";
|
||||
args[i] = n->get_arg(i);
|
||||
add_unit(eq_internalize(r, arg_value));
|
||||
}
|
||||
IF_VERBOSE(0, verbose_stream() << "delay internalize @" << s().scope_lvl() << "\n");
|
||||
return false;
|
||||
}
|
||||
if (bv.is_zero(mul_value)) {
|
||||
|
|
|
@ -133,6 +133,9 @@ namespace bv {
|
|||
euf::enode* n = expr2enode(e);
|
||||
app* a = to_app(e);
|
||||
|
||||
if (visited(e))
|
||||
return true;
|
||||
|
||||
SASSERT(!n || !n->is_attached_to(get_id()));
|
||||
bool suppress_args = !get_config().m_bv_reflect && !m.is_considered_uninterpreted(a->get_decl());
|
||||
if (!n)
|
||||
|
@ -294,27 +297,12 @@ namespace bv {
|
|||
atom* a = get_bv2a(bv);
|
||||
if (a)
|
||||
return a;
|
||||
a = new (get_region()) atom();
|
||||
a = new (get_region()) atom(bv);
|
||||
insert_bv2a(bv, a);
|
||||
ctx.push(mk_atom_trail(bv, *this));
|
||||
return a;
|
||||
}
|
||||
|
||||
#if 0
|
||||
solver::eq_atom* solver::mk_eq_atom(sat::bool_var bv) {
|
||||
atom* a = get_bv2a(bv);
|
||||
if (a)
|
||||
return a->is_eq() ? &a->to_eq() : nullptr;
|
||||
else {
|
||||
eq_atom* b = new (get_region()) eq_atom();
|
||||
insert_bv2a(bv, b);
|
||||
ctx.push(mk_atom_trail(bv, *this));
|
||||
return b;
|
||||
}
|
||||
}
|
||||
#endif
|
||||
|
||||
|
||||
void solver::set_bit_eh(theory_var v, literal l, unsigned idx) {
|
||||
SASSERT(m_bits[v][idx] == l);
|
||||
if (s().value(l) != l_undef && s().lvl(l) == 0)
|
||||
|
@ -323,8 +311,7 @@ namespace bv {
|
|||
atom* b = mk_atom(l.var());
|
||||
if (b->m_occs)
|
||||
find_new_diseq_axioms(*b, v, idx);
|
||||
if (!b->is_fresh())
|
||||
ctx.push(add_var_pos_trail(b));
|
||||
ctx.push(add_var_pos_trail(b));
|
||||
b->m_occs = new (get_region()) var_pos_occ(v, idx, b->m_occs);
|
||||
}
|
||||
}
|
||||
|
@ -586,7 +573,7 @@ namespace bv {
|
|||
}
|
||||
|
||||
void solver::add_def(sat::literal def, sat::literal l) {
|
||||
atom* a = new (get_region()) atom();
|
||||
atom* a = new (get_region()) atom(l.var());
|
||||
a->m_var = l;
|
||||
a->m_def = def;
|
||||
insert_bv2a(l.var(), a);
|
||||
|
@ -648,7 +635,7 @@ namespace bv {
|
|||
m_bits[v_arg][idx] = lit;
|
||||
TRACE("bv", tout << "add-bit: " << lit << " " << literal2expr(lit) << "\n";);
|
||||
if (arg_sz > 1) {
|
||||
atom* a = new (get_region()) atom();
|
||||
atom* a = new (get_region()) atom(lit.var());
|
||||
a->m_occs = new (get_region()) var_pos_occ(v_arg, idx);
|
||||
insert_bv2a(lit.var(), a);
|
||||
ctx.push(mk_atom_trail(lit.var(), *this));
|
||||
|
@ -713,20 +700,12 @@ namespace bv {
|
|||
|
||||
void solver::eq_internalized(sat::bool_var b1, sat::bool_var b2, unsigned idx, theory_var v1, theory_var v2, literal lit, euf::enode* n) {
|
||||
atom* a = mk_atom(b1);
|
||||
// eq_atom* b = mk_eq_atom(lit.var());
|
||||
if (a) {
|
||||
if (!a->is_fresh())
|
||||
ctx.push(add_eq_occurs_trail(a));
|
||||
ctx.push(add_eq_occurs_trail(a));
|
||||
auto* next = a->m_eqs;
|
||||
a->m_eqs = new (get_region()) eq_occurs(b1, b2, idx, v1, v2, lit, n, next);
|
||||
if (next)
|
||||
next->m_prev = a->m_eqs;
|
||||
#if 0
|
||||
if (b) {
|
||||
b->m_eqs.push_back(std::make_pair(a, a->m_eqs));
|
||||
ctx.push(push_back_vector<euf::solver, svector<std::pair<bit_atom*,eq_occurs*>>>(b->m_eqs));
|
||||
}
|
||||
#endif
|
||||
}
|
||||
}
|
||||
|
||||
|
|
|
@ -44,7 +44,6 @@ namespace bv {
|
|||
bit_occs_trail(solver& s, atom& a): a(a), m_occs(a.m_occs) {}
|
||||
|
||||
virtual void undo(euf::solver& euf) {
|
||||
IF_VERBOSE(1, verbose_stream() << "add back occurrences " << & a << "\n");
|
||||
a.m_occs = m_occs;
|
||||
}
|
||||
};
|
||||
|
@ -400,20 +399,10 @@ namespace bv {
|
|||
for (; m_prop_queue_head < m_prop_queue.size() && !s().inconsistent(); ++m_prop_queue_head) {
|
||||
auto const p = m_prop_queue[m_prop_queue_head];
|
||||
if (p.m_atom) {
|
||||
unsigned num_atoms = 0, num_eqs = 0, num_assigned = 0, num_eq_assigned = 0, num_lit_assigned = 0;
|
||||
for (auto vp : *p.m_atom) {
|
||||
if (propagate_bits(vp))
|
||||
++num_assigned;
|
||||
++num_atoms;
|
||||
}
|
||||
for (auto const& eq : p.m_atom->eqs()) {
|
||||
++num_eqs;
|
||||
if (s().value(eq.m_literal) != l_undef)
|
||||
++num_lit_assigned;
|
||||
if (propagate_eq_occurs(eq)) {
|
||||
++num_eq_assigned;
|
||||
}
|
||||
}
|
||||
for (auto vp : *p.m_atom)
|
||||
propagate_bits(vp);
|
||||
for (auto const& eq : p.m_atom->eqs())
|
||||
propagate_eq_occurs(eq);
|
||||
}
|
||||
else
|
||||
propagate_bits(p.m_vp);
|
||||
|
@ -669,7 +658,7 @@ namespace bv {
|
|||
if (!a)
|
||||
continue;
|
||||
|
||||
atom* new_a = new (result->get_region()) atom();
|
||||
atom* new_a = new (result->get_region()) atom(i);
|
||||
m_bool_var2atom.setx(i, new_a, nullptr);
|
||||
for (auto vp : *a)
|
||||
new_a->m_occs = new (result->get_region()) var_pos_occ(vp.first, vp.second, new_a->m_occs);
|
||||
|
@ -800,6 +789,7 @@ namespace bv {
|
|||
find_wpos(v2);
|
||||
bool_var cv = consequent.var();
|
||||
atom* a = get_bv2a(cv);
|
||||
force_push();
|
||||
if (a)
|
||||
for (auto curr : *a)
|
||||
if (propagate_eqc || find(curr.first) != find(v2) || curr.second != idx)
|
||||
|
|
|
@ -126,7 +126,7 @@ namespace bv {
|
|||
eq_occurs_it(eq_occurs* c) : m_first(c) {}
|
||||
eq_occurs operator*() { return *m_first; }
|
||||
eq_occurs_it& operator++() { m_first = m_first->m_next; return *this; }
|
||||
eq_occurs_it operator++(int) { eq_occurs_it tmp = *this; ++* this; return tmp; }
|
||||
eq_occurs_it operator++(int) { eq_occurs_it tmp = *this; ++*this; return tmp; }
|
||||
bool operator==(eq_occurs_it const& other) const { return m_first == other.m_first; }
|
||||
bool operator!=(eq_occurs_it const& other) const { return !(*this == other); }
|
||||
};
|
||||
|
@ -157,16 +157,16 @@ namespace bv {
|
|||
};
|
||||
|
||||
struct atom {
|
||||
bool_var m_bv;
|
||||
eq_occurs* m_eqs;
|
||||
var_pos_occ * m_occs;
|
||||
svector<std::pair<atom*, eq_occurs*>> m_bit2occ;
|
||||
literal m_var { sat::null_literal };
|
||||
literal m_def { sat::null_literal };
|
||||
atom() :m_eqs(nullptr), m_occs(nullptr) {}
|
||||
atom(bool_var b) :m_bv(b), m_eqs(nullptr), m_occs(nullptr) {}
|
||||
~atom() { m_bit2occ.clear(); }
|
||||
var_pos_it begin() const { return var_pos_it(m_occs); }
|
||||
var_pos_it end() const { return var_pos_it(nullptr); }
|
||||
bool is_fresh() const { return !m_occs && !m_eqs; }
|
||||
eqs_iterator eqs() const { return eqs_iterator(m_eqs); }
|
||||
};
|
||||
|
||||
|
|
|
@ -104,7 +104,7 @@ namespace euf {
|
|||
sat::literal lit;
|
||||
if (!m.is_bool(e))
|
||||
drat_log_node(e);
|
||||
else
|
||||
else
|
||||
lit = attach_lit(literal(si.add_bool_var(e), false), e);
|
||||
|
||||
if (!m.is_bool(e) && m.get_sort(e)->get_family_id() != null_family_id) {
|
||||
|
@ -153,6 +153,8 @@ namespace euf {
|
|||
m_egraph.set_bool_var(n, v);
|
||||
if (m.is_eq(e) || m.is_or(e) || m.is_and(e) || m.is_not(e))
|
||||
m_egraph.set_merge_enabled(n, false);
|
||||
if (!si.is_bool_op(e))
|
||||
track_relevancy(lit.var());
|
||||
return lit;
|
||||
}
|
||||
|
||||
|
|
|
@ -90,19 +90,42 @@ namespace sat {
|
|||
}
|
||||
|
||||
bool dual_solver::operator()(solver const& s) {
|
||||
m_core.reset();
|
||||
m_core.append(m_units);
|
||||
if (m_roots.empty())
|
||||
return true;
|
||||
m_solver.user_push();
|
||||
m_solver.add_clause(m_roots.size(), m_roots.c_ptr(), status::input());
|
||||
m_lits.reset();
|
||||
for (bool_var v : m_tracked_vars)
|
||||
m_lits.push_back(literal(v, l_false == s.value(m_var2ext[v])));
|
||||
lbool is_sat = m_solver.check(m_lits.size(), m_lits.c_ptr());
|
||||
m_core.reset();
|
||||
m_core.append(m_units);
|
||||
if (is_sat == l_false)
|
||||
for (literal lit : m_solver.get_core())
|
||||
m_core.push_back(lit2ext(lit));
|
||||
TRACE("euf", m_solver.display(tout << "is-sat: " << is_sat << " core: " << m_core << "\n"););
|
||||
m_core.push_back(lit2ext(lit));
|
||||
if (is_sat == l_true) {
|
||||
IF_VERBOSE(0, display(s, verbose_stream()));
|
||||
UNREACHABLE();
|
||||
}
|
||||
TRACE("dual", m_solver.display(tout << "is-sat: " << is_sat << " core: " << m_core << "\n"););
|
||||
m_solver.user_pop(1);
|
||||
return is_sat == l_false;
|
||||
}
|
||||
|
||||
|
||||
std::ostream& dual_solver::display(solver const& s, std::ostream& out) const {
|
||||
for (auto r : m_roots)
|
||||
out << r << " " << m_solver.value(r) << "\n";
|
||||
for (unsigned v = 0; v < m_solver.num_vars(); ++v) {
|
||||
bool_var w = m_var2ext.get(v, null_bool_var);
|
||||
if (w == null_bool_var)
|
||||
continue;
|
||||
lbool v1 = m_solver.value(v);
|
||||
lbool v2 = s.value(w);
|
||||
if (v1 == v2)
|
||||
continue;
|
||||
out << w << " " << v1 << " " << v2 << "\n";
|
||||
}
|
||||
return out;
|
||||
}
|
||||
}
|
||||
|
|
|
@ -40,6 +40,9 @@ namespace sat {
|
|||
bool_var var2ext(bool_var v);
|
||||
literal ext2lit(literal lit);
|
||||
literal lit2ext(literal lit);
|
||||
|
||||
std::ostream& display(solver const& s, std::ostream& out) const;
|
||||
|
||||
public:
|
||||
dual_solver(reslimit& l);
|
||||
void push();
|
||||
|
|
Loading…
Reference in a new issue