mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-29 20:05:51 +00:00
Code Activity

Merge branch 'master' of https://github.com/Z3Prover/z3

Browse source
This commit is contained in:
Nikolaj Bjorner 2022-08-26 10:44:40 -07:00
commit dd91fab6f4
6 changed files with 72 additions and 71 deletions
Download patch file Download diff file Expand all files Collapse all files

62
src/sat/smt/euf_proof.cpp
View file

@ -29,6 +29,31 @@ namespace euf {
m_drat_initialized = true;
}
void solver::def_add_arg(unsigned arg) {
auto* out = get_drat().out();
if (out)
(*out) << " " << arg;
}
void solver::def_end() {
auto* out = get_drat().out();
if (out)
(*out) << " 0\n";
}
void solver::def_begin(char id, unsigned n, std::string const& name) {
auto* out = get_drat().out();
if (out)
(*out) << id << " " << n << " " << name;
}
void solver::bool_def(bool_var v, unsigned n) {
auto* out = get_drat().out();
if (out)
(*out) << "b " << v << " " << n << " 0\n";
}
void solver::drat_log_params(func_decl* f) {
for (unsigned i = f->get_num_parameters(); i-- > 0; ) {
auto const& p = f->get_parameter(i);
@ -39,6 +64,7 @@ namespace euf {
drat_log_decl(to_func_decl(a));
}
}
void solver::drat_log_expr1(expr* e) {
if (is_app(e)) {
app* a = to_app(e);
@ -46,16 +72,16 @@ namespace euf {
drat_log_decl(a->get_decl());
std::stringstream strm;
strm << mk_ismt2_func(a->get_decl(), m);
get_drat().def_begin('e', e->get_id(), strm.str());
def_begin('e', e->get_id(), strm.str());
for (expr* arg : *a)
get_drat().def_add_arg(arg->get_id());
get_drat().def_end();
def_add_arg(arg->get_id());
def_end();
}
else if (is_var(e)) {
var* v = to_var(e);
get_drat().def_begin('v', v->get_id(), "" + mk_pp(e->get_sort(), m));
get_drat().def_add_arg(v->get_idx());
get_drat().def_end();
def_begin('v', v->get_id(), "" + mk_pp(e->get_sort(), m));
def_add_arg(v->get_idx());
def_end();
}
else if (is_quantifier(e)) {
quantifier* q = to_quantifier(e);
@ -64,9 +90,9 @@ namespace euf {
for (unsigned i = 0; i < q->get_num_decls(); ++i)
strm << " (" << q->get_decl_name(i) << " " << mk_pp(q->get_decl_sort(i), m) << ")";
strm << ")";
get_drat().def_begin('q', q->get_id(), strm.str());
get_drat().def_add_arg(q->get_expr()->get_id());
get_drat().def_end();
def_begin('q', q->get_id(), strm.str());
def_add_arg(q->get_expr()->get_id());
def_end();
}
else
UNREACHABLE();
@ -103,7 +129,7 @@ namespace euf {
if (!use_drat())
return;
drat_log_expr(e);
get_drat().bool_def(v, e->get_id());
bool_def(v, e->get_id());
}
@ -117,8 +143,8 @@ namespace euf {
std::ostringstream strm;
smt2_pp_environment_dbg env(m);
ast_smt2_pp(strm, f, env);
get_drat().def_begin('f', f->get_small_id(), strm.str());
get_drat().def_end();
def_begin('f', f->get_small_id(), strm.str());
def_end();
}
/**
@ -187,14 +213,14 @@ namespace euf {
VERIFY(m.is_eq(eq, a, b));
drat_log_expr(a);
drat_log_expr(b);
get_drat().def_begin('e', eq->get_id(), std::string("="));
get_drat().def_add_arg(a->get_id());
get_drat().def_add_arg(b->get_id());
get_drat().def_end();
get_drat().bool_def(lit.var(), eq->get_id());
def_begin('e', eq->get_id(), std::string("="));
def_add_arg(a->get_id());
def_add_arg(b->get_id());
def_end();
bool_def(lit.var(), eq->get_id());
}
void solver::log_clause(unsigned n, literal const* lits, sat::status st) {
void solver::on_clause(unsigned n, literal const* lits, sat::status st) {
if (!get_config().m_lemmas2console)
return;
if (!st.is_redundant() && !st.is_asserted())

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

@ -171,13 +171,8 @@ namespace euf {
for (auto* s : m_solvers)
s->init_search();
if (get_config().m_lemmas2console) {
std::function<void(unsigned, sat::literal const*, sat::status)> on_clause =
[&](unsigned n, sat::literal const* lits, sat::status st) {
log_clause(n, lits, st);
};
get_drat().set_print_clause(on_clause);
}
if (get_config().m_lemmas2console)
get_drat().set_print_clause(*this);
}
bool solver::is_external(bool_var v) {

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

@ -60,7 +60,7 @@ namespace euf {
std::ostream& display(std::ostream& out) const;
};
class solver : public sat::extension, public th_internalizer, public th_decompile {
class solver : public sat::extension, public th_internalizer, public th_decompile, public sat::print_clause {
typedef top_sort<euf::enode> deps_t;
friend class ackerman;
class user_sort;
@ -183,7 +183,10 @@ namespace euf {
bool m_drat_initialized{ false };
void init_drat();
ast_pp_util m_clause_visitor;
void log_clause(unsigned n, literal const* lits, sat::status st);
void on_clause(unsigned n, literal const* lits, sat::status st) override;
void def_add_arg(unsigned arg);
void def_end();
void def_begin(char id, unsigned n, std::string const& name);
// relevancy
@ -349,6 +352,7 @@ namespace euf {
void drat_bool_def(sat::bool_var v, expr* n);
void drat_eq_def(sat::literal lit, expr* eq);
void drat_log_expr(expr* n);
void bool_def(bool_var v, unsigned n);
bool visit_clause(unsigned n, literal const* lits);
void display_clause(unsigned n, literal const* lits);
void visit_expr(expr* e);

7
src/sat/smt/pb_solver.cpp
View file

@ -1430,10 +1430,9 @@ namespace pb {
IF_VERBOSE(0, verbose_stream() << *c << "\n");
VERIFY(c->well_formed());
if (m_solver && m_solver->get_config().m_drat) {
std::function<void(std::ostream& out)> fn = [&](std::ostream& out) {
out << "c ba constraint " << *c << " 0\n";
};
m_solver->get_drat().log_adhoc(fn);
auto * out = s().get_drat().out();
if (out)
*out << "c ba constraint " << *c << " 0\n";
}
}