mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

initial sls experiment

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2014-03-19 15:39:11 -07:00
parent 78975827b2
commit 3b3498c4b5
7 changed files with 295 additions and 107 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/ast/arith_decl_plugin.cpp
View file

@ -496,6 +496,7 @@ func_decl * arith_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters
if (k == OP_NUM)
return mk_num_decl(num_parameters, parameters, arity);
if (arity == 0 && !is_const_op(k)) {
UNREACHABLE();
m_manager->raise_exception("no arguments supplied to arithmetical operator");
return 0;
}
@ -513,6 +514,7 @@ func_decl * arith_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters
if (k == OP_NUM)
return mk_num_decl(num_parameters, parameters, num_args);
if (num_args == 0 && !is_const_op(k)) {
UNREACHABLE();
m_manager->raise_exception("no arguments supplied to arithmetical operator");
return 0;
}

5
src/opt/fu_malik.cpp
View file

@ -54,6 +54,7 @@ namespace opt {
unsigned m_upper;
unsigned m_lower;
model_ref m_model;
unsigned m_num_steps;
imp(ast_manager& m, opt_solver& s, expr_ref_vector const& soft):
m(m),
@ -63,7 +64,8 @@ namespace opt {
m_orig_soft(soft),
m_aux(m),
m_upper(0),
m_lower(0)
m_lower(0),
m_num_steps(0)
{
m_upper = m_soft.size() + 1;
m_assignment.resize(m_soft.size(), false);
@ -100,6 +102,7 @@ namespace opt {
if (m_s != &m_opt_solver) {
m_s->collect_statistics(st);
}
st.update("opt-fm-num-steps", m_soft.size() + 2 - m_upper);
}
void set_union(expr_set const& set1, expr_set const& set2, expr_set & set) const {

258
src/opt/pb_sls.cpp
View file

@ -20,6 +20,7 @@ Notes:
#include "smt_literal.h"
#include "ast_pp.h"
#include "uint_set.h"
#include "th_rewriter.h"
namespace smt {
struct pb_sls::imp {
@ -56,8 +57,11 @@ namespace smt {
ast_manager& m;
pb_util pb;
unsynch_mpz_manager mgr;
th_rewriter m_rewrite;
volatile bool m_cancel;
vector<clause> m_clauses; // clauses to be satisfied
expr_ref_vector m_orig_clauses; // for debugging
model_ref m_orig_model; // for debugging
vector<clause> m_soft; // soft constraints
vector<rational> m_weights; // weights of soft constraints
rational m_penalty; // current penalty of soft constraints
@ -70,66 +74,88 @@ namespace smt {
uint_set m_hard_false; // list of hard clauses that are false.
uint_set m_soft_false; // list of soft clauses that are false.
unsigned m_max_flips; // maximal number of flips
unsigned m_non_greedy_perc; // percent of moves to do non-greedy style
unsigned m_non_greedy_percent; // percent of moves to do non-greedy style
random_gen m_rng;
imp(ast_manager& m):
m(m),
pb(m),
m_cancel(false)
m_rewrite(m),
m_cancel(false),
m_orig_clauses(m)
{
m_max_flips = 100;
m_non_greedy_perc = 30;
init_max_flips();
m_non_greedy_percent = 30;
m_decl2var.insert(m.mk_true()->get_decl(), 0);
m_var2decl.push_back(m.mk_true()->get_decl());
m_assignment.push_back(true);
m_hard_occ.push_back(unsigned_vector());
m_soft_occ.push_back(unsigned_vector());
}
~imp() {
}
unsigned max_flips() {
return m_max_flips;
void init_max_flips() {
m_max_flips = 200;
}
void add(expr* f) {
clause cls(mgr);
if (compile_clause(f, cls)) {
m_clauses.push_back(cls);
m_orig_clauses.push_back(f);
}
}
void add(expr* f, rational const& w) {
clause cls(mgr);
if (compile_clause(f, cls)) {
m_clauses.push_back(cls);
m_soft.push_back(cls);
m_weights.push_back(w);
}
}
void set_model(model const& mdl) {
unsigned sz = mdl.get_num_constants();
void set_model(model_ref & mdl) {
m_orig_model = mdl;
unsigned sz = mdl->get_num_constants();
for (unsigned i = 0; i < sz; ++i) {
func_decl* f = mdl.get_constant(i);
func_decl* f = mdl->get_constant(i);
if (m.is_bool(f->get_range())) {
literal lit = mk_literal(f);
SASSERT(!lit.sign());
m_assignment[lit.var()] = m.is_true(mdl.get_const_interp(f));
m_assignment[lit.var()] = m.is_true(mdl->get_const_interp(f));
}
}
}
lbool operator()() {
init();
for (unsigned i = 0; i < max_flips(); ++i) {
flip();
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";);
init_max_flips();
while (m_max_flips > 0) {
--m_max_flips;
literal lit = flip();
if (m_cancel) {
return l_undef;
}
IF_VERBOSE(3, verbose_stream()
IF_VERBOSE(1, verbose_stream()
<< "(pb.sls violated: " << m_hard_false.num_elems()
<< " penalty: " << m_penalty << ")\n";);
if (m_best_penalty.is_zero()) {
<< " penalty: " << m_penalty << " " << lit << ")\n";);
if (m_hard_false.num_elems() == 0 && m_best_penalty.is_zero()) {
return l_true;
}
}
return m_best_assignment.empty()?l_false:l_true;
IF_VERBOSE(1, verbose_stream() << "(pb.sls best penalty " << m_best_penalty << ")\n";);
if (m_best_assignment.empty()) {
return l_false;
}
else {
m_assignment.reset();
m_assignment.append(m_best_assignment);
return l_true;
}
}
bool get_value(literal l) {
@ -140,8 +166,8 @@ namespace smt {
}
void get_model(model_ref& mdl) {
mdl = alloc(model, m);
for (unsigned i = 0; i < m_var2decl.size(); ++i) {
mdl->register_decl(m_var2decl[i], m_best_assignment[i]?m.mk_true():m.mk_false());
for (unsigned i = 1; i < m_var2decl.size(); ++i) {
mdl->register_decl(m_var2decl[i], m_assignment[i]?m.mk_true():m.mk_false());
}
}
@ -151,6 +177,40 @@ namespace smt {
void updt_params(params_ref& p) {
}
bool soft_holds(unsigned index) {
return eval(m_soft[index]);
}
void display(std::ostream& out, clause const& cls) {
for (unsigned i = 0; i < cls.m_lits.size(); ++i) {
out << cls.m_weights[i] << "*" << cls.m_lits[i] << " ";
if (i + 1 < cls.m_lits.size()) {
out << "+ ";
}
}
out << "(" << cls.m_value << ") ";
if (cls.m_eq) {
out << "= ";
}
else {
out << ">= ";
}
out << cls.m_k << "\n";
}
void display(std::ostream& out) {
for (unsigned i = 0; i < m_clauses.size(); ++i) {
display(out, m_clauses[i]);
}
out << "soft:\n";
for (unsigned i = 0; i < m_soft.size(); ++i) {
display(out << m_weights[i] << ": ", m_soft[i]);
}
for (unsigned i = 0; i < m_assignment.size(); ++i) {
out << literal(i) << ": " << m_var2decl[i]->get_name() << " |-> " << (m_assignment[i]?"true":"false") << "\n";
}
}
bool eval(clause& cls) {
unsigned sz = cls.m_lits.size();
cls.m_value.reset();
@ -194,6 +254,9 @@ namespace smt {
for (unsigned i = 0; i < m_clauses.size(); ++i) {
if (!eval(m_clauses[i])) {
m_hard_false.insert(i);
expr_ref tmp(m);
VERIFY(m_orig_model->eval(m_orig_clauses[i].get(), tmp));
std::cout << "original evaluation: " << tmp << "\n";
}
}
for (unsigned i = 0; i < m_soft.size(); ++i) {
@ -203,44 +266,62 @@ namespace smt {
}
}
m_best_penalty = m_penalty;
TRACE("opt", display(tout););
}
void flip() {
literal flip() {
literal result;
if (m_hard_false.empty()) {
flip_soft();
result = flip_soft();
}
else {
flip_hard();
result = flip_hard();
}
if (m_hard_false.empty() && m_best_penalty > m_penalty) {
IF_VERBOSE(1, verbose_stream() << "(pb.sls improved bound " << m_penalty << ")\n";);
m_best_assignment.reset();
m_best_assignment.append(m_assignment);
m_best_penalty = m_penalty;
init_max_flips();
}
if (!m_assignment[result.var()]) {
result.neg();
}
return result;
}
void flip_hard() {
literal flip_hard() {
SASSERT(!m_hard_false.empty());
literal lit;
clause const& cls = pick_hard_clause();
// IF_VERBOSE(1, display(verbose_stream(), cls););
int break_count;
int min_bc = INT_MAX;
unsigned min_bc_index = 0;
for (unsigned i = 0; i < cls.m_lits.size(); ++i) {
literal lit = cls.m_lits[i];
lit = cls.m_lits[i];
break_count = flip(lit);
if (break_count <= 0) {
return;
}
if (break_count < min_bc) {
min_bc = break_count;
min_bc_index = i;
}
else if (break_count == min_bc && m_rng(5) == 1) {
min_bc_index = i;
}
VERIFY(-break_count == flip(~lit));
}
if (m_rng(100) <= m_non_greedy_perc) {
flip(cls.m_lits[m_rng(cls.m_lits.size())]);
if (m_rng(100) <= m_non_greedy_percent) {
lit = cls.m_lits[m_rng(cls.m_lits.size())];
}
else {
flip(cls.m_lits[min_bc_index]);
lit = cls.m_lits[min_bc_index];
}
flip(lit);
return lit;
}
void flip_soft() {
literal flip_soft() {
literal lit;
clause const& cls = pick_soft_clause();
int break_count;
int min_bc = INT_MAX;
@ -248,18 +329,11 @@ namespace smt {
rational penalty = m_penalty;
rational min_penalty = penalty;
for (unsigned i = 0; i < cls.m_lits.size(); ++i) {
literal lit = cls.m_lits[i];
lit = cls.m_lits[i];
break_count = flip(lit);
SASSERT(break_count >= 0);
if (break_count == 0 && penalty > m_penalty) {
if (m_best_penalty > m_penalty) {
IF_VERBOSE(1, verbose_stream() << "(pb.sls improved bound "
<< m_penalty << ")\n";);
m_best_assignment.reset();
m_best_assignment.append(m_assignment);
m_best_penalty = m_penalty;
}
return;
return lit;
}
if ((break_count < min_bc) ||
(break_count == min_bc && m_penalty < min_penalty)) {
@ -269,13 +343,15 @@ namespace smt {
}
VERIFY(-break_count == flip(~lit));
}
if (m_rng(100) <= m_non_greedy_perc) {
flip(cls.m_lits[m_rng(cls.m_lits.size())]);
if (m_rng(100) <= m_non_greedy_percent) {
lit = cls.m_lits[m_rng(cls.m_lits.size())];
}
else {
// just do a greedy move:
flip(cls.m_lits[min_bc_index]);
lit = cls.m_lits[min_bc_index];
}
flip(lit);
return lit;
}
//
@ -313,44 +389,47 @@ namespace smt {
SASSERT(get_value(l));
m_assignment[l.var()] = !m_assignment[l.var()];
int break_count = 0;
{
unsigned_vector const& occ = m_hard_occ[l.var()];
for (unsigned i = 0; i < occ.size(); ++i) {
unsigned j = occ[i];
if (eval(m_clauses[j])) {
if (m_hard_false.contains(j)) {
break_count--;
m_hard_false.remove(j);
}
unsigned_vector const& occh = m_hard_occ[l.var()];
scoped_mpz value(mgr);
for (unsigned i = 0; i < occh.size(); ++i) {
unsigned j = occh[i];
value = m_clauses[j].m_value;
if (eval(m_clauses[j])) {
if (m_hard_false.contains(j)) {
break_count--;
m_hard_false.remove(j);
}
else {
if (!m_hard_false.contains(j)) {
break_count++;
m_hard_false.insert(j);
}
}
else {
if (!m_hard_false.contains(j)) {
break_count++;
m_hard_false.insert(j);
}
else if (value < m_clauses[j].m_value) {
break_count++;
}
}
}
{
unsigned_vector const& occ = m_soft_occ[l.var()];
for (unsigned i = 0; i < occ.size(); ++i) {
unsigned j = occ[i];
if (eval(m_soft[j])) {
if (m_soft_false.contains(j)) {
m_penalty -= m_weights[j];
m_soft_false.remove(j);
}
unsigned_vector const& occs = m_soft_occ[l.var()];
for (unsigned i = 0; i < occs.size(); ++i) {
unsigned j = occs[i];
if (eval(m_soft[j])) {
if (m_soft_false.contains(j)) {
m_penalty -= m_weights[j];
m_soft_false.remove(j);
}
else {
if (!m_soft_false.contains(j)) {
m_penalty += m_weights[j];
m_soft_false.insert(j);
}
}
else {
if (!m_soft_false.contains(j)) {
m_penalty += m_weights[j];
m_soft_false.insert(j);
}
}
}
}
}
SASSERT(get_value(~l));
TRACE("opt", tout << "flip: " << l << " num false: " << m_hard_false.num_elems()
<< " penalty: " << m_penalty << " break count: " << break_count << "\n";);
return break_count;
}
@ -396,19 +475,28 @@ namespace smt {
}
bool compile_clause(expr* _f, clause& cls) {
if (!is_app(_f)) return false;
app* f = to_app(_f);
expr_ref tmp(m);
m_rewrite(_f, tmp);
if (!is_app(tmp)) return false;
app* f = to_app(tmp);
unsigned sz = f->get_num_args();
expr* const* args = f->get_args();
literal lit;
rational coeff;
rational coeff, k;
if (pb.is_ge(f) || pb.is_eq(f)) {
k = pb.get_k(f);
SASSERT(k.is_int());
cls.m_k = k.to_mpq().numerator();
for (unsigned i = 0; i < sz; ++i) {
coeff = pb.get_coeff(f, i);
coeff = pb.get_coeff(f, i);
SASSERT(coeff.is_int());
lit = mk_literal(args[i]);
if (lit == null_literal) return false;
SASSERT(lit != false_literal && lit != true_literal);
if (lit == false_literal) continue;
if (lit == true_literal) {
cls.m_k -= coeff.to_mpq().numerator();
continue;
}
cls.m_lits.push_back(lit);
cls.m_weights.push_back(coeff.to_mpq().numerator());
if (get_value(lit)) {
@ -416,15 +504,13 @@ namespace smt {
}
}
cls.m_eq = pb.is_eq(f);
coeff = pb.get_k(f);
SASSERT(coeff.is_int());
cls.m_k = coeff.to_mpq().numerator();
}
else if (m.is_or(f)) {
for (unsigned i = 0; i < sz; ++i) {
lit = mk_literal(args[i]);
if (lit == null_literal) return false;
SASSERT(lit != false_literal && lit != true_literal);
if (lit == false_literal) continue;
if (lit == true_literal) return false;
cls.m_lits.push_back(lit);
cls.m_weights.push_back(mpz(1));
if (get_value(lit)) {
@ -434,6 +520,9 @@ namespace smt {
cls.m_eq = false;
cls.m_k = mpz(1);
}
else if (m.is_true(f)) {
return false;
}
else {
lit = mk_literal(f);
if (lit == null_literal) return false;
@ -460,7 +549,7 @@ namespace smt {
void pb_sls::add(expr* f, rational const& w) {
m_imp->add(f, w);
}
void pb_sls::set_model(model const& mdl) {
void pb_sls::set_model(model_ref& mdl) {
m_imp->set_model(mdl);
}
lbool pb_sls::operator()() {
@ -475,6 +564,9 @@ namespace smt {
void pb_sls::get_model(model_ref& mdl) {
m_imp->get_model(mdl);
}
bool pb_sls::soft_holds(unsigned index) {
return m_imp->soft_holds(index);
}
void pb_sls::updt_params(params_ref& p) {
m_imp->updt_params(p);
}

3
src/opt/pb_sls.h
View file

@ -35,7 +35,8 @@ namespace smt {
~pb_sls();
void add(expr* f);
void add(expr* f, rational const& w);
void set_model(model const& mdl);
bool soft_holds(unsigned index);
void set_model(model_ref& mdl);
lbool operator()();
void set_cancel(bool f);
void collect_statistics(statistics& st) const;

112
src/opt/weighted_maxsat.cpp
View file

@ -118,7 +118,7 @@ namespace smt {
m_propagate = true;
}
void assert_weighted(expr* fml, rational const& w) {
bool_var assert_weighted(expr* fml, rational const& w) {
context & ctx = get_context();
ast_manager& m = get_manager();
app_ref var(m), wfml(m);
@ -132,7 +132,7 @@ namespace smt {
m_assigned.push_back(false);
m_rmin_cost += w;
m_normalize = true;
register_var(var, true);
return register_var(var, true);
}
bool_var register_var(app* var, bool attach) {
@ -341,6 +341,25 @@ namespace smt {
return result;
}
expr_ref mk_optimal_block(svector<bool_var> const& ws, rational const& weight) {
ast_manager& m = get_manager();
expr_ref_vector disj(m);
rational new_w = weight*m_den;
m_zmin_cost = new_w.to_mpq().numerator();
m_cost_save.reset();
for (unsigned i = 0; i < ws.size(); ++i) {
bool_var bv = ws[i];
theory_var v = m_bool2var[bv];
m_cost_save.push_back(v);
disj.push_back(m.mk_not(m_vars[v].get()));
}
if (m_min_cost_atom) {
disj.push_back(m.mk_not(m_min_cost_atom));
}
expr_ref result(m.mk_or(disj.size(), disj.c_ptr()), m);
return result;
}
private:
@ -493,6 +512,9 @@ namespace opt {
if (m_engine == symbol("wpm2b")) {
return wpm2b_solve();
}
if (m_engine == symbol("sls")) {
return sls_solve();
}
return incremental_solve();
}
@ -522,10 +544,6 @@ namespace opt {
lbool incremental_solve() {
IF_VERBOSE(3, verbose_stream() << "(incremental solve)\n";);
smt::pb_sls sls(m);
for (unsigned i = 0; i < s.get_num_assertions(); ++i) {
sls.add(s.get_assertion(i));
}
TRACE("opt", tout << "weighted maxsat\n";);
scoped_ensure_theory wth(*this);
solver::scoped_push _s(s);
@ -533,8 +551,9 @@ namespace opt {
bool was_sat = false;
for (unsigned i = 0; i < m_soft.size(); ++i) {
wth().assert_weighted(m_soft[i].get(), m_weights[i]);
sls.add(m_soft[i].get(), m_weights[i]);
}
s.display(std::cout);
solver::scoped_push __s(s);
while (l_true == is_sat) {
is_sat = s.check_sat_core(0,0);
@ -545,15 +564,6 @@ namespace opt {
if (wth().is_optimal()) {
m_upper = wth().get_min_cost();
updt_model(s);
s.display(std::cout);
model_ref mdl;
s.get_model(mdl);
model_smt2_pp(std::cout, m, *(mdl.get()), 0);
sls.set_model(*(mdl.get()));
lbool found = sls();
std::cout << found << "\n";
}
expr_ref fml = wth().mk_block();
s.assert_expr(fml);
@ -575,6 +585,76 @@ namespace opt {
return is_sat;
}
lbool sls_solve() {
IF_VERBOSE(3, verbose_stream() << "(incremental solve)\n";);
smt::pb_sls sls(m);
svector<smt::bool_var> ws;
for (unsigned i = 0; i < s.get_num_assertions(); ++i) {
sls.add(s.get_assertion(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]);
}
s.display(std::cout);
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();
}
}
else {
fml = wth().mk_block();
}
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;
}
/**
Iteratively increase cost until there is an assignment during
final_check that satisfies min_cost.

2
src/smt/theory_pb.h
View file

@ -121,7 +121,7 @@ namespace smt {
unsigned m_num_propagations;
unsigned m_compilation_threshold;
lbool m_compiled;
ineq(unsynch_mpz_manager& m, literal l, bool is_eq) :
m_mpz(m), m_lit(l), m_is_eq(is_eq),
m_max_watch(m), m_watch_sum(m),

20
src/tactic/arith/elim01_tactic.cpp
View file

@ -24,6 +24,7 @@ Notes:
#include"arith_decl_plugin.h"
#include"elim01_tactic.h"
#include"model_smt2_pp.h"
#include"th_rewriter.h"
class bool2int_model_converter : public model_converter {
ast_manager& m;
@ -120,6 +121,7 @@ public:
typedef obj_hashtable<expr> expr_set;
ast_manager & m;
arith_util a;
th_rewriter m_rewriter;
params_ref m_params;
unsigned m_max_hi_default;
rational m_max_hi;
@ -127,6 +129,7 @@ public:
elim01_tactic(ast_manager & _m, params_ref const & p):
m(_m),
a(m),
m_rewriter(m),
m_max_hi_default(8),
m_max_hi(rational(m_max_hi_default)) {
}
@ -177,12 +180,13 @@ public:
}
}
expr_ref new_curr(m);
expr_ref new_curr(m), tmp_curr(m);
proof_ref new_pr(m);
for (unsigned i = 0; i < g->size(); i++) {
expr * curr = g->form(i);
sub(curr, new_curr);
sub(curr, tmp_curr);
m_rewriter(tmp_curr, new_curr);
g->update(i, new_curr, new_pr, g->dep(i));
}
for (unsigned i = 0; i < axioms.size(); ++i) {
@ -219,12 +223,18 @@ public:
ites.push_back(m.mk_ite(xs.back(), a.mk_numeral(rational(1 << sh), true), zero));
++sh;
}
if (ites.size() == 1) {
switch (ites.size()) {
case 0:
sum = zero;
break;
case 1:
sum = ites[0].get();
}
else {
break;
default:
sum = a.mk_add(ites.size(), (expr*const*)ites.c_ptr());
break;
}
TRACE("pb", tout << mk_pp(x, m) << " " << sum << " max: " << max_value << "\n";);
sub.insert(x, sum);
b2i->insert(x->get_decl(), xfs.size(), xfs.c_ptr());