From b5309d5fd073c1e056b3ce436c393b28e13afe10 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 16 Apr 2022 16:42:57 +0200 Subject: [PATCH] na --- src/opt/maxres.cpp | 10 ++++++++-- src/opt/maxres.h | 4 ++++ src/opt/opt_params.pyg | 2 +- 3 files changed, 13 insertions(+), 3 deletions(-) diff --git a/src/opt/maxres.cpp b/src/opt/maxres.cpp index 9fcce1fce..10ab3c77b 100644 --- a/src/opt/maxres.cpp +++ b/src/opt/maxres.cpp @@ -774,8 +774,14 @@ public: for (expr* _ : core) partial.push_back(nullptr); - - for (unsigned i = 0; i + 1 < core.size(); ++i) { + + std::cout << "Core size " << core.size() << "\n"; + + if (core.size() > 2) + m_unfold_upper += rational(core.size()-2)*weight; + + expr* w = nullptr; + for (unsigned i = 0; i + 1 < core.size(); i += 2) { expr* a = core.get(i); expr* b = core.get(i + 1); expr* u = mk_fresh_bool("u"); diff --git a/src/opt/maxres.h b/src/opt/maxres.h index 25ef9bf05..947b60492 100644 --- a/src/opt/maxres.h +++ b/src/opt/maxres.h @@ -23,6 +23,10 @@ namespace opt { maxsmt_solver_base* mk_maxres(maxsat_context& c, unsigned id, vector& soft); + maxsmt_solver_base* mk_maxres_binary(maxsat_context& c, unsigned id, vector& soft); + + maxsmt_solver_base* mk_maxres_binary_delay(maxsat_context& c, unsigned id, vector& soft); + maxsmt_solver_base* mk_primal_dual_maxres(maxsat_context& c, unsigned id, vector& soft); }; diff --git a/src/opt/opt_params.pyg b/src/opt/opt_params.pyg index 5106c5492..cb8f1d129 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=(('optsmt_engine', SYMBOL, 'basic', "select optimization engine: 'basic', 'symba'"), - ('maxsat_engine', SYMBOL, 'maxres', "select engine for maxsat: 'core_maxsat', 'wmax', 'maxres', 'pd-maxres'"), + ('maxsat_engine', SYMBOL, 'maxres', "select engine for maxsat: 'core_maxsat', 'wmax', 'maxres', 'pd-maxres', 'maxres-bin', 'maxres-bin-delay'"), ('priority', SYMBOL, 'lex', "select how to priortize objectives: 'lex' (lexicographic), 'pareto', 'box'"), ('dump_benchmarks', BOOL, False, 'dump benchmarks for profiling'), ('dump_models', BOOL, False, 'display intermediary models to stdout'),