mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-04 05:11:21 +00:00
Code Activity

remove ite terms from objectives to synchronize values in tableau with objective value. Fixes part of (three repros) from issue #120

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@hotmail.com>
This commit is contained in:
Nikolaj Bjorner 2015-06-02 10:38:22 -07:00
parent ffff006945
commit d06207f072
2 changed files with 8 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

7
src/opt/opt_context.cpp
View file

@ -31,6 +31,7 @@ Notes:
#include "propagate_values_tactic.h" #include "propagate_values_tactic.h"
#include "solve_eqs_tactic.h" #include "solve_eqs_tactic.h"
#include "elim_uncnstr_tactic.h" #include "elim_uncnstr_tactic.h"
#include "elim_term_ite_tactic.h"
#include "tactical.h" #include "tactical.h"
#include "model_smt2_pp.h" #include "model_smt2_pp.h"
#include "card2bv_tactic.h" #include "card2bv_tactic.h"
@ -650,17 +651,19 @@ namespace opt {
and_then(mk_simplify_tactic(m), and_then(mk_simplify_tactic(m),
mk_propagate_values_tactic(m), mk_propagate_values_tactic(m),
mk_solve_eqs_tactic(m), mk_solve_eqs_tactic(m),
mk_elim_term_ite_tactic(m),
// NB: mk_elim_uncstr_tactic(m) is not sound with soft constraints // NB: mk_elim_uncstr_tactic(m) is not sound with soft constraints
mk_simplify_tactic(m)); mk_simplify_tactic(m));
opt_params optp(m_params); opt_params optp(m_params);
tactic_ref tac2, tac3; tactic_ref tac2, tac3, tac4;
if (optp.elim_01()) { if (optp.elim_01()) {
tac2 = mk_elim01_tactic(m); tac2 = mk_elim01_tactic(m);
tac3 = mk_lia2card_tactic(m); tac3 = mk_lia2card_tactic(m);
tac4 = mk_elim_term_ite_tactic(m);
params_ref lia_p; params_ref lia_p;
lia_p.set_bool("compile_equality", optp.pb_compile_equality()); lia_p.set_bool("compile_equality", optp.pb_compile_equality());
tac3->updt_params(lia_p); tac3->updt_params(lia_p);
set_simplify(and_then(tac0.get(), tac2.get(), tac3.get())); set_simplify(and_then(tac0.get(), tac2.get(), tac3.get(), tac4.get()));
} }
else { else {
set_simplify(tac0.get()); set_simplify(tac0.get());

3
src/opt/optsmt.cpp
View file

@ -141,6 +141,7 @@ namespace opt {
ors.push_back(m_s->mk_ge(i, m_upper[i])); ors.push_back(m_s->mk_ge(i, m_upper[i]));
} }
fml = m.mk_or(ors.size(), ors.c_ptr()); fml = m.mk_or(ors.size(), ors.c_ptr());
tmp = m.mk_fresh_const("b", m.mk_bool_sort()); tmp = m.mk_fresh_const("b", m.mk_bool_sort());
fml = m.mk_implies(tmp, fml); fml = m.mk_implies(tmp, fml);
@ -150,6 +151,7 @@ namespace opt {
solver::scoped_push _push(*m_s); solver::scoped_push _push(*m_s);
while (!m_cancel) { while (!m_cancel) {
m_s->assert_expr(fml); m_s->assert_expr(fml);
TRACE("opt", tout << fml << "\n";);
is_sat = m_s->check_sat(1,vars); is_sat = m_s->check_sat(1,vars);
if (is_sat == l_true) { if (is_sat == l_true) {
disj.reset(); disj.reset();
@ -343,6 +345,7 @@ namespace opt {
m_lower[i] = m_s->saved_objective_value(i); m_lower[i] = m_s->saved_objective_value(i);
} }
} }
TRACE("opt", tout << "strengthen bound: " << block << "\n";);
m_s->assert_expr(block); m_s->assert_expr(block);
// TBD: only works for simplex // TBD: only works for simplex