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

change model binding time

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2013-12-05 11:42:04 -08:00
parent 56c4fa8f6d
commit 192ce11ca6
2 changed files with 23 additions and 12 deletions
Download patch file Download diff file Expand all files Collapse all files

34
src/opt/opt_context.cpp
View file

@ -66,24 +66,34 @@ namespace opt {
s.assert_expr(m_hard_constraints[i].get()); s.assert_expr(m_hard_constraints[i].get());
} }
if (m_objectives.size() == 1) { lbool is_sat = s.check_sat_core(0,0);
if (is_sat != l_true) {
m_model = 0;
return is_sat;
}
s.get_model(m_model);
switch (m_objectives.size()) {
case 0:
return is_sat;
case 1:
return execute(m_objectives[0], false); return execute(m_objectives[0], false);
default: {
symbol pri = m_params.get_sym("priority", symbol("lex"));
if (pri == symbol("pareto")) {
return execute_pareto();
}
else if (pri == symbol("box")) {
return execute_box();
}
else {
return execute_lex();
}
} }
symbol pri = m_params.get_sym("priority", symbol("lex"));
if (pri == symbol("pareto")) {
return execute_pareto();
}
else if (pri == symbol("box")) {
return execute_box();
}
else {
return execute_lex();
} }
} }
void context::get_model(model_ref& mdl) { void context::get_model(model_ref& mdl) {
get_solver().get_model(mdl); mdl = m_model;
} }
lbool context::execute_min_max(unsigned index, bool committed, bool is_max) { lbool context::execute_min_max(unsigned index, bool committed, bool is_max) {

1
src/opt/opt_context.h
View file

@ -66,6 +66,7 @@ namespace opt {
optsmt m_optsmt; optsmt m_optsmt;
map_t m_maxsmts; map_t m_maxsmts;
vector<objective> m_objectives; vector<objective> m_objectives;
model_ref m_model;
public: public:
context(ast_manager& m); context(ast_manager& m);
~context(); ~context();