mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-02 20:31:21 +00:00
Code Activity

several fixes to proof logging in legacy solver

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2023-01-08 16:11:31 -08:00
parent 61b90e64b2
commit 1ddef117a2
3 changed files with 29 additions and 7 deletions
Download patch file Download diff file Expand all files Collapse all files

29
src/smt/smt_clause_proof.cpp
View file

@ -16,15 +16,27 @@ Revision History:
#include "smt/smt_context.h" #include "smt/smt_context.h"
#include "ast/ast_pp.h" #include "ast/ast_pp.h"
#include "ast/ast_ll_pp.h" #include "ast/ast_ll_pp.h"
#include <iostream>
namespace smt { namespace smt {
clause_proof::clause_proof(context& ctx): clause_proof::clause_proof(context& ctx):
ctx(ctx), m(ctx.get_manager()), m_lits(m), m_pp(m) { ctx(ctx), m(ctx.get_manager()), m_lits(m), m_pp(m) {
auto proof_log = ctx.get_fparams().m_proof_log; auto proof_log = ctx.get_fparams().m_proof_log;
m_enabled = ctx.get_fparams().m_clause_proof || proof_log.is_non_empty_string(); m_has_log = proof_log.is_non_empty_string();
if (proof_log.is_non_empty_string()) { m_enabled = ctx.get_fparams().m_clause_proof || m_has_log;
m_pp_out = alloc(std::ofstream, proof_log.str()); }
void clause_proof::init_pp_out() {
if (m_has_log && !m_pp_out) {
static unsigned id = 0;
auto proof_log = ctx.get_fparams().m_proof_log;
std::string log_name = proof_log.str();
if (id > 0)
log_name = std::to_string(id) + log_name;
++id;
m_pp_out = alloc(std::ofstream, log_name);
if (!*m_pp_out) if (!*m_pp_out)
throw default_exception(std::string("Could not open file ") + proof_log.str()); throw default_exception(std::string("Could not open file ") + proof_log.str());
} }
@ -170,14 +182,18 @@ namespace smt {
m_trail.push_back(info(st, v, p)); m_trail.push_back(info(st, v, p));
if (m_on_clause_eh) if (m_on_clause_eh)
m_on_clause_eh(m_on_clause_ctx, p, v.size(), v.data()); m_on_clause_eh(m_on_clause_ctx, p, v.size(), v.data());
if (m_pp_out) { if (m_has_log) {
init_pp_out();
auto& out = *m_pp_out; auto& out = *m_pp_out;
for (auto* e : v) for (auto* e : v)
declare(out, e); declare(out, e);
switch (st) { switch (st) {
case clause_proof::status::assumption: case clause_proof::status::assumption:
display_literals(out << "(assume", v) << ")\n"; if (!p || p->get_decl()->get_name() == "assumption") {
break; display_literals(out << "(assume", v) << ")\n";
break;
}
Z3_fallthrough;
case clause_proof::status::lemma: case clause_proof::status::lemma:
case clause_proof::status::th_lemma: case clause_proof::status::th_lemma:
case clause_proof::status::th_assumption: case clause_proof::status::th_assumption:
@ -191,6 +207,7 @@ namespace smt {
default: default:
UNREACHABLE(); UNREACHABLE();
} }
out.flush();
} }
} }

3
src/smt/smt_clause_proof.h
View file

@ -58,10 +58,13 @@ namespace smt {
expr_ref_vector m_lits; expr_ref_vector m_lits;
vector<info> m_trail; vector<info> m_trail;
bool m_enabled = false; bool m_enabled = false;
bool m_has_log = false;
user_propagator::on_clause_eh_t m_on_clause_eh; user_propagator::on_clause_eh_t m_on_clause_eh;
void* m_on_clause_ctx = nullptr; void* m_on_clause_ctx = nullptr;
ast_pp_util m_pp; ast_pp_util m_pp;
scoped_ptr<std::ofstream> m_pp_out; scoped_ptr<std::ofstream> m_pp_out;
void init_pp_out();
void update(status st, expr_ref_vector& v, proof* p); void update(status st, expr_ref_vector& v, proof* p);
void update(clause& c, status st, proof* p); void update(clause& c, status st, proof* p);

4
src/smt/smt_model_checker.cpp
View file

@ -405,13 +405,15 @@ namespace smt {
m_fparams->m_relevancy_lvl = 0; // no relevancy since the model checking problems are quantifier free m_fparams->m_relevancy_lvl = 0; // no relevancy since the model checking problems are quantifier free
m_fparams->m_case_split_strategy = CS_ACTIVITY; // avoid warning messages about smt.case_split >= 3. m_fparams->m_case_split_strategy = CS_ACTIVITY; // avoid warning messages about smt.case_split >= 3.
m_fparams->m_axioms2files = false; m_fparams->m_axioms2files = false;
m_fparams->m_lemmas2console = false; m_fparams->m_lemmas2console = false;
m_fparams->m_proof_log = symbol::null;
} }
if (!m_aux_context) { if (!m_aux_context) {
symbol logic; symbol logic;
params_ref p; params_ref p;
p.set_bool("solver.axioms2files", false); p.set_bool("solver.axioms2files", false);
p.set_bool("solver.lemmas2console", false); p.set_bool("solver.lemmas2console", false);
p.set_sym("solver.proof.log", symbol::null);
m_aux_context = m_context->mk_fresh(&logic, m_fparams.get(), p); m_aux_context = m_context->mk_fresh(&logic, m_fparams.get(), p);
} }
} }