mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-11 19:53:34 +00:00
Code Activity

Merge pull request #6072 from wintersteiger/cwinter_warnings

Browse source 
Fix a couple compiler warnings
This commit is contained in:
Christoph M. Wintersteiger 2022-06-04 11:40:14 +01:00 committed by GitHub
parent 4421f7d575 ed7db892f9
commit cb67f90f1a
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
2 changed files with 86 additions and 87 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
src/ast/ast_pp_util.h
View file

@ -30,15 +30,15 @@ class ast_pp_util {
stacked_value<unsigned> m_rec_decls;
stacked_value<unsigned> m_decls;
stacked_value<unsigned> m_sorts;
public:
public:
decl_collector coll;
ast_pp_util(ast_manager& m): m(m), m_env(m), coll(m), m_rec_decls(0), m_decls(0), m_sorts(0) {}
ast_pp_util(ast_manager& m): m(m), m_env(m), m_rec_decls(0), m_decls(0), m_sorts(0), coll(m) {}
void reset() { coll.reset(); m_removed.reset(); m_sorts.clear(0u); m_decls.clear(0u); m_rec_decls.clear(0u); }
void collect(expr* e);
@ -59,7 +59,7 @@ class ast_pp_util {
std::ostream& display_expr(std::ostream& out, expr* f, bool neat = true);
void push();
void pop(unsigned n);
smt2_pp_environment& env() { return m_env; }

163
src/opt/maxcore.cpp
View file

@ -6,7 +6,7 @@ Module Name:
maxcore.cpp
Abstract:
Core based (weighted) max-sat algorithms:
- mu: max-sat algorithm by Nina and Bacchus, AAAI 2014.
@ -26,20 +26,20 @@ Abstract:
the approach updates the upper bound if the current assignment
improves the current best assignmet.
Furthermore, take the soft constraints that are complements
to the current satisfying subset.
E.g, if F are the hard constraints and
s1,...,sn, t1,..., tm are the soft clauses and
F & s1 & ... & sn is satisfiable, then the complement
to the current satisfying subset.
E.g, if F are the hard constraints and
s1,...,sn, t1,..., tm are the soft clauses and
F & s1 & ... & sn is satisfiable, then the complement
of of the current satisfying subset is t1, .., tm.
Update the hard constraint:
F := F & (t1 or ... or tm)
Replace t1, .., tm by m-1 new soft clauses:
t1 & t2, t3 & (t1 or t2), t4 & (t1 or t2 or t3), ..., tn & (t1 or ... t_{n-1})
Claim:
If k of these soft clauses are satisfied, then k+1 of
Claim:
If k of these soft clauses are satisfied, then k+1 of
the previous soft clauses are satisfied.
If k of these soft clauses are false in the satisfying assignment
for the updated F, then k of the original soft clauses are also false
If k of these soft clauses are false in the satisfying assignment
for the updated F, then k of the original soft clauses are also false
under the assignment.
In summary: any assignment to the new clauses that satsfies F has the
same cost.
@ -78,7 +78,7 @@ public:
s_primal,
s_primal_dual,
s_primal_binary,
s_rc2
s_rc2
};
private:
struct stats {
@ -103,14 +103,14 @@ private:
stats m_stats;
expr_ref_vector m_B;
expr_ref_vector m_asms;
expr_ref_vector m_asms;
expr_ref_vector m_defs;
obj_map<expr, rational> m_asm2weight;
expr_ref_vector m_new_core;
mus m_mus;
expr_ref_vector m_trail;
strategy_t m_st;
rational m_max_upper;
rational m_max_upper;
model_ref m_csmodel;
lns_maxcore m_lnsctx;
lns m_lns;
@ -160,16 +160,16 @@ public:
default:
UNREACHABLE();
break;
}
}
}
~maxcore() override {}
bool is_literal(expr* l) {
return
return
is_uninterp_const(l) ||
(m.is_not(l, l) && is_uninterp_const(l));
}
}
void add(expr_ref_vector const& es) {
for (expr* e : es) add(e);
@ -205,7 +205,7 @@ public:
IF_VERBOSE(13, verbose_stream() << "new assumption " << mk_pp(e, m) << " " << w << "\n";);
m_asm2weight.insert(e, w);
m_asms.push_back(e);
m_trail.push_back(e);
m_trail.push_back(e);
TRACE("opt", tout << "insert: " << mk_pp(e, m) << " : " << w << "\n";
tout << m_asms << " " << "\n"; );
}
@ -222,7 +222,7 @@ public:
improve_model();
if (is_sat != l_true) return is_sat;
while (m_lower < m_upper) {
TRACE("opt_verbose",
TRACE("opt_verbose",
s().display(tout << m_asms << "\n") << "\n";
display(tout););
is_sat = check_sat_hill_climb(m_asms);
@ -230,8 +230,8 @@ public:
return l_undef;
}
switch (is_sat) {
case l_true:
CTRACE("opt", m_model->is_false(m_asms),
case l_true:
CTRACE("opt", m_model->is_false(m_asms),
tout << *m_model << "assumptions: ";
for (expr* a : m_asms) tout << mk_pp(a, m) << " -> " << (*m_model)(a) << " ";
tout << "\n";);
@ -244,7 +244,7 @@ public:
m_lower = m_upper;
}
if (is_sat == l_undef) {
return is_sat;
return is_sat;
}
break;
case l_undef:
@ -270,7 +270,7 @@ public:
return l_undef;
}
switch (is_sat) {
case l_true:
case l_true:
get_current_correction_set(cs);
if (cs.empty()) {
m_found_feasible_optimum = m_model.get() != nullptr;
@ -286,7 +286,7 @@ public:
m_lower = m_upper;
}
if (is_sat == l_undef) {
return is_sat;
return is_sat;
}
break;
case l_undef:
@ -307,7 +307,7 @@ public:
/**
Give preference to cores that have large minimal values.
*/
sort_assumptions(asms);
sort_assumptions(asms);
unsigned last_index = 0;
unsigned index = 0;
SASSERT(index < asms.size() || asms.empty());
@ -318,16 +318,16 @@ public:
}
last_index = index;
is_sat = check_sat(index, asms.data());
}
}
}
else {
is_sat = check_sat(asms.size(), asms.data());
}
is_sat = check_sat(asms.size(), asms.data());
}
return is_sat;
}
lbool check_sat(unsigned sz, expr* const* asms) {
lbool r = s().check_sat(sz, asms);
lbool r = s().check_sat(sz, asms);
if (r == l_true) {
model_ref mdl;
s().get_model(mdl);
@ -399,7 +399,7 @@ public:
return l_true;
}
// 1. remove all core literals from m_asms
// 2. re-add literals of higher weight than min-weight.
// 3. 'core' stores the core literals that are
@ -407,19 +407,19 @@ public:
cores.push_back(weighted_core(core, core_weight(core)));
remove_soft(core, m_asms);
split_core(core);
split_core(core);
if (core.size() >= m_max_core_size)
break;
is_sat = check_sat_hill_climb(m_asms);
is_sat = check_sat_hill_climb(m_asms);
}
TRACE("opt",
TRACE("opt",
tout << "sat: " << is_sat << " num cores: " << cores.size() << "\n";
for (auto const& c : cores) display_vec(tout, c.m_core);
tout << "num assumptions: " << m_asms.size() << "\n";);
return is_sat;
}
@ -479,14 +479,14 @@ public:
TRACE("opt", display_vec(tout << "corr_set: ", corr_set););
remove_soft(corr_set, m_asms);
rational w = split_core(corr_set);
cs_max_resolve(corr_set, w);
cs_max_resolve(corr_set, w);
IF_VERBOSE(2, verbose_stream() << "(opt.maxres.correction-set " << corr_set.size() << ")\n";);
m_csmodel = nullptr;
m_correction_set_size = 0;
}
lbool process_unsat() {
if (m_enable_core_rotate)
if (m_enable_core_rotate)
return core_rotate();
vector<weighted_core> cores;
@ -518,28 +518,28 @@ public:
return l_true;
}
unsigned max_core_size(vector<exprs> const& cores) {
unsigned result = 0;
for (auto const& c : cores)
for (auto const& c : cores)
result = std::max(c.size(), result);
return result;
}
void process_unsat(vector<weighted_core> const& cores) {
for (auto const & c : cores)
for (auto const & c : cores)
process_unsat(c.m_core, c.m_weight);
improve_model(m_model);
}
void update_model(expr* def, expr* value) {
SASSERT(is_uninterp_const(def));
if (m_csmodel)
SASSERT(is_uninterp_const(def));
if (m_csmodel)
m_csmodel->register_decl(to_app(def)->get_decl(), (*m_csmodel)(value));
if (m_model)
m_model->register_decl(to_app(def)->get_decl(), (*m_model)(value));
}
void process_unsat(exprs const& core, rational w) {
IF_VERBOSE(3, verbose_stream() << "(maxres cs model valid: " << (m_csmodel.get() != nullptr) << " cs size:" << m_correction_set_size << " core: " << core.size() << ")\n";);
expr_ref fml(m);
@ -568,7 +568,7 @@ public:
m_lower = std::min(m_lower, m_upper);
}
if (m_csmodel.get() && m_correction_set_size > 0) {
// this estimate can overshoot for weighted soft constraints.
// this estimate can overshoot for weighted soft constraints.
--m_correction_set_size;
}
trace();
@ -578,7 +578,7 @@ public:
get_current_correction_set(m_csmodel.get(), cs);
m_correction_set_size = cs.size();
TRACE("opt", tout << "cs " << m_correction_set_size << " " << core.size() << "\n";);
if (m_correction_set_size >= core.size())
if (m_correction_set_size >= core.size())
return;
rational w(0);
for (expr* a : m_asms) {
@ -593,7 +593,7 @@ public:
bool get_mus_model(model_ref& mdl) {
rational w(0);
if (m_c.sat_enabled()) {
// SAT solver core extracts some model
// SAT solver core extracts some model
// during unsat core computation.
mdl = nullptr;
s().get_model(mdl);
@ -601,20 +601,20 @@ public:
else {
w = m_mus.get_best_model(mdl);
}
if (mdl.get() && w < m_upper)
if (mdl.get() && w < m_upper)
update_assignment(mdl);
return nullptr != mdl.get();
}
lbool minimize_core(expr_ref_vector& core) {
if (core.empty())
if (core.empty())
return l_true;
if (m_c.sat_enabled())
if (m_c.sat_enabled())
return l_true;
m_mus.reset();
m_mus.add_soft(core.size(), core.data());
lbool is_sat = m_mus.get_mus(m_new_core);
if (is_sat != l_true)
if (is_sat != l_true)
return is_sat;
core.reset();
core.append(m_new_core);
@ -629,7 +629,7 @@ public:
if (core.empty()) return rational(0);
// find the minimal weight:
rational w = get_weight(core[0]);
for (unsigned i = 1; i < core.size(); ++i)
for (unsigned i = 1; i < core.size(); ++i)
w = std::min(w, get_weight(core[i]));
return w;
}
@ -643,7 +643,7 @@ public:
rational w3 = w2 - w;
new_assumption(e, w3);
}
}
}
return w;
}
@ -663,7 +663,7 @@ public:
}
void display(std::ostream& out) {
for (expr * a : m_asms)
for (expr * a : m_asms)
out << mk_pp(a, m) << " : " << get_weight(a) << "\n";
}
@ -677,15 +677,15 @@ public:
//
// d_0 := true
// d_i := b_{i-1} and d_{i-1} for i = 1...sz-1
// soft (b_i or !d_i)
// soft (b_i or !d_i)
// == (b_i or !(!b_{i-1} or d_{i-1}))
// == (b_i or b_0 & b_1 & ... & b_{i-1})
//
//
// Soft constraint is satisfied if previous soft constraint
// holds or if it is the first soft constraint to fail.
//
//
// Soundness of this rule can be established using MaxRes
//
//
for (unsigned i = 1; i < core.size(); ++i) {
expr* b_i = core[i-1];
expr* b_i1 = core[i];
@ -761,7 +761,7 @@ public:
bound_info(expr_ref_vector const& es, unsigned k, rational const& weight):
es(es.size(), es.data()), k(k), weight(weight) {}
};
obj_map<expr, expr*> m_at_mostk;
obj_map<expr, bound_info> m_bounds;
rational m_unfold_upper;
@ -770,7 +770,7 @@ public:
pb_util pb(m);
expr_ref am(pb.mk_at_most_k(es, bound), m);
expr* r = nullptr;
if (m_at_mostk.find(am, r))
if (m_at_mostk.find(am, r))
return r;
r = mk_fresh_bool("r");
m_trail.push_back(am);
@ -806,7 +806,7 @@ public:
new_assumption(am, weight);
}
}
// cs is a correction set (a complement of a (maximal) satisfying assignment).
void cs_max_resolve(exprs const& cs, rational const& w) {
@ -820,7 +820,7 @@ public:
//
// d_0 := false
// d_i := b_{i-1} or d_{i-1} for i = 1...sz-1
// soft (b_i and d_i)
// soft (b_i and d_i)
// == (b_i and (b_0 or b_1 or ... or b_{i-1}))
//
// asm => b_i
@ -836,7 +836,7 @@ public:
fml = m.mk_implies(d, cls);
update_model(d, cls);
add(fml);
m_defs.push_back(fml);
m_defs.push_back(fml);
}
else {
d = cls;
@ -869,7 +869,7 @@ public:
void improve_model(model_ref& mdl) {
if (!m_enable_lns)
if (!m_enable_lns)
return;
flet<bool> _disable_lns(m_enable_lns, false);
m_lns.climb(mdl);
@ -881,16 +881,16 @@ public:
exprs _core(core.size(), core.data());
wcores.push_back(weighted_core(_core, core_weight(_core)));
remove_soft(_core, m_asms);
split_core(_core);
split_core(_core);
}
process_unsat(wcores);
}
rational cost(model& mdl) {
rational upper = m_unfold_upper;
for (soft& s : m_soft)
if (!mdl.is_true(s.s))
upper += s.weight;
for (soft& s : m_soft)
if (!mdl.is_true(s.s))
upper += s.weight;
return upper;
}
@ -898,8 +898,8 @@ public:
improve_model(mdl);
mdl->set_model_completion(true);
unsigned correction_set_size = 0;
for (expr* a : m_asms)
if (mdl->is_false(a))
for (expr* a : m_asms)
if (mdl->is_false(a))
++correction_set_size;
if (!m_csmodel.get() || correction_set_size < m_correction_set_size) {
@ -916,7 +916,7 @@ public:
return;
}
if (!m_c.verify_model(m_index, mdl.get(), upper))
if (!m_c.verify_model(m_index, mdl.get(), upper))
return;
unsigned num_assertions = s().get_num_assertions();
@ -925,14 +925,14 @@ public:
TRACE("opt", tout << "updated upper: " << upper << "\n";);
for (soft& s : m_soft)
for (soft& s : m_soft)
s.set_value(m_model->is_true(s.s));
verify_assignment();
if (num_assertions == s().get_num_assertions())
m_upper = upper;
trace();
add_upper_bound_block();
@ -947,17 +947,17 @@ public:
for (soft& s : m_soft) {
nsoft.push_back(mk_not(m, s.s));
weights.push_back(s.weight);
}
}
fml = u.mk_lt(nsoft.size(), weights.data(), nsoft.data(), m_upper);
TRACE("opt", tout << "block upper bound " << fml << "\n";);;
add(fml);
add(fml);
}
void remove_soft(exprs const& core, expr_ref_vector& asms) {
TRACE("opt", tout << "before remove: " << asms << "\n";);
unsigned j = 0;
for (expr* a : asms)
if (!core.contains(a))
for (expr* a : asms)
if (!core.contains(a))
asms[j++] = a;
asms.shrink(j);
TRACE("opt", tout << "after remove: " << asms << "\n";);
@ -974,8 +974,8 @@ public:
m_pivot_on_cs = p.maxres_pivot_on_correction_set();
m_wmax = p.maxres_wmax();
m_dump_benchmarks = p.dump_benchmarks();
m_enable_lns = p.enable_lns();
m_enable_core_rotate = p.enable_core_rotate();
m_enable_lns = p.enable_lns();
m_enable_core_rotate = p.enable_core_rotate();
m_lns_conflicts = p.lns_conflicts();
if (m_c.num_objectives() > 1)
m_add_upper_bound_block = false;
@ -983,7 +983,6 @@ public:
lbool init_local() {
m_trail.reset();
lbool is_sat = l_true;
for (auto const& [e, w, t] : m_soft)
add_soft(e, w);
m_max_upper = m_upper;
@ -1008,13 +1007,13 @@ public:
void verify_core(exprs const& core) {
return;
IF_VERBOSE(1, verbose_stream() << "verify core " << s().check_sat(core.size(), core.data()) << "\n";);
IF_VERBOSE(1, verbose_stream() << "verify core " << s().check_sat(core.size(), core.data()) << "\n";);
ref<solver> _solver = mk_smt_solver(m, m_params, symbol());
_solver->assert_expr(s().get_assertions());
_solver->assert_expr(core);
lbool is_sat = _solver->check_sat(0, nullptr);
IF_VERBOSE(0, verbose_stream() << "core status (l_false:) " << is_sat << " core size " << core.size() << "\n");
CTRACE("opt", is_sat != l_false,
CTRACE("opt", is_sat != l_false,
for (expr* c : core) tout << "core: " << mk_pp(c, m) << "\n";
_solver->display(tout);
tout << "other solver\n";
@ -1025,18 +1024,18 @@ public:
void verify_assumptions() {
return;
IF_VERBOSE(1, verbose_stream() << "verify assumptions\n";);
IF_VERBOSE(1, verbose_stream() << "verify assumptions\n";);
ref<solver> _solver = mk_smt_solver(m, m_params, symbol());
_solver->assert_expr(s().get_assertions());
_solver->assert_expr(m_asms);
lbool is_sat = _solver->check_sat(0, nullptr);
IF_VERBOSE(1, verbose_stream() << "assignment status (l_true) " << is_sat << "\n";);
IF_VERBOSE(1, verbose_stream() << "assignment status (l_true) " << is_sat << "\n";);
VERIFY(is_sat == l_true);
}
void verify_assignment() {
return;
IF_VERBOSE(1, verbose_stream() << "verify assignment\n";);
IF_VERBOSE(1, verbose_stream() << "verify assignment\n";);
ref<solver> _solver = mk_smt_solver(m, m_params, symbol());
_solver->assert_expr(s().get_assertions());
expr_ref n(m);