mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-24 23:03:41 +00:00
Code Activity

Fix a couple compiler warnings

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2022-06-04 08:00:56 +01:00
parent f652c57bfe
commit ed7db892f9
No known key found for this signature in database
GPG key ID: BCF6360F86294467
2 changed files with 86 additions and 87 deletions
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_rec_decls;
stacked_value<unsigned> m_decls; stacked_value<unsigned> m_decls;
stacked_value<unsigned> m_sorts; stacked_value<unsigned> m_sorts;
public: public:
decl_collector coll; 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 reset() { coll.reset(); m_removed.reset(); m_sorts.clear(0u); m_decls.clear(0u); m_rec_decls.clear(0u); }
void collect(expr* e); void collect(expr* e);
@ -59,7 +59,7 @@ class ast_pp_util {
std::ostream& display_expr(std::ostream& out, expr* f, bool neat = true); std::ostream& display_expr(std::ostream& out, expr* f, bool neat = true);
void push(); void push();
void pop(unsigned n); void pop(unsigned n);
smt2_pp_environment& env() { return m_env; } smt2_pp_environment& env() { return m_env; }

163
src/opt/maxcore.cpp
View file

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