mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 17:44:08 +00:00
Code Activity

remove stale SLS option

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2016-07-21 18:18:42 -07:00
parent 1073e161c7
commit 3581f6de42
8 changed files with 10 additions and 117 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
contrib/cmake/src/opt/CMakeLists.txt
View file

@ -1,7 +1,6 @@
z3_add_component(opt
SOURCES
maxres.cpp
maxsls.cpp
maxsmt.cpp
mss.cpp
opt_cmds.cpp

73
src/opt/maxsls.cpp
View file

@ -1,73 +0,0 @@
/*++
Copyright (c) 2013 Microsoft Corporation
Module Name:
maxsls.cpp
Abstract:
Weighted SLS MAXSAT module
Author:
Nikolaj Bjorner (nbjorner) 2014-4-17
Notes:
--*/
#include "maxsls.h"
#include "ast_pp.h"
#include "model_smt2_pp.h"
#include "opt_context.h"
#include "inc_sat_solver.h"
namespace opt {
class sls : public maxsmt_solver_base {
public:
sls(maxsat_context& c, weights_t& ws, expr_ref_vector const& soft):
maxsmt_solver_base(c, ws, soft) {
}
virtual ~sls() {}
lbool operator()() {
IF_VERBOSE(1, verbose_stream() << "(opt.sls)\n";);
init();
enable_sls(true);
lbool is_sat = check();
if (is_sat == l_true) {
s().get_model(m_model);
m_upper.reset();
for (unsigned i = 0; i < m_soft.size(); ++i) {
expr_ref tmp(m);
m_model->eval(m_soft[i], tmp, true);
m_assignment[i] = m.is_true(tmp);
if (!m_assignment[i]) {
m_upper += m_weights[i];
}
}
}
return is_sat;
}
lbool check() {
if (m_c.sat_enabled()) {
return inc_sat_check_sat(
s(), m_soft.size(), m_soft.c_ptr(), m_weights.c_ptr(), m_upper);
}
else {
return s().check_sat(0, 0);
}
}
};
maxsmt_solver_base* mk_sls(
maxsat_context& c, weights_t& ws, expr_ref_vector const& soft) {
return alloc(sls, c, ws, soft);
}
};

35
src/opt/maxsls.h
View file

@ -1,35 +0,0 @@
/*++
Copyright (c) 2013 Microsoft Corporation
Module Name:
maxsls.h
Abstract:
Weighted SLS MAXSAT module
Author:
Nikolaj Bjorner (nbjorner) 2014-4-17
Notes:
Partial, one-round SLS optimizer. Finds the first
local maximum given a resource bound and returns.
--*/
#ifndef OPT_SLS_MAX_SAT_H_
#define OPT_SLS_MAX_SAT_H_
#include "maxsmt.h"
namespace opt {
maxsmt_solver_base* mk_sls(maxsat_context& c, weights_t& ws, expr_ref_vector const& soft);
};
#endif

6
src/opt/maxsmt.cpp
View file

@ -21,7 +21,6 @@ Notes:
#include "maxsmt.h"
#include "maxres.h"
#include "wmax.h"
#include "maxsls.h"
#include "ast_pp.h"
#include "uint_set.h"
#include "opt_context.h"
@ -163,15 +162,12 @@ namespace opt {
else if (maxsat_engine == symbol("pd-maxres")) {
m_msolver = mk_primal_dual_maxres(m_c, m_index, m_weights, m_soft_constraints);
}
else if (maxsat_engine == symbol("sls")) {
// NB: this is experimental one-round version of SLS
m_msolver = mk_sls(m_c, m_weights, m_soft_constraints);
}
else {
if (maxsat_engine != symbol::null && maxsat_engine != symbol("wmax")) {
warning_msg("solver %s is not recognized, using default 'wmax'",
maxsat_engine.str().c_str());
}
std::cout << "wmax\n";
m_msolver = mk_wmax(m_c, m_weights, m_soft_constraints);
}

2
src/opt/opt_context.cpp
View file

@ -561,7 +561,7 @@ namespace opt {
if (opt_params(m_params).priority() == symbol("pareto")) {
return;
}
m_params.set_bool("minimize_core_partial", true); // false);
m_params.set_bool("minimize_core_partial", true);
m_params.set_bool("minimize_core", true);
m_sat_solver = mk_inc_sat_solver(m, m_params);
expr_ref_vector fmls(m);

2
src/opt/opt_params.pyg
View file

@ -2,7 +2,7 @@ def_module_params('opt',
description='optimization parameters',
export=True,
params=(('optsmt_engine', SYMBOL, 'basic', "select optimization engine: 'basic', 'farkas', 'symba'"),
('maxsat_engine', SYMBOL, 'maxres', "select engine for maxsat: 'core_maxsat', 'wmax', 'maxres', 'pd-maxres', 'sls'"),
('maxsat_engine', SYMBOL, 'maxres', "select engine for maxsat: 'core_maxsat', 'wmax', 'maxres', 'pd-maxres'"),
('priority', SYMBOL, 'lex', "select how to priortize objectives: 'lex' (lexicographic), 'pareto', or 'box'"),
('dump_benchmarks', BOOL, False, 'dump benchmarks for profiling'),
('print_model', BOOL, False, 'display model for satisfiable constraints'),

5
src/opt/opt_sls_solver.h
View file

@ -184,9 +184,10 @@ namespace opt {
expr_ref tmp(m);
goal_ref g(alloc(goal, m, true, false));
for (unsigned i = 0; i < m_solver->get_num_assertions(); ++i) {
m_pb2bv(m_solver->get_assertion(i), tmp);
m_pb2bv(m_solver->get_assertion(i), tmp);
g->assert_expr(tmp);
}
TRACE("opt", g->display(tout););
tactic_ref simplify = mk_nnf_tactic(m);
proof_converter_ref pc;
expr_dependency_ref core(m);
@ -198,6 +199,7 @@ namespace opt {
for (unsigned i = 0; i < r->size(); ++i) {
m_bvsls->assert_expr(r->form(i));
}
TRACE("opt", m_bvsls->display(tout););
}
void pbsls_opt(model_ref& mdl) {
@ -230,6 +232,7 @@ namespace opt {
}
assertions2sls();
expr_ref objective = soft2bv(m_soft, m_weights);
TRACE("opt", tout << objective << "\n";);
opt_result res(m);
res.is_sat = l_undef;
try {

3
src/sat/sat_solver/inc_sat_solver.cpp
View file

@ -474,6 +474,9 @@ lbool inc_sat_check_sat(solver& _s, unsigned sz, expr*const* soft, rational cons
for (unsigned i = 0; _weights && i < sz; ++i) {
weights.push_back(_weights[i].get_double());
}
params_ref p;
p.set_bool("minimize_core", false);
s.updt_params(p);
return s.check_sat(sz, soft, weights.c_ptr(), max_weight.get_double());
}