mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 12:08:18 +00:00
Code Activity

move drat functionality into euf

Browse source
This commit is contained in:
Nikolaj Bjorner 2022-08-25 19:19:13 -07:00
parent 1ffbe23ee3
commit 458f417f44
4 changed files with 16 additions and 39 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

25
src/sat/sat_drat.cpp
View file

@ -255,31 +255,6 @@ namespace sat {
} }
} }
void drat::bool_def(bool_var v, unsigned n) {
if (m_out)
(*m_out) << "b " << v << " " << n << " 0\n";
}
void drat::def_begin(char id, unsigned n, std::string const& name) {
if (m_out)
(*m_out) << id << " " << n << " " << name;
}
void drat::def_add_arg(unsigned arg) {
if (m_out)
(*m_out) << " " << arg;
}
void drat::def_end() {
if (m_out)
(*m_out) << " 0\n";
}
void drat::log_adhoc(std::function<void(std::ostream&)>& fn) {
if (m_out)
fn(*m_out);
}
void drat::append(clause& c, status st) { void drat::append(clause& c, status st) {
TRACE("sat_drat", pp(tout, st) << " " << c << "\n";); TRACE("sat_drat", pp(tout, st) << " " << c << "\n";);
for (literal lit : c) declare(lit); for (literal lit : c) declare(lit);

7
src/sat/sat_drat.h
View file

@ -153,13 +153,8 @@ namespace sat {
// associate AST node id with Boolean variable v // associate AST node id with Boolean variable v
// declare AST node n with 'name' and arguments arg // declare AST node n with 'name' and arguments arg
void def_begin(char id, unsigned n, std::string const& name); std::ostream* out() { return m_out; }
void def_add_arg(unsigned arg);
void def_end();
void bool_def(bool_var v, unsigned n);
// ad-hoc logging until a format is developed
void log_adhoc(std::function<void(std::ostream&)>& fn);
bool is_cleaned(clause& c) const; bool is_cleaned(clause& c) const;
void del(literal l); void del(literal l);

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

@ -30,19 +30,27 @@ namespace euf {
} }
void solver::def_add_arg(unsigned arg) { void solver::def_add_arg(unsigned arg) {
get_drat().def_add_arg(arg); auto* out = get_drat().out();
if (out)
(*out) << " " << arg;
} }
void solver::def_end() { void solver::def_end() {
get_drat().def_end(); auto* out = get_drat().out();
if (out)
(*out) << " 0\n";
} }
void solver::def_begin(char id, unsigned n, std::string const& name) { void solver::def_begin(char id, unsigned n, std::string const& name) {
get_drat().def_begin(id, n, name); auto* out = get_drat().out();
if (out)
(*out) << id << " " << n << " " << name;
} }
void solver::bool_def(bool_var v, unsigned n) { void solver::bool_def(bool_var v, unsigned n) {
get_drat().bool_def(v, n); auto* out = get_drat().out();
if (out)
(*out) << "b " << v << " " << n << " 0\n";
} }

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

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