mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 17:15:31 +00:00
Code Activity

bugfixes

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2023-12-27 14:00:28 -08:00
parent 6103c9d718
commit 737913b67e
10 changed files with 54 additions and 30 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/sat/smt/polysat/constraints.cpp
View file

@ -25,7 +25,7 @@ namespace polysat {
pdd lhs = p, rhs = q;
bool is_positive = true;
ule_constraint::simplify(is_positive, lhs, rhs);
auto* cnstr = alloc(ule_constraint, p, q);
auto* cnstr = alloc(ule_constraint, lhs, rhs);
c.trail().push(new_obj_trail(cnstr));
auto sc = signed_constraint(ckind_t::ule_t, cnstr);
return is_positive ? sc : ~sc;

30
src/sat/smt/polysat/core.cpp
View file

@ -39,7 +39,7 @@ namespace polysat {
public:
mk_assign_var(pvar v, core& c) : m_var(v), c(c) {}
void undo() {
c.m_justification[m_var] = constraint_id::null();
c.m_justification[m_var] = null_dependency;
c.m_assignment.pop();
}
};
@ -124,7 +124,7 @@ namespace polysat {
unsigned v = m_vars.size();
m_vars.push_back(sz2pdd(sz).mk_var(v));
m_activity.push_back({ sz, 0 });
m_justification.push_back(constraint_id::null());
m_justification.push_back(null_dependency);
m_watch.push_back({});
m_var_queue.mk_var_eh(v);
m_viable.ensure_var(v);
@ -173,18 +173,25 @@ namespace polysat {
return final_check();
m_var = m_var_queue.next_var();
s.trail().push(mk_dqueue_var(m_var, *this));
switch (m_viable.find_viable(m_var, m_value)) {
case find_t::empty:
TRACE("bv", tout << "check-conflict v" << m_var << "\n");
s.set_conflict(m_viable.explain());
// propagate_unsat_core();
return sat::check_result::CR_CONTINUE;
case find_t::singleton:
s.propagate(m_constraints.eq(var2pdd(m_var), m_value), m_viable.explain());
case find_t::singleton: {
TRACE("bv", tout << "check-propagate v" << m_var << " := " << m_value << "\n");
auto d = s.propagate(m_constraints.eq(var2pdd(m_var), m_value), m_viable.explain());
propagate_assignment(m_var, m_value, d);
return sat::check_result::CR_CONTINUE;
}
case find_t::multiple:
TRACE("bv", tout << "check-multiple v" << m_var << " := " << m_value << "\n");
s.add_eq_literal(m_var, m_value);
return sat::check_result::CR_CONTINUE;
case find_t::resource_out:
TRACE("bv", tout << "check-resource out v" << m_var << "\n");
m_var_queue.unassign_var_eh(m_var);
return sat::check_result::CR_GIVEUP;
}
@ -199,6 +206,8 @@ namespace polysat {
auto [sc, d, value] = m_constraint_index[idx.id];
SASSERT(value != l_undef);
lbool eval_value = eval(sc);
sc.display(verbose_stream()) << " eval: " << eval_value << "\n";
CTRACE("bv", eval_value == l_undef, sc.display(tout << "eval: ") << " evaluates to " << eval_value << "\n");
SASSERT(eval_value != l_undef);
if (eval_value == value)
continue;
@ -233,7 +242,7 @@ namespace polysat {
for (auto v : sc.vars()) {
if (!is_assigned(v))
continue;
auto new_level = s.level(get_dependency(m_justification[v]));
auto new_level = s.level(m_justification[v]);
if (new_level < lvl)
continue;
if (new_level > lvl)
@ -260,8 +269,9 @@ namespace polysat {
SASSERT(value != l_undef);
if (value == l_false)
sc = ~sc;
TRACE("bv", tout << "propagate " << sc << " using " << dep << " := " << value << "\n");
if (sc.is_eq(m_var, m_value))
propagate_assignment(m_var, m_value, idx);
propagate_assignment(m_var, m_value, dep);
else
sc.activate(*this, dep);
}
@ -270,13 +280,15 @@ namespace polysat {
m_watch[var].push_back(idx);
}
void core::propagate_assignment(pvar v, rational const& value, constraint_id dep) {
void core::propagate_assignment(pvar v, rational const& value, dependency dep) {
TRACE("bv", tout << "propagate assignment v" << v << " := " << value << " " << is_assigned(v) << "\n");
if (is_assigned(v))
return;
if (m_var_queue.contains(v)) {
m_var_queue.del_var_eh(v);
s.trail().push(mk_dqueue_var(v, *this));
}
m_values[v] = value;
m_justification[v] = dep;
m_assignment.push(v , value);
@ -417,7 +429,7 @@ namespace polysat {
dependency_vector deps;
for (auto v : sc.vars())
if (is_assigned(v))
deps.push_back(get_dependency(m_justification[v]));
deps.push_back(m_justification[v]);
return deps;
}
@ -448,7 +460,7 @@ namespace polysat {
for (auto const& [sc, d, value] : m_constraint_index)
out << sc << " " << d << " := " << value << "\n";
for (unsigned i = 0; i < m_vars.size(); ++i) {
out << m_vars[i] << " := " << m_values[i] << " " << get_dependency(m_justification[i]) << "\n";
out << m_vars[i] << " := " << m_values[i] << " " << m_justification[i] << "\n";
}
m_var_queue.display(out << "vars ") << "\n";
return out;

4
src/sat/smt/polysat/core.h
View file

@ -63,7 +63,7 @@ namespace polysat {
// attributes associated with variables
vector<pdd> m_vars; // for each variable a pdd
vector<rational> m_values; // current value of assigned variable
constraint_id_vector m_justification; // justification for assignment
dependency_vector m_justification; // justification for assignment
activity m_activity; // activity of variables
var_queue<activity> m_var_queue; // priority queue of variables to assign
vector<unsigned_vector> m_watch; // watch lists for variables for constraints on m_prop_queue where they occur
@ -80,7 +80,7 @@ namespace polysat {
bool is_assigned(pvar v) { return !m_justification[v].is_null(); }
void propagate_assignment(constraint_id idx);
void propagate_eval(constraint_id idx);
void propagate_assignment(pvar v, rational const& value, constraint_id dep);
void propagate_assignment(pvar v, rational const& value, dependency dep);
void propagate_unsat_core();
void propagate(constraint_id id, signed_constraint& sc, lbool value, dependency const& d);

13
src/sat/smt/polysat/ule_constraint.cpp
View file

@ -86,6 +86,8 @@ namespace polysat {
SASSERT_EQ(lhs.power_of_2(), rhs.power_of_2());
unsigned const N = lhs.power_of_2();
// verbose_stream() << "simplify " << lhs << " <= " << rhs << "\n";
// 0 <= p --> 0 <= 0
if (lhs.is_zero()) {
rhs = 0;
@ -139,13 +141,11 @@ namespace polysat {
}
}
// -p + k <= k --> p <= k
if (rhs.is_val() && !rhs.is_zero() && lhs.offset() == rhs.val()) {
LOG("-p + k <= k --> p <= k");
lhs = rhs - lhs;
}
// k <= p + k --> p <= -k-1
if (lhs.is_val() && !lhs.is_zero() && lhs.val() == rhs.offset()) {
LOG("k <= p + k --> p <= -k-1");
pdd k = lhs;
@ -153,7 +153,6 @@ namespace polysat {
rhs = -k - 1;
}
// k <= -p --> p-1 <= -k-1
if (lhs.is_val() && rhs.leading_coefficient().get_bit(N - 1) && !rhs.offset().is_zero()) {
LOG("k <= -p --> p-1 <= -k-1");
pdd k = lhs;
@ -161,8 +160,6 @@ namespace polysat {
rhs = -k - 1;
}
// -p <= k --> -k-1 <= p-1
// if (rhs.is_val() && lhs.leading_coefficient() > rational::power_of_two(N - 1) && !lhs.offset().is_zero()) {
if (rhs.is_val() && lhs.leading_coefficient().get_bit(N - 1) && !lhs.offset().is_zero()) {
LOG("-p <= k --> -k-1 <= p-1");
pdd k = rhs;
@ -170,6 +167,10 @@ namespace polysat {
lhs = -k - 1;
}
if (rhs.is_zero() && lhs.leading_coefficient().get_bit(N - 1) && !lhs.offset().is_zero()) {
LOG("-p <= 0 --> p <= 0");
lhs = -lhs;
}
// NOTE: do not use pdd operations in conditions when comparing pdd values.
// e.g.: "lhs.offset() == (rhs + 1).val()" is problematic with the following evaluation:
// 1. return reference into pdd_manager::m_values from lhs.offset()
@ -177,7 +178,6 @@ namespace polysat {
// 3. now the reference returned from lhs.offset() may be invalid
pdd const rhs_plus_one = rhs + 1;
// p - k <= -k - 1 --> k <= p
// TODO: potential bug here: first call offset(), then rhs+1 has to reallocate pdd_manager::m_values, then the reference to offset is broken.
if (rhs.is_val() && !rhs.is_zero() && lhs.offset() == rhs_plus_one.val()) {
LOG("p - k <= -k - 1 --> k <= p");
@ -231,6 +231,7 @@ namespace polysat {
lhs *= x;
SASSERT(lhs.leading_coefficient().is_power_of_two());
}
// verbose_stream() << "simplified " << lhs << " <= " << rhs << "\n";
} // simplify_impl
}

3
src/sat/smt/polysat/viable.cpp
View file

@ -84,7 +84,6 @@ namespace polysat {
}
find_t viable::find_viable(pvar v, rational& lo) {
display(verbose_stream() << "find viable for v" << v << "\n");
rational hi;
switch (find_viable(v, lo, hi)) {
case l_true:
@ -193,6 +192,8 @@ namespace polysat {
* - set k := l + v.width - w.width, lo' := 2^{v.width-w.width} lo, hi' := 2^{v.width-w.width} hi.
*/
lbool viable::next_viable_layer(pvar w, layer& layer, rational& val) {
if (!layer.entries)
return l_true;
unsigned v_width = m_num_bits;
unsigned w_width = c.size(w);
unsigned l = w_width - layer.bit_width;

10
src/sat/smt/polysat_internalize.cpp
View file

@ -106,9 +106,9 @@ namespace polysat {
case OP_UGT: internalize_le<false, false, true>(a); break;
case OP_SGT: internalize_le<true, false, true>(a); break;
case OP_BUMUL_NO_OVFL: internalize_binaryc(a, [&](pdd const& p, pdd const& q) { return m_core.umul_ovfl(p, q); }); break;
case OP_BSMUL_NO_OVFL: internalize_binaryc(a, [&](pdd const& p, pdd const& q) { return m_core.smul_ovfl(p, q); }); break;
case OP_BSMUL_NO_UDFL: internalize_binaryc(a, [&](pdd const& p, pdd const& q) { return m_core.smul_udfl(p, q); }); break;
case OP_BUMUL_NO_OVFL: internalize_binary_predicate(a, [&](pdd const& p, pdd const& q) { return ~m_core.umul_ovfl(p, q); }); break;
case OP_BSMUL_NO_OVFL: internalize_binary_predicate(a, [&](pdd const& p, pdd const& q) { return ~m_core.smul_ovfl(p, q); }); break;
case OP_BSMUL_NO_UDFL: internalize_binary_predicate(a, [&](pdd const& p, pdd const& q) { return ~m_core.smul_udfl(p, q); }); break;
case OP_BUMUL_OVFL:
case OP_BSMUL_OVFL:
@ -187,10 +187,10 @@ namespace polysat {
ctx.push(mk_atom_trail(bv, *this));
}
void solver::internalize_binaryc(app* e, std::function<polysat::signed_constraint(pdd, pdd)> const& fn) {
void solver::internalize_binary_predicate(app* e, std::function<polysat::signed_constraint(pdd, pdd)> const& fn) {
auto p = expr2pdd(e->get_arg(0));
auto q = expr2pdd(e->get_arg(1));
auto sc = ~fn(p, q);
auto sc = fn(p, q);
sat::literal lit = expr2literal(e);
if (lit.sign())
sc = ~sc;

15
src/sat/smt/polysat_solver.cpp
View file

@ -167,6 +167,7 @@ namespace polysat {
auto n = var2enode(v);
auto eq = eq_internalize(n->get_expr(), bv.mk_numeral(val, get_bv_size(v)));
s().set_phase(eq);
ctx.mark_relevant(eq);
}
void solver::new_eq_eh(euf::th_eq const& eq) {
@ -205,6 +206,7 @@ namespace polysat {
// Everything goes over expressions/literals. polysat::core is not responsible for replaying expressions.
dependency solver::propagate(signed_constraint sc, dependency_vector const& deps) {
TRACE("bv", sc.display(tout << "propagate ") << "\n");
sat::literal lit = ctx.mk_literal(constraint2expr(sc));
if (s().value(lit) == l_true)
return dependency(lit.var());
@ -257,7 +259,9 @@ namespace polysat {
}
void solver::propagate(dependency const& d, bool sign, dependency_vector const& deps) {
TRACE("bv", tout << "propagate " << d << " " << sign << "\n");
auto [core, eqs] = explain_deps(deps);
SASSERT(d.is_bool_var() || d.is_eq());
if (d.is_bool_var()) {
auto bv = d.bool_var();
auto lit = sat::literal(bv, sign);
@ -335,16 +339,23 @@ namespace polysat {
}
expr_ref solver::constraint2expr(signed_constraint const& sc) {
expr_ref result(m);
switch (sc.op()) {
case ckind_t::ule_t: {
auto l = pdd2expr(sc.to_ule().lhs());
auto h = pdd2expr(sc.to_ule().rhs());
return expr_ref(bv.mk_ule(l, h), m);
result = bv.mk_ule(l, h);
if (sc.sign())
result = m.mk_not(result);
return result;
}
case ckind_t::umul_ovfl_t: {
auto l = pdd2expr(sc.to_umul_ovfl().p());
auto r = pdd2expr(sc.to_umul_ovfl().q());
return expr_ref(m.mk_not(bv.mk_bvumul_no_ovfl(l, r)), m);
result = bv.mk_bvumul_no_ovfl(l, r);
if (!sc.sign())
result = m.mk_not(result);
return result;
}
case ckind_t::smul_fl_t:
case ckind_t::op_t:

2
src/sat/smt/polysat_solver.h
View file

@ -105,7 +105,7 @@ namespace polysat {
void internalize_unary(app* e, std::function<pdd(pdd)> const& fn);
void internalize_binary(app* e, std::function<pdd(pdd, pdd)> const& fn);
void internalize_binary(app* e, std::function<expr*(expr*, expr*)> const& fn);
void internalize_binaryc(app* e, std::function<signed_constraint(pdd, pdd)> const& fn);
void internalize_binary_predicate(app* e, std::function<signed_constraint(pdd, pdd)> const& fn);
void internalize_par_unary(app* e, std::function<pdd(pdd,unsigned)> const& fn);
void internalize_novfl(app* n, std::function<void(unsigned, expr* const*, expr* const*, expr_ref&)>& fn);
void internalize_interp(app* n, std::function<expr*(expr*, expr*)>& ibin, std::function<expr*(expr*)>& un);