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

tidy

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2014-04-14 21:18:18 -07:00
parent ac31e3856e
commit 91dc527635
1 changed files with 19 additions and 35 deletions
Download patch file Download diff file Expand all files Collapse all files

52
src/opt/weighted_maxsat.cpp
View file

@ -89,8 +89,14 @@ namespace opt {
m_weights.append(weights); m_weights.append(weights);
m_assignment.reset(); m_assignment.reset();
m_assignment.resize(m_soft.size(), false); m_assignment.resize(m_soft.size(), false);
init();
}
void init() {
m_lower.reset(); m_lower.reset();
m_upper.reset(); m_upper.reset();
for (unsigned i = 0; i < m_weights.size(); ++i) {
m_upper += m_weights[i];
}
} }
expr* mk_not(expr* e) { expr* mk_not(expr* e) {
if (m.is_not(e, e)) { if (m.is_not(e, e)) {
@ -127,15 +133,12 @@ namespace opt {
obj_map<expr, unsigned> ans2core; // answer literal to core index obj_map<expr, unsigned> ans2core; // answer literal to core index
lbool is_sat = l_undef; lbool is_sat = l_undef;
expr_ref_vector rs(m), asms(m); expr_ref_vector rs(m), asms(m);
m_lower = m_upper = rational::zero(); // current upper and lower bounds
vector<rational> sigmas; // sigma_j := w_j if soft clause has not been satisfied vector<rational> sigmas; // sigma_j := w_j if soft clause has not been satisfied
bool first = true; bool first = true;
init();
for (unsigned i = 0; i < m_soft.size(); ++i) { for (unsigned i = 0; i < m_soft.size(); ++i) {
m_upper += m_weights[i];
r = m.mk_fresh_const("r", m.mk_bool_sort()); r = m.mk_fresh_const("r", m.mk_bool_sort());
if (m_mc) {
m_mc->insert(r->get_decl()); m_mc->insert(r->get_decl());
}
fml = m.mk_or(m_soft[i].get(), r); fml = m.mk_or(m_soft[i].get(), r);
s().assert_expr(fml); // does not get asserted in model-based mode. s().assert_expr(fml); // does not get asserted in model-based mode.
rs.push_back(r); rs.push_back(r);
@ -307,9 +310,8 @@ namespace opt {
pb_util u(m); pb_util u(m);
expr_ref fml(m), val(m); expr_ref fml(m), val(m);
expr_ref_vector nsoft(m); expr_ref_vector nsoft(m);
m_lower = m_upper = rational::zero(); init();
for (unsigned i = 0; i < m_soft.size(); ++i) { for (unsigned i = 0; i < m_soft.size(); ++i) {
m_upper += m_weights[i];
nsoft.push_back(mk_not(m_soft[i].get())); nsoft.push_back(mk_not(m_soft[i].get()));
} }
solver::scoped_push _s1(s()); solver::scoped_push _s1(s());
@ -320,7 +322,7 @@ namespace opt {
TRACE("opt", s().display(tout<<"looping\n");); TRACE("opt", s().display(tout<<"looping\n"););
solver::scoped_push _s2(s()); solver::scoped_push _s2(s());
s().assert_expr(fml); s().assert_expr(fml);
is_sat = simplify_and_check_sat(0,0); is_sat = simplify_and_check_sat();
if (m_cancel) { if (m_cancel) {
is_sat = l_undef; is_sat = l_undef;
} }
@ -349,11 +351,10 @@ namespace opt {
} }
private: private:
lbool simplify_and_check_sat(unsigned n, expr* const* assumptions) { lbool simplify_and_check_sat() {
lbool is_sat = l_true; lbool is_sat = l_true;
tactic_ref tac1 = mk_simplify_tactic(m); tactic_ref tac = mk_simplify_tactic(m);
// tactic_ref tac2 = mk_pb_preprocess_tactic(m); // TBD: make tac attribute for cancelation.
tactic_ref tac = tac1; // and_then(tac1.get(), tac2.get()); // TBD: make attribute for cancelation.
proof_converter_ref pc; proof_converter_ref pc;
expr_dependency_ref core(m); expr_dependency_ref core(m);
model_converter_ref mc; model_converter_ref mc;
@ -362,10 +363,6 @@ namespace opt {
for (unsigned i = 0; i < s().get_num_assertions(); ++i) { for (unsigned i = 0; i < s().get_num_assertions(); ++i) {
g->assert_expr(s().get_assertion(i)); g->assert_expr(s().get_assertion(i));
} }
for (unsigned i = 0; i < n; ++i) {
NOT_IMPLEMENTED_YET();
// add assumption in a wrapper.
}
(*tac)(g, result, mc, pc, core); (*tac)(g, result, mc, pc, core);
if (result.empty()) { if (result.empty()) {
is_sat = l_false; is_sat = l_false;
@ -374,9 +371,7 @@ namespace opt {
SASSERT(result.size() == 1); SASSERT(result.size() == 1);
goal_ref r = result[0]; goal_ref r = result[0];
solver::scoped_push _s(s()); solver::scoped_push _s(s());
// TBD ptr_vector<expr> asms;
for (unsigned i = 0; i < r->size(); ++i) { for (unsigned i = 0; i < r->size(); ++i) {
// TBD collect assumptions from r
s().assert_expr(r->form(i)); s().assert_expr(r->form(i));
} }
is_sat = s().check_sat(0, 0); is_sat = s().check_sat(0, 0);
@ -410,14 +405,12 @@ namespace opt {
app_ref fml(m), a(m), b(m), c(m); app_ref fml(m), a(m), b(m), c(m);
expr_ref val(m); expr_ref val(m);
expr_ref_vector block(m), ans(m), al(m), am(m); expr_ref_vector block(m), ans(m), al(m), am(m);
m_lower = m_upper = rational::zero();
obj_map<expr, unsigned> ans_index; obj_map<expr, unsigned> ans_index;
vector<rational> amk; vector<rational> amk;
vector<uint_set> sc; vector<uint_set> sc;
init();
for (unsigned i = 0; i < m_soft.size(); ++i) { for (unsigned i = 0; i < m_soft.size(); ++i) {
rational w = m_weights[i]; rational w = m_weights[i];
m_upper += w;
b = m.mk_fresh_const("b", m.mk_bool_sort()); b = m.mk_fresh_const("b", m.mk_bool_sort());
m_mc->insert(b->get_decl()); m_mc->insert(b->get_decl());
@ -607,10 +600,9 @@ namespace opt {
expr_ref fml(m), val(m); expr_ref fml(m), val(m);
app_ref b(m); app_ref b(m);
expr_ref_vector nsoft(m); expr_ref_vector nsoft(m);
m_lower = m_upper = rational::zero(); init();
solver::scoped_push __s(s()); solver::scoped_push __s(s());
for (unsigned i = 0; i < m_soft.size(); ++i) { for (unsigned i = 0; i < m_soft.size(); ++i) {
m_upper += m_weights[i];
b = m.mk_fresh_const("b", m.mk_bool_sort()); b = m.mk_fresh_const("b", m.mk_bool_sort());
m_mc->insert(b->get_decl()); m_mc->insert(b->get_decl());
fml = m.mk_or(m_soft[i].get(), b); fml = m.mk_or(m_soft[i].get(), b);
@ -696,11 +688,7 @@ namespace opt {
m_bvsls.assert_expr(r->form(i)); m_bvsls.assert_expr(r->form(i));
} }
m_lower = m_upper = rational::zero(); init();
for (unsigned i = 0; i < m_soft.size(); ++i) {
m_upper += m_weights[i];
}
rational num = numerator(m_upper); rational num = numerator(m_upper);
rational den = denominator(m_upper); rational den = denominator(m_upper);
rational maxval = num*den; rational maxval = num*den;
@ -959,9 +947,8 @@ namespace opt {
expr_ref fml(m), val(m); expr_ref fml(m), val(m);
app_ref b(m); app_ref b(m);
expr_ref_vector nsoft(m); expr_ref_vector nsoft(m);
m_lower = m_upper = rational::zero(); init();
for (unsigned i = 0; i < m_soft.size(); ++i) { for (unsigned i = 0; i < m_soft.size(); ++i) {
m_upper += m_weights[i];
b = m.mk_fresh_const("b", m.mk_bool_sort()); b = m.mk_fresh_const("b", m.mk_bool_sort());
m_mc->insert(b->get_decl()); m_mc->insert(b->get_decl());
fml = m.mk_or(m_soft[i].get(), b); fml = m.mk_or(m_soft[i].get(), b);
@ -1011,10 +998,9 @@ namespace opt {
expr_ref fml(m), val(m); expr_ref fml(m), val(m);
app_ref b(m); app_ref b(m);
expr_ref_vector nsoft(m); expr_ref_vector nsoft(m);
m_lower = m_upper = rational::zero();
solver::scoped_push __s(s()); solver::scoped_push __s(s());
init();
for (unsigned i = 0; i < m_soft.size(); ++i) { for (unsigned i = 0; i < m_soft.size(); ++i) {
m_upper += m_weights[i];
b = m.mk_fresh_const("b", m.mk_bool_sort()); b = m.mk_fresh_const("b", m.mk_bool_sort());
m_mc->insert(b->get_decl()); m_mc->insert(b->get_decl());
fml = m.mk_or(m_soft[i].get(), b); fml = m.mk_or(m_soft[i].get(), b);
@ -1189,16 +1175,14 @@ namespace opt {
app_ref fml(m), a(m), b(m), c(m); app_ref fml(m), a(m), b(m), c(m);
expr_ref val(m); expr_ref val(m);
expr_ref_vector block(m), ans(m), am(m), soft(m); expr_ref_vector block(m), ans(m), am(m), soft(m);
m_lower = m_upper = rational::zero();
obj_map<expr, unsigned> ans_index; obj_map<expr, unsigned> ans_index;
vector<rational> amk; vector<rational> amk;
vector<uint_set> sc; // vector of indices used in at last constraints vector<uint_set> sc; // vector of indices used in at last constraints
expr_ref_vector al(m); // vector of at least constraints. expr_ref_vector al(m); // vector of at least constraints.
rational wmax; rational wmax;
init();
for (unsigned i = 0; i < m_soft.size(); ++i) { for (unsigned i = 0; i < m_soft.size(); ++i) {
rational w = m_weights[i]; rational w = m_weights[i];
m_upper += w;
if (wmax < w) wmax = w; if (wmax < w) wmax = w;
b = m.mk_fresh_const("b", m.mk_bool_sort()); b = m.mk_fresh_const("b", m.mk_bool_sort());
block.push_back(b); block.push_back(b);