mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 21:38:44 +00:00
Code Activity

Merge branch 'opt' of https://git01.codeplex.com/z3 into opt

Browse source
This commit is contained in:
Nikolaj Bjorner 2014-03-18 20:04:33 -07:00
parent e11e1231dc ce2338d4fb
commit 7b0ffc9108
1 changed files with 48 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

49
src/opt/pb_sls.cpp
View file

@ -1,3 +1,21 @@
/*++
Copyright (c) 2014 Microsoft Corporation
Module Name:
pb_sls.cpp
Abstract:
SLS for PB optimization.
Author:
Nikolaj Bjorner (nbjorner) 2014-03-18
Notes:
--*/
#include "pb_sls.h"
#include "smt_literal.h"
#include "ast_pp.h"
@ -105,6 +123,7 @@ namespace smt {
void collect_statistics(statistics& st) const {
}
void get_model(model_ref& mdl) {
NOT_IMPLEMENTED_YET();
}
void updt_params(params_ref& p) {
}
@ -186,9 +205,37 @@ namespace smt {
}
void flip_soft() {
NOT_IMPLEMENTED_YET();
clause const& cls = pick_soft_clause();
int break_count;
int min_bc = INT_MAX;
unsigned min_bc_index = 0;
rational penalty = m_penalty;
rational min_penalty = penalty;
for (unsigned i = 0; i < cls.m_lits.size(); ++i) {
literal lit = cls.m_lits[i];
break_count = flip(lit);
SASSERT(break_count >= 0);
if (break_count == 0 && penalty > m_penalty) {
// TODO: save into best so far if this qualifies.
return;
}
if ((break_count < min_bc) ||
(break_count == min_bc && m_penalty < min_penalty)) {
min_bc = break_count;
min_bc_index = i;
min_penality = m_penalty;
}
VERIFY(-break_count == flip(~lit));
}
// just do a greedy move:
flip(cls.m_lits[min_bc_index]);
}
//
// TODO: alternate version: loop over soft clauses and see if there is a flip that
// reduces the penalty while preserving the hard constraints.
//
// crude selection strategy.
clause const& pick_hard_clause() {
SASSERT(!m_hard_false.empty());