diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp index dbb2b7eb9..93f7e1acd 100644 --- a/src/opt/opt_context.cpp +++ b/src/opt/opt_context.cpp @@ -27,7 +27,6 @@ Notes: #include "th_rewriter.h" #include "opt_params.hpp" - namespace opt { context::context(ast_manager& m): @@ -49,7 +48,7 @@ namespace opt { // really just works for opt_solver now. solver* s = m_solver.get(); - opt_solver::scoped_push _sp(get_opt_solver(*s)); + opt_solver::scoped_push _sp(*s); for (unsigned i = 0; i < m_hard_constraints.size(); ++i) { s->assert_expr(m_hard_constraints[i].get()); @@ -57,7 +56,7 @@ namespace opt { lbool is_sat; - is_sat = m_maxsmt(get_opt_solver(*s)); + is_sat = m_maxsmt(*s); expr_ref_vector ans = m_maxsmt.get_assignment(); for (unsigned i = 0; i < ans.size(); ++i) { @@ -65,32 +64,17 @@ namespace opt { } if (is_sat == l_true) { - is_sat = m_optsmt(get_opt_solver(*s)); + is_sat = m_optsmt(opt_solver::to_opt(*s)); } } - opt_solver& context::get_opt_solver(solver& s) { - if (typeid(opt_solver) != typeid(s)) { - throw default_exception("BUG: optimization context has not been initialized correctly"); - } - return dynamic_cast(s); - } - - void context::cancel() { + void context::set_cancel(bool f) { if (m_solver) { - m_solver->cancel(); + m_solver->set_cancel(f); } - m_optsmt.set_cancel(true); - m_maxsmt.set_cancel(true); - } - - void context::reset_cancel() { - if (m_solver) { - m_solver->reset_cancel(); - } - m_optsmt.set_cancel(false); - m_maxsmt.set_cancel(false); + m_optsmt.set_cancel(f); + m_maxsmt.set_cancel(f); } void context::collect_statistics(statistics& stats) { @@ -108,8 +92,7 @@ namespace opt { if (m_solver) { m_solver->updt_params(m_params); } - opt_params _p(m_params); - m_optsmt.set_engine(_p.engine()); + m_optsmt.updt_params(m_params); } diff --git a/src/opt/opt_context.h b/src/opt/opt_context.h index beae83fe0..df2ca8248 100644 --- a/src/opt/opt_context.h +++ b/src/opt/opt_context.h @@ -28,7 +28,7 @@ Notes: #include "ast.h" #include "solver.h" #include "optsmt.h" -#include "opt_maxsmt.h" +#include "maxsmt.h" namespace opt { @@ -49,8 +49,9 @@ namespace opt { void add_hard_constraint(expr* f) { m_hard_constraints.push_back(f); } void set_solver(solver* s) { m_solver = s; } void optimize(); - void cancel(); - void reset_cancel(); + void set_cancel(bool f); + void reset_cancel() { set_cancel(false); } + void cancel() { set_cancel(true); } void collect_statistics(statistics& stats); static void collect_param_descrs(param_descrs & r); void updt_params(params_ref& p); diff --git a/src/opt/opt_maxsmt.cpp b/src/opt/opt_maxsmt.cpp deleted file mode 100644 index 97c73b61f..000000000 --- a/src/opt/opt_maxsmt.cpp +++ /dev/null @@ -1,75 +0,0 @@ -/*++ -Copyright (c) 2013 Microsoft Corporation - -Module Name: - - opt_maxsmt.cpp - -Abstract: - - MaxSMT optimization context. - -Author: - - Nikolaj Bjorner (nbjorner) 2013-11-7 - -Notes: - ---*/ - -#include "opt_maxsmt.h" -#include "fu_malik.h" -#include "weighted_maxsat.h" -#include "ast_pp.h" - -namespace opt { - - lbool maxsmt::operator()(opt_solver& s) { - lbool is_sat; - m_answer.reset(); - m_answer.append(m_soft_constraints); - if (m_answer.empty()) { - is_sat = s.check_sat(0, 0); - } - else if (is_maxsat_problem(m_weights)) { - is_sat = opt::fu_malik_maxsat(s, m_answer); - } - else { - is_sat = weighted_maxsat(s, m_answer, m_weights); - } - - // Infrastructure for displaying and storing solution is TBD. - std::cout << "is-sat: " << is_sat << "\n"; - if (is_sat == l_true) { - std::cout << "Satisfying soft constraints\n"; - display_answer(std::cout); - } - return is_sat; - } - - expr_ref_vector maxsmt::get_assignment() const { - return m_answer; - } - - void maxsmt::display_answer(std::ostream& out) const { - for (unsigned i = 0; i < m_answer.size(); ++i) { - out << mk_pp(m_answer[i], m) << "\n"; - } - } - - void maxsmt::set_cancel(bool f) { - m_cancel = f; - } - - bool maxsmt::is_maxsat_problem(vector const& ws) const { - for (unsigned i = 0; i < ws.size(); ++i) { - if (!ws[i].is_one()) { - return false; - } - } - return true; - } - - - -}; diff --git a/src/opt/opt_maxsmt.h b/src/opt/opt_maxsmt.h deleted file mode 100644 index 0303e4a99..000000000 --- a/src/opt/opt_maxsmt.h +++ /dev/null @@ -1,66 +0,0 @@ -/*++ -Copyright (c) 2013 Microsoft Corporation - -Module Name: - - opt_maxsmt.h - -Abstract: - - MaxSMT optimization context. - -Author: - - Nikolaj Bjorner (nbjorner) 2013-11-7 - -Notes: - ---*/ -#ifndef _OPT_MAXSMT_H_ -#define _OPT_MAXSMT_H_ - -#include "opt_solver.h" - -namespace opt { - /** - Takes solver with hard constraints added. - Returns modified soft constraints that are maximal assignments. - */ - - class maxsmt { - ast_manager& m; - opt_solver* s; - volatile bool m_cancel; - expr_ref_vector m_soft_constraints; - expr_ref_vector m_answer; - vector m_weights; - symbol m_engine; - public: - maxsmt(ast_manager& m): m(m), s(0), m_cancel(false), m_soft_constraints(m), m_answer(m) {} - - lbool operator()(opt_solver& s); - - void set_cancel(bool f); - - void add(expr* f, rational const& w) { - m_soft_constraints.push_back(f); - m_weights.push_back(w); - } - - void set_engine(symbol const& e) { m_engine = e; } - - // TBD: rational get_value() const; - - expr_ref_vector get_assignment() const; - - void display_answer(std::ostream& out) const; - - private: - - bool is_maxsat_problem(vector const& ws) const; - - }; - -}; - -#endif diff --git a/src/opt/opt_solver.cpp b/src/opt/opt_solver.cpp index 998214464..cd31e870c 100644 --- a/src/opt/opt_solver.cpp +++ b/src/opt/opt_solver.cpp @@ -187,6 +187,13 @@ namespace opt { m_objective_values.reset(); } + opt_solver& opt_solver::to_opt(solver& s) { + if (typeid(opt_solver) != typeid(s)) { + throw default_exception("BUG: optimization context has not been initialized correctly"); + } + return dynamic_cast(s); + } + opt_solver::toggle_objective::toggle_objective(opt_solver& s, bool new_value): s(s), m_old_value(s.m_objective_enabled) { s.m_objective_enabled = new_value; } diff --git a/src/opt/opt_solver.h b/src/opt/opt_solver.h index 4afa65f31..2c96e65ec 100644 --- a/src/opt/opt_solver.h +++ b/src/opt/opt_solver.h @@ -73,6 +73,8 @@ namespace opt { vector const& get_objective_values(); expr_ref block_lower_bound(unsigned obj_index, inf_eps const& val); + + static opt_solver& to_opt(solver& s); class toggle_objective { opt_solver& s; @@ -83,9 +85,9 @@ namespace opt { }; class scoped_push { - opt_solver& s; + solver& s; public: - scoped_push(opt_solver& s):s(s) { s.push(); } + scoped_push(solver& s):s(s) { s.push(); } ~scoped_push() { s.pop(1); } }; diff --git a/src/opt/optsmt.cpp b/src/opt/optsmt.cpp index 4dcefb577..9c7268913 100644 --- a/src/opt/optsmt.cpp +++ b/src/opt/optsmt.cpp @@ -47,6 +47,7 @@ Notes: #include "ast_pp.h" #include "model_pp.h" #include "th_rewriter.h" +#include "opt_params.hpp" namespace opt { @@ -245,8 +246,8 @@ namespace opt { return is_sat; } - inf_eps optsmt::get_value(bool as_positive, unsigned index) const { - if (as_positive) { + inf_eps optsmt::get_value(unsigned index) const { + if (m_is_max[index]) { return m_lower[index]; } else { @@ -258,7 +259,7 @@ namespace opt { unsigned sz = m_objs.size(); for (unsigned i = 0; i < sz; ++i) { bool is_max = m_is_max[i]; - inf_eps val = get_value(is_max, i); + inf_eps val = get_value(i); expr_ref obj(m_objs[i], m); if (!is_max) { arith_util a(m); @@ -283,6 +284,10 @@ namespace opt { m_is_max.push_back(is_max); } + void optsmt::updt_params(params_ref& p) { + opt_params _p(p); + m_engine = _p.engine(); + } } diff --git a/src/opt/optsmt.h b/src/opt/optsmt.h index 1d51dadfc..297f924ae 100644 --- a/src/opt/optsmt.h +++ b/src/opt/optsmt.h @@ -36,7 +36,7 @@ namespace opt { app_ref_vector m_objs; svector m_is_max; svector m_vars; - symbol m_engine; + symbol m_engine; public: optsmt(ast_manager& m): m(m), s(0), m_cancel(false), m_objs(m) {} @@ -46,11 +46,11 @@ namespace opt { void set_cancel(bool f); - void set_engine(symbol const& e) { m_engine = e; } + void updt_params(params_ref& p); void display(std::ostream& out) const; - inf_eps get_value(bool as_positive, unsigned index) const; + inf_eps get_value(unsigned index) const; private: