mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-07 18:05:21 +00:00
Code Activity

local change

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2014-01-27 11:18:48 -08:00
parent c6a9dae00a
commit fb86cf980b
3 changed files with 21 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/opt/opt_params.pyg
View file

@ -7,6 +7,7 @@ def_module_params('opt',
('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'),
('print_all_models', BOOL, False, 'display all intermediary models for satisfiable constraints'),
('debug_conflict', BOOL, False, 'debug conflict resolution'),
('wmaxsat_engine', SYMBOL, 'wmax', "weighted maxsat engine: 'wmax', 'iwmax' (iterative), 'bwmax' (bisection)"),
('elim_01', BOOL, True, 'eliminate 01 variables')

25
src/opt/weighted_maxsat.cpp
View file

@ -423,13 +423,14 @@ namespace opt {
rational m_lower;
model_ref m_model;
symbol m_engine;
bool m_print_all_models;
volatile bool m_cancel;
params_ref m_params;
opt_solver m_solver;
scoped_ptr<imp> m_imp;
imp(ast_manager& m, opt_solver& s, expr_ref_vector const& soft_constraints, vector<rational> const& weights):
m(m), s(s), m_soft(soft_constraints), m_weights(weights), m_cancel(false),
m(m), s(s), m_soft(soft_constraints), m_weights(weights), m_print_all_models(false), m_cancel(false),
m_solver(m, m_params, symbol("bound"))
{
m_assignment.resize(m_soft.size(), false);
@ -533,7 +534,8 @@ namespace opt {
}
if (is_sat == l_true) {
if (wth().is_optimal()) {
s.get_model(m_model);
m_upper = wth().get_min_cost();
updt_model(s);
}
expr_ref fml = wth().mk_block();
s.assert_expr(fml);
@ -776,8 +778,8 @@ namespace opt {
is_sat = l_undef;
}
if (is_sat == l_true) {
s.get_model(m_model);
m_upper = m_lower;
updt_model(s);
for (unsigned i = 0; i < block.size(); ++i) {
VERIFY(m_model->eval(block[i].get(), val));
m_assignment[i] = m.is_false(val);
@ -904,8 +906,8 @@ namespace opt {
return l_undef;
}
if (is_sat == l_true && wmax.is_zero()) {
s.get_model(m_model);
m_upper = m_lower;
updt_model(s);
for (unsigned i = 0; i < block.size(); ++i) {
VERIFY(m_model->eval(block[i].get(), val));
m_assignment[i] = m.is_false(val);
@ -1059,12 +1061,23 @@ namespace opt {
void updt_params(params_ref& p) {
opt_params _p(p);
m_engine = _p.wmaxsat_engine();
m_print_all_models = _p.print_all_models();
m_solver.updt_params(p);
if (m_imp) {
m_imp->updt_params(p);
}
}
void updt_model(solver& s) {
s.get_model(m_model);
if (m_print_all_models) {
std::cout << "[" << m_lower << ":" << m_upper << "]\n";
std::cout << "(model " << std::endl;
model_smt2_pp(std::cout, m, *(m_model.get()), 2);
std::cout << ")" << std::endl;
}
}
lbool simplify_and_check_sat(unsigned n, expr* const* assumptions) {
lbool is_sat = l_true;
tactic_ref tac1 = mk_simplify_tactic(m);
@ -1097,7 +1110,7 @@ namespace opt {
}
is_sat = m_solver.check_sat_core(0, 0);
if (l_true == is_sat && !m_cancel) {
m_solver.get_model(m_model);
updt_model(m_solver);
if (mc && m_model) (*mc)(m_model, 0);
IF_VERBOSE(2,
g->display(verbose_stream() << "goal:\n");
@ -1178,7 +1191,7 @@ namespace opt {
switch(is_sat) {
case l_true: {
if (wth().is_optimal()) {
s.get_model(m_model);
updt_model(s);
}
expr_ref fml = wth().mk_block();
s.assert_expr(fml);

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

@ -127,7 +127,7 @@ public:
elim01_tactic(ast_manager & _m, params_ref const & p):
m(_m),
a(m),
m_max_hi_default(8),
m_max_hi_default(1),
m_max_hi(rational(m_max_hi_default)) {
}