mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-01-18 08:18:55 +00:00
Code Activity

add user propagators to opt_solver

Browse source
This commit is contained in:
Nikolaj Bjorner 2025-10-02 19:44:22 -07:00
parent 0e6b3a922a
commit e137aaa249
5 changed files with 58 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

8
src/cmd_context/cmd_context.cpp
View file

@ -657,6 +657,8 @@ void cmd_context::set_opt(opt_wrapper* opt) {
for (auto const& [var, value] : m_var2values)
m_opt->initialize_value(var, value);
m_opt->set_logic(m_logic);
if (m_preferred)
m_opt->set_preferred(m_preferred.get());
}
void cmd_context::global_params_updated() {
@ -1896,11 +1898,9 @@ void cmd_context::set_preferred(expr* fmla) {
get_solver()->user_propagate_register_decide(p->decide_eh);
}
}
if (get_opt())
get_opt()->set_preferred(m_preferred.get());
m_preferred->set_preferred(fmla);
if (get_opt()) {
throw default_exception("setting preferred on optimization context is not supported yet");
return;
}
}
void cmd_context::reset_preferred() {

5
src/cmd_context/cmd_context.h
View file

@ -164,6 +164,9 @@ struct builtin_decl {
};
class opt_wrapper : public check_sat_result {
protected:
preferred_value_propagator *m_preferred = nullptr;
public:
opt_wrapper(ast_manager& m): check_sat_result(m) {}
virtual bool empty() = 0;
@ -177,7 +180,7 @@ public:
virtual void get_box_model(model_ref& mdl, unsigned index) = 0;
virtual void updt_params(params_ref const& p) = 0;
virtual void initialize_value(expr* var, expr* value) = 0;
void set_preferred(preferred_value_propagator *p) { m_preferred = p; }
};
class ast_context_params : public context_params {