From 69a5634e7ed155387211dc87fa02f8272aff7619 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 14 Oct 2014 16:33:55 -0700 Subject: [PATCH] adding symba designated strategy (back?) to optsmt Signed-off-by: Nikolaj Bjorner --- src/opt/opt_context.cpp | 11 ++++++ src/opt/opt_context.h | 1 + src/opt/opt_params.pyg | 2 +- src/opt/optsmt.cpp | 82 +++++++++++++++++++++++++++++++++++------ src/opt/optsmt.h | 4 +- src/smt/smt_setup.cpp | 7 +++- 6 files changed, 92 insertions(+), 15 deletions(-) diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp index 09d3a809a..64978b39e 100644 --- a/src/opt/opt_context.cpp +++ b/src/opt/opt_context.cpp @@ -435,6 +435,7 @@ namespace opt { } void context::init_solver() { + setup_arith_solver(); #pragma omp critical (opt_context) { m_opt_solver = alloc(opt_solver, m, m_params, m_fm); @@ -443,6 +444,16 @@ namespace opt { } } + void context::setup_arith_solver() { + opt_params p(m_params); + if (p.optsmt_engine() == symbol("symba") || + p.optsmt_engine() == symbol("farkas")) { + std::stringstream strm; + strm << AS_OPTINF; + gparams::set("smt.arith.solver", strm.str().c_str()); + } + } + void context::update_solver() { if (!m_enable_sat || !probe_bv()) { return; diff --git a/src/opt/opt_context.h b/src/opt/opt_context.h index eb8dd6fc6..0a342e058 100644 --- a/src/opt/opt_context.h +++ b/src/opt/opt_context.h @@ -224,6 +224,7 @@ namespace opt { void init_solver(); void update_solver(); + void setup_arith_solver(); void add_maxsmt(symbol const& id); void set_simplify(tactic *simplify); void set_pareto(pareto_base* p); diff --git a/src/opt/opt_params.pyg b/src/opt/opt_params.pyg index 9d20dcb33..f84c6eebf 100644 --- a/src/opt/opt_params.pyg +++ b/src/opt/opt_params.pyg @@ -2,7 +2,7 @@ def_module_params('opt', description='optimization parameters', export=True, params=(('timeout', UINT, UINT_MAX, 'set timeout'), - ('engine', SYMBOL, 'basic', "select optimization engine: 'basic', 'farkas', 'symba'"), + ('optsmt_engine', SYMBOL, 'basic', "select optimization engine: 'basic', 'farkas', 'symba'"), ('maxsat_engine', SYMBOL, 'wmax', "select engine for maxsat: 'fu_malik', 'core_maxsat', 'wmax', 'pbmax', 'maxres', 'bcd2', 'wpm2', 'sls', 'maxhs'"), ('priority', SYMBOL, 'lex', "select how to priortize objectives: 'lex' (lexicographic), 'pareto', or 'box'"), ('dump_benchmarks', BOOL, False, 'dump benchmarks for profiling'), diff --git a/src/opt/optsmt.cpp b/src/opt/optsmt.cpp index 6cc6eeeab..0d82e4410 100644 --- a/src/opt/optsmt.cpp +++ b/src/opt/optsmt.cpp @@ -107,6 +107,62 @@ namespace opt { return l_true; } + lbool optsmt::symba_opt() { + smt::theory_opt& opt = m_s->get_optimizer(); + + if (typeid(smt::theory_inf_arith) != typeid(opt)) { + return l_undef; + } + + + expr_ref_vector ors(m), disj(m); + expr_ref or(m), bound(m.mk_true(), m); + for (unsigned i = 0; i < m_upper.size(); ++i) { + ors.push_back(m_s->mk_ge(i, m_upper[i])); + } + { + solver::scoped_push _push(*m_s); + or = m.mk_or(ors.size(), ors.c_ptr()); + m_s->assert_expr(or); + lbool is_sat = l_true; + while (!m_cancel) { + is_sat = m_s->check_sat(0,0); + if (is_sat == l_true) { + disj.reset(); + m_s->maximize_objectives(disj); + m_s->get_model(m_model); + set_max(m_lower, m_s->get_objective_values()); + for (unsigned i = 0; i < ors.size(); ++i) { + expr_ref tmp(m); + m_model->eval(ors[i].get(), tmp); + if (m.is_true(tmp)) { + m_lower[i] = m_upper[i]; + ors[i] = m.mk_false(); + } + if (m.is_false(ors[i].get())) { + disj[i] = m.mk_false(); + } + } + or = m.mk_or(ors.size(), ors.c_ptr()); + bound = m.mk_or(disj.size(), disj.c_ptr()); + m_s->assert_expr(or); + } + else if (is_sat == l_undef) { + return l_undef; + } + else { + break; + } + } + } + m_s->assert_expr(bound); + + if (m_cancel) { + return l_undef; + } + return basic_opt(); + } + void optsmt::update_lower(unsigned idx, inf_eps const& v, bool override) { if (m_lower[idx] < v || override) { m_lower[idx] = v; @@ -124,13 +180,13 @@ namespace opt { m_s->maximize_objectives(disj); m_s->get_model(m_model); set_max(m_lower, m_s->get_objective_values()); - IF_VERBOSE(1, - for (unsigned i = 0; i < m_lower.size(); ++i) { - verbose_stream() << m_lower[i] << " "; - } - verbose_stream() << "\n"; - model_pp(verbose_stream(), *m_model); - ); + TRACE("opt", + for (unsigned i = 0; i < m_lower.size(); ++i) { + tout << m_lower[i] << " "; + } + tout << "\n"; + model_pp(tout, *m_model); + ); expr_ref constraint(m); constraint = m.mk_or(disj.size(), disj.c_ptr()); m_s->assert_expr(constraint); @@ -171,13 +227,13 @@ namespace opt { lbool is_sat = m_s->check_sat(1, bounds.c_ptr() + i); switch(is_sat) { case l_true: - IF_VERBOSE(2, verbose_stream() << "Setting lower bound for v" << m_vars[i] << " to " << m_upper[i] << "\n";); + IF_VERBOSE(2, verbose_stream() << "(optsmt lower bound for v" << m_vars[i] << " := " << m_upper[i] << ")\n";); m_lower[i] = mid[i]; th.enable_record_conflict(0); update_lower(); break; case l_false: - IF_VERBOSE(2, verbose_stream() << "conflict: " << th.conflict_minimize() << "\n";); + IF_VERBOSE(2, verbose_stream() << "(optsmt conflict: " << th.conflict_minimize() << ") \n";); if (!th.conflict_minimize().is_finite()) { // bounds is not in the core. The context is unsat. m_upper[i] = m_lower[i]; @@ -288,13 +344,15 @@ namespace opt { } // assertions added during search are temporary. solver::scoped_push _push(*m_s); - if (m_engine == symbol("farkas")) { + if (m_optsmt_engine == symbol("farkas")) { is_sat = farkas_opt(); } + else if (m_optsmt_engine == symbol("symba")) { + is_sat = symba_opt(); + } else { is_sat = basic_opt(); } - return is_sat; } @@ -337,7 +395,7 @@ namespace opt { void optsmt::updt_params(params_ref& p) { opt_params _p(p); - m_engine = _p.engine(); + m_optsmt_engine = _p.optsmt_engine(); } void optsmt::reset() { diff --git a/src/opt/optsmt.h b/src/opt/optsmt.h index 95e24a439..35e2a3d46 100644 --- a/src/opt/optsmt.h +++ b/src/opt/optsmt.h @@ -35,7 +35,7 @@ namespace opt { vector m_upper; app_ref_vector m_objs; svector m_vars; - symbol m_engine; + symbol m_optsmt_engine; model_ref m_model; public: optsmt(ast_manager& m): m(m), m_s(0), m_cancel(false), m_objs(m) {} @@ -67,6 +67,8 @@ namespace opt { lbool basic_opt(); + lbool symba_opt(); + lbool basic_lex(unsigned idx, bool is_maximize); lbool farkas_opt(); diff --git a/src/smt/smt_setup.cpp b/src/smt/smt_setup.cpp index 092db9f1a..5eac22853 100644 --- a/src/smt/smt_setup.cpp +++ b/src/smt/smt_setup.cpp @@ -703,7 +703,12 @@ namespace smt { } void setup::setup_mi_arith() { - m_context.register_plugin(alloc(smt::theory_mi_arith, m_manager, m_params)); + if (m_params.m_arith_mode == AS_OPTINF) { + m_context.register_plugin(alloc(smt::theory_inf_arith, m_manager, m_params)); + } + else { + m_context.register_plugin(alloc(smt::theory_mi_arith, m_manager, m_params)); + } } void setup::setup_arith() {