mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
fixes to maxres/mss
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
b5bbf83847
commit
18b491eee0
|
@ -37,6 +37,7 @@ class inc_sat_solver : public solver {
|
|||
sat::solver m_solver;
|
||||
goal2sat m_goal2sat;
|
||||
params_ref m_params;
|
||||
bool m_optimize_model; // parameter
|
||||
expr_ref_vector m_fmls;
|
||||
expr_ref_vector m_current_fmls;
|
||||
unsigned_vector m_fmls_lim;
|
||||
|
@ -54,10 +55,12 @@ class inc_sat_solver : public solver {
|
|||
expr_ref_vector m_soft;
|
||||
vector<rational> m_weights;
|
||||
|
||||
|
||||
typedef obj_map<expr, sat::literal> dep2asm_t;
|
||||
public:
|
||||
inc_sat_solver(ast_manager& m, params_ref const& p):
|
||||
m(m), m_solver(p,0), m_params(p),
|
||||
m(m), m_solver(p,0),
|
||||
m_params(p), m_optimize_model(false),
|
||||
m_fmls(m), m_current_fmls(m), m_core(m), m_map(m),
|
||||
m_num_scopes(0),
|
||||
m_dep_core(m),
|
||||
|
@ -165,6 +168,7 @@ public:
|
|||
m_params = p;
|
||||
m_params.set_bool("elim_vars", false);
|
||||
m_solver.updt_params(m_params);
|
||||
m_optimize_model = m_params.get_bool("optimize_model", false);
|
||||
}
|
||||
virtual void collect_statistics(statistics & st) const {
|
||||
m_preprocess->collect_statistics(st);
|
||||
|
@ -226,32 +230,26 @@ private:
|
|||
lbool r = internalize_formulas();
|
||||
if (r != l_true) return r;
|
||||
r = internalize_assumptions(soft.size(), soft.c_ptr(), dep2asm);
|
||||
if (r != l_true) return r;
|
||||
sat::literal_vector lits;
|
||||
svector<double> weights;
|
||||
sat::literal lit;
|
||||
|
||||
if (r == l_true) {
|
||||
for (unsigned i = 0; i < soft.size(); ++i) {
|
||||
weights.push_back(m_weights[i].get_double());
|
||||
expr* s = soft[i].get();
|
||||
bool is_neg = m.is_not(s, s);
|
||||
if (!dep2asm.find(s, lit)) {
|
||||
std::cout << "not found: " << mk_pp(s, m) << "\n";
|
||||
dep2asm_t::iterator it = dep2asm.begin(), end = dep2asm.end();
|
||||
for (; it != end; ++it) {
|
||||
std::cout << mk_pp(it->m_key, m) << " " << it->m_value << "\n";
|
||||
}
|
||||
UNREACHABLE();
|
||||
}
|
||||
if (is_neg) {
|
||||
lit.neg();
|
||||
}
|
||||
lits.push_back(lit);
|
||||
for (unsigned i = 0; i < soft.size(); ++i) {
|
||||
weights.push_back(m_weights[i].get_double());
|
||||
expr* s = soft[i].get();
|
||||
if (!dep2asm.find(s, lit)) {
|
||||
IF_VERBOSE(0,
|
||||
verbose_stream() << "not found: " << mk_pp(s, m) << "\n";
|
||||
dep2asm_t::iterator it = dep2asm.begin();
|
||||
dep2asm_t::iterator end = dep2asm.end();
|
||||
for (; it != end; ++it) {
|
||||
verbose_stream() << mk_pp(it->m_key, m) << " " << it->m_value << "\n";
|
||||
}
|
||||
UNREACHABLE(););
|
||||
}
|
||||
m_solver.initialize_soft(lits.size(), lits.c_ptr(), weights.c_ptr());
|
||||
m_params.set_bool("optimize_model", true);
|
||||
m_solver.updt_params(m_params);
|
||||
lits.push_back(lit);
|
||||
}
|
||||
m_solver.initialize_soft(lits.size(), lits.c_ptr(), weights.c_ptr());
|
||||
return r;
|
||||
}
|
||||
|
||||
|
@ -324,12 +322,8 @@ private:
|
|||
m_core.reset();
|
||||
for (unsigned i = 0; i < core.size(); ++i) {
|
||||
expr* e;
|
||||
if (asm2dep.find(core[i].index(), e)) {
|
||||
if (core[i].sign()) {
|
||||
e = m.mk_not(e);
|
||||
}
|
||||
m_core.push_back(e);
|
||||
}
|
||||
VERIFY (asm2dep.find(core[i].index(), e));
|
||||
m_core.push_back(e);
|
||||
}
|
||||
TRACE("opt",
|
||||
dep2asm_t::iterator it = dep2asm.begin();
|
||||
|
|
|
@ -72,14 +72,12 @@ public:
|
|||
enum strategy_t {
|
||||
s_mus,
|
||||
s_mus_mss,
|
||||
s_mus_mss2,
|
||||
s_mss
|
||||
};
|
||||
private:
|
||||
expr_ref_vector m_B;
|
||||
expr_ref_vector m_asms;
|
||||
obj_map<expr, rational> m_asm2weight;
|
||||
obj_map<expr, bool> m_asm2value;
|
||||
ptr_vector<expr> m_new_core;
|
||||
mus m_mus;
|
||||
mss m_mss;
|
||||
|
@ -186,44 +184,6 @@ public:
|
|||
return l_true;
|
||||
}
|
||||
|
||||
lbool mus_mss_solver() {
|
||||
init();
|
||||
init_local();
|
||||
sls();
|
||||
exprs mcs;
|
||||
vector<exprs> cores;
|
||||
while (m_lower < m_upper) {
|
||||
TRACE("opt",
|
||||
display_vec(tout, m_asms.size(), m_asms.c_ptr());
|
||||
s().display(tout);
|
||||
tout << "\n";
|
||||
display(tout);
|
||||
);
|
||||
lbool is_sat = try_improve_bound(cores, mcs);
|
||||
if (m_cancel) {
|
||||
return l_undef;
|
||||
}
|
||||
switch (is_sat) {
|
||||
case l_undef:
|
||||
return l_undef;
|
||||
case l_false:
|
||||
SASSERT(cores.empty() && mcs.empty());
|
||||
m_lower = m_upper;
|
||||
return l_true;
|
||||
case l_true:
|
||||
SASSERT(cores.empty() || mcs.empty());
|
||||
for (unsigned i = 0; i < cores.size(); ++i) {
|
||||
process_unsat(cores[i]);
|
||||
}
|
||||
if (cores.empty()) {
|
||||
process_sat(mcs);
|
||||
}
|
||||
break;
|
||||
}
|
||||
}
|
||||
m_lower = m_upper;
|
||||
return l_true;
|
||||
}
|
||||
|
||||
lbool mss_solver() {
|
||||
init();
|
||||
|
@ -234,6 +194,9 @@ public:
|
|||
lbool is_sat = l_true;
|
||||
while (m_lower < m_upper && is_sat == l_true) {
|
||||
IF_VERBOSE(1, verbose_stream() << "(opt.maxres [" << m_lower << ":" << m_upper << "])\n";);
|
||||
if (m_cancel) {
|
||||
return l_undef;
|
||||
}
|
||||
vector<exprs> cores;
|
||||
exprs mss;
|
||||
model_ref mdl;
|
||||
|
@ -241,6 +204,12 @@ public:
|
|||
mcs.reset();
|
||||
s().get_model(mdl);
|
||||
update_assignment(mdl.get());
|
||||
|
||||
exprs cs;
|
||||
get_current_correction_set(mdl.get(), cs);
|
||||
process_sat(cs);
|
||||
|
||||
#if 0
|
||||
is_sat = get_mss(mdl.get(), cores, mss, mcs);
|
||||
|
||||
switch (is_sat) {
|
||||
|
@ -249,15 +218,12 @@ public:
|
|||
case l_false:
|
||||
m_lower = m_upper;
|
||||
return l_true;
|
||||
case l_true: {
|
||||
case l_true:
|
||||
process_sat(mcs);
|
||||
get_mss_model();
|
||||
break;
|
||||
}
|
||||
}
|
||||
if (m_cancel) {
|
||||
return l_undef;
|
||||
break;
|
||||
}
|
||||
#endif
|
||||
if (m_lower < m_upper) {
|
||||
is_sat = s().check_sat(0, 0);
|
||||
}
|
||||
|
@ -294,7 +260,7 @@ public:
|
|||
Suppose correction set is huge. Do we really need it?
|
||||
|
||||
*/
|
||||
lbool mus_mss2_solver() {
|
||||
lbool mus_mss_solver() {
|
||||
init();
|
||||
init_local();
|
||||
sls();
|
||||
|
@ -356,14 +322,8 @@ public:
|
|||
// obtained from the current best model.
|
||||
//
|
||||
|
||||
//
|
||||
// TBD: throttle blocking on correction sets if they are too big.
|
||||
// likewise, if the cores are too big, don't block the cores.
|
||||
//
|
||||
|
||||
|
||||
exprs cs;
|
||||
get_current_correction_set(cs);
|
||||
get_current_correction_set(mdl.get(), cs);
|
||||
unsigned max_core = max_core_size(cores);
|
||||
if (!cs.empty() && cs.size() < max_core) {
|
||||
process_sat(cs);
|
||||
|
@ -379,7 +339,6 @@ public:
|
|||
|
||||
void found_optimum() {
|
||||
s().get_model(m_model);
|
||||
m_asm2value.reset();
|
||||
DEBUG_CODE(
|
||||
for (unsigned i = 0; i < m_asms.size(); ++i) {
|
||||
SASSERT(is_true(m_asms[i].get()));
|
||||
|
@ -397,8 +356,6 @@ public:
|
|||
return mus_solver();
|
||||
case s_mus_mss:
|
||||
return mus_mss_solver();
|
||||
case s_mus_mss2:
|
||||
return mus_mss2_solver();
|
||||
case s_mss:
|
||||
return mss_solver();
|
||||
}
|
||||
|
@ -462,14 +419,14 @@ public:
|
|||
return is_sat;
|
||||
}
|
||||
|
||||
void get_current_correction_set(exprs& cs) {
|
||||
void get_current_correction_set(model* mdl, exprs& cs) {
|
||||
cs.reset();
|
||||
if (!mdl) return;
|
||||
for (unsigned i = 0; i < m_asms.size(); ++i) {
|
||||
if (!is_true(m_asms[i].get())) {
|
||||
if (!is_true(mdl, m_asms[i].get())) {
|
||||
cs.push_back(m_asms[i].get());
|
||||
}
|
||||
}
|
||||
IF_VERBOSE(2, verbose_stream() << "(opt.maxres correction set size: " << cs.size() << ")\n";);
|
||||
TRACE("opt", display_vec(tout << "new correction set: ", cs.size(), cs.c_ptr()););
|
||||
}
|
||||
|
||||
|
@ -554,7 +511,7 @@ public:
|
|||
IF_VERBOSE(1, verbose_stream() << "(opt.maxres [" << m_lower << ":" << m_upper << "])\n";);
|
||||
}
|
||||
|
||||
void get_mus_model(model_ref& mdl) {
|
||||
bool get_mus_model(model_ref& mdl) {
|
||||
rational w(0);
|
||||
if (m_c.sat_enabled()) {
|
||||
// SAT solver core extracts some model
|
||||
|
@ -567,6 +524,7 @@ public:
|
|||
if (mdl.get() && w < m_upper) {
|
||||
update_assignment(mdl.get());
|
||||
}
|
||||
return 0 != mdl.get();
|
||||
}
|
||||
|
||||
void get_mss_model() {
|
||||
|
@ -682,17 +640,13 @@ public:
|
|||
s().assert_expr(fml);
|
||||
fml = m.mk_implies(dd, b_i);
|
||||
s().assert_expr(fml);
|
||||
m_asm2value.insert(dd, is_true(d) && is_true(b_i));
|
||||
d = dd;
|
||||
}
|
||||
else {
|
||||
dd = m.mk_and(b_i, d);
|
||||
m_asm2value.insert(dd, is_true(d) && is_true(b_i));
|
||||
m_trail.push_back(dd);
|
||||
d = dd;
|
||||
d = m.mk_and(b_i, d);
|
||||
m_trail.push_back(d);
|
||||
}
|
||||
asum = mk_fresh_bool("a");
|
||||
m_asm2value.insert(asum, is_true(b_i1) || is_true(d));
|
||||
cls = m.mk_or(b_i1, d);
|
||||
fml = m.mk_implies(asum, cls);
|
||||
new_assumption(asum, w);
|
||||
|
@ -809,7 +763,6 @@ public:
|
|||
return l_undef;
|
||||
}
|
||||
|
||||
|
||||
void update_assignment(model* mdl) {
|
||||
rational upper(0);
|
||||
expr_ref tmp(m);
|
||||
|
@ -826,7 +779,6 @@ public:
|
|||
return;
|
||||
}
|
||||
m_model = mdl;
|
||||
m_asm2value.reset();
|
||||
|
||||
for (unsigned i = 0; i < m_soft.size(); ++i) {
|
||||
m_assignment[i] = is_true(m_soft[i].get());
|
||||
|
@ -851,16 +803,16 @@ public:
|
|||
s().assert_expr(fml);
|
||||
}
|
||||
|
||||
bool is_true(expr* e) {
|
||||
bool truth_value;
|
||||
if (m_asm2value.find(e, truth_value)) {
|
||||
return truth_value;
|
||||
}
|
||||
bool is_true(model* mdl, expr* e) {
|
||||
expr_ref tmp(m);
|
||||
VERIFY(m_model->eval(e, tmp));
|
||||
VERIFY(mdl->eval(e, tmp));
|
||||
return m.is_true(tmp);
|
||||
}
|
||||
|
||||
bool is_true(expr* e) {
|
||||
return is_true(m_model.get(), e);
|
||||
}
|
||||
|
||||
void remove_soft(exprs const& core, expr_ref_vector& asms) {
|
||||
for (unsigned i = 0; i < asms.size(); ++i) {
|
||||
if (core.contains(asms[i].get())) {
|
||||
|
@ -933,7 +885,7 @@ opt::maxsmt_solver_base* opt::mk_maxres(
|
|||
|
||||
opt::maxsmt_solver_base* opt::mk_mus_mss_maxres(
|
||||
context& c, weights_t& ws, expr_ref_vector const& soft) {
|
||||
return alloc(maxres, c, ws, soft, maxres::s_mus_mss2);
|
||||
return alloc(maxres, c, ws, soft, maxres::s_mus_mss);
|
||||
}
|
||||
|
||||
opt::maxsmt_solver_base* opt::mk_mss_maxres(
|
||||
|
|
|
@ -70,6 +70,7 @@ struct mus::imp {
|
|||
|
||||
lbool get_mus(unsigned_vector& mus) {
|
||||
// SASSERT: mus does not have duplicates.
|
||||
m_model.reset();
|
||||
unsigned_vector core;
|
||||
for (unsigned i = 0; i < m_cls2expr.size(); ++i) {
|
||||
core.push_back(i);
|
||||
|
|
|
@ -465,9 +465,13 @@ namespace opt {
|
|||
|
||||
void context::enable_sls(expr_ref_vector const& soft, vector<rational> const& weights) {
|
||||
SASSERT(soft.size() == weights.size());
|
||||
if (m_enable_sls && m_sat_solver.get()) {
|
||||
if (m_sat_solver.get()) {
|
||||
set_soft_inc_sat(m_sat_solver.get(), soft.size(), soft.c_ptr(), weights.c_ptr());
|
||||
}
|
||||
if (m_enable_sls && m_sat_solver.get()) {
|
||||
m_params.set_bool("optimize_model", true);
|
||||
m_sat_solver->updt_params(m_params);
|
||||
}
|
||||
}
|
||||
|
||||
struct context::is_bv {
|
||||
|
|
|
@ -32,6 +32,7 @@ namespace sat {
|
|||
m_core.reset();
|
||||
m_mus.reset();
|
||||
m_model.reset();
|
||||
m_best_value = 0;
|
||||
}
|
||||
|
||||
void mus::set_core() {
|
||||
|
@ -96,8 +97,15 @@ namespace sat {
|
|||
if (!core.empty()) {
|
||||
// mr(); // TBD: measure
|
||||
}
|
||||
double new_value = s.m_wsls.evaluate_model(s.m_model);
|
||||
if (m_model.empty()) {
|
||||
m_model.append(s.m_model);
|
||||
m_best_value = new_value;
|
||||
}
|
||||
else if (m_best_value > new_value) {
|
||||
m_model.reset();
|
||||
m_model.append(s.m_model);
|
||||
m_best_value = new_value;
|
||||
}
|
||||
break;
|
||||
}
|
||||
|
|
|
@ -25,6 +25,7 @@ namespace sat {
|
|||
literal_vector m_mus;
|
||||
bool m_is_active;
|
||||
model m_model; // model obtained during minimal unsat core
|
||||
double m_best_value;
|
||||
|
||||
|
||||
solver& s;
|
||||
|
|
|
@ -354,7 +354,7 @@ namespace sat {
|
|||
//
|
||||
// Initialize m_clause_weights, m_hscore, m_sscore.
|
||||
//
|
||||
m_best_value = m_false.empty()?evaluate_model():-1.0;
|
||||
m_best_value = m_false.empty()?evaluate_model(m_model):-1.0;
|
||||
m_best_model.reset();
|
||||
m_clause_weights.reset();
|
||||
m_hscore.reset();
|
||||
|
@ -382,7 +382,7 @@ namespace sat {
|
|||
for (; !m_cancel && m_best_value > 0 && i < m_max_tries; ++i) {
|
||||
wflip();
|
||||
if (m_false.empty()) {
|
||||
double val = evaluate_model();
|
||||
double val = evaluate_model(m_model);
|
||||
if (val < m_best_value || m_best_value < 0.0) {
|
||||
m_best_value = val;
|
||||
m_best_model.reset();
|
||||
|
@ -511,12 +511,12 @@ namespace sat {
|
|||
DEBUG_CODE(check_invariant(););
|
||||
}
|
||||
|
||||
double wsls::evaluate_model() {
|
||||
double wsls::evaluate_model(model& mdl) {
|
||||
SASSERT(m_false.empty());
|
||||
double result = 0.0;
|
||||
for (unsigned i = 0; i < m_soft.size(); ++i) {
|
||||
literal lit = m_soft[i];
|
||||
if (value_at(lit, m_model) != l_true) {
|
||||
if (value_at(lit, mdl) != l_true) {
|
||||
result += m_weights[i];
|
||||
}
|
||||
}
|
||||
|
|
|
@ -99,12 +99,12 @@ namespace sat {
|
|||
void opt(unsigned sz, literal const* tabu, bool reuse_model);
|
||||
model const& get_model() { return m_best_model; }
|
||||
virtual void display(std::ostream& out) const;
|
||||
double evaluate_model(model& mdl);
|
||||
private:
|
||||
void wflip();
|
||||
void wflip(literal lit);
|
||||
void update_hard_weights();
|
||||
bool pick_wflip(literal & lit);
|
||||
double evaluate_model();
|
||||
virtual void check_invariant();
|
||||
void refresh_scores(bool_var v);
|
||||
int compute_hscore(bool_var v);
|
||||
|
|
|
@ -1737,7 +1737,7 @@ namespace sat {
|
|||
|
||||
m_mus(); // ignore return value on cancelation.
|
||||
m_model.reset();
|
||||
m_model.append(m_mus.get_model());
|
||||
m_model.append(m_mus.get_model());
|
||||
}
|
||||
}
|
||||
|
||||
|
|
|
@ -372,7 +372,9 @@ struct goal2sat::imp {
|
|||
SASSERT(m_result_stack.empty());
|
||||
}
|
||||
|
||||
void insert_dep(expr* dep, bool sign) {
|
||||
void insert_dep(expr* dep0, expr* dep, bool sign) {
|
||||
SASSERT(sign || dep0 == dep); // !sign || (not dep0) == dep.
|
||||
SASSERT(!sign || m.is_not(dep0));
|
||||
expr_ref new_dep(m), fml(m);
|
||||
if (is_uninterp_const(dep)) {
|
||||
new_dep = dep;
|
||||
|
@ -386,7 +388,7 @@ struct goal2sat::imp {
|
|||
}
|
||||
convert_atom(new_dep, false, false);
|
||||
sat::literal lit = m_result_stack.back();
|
||||
m_dep2asm.insert(dep, sign?(~lit):lit);
|
||||
m_dep2asm.insert(dep0, sign?~lit:lit);
|
||||
m_result_stack.pop_back();
|
||||
}
|
||||
|
||||
|
@ -411,7 +413,7 @@ struct goal2sat::imp {
|
|||
SASSERT(m.is_bool(d));
|
||||
bool sign = m.is_not(d, d1);
|
||||
|
||||
insert_dep(d1, sign);
|
||||
insert_dep(d, d1, sign);
|
||||
if (d == f) {
|
||||
goto skip_dep;
|
||||
}
|
||||
|
|
Loading…
Reference in a new issue