mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-03 21:09:11 +00:00
Code Activity

working on pb sls

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2014-03-18 20:04:00 -07:00
parent 94b3a46811
commit ce2338d4fb
1 changed files with 49 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

50
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"
@ -75,6 +93,7 @@ namespace smt {
clause cls(mgr);
if (compile_clause(f, cls)) {
m_clauses.push_back(cls);
m_weights.push_back(w);
}
}
@ -112,6 +131,7 @@ namespace smt {
void collect_statistics(statistics& st) const {
}
void get_model(model_ref& mdl) {
NOT_IMPLEMENTED_YET();
}
void updt_params(params_ref& p) {
}
@ -193,9 +213,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());