mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
add virtual destructor to fix build
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
1894c86ee0
commit
1ffbe23ee3
|
@ -61,7 +61,8 @@ namespace sat {
|
|||
class clause;
|
||||
|
||||
struct print_clause {
|
||||
virtual void on_clause(unsigned, literal const*, status) = 0;
|
||||
virtual ~print_clause() {}
|
||||
virtual void on_clause(unsigned, literal const*, status) = 0;
|
||||
};
|
||||
|
||||
class drat {
|
||||
|
@ -150,12 +151,12 @@ namespace sat {
|
|||
|
||||
// support for SMT - connect Boolean variables with AST nodes
|
||||
// associate AST node id with Boolean variable v
|
||||
void bool_def(bool_var v, unsigned n);
|
||||
|
||||
// declare AST node n with 'name' and arguments arg
|
||||
void def_begin(char id, unsigned n, std::string const& name);
|
||||
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);
|
||||
|
|
|
@ -41,6 +41,11 @@ namespace euf {
|
|||
get_drat().def_begin(id, n, name);
|
||||
}
|
||||
|
||||
void solver::bool_def(bool_var v, unsigned n) {
|
||||
get_drat().bool_def(v, 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);
|
||||
|
@ -59,14 +64,14 @@ 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)
|
||||
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));
|
||||
def_begin('v', v->get_id(), "" + mk_pp(e->get_sort(), m));
|
||||
def_add_arg(v->get_idx());
|
||||
def_end();
|
||||
}
|
||||
|
@ -77,7 +82,7 @@ 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());
|
||||
def_begin('q', q->get_id(), strm.str());
|
||||
def_add_arg(q->get_expr()->get_id());
|
||||
def_end();
|
||||
}
|
||||
|
@ -116,7 +121,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());
|
||||
}
|
||||
|
||||
|
||||
|
@ -130,7 +135,7 @@ 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());
|
||||
def_begin('f', f->get_small_id(), strm.str());
|
||||
def_end();
|
||||
}
|
||||
|
||||
|
@ -200,11 +205,11 @@ 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("="));
|
||||
def_begin('e', eq->get_id(), std::string("="));
|
||||
def_add_arg(a->get_id());
|
||||
def_add_arg(b->get_id());
|
||||
def_end();
|
||||
get_drat().bool_def(lit.var(), eq->get_id());
|
||||
bool_def(lit.var(), eq->get_id());
|
||||
}
|
||||
|
||||
void solver::on_clause(unsigned n, literal const* lits, sat::status st) {
|
||||
|
|
|
@ -352,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);
|
||||
|
|
Loading…
Reference in a new issue