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

Another fix for #847. Reset wmax theory solver state between lex calls, otherwise it uses stale constraints

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-01-17 14:19:24 -08:00
parent 6d34899c46
commit 0aa912371b
5 changed files with 14 additions and 11 deletions
Download patch file Download diff file Expand all files Collapse all files

15
src/opt/maxsmt.cpp
View file

@ -55,15 +55,18 @@ namespace opt {
void maxsmt_solver_base::commit_assignment() { void maxsmt_solver_base::commit_assignment() {
expr_ref tmp(m); expr_ref tmp(m);
rational k(0); rational k(0), cost(0);
for (unsigned i = 0; i < m_soft.size(); ++i) { for (unsigned i = 0; i < m_soft.size(); ++i) {
if (get_assignment(i)) { if (get_assignment(i)) {
k += m_weights[i]; k += m_weights[i];
} }
else {
cost += m_weights[i];
}
} }
pb_util pb(m); pb_util pb(m);
tmp = pb.mk_ge(m_weights.size(), m_weights.c_ptr(), m_soft.c_ptr(), k); tmp = pb.mk_ge(m_weights.size(), m_weights.c_ptr(), m_soft.c_ptr(), k);
TRACE("opt", tout << tmp << "\n";); TRACE("opt", tout << "cost: " << cost << "\n" << tmp << "\n";);
s().assert_expr(tmp); s().assert_expr(tmp);
} }
@ -140,7 +143,9 @@ namespace opt {
m_wth = s.ensure_wmax_theory(); m_wth = s.ensure_wmax_theory();
} }
maxsmt_solver_base::scoped_ensure_theory::~scoped_ensure_theory() { maxsmt_solver_base::scoped_ensure_theory::~scoped_ensure_theory() {
//m_wth->reset_local(); if (m_wth) {
m_wth->reset_local();
}
} }
smt::theory_wmaxsat& maxsmt_solver_base::scoped_ensure_theory::operator()() { return *m_wth; } smt::theory_wmaxsat& maxsmt_solver_base::scoped_ensure_theory::operator()() { return *m_wth; }
@ -226,7 +231,9 @@ namespace opt {
m_msolver = 0; m_msolver = 0;
symbol const& maxsat_engine = m_c.maxsat_engine(); symbol const& maxsat_engine = m_c.maxsat_engine();
IF_VERBOSE(1, verbose_stream() << "(maxsmt)\n";); IF_VERBOSE(1, verbose_stream() << "(maxsmt)\n";);
TRACE("opt", tout << "maxsmt\n";); TRACE("opt", tout << "maxsmt\n";
s().display(tout); tout << "\n";
);
if (m_soft_constraints.empty() || maxsat_engine == symbol("maxres") || maxsat_engine == symbol::null) { if (m_soft_constraints.empty() || maxsat_engine == symbol("maxres") || maxsat_engine == symbol::null) {
m_msolver = mk_maxres(m_c, m_index, m_weights, m_soft_constraints); m_msolver = mk_maxres(m_c, m_index, m_weights, m_soft_constraints);
} }

5
src/opt/opt_solver.cpp
View file

@ -328,11 +328,6 @@ namespace opt {
return m_context.get_formulas()[idx]; return m_context.get_formulas()[idx];
} }
std::ostream& opt_solver::display(std::ostream & out) const {
m_context.display(out);
return out;
}
smt::theory_var opt_solver::add_objective(app* term) { smt::theory_var opt_solver::add_objective(app* term) {
smt::theory_var v = get_optimizer().add_objective(term); smt::theory_var v = get_optimizer().add_objective(term);
m_objective_vars.push_back(v); m_objective_vars.push_back(v);

1
src/opt/opt_solver.h
View file

@ -104,7 +104,6 @@ namespace opt {
virtual void set_progress_callback(progress_callback * callback); virtual void set_progress_callback(progress_callback * callback);
virtual unsigned get_num_assertions() const; virtual unsigned get_num_assertions() const;
virtual expr * get_assertion(unsigned idx) const; virtual expr * get_assertion(unsigned idx) const;
virtual std::ostream& display(std::ostream & out) const;
virtual ast_manager& get_manager() const { return m; } virtual ast_manager& get_manager() const { return m; }
virtual lbool find_mutexes(expr_ref_vector const& vars, vector<expr_ref_vector>& mutexes); virtual lbool find_mutexes(expr_ref_vector const& vars, vector<expr_ref_vector>& mutexes);
virtual lbool preferred_sat(expr_ref_vector const& asms, vector<expr_ref_vector>& cores); virtual lbool preferred_sat(expr_ref_vector const& asms, vector<expr_ref_vector>& cores);

1
src/opt/wmax.cpp
View file

@ -64,6 +64,7 @@ namespace opt {
bool was_sat = false; bool was_sat = false;
expr_ref_vector asms(m); expr_ref_vector asms(m);
vector<expr_ref_vector> cores; vector<expr_ref_vector> cores;
obj_map<expr, rational>::iterator it = soft.begin(), end = soft.end(); obj_map<expr, rational>::iterator it = soft.begin(), end = soft.end();
for (; it != end; ++it) { for (; it != end; ++it) {
expr* c = assert_weighted(wth(), it->m_key, it->m_value); expr* c = assert_weighted(wth(), it->m_key, it->m_value);

1
src/smt/smt_context.cpp
View file

@ -1795,6 +1795,7 @@ namespace smt {
void context::set_conflict(b_justification js, literal not_l) { void context::set_conflict(b_justification js, literal not_l) {
if (!inconsistent()) { if (!inconsistent()) {
TRACE("set_conflict", display_literal_verbose(tout, not_l); display(tout, js); );
m_conflict = js; m_conflict = js;
m_not_l = not_l; m_not_l = not_l;
} }