mirror of
https://github.com/Z3Prover/z3
synced 2025-04-22 16:45:31 +00:00
testing / debugging arithmetic
This commit is contained in:
Nikolaj Bjorner
parent
ae55d30961
commit
5b0d49cd76
10 changed files with 269 additions and 139 deletions
|
|
@ -61,13 +61,20 @@ namespace sat {
|
|||
m_steps_since_progress = 0;
|
||||
unsigned steps = 0;
|
||||
save_best_values();
|
||||
while (m_min_sz != 0 && m_steps_since_progress++ <= 1500000) {
|
||||
if (should_reinit_weights()) do_reinit_weights();
|
||||
else if (steps % 5000 == 0) shift_weights(), m_plugin->on_rescale();
|
||||
else if (should_restart()) do_restart(), m_plugin->on_restart();
|
||||
else if (do_flip<true>());
|
||||
else shift_weights(), m_plugin->on_rescale();
|
||||
++steps;
|
||||
try {
|
||||
while (m_min_sz != 0 && m_steps_since_progress++ <= 1500000) {
|
||||
if (should_reinit_weights()) do_reinit_weights();
|
||||
else if (steps % 5000 == 0) shift_weights(), m_plugin->on_rescale();
|
||||
else if (should_restart()) do_restart(), m_plugin->on_restart();
|
||||
else if (do_flip<true>());
|
||||
else shift_weights(), m_plugin->on_rescale();
|
||||
verbose_stream() << "steps: " << steps << " min_sz: " << m_min_sz << " unsat: " << m_unsat.size() << "\n";
|
||||
++steps;
|
||||
}
|
||||
}
|
||||
catch (z3_exception& ex) {
|
||||
IF_VERBOSE(0, verbose_stream() << "Exception: " << ex.msg() << "\n");
|
||||
throw;
|
||||
}
|
||||
m_plugin->finish_search();
|
||||
}
|
||||
|
|
|
|||
|
|
@ -214,19 +214,20 @@ namespace sls {
|
|||
// or flip on first non-negative score
|
||||
template<typename num_t>
|
||||
void arith_base<num_t>::repair(sat::literal lit, ineq const& ineq) {
|
||||
num_t new_value;
|
||||
num_t new_value, old_value;
|
||||
if (UINT_MAX == ineq.m_var_to_flip)
|
||||
dtt_reward(lit);
|
||||
auto v = ineq.m_var_to_flip;
|
||||
|
||||
if (v == UINT_MAX) {
|
||||
IF_VERBOSE(1, verbose_stream() << "no var to flip\n");
|
||||
IF_VERBOSE(0, verbose_stream() << "no var to flip\n");
|
||||
return;
|
||||
}
|
||||
// verbose_stream() << "var to flip " << v << "\n";
|
||||
if (!cm(ineq, v, new_value)) {
|
||||
IF_VERBOSE(1, verbose_stream() << "no critical move for " << v << "\n");
|
||||
IF_VERBOSE(0, verbose_stream() << "no critical move for " << v << "\n");
|
||||
return;
|
||||
}
|
||||
verbose_stream() << "repair " << lit << ": " << ineq << " var: v" << v << " := " << value(v) << " -> " << new_value << "\n";
|
||||
update(v, new_value);
|
||||
}
|
||||
|
||||
|
|
@ -331,9 +332,11 @@ namespace sls {
|
|||
template<typename num_t>
|
||||
void arith_base<num_t>::update(var_t v, num_t const& new_value) {
|
||||
auto& vi = m_vars[v];
|
||||
expr* e = vi.m_expr;
|
||||
auto old_value = vi.m_value;
|
||||
if (old_value == new_value)
|
||||
return;
|
||||
verbose_stream() << mk_bounded_pp(e, m) << " := " << new_value << "\n";
|
||||
for (auto const& [coeff, bv] : vi.m_bool_vars) {
|
||||
auto& ineq = *atom(bv);
|
||||
bool old_sign = sign(bv);
|
||||
|
|
@ -354,7 +357,8 @@ namespace sls {
|
|||
auto const& ad = m_adds[idx];
|
||||
ctx.new_value_eh(m_vars[ad.m_var].m_expr);
|
||||
}
|
||||
expr* e = vi.m_expr;
|
||||
|
||||
SASSERT(!m.is_value(e));
|
||||
ctx.new_value_eh(e);
|
||||
}
|
||||
|
||||
|
|
@ -374,7 +378,7 @@ namespace sls {
|
|||
template<>
|
||||
bool arith_base<checked_int64<true>>::is_num(expr* e, checked_int64<true>& i) {
|
||||
rational r;
|
||||
if (a.is_numeral(e, r)) {
|
||||
if (a.is_extended_numeral(e, r)) {
|
||||
if (!r.is_int64())
|
||||
throw overflow_exception();
|
||||
i = r.get_int64();
|
||||
|
|
@ -385,7 +389,7 @@ namespace sls {
|
|||
|
||||
template<>
|
||||
bool arith_base<rational>::is_num(expr* e, rational& i) {
|
||||
return a.is_numeral(e, i);
|
||||
return a.is_extended_numeral(e, i);
|
||||
}
|
||||
|
||||
template<typename num_t>
|
||||
|
|
@ -431,7 +435,7 @@ namespace sls {
|
|||
unsigned_vector m;
|
||||
num_t c = coeff;
|
||||
for (expr* arg : *to_app(e))
|
||||
if (is_num(x, i))
|
||||
if (is_num(arg, i))
|
||||
c *= i;
|
||||
else
|
||||
m.push_back(mk_term(arg));
|
||||
|
|
@ -620,16 +624,14 @@ namespace sls {
|
|||
}
|
||||
|
||||
template<typename num_t>
|
||||
void arith_base<num_t>::propagate_literal(sat::literal lit) {
|
||||
TRACE("sls", tout << "repair is-true: " << ctx.is_true(lit) << " lit: " << lit << "\n");
|
||||
void arith_base<num_t>::propagate_literal(sat::literal lit) {
|
||||
if (!ctx.is_true(lit))
|
||||
return;
|
||||
auto const* ineq = atom(lit.var());
|
||||
if (!ineq)
|
||||
return;
|
||||
TRACE("sls", tout << "repair lit: " << lit << " ineq-is-true: " << ineq->is_true() << "\n");
|
||||
return;
|
||||
if (ineq->is_true() != lit.sign())
|
||||
return;
|
||||
return;
|
||||
repair(lit, *ineq);
|
||||
}
|
||||
|
||||
|
|
@ -750,6 +752,9 @@ namespace sls {
|
|||
auto const& coeffs = ad.m_args;
|
||||
num_t sum(ad.m_coeff);
|
||||
num_t val = value(v);
|
||||
|
||||
verbose_stream() << mk_bounded_pp(m_vars[v].m_expr, m) << " := " << value(v) << "\n";
|
||||
|
||||
for (auto const& [c, w] : coeffs)
|
||||
sum += c * value(w);
|
||||
if (val == sum)
|
||||
|
|
@ -771,13 +776,14 @@ namespace sls {
|
|||
auto const& [v, coeff, monomial] = md;
|
||||
num_t product(coeff);
|
||||
num_t val = value(v);
|
||||
num_t new_value;
|
||||
for (auto v : monomial)
|
||||
product *= value(v);
|
||||
if (product == val)
|
||||
return;
|
||||
if (rand() % 20 == 0) {
|
||||
update(v, product);
|
||||
}
|
||||
verbose_stream() << "repair mul " << mk_bounded_pp(m_vars[v].m_expr, m) << " := " << val << "(" << product << ")\n";
|
||||
if (rand() % 20 == 0)
|
||||
update(v, product);
|
||||
else if (val == 0) {
|
||||
auto v = monomial[ctx.rand(monomial.size())];
|
||||
num_t zero(0);
|
||||
|
|
@ -801,28 +807,30 @@ namespace sls {
|
|||
// value1(v) * product / value(v) = val
|
||||
// value1(v) = value(v) * val / product
|
||||
auto w = monomial[ctx.rand(monomial.size())];
|
||||
auto old_value = value(w);
|
||||
num_t new_value;
|
||||
if (m_vars[w].m_sort == var_sort::REAL)
|
||||
new_value = old_value * val / product;
|
||||
else
|
||||
new_value = divide(w, old_value * val, product);
|
||||
auto old_value = value(w);
|
||||
new_value = divide(w, old_value * val, product);
|
||||
update(w, new_value);
|
||||
}
|
||||
else {
|
||||
product = coeff;
|
||||
auto w = monomial[ctx.rand(monomial.size())];
|
||||
num_t prod(coeff);
|
||||
for (auto v : monomial) {
|
||||
num_t new_value{ 1 };
|
||||
if (v == w)
|
||||
continue;
|
||||
num_t new_value(1);
|
||||
if (rand() % 2 == 0)
|
||||
new_value = -1;
|
||||
product *= new_value;
|
||||
prod *= new_value;
|
||||
update(v, new_value);
|
||||
}
|
||||
auto v = monomial[ctx.rand(monomial.size())];
|
||||
if ((product < 0 && 0 < val) || (val < 0 && 0 < product))
|
||||
update(v, -val * value(v));
|
||||
|
||||
verbose_stream() << "select random " << coeff << " " << val << " v" << w << "\n";
|
||||
new_value = divide(w, val * value(w), coeff);
|
||||
|
||||
if ((product < 0 && 0 < new_value) || (new_value < 0 && 0 < product))
|
||||
update(w, -new_value);
|
||||
else
|
||||
update(v, val * value(v));
|
||||
update(w, new_value);
|
||||
}
|
||||
}
|
||||
|
||||
|
|
@ -1076,6 +1084,19 @@ namespace sls {
|
|||
break;
|
||||
}
|
||||
}
|
||||
if (sat)
|
||||
continue;
|
||||
verbose_stream() << clause << "\n";
|
||||
for (auto lit : clause.m_clause) {
|
||||
verbose_stream() << lit << " (" << ctx.is_true(lit) << ") ";
|
||||
auto ineq = atom(lit.var());
|
||||
if (!ineq)
|
||||
continue;
|
||||
verbose_stream() << *ineq << "\n";
|
||||
for (auto const& [coeff, v] : ineq->m_args)
|
||||
verbose_stream() << coeff << " " << v << " " << mk_bounded_pp(m_vars[v].m_expr, m) << " := " << value(v) << "\n";
|
||||
}
|
||||
exit(0);
|
||||
if (!sat)
|
||||
return false;
|
||||
}
|
||||
|
|
|
|||
|
|
@ -21,34 +21,35 @@ Author:
|
|||
|
||||
namespace sls {
|
||||
|
||||
#define WITH_FALLBACK(_fn_) \
|
||||
if (!m_arith) { \
|
||||
try {\
|
||||
return m_arith64->_fn_;\
|
||||
}\
|
||||
catch (overflow_exception&) {\
|
||||
init_backup();\
|
||||
}\
|
||||
}\
|
||||
return m_arith->_fn_; \
|
||||
|
||||
arith_plugin::arith_plugin(context& ctx) :
|
||||
plugin(ctx), m_shared(ctx.get_manager()) {
|
||||
m_arith64 = alloc(arith_base<checked_int64<true>>, ctx);
|
||||
m_fid = m_arith64->fid();
|
||||
init_backup();
|
||||
}
|
||||
|
||||
void arith_plugin::init_backup() {
|
||||
m_arith = alloc(arith_base<rational>, ctx);
|
||||
m_arith->initialize();
|
||||
}
|
||||
|
||||
void arith_plugin::register_term(expr* e) {
|
||||
if (!m_arith) {
|
||||
try {
|
||||
m_arith64->register_term(e);
|
||||
return;
|
||||
}
|
||||
catch (overflow_exception&) {
|
||||
init_backup();
|
||||
}
|
||||
}
|
||||
m_arith->register_term(e);
|
||||
WITH_FALLBACK(register_term(e));
|
||||
}
|
||||
|
||||
expr_ref arith_plugin::get_value(expr* e) {
|
||||
if (!m_arith) {
|
||||
try {
|
||||
return m_arith64->get_value(e);
|
||||
}
|
||||
catch (overflow_exception&) {
|
||||
init_backup();
|
||||
}
|
||||
}
|
||||
return m_arith->get_value(e);
|
||||
WITH_FALLBACK(get_value(e));
|
||||
}
|
||||
|
||||
void arith_plugin::initialize() {
|
||||
|
|
@ -59,28 +60,11 @@ namespace sls {
|
|||
}
|
||||
|
||||
void arith_plugin::propagate_literal(sat::literal lit) {
|
||||
if (!m_arith) {
|
||||
try {
|
||||
m_arith64->propagate_literal(lit);
|
||||
return;
|
||||
}
|
||||
catch (overflow_exception&) {
|
||||
init_backup();
|
||||
}
|
||||
}
|
||||
m_arith->propagate_literal(lit);
|
||||
WITH_FALLBACK(propagate_literal(lit));
|
||||
}
|
||||
|
||||
bool arith_plugin::propagate() {
|
||||
if (!m_arith) {
|
||||
try {
|
||||
return m_arith64->propagate();
|
||||
}
|
||||
catch (overflow_exception&) {
|
||||
init_backup();
|
||||
}
|
||||
}
|
||||
return m_arith->propagate();
|
||||
WITH_FALLBACK(propagate());
|
||||
}
|
||||
|
||||
bool arith_plugin::is_sat() {
|
||||
|
|
@ -119,29 +103,14 @@ namespace sls {
|
|||
}
|
||||
|
||||
void arith_plugin::repair_down(app* e) {
|
||||
if (m_arith)
|
||||
m_arith->repair_down(e);
|
||||
else
|
||||
m_arith64->repair_down(e);
|
||||
WITH_FALLBACK(repair_down(e));
|
||||
}
|
||||
|
||||
void arith_plugin::repair_up(app* e) {
|
||||
if (m_arith)
|
||||
m_arith->repair_up(e);
|
||||
else
|
||||
m_arith64->repair_up(e);
|
||||
WITH_FALLBACK(repair_up(e));
|
||||
}
|
||||
|
||||
void arith_plugin::set_value(expr* e, expr* v) {
|
||||
if (!m_arith) {
|
||||
try {
|
||||
m_arith64->set_value(e, v);
|
||||
return;
|
||||
}
|
||||
catch (overflow_exception&) {
|
||||
init_backup();
|
||||
}
|
||||
}
|
||||
m_arith->set_value(e, v);
|
||||
WITH_FALLBACK(set_value(e, v));
|
||||
}
|
||||
}
|
||||
|
|
|
|||
|
|
@ -28,11 +28,7 @@ namespace sls {
|
|||
|
||||
void init_backup();
|
||||
public:
|
||||
arith_plugin(context& ctx) :
|
||||
plugin(ctx), m_shared(ctx.get_manager()) {
|
||||
m_arith64 = alloc(arith_base<checked_int64<true>>,ctx);
|
||||
m_fid = m_arith64->fid();
|
||||
}
|
||||
arith_plugin(context& ctx);
|
||||
~arith_plugin() override {}
|
||||
void register_term(expr* e) override;
|
||||
expr_ref get_value(expr* e) override;
|
||||
|
|
|
|||
|
|
@ -17,6 +17,8 @@ Author:
|
|||
|
||||
#include "ast/sls/sls_basic_plugin.h"
|
||||
#include "ast/ast_ll_pp.h"
|
||||
#include "ast/ast_pp.h"
|
||||
#include "ast/ast_util.h"
|
||||
|
||||
namespace sls {
|
||||
|
||||
|
|
@ -24,50 +26,76 @@ namespace sls {
|
|||
return expr_ref(m.mk_bool_val(bval0(e)), m);
|
||||
}
|
||||
|
||||
bool basic_plugin::is_basic(expr* e) const {
|
||||
if (!e || !is_app(e))
|
||||
return false;
|
||||
if (to_app(e)->get_family_id() != basic_family_id)
|
||||
return false;
|
||||
if (!m.is_bool(e))
|
||||
return false;
|
||||
expr* x, * y;
|
||||
if (m.is_eq(e, x, y) && !m.is_bool(x))
|
||||
return false;
|
||||
if (m.is_distinct(e) && !m.is_bool(to_app(e)->get_arg(0)))
|
||||
return false;
|
||||
return true;
|
||||
}
|
||||
|
||||
void basic_plugin::propagate_literal(sat::literal lit) {
|
||||
auto a = ctx.atom(lit.var());
|
||||
if (!a || !is_app(a))
|
||||
return;
|
||||
if (to_app(a)->get_family_id() != basic_family_id)
|
||||
if (!is_basic(a))
|
||||
return;
|
||||
if (bval1(to_app(a)) != bval0(to_app(a)))
|
||||
ctx.new_value_eh(a);
|
||||
}
|
||||
|
||||
void basic_plugin::register_term(expr* e) {
|
||||
if (is_app(e) && m.is_bool(e) && to_app(e)->get_family_id() == basic_family_id)
|
||||
if (is_basic(e))
|
||||
m_values.setx(e->get_id(), bval1(to_app(e)), false);
|
||||
}
|
||||
|
||||
void basic_plugin::initialize() {
|
||||
}
|
||||
|
||||
bool basic_plugin::propagate() {
|
||||
for (auto t : ctx.subterms())
|
||||
if (is_basic(t) && !m.is_not(t) &&
|
||||
bval0(t) != bval1(to_app(t))) {
|
||||
add_clause(to_app(t));
|
||||
return true;
|
||||
}
|
||||
|
||||
return false;
|
||||
}
|
||||
|
||||
bool basic_plugin::is_sat() {
|
||||
for (auto t : ctx.subterms())
|
||||
if (is_app(t) &&
|
||||
m.is_bool(t) &&
|
||||
to_app(t)->get_family_id() == basic_family_id &&
|
||||
bval0(t) != bval1(to_app(t)))
|
||||
return false;
|
||||
if (is_basic(t) && !m.is_not(t) &&
|
||||
bval0(t) != bval1(to_app(t))) {
|
||||
verbose_stream() << mk_bounded_pp(t, m) << " := " << (bval0(t) ? "T" : "F") << " eval: " << (bval1(to_app(t)) ? "T" : "F") << "\n";
|
||||
return false;
|
||||
}
|
||||
return true;
|
||||
}
|
||||
|
||||
|
||||
std::ostream& basic_plugin::display(std::ostream& out) const {
|
||||
for (auto t : ctx.subterms())
|
||||
if (is_app(t) && m.is_bool(t) && to_app(t)->get_family_id() == basic_family_id)
|
||||
if (is_basic(t))
|
||||
out << mk_bounded_pp(t, m) << " := " << (bval0(t)?"T":"F") << " eval: " << (bval1(to_app(t))?"T":"F") << "\n";
|
||||
return out;
|
||||
}
|
||||
|
||||
void basic_plugin::set_value(expr* e, expr* v) {
|
||||
if (!m.is_bool(e))
|
||||
if (!is_basic(e))
|
||||
return;
|
||||
SASSERT(m.is_true(v) || m.is_false(v));
|
||||
set_value(e, m.is_true(v));
|
||||
}
|
||||
|
||||
bool basic_plugin::bval1(app* e) const {
|
||||
if (m.is_not(e))
|
||||
return bval1(to_app(e->get_arg(0)));
|
||||
SASSERT(m.is_bool(e));
|
||||
SASSERT(e->get_family_id() == basic_family_id);
|
||||
|
||||
|
|
@ -103,6 +131,7 @@ namespace sls {
|
|||
auto b = e->get_arg(1);
|
||||
if (m.is_bool(a))
|
||||
return bval0(a) == bval0(b);
|
||||
verbose_stream() << mk_bounded_pp(e, m) << " " << ctx.get_value(a) << " " << ctx.get_value(b) << "\n";
|
||||
return ctx.get_value(a) == ctx.get_value(b);
|
||||
}
|
||||
case OP_DISTINCT: {
|
||||
|
|
@ -123,11 +152,14 @@ namespace sls {
|
|||
|
||||
bool basic_plugin::bval0(expr* e) const {
|
||||
SASSERT(m.is_bool(e));
|
||||
bool b = true;
|
||||
while (m.is_not(e, e))
|
||||
b = !b;
|
||||
sat::bool_var v = ctx.atom2bool_var(e);
|
||||
if (v == sat::null_bool_var)
|
||||
return m_values.get(e->get_id(), false);
|
||||
return b == m_values.get(e->get_id(), false);
|
||||
else
|
||||
return ctx.is_true(v);
|
||||
return b == ctx.is_true(v);
|
||||
}
|
||||
|
||||
bool basic_plugin::try_repair(app* e, unsigned i) {
|
||||
|
|
@ -158,6 +190,56 @@ namespace sls {
|
|||
}
|
||||
}
|
||||
|
||||
void basic_plugin::add_clause(app* e) {
|
||||
expr_ref_vector es(m);
|
||||
expr_ref fml(m);
|
||||
expr* x, *y;
|
||||
switch (e->get_decl_kind()) {
|
||||
case OP_AND:
|
||||
for (expr* arg : *e) {
|
||||
ctx.add_constraint(m.mk_or(m.mk_not(e), arg));
|
||||
es.push_back(mk_not(m, arg));
|
||||
}
|
||||
es.push_back(e);
|
||||
ctx.add_constraint(m.mk_or(es));
|
||||
break;
|
||||
case OP_OR:
|
||||
for (expr* arg : *e) {
|
||||
ctx.add_constraint(m.mk_or(mk_not(m, arg), e));
|
||||
es.push_back(arg);
|
||||
}
|
||||
es.push_back(m.mk_not(e));
|
||||
ctx.add_constraint(m.mk_or(es));
|
||||
break;
|
||||
case OP_NOT:
|
||||
break;
|
||||
case OP_FALSE:
|
||||
break;
|
||||
case OP_TRUE:
|
||||
break;
|
||||
case OP_EQ:
|
||||
VERIFY(m.is_eq(e, x, y));
|
||||
ctx.add_constraint(m.mk_or(m.mk_not(e), mk_not(m, x), y));
|
||||
ctx.add_constraint(m.mk_or(m.mk_not(e), mk_not(m, y), x));
|
||||
ctx.add_constraint(m.mk_or(e, y, x));
|
||||
ctx.add_constraint(m.mk_or(e, mk_not(m, x), mk_not(m, y)));
|
||||
break;
|
||||
case OP_IMPLIES:
|
||||
NOT_IMPLEMENTED_YET();
|
||||
case OP_XOR:
|
||||
NOT_IMPLEMENTED_YET();
|
||||
case OP_ITE:
|
||||
NOT_IMPLEMENTED_YET();
|
||||
case OP_DISTINCT:
|
||||
NOT_IMPLEMENTED_YET();
|
||||
default:
|
||||
UNREACHABLE();
|
||||
break;
|
||||
}
|
||||
|
||||
}
|
||||
|
||||
|
||||
bool basic_plugin::try_repair_and_or(app* e, unsigned i) {
|
||||
auto b = bval0(e);
|
||||
if ((b && m.is_and(e)) || (!b && m.is_or(e))) {
|
||||
|
|
@ -245,7 +327,7 @@ namespace sls {
|
|||
}
|
||||
|
||||
void basic_plugin::repair_up(app* e) {
|
||||
if (!m.is_bool(e) || e->get_family_id() != basic_family_id)
|
||||
if (!is_basic(e))
|
||||
return;
|
||||
auto b = bval1(e);
|
||||
if (bval0(e) == b)
|
||||
|
|
@ -256,7 +338,7 @@ namespace sls {
|
|||
void basic_plugin::repair_down(app* e) {
|
||||
SASSERT(m.is_bool(e));
|
||||
unsigned n = e->get_num_args();
|
||||
if (n == 0 || e->get_family_id() != m.get_basic_family_id())
|
||||
if (n == 0 || !is_basic(e))
|
||||
return;
|
||||
|
||||
if (bval0(e) == bval1(e))
|
||||
|
|
|
|||
|
|
@ -19,7 +19,8 @@ namespace sls {
|
|||
class basic_plugin : public plugin {
|
||||
bool_vector m_values;
|
||||
bool m_initialized = false;
|
||||
|
||||
|
||||
bool is_basic(expr* e) const;
|
||||
bool bval1(app* e) const;
|
||||
bool bval0(expr* e) const;
|
||||
bool try_repair(app* e, unsigned i);
|
||||
|
|
@ -32,6 +33,8 @@ namespace sls {
|
|||
bool try_repair_distinct(app* e, unsigned i);
|
||||
bool set_value(expr* e, bool b);
|
||||
|
||||
void add_clause(app* e);
|
||||
|
||||
public:
|
||||
basic_plugin(context& ctx) :
|
||||
plugin(ctx) {
|
||||
|
|
@ -42,7 +45,7 @@ namespace sls {
|
|||
expr_ref get_value(expr* e) override;
|
||||
void initialize() override;
|
||||
void propagate_literal(sat::literal lit) override;
|
||||
bool propagate() override { return false; }
|
||||
bool propagate() override;
|
||||
void repair_down(app* e) override;
|
||||
void repair_up(app* e) override;
|
||||
bool is_sat() override;
|
||||
|
|
|
|||
|
|
@ -59,15 +59,19 @@ namespace sls {
|
|||
// Use timestamps to make it incremental.
|
||||
//
|
||||
init();
|
||||
verbose_stream() << "check " << unsat().size() << "\n";
|
||||
while (unsat().empty()) {
|
||||
|
||||
propagate_boolean_assignment();
|
||||
|
||||
verbose_stream() << "propagate " << unsat().size() << " " << m_new_constraint << "\n";
|
||||
// display(verbose_stream());
|
||||
|
||||
if (m_new_constraint || !unsat().empty())
|
||||
return l_undef;
|
||||
|
||||
verbose_stream() << unsat().size() << " " << m_new_constraint << "\n";
|
||||
|
||||
if (all_of(m_plugins, [&](auto* p) { return !p || p->is_sat(); })) {
|
||||
model_ref mdl = alloc(model, m);
|
||||
for (expr* e : subterms())
|
||||
|
|
@ -97,8 +101,8 @@ namespace sls {
|
|||
while (!m_new_constraint && (!m_repair_up.empty() || !m_repair_down.empty())) {
|
||||
while (!m_repair_down.empty() && !m_new_constraint) {
|
||||
auto id = m_repair_down.erase_min();
|
||||
expr* e = term(id);
|
||||
// verbose_stream() << "repair down " << mk_bounded_pp(e, m) << "\n";
|
||||
expr* e = term(id);
|
||||
TRACE("sls", tout << "repair down " << mk_bounded_pp(e, m) << "\n");
|
||||
if (is_app(e)) {
|
||||
auto p = m_plugins.get(to_app(e)->get_family_id(), nullptr);
|
||||
if (p)
|
||||
|
|
@ -108,7 +112,7 @@ namespace sls {
|
|||
while (!m_repair_up.empty() && !m_new_constraint) {
|
||||
auto id = m_repair_up.erase_min();
|
||||
expr* e = term(id);
|
||||
// verbose_stream() << "repair up " << mk_bounded_pp(e, m) << "\n";
|
||||
TRACE("sls", tout << "repair up " << mk_bounded_pp(e, m) << "\n");
|
||||
if (is_app(e)) {
|
||||
auto p = m_plugins.get(to_app(e)->get_family_id(), nullptr);
|
||||
if (p)
|
||||
|
|
|
|||
|
|
@ -108,32 +108,73 @@ namespace sls {
|
|||
// send clauses to ddfw
|
||||
// send expression mapping to m_solver_ctx
|
||||
|
||||
sat::literal_vector clause;
|
||||
for (auto f : m_assertions) {
|
||||
if (m.is_or(f)) {
|
||||
clause.reset();
|
||||
for (auto arg : *to_app(f))
|
||||
clause.push_back(mk_literal(arg));
|
||||
m_solver_ctx->add_clause(clause.size(), clause.data());
|
||||
}
|
||||
else {
|
||||
sat::literal lit = mk_literal(f);
|
||||
m_solver_ctx->add_clause(1, &lit);
|
||||
}
|
||||
}
|
||||
for (auto f : m_assertions)
|
||||
add_clause(f);
|
||||
|
||||
IF_VERBOSE(10, m_solver_ctx->display(verbose_stream()));
|
||||
return m_ddfw.check(0, nullptr);
|
||||
}
|
||||
|
||||
sat::literal smt_solver::mk_literal(expr* e) {
|
||||
bool neg = m.is_not(e, e);
|
||||
sat::bool_var v;
|
||||
if (!m_expr2var.find(e, v)) {
|
||||
v = m_expr2var.size();
|
||||
m_expr2var.insert(e, v);
|
||||
m_solver_ctx->register_atom(v, e);
|
||||
void smt_solver::add_clause(expr* f) {
|
||||
sat::literal_vector clause;
|
||||
if (m.is_or(f)) {
|
||||
clause.reset();
|
||||
for (auto arg : *to_app(f))
|
||||
clause.push_back(mk_literal(arg));
|
||||
m_solver_ctx->add_clause(clause.size(), clause.data());
|
||||
}
|
||||
return sat::literal(v, neg);
|
||||
else if (m.is_and(f)) {
|
||||
for (auto arg : *to_app(f))
|
||||
add_clause(arg);
|
||||
}
|
||||
else {
|
||||
sat::literal lit = mk_literal(f);
|
||||
m_solver_ctx->add_clause(1, &lit);
|
||||
}
|
||||
}
|
||||
|
||||
sat::literal smt_solver::mk_literal(expr* e) {
|
||||
sat::literal lit;
|
||||
bool neg = false;
|
||||
while (m.is_not(e,e))
|
||||
neg = !neg;
|
||||
if (m_expr2lit.find(e, lit))
|
||||
return neg ? ~lit : lit;
|
||||
sat::literal_vector clause;
|
||||
if (m.is_and(e)) {
|
||||
lit = mk_literal();
|
||||
for (expr* arg : *to_app(e)) {
|
||||
auto lit2 = mk_literal(arg);
|
||||
clause.push_back(~lit2);
|
||||
sat::literal lits[2] = { ~lit, lit2 };
|
||||
m_solver_ctx->add_clause(2, lits);
|
||||
}
|
||||
clause.push_back(lit);
|
||||
m_solver_ctx->add_clause(clause.size(), clause.data());
|
||||
}
|
||||
else if (m.is_or(e)) {
|
||||
lit = mk_literal();
|
||||
for (expr* arg : *to_app(e)) {
|
||||
auto lit2 = mk_literal(arg);
|
||||
clause.push_back(lit2);
|
||||
sat::literal lits[2] = { lit, ~lit2 };
|
||||
m_solver_ctx->add_clause(2, lits);
|
||||
}
|
||||
clause.push_back(~lit);
|
||||
m_solver_ctx->add_clause(clause.size(), clause.data());
|
||||
}
|
||||
else {
|
||||
sat::bool_var v = m_num_vars++;
|
||||
lit = sat::literal(v, false);
|
||||
m_solver_ctx->register_atom(lit.var(), e);
|
||||
}
|
||||
m_expr2lit.insert(e, lit);
|
||||
return neg ? ~lit : lit;
|
||||
}
|
||||
|
||||
sat::literal smt_solver::mk_literal() {
|
||||
sat::bool_var v = m_num_vars++;
|
||||
return sat::literal(v, false);
|
||||
}
|
||||
|
||||
model_ref smt_solver::get_model() {
|
||||
|
|
|
|||
|
|
@ -29,9 +29,12 @@ namespace sls {
|
|||
solver_ctx* m_solver_ctx = nullptr;
|
||||
expr_ref_vector m_assertions;
|
||||
statistics m_st;
|
||||
obj_map<expr, sat::bool_var> m_expr2var;
|
||||
obj_map<expr, sat::literal> m_expr2lit;
|
||||
unsigned m_num_vars = 0;
|
||||
|
||||
sat::literal mk_literal(expr* e);
|
||||
sat::literal mk_literal();
|
||||
void add_clause(expr* f);
|
||||
public:
|
||||
smt_solver(ast_manager& m, params_ref const& p);
|
||||
~smt_solver();
|
||||
|
|
|
|||
|
|
@ -32,6 +32,10 @@ namespace sat {
|
|||
void add(literal lit) { ++m_num_trues; m_trues += lit.index(); }
|
||||
void del(literal lit) { SASSERT(m_num_trues > 0); --m_num_trues; m_trues -= lit.index(); }
|
||||
};
|
||||
|
||||
inline std::ostream& operator<<(std::ostream& out, clause_info const& ci) {
|
||||
return out << ci.m_clause << " w: " << ci.m_weight << " nt: " << ci.m_num_trues;
|
||||
}
|
||||
};
|
||||
|
||||
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue