mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
break on small cores
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
f020b7c7b8
commit
8141dadc89
|
@ -291,10 +291,10 @@ extern "C" {
|
|||
}
|
||||
}
|
||||
else {
|
||||
model_ref _m;
|
||||
m_solver.get()->get_model(_m);
|
||||
model_ref mr;
|
||||
m_solver.get()->get_model(mr);
|
||||
Z3_model_ref *crap = alloc(Z3_model_ref);
|
||||
crap->m_model = _m.get();
|
||||
crap->m_model = mr.get();
|
||||
mk_c(c)->save_object(crap);
|
||||
*model = of_model(crap);
|
||||
}
|
||||
|
|
|
@ -141,7 +141,7 @@ namespace simplex {
|
|||
void unset_upper(var_t var);
|
||||
void set_value(var_t var, eps_numeral const& b);
|
||||
void set_cancel(bool f) { m_cancel = f; }
|
||||
void set_max_iterations(unsigned m) { m_max_iterations = m; }
|
||||
void set_max_iterations(unsigned n) { m_max_iterations = n; }
|
||||
void reset();
|
||||
lbool make_feasible();
|
||||
lbool minimize(var_t var);
|
||||
|
|
|
@ -100,7 +100,7 @@ namespace simplex {
|
|||
_row_entry & add_row_entry(unsigned & pos_idx);
|
||||
void del_row_entry(unsigned idx);
|
||||
void compress(manager& m, vector<column> & cols);
|
||||
void compress_if_needed(manager& m, vector<column> & cols);
|
||||
void compress_if_needed(manager& _m, vector<column> & cols);
|
||||
void save_var_pos(svector<int> & result_map, unsigned_vector& idxs) const;
|
||||
//bool is_coeff_of(var_t v, numeral const & expected) const;
|
||||
int get_idx_of(var_t v) const;
|
||||
|
@ -143,7 +143,7 @@ namespace simplex {
|
|||
|
||||
public:
|
||||
|
||||
sparse_matrix(manager& m): m(m) {}
|
||||
sparse_matrix(manager& _m): m(_m) {}
|
||||
~sparse_matrix();
|
||||
void reset();
|
||||
|
||||
|
|
|
@ -190,11 +190,11 @@ public:
|
|||
r.reset();
|
||||
r.append(m_core.size(), m_core.c_ptr());
|
||||
}
|
||||
virtual void get_model(model_ref & m) {
|
||||
virtual void get_model(model_ref & mdl) {
|
||||
if (!m_model.get()) {
|
||||
extract_model();
|
||||
}
|
||||
m = m_model;
|
||||
mdl = m_model;
|
||||
}
|
||||
virtual proof * get_proof() {
|
||||
UNREACHABLE();
|
||||
|
@ -331,10 +331,10 @@ private:
|
|||
}
|
||||
sat::literal_vector const& core = m_solver.get_core();
|
||||
TRACE("opt",
|
||||
dep2asm_t::iterator it = dep2asm.begin();
|
||||
dep2asm_t::iterator end = dep2asm.end();
|
||||
for (; it != end; ++it) {
|
||||
tout << mk_pp(it->m_key, m) << " |-> " << sat::literal(it->m_value) << "\n";
|
||||
dep2asm_t::iterator it2 = dep2asm.begin();
|
||||
dep2asm_t::iterator end2 = dep2asm.end();
|
||||
for (; it2 != end2; ++it2) {
|
||||
tout << mk_pp(it2->m_key, m) << " |-> " << sat::literal(it2->m_value) << "\n";
|
||||
}
|
||||
tout << "core: ";
|
||||
for (unsigned i = 0; i < core.size(); ++i) {
|
||||
|
|
|
@ -58,7 +58,8 @@ struct mus::imp {
|
|||
unsigned idx = m_cls2expr.size();
|
||||
m_expr2cls.insert(cls, idx);
|
||||
m_cls2expr.push_back(cls);
|
||||
TRACE("opt", tout << idx << ": " << mk_pp(cls, m) << "\n";);
|
||||
TRACE("opt", tout << idx << ": " << mk_pp(cls, m) << "\n";
|
||||
display_vec(tout, m_cls2expr););
|
||||
return idx;
|
||||
}
|
||||
|
||||
|
@ -113,6 +114,11 @@ struct mus::imp {
|
|||
core.push_back(cls_id);
|
||||
}
|
||||
}
|
||||
TRACE("opt", display_vec(tout << "core exprs:", core_exprs);
|
||||
display_vec(tout << "core:", core);
|
||||
display_vec(tout << "mus:", mus);
|
||||
);
|
||||
|
||||
}
|
||||
break;
|
||||
}
|
||||
|
@ -144,6 +150,21 @@ struct mus::imp {
|
|||
out << "\n";
|
||||
}
|
||||
|
||||
void display_vec(std::ostream& out, expr_ref_vector const& v) const {
|
||||
for (unsigned i = 0; i < v.size(); ++i) {
|
||||
out << mk_pp(v[i], m) << " ";
|
||||
}
|
||||
out << "\n";
|
||||
}
|
||||
|
||||
|
||||
void display_vec(std::ostream& out, ptr_vector<expr> const& v) const {
|
||||
for (unsigned i = 0; i < v.size(); ++i) {
|
||||
out << mk_pp(v[i], m) << " ";
|
||||
}
|
||||
out << "\n";
|
||||
}
|
||||
|
||||
void set_soft(unsigned sz, expr* const* soft, rational const* weights) {
|
||||
m_model.reset();
|
||||
m_weight.reset();
|
||||
|
|
|
@ -146,9 +146,9 @@ namespace opt {
|
|||
virtual void cancel() { set_cancel(true); }
|
||||
virtual void set_hard_constraints(ptr_vector<expr> & hard);
|
||||
virtual lbool optimize();
|
||||
virtual void get_model(model_ref& m);
|
||||
virtual void set_model(model_ref& m);
|
||||
virtual void fix_model(model_ref& m);
|
||||
virtual void get_model(model_ref& _m);
|
||||
virtual void set_model(model_ref& _m);
|
||||
virtual void fix_model(model_ref& _m);
|
||||
virtual void collect_statistics(statistics& stats) const;
|
||||
virtual proof* get_proof() { return 0; }
|
||||
virtual void get_labels(svector<symbol> & r) {}
|
||||
|
@ -186,7 +186,7 @@ namespace opt {
|
|||
void set_enable_sls(bool f) { m_enable_sls = f; }
|
||||
void set_soft_assumptions();
|
||||
symbol const& maxsat_engine() const { return m_maxsat_engine; }
|
||||
void get_base_model(model_ref& m);
|
||||
void get_base_model(model_ref& _m);
|
||||
|
||||
|
||||
private:
|
||||
|
|
|
@ -94,7 +94,7 @@ namespace opt {
|
|||
virtual void pop_core(unsigned n);
|
||||
virtual lbool check_sat_core(unsigned num_assumptions, expr * const * assumptions);
|
||||
virtual void get_unsat_core(ptr_vector<expr> & r);
|
||||
virtual void get_model(model_ref & m);
|
||||
virtual void get_model(model_ref & _m);
|
||||
virtual proof * get_proof();
|
||||
virtual std::string reason_unknown() const;
|
||||
virtual void get_labels(svector<symbol> & r);
|
||||
|
|
|
@ -923,9 +923,28 @@ namespace sat {
|
|||
m_assumption_set.insert(lit);
|
||||
|
||||
if (m_config.m_soft_assumptions) {
|
||||
if (value(lit) == l_undef) {
|
||||
switch(value(lit)) {
|
||||
case l_undef:
|
||||
m_assumptions.push_back(lit);
|
||||
assign(lit, justification());
|
||||
break;
|
||||
case l_false: {
|
||||
set_conflict(lit);
|
||||
flet<bool> _min1(m_config.m_minimize_core, false);
|
||||
flet<bool> _min2(m_config.m_minimize_core_partial, false);
|
||||
resolve_conflict_for_unsat_core();
|
||||
SASSERT(m_core.size() <= m_assumptions.size());
|
||||
if (m_core.size() <= 3 ||
|
||||
m_core.size() <= i - m_assumptions.size() + 1) {
|
||||
return;
|
||||
}
|
||||
else {
|
||||
m_inconsistent = false;
|
||||
}
|
||||
break;
|
||||
}
|
||||
case l_true:
|
||||
break;
|
||||
}
|
||||
propagate(false);
|
||||
}
|
||||
|
|
|
@ -370,7 +370,12 @@ namespace smt {
|
|||
tout << "conflict_lvl: " << m_conflict_lvl << " scope_lvl: " << m_ctx.get_scope_level() << " base_lvl: " << m_ctx.get_base_level()
|
||||
<< " search_lvl: " << m_ctx.get_search_level() << "\n";
|
||||
tout << "js.kind: " << js.get_kind() << "\n";
|
||||
m_ctx.display_literal(tout, consequent); tout << "\n";);
|
||||
tout << "consequent: " << consequent << "\n";
|
||||
for (unsigned i = 0; i < m_assigned_literals.size(); ++i) {
|
||||
tout << m_assigned_literals[i] << " ";
|
||||
}
|
||||
tout << "\n";
|
||||
);
|
||||
|
||||
// m_conflict_lvl can be smaller than m_ctx.get_search_level() when:
|
||||
// there are user level scopes created using the Z3 API, and
|
||||
|
@ -1310,8 +1315,11 @@ namespace smt {
|
|||
}
|
||||
|
||||
void conflict_resolution::process_antecedent_for_unsat_core(literal antecedent) {
|
||||
TRACE("conflict", tout << "processing antecedent: "; m_ctx.display_literal(tout, antecedent); tout << "\n";);
|
||||
bool_var var = antecedent.var();
|
||||
TRACE("conflict", tout << "processing antecedent: ";
|
||||
m_ctx.display_literal_info(tout << antecedent << " ", antecedent);
|
||||
tout << (m_ctx.is_marked(var)?"marked":"not marked");
|
||||
tout << "\n";);
|
||||
|
||||
if (!m_ctx.is_marked(var)) {
|
||||
m_ctx.set_mark(var);
|
||||
|
@ -1341,13 +1349,14 @@ namespace smt {
|
|||
|
||||
b_justification js = conflict;
|
||||
literal consequent = false_literal;
|
||||
if (not_l != null_literal)
|
||||
if (not_l != null_literal) {
|
||||
consequent = ~not_l;
|
||||
}
|
||||
|
||||
int idx = skip_literals_above_conflict_level();
|
||||
|
||||
if (not_l != null_literal)
|
||||
process_antecedent_for_unsat_core(not_l);
|
||||
process_antecedent_for_unsat_core(consequent);
|
||||
|
||||
if (m_assigned_literals.empty()) {
|
||||
goto end_unsat_core;
|
||||
|
|
|
@ -103,9 +103,9 @@ namespace smt {
|
|||
void context::display_literal_info(std::ostream & out, literal l) const {
|
||||
l.display_compact(out, m_bool_var2expr.c_ptr());
|
||||
if (l.sign())
|
||||
out << " (not " << mk_bounded_pp(bool_var2expr(l.var()), m_manager, 10) << ")\n";
|
||||
out << " (not " << mk_bounded_pp(bool_var2expr(l.var()), m_manager, 10) << ") ";
|
||||
else
|
||||
out << " " << mk_bounded_pp(bool_var2expr(l.var()), m_manager, 10) << "\n";
|
||||
out << " " << mk_bounded_pp(bool_var2expr(l.var()), m_manager, 10) << " ";
|
||||
out << "relevant: " << is_relevant(bool_var2expr(l.var())) << ", val: " << get_assignment(l) << "\n";
|
||||
}
|
||||
|
||||
|
|
|
@ -72,7 +72,7 @@ public:
|
|||
|
||||
void insert(func_decl* p, expr* body) { m_funcs.push_back(p); m_bodies.push_back(body); }
|
||||
|
||||
virtual void operator()(model_ref& m);
|
||||
virtual void operator()(model_ref& _m);
|
||||
|
||||
virtual model_converter * translate(ast_translation & translator);
|
||||
|
||||
|
|
|
@ -30,11 +30,11 @@ class replace_proof_converter : public proof_converter {
|
|||
proof_ref_vector m_proofs;
|
||||
public:
|
||||
|
||||
replace_proof_converter(ast_manager& m): m(m), m_proofs(m) {}
|
||||
replace_proof_converter(ast_manager& _m): m(_m), m_proofs(m) {}
|
||||
|
||||
virtual ~replace_proof_converter() {}
|
||||
|
||||
virtual void operator()(ast_manager & m, unsigned num_source, proof * const * source, proof_ref & result);
|
||||
virtual void operator()(ast_manager & _m, unsigned num_source, proof * const * source, proof_ref & result);
|
||||
|
||||
virtual proof_converter * translate(ast_translation & translator);
|
||||
|
||||
|
|
|
@ -171,7 +171,7 @@ public:
|
|||
m_todo.push_back(d);
|
||||
unsigned qhead = 0;
|
||||
while (qhead < m_todo.size()) {
|
||||
dependency * d = m_todo[qhead];
|
||||
d = m_todo[qhead];
|
||||
qhead++;
|
||||
if (d->is_leaf()) {
|
||||
if (to_leaf(d)->m_value == v) {
|
||||
|
@ -201,7 +201,7 @@ public:
|
|||
m_todo.push_back(d);
|
||||
unsigned qhead = 0;
|
||||
while (qhead < m_todo.size()) {
|
||||
dependency * d = m_todo[qhead];
|
||||
d = m_todo[qhead];
|
||||
qhead++;
|
||||
if (d->is_leaf()) {
|
||||
vs.push_back(to_leaf(d)->m_value);
|
||||
|
|
|
@ -46,7 +46,7 @@ class mpf {
|
|||
mpz significand;
|
||||
mpf_exp_t exponent;
|
||||
mpf & operator=(mpf const & other) { UNREACHABLE(); return *this; }
|
||||
void set(unsigned ebits, unsigned sbits);
|
||||
void set(unsigned _ebits, unsigned _sbits);
|
||||
public:
|
||||
mpf();
|
||||
mpf(unsigned ebits, unsigned sbits);
|
||||
|
|
Loading…
Reference in a new issue