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

add solution_prefix per #1463, have parto with single objective behave similar to multipe-objectives #1439

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-01-28 11:45:39 -08:00
parent 57406d6cc4
commit e4198c38e2
6 changed files with 31 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/opt/maxres.cpp
View file

@ -727,6 +727,7 @@ public:
}
m_model = mdl;
m_c.model_updated(mdl);
for (unsigned i = 0; i < m_soft.size(); ++i) {
m_assignment[i] = is_true(m_soft[i]);

6
src/opt/maxsmt.cpp
View file

@ -155,7 +155,7 @@ namespace opt {
rational l = m_adjust_value(m_lower);
rational u = m_adjust_value(m_upper);
if (l > u) std::swap(l, u);
verbose_stream() << "(opt." << solver << " [" << l << ":" << u << "])\n";);
verbose_stream() << "(opt." << solver << " [" << l << ":" << u << "])\n";);
}
lbool maxsmt_solver_base::find_mutexes(obj_map<expr, rational>& new_soft) {
@ -391,6 +391,10 @@ namespace opt {
return m_c.get_solver();
}
void maxsmt::model_updated(model* mdl) {
m_c.model_updated(mdl);
}
};

1
src/opt/maxsmt.h
View file

@ -147,6 +147,7 @@ namespace opt {
bool get_assignment(unsigned index) const;
void display_answer(std::ostream& out) const;
void collect_statistics(statistics& st) const;
void model_updated(model* mdl);
private:
bool is_maxsat_problem(weights_t& ws) const;
void verify_assignment();

19
src/opt/opt_context.cpp
View file

@ -138,6 +138,7 @@ namespace opt {
p.set_bool("unsat_core", true);
p.set_bool("elim_to_real", true);
updt_params(p);
m_model_counter = 0;
}
context::~context() {
@ -1007,6 +1008,22 @@ namespace opt {
}
}
void context::model_updated(model* md) {
opt_params optp(m_params);
symbol prefix = optp.solution_prefix();
if (prefix == symbol::null) return;
model_ref mdl = md->copy();
fix_model(mdl);
std::ostringstream buffer;
buffer << prefix << (m_model_counter++) << ".smt2";
std::ofstream out(buffer.str());
if (out) {
model_smt2_pp(out, m, *mdl, 0);
out.close();
}
}
bool context::verify_model(unsigned index, model* md, rational const& _v) {
rational r;
app_ref term = m_objectives[index].m_term;
@ -1015,7 +1032,7 @@ namespace opt {
}
rational v = m_objectives[index].m_adjust_value(_v);
expr_ref val(m);
model_ref mdl = md;
model_ref mdl = md->copy();
fix_model(mdl);
if (!mdl->eval(term, val)) {

6
src/opt/opt_context.h
View file

@ -57,6 +57,7 @@ namespace opt {
virtual unsigned num_objectives() = 0;
virtual bool verify_model(unsigned id, model* mdl, rational const& v) = 0;
virtual void set_model(model_ref& _m) = 0;
virtual void model_updated(model* mdl) = 0;
};
/**
@ -154,9 +155,10 @@ namespace opt {
map_t m_maxsmts;
scoped_state m_scoped_state;
vector<objective> m_objectives;
model_ref m_model;
model_ref m_model;
model_converter_ref m_model_converter;
filter_model_converter m_fm;
unsigned m_model_counter;
obj_map<func_decl, unsigned> m_objective_fns;
obj_map<func_decl, expr*> m_objective_orig;
func_decl_ref_vector m_objective_refs;
@ -231,6 +233,8 @@ namespace opt {
virtual bool verify_model(unsigned id, model* mdl, rational const& v);
virtual void model_updated(model* mdl);
private:
lbool execute(objective const& obj, bool committed, bool scoped);

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', or 'box'"),
('dump_benchmarks', BOOL, False, 'dump benchmarks for profiling'),
('solution_prefix', SYMBOL, None, "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)'),
('enable_sls', BOOL, False, 'enable SLS tuning during weighted maxsast'),