mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
build fixes
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
6f2a6da600
commit
dd90689339
|
@ -397,7 +397,7 @@ namespace arith {
|
|||
return false;
|
||||
}
|
||||
|
||||
void register_plugins(euf::proof_checker& pc) {
|
||||
void register_plugins(euf::proof_checker& pc) override {
|
||||
pc.register_plugin(symbol("farkas"), this);
|
||||
pc.register_plugin(symbol("bound"), this);
|
||||
pc.register_plugin(symbol("implied-eq"), this);
|
||||
|
|
|
@ -176,7 +176,7 @@ namespace euf {
|
|||
display_literals(out << "(assume", n, lits) << ")\n";
|
||||
}
|
||||
|
||||
void solver::display_redundant(std::ostream& out, unsigned n, literal const* lits, expr_ref& proof_hint) {
|
||||
void solver::display_redundant(std::ostream& out, unsigned n, literal const* lits, expr* proof_hint) {
|
||||
if (proof_hint)
|
||||
visit_expr(out, proof_hint);
|
||||
display_hint(display_literals(out << "(learn", n, lits), proof_hint) << ")\n";
|
||||
|
|
|
@ -26,6 +26,7 @@ namespace euf {
|
|||
arith::proof_checker* apc = alloc(arith::proof_checker, m);
|
||||
m_plugins.push_back(apc);
|
||||
apc->register_plugins(*this);
|
||||
(void)m;
|
||||
}
|
||||
|
||||
proof_checker::~proof_checker() {}
|
||||
|
|
|
@ -184,7 +184,7 @@ namespace euf {
|
|||
void on_proof(unsigned n, literal const* lits, sat::status st);
|
||||
std::ostream& display_literals(std::ostream& out, unsigned n, sat::literal const* lits);
|
||||
void display_assume(std::ostream& out, unsigned n, literal const* lits);
|
||||
void display_redundant(std::ostream& out, unsigned n, literal const* lits, expr_ref& proof_hint);
|
||||
void display_redundant(std::ostream& out, unsigned n, literal const* lits, expr* proof_hint);
|
||||
void display_deleted(std::ostream& out, unsigned n, literal const* lits);
|
||||
std::ostream& display_hint(std::ostream& out, expr* proof_hint);
|
||||
expr_ref status2proof_hint(sat::status st);
|
||||
|
|
Loading…
Reference in a new issue