mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-19 20:33:38 +00:00
Code Activity

rename hsmax

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2014-07-26 12:45:21 -07:00
parent 9f1b2ccfc4
commit ff64adf292
3 changed files with 22 additions and 22 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/opt/maxsmt.cpp
View file

@ -182,8 +182,8 @@ namespace opt {
else if (m_maxsat_engine == symbol("bcd2")) { else if (m_maxsat_engine == symbol("bcd2")) {
m_msolver = mk_bcd2(m, s, m_params, m_weights, m_soft_constraints); m_msolver = mk_bcd2(m, s, m_params, m_weights, m_soft_constraints);
} }
else if (m_maxsat_engine == symbol("hsmax")) { else if (m_maxsat_engine == symbol("maxhs")) {
m_msolver = mk_hsmax(m, s, m_params, m_weights, m_soft_constraints); m_msolver = mk_maxhs(m, s, m_params, m_weights, m_soft_constraints);
} }
else if (m_maxsat_engine == symbol("sls")) { else if (m_maxsat_engine == symbol("sls")) {
// NB: this is experimental one-round version of SLS // NB: this is experimental one-round version of SLS

38
src/opt/weighted_maxsat.cpp
View file

@ -434,7 +434,7 @@ namespace opt {
// to the underlying optimization solver for the soft constraints. // to the underlying optimization solver for the soft constraints.
// //
class hsmax : public maxsmt_solver_base { class maxhs : public maxsmt_solver_base {
struct stats { struct stats {
stats() { reset(); } stats() { reset(); }
void reset() { memset(this, 0, sizeof(*this)); } void reset() { memset(this, 0, sizeof(*this)); }
@ -463,14 +463,14 @@ namespace opt {
public: public:
hsmax(opt_solver* s, ast_manager& m, params_ref& p, vector<rational> const& ws, expr_ref_vector const& soft): 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), maxsmt_solver_base(s, m, p, ws, soft),
m_aux(m), m_aux(m),
pb(m), pb(m),
a(m), a(m),
m_at_lower_bound(false) { m_at_lower_bound(false) {
} }
virtual ~hsmax() {} virtual ~maxhs() {}
virtual void set_cancel(bool f) { virtual void set_cancel(bool f) {
maxsmt_solver_base::set_cancel(f); maxsmt_solver_base::set_cancel(f);
@ -480,15 +480,15 @@ namespace opt {
virtual void collect_statistics(statistics& st) const { virtual void collect_statistics(statistics& st) const {
maxsmt_solver_base::collect_statistics(st); maxsmt_solver_base::collect_statistics(st);
m_hs.collect_statistics(st); m_hs.collect_statistics(st);
st.update("hsmax-num-iterations", m_stats.m_num_iterations); st.update("maxhs-num-iterations", m_stats.m_num_iterations);
st.update("hsmax-num-core-reductions-n", m_stats.m_num_core_reductions_failure); st.update("maxhs-num-core-reductions-n", m_stats.m_num_core_reductions_failure);
st.update("hsmax-num-core-reductions-y", m_stats.m_num_core_reductions_success); st.update("maxhs-num-core-reductions-y", m_stats.m_num_core_reductions_success);
st.update("hsmax-num-model-expansions-n", m_stats.m_num_model_expansions_failure); st.update("maxhs-num-model-expansions-n", m_stats.m_num_model_expansions_failure);
st.update("hsmax-num-model-expansions-y", m_stats.m_num_model_expansions_success); st.update("maxhs-num-model-expansions-y", m_stats.m_num_model_expansions_success);
st.update("hsmax-core-reduction-time", m_stats.m_core_reduction_time); st.update("maxhs-core-reduction-time", m_stats.m_core_reduction_time);
st.update("hsmax-model-expansion-time", m_stats.m_model_expansion_time); st.update("maxhs-model-expansion-time", m_stats.m_model_expansion_time);
st.update("hsmax-aux-sat-time", m_stats.m_aux_sat_time); st.update("maxhs-aux-sat-time", m_stats.m_aux_sat_time);
st.update("hsmax-disj-core-time", m_stats.m_disjoint_cores_time); st.update("maxhs-disj-core-time", m_stats.m_disjoint_cores_time);
} }
lbool operator()() { lbool operator()() {
@ -502,8 +502,8 @@ namespace opt {
while (m_lower < m_upper) { while (m_lower < m_upper) {
++m_stats.m_num_iterations; ++m_stats.m_num_iterations;
IF_VERBOSE(1, verbose_stream() << IF_VERBOSE(1, verbose_stream() <<
"(hsmax [" << m_lower << ":" << m_upper << "])\n";); "(maxhs [" << m_lower << ":" << m_upper << "])\n";);
TRACE("opt", tout << "(hsmax [" << m_lower << ":" << m_upper << "])\n";); TRACE("opt", tout << "(maxhs [" << m_lower << ":" << m_upper << "])\n";);
if (m_cancel) { if (m_cancel) {
return l_undef; return l_undef;
} }
@ -681,8 +681,8 @@ namespace opt {
} }
struct lt_activity { struct lt_activity {
hsmax& hs; maxhs& hs;
lt_activity(hsmax& hs):hs(hs) {} lt_activity(maxhs& hs):hs(hs) {}
bool operator()(expr* a, expr* b) const { bool operator()(expr* a, expr* b) const {
unsigned w1 = hs.m_core_activity[hs.m_aux2index.find(a)]; unsigned w1 = hs.m_core_activity[hs.m_aux2index.find(a)];
unsigned w2 = hs.m_core_activity[hs.m_aux2index.find(b)]; unsigned w2 = hs.m_core_activity[hs.m_aux2index.find(b)];
@ -1358,13 +1358,13 @@ namespace opt {
vector<rational> const& ws, expr_ref_vector const& soft) { vector<rational> const& ws, expr_ref_vector const& soft) {
return alloc(pbmax, s, m, p, ws, soft); return alloc(pbmax, s, m, p, ws, soft);
} }
maxsmt_solver_base* opt::mk_hsmax(ast_manager& m, opt_solver* s, params_ref& p, maxsmt_solver_base* opt::mk_maxhs(ast_manager& m, opt_solver* s, params_ref& p,
vector<rational> const& ws, expr_ref_vector const& soft) { vector<rational> const& ws, expr_ref_vector const& soft) {
return alloc(hsmax, s, m, p, ws, soft); return alloc(maxhs, s, m, p, ws, soft);
} }
maxsmt_solver_base* opt::mk_sls(ast_manager& m, opt_solver* s, params_ref& p, maxsmt_solver_base* opt::mk_sls(ast_manager& m, opt_solver* s, params_ref& p,
vector<rational> const& ws, expr_ref_vector const& soft) { vector<rational> const& ws, expr_ref_vector const& soft) {
return alloc(hsmax, s, m, p, ws, soft); return alloc(maxhs, s, m, p, ws, soft);
} }
maxsmt_solver_base* opt::mk_wmax(ast_manager& m, opt_solver* s, params_ref& p, maxsmt_solver_base* opt::mk_wmax(ast_manager& m, opt_solver* s, params_ref& p,
vector<rational> const& ws, expr_ref_vector const& soft) { vector<rational> const& ws, expr_ref_vector const& soft) {

2
src/opt/weighted_maxsat.h
View file

@ -31,7 +31,7 @@ namespace opt {
maxsmt_solver_base* mk_bcd2(ast_manager& m, opt_solver* s, params_ref& p, maxsmt_solver_base* mk_bcd2(ast_manager& m, opt_solver* s, params_ref& p,
vector<rational> const& ws, expr_ref_vector const& soft); vector<rational> const& ws, expr_ref_vector const& soft);
maxsmt_solver_base* mk_hsmax(ast_manager& m, opt_solver* s, params_ref& p, maxsmt_solver_base* mk_maxhs(ast_manager& m, opt_solver* s, params_ref& p,
vector<rational> const& ws, expr_ref_vector const& soft); vector<rational> const& ws, expr_ref_vector const& soft);
maxsmt_solver_base* mk_pbmax(ast_manager& m, opt_solver* s, params_ref& p, maxsmt_solver_base* mk_pbmax(ast_manager& m, opt_solver* s, params_ref& p,