mirror of
https://github.com/Z3Prover/z3
synced 2025-11-04 05:19:11 +00:00
refactor basic plugin and clause generation
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner
parent
438389771d
commit
98f4b5103e
8 changed files with 248 additions and 466 deletions
|
|
@ -604,10 +604,9 @@ namespace sls {
|
|||
bool arith_base<num_t>::update(var_t v, num_t const& new_value) {
|
||||
auto& vi = m_vars[v];
|
||||
expr* e = vi.m_expr;
|
||||
SASSERT(!m.is_value(e));
|
||||
auto old_value = vi.m_value;
|
||||
if (old_value == new_value)
|
||||
return true;
|
||||
return true;
|
||||
if (!vi.in_range(new_value))
|
||||
return false;
|
||||
if (!in_bounds(v, new_value) && in_bounds(v, old_value))
|
||||
|
|
|
|||
|
|
@ -29,246 +29,85 @@ namespace sls {
|
|||
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;
|
||||
if (m.is_not(e, x))
|
||||
return is_basic(x);
|
||||
return true;
|
||||
if (m.is_ite(e) && !m.is_bool(e))
|
||||
return true;
|
||||
if (m.is_xor(e) && to_app(e)->get_num_args() != 2)
|
||||
return true;
|
||||
if (m.is_distinct(e))
|
||||
return true;
|
||||
return false;
|
||||
}
|
||||
|
||||
void basic_plugin::propagate_literal(sat::literal lit) {
|
||||
auto a = ctx.atom(lit.var());
|
||||
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_basic(e) && m.is_bool(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_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_basic(t))
|
||||
out << mk_bounded_pp(t, m) << " := " << (bval0(t)?"T":"F") << " eval: " << (bval1(to_app(t))?"T":"F") << "\n";
|
||||
return out;
|
||||
}
|
||||
|
||||
bool basic_plugin::set_value(expr* e, expr* v) {
|
||||
if (!is_basic(e))
|
||||
if (!m.is_bool(e))
|
||||
return false;
|
||||
SASSERT(m.is_true(v) || m.is_false(v));
|
||||
return set_value(e, m.is_true(v));
|
||||
}
|
||||
|
||||
bool basic_plugin::bval1(app* e) const {
|
||||
verbose_stream() << mk_bounded_pp(e, m) << "\n";
|
||||
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);
|
||||
expr_ref basic_plugin::eval_ite(app* e) {
|
||||
expr* c, * th, * el;
|
||||
VERIFY(m.is_ite(e, c, th, el));
|
||||
if (bval0(c))
|
||||
return ctx.get_value(th);
|
||||
else
|
||||
return ctx.get_value(el);
|
||||
}
|
||||
|
||||
auto id = e->get_id();
|
||||
switch (e->get_decl_kind()) {
|
||||
case OP_TRUE:
|
||||
return true;
|
||||
case OP_FALSE:
|
||||
return false;
|
||||
case OP_AND:
|
||||
return all_of(*to_app(e), [&](expr* arg) { return bval0(arg); });
|
||||
case OP_OR:
|
||||
return any_of(*to_app(e), [&](expr* arg) { return bval0(arg); });
|
||||
case OP_NOT:
|
||||
return !bval0(e->get_arg(0));
|
||||
case OP_XOR: {
|
||||
bool r = false;
|
||||
for (auto* arg : *to_app(e))
|
||||
r ^= bval0(arg);
|
||||
return r;
|
||||
expr_ref basic_plugin::eval_distinct(app* e) {
|
||||
for (unsigned i = 0; i < e->get_num_args(); ++i) {
|
||||
for (unsigned j = i + 1; j < e->get_num_args(); ++j) {
|
||||
if (bval0(e->get_arg(i)) == bval0(e->get_arg(j)))
|
||||
return expr_ref(m.mk_false(), m);
|
||||
}
|
||||
}
|
||||
case OP_IMPLIES: {
|
||||
auto a = e->get_arg(0);
|
||||
auto b = e->get_arg(1);
|
||||
return !bval0(a) || bval0(b);
|
||||
}
|
||||
case OP_ITE: {
|
||||
auto c = bval0(e->get_arg(0));
|
||||
return bval0(c ? e->get_arg(1) : e->get_arg(2));
|
||||
}
|
||||
case OP_EQ: {
|
||||
auto a = e->get_arg(0);
|
||||
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: {
|
||||
for (unsigned i = 0; i < e->get_num_args(); ++i)
|
||||
for (unsigned j = i + 1; j < e->get_num_args(); ++j)
|
||||
if (ctx.get_value(e->get_arg(i)) == ctx.get_value(e->get_arg(j)))
|
||||
return false;
|
||||
return true;
|
||||
}
|
||||
default:
|
||||
verbose_stream() << mk_bounded_pp(e, m) << "\n";
|
||||
UNREACHABLE();
|
||||
break;
|
||||
}
|
||||
UNREACHABLE();
|
||||
return false;
|
||||
return expr_ref(m.mk_true(), m);
|
||||
}
|
||||
|
||||
expr_ref basic_plugin::eval_xor(app* e) {
|
||||
bool b = false;
|
||||
for (expr* arg : *e)
|
||||
b ^= bval0(arg);
|
||||
return expr_ref(m.mk_bool_val(b), m);
|
||||
}
|
||||
|
||||
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 b == m_values.get(e->get_id(), false);
|
||||
else
|
||||
return b == ctx.is_true(v);
|
||||
SASSERT(m.is_bool(e));
|
||||
return ctx.is_true(ctx.mk_literal(e));
|
||||
}
|
||||
|
||||
bool basic_plugin::try_repair(app* e, unsigned i) {
|
||||
switch (e->get_decl_kind()) {
|
||||
case OP_AND:
|
||||
return try_repair_and_or(e, i);
|
||||
case OP_OR:
|
||||
return try_repair_and_or(e, i);
|
||||
case OP_NOT:
|
||||
return try_repair_not(e);
|
||||
case OP_FALSE:
|
||||
return false;
|
||||
case OP_TRUE:
|
||||
return false;
|
||||
case OP_EQ:
|
||||
return try_repair_eq(e, i);
|
||||
case OP_IMPLIES:
|
||||
return try_repair_implies(e, i);
|
||||
case OP_XOR:
|
||||
return try_repair_xor(e, i);
|
||||
case OP_ITE:
|
||||
return try_repair_ite(e, i);
|
||||
case OP_DISTINCT:
|
||||
return try_repair_distinct(e, i);
|
||||
default:
|
||||
UNREACHABLE();
|
||||
return false;
|
||||
}
|
||||
}
|
||||
|
||||
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))) {
|
||||
for (auto arg : *e)
|
||||
if (!set_value(arg, b))
|
||||
return false;
|
||||
default:
|
||||
return true;
|
||||
}
|
||||
auto child = e->get_arg(i);
|
||||
if (b == bval0(child))
|
||||
return false;
|
||||
return set_value(child, b);
|
||||
}
|
||||
|
||||
bool basic_plugin::try_repair_not(app* e) {
|
||||
auto child = e->get_arg(0);
|
||||
return set_value(child, !bval0(e));
|
||||
}
|
||||
|
||||
bool basic_plugin::try_repair_eq(app* e, unsigned i) {
|
||||
auto child = e->get_arg(i);
|
||||
auto sibling = e->get_arg(1 - i);
|
||||
if (!m.is_bool(child))
|
||||
return false;
|
||||
return set_value(child, bval0(e) == bval0(sibling));
|
||||
}
|
||||
}
|
||||
|
||||
bool basic_plugin::try_repair_xor(app* e, unsigned i) {
|
||||
|
|
@ -283,12 +122,7 @@ namespace sls {
|
|||
|
||||
bool basic_plugin::try_repair_ite(app* e, unsigned i) {
|
||||
if (m.is_bool(e))
|
||||
return try_repair_ite_bool(e, i);
|
||||
else
|
||||
return try_repair_ite_nonbool(e, i);
|
||||
}
|
||||
|
||||
bool basic_plugin::try_repair_ite_nonbool(app* e, unsigned i) {
|
||||
return true;
|
||||
auto child = e->get_arg(i);
|
||||
auto cond = e->get_arg(0);
|
||||
bool c = bval0(cond);
|
||||
|
|
@ -307,85 +141,45 @@ namespace sls {
|
|||
}
|
||||
if (c != (i == 1))
|
||||
return false;
|
||||
return ctx.set_value(child, ctx.get_value(e));
|
||||
}
|
||||
|
||||
bool basic_plugin::try_repair_ite_bool(app* e, unsigned i) {
|
||||
auto child = e->get_arg(i);
|
||||
auto cond = e->get_arg(0);
|
||||
bool c = bval0(cond);
|
||||
if (i == 0) {
|
||||
if (ctx.rand(2) == 0)
|
||||
return set_value(cond, true) && set_value(e->get_arg(1), bval0(e));
|
||||
else
|
||||
return set_value(cond, false) && set_value(e->get_arg(2), bval0(e));
|
||||
}
|
||||
|
||||
if (!set_value(child, bval0(e)))
|
||||
if (m.is_value(child))
|
||||
return false;
|
||||
return (c == (i == 1)) || set_value(cond, !c);
|
||||
}
|
||||
|
||||
bool basic_plugin::try_repair_implies(app* e, unsigned i) {
|
||||
auto child = e->get_arg(i);
|
||||
auto sibling = e->get_arg(1 - i);
|
||||
bool ev = bval0(e);
|
||||
bool av = bval0(child);
|
||||
bool bv = bval0(sibling);
|
||||
if (ev) {
|
||||
|
||||
if (i == 0 && (!av || bv))
|
||||
return true;
|
||||
if (i == 1 && (!bv || av))
|
||||
return true;
|
||||
if (i == 0) {
|
||||
return set_value(child, false);
|
||||
}
|
||||
if (i == 1) {
|
||||
return set_value(child, true);
|
||||
}
|
||||
return false;
|
||||
}
|
||||
if (i == 0 && av && !bv)
|
||||
return true;
|
||||
if (i == 1 && bv && !av)
|
||||
return true;
|
||||
if (i == 0)
|
||||
return set_value(child, true) && set_value(sibling, false);
|
||||
if (i == 1)
|
||||
return set_value(child, false) && set_value(sibling, true);
|
||||
return false;
|
||||
bool r = ctx.set_value(child, ctx.get_value(e));
|
||||
verbose_stream() << "repair-ite-down " << mk_bounded_pp(e, m) << " @ " << mk_bounded_pp(child, m) << " := " << ctx.get_value(e) << " success " << r << "\n";
|
||||
return r;
|
||||
}
|
||||
|
||||
void basic_plugin::repair_up(app* e) {
|
||||
expr* c, * th, * el;
|
||||
expr_ref val(m);
|
||||
if (!is_basic(e))
|
||||
return;
|
||||
auto b = bval1(e);
|
||||
if (bval0(e) == b)
|
||||
if (m.is_ite(e, c, th, el) && !m.is_bool(e))
|
||||
val = eval_ite(e);
|
||||
else if (m.is_xor(e))
|
||||
val = eval_xor(e);
|
||||
else if (m.is_distinct(e))
|
||||
val = eval_distinct(e);
|
||||
else
|
||||
return;
|
||||
set_value(e, b);
|
||||
verbose_stream() << "repair-up " << mk_bounded_pp(e, m) << " " << val << "\n";
|
||||
if (!ctx.set_value(e, val))
|
||||
ctx.new_value_eh(e);
|
||||
}
|
||||
|
||||
void basic_plugin::repair_literal(sat::literal lit) {
|
||||
auto a = ctx.atom(lit.var());
|
||||
if (!is_basic(a))
|
||||
return;
|
||||
if (bval1(to_app(a)) != bval0(to_app(a)))
|
||||
ctx.flip(lit.var());
|
||||
}
|
||||
|
||||
bool basic_plugin::repair_down(app* e) {
|
||||
SASSERT(m.is_bool(e));
|
||||
|
||||
unsigned n = e->get_num_args();
|
||||
bool basic_plugin::repair_down(app* e) {
|
||||
if (!is_basic(e))
|
||||
return false;
|
||||
if (n == 0)
|
||||
return true;
|
||||
if (m.is_xor(e) && eval_xor(e) == ctx.get_value(e))
|
||||
return true;
|
||||
|
||||
if (bval0(e) == bval1(e))
|
||||
if (m.is_ite(e) && eval_ite(e) == ctx.get_value(e))
|
||||
return true;
|
||||
if (m.is_distinct(e) && eval_distinct(e) == ctx.get_value(e))
|
||||
return true;
|
||||
verbose_stream() << "basic repair down " << mk_bounded_pp(e, m) << "\n";
|
||||
unsigned n = e->get_num_args();
|
||||
unsigned s = ctx.rand(n);
|
||||
for (unsigned i = 0; i < n; ++i) {
|
||||
auto j = (i + s) % n;
|
||||
|
|
@ -396,23 +190,14 @@ namespace sls {
|
|||
}
|
||||
|
||||
bool basic_plugin::try_repair_distinct(app* e, unsigned i) {
|
||||
NOT_IMPLEMENTED_YET();
|
||||
return false;
|
||||
}
|
||||
|
||||
bool basic_plugin::set_value(expr* e, bool b) {
|
||||
if (m.is_true(e) && !b)
|
||||
return false;
|
||||
if (m.is_false(e) && b)
|
||||
return false;
|
||||
sat::bool_var v = ctx.atom2bool_var(e);
|
||||
if (v == sat::null_bool_var) {
|
||||
if (m_values.get(e->get_id(), b) != b) {
|
||||
m_values.set(e->get_id(), b);
|
||||
ctx.new_value_eh(e);
|
||||
}
|
||||
}
|
||||
else if (ctx.is_true(v) != b) {
|
||||
ctx.flip(v);
|
||||
auto lit = ctx.mk_literal(e);
|
||||
if (ctx.is_true(lit) != b) {
|
||||
ctx.flip(lit.var());
|
||||
ctx.new_value_eh(e);
|
||||
}
|
||||
return true;
|
||||
|
|
|
|||
|
|
@ -17,25 +17,20 @@ Author:
|
|||
namespace sls {
|
||||
|
||||
class basic_plugin : public plugin {
|
||||
bool_vector m_values;
|
||||
bool m_initialized = false;
|
||||
expr_mark m_axiomatized;
|
||||
|
||||
bool is_basic(expr* e) const;
|
||||
bool bval1(app* e) const;
|
||||
bool bval0(expr* e) const;
|
||||
bool try_repair(app* e, unsigned i);
|
||||
bool try_repair_and_or(app* e, unsigned i);
|
||||
bool try_repair_not(app* e);
|
||||
bool try_repair_eq(app* e, unsigned i);
|
||||
bool try_repair_xor(app* e, unsigned i);
|
||||
bool try_repair_ite(app* e, unsigned i);
|
||||
bool try_repair_ite_nonbool(app* e, unsigned i);
|
||||
bool try_repair_ite_bool(app* e, unsigned i);
|
||||
bool try_repair_implies(app* e, unsigned i);
|
||||
bool try_repair_distinct(app* e, unsigned i);
|
||||
bool set_value(expr* e, bool b);
|
||||
|
||||
void add_clause(app* e);
|
||||
expr_ref eval_ite(app* e);
|
||||
expr_ref eval_distinct(app* e);
|
||||
expr_ref eval_xor(app* e);
|
||||
|
||||
public:
|
||||
basic_plugin(context& ctx) :
|
||||
|
|
|
|||
|
|
@ -21,6 +21,7 @@ Author:
|
|||
#include "ast/sls/sls_bv_plugin.h"
|
||||
#include "ast/sls/sls_basic_plugin.h"
|
||||
#include "ast/ast_ll_pp.h"
|
||||
#include "ast/ast_pp.h"
|
||||
|
||||
namespace sls {
|
||||
|
||||
|
|
@ -96,9 +97,9 @@ namespace sls {
|
|||
reinit_relevant();
|
||||
|
||||
for (sat::literal lit : root_literals()) {
|
||||
if (m_new_constraint)
|
||||
break;
|
||||
propagate_literal(lit);
|
||||
if (m_new_constraint)
|
||||
return;
|
||||
}
|
||||
|
||||
while (!m_new_constraint && m.inc() && (!m_repair_up.empty() || !m_repair_down.empty())) {
|
||||
|
|
@ -125,15 +126,20 @@ namespace sls {
|
|||
}
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
// propagate "final checks"
|
||||
bool propagated = true;
|
||||
while (propagated && !m_new_constraint) {
|
||||
propagated = false;
|
||||
for (auto p : m_plugins)
|
||||
propagated |= p && !m_new_constraint && p->propagate();
|
||||
}
|
||||
}
|
||||
|
||||
for (sat::bool_var v = 0; v < s.num_vars(); ++v) {
|
||||
if (m_new_constraint)
|
||||
return;
|
||||
|
||||
for (sat::bool_var v = 0; v < s.num_vars() && !m_new_constraint; ++v) {
|
||||
auto a = atom(v);
|
||||
if (!a)
|
||||
continue;
|
||||
|
|
@ -148,10 +154,8 @@ namespace sls {
|
|||
if (!is_app(e))
|
||||
return null_family_id;
|
||||
family_id fid = to_app(e)->get_family_id();
|
||||
if (m.is_eq(e) || m.is_distinct(e))
|
||||
if (m.is_eq(e))
|
||||
fid = to_app(e)->get_arg(0)->get_sort()->get_family_id();
|
||||
else if (m.is_ite(e))
|
||||
fid = to_app(e)->get_arg(1)->get_sort()->get_family_id();
|
||||
return fid;
|
||||
}
|
||||
|
||||
|
|
@ -191,7 +195,6 @@ namespace sls {
|
|||
return expr_ref(e, m);
|
||||
}
|
||||
|
||||
|
||||
bool context::set_value(expr * e, expr * v) {
|
||||
for (auto p : m_plugins)
|
||||
if (p && p->set_value(e, v))
|
||||
|
|
@ -215,34 +218,151 @@ namespace sls {
|
|||
return false;
|
||||
}
|
||||
|
||||
void context::add_constraint(expr* e) {
|
||||
expr_ref _e(e, m);
|
||||
sat::literal_vector lits;
|
||||
auto add_literal = [&](expr* e) {
|
||||
bool is_neg = m.is_not(e, e);
|
||||
auto v = mk_atom(e);
|
||||
lits.push_back(sat::literal(v, is_neg));
|
||||
};
|
||||
if (m.is_or(e))
|
||||
for (auto arg : *to_app(e))
|
||||
add_literal(arg);
|
||||
else
|
||||
add_literal(e);
|
||||
TRACE("sls", tout << "new clause " << lits << "\n");
|
||||
s.add_clause(lits.size(), lits.data());
|
||||
void context::add_constraint(expr* e) {
|
||||
add_clause(e);
|
||||
m_new_constraint = true;
|
||||
}
|
||||
|
||||
sat::bool_var context::mk_atom(expr* e) {
|
||||
auto v = m_atom2bool_var.get(e->get_id(), sat::null_bool_var);
|
||||
if (v == sat::null_bool_var) {
|
||||
v = s.add_var();
|
||||
register_atom(v, e);
|
||||
register_terms(e);
|
||||
void context::add_clause(expr* f) {
|
||||
expr_ref _e(f, m);
|
||||
verbose_stream() << "add constraint " << _e << "\n";
|
||||
expr* g, * h, * k;
|
||||
sat::literal_vector clause;
|
||||
if (m.is_not(f, g) && m.is_not(g, g)) {
|
||||
add_clause(g);
|
||||
return;
|
||||
}
|
||||
bool sign = m.is_not(f, f);
|
||||
if (!sign && m.is_or(f)) {
|
||||
clause.reset();
|
||||
for (auto arg : *to_app(f))
|
||||
clause.push_back(mk_literal(arg));
|
||||
s.add_clause(clause.size(), clause.data());
|
||||
}
|
||||
else if (!sign && m.is_and(f)) {
|
||||
for (auto arg : *to_app(f))
|
||||
add_clause(arg);
|
||||
}
|
||||
else if (sign && m.is_or(f)) {
|
||||
for (auto arg : *to_app(f)) {
|
||||
expr_ref fml(m.mk_not(arg), m);;
|
||||
add_clause(fml);
|
||||
}
|
||||
}
|
||||
else if (sign && m.is_and(f)) {
|
||||
clause.reset();
|
||||
for (auto arg : *to_app(f))
|
||||
clause.push_back(~mk_literal(arg));
|
||||
s.add_clause(clause.size(), clause.data());
|
||||
}
|
||||
else if (m.is_iff(f, g, h)) {
|
||||
auto lit1 = mk_literal(g);
|
||||
auto lit2 = mk_literal(h);
|
||||
sat::literal cls1[2] = { sign ? lit1 : ~lit1, lit2 };
|
||||
sat::literal cls2[2] = { sign ? ~lit1 : lit1, ~lit2 };
|
||||
s.add_clause(2, cls1);
|
||||
s.add_clause(2, cls2);
|
||||
}
|
||||
else if (m.is_ite(f, g, h, k)) {
|
||||
auto lit1 = mk_literal(g);
|
||||
auto lit2 = mk_literal(h);
|
||||
auto lit3 = mk_literal(k);
|
||||
// (g -> h) & (~g -> k)
|
||||
// (g & h) | (~g & k)
|
||||
// negated: (g -> ~h) & (g -> ~k)
|
||||
sat::literal cls1[2] = { ~lit1, sign ? ~lit2 : lit2 };
|
||||
sat::literal cls2[2] = { lit1, sign ? ~lit3 : lit3 };
|
||||
s.add_clause(2, cls1);
|
||||
s.add_clause(2, cls2);
|
||||
}
|
||||
else {
|
||||
sat::literal lit = mk_literal(f);
|
||||
if (sign)
|
||||
lit.neg();
|
||||
s.add_clause(1, &lit);
|
||||
}
|
||||
return v;
|
||||
}
|
||||
|
||||
sat::literal context::mk_literal() {
|
||||
sat::bool_var v = s.add_var();
|
||||
return sat::literal(v, false);
|
||||
}
|
||||
|
||||
sat::literal context::mk_literal(expr* e) {
|
||||
sat::literal lit;
|
||||
bool neg = false;
|
||||
expr* a, * b, * c;
|
||||
while (m.is_not(e, e))
|
||||
neg = !neg;
|
||||
auto v = m_atom2bool_var.get(e->get_id(), sat::null_bool_var);
|
||||
if (v != sat::null_bool_var)
|
||||
return sat::literal(v, neg);
|
||||
sat::literal_vector clause;
|
||||
lit = mk_literal();
|
||||
if (m.is_true(e)) {
|
||||
clause.push_back(lit);
|
||||
s.add_clause(clause.size(), clause.data());
|
||||
}
|
||||
else if (m.is_false(e)) {
|
||||
clause.push_back(~lit);
|
||||
s.add_clause(clause.size(), clause.data());
|
||||
}
|
||||
else if (m.is_and(e)) {
|
||||
for (expr* arg : *to_app(e)) {
|
||||
auto lit2 = mk_literal(arg);
|
||||
clause.push_back(~lit2);
|
||||
sat::literal lits[2] = { ~lit, lit2 };
|
||||
s.add_clause(2, lits);
|
||||
}
|
||||
clause.push_back(lit);
|
||||
s.add_clause(clause.size(), clause.data());
|
||||
}
|
||||
else if (m.is_or(e)) {
|
||||
for (expr* arg : *to_app(e)) {
|
||||
auto lit2 = mk_literal(arg);
|
||||
clause.push_back(lit2);
|
||||
sat::literal lits[2] = { lit, ~lit2 };
|
||||
s.add_clause(2, lits);
|
||||
}
|
||||
clause.push_back(~lit);
|
||||
s.add_clause(clause.size(), clause.data());
|
||||
}
|
||||
else if (m.is_iff(e, a, b) || m.is_xor(e, a, b)) {
|
||||
auto lit1 = mk_literal(a);
|
||||
auto lit2 = mk_literal(b);
|
||||
if (m.is_xor(e))
|
||||
lit2.neg();
|
||||
sat::literal cls1[3] = { ~lit, ~lit1, lit2 };
|
||||
sat::literal cls2[3] = { ~lit, lit1, ~lit2 };
|
||||
sat::literal cls3[3] = { lit, lit1, lit2 };
|
||||
sat::literal cls4[3] = { lit, ~lit1, ~lit2 };
|
||||
s.add_clause(3, cls1);
|
||||
s.add_clause(3, cls2);
|
||||
s.add_clause(3, cls3);
|
||||
s.add_clause(3, cls4);
|
||||
}
|
||||
else if (m.is_ite(e, a, b, c)) {
|
||||
auto lit1 = mk_literal(a);
|
||||
auto lit2 = mk_literal(b);
|
||||
auto lit3 = mk_literal(c);
|
||||
sat::literal cls1[3] = { ~lit, ~lit1, lit2 };
|
||||
sat::literal cls2[3] = { ~lit, lit1, lit3 };
|
||||
sat::literal cls3[3] = { lit, ~lit1, ~lit2 };
|
||||
sat::literal cls4[3] = { lit, lit1, ~lit3 };
|
||||
s.add_clause(3, cls1);
|
||||
s.add_clause(3, cls2);
|
||||
s.add_clause(3, cls3);
|
||||
s.add_clause(3, cls4);
|
||||
}
|
||||
else
|
||||
register_terms(e);
|
||||
|
||||
register_atom(lit.var(), e);
|
||||
|
||||
return neg ? ~lit : lit;
|
||||
}
|
||||
|
||||
|
||||
void context::init() {
|
||||
m_new_constraint = false;
|
||||
if (m_initialized)
|
||||
|
|
|
|||
|
|
@ -104,12 +104,13 @@ namespace sls {
|
|||
random_gen m_rand;
|
||||
bool m_initialized = false;
|
||||
bool m_new_constraint = false;
|
||||
bool m_dirty = false;
|
||||
expr_ref_vector m_allterms;
|
||||
ptr_vector<expr> m_subterms;
|
||||
greater_depth m_gd;
|
||||
less_depth m_ld;
|
||||
heap<greater_depth> m_repair_down;
|
||||
heap<less_depth> m_repair_up;
|
||||
heap<less_depth> m_repair_up;
|
||||
|
||||
void register_plugin(plugin* p);
|
||||
|
||||
|
|
@ -117,12 +118,14 @@ namespace sls {
|
|||
ptr_vector<expr> m_todo;
|
||||
void register_terms(expr* e);
|
||||
void register_term(expr* e);
|
||||
sat::bool_var mk_atom(expr* e);
|
||||
|
||||
void propagate_boolean_assignment();
|
||||
void propagate_literal(sat::literal lit);
|
||||
|
||||
family_id get_fid(expr* e) const;
|
||||
|
||||
|
||||
sat::literal mk_literal();
|
||||
|
||||
public:
|
||||
context(ast_manager& m, sat_solver_context& s);
|
||||
|
|
@ -142,6 +145,8 @@ namespace sls {
|
|||
expr* atom(sat::bool_var v) { return m_atoms.get(v, nullptr); }
|
||||
expr* term(unsigned id) const { return m_allterms.get(id); }
|
||||
sat::bool_var atom2bool_var(expr* e) const { return m_atom2bool_var.get(e->get_id(), sat::null_bool_var); }
|
||||
sat::literal mk_literal(expr* e);
|
||||
void add_clause(expr* f);
|
||||
void flip(sat::bool_var v) { s.flip(v); }
|
||||
double reward(sat::bool_var v) { return s.reward(v); }
|
||||
indexed_uint_set const& unsat() const { return s.unsat(); }
|
||||
|
|
|
|||
|
|
@ -27,8 +27,9 @@ namespace sls {
|
|||
ast_manager& m;
|
||||
sat::ddfw& m_ddfw;
|
||||
context m_context;
|
||||
bool m_new_clause_added = false;
|
||||
bool m_dirty = false;
|
||||
model_ref m_model;
|
||||
obj_map<expr, sat::literal> m_expr2lit;
|
||||
public:
|
||||
solver_ctx(ast_manager& m, sat::ddfw& d) :
|
||||
m(m), m_ddfw(d), m_context(m, *this) {
|
||||
|
|
@ -54,11 +55,11 @@ namespace sls {
|
|||
TRACE("sls", display(tout));
|
||||
while (unsat().empty()) {
|
||||
m_context.check();
|
||||
if (!m_new_clause_added)
|
||||
if (!m_dirty)
|
||||
break;
|
||||
TRACE("sls", display(tout));
|
||||
m_ddfw.reinit();
|
||||
m_new_clause_added = false;
|
||||
m_dirty = false;
|
||||
}
|
||||
}
|
||||
|
||||
|
|
@ -80,17 +81,29 @@ namespace sls {
|
|||
vector<sat::clause_info> const& clauses() const override { return m_ddfw.clauses(); }
|
||||
sat::clause_info const& get_clause(unsigned idx) const override { return m_ddfw.get_clause_info(idx); }
|
||||
ptr_iterator<unsigned> get_use_list(sat::literal lit) override { return m_ddfw.use_list(lit); }
|
||||
void flip(sat::bool_var v) override { m_ddfw.flip(v); }
|
||||
void flip(sat::bool_var v) override { if (m_dirty) m_ddfw.reinit(), m_dirty = false; m_ddfw.flip(v); }
|
||||
double reward(sat::bool_var v) override { return m_ddfw.get_reward(v); }
|
||||
double get_weigth(unsigned clause_idx) override { return m_ddfw.get_clause_info(clause_idx).m_weight; }
|
||||
bool is_true(sat::literal lit) override { return m_ddfw.get_value(lit.var()) != lit.sign(); }
|
||||
unsigned num_vars() const override { return m_ddfw.num_vars(); }
|
||||
indexed_uint_set const& unsat() const override { return m_ddfw.unsat_set(); }
|
||||
sat::bool_var add_var() override { return m_ddfw.add_var(); }
|
||||
void add_clause(unsigned n, sat::literal const* lits) override {
|
||||
m_ddfw.add(n, lits);
|
||||
m_new_clause_added = true;
|
||||
sat::bool_var add_var() override { m_dirty = true; return m_ddfw.add_var(); }
|
||||
|
||||
|
||||
void add_clause(expr* f) {
|
||||
m_context.add_clause(f);
|
||||
}
|
||||
|
||||
void add_clause(unsigned n, sat::literal const* lits) override {
|
||||
m_ddfw.add(n, lits);
|
||||
m_dirty = true;
|
||||
}
|
||||
|
||||
sat::literal mk_literal() {
|
||||
sat::bool_var v = add_var();
|
||||
return sat::literal(v, false);
|
||||
}
|
||||
|
||||
model_ref get_model() { return m_model; }
|
||||
|
||||
void collect_statistics(statistics& st) {
|
||||
|
|
@ -129,143 +142,13 @@ namespace sls {
|
|||
// send expression mapping to m_solver_ctx
|
||||
|
||||
for (auto f : m_assertions)
|
||||
add_clause(f);
|
||||
m_solver_ctx->add_clause(f);
|
||||
|
||||
IF_VERBOSE(10, m_solver_ctx->display(verbose_stream()));
|
||||
auto r = m_ddfw.check(0, nullptr);
|
||||
|
||||
return r;
|
||||
}
|
||||
|
||||
void smt_solver::add_clause(expr* f) {
|
||||
expr* g, * h, * k;
|
||||
sat::literal_vector clause;
|
||||
if (m.is_not(f, g) && m.is_not(g, g)) {
|
||||
add_clause(g);
|
||||
return;
|
||||
}
|
||||
bool sign = m.is_not(f, f);
|
||||
if (!sign && 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 if (!sign && m.is_and(f)) {
|
||||
for (auto arg : *to_app(f))
|
||||
add_clause(arg);
|
||||
}
|
||||
else if (sign && m.is_or(f)) {
|
||||
for (auto arg : *to_app(f)) {
|
||||
expr_ref fml(m.mk_not(arg), m);;
|
||||
add_clause(fml);
|
||||
}
|
||||
}
|
||||
else if (sign && m.is_and(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 if (m.is_iff(f, g, h)) {
|
||||
auto lit1 = mk_literal(g);
|
||||
auto lit2 = mk_literal(h);
|
||||
sat::literal cls1[2] = { sign ? lit1 :~lit1, lit2 };
|
||||
sat::literal cls2[2] = { sign ? ~lit1 : lit1, ~lit2 };
|
||||
m_solver_ctx->add_clause(2, cls1);
|
||||
m_solver_ctx->add_clause(2, cls2);
|
||||
}
|
||||
else if (m.is_ite(f, g, h, k)) {
|
||||
auto lit1 = mk_literal(g);
|
||||
auto lit2 = mk_literal(h);
|
||||
auto lit3 = mk_literal(k);
|
||||
// (g -> h) & (~g -> k)
|
||||
// (g & h) | (~g & k)
|
||||
// negated: (g -> ~h) & (g -> ~k)
|
||||
sat::literal cls1[2] = { ~lit1, sign ? ~lit2 : lit2 };
|
||||
sat::literal cls2[2] = { lit1, sign ? ~lit3 : lit3 };
|
||||
m_solver_ctx->add_clause(2, cls1);
|
||||
m_solver_ctx->add_clause(2, cls2);
|
||||
}
|
||||
else {
|
||||
sat::literal lit = mk_literal(f);
|
||||
if (sign)
|
||||
lit.neg();
|
||||
m_solver_ctx->add_clause(1, &lit);
|
||||
}
|
||||
}
|
||||
|
||||
sat::literal smt_solver::mk_literal(expr* e) {
|
||||
sat::literal lit;
|
||||
bool neg = false;
|
||||
expr* a, * b, * c;
|
||||
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 if (m.is_iff(e, a, b)) {
|
||||
lit = mk_literal();
|
||||
auto lit1 = mk_literal(a);
|
||||
auto lit2 = mk_literal(b);
|
||||
sat::literal cls1[3] = { ~lit, ~lit1, lit2 };
|
||||
sat::literal cls2[3] = { ~lit, lit1, ~lit2 };
|
||||
sat::literal cls3[3] = { lit, lit1, lit2 };
|
||||
sat::literal cls4[3] = { lit, ~lit1, ~lit2 };
|
||||
m_solver_ctx->add_clause(3, cls1);
|
||||
m_solver_ctx->add_clause(3, cls2);
|
||||
m_solver_ctx->add_clause(3, cls3);
|
||||
m_solver_ctx->add_clause(3, cls4);
|
||||
}
|
||||
else if (m.is_ite(e, a, b, c)) {
|
||||
lit = mk_literal();
|
||||
auto lit1 = mk_literal(a);
|
||||
auto lit2 = mk_literal(b);
|
||||
auto lit3 = mk_literal(c);
|
||||
sat::literal cls1[3] = { ~lit, ~lit1, lit2 };
|
||||
sat::literal cls2[3] = { ~lit, lit1, lit3 };
|
||||
sat::literal cls3[3] = { lit, ~lit1, ~lit2 };
|
||||
sat::literal cls4[3] = { lit, lit1, ~lit3 };
|
||||
m_solver_ctx->add_clause(3, cls1);
|
||||
m_solver_ctx->add_clause(3, cls2);
|
||||
m_solver_ctx->add_clause(3, cls3);
|
||||
m_solver_ctx->add_clause(3, cls4);
|
||||
}
|
||||
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() {
|
||||
return m_solver_ctx->get_model();
|
||||
|
|
|
|||
|
|
@ -29,12 +29,7 @@ namespace sls {
|
|||
solver_ctx* m_solver_ctx = nullptr;
|
||||
expr_ref_vector m_assertions;
|
||||
statistics m_st;
|
||||
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();
|
||||
|
|
|
|||
|
|
@ -78,7 +78,7 @@ public:
|
|||
try {
|
||||
res = m_sls->check();
|
||||
}
|
||||
catch (z3_exception& ex) {
|
||||
catch (z3_exception&) {
|
||||
m_sls->collect_statistics(m_st);
|
||||
throw;
|
||||
}
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue