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

fix #6778

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2023-06-25 21:08:06 -07:00
parent 7c4d098f65
commit b451735aa0
3 changed files with 17 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/api/z3_replayer.cpp
View file

@ -72,7 +72,7 @@ struct z3_replayer::imp {
void check_arg(unsigned pos, value_kind k) const {
if (pos >= m_args.size()) {
TRACE("z3_replayer", tout << "too few arguments " << m_args.size() << " expecting " << kind2string(k) << "\n";);
TRACE("z3_replayer", tout << pos << " too few arguments " << m_args.size() << " expecting " << kind2string(k) << "\n";);
throw z3_replayer_exception("invalid argument reference");
}
if (m_args[pos].m_kind != k) {

1
src/smt/smt_solver.cpp
View file

@ -267,6 +267,7 @@ namespace {
};
void get_unsat_core(expr_ref_vector & r) override {
unsigned sz = m_context.get_unsat_core_size();
for (unsigned i = 0; i < sz; i++) {
r.push_back(m_context.get_unsat_core_expr(i));

15
src/solver/tactic2solver.cpp
View file

@ -25,6 +25,9 @@ Notes:
#include "solver/tactic2solver.h"
#include "solver/solver_na2as.h"
#include "solver/mus.h"
#include "smt/params/smt_params.h"
#include "smt/params/smt_params_helper.hpp"
/**
\brief Simulates the incremental solver interface using a tactic.
@ -48,6 +51,7 @@ class tactic2solver : public solver_na2as {
bool m_produce_proofs;
bool m_produce_unsat_cores;
statistics m_stats;
bool m_minimizing = false;
public:
tactic2solver(ast_manager & m, tactic * t, params_ref const & p, bool produce_proofs, bool produce_models, bool produce_unsat_cores, symbol const & logic);
@ -173,6 +177,7 @@ tactic2solver::~tactic2solver() {
void tactic2solver::updt_params(params_ref const & p) {
solver::updt_params(p);
m_produce_unsat_cores |= p.get_bool("unsat_core", false);
}
void tactic2solver::collect_param_descrs(param_descrs & r) {
@ -309,6 +314,16 @@ void tactic2solver::collect_statistics(statistics & st) const {
void tactic2solver::get_unsat_core(expr_ref_vector & r) {
if (m_result.get()) {
m_result->get_unsat_core(r);
if (!m_minimizing && smt_params_helper(get_params()).core_minimize()) {
flet<bool> minimizing(m_minimizing, true);
mus mus(*this);
mus.add_soft(r.size(), r.data());
expr_ref_vector r2(m);
if (l_true == mus.get_mus(r2)) {
r.reset();
r.append(r2);
}
}
}
}