From fc36d861a7e451cc1793242b8e0d8eb719c8aaad Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 1 Apr 2015 19:32:50 -0700 Subject: [PATCH] update default to maxres for MaxSAT, reset pareto and box state on every constraint update Signed-off-by: Nikolaj Bjorner --- src/opt/opt_context.cpp | 16 +++++++++++----- src/opt/opt_context.h | 1 + src/opt/opt_params.pyg | 2 +- 3 files changed, 13 insertions(+), 6 deletions(-) diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp index 6718f401e..0503fa664 100644 --- a/src/opt/opt_context.cpp +++ b/src/opt/opt_context.cpp @@ -154,7 +154,7 @@ namespace opt { for (unsigned i = 0; i < n; ++i) { m_scoped_state.pop(); } - m_model.reset(); + clear_state(); reset_maxsmts(); m_optsmt.reset(); m_hard_constraints.reset(); @@ -162,21 +162,21 @@ namespace opt { void context::set_hard_constraints(ptr_vector& fmls) { m_scoped_state.set(fmls); - m_model.reset(); + clear_state(); } void context::add_hard_constraint(expr* f) { m_scoped_state.add(f); - m_model.reset(); + clear_state(); } unsigned context::add_soft_constraint(expr* f, rational const& w, symbol const& id) { - m_model.reset(); + clear_state(); return m_scoped_state.add(f, w, id); } unsigned context::add_objective(app* t, bool is_max) { - m_model.reset(); + clear_state(); return m_scoped_state.add(t, is_max); } @@ -1122,6 +1122,12 @@ namespace opt { } } + void context::clear_state() { + set_pareto(0); + m_box_index = UINT_MAX; + m_model.reset(); + } + void context::set_pareto(pareto_base* p) { #pragma omp critical (opt_context) { diff --git a/src/opt/opt_context.h b/src/opt/opt_context.h index 0815e0061..1b5671113 100644 --- a/src/opt/opt_context.h +++ b/src/opt/opt_context.h @@ -271,6 +271,7 @@ namespace opt { void add_maxsmt(symbol const& id); void set_simplify(tactic *simplify); void set_pareto(pareto_base* p); + void clear_state(); bool is_numeral(expr* e, rational& n) const; diff --git a/src/opt/opt_params.pyg b/src/opt/opt_params.pyg index 059ac0bd2..13049986a 100644 --- a/src/opt/opt_params.pyg +++ b/src/opt/opt_params.pyg @@ -3,7 +3,7 @@ def_module_params('opt', export=True, params=(('timeout', UINT, UINT_MAX, 'set timeout'), ('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', 'pd-maxres', 'bcd2', 'wpm2', 'sls', 'maxhs'"), + ('maxsat_engine', SYMBOL, 'maxres', "select engine for maxsat: 'fu_malik', 'core_maxsat', 'wmax', 'pbmax', 'maxres', 'pd-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'), ('print_model', BOOL, False, 'display model for satisfiable constraints'),