mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
add clause proof module, small improvements to bapa
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
f128398bf9
commit
fc4c162e31
|
@ -110,7 +110,11 @@ public:
|
|||
extract_clauses_and_dependencies(in, clauses, assumptions, bool2dep, fmc);
|
||||
ref<solver> local_solver = m_solver->translate(m, m_params);
|
||||
local_solver->assert_expr(clauses);
|
||||
TRACE("solver2tactic", tout << "clauses asserted\n";);
|
||||
lbool r = local_solver->check_sat(assumptions.size(), assumptions.c_ptr());
|
||||
TRACE("solver2tactic", tout << "check sat result " << r << "\n";);
|
||||
proof* pr = local_solver->get_proof();
|
||||
if (pr) in->set(proof2proof_converter(m, pr));
|
||||
switch (r) {
|
||||
case l_true:
|
||||
if (in->models_enabled()) {
|
||||
|
@ -128,11 +132,6 @@ public:
|
|||
case l_false: {
|
||||
in->reset();
|
||||
expr_dependency_ref lcore(m);
|
||||
proof* pr = nullptr;
|
||||
if (in->proofs_enabled()) {
|
||||
pr = local_solver->get_proof();
|
||||
in->set(proof2proof_converter(m, pr));
|
||||
}
|
||||
if (in->unsat_core_enabled()) {
|
||||
expr_ref_vector core(m);
|
||||
local_solver->get_unsat_core(core);
|
||||
|
|
|
@ -196,12 +196,14 @@ lbool tactic2solver::check_sat_core2(unsigned num_assumptions, expr * const * as
|
|||
}
|
||||
catch (z3_error & ex) {
|
||||
TRACE("tactic2solver", tout << "exception: " << ex.msg() << "\n";);
|
||||
m_result->m_proof = pr;
|
||||
throw ex;
|
||||
}
|
||||
catch (z3_exception & ex) {
|
||||
TRACE("tactic2solver", tout << "exception: " << ex.msg() << "\n";);
|
||||
m_result->set_status(l_undef);
|
||||
m_result->m_unknown = ex.msg();
|
||||
m_result->m_proof = pr;
|
||||
}
|
||||
m_tactic->collect_statistics(m_result->m_stats);
|
||||
m_tactic->collect_statistics(m_stats);
|
||||
|
|
Loading…
Reference in a new issue