mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-28 11:25:51 +00:00
Code Activity

refactor sat/sls interface. Remove wpm2 and bvsls dependencies

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2014-08-15 10:40:44 -07:00
parent a02cab2194
commit ee1a1b1135
43 changed files with 609 additions and 891 deletions
Download patch file Download diff file Expand all files Collapse all files

9
src/opt/bcd2.cpp
View file

@ -99,9 +99,9 @@ namespace opt {
}
public:
bcd2(opt_solver* s, ast_manager& m, params_ref& p,
bcd2(context& c,
vector<rational> const& ws, expr_ref_vector const& soft):
maxsmt_solver_base(s, m, p, ws, soft),
maxsmt_solver_base(c, ws, soft),
pb(m),
m_soft_aux(m),
m_trail(m),
@ -116,7 +116,6 @@ namespace opt {
expr_ref fml(m), r(m);
lbool is_sat = l_undef;
expr_ref_vector asms(m);
enable_sls();
solver::scoped_push _scope1(s());
init();
init_bcd();
@ -400,9 +399,9 @@ namespace opt {
}
};
maxsmt_solver_base* opt::mk_bcd2(ast_manager& m, opt_solver* s, params_ref& p,
maxsmt_solver_base* opt::mk_bcd2(context& c,
vector<rational> const& ws, expr_ref_vector const& soft) {
return alloc(bcd2, s, m, p, ws, soft);
return alloc(bcd2, c, ws, soft);
}
}

3
src/opt/bcd2.h
View file

@ -23,7 +23,6 @@ Notes:
#include "maxsmt.h"
namespace opt {
maxsmt_solver_base* mk_bcd2(ast_manager& m, opt_solver* s, params_ref& p,
vector<rational> const& ws, expr_ref_vector const& soft);
maxsmt_solver_base* mk_bcd2(context& c, vector<rational> const& ws, expr_ref_vector const& soft);
}
#endif

123
src/opt/bvsls_opt_solver.cpp
View file

@ -1,123 +0,0 @@
/*++
Copyright (c) 2013 Microsoft Corporation
Module Name:
bvsls_opt_solver.cpp
Abstract:
Uses the bvsls engine for optimization
Author:
Christoph (cwinter) 2014-3-28
Notes:
--*/
#include "bvsls_opt_solver.h"
namespace opt {
bvsls_opt_solver::bvsls_opt_solver(ast_manager & m, params_ref const & p) :
opt_solver(m, p, symbol("QF_BV")),
m_manager(m),
m_params(p),
m_engine(m, p)
{
}
bvsls_opt_solver::~bvsls_opt_solver()
{
}
void bvsls_opt_solver::updt_params(params_ref & p)
{
opt_solver::updt_params(p);
m_engine.updt_params(p);
}
void bvsls_opt_solver::collect_param_descrs(param_descrs & r)
{
opt_solver::collect_param_descrs(r);
}
void bvsls_opt_solver::collect_statistics(statistics & st) const
{
opt_solver::collect_statistics(st);
}
void bvsls_opt_solver::assert_expr(expr * t) {
m_engine.assert_expr(t);
}
void bvsls_opt_solver::push_core()
{
opt_solver::push_core();
}
void bvsls_opt_solver::pop_core(unsigned n)
{
opt_solver::pop_core(n);
}
lbool bvsls_opt_solver::check_sat_core(unsigned num_assumptions, expr * const * assumptions)
{
SASSERT(num_assumptions == 0);
SASSERT(assumptions == 0);
return m_engine();
}
void bvsls_opt_solver::get_unsat_core(ptr_vector<expr> & r)
{
NOT_IMPLEMENTED_YET();
}
void bvsls_opt_solver::get_model(model_ref & m)
{
NOT_IMPLEMENTED_YET();
}
proof * bvsls_opt_solver::get_proof()
{
NOT_IMPLEMENTED_YET();
}
std::string bvsls_opt_solver::reason_unknown() const
{
NOT_IMPLEMENTED_YET();
}
void bvsls_opt_solver::get_labels(svector<symbol> & r)
{
opt_solver::get_labels(r);
}
void bvsls_opt_solver::set_cancel(bool f)
{
opt_solver::set_cancel(f);
m_engine.set_cancel(f);
}
void bvsls_opt_solver::set_progress_callback(progress_callback * callback)
{
opt_solver::set_progress_callback(callback);
}
unsigned bvsls_opt_solver::get_num_assertions() const
{
NOT_IMPLEMENTED_YET();
}
expr * bvsls_opt_solver::get_assertion(unsigned idx) const
{
NOT_IMPLEMENTED_YET();
}
void bvsls_opt_solver::display(std::ostream & out) const
{
NOT_IMPLEMENTED_YET();
}
}

57
src/opt/bvsls_opt_solver.h
View file

@ -1,57 +0,0 @@
/*++
Copyright (c) 2013 Microsoft Corporation
Module Name:
bvsls_opt_solver.h
Abstract:
Uses the bvsls engine for optimization
Author:
Christoph (cwinter) 2014-3-28
Notes:
--*/
#ifndef _BVSLS_OPT_SOLVER_H_
#define _BVSLS_OPT_SOLVER_H_
#include "bvsls_opt_engine.h"
#include "opt_solver.h"
namespace opt {
class bvsls_opt_solver : public opt_solver {
ast_manager & m_manager;
params_ref const & m_params;
bvsls_opt_engine m_engine;
public:
bvsls_opt_solver(ast_manager & m, params_ref const & p);
virtual ~bvsls_opt_solver();
virtual void updt_params(params_ref & p);
virtual void collect_param_descrs(param_descrs & r);
virtual void collect_statistics(statistics & st) const;
virtual void assert_expr(expr * t);
virtual void push_core();
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 proof * get_proof();
virtual std::string reason_unknown() const;
virtual void get_labels(svector<symbol> & r);
virtual void set_cancel(bool f);
virtual void set_progress_callback(progress_callback * callback);
virtual unsigned get_num_assertions() const;
virtual expr * get_assertion(unsigned idx) const;
virtual void display(std::ostream & out) const;
};
}
#endif

6
src/opt/core_maxsat.cpp
View file

@ -19,11 +19,13 @@ Notes:
#include "core_maxsat.h"
#include "pb_decl_plugin.h"
#include "ast_pp.h"
#include "opt_context.h"
namespace opt {
core_maxsat::core_maxsat(ast_manager& m, solver& s, expr_ref_vector& soft_constraints):
m(m), s(s), m_lower(0), m_upper(soft_constraints.size()), m_soft(soft_constraints) {
core_maxsat::core_maxsat(context& c, expr_ref_vector& soft_constraints):
m(c.get_manager()), s(c.get_solver()),
m_lower(0), m_upper(soft_constraints.size()), m_soft(soft_constraints) {
m_answer.resize(m_soft.size(), false);
}

2
src/opt/core_maxsat.h
View file

@ -34,7 +34,7 @@ namespace opt {
unsigned m_lower;
model_ref m_model;
public:
core_maxsat(ast_manager& m, solver& s, expr_ref_vector& soft_constraints);
core_maxsat(context& c, expr_ref_vector& soft_constraints);
virtual ~core_maxsat();
virtual lbool operator()();
virtual rational get_lower() const;

90
src/opt/fu_malik.cpp
View file

@ -23,9 +23,9 @@ Notes:
#include "goal.h"
#include "probe.h"
#include "tactic.h"
#include "smt_context.h"
#include "ast_pp.h"
#include "model_smt2_pp.h"
#include "opt_context.h"
/**
\brief Fu & Malik procedure for MaxSAT. This procedure is based on
@ -44,9 +44,9 @@ Notes:
namespace opt {
struct fu_malik::imp {
ast_manager& m;
opt_solver & m_opt_solver;
ref<solver> m_s;
ast_manager& m;
solver& m_s;
filter_model_converter& m_fm;
expr_ref_vector m_soft;
expr_ref_vector m_orig_soft;
expr_ref_vector m_aux;
@ -55,10 +55,10 @@ namespace opt {
unsigned m_lower;
model_ref m_model;
imp(ast_manager& m, opt_solver& s, expr_ref_vector const& soft):
m(m),
m_opt_solver(s),
m_s(&s),
imp(context& c, expr_ref_vector const& soft):
m(c.get_manager()),
m_s(c.get_solver()),
m_fm(c.fm()),
m_soft(soft),
m_orig_soft(soft),
m_aux(m),
@ -69,7 +69,7 @@ namespace opt {
m_assignment.resize(m_soft.size(), false);
}
solver& s() { return *m_s; }
solver& s() { return m_s; }
/**
\brief One step of the Fu&Malik algorithm.
@ -96,10 +96,8 @@ namespace opt {
}
}
void collect_statistics(statistics& st) const {
if (m_s != &m_opt_solver) {
m_s->collect_statistics(st);
}
st.update("opt-fm-num-steps", m_soft.size() + 2 - m_upper);
}
@ -145,8 +143,8 @@ namespace opt {
app_ref block_var(m), tmp(m);
block_var = m.mk_fresh_const("block_var", m.mk_bool_sort());
m_aux[i] = m.mk_fresh_const("aux", m.mk_bool_sort());
m_opt_solver.mc().insert(block_var->get_decl());
m_opt_solver.mc().insert(to_app(m_aux[i].get())->get_decl());
m_fm.insert(block_var->get_decl());
m_fm.insert(to_app(m_aux[i].get())->get_decl());
m_soft[i] = m.mk_or(m_soft[i].get(), block_var);
block_vars.push_back(block_var);
tmp = m.mk_or(m_soft[i].get(), m_aux[i].get());
@ -181,17 +179,6 @@ namespace opt {
}
}
void set_solver() {
if (m_opt_solver.dump_benchmarks())
return;
solver& current_solver = s();
goal g(m, true, false);
unsigned num_assertions = current_solver.get_num_assertions();
for (unsigned i = 0; i < num_assertions; ++i) {
g.assert_expr(current_solver.get_assertion(i));
}
}
// TBD: bug when cancel flag is set, fu_malik returns is_sat == l_true instead of l_undef
lbool operator()() {
@ -199,7 +186,6 @@ namespace opt {
if (m_soft.empty()) {
return is_sat;
}
set_solver();
solver::scoped_push _sp(s());
expr_ref tmp(m);
@ -211,7 +197,7 @@ namespace opt {
for (unsigned i = 0; i < m_soft.size(); ++i) {
m_aux.push_back(m.mk_fresh_const("p", m.mk_bool_sort()));
m_opt_solver.mc().insert(to_app(m_aux.back())->get_decl());
m_fm.insert(to_app(m_aux.back())->get_decl());
tmp = m.mk_or(m_soft[i].get(), m_aux[i].get());
s().assert_expr(tmp);
}
@ -247,8 +233,8 @@ namespace opt {
};
fu_malik::fu_malik(ast_manager& m, opt_solver& s, expr_ref_vector& soft_constraints) {
m_imp = alloc(imp, m, s, soft_constraints);
fu_malik::fu_malik(context& c, expr_ref_vector& soft_constraints) {
m_imp = alloc(imp, c, soft_constraints);
}
fu_malik::~fu_malik() {
dealloc(m_imp);
@ -281,49 +267,3 @@ namespace opt {
}
};
#if 0
void quick_explain(expr_ref_vector const& assumptions, expr_ref_vector & literals, bool has_set, expr_set & core) {
if (has_set && s().check_sat(assumptions.size(), assumptions.c_ptr()) == l_false) {
core.reset();
return;
}
SASSERT(!literals.empty());
if (literals.size() == 1) {
core.reset();
core.insert(literals[0].get());
return;
}
unsigned mid = literals.size()/2;
expr_ref_vector ls1(m), ls2(m);
ls1.append(mid, literals.c_ptr());
ls2.append(literals.size()-mid, literals.c_ptr() + mid);
#if Z3DEBUG
expr_ref_vector ls(m);
ls.append(ls1);
ls.append(ls2);
SASSERT(ls.size() == literals.size());
for (unsigned i = 0; i < literals.size(); ++i) {
SASSERT(ls[i].get() == literals[i].get());
}
#endif
expr_ref_vector as1(m);
as1.append(assumptions);
as1.append(ls1);
expr_set core2;
quick_explain(as1, ls2, !ls1.empty(), core2);
expr_ref_vector as2(m), cs2(m);
as2.append(assumptions);
set2vector(core2, cs2);
as2.append(cs2);
expr_set core1;
quick_explain(as2, ls1, !core2.empty(), core1);
set_union(core1, core2, core);
}
#endif

2
src/opt/fu_malik.h
View file

@ -33,7 +33,7 @@ namespace opt {
struct imp;
imp* m_imp;
public:
fu_malik(ast_manager& m, opt_solver& s, expr_ref_vector& soft_constraints);
fu_malik(context& c, expr_ref_vector& soft_constraints);
virtual ~fu_malik();
virtual lbool operator()();
virtual rational get_lower() const;

93
src/opt/inc_sat_solver.cpp
View file

@ -40,18 +40,19 @@ class inc_sat_solver : public solver {
expr_ref_vector m_fmls;
expr_ref_vector m_current_fmls;
unsigned_vector m_fmls_lim;
expr_ref_vector m_core;
atom2bool_var m_map;
model_ref m_model;
expr_ref_vector m_core;
atom2bool_var m_map;
model_ref m_model;
model_converter_ref m_mc;
tactic_ref m_preprocess;
unsigned m_num_scopes;
tactic_ref m_preprocess;
unsigned m_num_scopes;
sat::literal_vector m_asms;
goal_ref_buffer m_subgoals;
proof_converter_ref m_pc;
model_converter_ref m_mc2;
expr_dependency_ref m_dep_core;
expr_ref_vector m_soft;
vector<rational> m_weights;
typedef obj_map<expr, sat::literal> dep2asm_t;
public:
@ -59,7 +60,8 @@ public:
m(m), m_solver(p,0), m_params(p),
m_fmls(m), m_current_fmls(m), m_core(m), m_map(m),
m_num_scopes(0),
m_dep_core(m) {
m_dep_core(m),
m_soft(m) {
m_params.set_bool("elim_vars", false);
m_solver.updt_params(m_params);
params_ref simp2_p = p;
@ -78,29 +80,32 @@ public:
mk_max_bv_sharing_tactic(m),
mk_bit_blaster_tactic(m),
mk_aig_tactic(),
using_params(mk_simplify_tactic(m), simp2_p));
using_params(mk_simplify_tactic(m), simp2_p));
}
virtual ~inc_sat_solver() {}
virtual void set_progress_callback(progress_callback * callback) {
}
virtual void set_progress_callback(progress_callback * callback) {}
virtual lbool check_sat(unsigned num_assumptions, expr * const * assumptions) {
m_solver.pop_to_base_level();
dep2asm_t dep2asm;
m_model = 0;
lbool r = internalize_formulas();
if (r != l_true) return r;
r = internalize_assumptions(num_assumptions, assumptions, dep2asm);
if (r != l_true) return r;
extract_assumptions(dep2asm, m_asms);
r = initialize_soft_constraints();
if (r != l_true) return r;
r = m_solver.check(m_asms.size(), m_asms.c_ptr());
switch (r) {
case l_true:
check_assumptions(dep2asm);
if (num_assumptions > 0) {
check_assumptions(dep2asm);
}
break;
case l_false:
// TBD: expr_dependency core is not accounted for.
@ -160,8 +165,7 @@ public:
m_params = p;
m_params.set_bool("elim_vars", false);
m_solver.updt_params(m_params);
}
}
virtual void collect_statistics(statistics & st) const {
m_preprocess->collect_statistics(st);
m_solver.collect_statistics(st);
@ -186,18 +190,57 @@ public:
virtual void get_labels(svector<symbol> & r) {
UNREACHABLE();
}
virtual unsigned get_num_assertions() const {
return m_fmls.size();
}
virtual expr * get_assertion(unsigned idx) const {
return m_fmls[idx];
}
void set_soft(unsigned sz, expr*const* soft, rational const* weights) {
m_soft.reset();
m_weights.reset();
m_soft.append(sz, soft);
m_weights.append(sz, weights);
}
private:
lbool initialize_soft_constraints() {
dep2asm_t dep2asm;
if (m_soft.empty()) {
return l_true;
}
expr_ref_vector soft(m_soft);
for (unsigned i = 0; i < soft.size(); ++i) {
expr* e = soft[i].get(), *e1;
if (is_uninterp_const(e) || (m.is_not(e, e1) && is_uninterp_const(e1))) {
continue;
}
expr_ref asum(m), fml(m);
asum = m.mk_fresh_const("soft", m.mk_bool_sort());
fml = m.mk_iff(asum, e);
m_fmls.push_back(fml);
soft[i] = asum;
}
m_soft.reset();
lbool r = internalize_formulas();
if (r != l_true) return r;
r = internalize_assumptions(soft.size(), soft.c_ptr(), dep2asm);
sat::literal_vector lits;
svector<double> weights;
if (r == l_true) {
for (unsigned i = 0; i < soft.size(); ++i) {
weights.push_back(m_weights[i].get_double());
lits.push_back(dep2asm.find(soft[i].get()));
}
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);
}
return r;
}
lbool internalize_goal(goal_ref& g, dep2asm_t& dep2asm) {
m_mc2.reset();
m_pc.reset();
@ -295,10 +338,8 @@ private:
dep2asm_t::iterator it = dep2asm.begin(), end = dep2asm.end();
for (; it != end; ++it) {
sat::literal lit = it->m_value;
lbool polarity = lit.sign()?l_false:l_true;
lbool value = sat::value_at(lit.var(), ll_m);
if (value != polarity) {
IF_VERBOSE(0, verbose_stream() << mk_pp(it->m_key, m) << " evaluates to " << value << "\n";
if (sat::value_at(lit, ll_m) != l_true) {
IF_VERBOSE(0, verbose_stream() << mk_pp(it->m_key, m) << " does not evaluate to true\n";
verbose_stream() << m_asms << "\n";
m_solver.display_assignment(verbose_stream());
m_solver.display(verbose_stream()););
@ -343,6 +384,12 @@ private:
}
};
solver* mk_inc_sat_solver(ast_manager& m, params_ref& p) {
return alloc(inc_sat_solver, m, p);
}
void set_soft_inc_sat(solver* _s, unsigned sz, expr*const* soft, rational const* weights) {
inc_sat_solver* s = dynamic_cast<inc_sat_solver*>(_s);
s->set_soft(sz, soft, weights);
}

2
src/opt/inc_sat_solver.h
View file

@ -24,4 +24,6 @@ Notes:
solver* mk_inc_sat_solver(ast_manager& m, params_ref& p);
void set_soft_inc_sat(solver* s, unsigned sz, expr*const* soft, rational const* weights);
#endif

11
src/opt/maxhs.cpp
View file

@ -23,6 +23,7 @@ Notes:
#include "model_smt2_pp.h"
#include "uint_set.h"
#include "maxhs.h"
#include "opt_context.h"
namespace opt {
@ -74,8 +75,8 @@ namespace opt {
public:
maxhs(opt_solver* s, ast_manager& m, params_ref& p, vector<rational> const& ws, expr_ref_vector const& soft):
maxsmt_solver_base(s, m, p, ws, soft),
maxhs(context& c, vector<rational> const& ws, expr_ref_vector const& soft):
maxsmt_solver_base(c, ws, soft),
m_aux(m),
m_at_lower_bound(false) {
}
@ -528,7 +529,7 @@ namespace opt {
app_ref mk_fresh(sort* s) {
app_ref r(m);
r = m.mk_fresh_const("r", s);
m_mc->insert(r->get_decl());
m_c.fm().insert(r->get_decl());
return r;
}
@ -553,9 +554,9 @@ namespace opt {
};
maxsmt_solver_base* opt::mk_maxhs(ast_manager& m, opt_solver* s, params_ref& p,
maxsmt_solver_base* opt::mk_maxhs(context& c,
vector<rational> const& ws, expr_ref_vector const& soft) {
return alloc(maxhs, s, m, p, ws, soft);
return alloc(maxhs, c, ws, soft);
}
}

2
src/opt/maxhs.h
View file

@ -23,7 +23,7 @@ Notes:
#include "maxsmt.h"
namespace opt {
maxsmt_solver_base* mk_maxhs(ast_manager& m, opt_solver* s, params_ref& p,
maxsmt_solver_base* mk_maxhs(context& c,
vector<rational> const& ws, expr_ref_vector const& soft);
}
#endif

61
src/opt/maxres.cpp
View file

@ -60,6 +60,7 @@ Notes:
#include "mus.h"
#include "mss.h"
#include "inc_sat_solver.h"
#include "opt_context.h"
using namespace opt;
@ -83,10 +84,10 @@ private:
rational m_max_upper;
public:
maxres(ast_manager& m, opt_solver* s, params_ref& p,
maxres(context& c,
vector<rational> const& ws, expr_ref_vector const& soft,
strategy_t st):
maxsmt_solver_base(s, m, p, ws, soft),
maxsmt_solver_base(c, ws, soft),
m_B(m), m_asms(m),
m_mus(m_s, m),
m_mss(m_s, m),
@ -133,10 +134,9 @@ public:
}
lbool mus_solver() {
solver::scoped_push _sc(*m_s.get());
solver::scoped_push _sc(m_s);
init();
init_local();
enable_bvsat();
while (true) {
TRACE("opt",
display_vec(tout, m_asms.size(), m_asms.c_ptr());
@ -159,7 +159,6 @@ public:
});
for (unsigned i = 0; i < m_soft.size(); ++i) {
VERIFY(m_model->eval(m_soft[i].get(), tmp));
std::cout << mk_pp(m_soft[i].get(), m) << " -> " << tmp << "\n";
m_assignment[i] = m.is_true(tmp);
}
m_upper = m_lower;
@ -179,11 +178,10 @@ public:
}
lbool mus_mss_solver() {
solver::scoped_push _sc(*m_s.get());
solver::scoped_push _sc(s());
init();
init_local();
enable_bvsat();
enable_sls();
enable_sls(m_asms);
ptr_vector<expr> mcs;
vector<ptr_vector<expr> > cores;
while (m_lower < m_upper) {
@ -222,11 +220,32 @@ public:
return l_true;
}
lbool mss_solver() {
NOT_IMPLEMENTED_YET();
return l_undef;
solver::scoped_push _sc(s());
init();
init_local();
ptr_vector<expr> mcs;
while (m_lower < m_upper) {
lbool is_sat = s().check_sat(0, 0);
// is_sat = get_mcs(mcs);
switch (is_sat) {
case l_undef:
return l_undef;
case l_false:
m_lower = m_upper;
break;
case l_true:
//
is_sat = process_sat(mcs);
if (is_sat != l_true) {
return is_sat;
}
break;
}
}
m_lower = m_upper;
return l_true;
}
lbool operator()() {
@ -322,7 +341,7 @@ public:
}
lbool minimize_core(ptr_vector<expr>& core) {
if (m_sat_enabled) {
if (m_c.sat_enabled()) {
return l_true;
}
m_mus.reset();
@ -592,9 +611,9 @@ public:
void verify_assignment() {
IF_VERBOSE(0, verbose_stream() << "verify assignment\n";);
ref<solver> sat_solver = mk_inc_sat_solver(m, m_params);
for (unsigned i = 0; i < m_assertions.size(); ++i) {
sat_solver->assert_expr(m_assertions[i].get());
ref<solver> sat_solver = mk_inc_sat_solver(m, m_params);
for (unsigned i = 0; i < s().get_num_assertions(); ++i) {
sat_solver->assert_expr(s().get_assertion(i));
}
expr_ref n(m);
for (unsigned i = 0; i < m_soft.size(); ++i) {
@ -612,18 +631,18 @@ public:
};
opt::maxsmt_solver_base* opt::mk_maxres(ast_manager& m, opt_solver* s, params_ref& p,
opt::maxsmt_solver_base* opt::mk_maxres(context& c,
vector<rational> const& ws, expr_ref_vector const& soft) {
return alloc(maxres, m, s, p, ws, soft, maxres::s_mus);
return alloc(maxres, c, ws, soft, maxres::s_mus);
}
opt::maxsmt_solver_base* opt::mk_mus_mss_maxres(ast_manager& m, opt_solver* s, params_ref& p,
opt::maxsmt_solver_base* opt::mk_mus_mss_maxres(context& c,
vector<rational> const& ws, expr_ref_vector const& soft) {
return alloc(maxres, m, s, p, ws, soft, maxres::s_mus_mss);
return alloc(maxres, c, ws, soft, maxres::s_mus_mss);
}
opt::maxsmt_solver_base* opt::mk_mss_maxres(ast_manager& m, opt_solver* s, params_ref& p,
opt::maxsmt_solver_base* opt::mk_mss_maxres(context& c,
vector<rational> const& ws, expr_ref_vector const& soft) {
return alloc(maxres, m, s, p, ws, soft, maxres::s_mss);
return alloc(maxres, c, ws, soft, maxres::s_mss);
}

6
src/opt/maxres.h
View file

@ -23,15 +23,15 @@ Notes:
namespace opt {
maxsmt_solver_base* mk_maxres(
ast_manager& m, opt_solver* s, params_ref& p,
context& c,
vector<rational> const& ws, expr_ref_vector const& soft);
maxsmt_solver_base* mk_mus_mss_maxres(
ast_manager& m, opt_solver* s, params_ref& p,
context& c,
vector<rational> const& ws, expr_ref_vector const& soft);
maxsmt_solver_base* mk_mss_maxres(
ast_manager& m, opt_solver* s, params_ref& p,
context& c,
vector<rational> const& ws, expr_ref_vector const& soft);
};

12
src/opt/maxsls.cpp
View file

@ -26,16 +26,14 @@ namespace opt {
class sls : public maxsmt_solver_base {
public:
sls(opt_solver* s, ast_manager& m, params_ref& p,
vector<rational> const& ws, expr_ref_vector const& soft):
maxsmt_solver_base(s, m, p, ws, soft) {
sls(context& c, vector<rational> const& ws, expr_ref_vector const& soft):
maxsmt_solver_base(c, ws, soft) {
}
virtual ~sls() {}
lbool operator()() {
IF_VERBOSE(1, verbose_stream() << "(opt.sls)\n";);
enable_bvsat();
enable_sls();
init();
enable_sls(m_soft);
lbool is_sat = s().check_sat(0, 0);
if (is_sat == l_true) {
s().get_model(m_model);
@ -54,9 +52,9 @@ namespace opt {
};
maxsmt_solver_base* opt::mk_sls(ast_manager& m, opt_solver* s, params_ref& p,
maxsmt_solver_base* opt::mk_sls(context& c,
vector<rational> const& ws, expr_ref_vector const& soft) {
return alloc(sls, s, m, p, ws, soft);
return alloc(sls, c, ws, soft);
}

2
src/opt/maxsls.h
View file

@ -27,7 +27,7 @@ Notes:
namespace opt {
maxsmt_solver_base* mk_sls(ast_manager& m, opt_solver* s, params_ref& p,
maxsmt_solver_base* mk_sls(context& c,
vector<rational> const& ws, expr_ref_vector const& soft);

160
src/opt/maxsmt.cpp
View file

@ -24,12 +24,10 @@ Notes:
#include "maxres.h"
#include "maxhs.h"
#include "bcd2.h"
#include "wpm2.h"
#include "pbmax.h"
#include "wmax.h"
#include "maxsls.h"
#include "ast_pp.h"
#include "opt_params.hpp"
#include "pb_decl_plugin.h"
#include "pb_sls.h"
#include "tactical.h"
@ -38,19 +36,27 @@ Notes:
#include "qfbv_tactic.h"
#include "card2bv_tactic.h"
#include "uint_set.h"
#include "opt_sls_solver.h"
#include "pb_preprocess_tactic.h"
#include "inc_sat_solver.h"
#include "opt_context.h"
namespace opt {
maxsmt_solver_base::maxsmt_solver_base(
context& c, vector<rational> const& ws, expr_ref_vector const& soft):
m_s(c.get_solver()),
m(c.get_manager()),
m_c(c),
m_cancel(false), m_soft(m),
m_assertions(m) {
m_s.get_model(m_model);
SASSERT(m_model);
updt_params(c.params());
init_soft(ws, soft);
}
void maxsmt_solver_base::updt_params(params_ref& p) {
m_params.copy(p);
s().updt_params(p);
opt_params _p(p);
m_enable_sat = _p.enable_sat();
m_enable_sls = _p.enable_sls();
}
void maxsmt_solver_base::init_soft(vector<rational> const& weights, expr_ref_vector const& soft) {
@ -90,132 +96,68 @@ namespace opt {
}
}
struct maxsmt_solver_base::is_bv {
struct found {};
ast_manager& m;
pb_util pb;
bv_util bv;
is_bv(ast_manager& m): m(m), pb(m), bv(m) {}
void operator()(var *) { throw found(); }
void operator()(quantifier *) { throw found(); }
void operator()(app *n) {
family_id fid = n->get_family_id();
if (fid != m.get_basic_family_id() &&
fid != pb.get_family_id() &&
fid != bv.get_family_id() &&
!is_uninterp_const(n)) {
throw found();
}
}
};
bool maxsmt_solver_base::probe_bv() {
expr_fast_mark1 visited;
is_bv proc(m);
try {
unsigned sz = s().get_num_assertions();
for (unsigned i = 0; i < sz; i++) {
quick_for_each_expr(proc, visited, s().get_assertion(i));
}
sz = m_soft.size();
for (unsigned i = 0; i < sz; ++i) {
quick_for_each_expr(proc, visited, m_soft[i].get());
}
}
catch (is_bv::found) {
return false;
}
return true;
}
void maxsmt_solver_base::enable_inc_bvsat() {
m_params.set_bool("minimize_core", true);
solver* sat_solver = mk_inc_sat_solver(m, m_params);
unsigned sz = s().get_num_assertions();
for (unsigned i = 0; i < sz; ++i) {
sat_solver->assert_expr(s().get_assertion(i));
m_assertions.push_back(s().get_assertion(i));
}
m_s = sat_solver;
}
void maxsmt_solver_base::enable_bvsat() {
if (m_enable_sat && !m_sat_enabled && probe_bv()) {
enable_inc_bvsat();
m_sat_enabled = true;
}
}
void maxsmt_solver_base::enable_sls() {
if (m_enable_sls && !m_sls_enabled && probe_bv()) {
m_params.set_uint("restarts", 20);
unsigned lvl = m_s->get_scope_level();
sls_solver* sls = alloc(sls_solver, m, m_s.get(), m_soft, m_weights, m_params);
m_s = sls;
while (lvl > 0) { m_s->push(); --lvl; }
m_sls_enabled = true;
sls->opt(m_model);
}
}
void maxsmt_solver_base::set_mus(bool f) {
params_ref p;
p.set_bool("minimize_core", f);
m_s->updt_params(p);
m_s.updt_params(p);
}
void maxsmt_solver_base::enable_sls(expr_ref_vector const& soft) {
m_c.enable_sls(soft, m_weights);
}
app* maxsmt_solver_base::mk_fresh_bool(char const* name) {
app* result = m.mk_fresh_const(name, m.mk_bool_sort());
m_mc->insert(result->get_decl());
m_c.fm().insert(result->get_decl());
return result;
}
maxsmt::maxsmt(context& c):
m_s(c.get_solver()), m(c.get_manager()), m_c(c), m_cancel(false),
m_soft_constraints(m), m_answer(m) {}
lbool maxsmt::operator()(opt_solver* s) {
lbool maxsmt::operator()(solver* s) {
lbool is_sat;
m_msolver = 0;
m_s = s;
symbol const& maxsat_engine = m_c.maxsat_engine();
IF_VERBOSE(1, verbose_stream() << "(maxsmt)\n";);
TRACE("opt", tout << "maxsmt\n";);
if (m_soft_constraints.empty()) {
TRACE("opt", tout << "no constraints\n";);
m_msolver = 0;
is_sat = m_s->check_sat(0, 0);
is_sat = m_s.check_sat(0, 0);
}
else if (m_maxsat_engine == symbol("maxres")) {
m_msolver = mk_maxres(m, s, m_params, m_weights, m_soft_constraints);
else if (maxsat_engine == symbol("maxres")) {
m_msolver = mk_maxres(m_c, m_weights, m_soft_constraints);
}
else if (m_maxsat_engine == symbol("mus-mss-maxres")) {
m_msolver = mk_mus_mss_maxres(m, s, m_params, m_weights, m_soft_constraints);
else if (maxsat_engine == symbol("mus-mss-maxres")) {
m_msolver = mk_mus_mss_maxres(m_c, m_weights, m_soft_constraints);
}
else if (m_maxsat_engine == symbol("pbmax")) {
m_msolver = mk_pbmax(m, s, m_params, m_weights, m_soft_constraints);
else if (maxsat_engine == symbol("pbmax")) {
m_msolver = mk_pbmax(m_c, m_weights, m_soft_constraints);
}
else if (m_maxsat_engine == symbol("wpm2")) {
m_msolver = mk_wpm2(m, s, m_params, m_weights, m_soft_constraints);
else if (maxsat_engine == symbol("bcd2")) {
m_msolver = mk_bcd2(m_c, m_weights, m_soft_constraints);
}
else if (m_maxsat_engine == symbol("bcd2")) {
m_msolver = mk_bcd2(m, s, m_params, m_weights, m_soft_constraints);
else if (maxsat_engine == symbol("maxhs")) {
m_msolver = mk_maxhs(m_c, m_weights, m_soft_constraints);
}
else if (m_maxsat_engine == symbol("maxhs")) {
m_msolver = mk_maxhs(m, s, m_params, m_weights, m_soft_constraints);
}
else if (m_maxsat_engine == symbol("sls")) {
else if (maxsat_engine == symbol("sls")) {
// NB: this is experimental one-round version of SLS
m_msolver = mk_sls(m, s, m_params, m_weights, m_soft_constraints);
m_msolver = mk_sls(m_c, m_weights, m_soft_constraints);
}
else if (is_maxsat_problem(m_weights) && m_maxsat_engine == symbol("core_maxsat")) {
m_msolver = alloc(core_maxsat, m, *m_s, m_soft_constraints);
else if (is_maxsat_problem(m_weights) && maxsat_engine == symbol("core_maxsat")) {
m_msolver = alloc(core_maxsat, m_c, m_soft_constraints);
}
else if (is_maxsat_problem(m_weights) && m_maxsat_engine == symbol("fu_malik")) {
m_msolver = alloc(fu_malik, m, *m_s, m_soft_constraints);
else if (is_maxsat_problem(m_weights) && maxsat_engine == symbol("fu_malik")) {
m_msolver = alloc(fu_malik, m_c, m_soft_constraints);
}
else {
if (m_maxsat_engine != symbol::null && m_maxsat_engine != symbol("wmax")) {
if (maxsat_engine != symbol::null && maxsat_engine != symbol("wmax")) {
warning_msg("solver %s is not recognized, using default 'wmax'",
m_maxsat_engine.str().c_str());
maxsat_engine.str().c_str());
}
m_msolver = mk_wmax(m, m_s.get(), m_params, m_weights, m_soft_constraints);
m_msolver = mk_wmax(m_c, m_weights, m_soft_constraints);
}
if (m_msolver) {
@ -242,13 +184,12 @@ namespace opt {
}
void maxsmt::verify_assignment() {
m_s->push();
solver::scoped_push _sp(m_s);
commit_assignment();
if (l_true != m_s->check_sat(0,0)) {
if (l_true != m_s.check_sat(0,0)) {
IF_VERBOSE(0, verbose_stream() << "could not verify assignment\n";);
UNREACHABLE();
}
m_s->pop(1);
}
bool maxsmt::get_assignment(unsigned idx) const {
@ -292,7 +233,6 @@ namespace opt {
}
void maxsmt::commit_assignment() {
SASSERT(m_s);
for (unsigned i = 0; i < m_soft_constraints.size(); ++i) {
expr_ref tmp(m);
tmp = m_soft_constraints[i].get();
@ -300,7 +240,7 @@ namespace opt {
tmp = m.mk_not(tmp);
}
TRACE("opt", tout << "committing: " << tmp << "\n";);
m_s->assert_expr(tmp);
m_s.assert_expr(tmp);
}
}
@ -337,9 +277,7 @@ namespace opt {
}
void maxsmt::updt_params(params_ref& p) {
opt_params _p(p);
m_maxsat_engine = _p.maxsat_engine();
m_params = p;
m_params.append(p);
if (m_msolver) {
m_msolver->updt_params(p);
}

70
src/opt/maxsmt.h
View file

@ -19,11 +19,16 @@ Notes:
#ifndef _OPT_MAXSMT_H_
#define _OPT_MAXSMT_H_
#include "opt_solver.h"
#include "statistics.h"
#include"ast.h"
#include"params.h"
#include"solver.h"
#include"filter_model_converter.h"
#include"statistics.h"
namespace opt {
class context;
class maxsmt_solver {
public:
virtual ~maxsmt_solver() {}
@ -44,8 +49,9 @@ namespace opt {
//
class maxsmt_solver_base : public maxsmt_solver {
protected:
ref<solver> m_s;
solver& m_s;
ast_manager& m;
context& m_c;
volatile bool m_cancel;
expr_ref_vector m_soft;
expr_ref_vector m_assertions;
@ -53,55 +59,30 @@ namespace opt {
rational m_lower;
rational m_upper;
model_ref m_model;
ref<filter_model_converter> m_mc; // model converter to remove fresh variables
svector<bool> m_assignment; // truth assignment to soft constraints
params_ref m_params; // config
bool m_enable_sls; // config
bool m_enable_sat; // config
bool m_sls_enabled;
bool m_sat_enabled;
struct is_bv;
public:
maxsmt_solver_base(opt_solver* s, ast_manager& m, params_ref& p,
vector<rational> const& ws, expr_ref_vector const& soft):
m_s(s), m(m), m_cancel(false), m_soft(m),
m_assertions(m),
m_enable_sls(false), m_enable_sat(false),
m_sls_enabled(false), m_sat_enabled(false) {
m_s->get_model(m_model);
SASSERT(m_model);
updt_params(p);
set_converter(s->mc_ref().get());
init_soft(ws, soft);
}
maxsmt_solver_base(context& c, vector<rational> const& ws, expr_ref_vector const& soft);
virtual ~maxsmt_solver_base() {}
virtual rational get_lower() const { return m_lower; }
virtual rational get_upper() const { return m_upper; }
virtual bool get_assignment(unsigned index) const { return m_assignment[index]; }
virtual void set_cancel(bool f) { m_cancel = f; m_s->set_cancel(f); }
virtual void collect_statistics(statistics& st) const {
if (m_sls_enabled || m_sat_enabled) {
m_s->collect_statistics(st);
}
}
virtual void set_cancel(bool f) { m_cancel = f; s().set_cancel(f); }
virtual void collect_statistics(statistics& st) const { }
virtual void get_model(model_ref& mdl) { mdl = m_model.get(); }
void set_model() { s().get_model(m_model); }
virtual void updt_params(params_ref& p);
virtual void init_soft(vector<rational> const& weights, expr_ref_vector const& soft);
void add_hard(expr* e){ s().assert_expr(e); }
solver& s() { return *m_s; }
void set_converter(filter_model_converter* mc) { m_mc = mc; }
solver& s() { return m_s; }
void init();
expr* mk_not(expr* e);
bool probe_bv();
void set_mus(bool f);
void enable_bvsat();
void enable_sls();
app* mk_fresh_bool(char const* name);
private:
void enable_inc_bvsat();
protected:
void enable_sls(expr_ref_vector const& soft);
};
/**
@ -110,32 +91,27 @@ namespace opt {
*/
class maxsmt {
ast_manager& m;
ref<opt_solver> m_s;
ast_manager& m;
solver& m_s;
context& m_c;
scoped_ptr<maxsmt_solver> m_msolver;
volatile bool m_cancel;
expr_ref_vector m_soft_constraints;
expr_ref_vector m_answer;
vector<rational> m_weights;
rational m_lower;
rational m_upper;
scoped_ptr<maxsmt_solver> m_msolver;
symbol m_maxsat_engine;
model_ref m_model;
params_ref m_params;
public:
maxsmt(ast_manager& m): m(m), m_s(0), m_cancel(false), m_soft_constraints(m), m_answer(m) {}
lbool operator()(opt_solver* s);
maxsmt(context& c);
lbool operator()(solver* s);
void set_cancel(bool f);
void updt_params(params_ref& p);
void add(expr* f, rational const& w);
unsigned size() const { return m_soft_constraints.size(); }
expr* operator[](unsigned idx) const { return m_soft_constraints[idx]; }
rational weight(unsigned idx) const { return m_weights[idx]; }
void commit_assignment();
rational get_value() const;
rational get_lower() const;
@ -146,13 +122,9 @@ namespace opt {
bool get_assignment(unsigned index) const;
void display_answer(std::ostream& out) const;
void collect_statistics(statistics& st) const;
private:
bool is_maxsat_problem(vector<rational> const& ws) const;
void verify_assignment();
};
};

14
src/opt/mss.cpp
View file

@ -26,21 +26,21 @@ Notes:
namespace opt {
mss::mss(ref<solver>& s, ast_manager& m): m_s(s), m(m), m_cancel(false) {
mss::mss(solver& s, ast_manager& m): m_s(s), m(m), m_cancel(false) {
}
mss::~mss() {
}
bool mss::check_result() {
lbool is_sat = m_s->check_sat(m_mss.size(), m_mss.c_ptr());
lbool is_sat = m_s.check_sat(m_mss.size(), m_mss.c_ptr());
if (is_sat == l_undef) return true;
SASSERT(is_sat == l_true);
if (is_sat == l_false) return false;
expr_set::iterator it = m_mcs.begin(), end = m_mcs.end();
for (; it != end; ++it) {
m_mss.push_back(*it);
is_sat = m_s->check_sat(m_mss.size(), m_mss.c_ptr());
is_sat = m_s.check_sat(m_mss.size(), m_mss.c_ptr());
m_mss.pop_back();
if (is_sat == l_undef) return true;
SASSERT(is_sat == l_false);
@ -147,7 +147,7 @@ namespace opt {
lbool mss::operator()(vector<exprs> const& _cores, exprs& literals, exprs& mcs) {
m_mss.reset();
m_todo.reset();
m_s->get_model(m_model);
m_s.get_model(m_model);
SASSERT(m_model);
vector<exprs> cores(_cores);
TRACE("opt",
@ -207,12 +207,12 @@ namespace opt {
TRACE("opt", display_vec(tout << "process (total " << core.size() << ") :", sz, core.c_ptr()););
unsigned sz_save = m_mss.size();
m_mss.append(sz, core.c_ptr());
lbool is_sat = m_s->check_sat(m_mss.size(), m_mss.c_ptr());
IF_VERBOSE(1, display_vec(verbose_stream(), sz, core.c_ptr()););
lbool is_sat = m_s.check_sat(m_mss.size(), m_mss.c_ptr());
IF_VERBOSE(2, display_vec(verbose_stream() << "mss: ", m_mss.size(), m_mss.c_ptr()););
m_mss.resize(sz_save);
switch (is_sat) {
case l_true:
m_s->get_model(m_model);
m_s.get_model(m_model);
update_mss();
DEBUG_CODE(
for (unsigned i = 0; i < sz; ++i) {

4
src/opt/mss.h
View file

@ -21,7 +21,7 @@ Notes:
namespace opt {
class mss {
ref<solver>& m_s;
solver& m_s;
ast_manager& m;
volatile bool m_cancel;
typedef ptr_vector<expr> exprs;
@ -32,7 +32,7 @@ namespace opt {
exprs m_todo;
model_ref m_model;
public:
mss(ref<solver>& s, ast_manager& m);
mss(solver& s, ast_manager& m);
~mss();
lbool operator()(vector<exprs> const& cores, exprs& literals, exprs& mcs);

20
src/opt/mus.cpp
View file

@ -29,13 +29,13 @@ using namespace opt;
//
struct mus::imp {
ref<solver>& m_s;
ast_manager& m;
expr_ref_vector m_cls2expr;
obj_map<expr, unsigned> m_expr2cls;
volatile bool m_cancel;
solver& m_s;
ast_manager& m;
expr_ref_vector m_cls2expr;
obj_map<expr, unsigned> m_expr2cls;
volatile bool m_cancel;
imp(ref<solver>& s, ast_manager& m):
imp(solver& s, ast_manager& m):
m_s(s), m(m), m_cls2expr(m), m_cancel(false)
{}
@ -92,7 +92,7 @@ struct mus::imp {
unsigned sz = assumptions.size();
assumptions.push_back(not_cls);
add_core(core, assumptions);
lbool is_sat = m_s->check_sat(assumptions.size(), assumptions.c_ptr());
lbool is_sat = m_s.check_sat(assumptions.size(), assumptions.c_ptr());
assumptions.resize(sz);
switch (is_sat) {
case l_undef:
@ -103,7 +103,7 @@ struct mus::imp {
break;
default:
core_exprs.reset();
m_s->get_unsat_core(core_exprs);
m_s.get_unsat_core(core_exprs);
if (!core_exprs.contains(not_cls)) {
// core := core_exprs \ mus
core.reset();
@ -124,7 +124,7 @@ struct mus::imp {
for (unsigned i = 0; i < mus.size(); ++i) {
assumptions.push_back(m_cls2expr[mus[i]].get());
}
lbool is_sat = m_s->check_sat(assumptions.size(), assumptions.c_ptr());
lbool is_sat = m_s.check_sat(assumptions.size(), assumptions.c_ptr());
SASSERT(is_sat == l_false);
);
#endif
@ -147,7 +147,7 @@ struct mus::imp {
};
mus::mus(ref<solver>& s, ast_manager& m) {
mus::mus(solver& s, ast_manager& m) {
m_imp = alloc(imp, s, m);
}

2
src/opt/mus.h
View file

@ -24,7 +24,7 @@ namespace opt {
struct imp;
imp * m_imp;
public:
mus(ref<solver>& s, ast_manager& m);
mus(solver& s, ast_manager& m);
~mus();
/**
Add soft constraint.

208
src/opt/opt_context.cpp
View file

@ -34,8 +34,10 @@ Notes:
#include "tactical.h"
#include "model_smt2_pp.h"
#include "card2bv_tactic.h"
#include "bvsls_opt_solver.h"
#include "nnf_tactic.h"
#include "inc_sat_solver.h"
#include "bv_decl_plugin.h"
#include "pb_decl_plugin.h"
namespace opt {
@ -114,13 +116,18 @@ namespace opt {
m_arith(m),
m_bv(m),
m_hard_constraints(m),
m_solver(0),
m_optsmt(m),
m_scoped_state(m),
m_objective_refs(m)
m_fm(m),
m_objective_refs(m),
m_enable_sat(false),
m_enable_sls(false)
{
m_params.set_bool("model", true);
m_params.set_bool("unsat_core", true);
m_solver = alloc(opt_solver, m, m_params, symbol());
params_ref p;
p.set_bool("model", true);
p.set_bool("unsat_core", true);
updt_params(p);
}
context::~context() {
@ -172,9 +179,7 @@ namespace opt {
objective& obj = s.m_objectives[i];
m_objectives.push_back(obj);
if (obj.m_type == O_MAXSMT) {
maxsmt* ms = alloc(maxsmt, m);
ms->updt_params(m_params);
m_maxsmts.insert(obj.m_id, ms);
add_maxsmt(obj.m_id);
}
}
m_hard_constraints.append(s.m_hard);
@ -184,18 +189,19 @@ namespace opt {
if (m_pareto) {
return execute_pareto();
}
import_scoped_state();
init_solver();
import_scoped_state();
normalize();
internalize();
opt_solver& s = get_solver();
solver::scoped_push _sp(s);
update_solver();
solver& s = get_solver();
for (unsigned i = 0; i < m_hard_constraints.size(); ++i) {
TRACE("opt", tout << "Hard constraint: " << mk_ismt2_pp(m_hard_constraints[i].get(), m) << std::endl;);
s.assert_expr(m_hard_constraints[i].get());
}
IF_VERBOSE(1, verbose_stream() << "(optimize:check-sat)\n";);
lbool is_sat = s.check_sat_core(0,0);
lbool is_sat = s.check_sat(0,0);
TRACE("opt", tout << "initial search result: " << is_sat << "\n";);
if (is_sat != l_true) {
m_model = 0;
@ -203,7 +209,7 @@ namespace opt {
}
IF_VERBOSE(1, verbose_stream() << "(optimize:sat)\n";);
s.get_model(m_model);
m_optsmt.setup(s);
m_optsmt.setup(*m_opt_solver.get());
update_lower(true);
switch (m_objectives.size()) {
case 0:
@ -214,7 +220,6 @@ namespace opt {
opt_params optp(m_params);
symbol pri = optp.priority();
if (pri == symbol("pareto")) {
_sp.disable_pop();
return execute_pareto();
}
else if (pri == symbol("box")) {
@ -233,7 +238,7 @@ namespace opt {
if (m_model_converter) {
(*m_model_converter)(mdl, 0);
}
get_solver().mc()(mdl, 0);
m_fm(mdl, 0);
}
}
@ -243,7 +248,7 @@ namespace opt {
if (result == l_true) m_optsmt.get_model(m_model);
return result;
}
lbool context::execute_maxsat(symbol const& id, bool committed) {
model_ref tmp;
maxsmt& ms = *m_maxsmts.find(id);
@ -265,7 +270,10 @@ namespace opt {
lbool context::execute_lex() {
lbool r = l_true;
for (unsigned i = 0; r == l_true && i < m_objectives.size(); ++i) {
bool is_last = i + 1 == m_objectives.size();
if (!is_last) get_solver().push();
r = execute(m_objectives[i], i + 1 < m_objectives.size());
if (!is_last) get_solver().pop(1);
if (r == l_true && !get_lower_as_num(i).is_finite()) {
return r;
}
@ -282,9 +290,8 @@ namespace opt {
for (unsigned i = 0; r == l_true && i < m_objectives.size(); ++i) {
objective const& obj = m_objectives[i];
if (obj.m_type == O_MAXSMT) {
get_solver().push();
solver::scoped_push _sp(get_solver());
r = execute(obj, false);
get_solver().pop(1);
}
}
return r;
@ -381,12 +388,13 @@ namespace opt {
}
lbool context::execute_pareto() {
if (!m_pareto) {
m_pareto = alloc(gia_pareto, m, *this, m_solver.get(), m_params);
set_pareto(alloc(gia_pareto, m, *this, m_solver.get(), m_params));
}
lbool is_sat = (*(m_pareto.get()))();
if (is_sat != l_true) {
m_pareto = 0;
set_pareto(0);
}
if (is_sat == l_true) {
yield();
@ -395,7 +403,6 @@ namespace opt {
m_solver->pop(1);
}
return is_sat;
// NB. fix race condition for set_cancel
}
void context::display_bounds(std::ostream& out, bounds_t const& b) const {
@ -411,10 +418,98 @@ namespace opt {
}
}
opt_solver& context::get_solver() {
solver& context::get_solver() {
return *m_solver.get();
}
void context::init_solver() {
#pragma omp critical (opt_context)
{
m_opt_solver = alloc(opt_solver, m, m_params, m_fm, symbol());
m_solver = m_opt_solver.get();
}
}
void context::update_solver() {
if (!m_enable_sat || !probe_bv()) {
return;
}
if (m_maxsat_engine != symbol("maxres") &&
m_maxsat_engine != symbol("mus-mss-maxres") &&
m_maxsat_engine != symbol("bcd2") &&
m_maxsat_engine != symbol("sls")) {
return;
}
m_params.set_bool("minimize_core", true);
m_sat_solver = mk_inc_sat_solver(m, m_params);
unsigned sz = get_solver().get_num_assertions();
for (unsigned i = 0; i < sz; ++i) {
m_sat_solver->assert_expr(get_solver().get_assertion(i));
}
#pragma omp critical (opt_context)
{
m_solver = m_sat_solver.get();
}
}
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()) {
set_soft_inc_sat(m_sat_solver.get(), soft.size(), soft.c_ptr(), weights.c_ptr());
}
}
struct context::is_bv {
struct found {};
ast_manager& m;
pb_util pb;
bv_util bv;
is_bv(ast_manager& m): m(m), pb(m), bv(m) {}
void operator()(var *) { throw found(); }
void operator()(quantifier *) { throw found(); }
void operator()(app *n) {
family_id fid = n->get_family_id();
if (fid != m.get_basic_family_id() &&
fid != pb.get_family_id() &&
fid != bv.get_family_id() &&
!is_uninterp_const(n)) {
throw found();
}
}
};
bool context::probe_bv() {
expr_fast_mark1 visited;
is_bv proc(m);
try {
for (unsigned i = 0; i < m_objectives.size(); ++i) {
objective & obj = m_objectives[i];
if (obj.m_type != O_MAXSMT) return false;
maxsmt& ms = *m_maxsmts.find(obj.m_id);
for (unsigned j = 0; j < ms.size(); ++j) {
quick_for_each_expr(proc, visited, ms[j]);
}
}
unsigned sz = get_solver().get_num_assertions();
for (unsigned i = 0; i < sz; i++) {
quick_for_each_expr(proc, visited, get_solver().get_assertion(i));
}
}
catch (is_bv::found) {
return false;
}
return true;
}
void context::add_maxsmt(symbol const& id) {
maxsmt* ms = alloc(maxsmt, *this);
ms->updt_params(m_params);
#pragma omp critical (opt_context)
{
m_maxsmts.insert(id, ms);
}
}
bool context::is_numeral(expr* e, rational & n) const {
unsigned sz;
return m_arith.is_numeral(e, n) || m_bv.is_numeral(e, n, sz);
@ -440,28 +535,16 @@ namespace opt {
mk_simplify_tactic(m));
opt_params optp(m_params);
tactic_ref tac2, tac3;
if (optp.engine() == "bvsls") {
if (optp.elim_01()) {
tac2 = mk_elim01_tactic(m);
tac3 = mk_lia2card_tactic(m);
params_ref lia_p;
lia_p.set_bool("compile_equality", optp.pb_compile_equality());
tac3->updt_params(lia_p);
m_simplify = and_then(tac0.get(), tac2.get(), tac3.get(),
mk_card2bv_tactic(m),
mk_simplify_tactic(m),
mk_nnf_tactic(m));
m_solver = alloc(bvsls_opt_solver, m, m_params);
}
else if (optp.elim_01()) {
tac2 = mk_elim01_tactic(m);
tac3 = mk_lia2card_tactic(m);
params_ref lia_p;
lia_p.set_bool("compile_equality", optp.pb_compile_equality());
tac3->updt_params(lia_p);
m_simplify = and_then(tac0.get(), tac2.get(), tac3.get());
set_simplify(and_then(tac0.get(), tac2.get(), tac3.get()));
}
else {
m_simplify = tac0.get();
set_simplify(tac0.get());
}
proof_converter_ref pc;
expr_dependency_ref core(m);
@ -657,9 +740,7 @@ namespace opt {
obj.m_type = O_MAXSMT;
obj.m_weights.append(weights);
SASSERT(!m_maxsmts.contains(id));
maxsmt* ms = alloc(maxsmt, m);
ms->updt_params(m_params);
m_maxsmts.insert(id, ms);
add_maxsmt(id);
}
SASSERT(obj.m_id == id);
obj.m_terms.reset();
@ -899,22 +980,39 @@ namespace opt {
default: return expr_ref(m_arith.mk_add(args.size(), args.c_ptr()), m);
}
}
void context::set_simplify(tactic* tac) {
#pragma omp critical (opt_context)
{
m_simplify = tac;
}
}
void context::set_pareto(pareto_base* p) {
#pragma omp critical (opt_context)
{
m_pareto = p;
}
}
void context::set_cancel(bool f) {
if (m_solver) {
m_solver->set_cancel(f);
}
if (m_simplify) {
m_simplify->set_cancel(f);
}
if (m_pareto) {
m_pareto->set_cancel(f);
#pragma omp critical (opt_context)
{
if (m_solver) {
m_solver->set_cancel(f);
}
if (m_pareto) {
m_pareto->set_cancel(f);
}
if (m_simplify) {
m_simplify->set_cancel(f);
}
map_t::iterator it = m_maxsmts.begin(), end = m_maxsmts.end();
for (; it != end; ++it) {
it->m_value->set_cancel(f);
}
}
m_optsmt.set_cancel(f);
map_t::iterator it = m_maxsmts.begin(), end = m_maxsmts.end();
for (; it != end; ++it) {
it->m_value->set_cancel(f);
}
}
void context::collect_statistics(statistics& stats) const {
@ -944,6 +1042,10 @@ namespace opt {
for (; it != end; ++it) {
it->m_value->updt_params(m_params);
}
opt_params _p(p);
m_enable_sat = _p.enable_sat();
m_enable_sls = _p.enable_sls();
m_maxsat_engine = _p.maxsat_engine();
}
typedef obj_hashtable<func_decl> func_decl_set;

28
src/opt/opt_context.h
View file

@ -108,7 +108,9 @@ namespace opt {
arith_util m_arith;
bv_util m_bv;
expr_ref_vector m_hard_constraints;
ref<opt_solver> m_solver;
ref<opt_solver> m_opt_solver;
ref<solver> m_solver;
ref<solver> m_sat_solver;
scoped_ptr<pareto_base> m_pareto;
params_ref m_params;
optsmt m_optsmt;
@ -116,11 +118,15 @@ namespace opt {
scoped_state m_scoped_state;
vector<objective> m_objectives;
model_ref m_model;
model_converter_ref m_model_converter;
model_converter_ref m_model_converter;
filter_model_converter m_fm;
obj_map<func_decl, unsigned> m_objective_fns;
obj_map<func_decl, expr*> m_objective_orig;
func_decl_ref_vector m_objective_refs;
tactic_ref m_simplify;
bool m_enable_sat;
bool m_enable_sls;
symbol m_maxsat_engine;
public:
context(ast_manager& m);
virtual ~context();
@ -163,6 +169,15 @@ namespace opt {
virtual expr_ref mk_ge(unsigned i, model_ref& model);
virtual expr_ref mk_le(unsigned i, model_ref& model);
smt::context& smt_context() { return m_opt_solver->get_context(); }
filter_model_converter& fm() { return m_fm; }
bool sat_enabled() const { return 0 != m_sat_solver.get(); }
solver& get_solver();
ast_manager& get_manager() { return this->m; }
params_ref& params() { return m_params; }
void enable_sls(expr_ref_vector const& soft, vector<rational> const& weights);
symbol const& maxsat_engine() const { return m_maxsat_engine; }
private:
void validate_feasibility(maxsmt& ms);
@ -199,7 +214,14 @@ namespace opt {
inf_eps get_upper_as_num(unsigned idx);
opt_solver& get_solver();
struct is_bv;
bool probe_bv();
void init_solver();
void update_solver();
void add_maxsmt(symbol const& id);
void set_simplify(tactic *simplify);
void set_pareto(pareto_base* p);
bool is_numeral(expr* e, rational& n) const;

11
src/opt/opt_solver.cpp
View file

@ -35,13 +35,14 @@ Notes:
namespace opt {
opt_solver::opt_solver(ast_manager & mgr, params_ref const & p, symbol const & l):
opt_solver::opt_solver(ast_manager & mgr, params_ref const & p,
filter_model_converter& fm, symbol const & l):
solver_na2as(mgr),
m_params(p),
m_context(mgr, m_params),
m(mgr),
m_dump_benchmarks(false),
m_fm(alloc(filter_model_converter, m)) {
m_fm(fm) {
m_logic = l;
if (m_logic != symbol::null) {
m_context.set_logic(m_logic);
@ -233,20 +234,20 @@ namespace opt {
if (typeid(smt::theory_inf_arith) == typeid(opt)) {
smt::theory_inf_arith& th = dynamic_cast<smt::theory_inf_arith&>(opt);
return expr_ref(th.mk_ge(mc(), v, val), m);
return expr_ref(th.mk_ge(m_fm, v, val), m);
}
if (typeid(smt::theory_mi_arith) == typeid(opt)) {
smt::theory_mi_arith& th = dynamic_cast<smt::theory_mi_arith&>(opt);
SASSERT(val.is_finite());
return expr_ref(th.mk_ge(mc(), v, val.get_numeral()), m);
return expr_ref(th.mk_ge(m_fm, v, val.get_numeral()), m);
}
if (typeid(smt::theory_i_arith) == typeid(opt)) {
SASSERT(val.is_finite());
SASSERT(val.get_infinitesimal().is_zero());
smt::theory_i_arith& th = dynamic_cast<smt::theory_i_arith&>(opt);
return expr_ref(th.mk_ge(mc(), v, val.get_rational()), m);
return expr_ref(th.mk_ge(m_fm, v, val.get_rational()), m);
}
// difference logic?

7
src/opt/opt_solver.h
View file

@ -42,6 +42,7 @@ namespace opt {
smt_params m_params;
smt::kernel m_context;
ast_manager& m;
filter_model_converter& m_fm;
progress_callback * m_callback;
symbol m_logic;
bool m_objective_enabled;
@ -50,9 +51,8 @@ namespace opt {
bool m_dump_benchmarks;
static unsigned m_dump_count;
statistics m_stats;
ref<filter_model_converter> m_fm;
public:
opt_solver(ast_manager & m, params_ref const & p, symbol const & l);
opt_solver(ast_manager & m, params_ref const & p, filter_model_converter& fm, symbol const & l);
virtual ~opt_solver();
virtual void updt_params(params_ref & p);
@ -82,9 +82,6 @@ namespace opt {
inf_eps const & get_objective_value(unsigned obj_index);
expr_ref mk_ge(unsigned obj_index, inf_eps const& val);
filter_model_converter& mc() { return *(m_fm.get()); }
ref<filter_model_converter>& mc_ref() { return m_fm; }
static opt_solver& to_opt(solver& s);
bool dump_benchmarks();

10
src/opt/pbmax.cpp
View file

@ -31,16 +31,14 @@ namespace opt {
class pbmax : public maxsmt_solver_base {
public:
pbmax(opt_solver* s, ast_manager& m, params_ref& p,
pbmax(context& c,
vector<rational> const& ws, expr_ref_vector const& soft):
maxsmt_solver_base(s, m, p, ws, soft) {
maxsmt_solver_base(c, ws, soft) {
}
virtual ~pbmax() {}
lbool operator()() {
enable_bvsat();
enable_sls();
TRACE("opt", s().display(tout); tout << "\n";
for (unsigned i = 0; i < m_soft.size(); ++i) {
@ -90,9 +88,9 @@ namespace opt {
}
};
maxsmt_solver_base* opt::mk_pbmax(ast_manager& m, opt_solver* s, params_ref& p,
maxsmt_solver_base* opt::mk_pbmax(context & c,
vector<rational> const& ws, expr_ref_vector const& soft) {
return alloc(pbmax, s, m, p, ws, soft);
return alloc(pbmax, c, ws, soft);
}
}

2
src/opt/pbmax.h
View file

@ -23,7 +23,7 @@ Notes:
#include "maxsmt.h"
namespace opt {
maxsmt_solver_base* mk_pbmax(ast_manager& m, opt_solver* s, params_ref& p,
maxsmt_solver_base* mk_pbmax(context& c,
vector<rational> const& ws, expr_ref_vector const& soft);
}

18
src/opt/wmax.cpp
View file

@ -23,15 +23,15 @@ Notes:
#include "smt_theory.h"
#include "smt_context.h"
#include "theory_wmaxsat.h"
#include "opt_context.h"
namespace opt {
class maxsmt_solver_wbase : public maxsmt_solver_base {
smt::context& ctx;
public:
maxsmt_solver_wbase(opt_solver* s, ast_manager& m, smt::context& ctx, params_ref& p,
maxsmt_solver_wbase(context& c,
vector<rational> const& ws, expr_ref_vector const& soft):
maxsmt_solver_base(s, m, p, ws, soft), ctx(ctx) {}
maxsmt_solver_base(c, ws, soft), ctx(c.smt_context()) {}
~maxsmt_solver_wbase() {}
class scoped_ensure_theory {
@ -52,7 +52,7 @@ namespace opt {
wth->reset();
}
else {
wth = alloc(smt::theory_wmaxsat, m, m_mc);
wth = alloc(smt::theory_wmaxsat, m, m_c.fm());
ctx.register_plugin(wth);
}
return wth;
@ -76,9 +76,9 @@ namespace opt {
class wmax : public maxsmt_solver_wbase {
public:
wmax(opt_solver* s, ast_manager& m, smt::context& ctx, params_ref& p,
wmax(context& c,
vector<rational> const& ws, expr_ref_vector const& soft):
maxsmt_solver_wbase(s, m, ctx, p, ws, soft) {}
maxsmt_solver_wbase(c, ws, soft) {}
virtual ~wmax() {}
lbool operator()() {
@ -122,9 +122,9 @@ namespace opt {
}
};
maxsmt_solver_base* opt::mk_wmax(ast_manager& m, opt_solver* s, params_ref& p,
vector<rational> const& ws, expr_ref_vector const& soft) {
return alloc(wmax, s, m, s->get_context(), p, ws, soft);
maxsmt_solver_base* opt::mk_wmax(context& c,
vector<rational> const& ws, expr_ref_vector const& soft) {
return alloc(wmax, c, ws, soft);
}
}

2
src/opt/wmax.h
View file

@ -23,7 +23,7 @@ Notes:
#include "maxsmt.h"
namespace opt {
maxsmt_solver_base* mk_wmax(ast_manager& m, opt_solver* s, params_ref& p,
maxsmt_solver_base* mk_wmax(context& c,
vector<rational> const& ws, expr_ref_vector const& soft);
}

251
src/opt/wpm2.cpp
View file

@ -1,251 +0,0 @@
/*++
Copyright (c) 2014 Microsoft Corporation
Module Name:
wpm2.cpp
Abstract:
wpn2 based MaxSAT.
Author:
Nikolaj Bjorner (nbjorner) 2014-4-17
Notes:
--*/
#include "wpm2.h"
#include "pbmax.h"
#include "pb_decl_plugin.h"
#include "uint_set.h"
#include "ast_pp.h"
#include "model_smt2_pp.h"
namespace opt {
// ------------------------------------------------------
// AAAI 2010
class wpm2 : public maxsmt_solver_base {
scoped_ptr<maxsmt_solver_base> maxs;
public:
wpm2(opt_solver* s, ast_manager& m, maxsmt_solver_base* _maxs, params_ref& p,
vector<rational> const& ws, expr_ref_vector const& soft):
maxsmt_solver_base(s, m, p, ws, soft), maxs(_maxs) {
}
virtual ~wpm2() {}
lbool operator()() {
enable_sls();
IF_VERBOSE(1, verbose_stream() << "(opt.wpm2)\n";);
solver::scoped_push _s(s());
pb_util u(m);
app_ref fml(m), a(m), b(m), c(m);
expr_ref val(m);
expr_ref_vector block(m), ans(m), al(m), am(m);
obj_map<expr, unsigned> ans_index;
vector<rational> amk;
vector<uint_set> sc;
init();
for (unsigned i = 0; i < m_soft.size(); ++i) {
rational w = m_weights[i];
b = mk_fresh_bool("b");
block.push_back(b);
expr* bb = b;
a = mk_fresh_bool("a");
ans.push_back(a);
ans_index.insert(a, i);
fml = m.mk_or(m_soft[i].get(), b, m.mk_not(a));
s().assert_expr(fml);
c = mk_fresh_bool("c");
fml = m.mk_implies(c, u.mk_le(1,&w,&bb,rational(0)));
s().assert_expr(fml);
sc.push_back(uint_set());
sc.back().insert(i);
am.push_back(c);
amk.push_back(rational(0));
}
while (true) {
expr_ref_vector asms(m);
ptr_vector<expr> core;
asms.append(ans);
asms.append(am);
lbool is_sat = s().check_sat(asms.size(), asms.c_ptr());
TRACE("opt",
tout << "\nassumptions: ";
for (unsigned i = 0; i < asms.size(); ++i) {
tout << mk_pp(asms[i].get(), m) << " ";
}
tout << "\n" << is_sat << "\n";
tout << "upper: " << m_upper << "\n";
tout << "lower: " << m_lower << "\n";
if (is_sat == l_true) {
model_ref mdl;
s().get_model(mdl);
model_smt2_pp(tout, m, *(mdl.get()), 0);
});
if (m_cancel && is_sat != l_false) {
is_sat = l_undef;
}
if (is_sat == l_true) {
m_upper = m_lower;
s().get_model(m_model);
for (unsigned i = 0; i < block.size(); ++i) {
VERIFY(m_model->eval(m_soft[i].get(), val));
TRACE("opt", tout << mk_pp(block[i].get(), m) << " " << val << "\n";);
m_assignment[i] = m.is_true(val);
}
}
if (is_sat != l_false) {
return is_sat;
}
s().get_unsat_core(core);
if (core.empty()) {
return l_false;
}
TRACE("opt",
tout << "core: ";
for (unsigned i = 0; i < core.size(); ++i) {
tout << mk_pp(core[i],m) << " ";
}
tout << "\n";);
uint_set A;
for (unsigned i = 0; i < core.size(); ++i) {
unsigned j;
if (ans_index.find(core[i], j)) {
A.insert(j);
}
}
if (A.empty()) {
return l_false;
}
uint_set B;
rational k(0);
rational old_lower(m_lower);
for (unsigned i = 0; i < sc.size(); ++i) {
uint_set t(sc[i]);
t &= A;
if (!t.empty()) {
B |= sc[i];
k += amk[i];
m_lower -= amk[i];
sc[i] = sc.back();
sc.pop_back();
am[i] = am.back();
am.pop_back();
amk[i] = amk.back();
amk.pop_back();
--i;
}
}
vector<rational> ws;
expr_ref_vector bs(m);
for (unsigned i = 0; i < m_soft.size(); ++i) {
if (B.contains(i)) {
ws.push_back(m_weights[i]);
bs.push_back(block[i].get());
}
}
TRACE("opt", tout << "at most bound: " << k << "\n";);
is_sat = new_bound(al, ws, bs, k);
if (is_sat != l_true) {
return is_sat;
}
m_lower += k;
SASSERT(m_lower > old_lower);
TRACE("opt", tout << "new bound: " << m_lower << "\n";);
expr_ref B_le_k(m), B_ge_k(m);
B_le_k = u.mk_le(ws.size(), ws.c_ptr(), bs.c_ptr(), k);
B_ge_k = u.mk_ge(ws.size(), ws.c_ptr(), bs.c_ptr(), k);
s().assert_expr(B_ge_k);
al.push_back(B_ge_k);
IF_VERBOSE(1, verbose_stream() << "(opt.wpm2 [" << m_lower << ":" << m_upper << "])\n";);
IF_VERBOSE(2, verbose_stream() << "New lower bound: " << B_ge_k << "\n";);
c = mk_fresh_bool("c");
fml = m.mk_implies(c, B_le_k);
s().assert_expr(fml);
sc.push_back(B);
am.push_back(c);
amk.push_back(k);
}
}
virtual void set_cancel(bool f) {
maxsmt_solver_base::set_cancel(f);
maxs->set_cancel(f);
}
virtual void collect_statistics(statistics& st) const {
maxsmt_solver_base::collect_statistics(st);
maxs->collect_statistics(st);
}
private:
lbool new_bound(expr_ref_vector const& al,
vector<rational> const& ws,
expr_ref_vector const& bs,
rational& k) {
pb_util u(m);
expr_ref_vector al2(m);
al2.append(al);
// w_j*b_j > k
al2.push_back(m.mk_not(u.mk_le(ws.size(), ws.c_ptr(), bs.c_ptr(), k)));
return bound(al2, ws, bs, k);
}
//
// minimal k, such that al & w_j*b_j >= k is sat
// minimal k, such that al & 3*x + 4*y >= k is sat
// minimal k, such that al & (or (not x) w3) & (or (not y) w4)
//
lbool bound(expr_ref_vector const& al,
vector<rational> const& ws,
expr_ref_vector const& bs,
rational& k) {
expr_ref_vector nbs(m);
opt_solver::scoped_push _sc(maxs->s());
for (unsigned i = 0; i < al.size(); ++i) {
maxs->add_hard(al[i]);
}
for (unsigned i = 0; i < bs.size(); ++i) {
nbs.push_back(mk_not(bs[i]));
}
TRACE("opt",
maxs->s().display(tout);
tout << "\n";
for (unsigned i = 0; i < bs.size(); ++i) {
tout << mk_pp(bs[i], m) << " " << ws[i] << "\n";
});
maxs->init_soft(ws, nbs);
lbool is_sat = maxs->s().check_sat(0,0);
if (is_sat == l_true) {
maxs->set_model();
is_sat = (*maxs)();
}
SASSERT(maxs->get_lower() > k);
k = maxs->get_lower();
return is_sat;
}
};
maxsmt_solver_base* opt::mk_wpm2(ast_manager& m, opt_solver* s, params_ref& p,
vector<rational> const& ws, expr_ref_vector const& soft) {
ref<opt_solver> s0 = alloc(opt_solver, m, p, symbol());
// initialize model.
s0->check_sat(0,0);
maxsmt_solver_base* s2 = mk_pbmax(m, s0.get(), p, ws, soft);
return alloc(wpm2, s, m, s2, p, ws, soft);
}
}

29
src/opt/wpm2.h
View file

@ -1,29 +0,0 @@
/*++
Copyright (c) 2014 Microsoft Corporation
Module Name:
wpm2.h
Abstract:
Wpm2 based MaxSAT.
Author:
Nikolaj Bjorner (nbjorner) 2014-4-17
Notes:
--*/
#ifndef _WPM2_H_
#define _WPM2_H_
#include "maxsmt.h"
namespace opt {
maxsmt_solver_base* mk_wpm2(ast_manager& m, opt_solver* s, params_ref& p,
vector<rational> const& ws, expr_ref_vector const& soft);
}
#endif

1
src/sat/sat_config.cpp
View file

@ -105,6 +105,7 @@ namespace sat {
}
m_minimize_lemmas = p.minimize_lemmas();
m_minimize_core = p.minimize_core();
m_optimize_model = p.optimize_model();
m_dyn_sub_res = p.dyn_sub_res();
}

1
src/sat/sat_config.h
View file

@ -69,6 +69,7 @@ namespace sat {
bool m_minimize_lemmas;
bool m_dyn_sub_res;
bool m_minimize_core;
bool m_optimize_model;
symbol m_always_true;

1
src/sat/sat_mus.cpp
View file

@ -41,6 +41,7 @@ namespace sat {
lbool mus::operator()() {
flet<bool> _disable_min(s.m_config.m_minimize_core, false);
flet<bool> _disable_opt(s.m_config.m_optimize_model, false);
TRACE("sat", tout << "old core: " << s.get_core() << "\n";);
IF_VERBOSE(2, verbose_stream() << "(sat.mus " << s.get_core() << ")\n";);
reset();

1
src/sat/sat_params.pyg
View file

@ -19,4 +19,5 @@ def_module_params('sat',
('minimize_lemmas', BOOL, True, 'minimize learned clauses'),
('dyn_sub_res', BOOL, True, 'dynamic subsumption resolution for minimizing learned clauses'),
('minimize_core', BOOL, False, 'minimize computed core'),
('optimize_model', BOOL, False, 'enable optimization of soft constraints'),
('dimacs.core', BOOL, False, 'extract core from DIMACS benchmarks')))

135
src/sat/sat_sls.cpp
View file

@ -50,8 +50,8 @@ namespace sat {
return m_elems[rnd(num_elems())];
}
sls::sls(solver& s): s(s) {
m_max_tries = 10000;
sls::sls(solver& s): s(s), m_cancel(false) {
m_max_tries = 1000000;
m_prob_choose_min_var = 43;
m_clause_generation = 0;
}
@ -180,6 +180,7 @@ namespace sat {
m_use_list[c[j].index()].push_back(i);
}
}
DEBUG_CODE(check_use_list(););
}
unsigned_vector const& sls::get_use(literal lit) {
@ -242,7 +243,7 @@ namespace sat {
}
void sls::flip(literal lit) {
// IF_VERBOSE(0, verbose_stream() << lit << " ";);
//IF_VERBOSE(0, verbose_stream() << lit << " ";);
SASSERT(value_at(lit, m_model) == l_false);
SASSERT(!m_tabu[lit.var()]);
m_model[lit.var()] = lit.sign()?l_false:l_true;
@ -266,9 +267,70 @@ namespace sat {
}
void sls::check_invariant() {
for (unsigned i = 0; i < m_clauses.size(); ++i) {
clause const& c = *m_clauses[i];
bool is_sat = c.satisfied_by(m_model);
SASSERT(is_sat != m_false.contains(i));
SASSERT(is_sat == m_num_true[i] > 0);
}
}
void sls::check_use_list() {
for (unsigned i = 0; i < m_clauses.size(); ++i) {
clause const& c = *m_clauses[i];
for (unsigned j = 0; j < c.size(); ++j) {
unsigned idx = c[j].index();
SASSERT(m_use_list[idx].contains(i));
}
}
for (unsigned i = 0; i < m_use_list.size(); ++i) {
literal lit = to_literal(i);
for (unsigned j = 0; j < m_use_list[i].size(); ++j) {
clause const& c = *m_clauses[m_use_list[i][j]];
bool found = false;
for (unsigned k = 0; !found && k < c.size(); ++k) {
found = c[k] == lit;
}
SASSERT(found);
}
}
}
void sls::display(std::ostream& out) const {
out << "Model\n";
for (bool_var v = 0; v < m_model.size(); ++v) {
out << v << ": " << m_model[v] << "\n";
}
out << "Clauses\n";
unsigned sz = m_false.num_elems();
for (unsigned i = 0; i < sz; ++i) {
out << *m_clauses[m_false[i]] << "\n";
}
for (unsigned i = 0; i < m_clauses.size(); ++i) {
if (m_false.contains(i)) continue;
clause const& c = *m_clauses[i];
out << c << " " << m_num_true[i] << "\n";
}
bool has_tabu = false;
for (unsigned i = 0; !has_tabu && i < m_tabu.size(); ++i) {
has_tabu = m_tabu[i];
}
if (has_tabu) {
out << "Tabu: ";
for (unsigned i = 0; i < m_tabu.size(); ++i) {
if (m_tabu[i]) {
literal lit(i, false);
if (value_at(lit, m_model) == l_false) lit.neg();
out << lit << " ";
}
}
out << "\n";
}
}
wsls::wsls(solver& s):
sls(s)
{
@ -277,7 +339,7 @@ namespace sat {
wsls::~wsls() {}
void wsls::set_soft(unsigned sz, double const* weights, literal const* lits) {
void wsls::set_soft(unsigned sz, literal const* lits, double const* weights) {
m_soft.reset();
m_weights.reset();
m_soft.append(sz, lits);
@ -291,14 +353,17 @@ namespace sat {
// Initialize m_clause_weights, m_hscore, m_sscore.
//
m_best_value = m_false.empty()?evaluate_model():-1.0;
m_best_model.reset();
m_clause_weights.reset();
m_hscore.reset();
m_sscore.reset();
m_H.reset();
m_S.reset();
m_best_model.append(s.get_model());
m_clause_weights.resize(m_clauses.size(), 1);
m_sscore.resize(s.num_vars(), 0.0);
m_hscore.resize(s.num_vars(), 0);
unsigned num_violated = 0;
for (unsigned i = 0; i < m_soft.size(); ++i) {
literal lit = m_soft[i];
m_sscore[lit.var()] = m_weights[i];
@ -310,16 +375,19 @@ namespace sat {
m_hscore[i] = compute_hscore(i);
refresh_scores(i);
}
DEBUG_CODE(check_invariant(););
unsigned i = 0;
for (; !m_cancel && i < m_max_tries; ++i) {
for (; !m_cancel && m_best_value > 0 && i < m_max_tries; ++i) {
wflip();
}
IF_VERBOSE(2, verbose_stream() << "tries " << i << "\n";);
TRACE("sat", display(tout););
IF_VERBOSE(0, verbose_stream() << "tries " << i << "\n";);
}
void wsls::wflip() {
literal lit;
if (pick_wflip(lit)) {
// IF_VERBOSE(0, verbose_stream() << lit << " ";);
wflip(lit);
}
}
@ -328,8 +396,10 @@ namespace sat {
if (m_false.empty()) {
double val = evaluate_model();
if (val < m_best_value || m_best_value < 0.0) {
m_best_value = val;
m_best_model.reset();
m_best_model.append(m_model);
IF_VERBOSE(0, verbose_stream() << "new value:" << val << "\n";);
}
}
unsigned idx;
@ -337,6 +407,8 @@ namespace sat {
idx = m_H.choose(m_rand);
lit = literal(idx, false);
if (value_at(lit, m_model) == l_true) lit.neg();
SASSERT(value_at(lit, m_model) == l_false);
TRACE("sat", tout << "flip H(" << m_H.num_elems() << ") " << lit << "\n";);
}
else if (!m_S.empty()) {
double score = 0.0;
@ -353,16 +425,38 @@ namespace sat {
m_min_vars.push_back(literal(v, false));
}
}
idx = m_min_vars[m_rand(m_min_vars.size())].var(); // pick with largest sscore.
lit = m_min_vars[m_rand(m_min_vars.size())]; // pick with largest sscore.
SASSERT(value_at(lit, m_model) == l_false);
TRACE("sat", tout << "flip S(" << m_min_vars.size() << "," << score << ") " << lit << "\n";);
}
else {
update_hard_weights();
if (!m_false.empty()) {
unsigned cls_idx = m_false.choose(m_rand);
clause const& c = *m_clauses[cls_idx];
lit = c[m_rand(c.size())];
TRACE("sat", tout << "flip hard(" << m_false.num_elems() << "," << c.size() << ") " << lit << "\n";);
}
else {
lit = m_soft[m_rand(m_soft.size())];
m_min_vars.reset();
for (unsigned i = 0; i < m_soft.size(); ++i) {
lit = m_soft[i];
if (value_at(lit, m_model) == l_false) {
m_min_vars.push_back(lit);
}
}
if (m_min_vars.empty()) {
SASSERT(m_best_value == 0.0);
UNREACHABLE(); // we should have exited the main loop before.
return false;
}
else {
lit = m_min_vars[m_rand(m_min_vars.size())];
}
TRACE("sat", tout << "flip soft(" << m_min_vars.size() << ") " << lit << "\n";);
}
SASSERT(value_at(lit, m_model) == l_false);
}
return !m_tabu[lit.var()];
}
@ -408,7 +502,6 @@ namespace sat {
}
}
}
DEBUG_CODE(check_invariant(););
}
@ -488,9 +581,29 @@ namespace sat {
// The score(v) is the reward on soft clauses for flipping v.
for (unsigned j = 0; j < m_soft.size(); ++j) {
unsigned v = m_soft[j].var();
double ss = value_at(m_soft[j], m_model)?(-m_weights[j]):m_weights[j];
double ss = (l_true == value_at(m_soft[j], m_model))?(-m_weights[j]):m_weights[j];
SASSERT(m_sscore[v] == ss);
}
// m_H are values such that m_hscore >= 0.
for (bool_var v = 0; v < m_hscore.size(); ++v) {
SASSERT(m_hscore[v] > 0 == m_H.contains(v));
}
// m_S are values such that hscore = 0, sscore > 0
for (bool_var v = 0; v < m_sscore.size(); ++v) {
SASSERT((m_hscore[v] == 0 && m_sscore[v] > 0) == m_S.contains(v));
}
}
void wsls::display(std::ostream& out) const {
sls::display(out);
out << "Best model\n";
for (bool_var v = 0; v < m_best_model.size(); ++v) {
out << v << ": " << m_best_model[v] << " h: " << m_hscore[v];
if (m_sscore[v] != 0.0) out << " s: " << m_sscore[v];
out << "\n";
}
}
};

7
src/sat/sat_sls.h
View file

@ -60,6 +60,8 @@ namespace sat {
virtual ~sls();
lbool operator()(unsigned sz, literal const* tabu, bool reuse_model);
void set_cancel(bool f) { m_cancel = f; }
void set_max_tries(unsigned mx) { m_max_tries = mx; }
virtual void display(std::ostream& out) const;
protected:
void init(unsigned sz, literal const* tabu, bool reuse_model);
void init_tabu(unsigned sz, literal const* tabu);
@ -69,6 +71,7 @@ namespace sat {
unsigned_vector const& get_use(literal lit);
void flip(literal lit);
virtual void check_invariant();
void check_use_list();
private:
bool pick_flip(literal& lit);
void flip();
@ -91,9 +94,11 @@ namespace sat {
public:
wsls(solver& s);
virtual ~wsls();
void set_soft(unsigned sz, double const* weights, literal const* lits);
void set_soft(unsigned sz, literal const* lits, double const* weights);
bool has_soft() const { return !m_soft.empty(); }
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;
private:
void wflip();
void wflip(literal lit);

11
src/sat/sat_solver.cpp
View file

@ -40,6 +40,7 @@ namespace sat {
m_asymm_branch(*this, p),
m_probing(*this, p),
m_mus(*this),
m_wsls(*this),
m_inconsistent(false),
m_num_frozen(0),
m_activity_inc(128),
@ -528,6 +529,10 @@ namespace sat {
return found_undef ? l_undef : l_false;
}
void solver::initialize_soft(unsigned sz, literal const* lits, double const* weights) {
m_wsls.set_soft(sz, lits, weights);
}
// -----------------------
//
// Propagation
@ -1003,6 +1008,11 @@ namespace sat {
m_model[v] = value(v);
}
TRACE("sat_mc_bug", m_mc.display(tout););
if (m_config.m_optimize_model) {
m_wsls.opt(0, 0, false);
m_model.reset();
m_model.append(m_wsls.get_model());
}
m_mc(m_model);
TRACE("sat", for (bool_var v = 0; v < num; v++) tout << v << ": " << m_model[v] << "\n";);
@ -2305,6 +2315,7 @@ namespace sat {
void solver::set_cancel(bool f) {
m_cancel = f;
m_wsls.set_cancel(f);
}
void solver::collect_statistics(statistics & st) const {

5
src/sat/sat_solver.h
View file

@ -33,6 +33,7 @@ Revision History:
#include"sat_iff3_finder.h"
#include"sat_probing.h"
#include"sat_mus.h"
#include"sat_sls.h"
#include"params.h"
#include"statistics.h"
#include"stopwatch.h"
@ -82,6 +83,7 @@ namespace sat {
asymm_branch m_asymm_branch;
probing m_probing;
mus m_mus;
wsls m_wsls;
bool m_inconsistent;
// A conflict is usually a single justification. That is, a justification
// for false. If m_not_l is not null_literal, then m_conflict is a
@ -224,13 +226,14 @@ namespace sat {
void assign_core(literal l, justification jst);
void set_conflict(justification c, literal not_l);
void set_conflict(justification c) { set_conflict(c, null_literal); }
lbool status(clause const & c) const;
lbool status(clause const & c) const;
clause_offset get_offset(clause const & c) const { return m_cls_allocator.get_offset(&c); }
void checkpoint() {
if (m_cancel) throw solver_exception(Z3_CANCELED_MSG);
if (memory::get_allocation_size() > m_config.m_max_memory) throw solver_exception(Z3_MAX_MEMORY_MSG);
}
typedef std::pair<literal, literal> bin_clause;
void initialize_soft(unsigned sz, literal const* lits, double const* weights);
protected:
watch_list & get_wlist(literal l) { return m_watches[l.index()]; }
watch_list const & get_wlist(literal l) const { return m_watches[l.index()]; }

13
src/sat/tactic/goal2sat.cpp
View file

@ -36,6 +36,7 @@ Notes:
#include"model_v2_pp.h"
#include"tactic.h"
#include"ast_pp.h"
#include<strstream>
struct goal2sat::imp {
struct frame {
@ -78,8 +79,9 @@ struct goal2sat::imp {
m_max_memory = megabytes_to_bytes(p.get_uint("max_memory", UINT_MAX));
}
void throw_op_not_handled() {
throw tactic_exception("operator not supported, apply simplifier before invoking translator");
void throw_op_not_handled(std::string const& s) {
std::string s0 = "operator " + s + " not supported, apply simplifier before invoking translator";
throw tactic_exception(s0.c_str());
}
void mk_clause(sat::literal l) {
@ -183,9 +185,12 @@ struct goal2sat::imp {
case OP_AND:
case OP_XOR:
case OP_IMPLIES:
case OP_DISTINCT:
case OP_DISTINCT: {
TRACE("goal2sat_not_handled", tout << mk_ismt2_pp(t, m) << "\n";);
throw_op_not_handled();
std::ostringstream strm;
strm << mk_ismt2_pp(t, m);
throw_op_not_handled(strm.str());
}
default:
convert_atom(t, root, sign);
return true;

4
src/smt/theory_wmaxsat.cpp
View file

@ -24,7 +24,7 @@ Notes:
namespace smt {
theory_wmaxsat::theory_wmaxsat(ast_manager& m, ref<filter_model_converter>& mc):
theory_wmaxsat::theory_wmaxsat(ast_manager& m, filter_model_converter& mc):
theory(m.mk_family_id("weighted_maxsat")),
m_mc(mc),
m_vars(m),
@ -91,7 +91,7 @@ bool_var theory_wmaxsat::assert_weighted(expr* fml, rational const& w) {
ast_manager& m = get_manager();
app_ref var(m), wfml(m);
var = m.mk_fresh_const("w", m.mk_bool_sort());
m_mc->insert(var->get_decl());
m_mc.insert(var->get_decl());
wfml = m.mk_or(var, fml);
ctx.assert_expr(wfml);
m_rweights.push_back(w);

4
src/smt/theory_wmaxsat.h
View file

@ -28,7 +28,7 @@ namespace smt {
void reset() { memset(this, 0, sizeof(*this)); }
stats() { reset(); }
};
ref<filter_model_converter> m_mc;
filter_model_converter& m_mc;
mutable unsynch_mpz_manager m_mpz;
app_ref_vector m_vars; // Auxiliary variables per soft clause
expr_ref_vector m_fmls; // Formulas per soft clause
@ -50,7 +50,7 @@ namespace smt {
svector<bool> m_assigned;
stats m_stats;
public:
theory_wmaxsat(ast_manager& m, ref<filter_model_converter>& mc);
theory_wmaxsat(ast_manager& m, filter_model_converter& mc);
virtual ~theory_wmaxsat();
void get_assignment(svector<bool>& result);
virtual void init_search_eh();