mirror of
https://github.com/Z3Prover/z3
synced 2025-04-07 18:05:21 +00:00
SLS: log clause , allow more frequent export of SLS state to SMT
This commit is contained in:
parent
84447b7031
commit
4b72e517b7
|
@ -123,38 +123,37 @@ namespace sls {
|
|||
// distance to true
|
||||
template<typename num_t>
|
||||
num_t arith_base<num_t>::dtt(bool sign, num_t const& args, ineq const& ineq) const {
|
||||
num_t zero{ 0 };
|
||||
switch (ineq.m_op) {
|
||||
case ineq_kind::LE:
|
||||
if (sign) {
|
||||
if (args + ineq.m_coeff <= 0)
|
||||
return -ineq.m_coeff - args + 1;
|
||||
return zero;
|
||||
return num_t(0);
|
||||
}
|
||||
if (args + ineq.m_coeff <= 0)
|
||||
return zero;
|
||||
return num_t(0);
|
||||
return args + ineq.m_coeff;
|
||||
case ineq_kind::EQ:
|
||||
if (sign) {
|
||||
if (args + ineq.m_coeff == 0)
|
||||
return num_t(1);
|
||||
return zero;
|
||||
return num_t(0);
|
||||
}
|
||||
if (args + ineq.m_coeff == 0)
|
||||
return zero;
|
||||
return num_t(0);
|
||||
return num_t(1);
|
||||
case ineq_kind::LT:
|
||||
if (sign) {
|
||||
if (args + ineq.m_coeff < 0)
|
||||
return -ineq.m_coeff - args;
|
||||
return zero;
|
||||
return num_t(0);
|
||||
}
|
||||
if (args + ineq.m_coeff < 0)
|
||||
return zero;
|
||||
return num_t(0);
|
||||
return args + ineq.m_coeff + 1;
|
||||
default:
|
||||
UNREACHABLE();
|
||||
return zero;
|
||||
return num_t(0);
|
||||
}
|
||||
}
|
||||
|
||||
|
@ -863,36 +862,36 @@ namespace sls {
|
|||
template<typename num_t>
|
||||
typename arith_base<num_t>::var_t arith_base<num_t>::mk_op(arith_op_kind k, expr* e, expr* x, expr* y) {
|
||||
auto v = mk_var(e);
|
||||
auto w = mk_term(x);
|
||||
auto vx = mk_term(x);
|
||||
auto vy = mk_term(y);
|
||||
unsigned idx = m_ops.size();
|
||||
num_t val;
|
||||
switch (k) {
|
||||
case arith_op_kind::OP_MOD:
|
||||
val = value(v) == 0 ? num_t(0) : mod(value(w), value(v));
|
||||
val = value(vy) == 0 ? num_t(0) : mod(value(v), value(vy));
|
||||
break;
|
||||
case arith_op_kind::OP_REM:
|
||||
if (value(v) == 0)
|
||||
if (value(vy) == 0)
|
||||
val = 0;
|
||||
else {
|
||||
val = value(w);
|
||||
val %= value(v);
|
||||
val = value(vx);
|
||||
val %= value(vy);
|
||||
}
|
||||
break;
|
||||
case arith_op_kind::OP_IDIV:
|
||||
val = value(v) == 0 ? num_t(0): div(value(w), value(v));
|
||||
val = value(vy) == 0 ? num_t(0): div(value(vx), value(vy));
|
||||
break;
|
||||
case arith_op_kind::OP_DIV:
|
||||
val = value(v) == 0? num_t(0) : value(w) / value(v);
|
||||
val = value(vy) == 0? num_t(0) : value(vx) / value(vy);
|
||||
break;
|
||||
case arith_op_kind::OP_ABS:
|
||||
val = abs(value(w));
|
||||
val = abs(value(vx));
|
||||
break;
|
||||
default:
|
||||
NOT_IMPLEMENTED_YET();
|
||||
break;
|
||||
}
|
||||
verbose_stream() << "mk-op " << mk_bounded_pp(e, m) << "\n";
|
||||
m_ops.push_back({v, k, v, w});
|
||||
m_ops.push_back({v, k, vx, vy});
|
||||
m_vars[v].m_def_idx = idx;
|
||||
m_vars[v].m_op = k;
|
||||
m_vars[v].set_value(val);
|
||||
|
@ -1606,7 +1605,7 @@ namespace sls {
|
|||
bool arith_base<num_t>::repair_idiv(op_def const& od) {
|
||||
auto v1 = value(od.m_arg1);
|
||||
auto v2 = value(od.m_arg2);
|
||||
IF_VERBOSE(0, verbose_stream() << "todo repair div");
|
||||
IF_VERBOSE(0, verbose_stream() << "TODO repair div");
|
||||
// bail
|
||||
return update(od.m_var, v2 == 0 ? num_t(0) : div(v1, v2));
|
||||
}
|
||||
|
@ -1615,7 +1614,7 @@ namespace sls {
|
|||
bool arith_base<num_t>::repair_div(op_def const& od) {
|
||||
auto v1 = value(od.m_arg1);
|
||||
auto v2 = value(od.m_arg2);
|
||||
IF_VERBOSE(0, verbose_stream() << "todo repair /");
|
||||
IF_VERBOSE(0, verbose_stream() << "TODO repair /");
|
||||
// bail
|
||||
return update(od.m_var, v2 == 0 ? num_t(0) : v1 / v2);
|
||||
}
|
||||
|
@ -2112,6 +2111,7 @@ namespace sls {
|
|||
auto const& vi = m_vars[v];
|
||||
if (vi.m_def_idx == UINT_MAX)
|
||||
return true;
|
||||
verbose_stream() << " repair def " << mk_bounded_pp(vi.m_expr, m) << "\n";
|
||||
TRACE("sls", tout << "repair def " << mk_bounded_pp(vi.m_expr, m) << "\n");
|
||||
switch (vi.m_op) {
|
||||
case arith_op_kind::LAST_ARITH_OP:
|
||||
|
|
|
@ -114,10 +114,19 @@ namespace sls {
|
|||
}
|
||||
// flip the last literal on the replay stack
|
||||
IF_VERBOSE(10, verbose_stream() << "sls.euf - flip " << flit << "\n");
|
||||
log_clause(lits);
|
||||
ctx.add_clause(lits);
|
||||
return flit;
|
||||
}
|
||||
|
||||
void euf_plugin::log_clause(sat::literal_vector const& lits) {
|
||||
IF_VERBOSE(3, verbose_stream() << "block " << lits << "\n";
|
||||
for (auto lit : lits)
|
||||
verbose_stream() << (lit.sign() ? "~" : "") << mk_bounded_pp(ctx.atom(lit.var()), m) << "\n";
|
||||
verbose_stream() << "\n";
|
||||
);
|
||||
}
|
||||
|
||||
void euf_plugin::propagate_literal(sat::literal lit) {
|
||||
SASSERT(ctx.is_true(lit));
|
||||
auto e = ctx.atom(lit.var());
|
||||
|
@ -154,6 +163,7 @@ namespace sls {
|
|||
++m_stats.m_num_conflicts;
|
||||
if (flit != sat::null_literal)
|
||||
ctx.flip(flit.var());
|
||||
log_clause(lits);
|
||||
};
|
||||
|
||||
if (lit.sign() && m.is_eq(e, x, y))
|
||||
|
|
|
@ -56,6 +56,7 @@ namespace sls {
|
|||
sat::literal to_literal(size_t* p) { return sat::to_literal(static_cast<unsigned>(reinterpret_cast<size_t>(p) >> 4)); };
|
||||
|
||||
void validate_model();
|
||||
void log_clause(sat::literal_vector const& lits);
|
||||
|
||||
public:
|
||||
euf_plugin(context& c);
|
||||
|
|
|
@ -293,7 +293,7 @@ namespace sls {
|
|||
}
|
||||
|
||||
void smt_plugin::export_from_sls() {
|
||||
if (unsat().size() >= m_min_unsat_size)
|
||||
if (unsat().size() > m_min_unsat_size)
|
||||
return;
|
||||
m_min_unsat_size = unsat().size();
|
||||
export_phase_from_sls();
|
||||
|
|
Loading…
Reference in a new issue