mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-26 21:16:02 +00:00
Code Activity

adding euf

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-08-31 14:36:16 -07:00
parent 314bd9277b
commit 4d41db3028
26 changed files with 353 additions and 152 deletions
Download patch file Download diff file Expand all files Collapse all files

5
src/sat/smt/CMakeLists.txt
View file

@ -1,13 +1,14 @@
z3_add_component(sat_smt
SOURCES
atom2bool_var.cpp
ba_internalize.cpp
ba_solver.cpp
xor_solver.cpp
ba_internalize.cpp
euf_ackerman.cpp
euf_internalize.cpp
euf_solver.cpp
euf_model.cpp
euf_proof.cpp
euf_solver.cpp
COMPONENT_DEPENDENCIES
sat
ast

24
src/sat/smt/ba_solver.cpp
View file

@ -317,14 +317,6 @@ namespace sat {
m_num_propagations_since_pop++;
//TRACE("ba", tout << "#prop: " << m_stats.m_num_propagations << " - " << c.lit() << " => " << lit << "\n";);
SASSERT(validate_unit_propagation(c, lit));
if (get_config().m_drat) {
svector<drat::premise> ps;
literal_vector lits;
get_antecedents(lit, c, lits);
lits.push_back(lit);
ps.push_back(drat::premise(drat::s_ext(), c.lit())); // null_literal case.
drat_add(lits, ps);
}
assign(lit, justification::mk_ext_justification(s().scope_lvl(), c.cindex()));
break;
}
@ -1604,9 +1596,8 @@ namespace sat {
TRACE("ba", tout << m_lemma << "\n";);
if (get_config().m_drat) {
svector<drat::premise> ps; // TBD fill in
drat_add(m_lemma, ps);
if (get_config().m_drat && m_solver) {
s().m_drat.add(m_lemma, sat::drat::status::ba);
}
s().m_lemma.reset();
@ -1843,6 +1834,10 @@ namespace sat {
add_pb_ge(lit, wlits, k, m_is_redundant);
}
bool ba_solver::is_external(bool_var v) {
return false;
}
/*
\brief return true to keep watching literal.
*/
@ -2129,6 +2124,13 @@ namespace sat {
case xr_t: get_antecedents(l, c.to_xr(), r); break;
default: UNREACHABLE(); break;
}
if (get_config().m_drat && m_solver) {
literal_vector lits;
for (literal lit : r)
lits.push_back(~lit);
lits.push_back(l);
s().m_drat.add(lits, sat::drat::status::ba);
}
}
void ba_solver::nullify_tracking_literal(constraint& c) {

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

@ -469,7 +469,6 @@ namespace sat {
else m_solver->set_conflict(j, l);
}
inline config const& get_config() const { return m_lookahead ? m_lookahead->get_config() : m_solver->get_config(); }
inline void drat_add(literal_vector const& c, svector<drat::premise> const& premises) { if (m_solver) m_solver->m_drat.add(c, premises); }
mutable bool m_overflow;
@ -572,6 +571,7 @@ namespace sat {
void add_pb_ge(bool_var v, svector<wliteral> const& wlits, unsigned k);
void add_xr(literal_vector const& lits);
bool is_external(bool_var v) override;
bool propagate(literal l, ext_constraint_idx idx) override;
lbool resolve_conflict() override;
void get_antecedents(literal l, ext_justification_idx idx, literal_vector & r) override;

20
src/sat/smt/euf_internalize.cpp
View file

@ -54,7 +54,7 @@ namespace euf {
m_args.reset();
for (unsigned i = 0; i < num; ++i)
m_args.push_back(m_egraph.find(to_app(e)->get_arg(i)));
if (root && internalize_root(to_app(e), m_args.c_ptr(), sign))
if (root && internalize_root(to_app(e), sign))
return sat::null_literal;
n = m_egraph.mk(e, num, m_args.c_ptr());
attach_node(n);
@ -90,8 +90,10 @@ namespace euf {
void solver::attach_node(euf::enode* n) {
expr* e = n->get_owner();
log_node(n);
if (m.is_bool(e)) {
sat::bool_var v = si.add_bool_var(e);
log_bool_var(v, n);
attach_lit(literal(v, false), n);
}
axiomatize_basic(n);
@ -112,12 +114,13 @@ namespace euf {
m_var_trail.push_back(v);
}
bool solver::internalize_root(app* e, enode* const* args, bool sign) {
bool solver::internalize_root(app* e, bool sign) {
if (m.is_distinct(e)) {
enode_vector _args(m_args);
if (sign)
add_not_distinct_axiom(e, args);
add_not_distinct_axiom(e, _args.c_ptr());
else
add_distinct_axiom(e, args);
add_distinct_axiom(e, _args.c_ptr());
return true;
}
return false;
@ -129,7 +132,7 @@ namespace euf {
if (sz <= 1)
return;
static const unsigned distinct_max_args = 24;
static const unsigned distinct_max_args = 32;
if (sz <= distinct_max_args) {
sat::literal_vector lits;
for (unsigned i = 0; i < sz; ++i) {
@ -157,19 +160,19 @@ namespace euf {
expr_ref gapp(m.mk_app(g, fapp.get()), m);
expr_ref eq(m.mk_eq(gapp, arg), m);
sat::literal lit = internalize(eq, false, false, m_is_redundant);
s().add_clause(1, &lit, false);
s().add_clause(1, &lit, m_is_redundant);
eqs.push_back(m.mk_eq(fapp, a));
}
pb_util pb(m);
expr_ref at_least2(pb.mk_at_least_k(eqs.size(), eqs.c_ptr(), 2), m);
sat::literal lit = si.internalize(at_least2, m_is_redundant);
s().mk_clause(1, &lit, false);
s().mk_clause(1, &lit, m_is_redundant);
}
}
void solver::add_distinct_axiom(app* e, enode* const* args) {
SASSERT(m.is_distinct(e));
static const unsigned distinct_max_args = 24;
static const unsigned distinct_max_args = 32;
unsigned sz = e->get_num_args();
if (sz <= 1) {
s().mk_clause(0, nullptr, m_is_redundant);
@ -211,6 +214,7 @@ namespace euf {
expr* el = a->get_arg(2);
sat::bool_var v = m_expr2var.to_bool_var(c);
SASSERT(v != sat::null_bool_var);
SASSERT(!m.is_bool(e));
expr_ref eq_th(m.mk_eq(a, th), m);
expr_ref eq_el(m.mk_eq(a, el), m);
sat::literal lit_th = internalize(eq_th, false, false, m_is_redundant);

14
src/sat/smt/euf_model.cpp
View file

@ -69,7 +69,19 @@ namespace euf {
}
// model of s() must have been fixed.
if (m.is_bool(e)) {
switch (s().value(m_expr2var.to_bool_var(e))) {
if (m.is_true(e)) {
values.set(id, m.mk_true());
continue;
}
if (m.is_false(e)) {
values.set(id, m.mk_false());
continue;
}
if (is_app(e) && to_app(e)->get_family_id() == m.get_basic_family_id())
continue;
sat::bool_var v = m_expr2var.to_bool_var(e);
SASSERT(v != sat::null_bool_var);
switch (s().value(v)) {
case l_true:
values.set(id, m.mk_true());
break;

73
src/sat/smt/euf_proof.cpp Normal file
View file

@ -0,0 +1,73 @@
/*++
Copyright (c) 2020 Microsoft Corporation
Module Name:
euf_proof.cpp
Abstract:
Proof logging facilities.
Author:
Nikolaj Bjorner (nbjorner) 2020-08-25
--*/
#include "sat/smt/euf_solver.h"
namespace euf {
void solver::log_node(enode* n) {
if (m_drat) {
expr* e = n->get_owner();
if (is_app(e)) {
symbol const& name = to_app(e)->get_name();
s().get_drat().def_begin(n->get_owner_id(), name);
for (enode* arg : enode_args(n)) {
s().get_drat().def_add_arg(arg->get_owner_id());
}
s().get_drat().def_end();
}
else {
IF_VERBOSE(0, verbose_stream() << "logging binders is TBD\n");
}
}
}
void solver::log_bool_var(sat::bool_var v, enode* n) {
if (m_drat) {
s().get_drat().bool_def(v, n->get_owner_id());
}
}
void solver::log_antecedents(literal l, literal_vector const& r) {
TRACE("euf", log_antecedents(tout, l, r););
if (m_drat) {
literal_vector lits;
for (literal lit : r) lits.push_back(~lit);
if (l != sat::null_literal)
lits.push_back(l);
s().get_drat().add(lits, sat::drat::status::euf);
}
}
void solver::log_antecedents(std::ostream& out, literal l, literal_vector const& r) {
for (sat::literal l : r) {
enode* n = m_var2node[l.var()];
out << ~l << ": ";
if (!l.sign()) out << "! ";
out << mk_pp(n->get_owner(), m) << "\n";
SASSERT(s().value(l) == l_true);
}
if (l != sat::null_literal) {
out << l << ": ";
if (l.sign()) out << "! ";
enode* n = m_var2node[l.var()];
out << mk_pp(n->get_owner(), m) << "\n";
}
}
}

54
src/sat/smt/euf_solver.cpp
View file

@ -16,6 +16,7 @@ Author:
--*/
#include "ast/pb_decl_plugin.h"
#include "ast/ast_ll_pp.h"
#include "sat/sat_solver.h"
#include "sat/smt/sat_smt.h"
#include "sat/smt/ba_solver.h"
@ -25,6 +26,7 @@ namespace euf {
void solver::updt_params(params_ref const& p) {
m_config.updt_params(p);
m_drat = s().get_config().m_drat;
}
/**
@ -82,6 +84,19 @@ namespace euf {
IF_VERBOSE(0, verbose_stream() << mk_pp(f, m) << " not handled\n");
}
void solver::init_search() {
TRACE("euf", display(tout););
}
bool solver::is_external(bool_var v) {
if (nullptr != m_var2node.get(v, nullptr))
return true;
for (auto* s : m_solvers)
if (s->is_external(v))
return true;
return false;
}
bool solver::propagate(literal l, ext_constraint_idx idx) {
force_push();
auto* ext = sat::constraint_base::to_extension(idx);
@ -127,6 +142,8 @@ namespace euf {
}
for (unsigned* idx : m_explain)
r.push_back(sat::to_literal((unsigned)(idx - base_ptr())));
log_antecedents(l, r);
}
void solver::asserted(literal l) {
@ -145,12 +162,12 @@ namespace euf {
if (m.is_eq(e) && !sign) {
euf::enode* na = n->get_arg(0);
euf::enode* nb = n->get_arg(1);
TRACE("euf", tout << "merge " << na->get_owner_id() << nb->get_owner_id() << "\n";);
TRACE("euf", tout << mk_pp(e, m) << "\n";);
m_egraph.merge(na, nb, base_ptr() + l.index());
}
else {
euf::enode* nb = sign ? mk_false() : mk_true();
TRACE("euf", tout << "merge " << n->get_owner_id() << " " << mk_pp(nb->get_owner(), m) << "\n";);
TRACE("euf", tout << (sign ? "not ": " ") << mk_pp(n->get_owner(), m) << "\n";);
m_egraph.merge(n, nb, base_ptr() + l.index());
}
// TBD: delay propagation?
@ -159,8 +176,10 @@ namespace euf {
void solver::propagate() {
m_egraph.propagate();
if (m_egraph.inconsistent()) {
s().set_conflict(sat::justification::mk_ext_justification(s().scope_lvl(), conflict_constraint().to_index()));
unsigned lvl = s().scope_lvl();
if (m_egraph.inconsistent()) {
s().set_conflict(sat::justification::mk_ext_justification(lvl, conflict_constraint().to_index()));
return;
}
for (euf::enode* eq : m_egraph.new_eqs()) {
@ -168,7 +187,10 @@ namespace euf {
expr* a = nullptr, *b = nullptr;
if (s().value(v) == l_false && m_ackerman && m.is_eq(eq->get_owner(), a, b))
m_ackerman->cg_conflict_eh(a, b);
s().assign(literal(v, false), sat::justification::mk_ext_justification(s().scope_lvl(), eq_constraint().to_index()));
literal lit(v, false);
if (s().value(lit) == l_true)
continue;
s().assign(literal(v, false), sat::justification::mk_ext_justification(lvl, eq_constraint().to_index()));
}
for (euf::enode* p : m_egraph.new_lits()) {
expr* e = p->get_owner();
@ -177,9 +199,11 @@ namespace euf {
SASSERT(m.is_true(p->get_root()->get_owner()) || sign);
bool_var v = m_expr2var.to_bool_var(e);
literal lit(v, sign);
if (s().value(lit) == l_true)
continue;
if (s().value(lit) == l_false && m_ackerman)
m_ackerman->cg_conflict_eh(p->get_owner(), p->get_root()->get_owner());
s().assign(lit, sat::justification::mk_ext_justification(s().scope_lvl(), lit_constraint().to_index()));
s().assign(lit, sat::justification::mk_ext_justification(lvl, lit_constraint().to_index()));
}
}
@ -218,14 +242,14 @@ namespace euf {
}
void solver::push() {
scope s;
s.m_var_lim = m_var_trail.size();
s.m_trail_lim = m_trail.size();
m_scopes.push_back(s);
m_region.push_scope();
for (auto* e : m_solvers)
e->push();
m_egraph.push();
scope s;
s.m_var_lim = m_var_trail.size();
s.m_trail_lim = m_trail.size();
m_scopes.push_back(s);
m_region.push_scope();
for (auto* e : m_solvers)
e->push();
m_egraph.push();
}
void solver::force_push() {
@ -281,7 +305,7 @@ namespace euf {
out << "bool-vars\n";
for (unsigned v : m_var_trail) {
euf::enode* n = m_var2node[v];
out << v << ": " << m_egraph.pp(n);
out << v << ": " << n->get_owner_id() << " " << mk_bounded_pp(n->get_owner(), m, 1) << "\n";
}
for (auto* e : m_solvers)
e->display(out);

39
src/sat/smt/euf_solver.h
View file

@ -66,6 +66,7 @@ namespace euf {
atom2bool_var& m_expr2var;
sat::sat_internalizer& si;
smt_params m_config;
bool m_drat { false };
euf::egraph m_egraph;
stats m_stats;
region m_region;
@ -104,7 +105,7 @@ namespace euf {
void add_distinct_axiom(app* e, euf::enode* const* args);
void add_not_distinct_axiom(app* e, euf::enode* const* args);
void axiomatize_basic(enode* n);
bool internalize_root(app* e, enode* const* args, bool sign);
bool internalize_root(app* e, bool sign);
euf::enode* mk_true();
euf::enode* mk_false();
@ -127,6 +128,10 @@ namespace euf {
void propagate();
void get_antecedents(literal l, constraint& j, literal_vector& r);
void force_push();
void log_antecedents(std::ostream& out, literal l, literal_vector const& r);
void log_antecedents(literal l, literal_vector const& r);
void log_node(enode* n);
void log_bool_var(sat::bool_var v, enode* n);
constraint& mk_constraint(constraint*& c, constraint::kind_t k);
constraint& conflict_constraint() { return mk_constraint(m_conflict, constraint::kind_t::conflict); }
@ -155,26 +160,28 @@ namespace euf {
if (m_lit) dealloc(sat::constraint_base::mem2base_ptr(m_lit));
}
struct scoped_set_translate {
solver& s;
scoped_set_translate(solver& s, ast_manager& m, atom2bool_var& a2b, sat::sat_internalizer& si) :
s(s) {
s.m_to_m = &m;
s.m_to_expr2var = &a2b;
s.m_to_si = &si;
}
~scoped_set_translate() {
s.m_to_m = &s.m;
s.m_to_expr2var = &s.m_expr2var;
s.m_to_si = &s.si;
}
};
void updt_params(params_ref const& p);
void set_solver(sat::solver* s) override { m_solver = s; }
void set_lookahead(sat::lookahead* s) override { m_lookahead = s; }
struct scoped_set_translate {
solver& s;
scoped_set_translate(solver& s, ast_manager& m, atom2bool_var& a2b, sat::sat_internalizer& si) :
s(s) {
s.m_to_m = &m;
s.m_to_expr2var = &a2b;
s.m_to_si = &si;
}
~scoped_set_translate() {
s.m_to_m = &s.m;
s.m_to_expr2var = &s.m_expr2var;
s.m_to_si = &s.si;
}
};
void init_search() override;
double get_reward(literal l, ext_constraint_idx idx, sat::literal_occs_fun& occs) const override;
bool is_extended_binary(ext_justification_idx idx, literal_vector& r) override;
bool is_external(bool_var v) override;
bool propagate(literal l, ext_constraint_idx idx) override;
void get_antecedents(literal l, ext_justification_idx idx, literal_vector & r) override;
void asserted(literal l) override;