mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-10 19:27:06 +00:00
Code Activity

na

Browse source
This commit is contained in:
Nikolaj Bjorner 2022-04-16 16:42:57 +02:00
parent c131eb4db1
commit b5309d5fd0
3 changed files with 13 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
src/opt/maxres.cpp
View file

@ -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");

4
src/opt/maxres.h
View file

@ -23,6 +23,10 @@ namespace opt {
maxsmt_solver_base* mk_maxres(maxsat_context& c, unsigned id, vector<soft>& soft);
maxsmt_solver_base* mk_maxres_binary(maxsat_context& c, unsigned id, vector<soft>& soft);
maxsmt_solver_base* mk_maxres_binary_delay(maxsat_context& c, unsigned id, vector<soft>& soft);
maxsmt_solver_base* mk_primal_dual_maxres(maxsat_context& c, unsigned id, vector<soft>& soft);
};

2
src/opt/opt_params.pyg
View file

@ -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'),