mirror of
https://github.com/Z3Prover/z3
synced 2025-11-04 05:19:11 +00:00
sls testing
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner
parent
c148272cc4
commit
39ac22c37e
3 changed files with 121 additions and 84 deletions
|
|
@ -19,12 +19,50 @@ Notes:
|
|||
#include "pb_sls.h"
|
||||
#include "smt_literal.h"
|
||||
#include "ast_pp.h"
|
||||
#include "uint_set.h"
|
||||
#include "th_rewriter.h"
|
||||
|
||||
namespace smt {
|
||||
struct pb_sls::imp {
|
||||
|
||||
struct index_set {
|
||||
unsigned_vector m_elems;
|
||||
unsigned_vector m_index;
|
||||
|
||||
unsigned num_elems() const { return m_elems.size(); }
|
||||
|
||||
void reset() { m_elems.reset(); m_index.reset(); }
|
||||
|
||||
bool empty() const { return m_elems.empty(); }
|
||||
|
||||
bool contains(unsigned idx) const {
|
||||
return
|
||||
(idx < m_index.size()) &&
|
||||
(m_index[idx] < m_elems.size()) &&
|
||||
(m_elems[m_index[idx]] == idx);
|
||||
}
|
||||
|
||||
void insert(unsigned idx) {
|
||||
m_index.reserve(idx+1);
|
||||
if (!contains(idx)) {
|
||||
m_index[idx] = m_elems.size();
|
||||
m_elems.push_back(idx);
|
||||
}
|
||||
}
|
||||
|
||||
void remove(unsigned idx) {
|
||||
if (!contains(idx)) return;
|
||||
unsigned pos = m_index[idx];
|
||||
m_elems[pos] = m_elems.back();
|
||||
m_index[m_elems[pos]] = pos;
|
||||
m_elems.pop_back();
|
||||
}
|
||||
|
||||
unsigned choose(random_gen& rnd) const {
|
||||
SASSERT(!empty());
|
||||
return m_elems[rnd(num_elems())];
|
||||
}
|
||||
};
|
||||
|
||||
struct clause {
|
||||
literal_vector m_lits;
|
||||
scoped_mpz_vector m_weights;
|
||||
|
|
@ -71,8 +109,8 @@ namespace smt {
|
|||
svector<bool> m_best_assignment;
|
||||
obj_map<func_decl, unsigned> m_decl2var; // map declarations to Boolean variables.
|
||||
ptr_vector<func_decl> m_var2decl; // reverse map
|
||||
uint_set m_hard_false; // list of hard clauses that are false.
|
||||
uint_set m_soft_false; // list of soft clauses that are false.
|
||||
index_set m_hard_false; // list of hard clauses that are false.
|
||||
index_set m_soft_false; // list of soft clauses that are false.
|
||||
unsigned m_max_flips; // maximal number of flips
|
||||
unsigned m_non_greedy_percent; // percent of moves to do non-greedy style
|
||||
random_gen m_rng;
|
||||
|
|
@ -133,6 +171,8 @@ namespace smt {
|
|||
IF_VERBOSE(1, verbose_stream() << "(pb.sls initial penalty: " << m_best_penalty << ")\n";
|
||||
verbose_stream() << "(pb.sls violated: " << m_hard_false.num_elems()
|
||||
<< " penalty: " << m_penalty << ")\n";);
|
||||
svector<bool> assignment(m_assignment);
|
||||
for (unsigned i = 0; i < 20; ++i) {
|
||||
init_max_flips();
|
||||
while (m_max_flips > 0) {
|
||||
--m_max_flips;
|
||||
|
|
@ -143,20 +183,35 @@ namespace smt {
|
|||
IF_VERBOSE(1, verbose_stream()
|
||||
<< "(pb.sls violated: " << m_hard_false.num_elems()
|
||||
<< " penalty: " << m_penalty << " " << lit << ")\n";);
|
||||
if (m_hard_false.num_elems() == 0 && m_best_penalty.is_zero()) {
|
||||
return l_true;
|
||||
if (m_hard_false.empty() && m_best_penalty.is_zero()) {
|
||||
break;
|
||||
}
|
||||
}
|
||||
if (m_hard_false.empty() && m_best_penalty.is_zero()) {
|
||||
break;
|
||||
}
|
||||
IF_VERBOSE(1, verbose_stream() << "(pb.sls best penalty " << m_best_penalty << ")\n";);
|
||||
if (m_best_assignment.empty()) {
|
||||
return l_false;
|
||||
if (!m_best_assignment.empty()) {
|
||||
assignment.reset();
|
||||
assignment.append(m_best_assignment);
|
||||
}
|
||||
else {
|
||||
m_assignment.reset();
|
||||
m_assignment.append(m_best_assignment);
|
||||
return l_true;
|
||||
m_assignment.append(assignment);
|
||||
m_penalty = m_best_penalty;
|
||||
m_best_assignment.reset();
|
||||
m_soft_false.reset();
|
||||
for (unsigned i = 0; i < m_soft.size(); ++i) {
|
||||
if (!eval(m_soft[i])) {
|
||||
m_soft_false.insert(i);
|
||||
m_penalty += m_weights[i];
|
||||
}
|
||||
}
|
||||
}
|
||||
m_assignment.reset();
|
||||
m_assignment.append(assignment);
|
||||
m_penalty = m_best_penalty;
|
||||
return l_true;
|
||||
}
|
||||
|
||||
bool get_value(literal l) {
|
||||
return l.sign() ^ m_assignment[l.var()];
|
||||
|
|
@ -362,27 +417,12 @@ namespace smt {
|
|||
// crude selection strategy.
|
||||
clause const& pick_hard_clause() {
|
||||
SASSERT(!m_hard_false.empty());
|
||||
uint_set::iterator it = m_hard_false.begin();
|
||||
uint_set::iterator end = m_hard_false.end();
|
||||
SASSERT(it != end);
|
||||
return m_clauses[*it];
|
||||
return m_clauses[m_hard_false.choose(m_rng)];
|
||||
}
|
||||
|
||||
clause const& pick_soft_clause() {
|
||||
SASSERT(!m_soft_false.empty());
|
||||
uint_set::iterator it = m_soft_false.begin();
|
||||
uint_set::iterator end = m_soft_false.end();
|
||||
SASSERT(it != end);
|
||||
unsigned index = *it;
|
||||
rational penalty = m_weights[index];
|
||||
++it;
|
||||
for (; it != end; ++it) {
|
||||
if (m_weights[*it] > penalty) {
|
||||
index = *it;
|
||||
penalty = m_weights[*it];
|
||||
}
|
||||
}
|
||||
return m_soft[index];
|
||||
return m_soft[m_soft_false.choose(m_rng)];
|
||||
}
|
||||
|
||||
int flip(literal l) {
|
||||
|
|
|
|||
|
|
@ -448,10 +448,12 @@ namespace opt {
|
|||
params_ref m_params;
|
||||
opt_solver m_solver;
|
||||
scoped_ptr<imp> m_imp;
|
||||
smt::pb_sls m_sls;
|
||||
|
||||
imp(ast_manager& m, opt_solver& s, expr_ref_vector const& soft_constraints, vector<rational> const& weights):
|
||||
m(m), s(s), m_soft(soft_constraints), m_weights(weights), m_print_all_models(false), m_cancel(false),
|
||||
m_solver(m, m_params, symbol("bound"))
|
||||
m_solver(m, m_params, symbol("bound")),
|
||||
m_sls(m)
|
||||
{
|
||||
m_assignment.resize(m_soft.size(), false);
|
||||
}
|
||||
|
|
@ -585,71 +587,63 @@ namespace opt {
|
|||
}
|
||||
|
||||
lbool sls_solve() {
|
||||
IF_VERBOSE(3, verbose_stream() << "(incremental solve)\n";);
|
||||
smt::pb_sls sls(m);
|
||||
svector<smt::bool_var> ws;
|
||||
IF_VERBOSE(1, verbose_stream() << "(sls solve)\n";);
|
||||
for (unsigned i = 0; i < s.get_num_assertions(); ++i) {
|
||||
sls.add(s.get_assertion(i));
|
||||
m_sls.add(s.get_assertion(i));
|
||||
}
|
||||
pb_util u(m);
|
||||
expr_ref fml(m), val(m);
|
||||
app_ref b(m);
|
||||
expr_ref_vector nsoft(m);
|
||||
m_lower = m_upper = rational::zero();
|
||||
solver::scoped_push __s(s);
|
||||
for (unsigned i = 0; i < m_soft.size(); ++i) {
|
||||
m_upper += m_weights[i];
|
||||
b = m.mk_fresh_const("b", m.mk_bool_sort());
|
||||
s.mc().insert(b->get_decl());
|
||||
fml = m.mk_or(m_soft[i].get(), b);
|
||||
s.assert_expr(fml);
|
||||
nsoft.push_back(b);
|
||||
m_sls.add(m_soft[i].get(), m_weights[i]);
|
||||
}
|
||||
TRACE("opt", tout << "weighted maxsat\n";);
|
||||
scoped_ensure_theory wth(*this);
|
||||
solver::scoped_push _s(s);
|
||||
lbool is_sat = l_true;
|
||||
bool was_sat = false;
|
||||
for (unsigned i = 0; i < m_soft.size(); ++i) {
|
||||
ws.push_back(wth().assert_weighted(m_soft[i].get(), m_weights[i]));
|
||||
sls.add(m_soft[i].get(), m_weights[i]);
|
||||
}
|
||||
|
||||
expr_ref fml(m);
|
||||
solver::scoped_push __s(s);
|
||||
while (l_true == is_sat) {
|
||||
is_sat = s.check_sat_core(0,0);
|
||||
if (m_cancel) {
|
||||
is_sat = l_undef;
|
||||
}
|
||||
if (is_sat == l_true) {
|
||||
if (wth().is_optimal()) {
|
||||
m_upper = wth().get_min_cost();
|
||||
updt_model(s);
|
||||
sls.set_model(m_model);
|
||||
if (l_true == sls()) {
|
||||
sls.get_model(m_model);
|
||||
svector<smt::bool_var> wsf;
|
||||
rational weight(0);
|
||||
for (unsigned i = 0; i < ws.size(); ++i) {
|
||||
if (!sls.soft_holds(i)) {
|
||||
wsf.push_back(ws[i]);
|
||||
weight += m_weights[i];
|
||||
}
|
||||
}
|
||||
fml = wth().mk_optimal_block(wsf, weight);
|
||||
m_upper = weight;
|
||||
s.assert_expr(fml);
|
||||
}
|
||||
else {
|
||||
fml = wth().mk_block();
|
||||
m_sls.set_model(m_model);
|
||||
m_upper = rational::zero();
|
||||
if (l_true == m_sls()) {
|
||||
m_sls.get_model(m_model);
|
||||
for (unsigned i = 0; i < m_soft.size(); ++i) {
|
||||
m_assignment[i] = m_sls.soft_holds(i);
|
||||
}
|
||||
}
|
||||
else {
|
||||
fml = wth().mk_block();
|
||||
for (unsigned i = 0; i < m_soft.size(); ++i) {
|
||||
VERIFY(m_model->eval(nsoft[i].get(), val));
|
||||
m_assignment[i] = !m.is_true(val);
|
||||
}
|
||||
}
|
||||
for (unsigned i = 0; i < m_soft.size(); ++i) {
|
||||
if (!m_assignment[i]) {
|
||||
m_upper += m_weights[i];
|
||||
}
|
||||
}
|
||||
IF_VERBOSE(1, verbose_stream() << "(sls.pb with upper bound: " << m_upper << ")\n";);
|
||||
fml = m.mk_not(u.mk_ge(nsoft.size(), m_weights.c_ptr(), nsoft.c_ptr(), m_upper));
|
||||
s.assert_expr(fml);
|
||||
was_sat = true;
|
||||
}
|
||||
IF_VERBOSE(3, verbose_stream() << "(incremental bound)\n";);
|
||||
}
|
||||
if (was_sat) {
|
||||
wth().get_assignment(m_assignment);
|
||||
}
|
||||
if (is_sat == l_false && was_sat) {
|
||||
is_sat = l_true;
|
||||
}
|
||||
m_upper = wth().get_min_cost();
|
||||
if (is_sat == l_true) {
|
||||
m_lower = m_upper;
|
||||
}
|
||||
TRACE("opt", tout << "min cost: " << m_upper << "\n";);
|
||||
return is_sat;
|
||||
}
|
||||
|
||||
|
|
@ -1288,6 +1282,7 @@ namespace opt {
|
|||
return m_imp->m_assignment[idx];
|
||||
}
|
||||
void wmaxsmt::set_cancel(bool f) {
|
||||
m_imp->m_sls.set_cancel(f);
|
||||
m_imp->m_cancel = f;
|
||||
m_imp->m_solver.set_cancel(f);
|
||||
m_imp->m_imp->m_cancel = f;
|
||||
|
|
|
|||
|
|
@ -1,3 +1,5 @@
|
|||
(set-option :smt.relevancy 0)
|
||||
(set-option :smt.pb.conflict_frequency 10000)
|
||||
(declare-fun x_354 () Int)
|
||||
(declare-fun x_522 () Int)
|
||||
(declare-fun x_464 () Int)
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue