mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

fix bug exposed by example by Robert White

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2014-03-28 08:34:31 -07:00
parent 2103bc3831
commit ac7fffa9cb
3 changed files with 28 additions and 22 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/duality/duality.h
View file

@ -29,7 +29,7 @@ using namespace stl_ext;
namespace Duality {
class implicant_solver;
struct implicant_solver;
/* Generic operations on Z3 formulas */

4
src/interp/iz3hash.h
View file

@ -52,7 +52,7 @@ namespace hash_space {
class hash<std::string> {
public:
size_t operator()(const std::string &s) const {
return string_hash(s.c_str(), s.size(), 0);
return string_hash(s.c_str(), static_cast<unsigned>(s.size()), 0);
}
};
@ -374,7 +374,7 @@ namespace hash_space {
void resize(size_t new_size) {
const size_t old_n = buckets.size();
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;
Table tmp(n, (Entry*)(0));
for (size_t i = 0; i < old_n; ++i) {

44
src/opt/weighted_maxsat.cpp
View file

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