mirror of
https://github.com/Z3Prover/z3
synced 2025-04-16 05:48:44 +00:00
bugfixes to hsmax
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner
parent
5427964c54
commit
7fbe7124f9
|
|
@ -71,23 +71,6 @@ namespace pdr {
|
|||
virtual expr* get_unsat_core_expr(unsigned i) { return m_context.get_unsat_core_expr(i); }
|
||||
};
|
||||
|
||||
// TBD:
|
||||
class sat_context : public smt_context {
|
||||
sat::solver m_solver;
|
||||
public:
|
||||
sat_context(smt::kernel & ctx, smt_context_manager& p, app* pred);
|
||||
virtual ~sat_context() {}
|
||||
virtual void assert_expr(expr* e);
|
||||
virtual lbool check(expr_ref_vector& assumptions);
|
||||
virtual void get_model(model_ref& model);
|
||||
virtual proof* get_proof();
|
||||
virtual void pop() { m_solver.pop(1); }
|
||||
virtual void push() { m_solver.push(); }
|
||||
// TBD: add unsat core extraction with sat::solver.
|
||||
virtual unsigned get_unsat_core_size();
|
||||
virtual expr* get_unsat_core_expr(unsigned i);
|
||||
};
|
||||
|
||||
class smt_context_manager {
|
||||
smt_params& m_fparams;
|
||||
ast_manager& m;
|
||||
|
|
|
|||
|
|
@ -110,7 +110,8 @@ namespace opt {
|
|||
|
||||
lbool compute_lower() {
|
||||
m_lower.reset();
|
||||
if (L1() && L2() && L3()) {
|
||||
// L3() disabled: mostly a waste of time.
|
||||
if (L1() && L2()) {
|
||||
return l_true;
|
||||
}
|
||||
else {
|
||||
|
|
@ -238,7 +239,9 @@ namespace opt {
|
|||
lbool U1() {
|
||||
scoped_select _sc(*this);
|
||||
while (true) {
|
||||
if (!compute_U1()) return l_undef;
|
||||
if (!compute_U1()) {
|
||||
return l_undef;
|
||||
}
|
||||
unsigned i = 0, j = 0;
|
||||
set_undef_to_false();
|
||||
if (values_satisfy_Ts(i)) {
|
||||
|
|
@ -251,7 +254,7 @@ namespace opt {
|
|||
// literal to true.
|
||||
//
|
||||
|
||||
IF_VERBOSE(1, verbose_stream() << "(hs.refining exclusion set " << i << "\n";);
|
||||
IF_VERBOSE(1, verbose_stream() << "(hs.refining exclusion set " << i << ")\n";);
|
||||
set const& T = m_T[i];
|
||||
rational max_value(0);
|
||||
j = 0;
|
||||
|
|
@ -270,7 +273,7 @@ namespace opt {
|
|||
if (l_false != selected(S[j])) break;
|
||||
}
|
||||
if (j == S.size()) {
|
||||
IF_VERBOSE(1, verbose_stream() << "approximation failed, fall back to SAT\n";);
|
||||
IF_VERBOSE(1, verbose_stream() << "(hs.fallback-to-SAT)\n";);
|
||||
return compute_U2();
|
||||
}
|
||||
}
|
||||
|
|
@ -327,7 +330,7 @@ namespace opt {
|
|||
m_value_saved.reset();
|
||||
m_value_saved.append(m_value);
|
||||
if (m_upper > m_max_weight) {
|
||||
IF_VERBOSE(0, verbose_stream() << "got worse upper bound\n";);
|
||||
IF_VERBOSE(1, verbose_stream() << "(hs.bound_degradation " << m_upper << " )\n";);
|
||||
}
|
||||
return !m_cancel;
|
||||
}
|
||||
|
|
|
|||
|
|
@ -686,8 +686,9 @@ namespace opt {
|
|||
case l_true:
|
||||
seed2hs(false, hs);
|
||||
break;
|
||||
case l_false:
|
||||
case l_false:
|
||||
TRACE("opt", tout << "no more seeds\n";);
|
||||
IF_VERBOSE(1, verbose_stream() << "(wmaxsat.maxhs.no-more-seeds)\n";);
|
||||
m_lower = m_upper;
|
||||
return l_true;
|
||||
case l_undef:
|
||||
|
|
@ -696,6 +697,7 @@ namespace opt {
|
|||
break;
|
||||
}
|
||||
case l_false:
|
||||
IF_VERBOSE(1, verbose_stream() << "(wmaxsat.maxhs.no-more-cores)\n";);
|
||||
TRACE("opt", tout << "no more cores\n";);
|
||||
m_lower = m_upper;
|
||||
return l_true;
|
||||
|
|
@ -825,7 +827,7 @@ namespace opt {
|
|||
// Auxiliary Algorithm 10 for producing cores.
|
||||
//
|
||||
lbool generate_cores(ptr_vector<expr>& hs) {
|
||||
bool core = false;
|
||||
bool core = !m_at_lower_bound;
|
||||
while (true) {
|
||||
hs2seed(hs);
|
||||
lbool is_sat = check_subset();
|
||||
|
|
@ -869,25 +871,6 @@ namespace opt {
|
|||
}
|
||||
}
|
||||
|
||||
lbool next_seed(ptr_vector<expr>& hs, lbool core_found) {
|
||||
|
||||
if (core_found == l_false && m_at_lower_bound) {
|
||||
return l_true;
|
||||
}
|
||||
lbool is_sat = next_seed();
|
||||
switch(is_sat) {
|
||||
case l_true:
|
||||
seed2hs(false, hs);
|
||||
return m_at_lower_bound?l_true:l_false;
|
||||
case l_false:
|
||||
TRACE("opt", tout << "no more seeds\n";);
|
||||
return l_true;
|
||||
case l_undef:
|
||||
return l_undef;
|
||||
}
|
||||
return l_undef;
|
||||
}
|
||||
|
||||
//
|
||||
// retrieve the next seed that satisfies state of hs.
|
||||
// state of hs must be satisfiable before optimization is called.
|
||||
|
|
@ -922,9 +905,6 @@ namespace opt {
|
|||
//
|
||||
// check assignment returned by HS with the original
|
||||
// hard constraints.
|
||||
// If the assignment is consistent with the hard constraints
|
||||
// update the current model, otherwise, update the current lower
|
||||
// bound.
|
||||
//
|
||||
lbool check_subset() {
|
||||
TRACE("opt", tout << "\n";);
|
||||
|
|
@ -935,19 +915,7 @@ namespace opt {
|
|||
ensure_active(i);
|
||||
}
|
||||
}
|
||||
lbool is_sat = s().check_sat(m_asms.size(), m_asms.c_ptr());
|
||||
switch (is_sat) {
|
||||
case l_true:
|
||||
update_model();
|
||||
break;
|
||||
case l_false:
|
||||
break;
|
||||
default:
|
||||
break;
|
||||
}
|
||||
TRACE("opt", tout << is_sat << "\n";);
|
||||
|
||||
return is_sat;
|
||||
return s().check_sat(m_asms.size(), m_asms.c_ptr());
|
||||
}
|
||||
|
||||
//
|
||||
|
|
@ -957,18 +925,17 @@ namespace opt {
|
|||
//
|
||||
bool grow() {
|
||||
scoped_stopwatch _sw(m_stats.m_model_expansion_time);
|
||||
model_ref mdl;
|
||||
s().get_model(mdl);
|
||||
for (unsigned i = 0; i < num_soft(); ++i) {
|
||||
if (!m_seed[i]) {
|
||||
if (is_true(m_model, m_soft[i].get())) {
|
||||
if (is_true(mdl, m_soft[i].get())) {
|
||||
m_seed[i] = true;
|
||||
}
|
||||
else {
|
||||
ensure_active(i);
|
||||
m_asms.push_back(m_aux[i].get());
|
||||
lbool is_sat = s().check_sat(m_asms.size(), m_asms.c_ptr());
|
||||
IF_VERBOSE(3, verbose_stream()
|
||||
<< "check: " << mk_pp(m_asms.back(), m)
|
||||
<< ":" << is_sat << "\n";);
|
||||
TRACE("opt", tout
|
||||
<< "check: " << mk_pp(m_asms.back(), m)
|
||||
<< ":" << is_sat << "\n";);
|
||||
|
|
@ -981,9 +948,7 @@ namespace opt {
|
|||
break;
|
||||
case l_true:
|
||||
++m_stats.m_num_model_expansions_success;
|
||||
update_model();
|
||||
TRACE("opt", model_smt2_pp(tout << mk_pp(m_aux[i].get(), m) << "\n",
|
||||
m, *(m_model.get()), 0););
|
||||
s().get_model(mdl);
|
||||
m_seed[i] = true;
|
||||
break;
|
||||
}
|
||||
|
|
@ -999,7 +964,12 @@ namespace opt {
|
|||
if (upper < m_upper) {
|
||||
m_upper = upper;
|
||||
m_hs.set_upper(upper);
|
||||
TRACE("opt", tout << "new upper: " << m_upper << "\n";);
|
||||
m_model = mdl;
|
||||
m_assignment.reset();
|
||||
m_assignment.append(m_seed);
|
||||
TRACE("opt",
|
||||
tout << "new upper: " << m_upper << "\n";
|
||||
model_smt2_pp(tout, m, *(mdl.get()), 0););
|
||||
}
|
||||
return true;
|
||||
}
|
||||
|
|
@ -1049,13 +1019,6 @@ namespace opt {
|
|||
return true;
|
||||
}
|
||||
|
||||
void update_model() {
|
||||
s().get_model(m_model);
|
||||
for (unsigned i = 0; i < num_soft(); ++i) {
|
||||
m_assignment[i] = is_true(m_model, m_soft[i].get());
|
||||
}
|
||||
}
|
||||
|
||||
void print_asms(std::ostream& out, ptr_vector<expr> const& asms) {
|
||||
for (unsigned j = 0; j < asms.size(); ++j) {
|
||||
out << mk_pp(asms[j], m) << " ";
|
||||
|
|
|
|||
|
|
@ -339,8 +339,8 @@ namespace sat {
|
|||
// Backtracking
|
||||
//
|
||||
// -----------------------
|
||||
public:
|
||||
void push();
|
||||
public:
|
||||
void pop(unsigned num_scopes);
|
||||
|
||||
protected:
|
||||
|
|
|
|||
Loading…
Reference in a new issue