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

add setting to dump intermediary models #2087

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-01-18 15:12:08 -08:00
parent 4caadc6519
commit c45ab6efed
5 changed files with 27 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

17
src/opt/opt_context.cpp
View file

@ -125,7 +125,7 @@ namespace opt {
m_solver(nullptr),
m_pareto1(false),
m_box_index(UINT_MAX),
m_optsmt(m),
m_optsmt(m, *this),
m_scoped_state(m),
m_fm(alloc(generic_model_converter, m, "opt")),
m_model_fixed(),
@ -357,6 +357,17 @@ namespace opt {
}
}
void context::set_model(model_ref& m) {
m_model = m;
opt_params optp(m_params);
if (optp.dump_models()) {
model_ref md = m->copy();
fix_model(md);
std::cout << *md << "\n";
}
}
void context::get_model_core(model_ref& mdl) {
mdl = m_model;
fix_model(mdl);
@ -1062,6 +1073,9 @@ namespace opt {
void context::model_updated(model* md) {
model_ref mdl = md;
set_model(mdl);
#if 0
opt_params optp(m_params);
symbol prefix = optp.solution_prefix();
if (prefix == symbol::null || prefix == symbol("")) return;
@ -1074,6 +1088,7 @@ namespace opt {
out << *mdl;
out.close();
}
#endif
}

2
src/opt/opt_context.h
View file

@ -189,7 +189,7 @@ namespace opt {
bool empty() override { return m_scoped_state.m_objectives.empty(); }
void set_hard_constraints(expr_ref_vector const& hard) override;
lbool optimize(expr_ref_vector const& asms) override;
void set_model(model_ref& _m) override { m_model = _m; }
void set_model(model_ref& _m) override;
void get_model_core(model_ref& _m) override;
void get_box_model(model_ref& _m, unsigned index) override;
void fix_model(model_ref& _m) override;

1
src/opt/opt_params.pyg
View file

@ -5,6 +5,7 @@ def_module_params('opt',
('maxsat_engine', SYMBOL, 'maxres', "select engine for maxsat: 'core_maxsat', 'wmax', 'maxres', 'pd-maxres'"),
('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'),
('solution_prefix', SYMBOL, '', "path prefix to dump intermediary, but non-optimal, solutions"),
('timeout', UINT, UINT_MAX, 'timeout (in milliseconds) (UINT_MAX and 0 mean no timeout)'),
('rlimit', UINT, 0, 'resource limit (0 means no limit)'),

5
src/opt/optsmt.cpp
View file

@ -31,6 +31,7 @@ Notes:
#include <typeinfo>
#include "opt/optsmt.h"
#include "opt/opt_solver.h"
#include "opt/opt_context.h"
#include "ast/arith_decl_plugin.h"
#include "smt/theory_arith.h"
#include "ast/ast_pp.h"
@ -362,12 +363,14 @@ namespace opt {
verbose_stream() << "(optsmt lower bound: " << v << ")\n";
else
verbose_stream() << "(optsmt upper bound: " << (-v) << ")\n";
);
);
expr_ref tmp(m);
for (unsigned i = idx+1; i < m_vars.size(); ++i) {
m_s->maximize_objective(i, tmp);
m_lower[i] = m_s->saved_objective_value(i);
}
m_context.set_model(m_model);
}
}

7
src/opt/optsmt.h
View file

@ -27,8 +27,11 @@ namespace opt {
Returns an optimal assignment to objective functions.
*/
class context;
class optsmt {
ast_manager& m;
context& m_context;
opt_solver* m_s;
vector<inf_eps> m_lower;
vector<inf_eps> m_upper;
@ -40,8 +43,8 @@ namespace opt {
svector<symbol> m_labels;
sref_vector<model> m_models;
public:
optsmt(ast_manager& m):
m(m), m_s(nullptr), m_objs(m), m_lower_fmls(m) {}
optsmt(ast_manager& m, context& ctx):
m(m), m_context(ctx), m_s(nullptr), m_objs(m), m_lower_fmls(m) {}
void setup(opt_solver& solver);