mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-19 19:02:02 +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-28 08:35:02 -07:00
commit 9916439913
2 changed files with 26 additions and 20 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/interp/iz3hash.h
View file

@ -374,7 +374,7 @@ namespace hash_space {
void resize(size_t new_size) { void resize(size_t new_size) {
const size_t old_n = buckets.size(); const size_t old_n = buckets.size();
if (new_size <= old_n) return; if (new_size <= old_n) return;
const size_t n = next_prime(new_size); const size_t n = next_prime(static_cast<unsigned>(new_size));
if (n <= old_n) return; if (n <= old_n) return;
Table tmp(n, (Entry*)(0)); Table tmp(n, (Entry*)(0));
for (size_t i = 0; i < old_n; ++i) { for (size_t i = 0; i < old_n; ++i) {

30
src/opt/weighted_maxsat.cpp
View file

@ -59,6 +59,7 @@ namespace smt {
rational m_rmin_cost; // current maximal cost assignment. rational m_rmin_cost; // current maximal cost assignment.
scoped_mpz m_zcost; // current sum of asserted costs scoped_mpz m_zcost; // current sum of asserted costs
scoped_mpz m_zmin_cost; // current maximal cost assignment. scoped_mpz m_zmin_cost; // current maximal cost assignment.
bool m_found_optimal;
u_map<theory_var> m_bool2var; // bool_var -> theory_var u_map<theory_var> m_bool2var; // bool_var -> theory_var
svector<bool_var> m_var2bool; // theory_var -> bool_var svector<bool_var> m_var2bool; // theory_var -> bool_var
bool m_propagate; bool m_propagate;
@ -79,6 +80,7 @@ namespace smt {
m_old_values(m_mpz), m_old_values(m_mpz),
m_zcost(m_mpz), m_zcost(m_mpz),
m_zmin_cost(m_mpz), m_zmin_cost(m_mpz),
m_found_optimal(false),
m_propagate(false), m_propagate(false),
m_normalize(false) m_normalize(false)
{} {}
@ -93,6 +95,12 @@ namespace smt {
void get_assignment(svector<bool>& result) { void get_assignment(svector<bool>& result) {
result.reset(); result.reset();
if (!m_found_optimal) {
for (unsigned i = 0; i < m_vars.size(); ++i) {
result.push_back(false);
}
}
else {
std::sort(m_cost_save.begin(), m_cost_save.end()); std::sort(m_cost_save.begin(), m_cost_save.end());
for (unsigned i = 0, j = 0; i < m_vars.size(); ++i) { for (unsigned i = 0, j = 0; i < m_vars.size(); ++i) {
if (j < m_cost_save.size() && m_cost_save[j] == i) { if (j < m_cost_save.size() && m_cost_save[j] == i) {
@ -103,6 +111,7 @@ namespace smt {
result.push_back(true); result.push_back(true);
} }
} }
}
TRACE("opt", TRACE("opt",
tout << "cost save: "; tout << "cost save: ";
for (unsigned i = 0; i < m_cost_save.size(); ++i) { for (unsigned i = 0; i < m_cost_save.size(); ++i) {
@ -189,10 +198,6 @@ namespace smt {
return m_min_cost_atom; return m_min_cost_atom;
} }
bool found_solution() const {
return !m_cost_save.empty();
}
// scoped_mpz leaks. // scoped_mpz leaks.
class numeral_trail : public trail<context> { class numeral_trail : public trail<context> {
@ -273,6 +278,7 @@ namespace smt {
m_min_cost_atom = 0; m_min_cost_atom = 0;
m_min_cost_atoms.reset(); m_min_cost_atoms.reset();
m_propagate = false; m_propagate = false;
m_found_optimal = false;
m_assigned.reset(); m_assigned.reset();
} }
@ -303,7 +309,7 @@ namespace smt {
} }
bool is_optimal() const { bool is_optimal() const {
return m_mpz.lt(m_zcost, m_zmin_cost); return !m_found_optimal || m_zcost < m_zmin_cost;
} }
expr_ref mk_block() { expr_ref mk_block() {
@ -329,22 +335,22 @@ namespace smt {
rational rw = rational(q); rational rw = rational(q);
IF_VERBOSE(1, verbose_stream() << "(wmaxsat with upper bound: " << rw << ")\n";); IF_VERBOSE(1, verbose_stream() << "(wmaxsat with upper bound: " << rw << ")\n";);
m_zmin_cost = weight; m_zmin_cost = weight;
m_found_optimal = true;
m_cost_save.reset(); m_cost_save.reset();
m_cost_save.append(m_costs); m_cost_save.append(m_costs);
}
expr_ref result(m.mk_or(disj.size(), disj.c_ptr()), m);
TRACE("opt", TRACE("opt",
tout << result << "\n";
if (is_optimal()) {
tout << "costs: "; tout << "costs: ";
for (unsigned i = 0; i < m_costs.size(); ++i) { for (unsigned i = 0; i < m_costs.size(); ++i) {
tout << mk_pp(get_enode(m_costs[i])->get_owner(), get_manager()) << " "; tout << mk_pp(get_enode(m_costs[i])->get_owner(), get_manager()) << " ";
} }
tout << "\n"; tout << "\n";
get_context().display(tout); get_context().display(tout);
}); );
}
expr_ref result(m.mk_or(disj.size(), disj.c_ptr()), m);
TRACE("opt",
tout << result << " weight: " << weight << "\n";
tout << "cost: " << m_zcost << " min-cost: " << m_zmin_cost << "\n";);
return result; return result;
} }