mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-19 20:33:38 +00:00
Code Activity

Allow adding constraints in the model_eh callback

Browse source
This commit is contained in:
Nikolaj Bjorner 2022-04-08 17:12:20 +02:00
parent fbd35fb58d
commit d6d9b25c68
2 changed files with 18 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

15
src/opt/opt_context.cpp
View file

@ -185,17 +185,27 @@ namespace opt {
} }
void context::set_hard_constraints(expr_ref_vector const& fmls) { void context::set_hard_constraints(expr_ref_vector const& fmls) {
if (m_scoped_state.set(fmls)) { if (m_calling_on_model) {
clear_state(); for (expr* f : fmls)
add_hard_constraint(f);
return;
} }
if (m_scoped_state.set(fmls))
clear_state();
} }
void context::add_hard_constraint(expr* f) { void context::add_hard_constraint(expr* f) {
if (m_calling_on_model)
get_solver().assert_expr(f);
else {
m_scoped_state.add(f); m_scoped_state.add(f);
clear_state(); clear_state();
} }
}
void context::add_hard_constraint(expr* f, expr* t) { void context::add_hard_constraint(expr* f, expr* t) {
if (m_calling_on_model)
throw default_exception("adding soft constraints is not supported during callbacks");
m_scoped_state.m_asms.push_back(t); m_scoped_state.m_asms.push_back(t);
m_scoped_state.add(m.mk_implies(t, f)); m_scoped_state.add(m.mk_implies(t, f));
clear_state(); clear_state();
@ -389,6 +399,7 @@ namespace opt {
model_ref md = m->copy(); model_ref md = m->copy();
if (!m_model_fixed.contains(md.get())) if (!m_model_fixed.contains(md.get()))
fix_model(md); fix_model(md);
flet<bool> _calling(m_calling_on_model, true);
m_on_model_eh(m_on_model_ctx, md); m_on_model_eh(m_on_model_ctx, md);
m_model_fixed.pop_back(); m_model_fixed.pop_back();
} }

1
src/opt/opt_context.h
View file

@ -165,6 +165,7 @@ namespace opt {
ast_manager& m; ast_manager& m;
on_model_t m_on_model_ctx; on_model_t m_on_model_ctx;
std::function<void(on_model_t&, model_ref&)> m_on_model_eh; std::function<void(on_model_t&, model_ref&)> m_on_model_eh;
bool m_calling_on_model = false;
arith_util m_arith; arith_util m_arith;
bv_util m_bv; bv_util m_bv;
expr_ref_vector m_hard_constraints; expr_ref_vector m_hard_constraints;