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

Merge branch 'opt' of https://git01.codeplex.com/z3 into opt

Browse source
This commit is contained in:
Nikolaj Bjorner 2013-12-04 14:38:24 -08:00
commit 686d146cc6
2 changed files with 12 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

14
src/opt/fu_malik.cpp
View file

@ -205,12 +205,13 @@ namespace opt {
if (!found) { if (!found) {
continue; continue;
} }
expr_ref block_var(m); expr_ref block_var(m), tmp(m);
block_var = m.mk_fresh_const("block_var", m.mk_bool_sort()); block_var = m.mk_fresh_const("block_var", m.mk_bool_sort());
m_aux[i] = m.mk_fresh_const("aux", m.mk_bool_sort()); m_aux[i] = m.mk_fresh_const("aux", m.mk_bool_sort());
m_soft[i] = m.mk_or(m_soft[i].get(), block_var); m_soft[i] = m.mk_or(m_soft[i].get(), block_var);
block_vars.push_back(block_var); block_vars.push_back(block_var);
s().assert_expr(m.mk_or(m_soft[i].get(), m_aux[i].get())); tmp = m.mk_or(m_soft[i].get(), m_aux[i].get());
s().assert_expr(tmp);
} }
SASSERT (!block_vars.empty()); SASSERT (!block_vars.empty());
assert_at_most_one(block_vars); assert_at_most_one(block_vars);
@ -252,7 +253,9 @@ namespace opt {
for (unsigned i = 0; i < num_assertions; ++i) { for (unsigned i = 0; i < num_assertions; ++i) {
g.assert_expr(current_solver.get_assertion(i)); g.assert_expr(current_solver.get_assertion(i));
} }
probe *p = mk_is_qfbv_probe(); #if 0
// TBD: this leaks references somehow
probe_ref p = mk_is_qfbv_probe();
bool all_bv = (*p)(g).is_true(); bool all_bv = (*p)(g).is_true();
if (all_bv) { if (all_bv) {
smt::context & ctx = opt_s.get_context(); smt::context & ctx = opt_s.get_context();
@ -266,6 +269,7 @@ namespace opt {
m_use_new_bv_solver = true; m_use_new_bv_solver = true;
IF_VERBOSE(1, verbose_stream() << "Force to use the new BV solver." << std::endl;); IF_VERBOSE(1, verbose_stream() << "Force to use the new BV solver." << std::endl;);
} }
#endif
} }
// TBD: bug when cancel flag is set, fu_malik returns is_sat == l_true instead of l_undef // TBD: bug when cancel flag is set, fu_malik returns is_sat == l_true instead of l_undef
@ -274,9 +278,11 @@ namespace opt {
lbool is_sat = s().check_sat(0,0); lbool is_sat = s().check_sat(0,0);
if (!m_soft.empty() && is_sat == l_true) { if (!m_soft.empty() && is_sat == l_true) {
solver::scoped_push _sp(s()); solver::scoped_push _sp(s());
expr_ref tmp(m);
for (unsigned i = 0; i < m_soft.size(); ++i) { for (unsigned i = 0; i < m_soft.size(); ++i) {
m_aux.push_back(m.mk_fresh_const("p", m.mk_bool_sort())); m_aux.push_back(m.mk_fresh_const("p", m.mk_bool_sort()));
s().assert_expr(m.mk_or(m_soft[i].get(), m_aux[i].get())); tmp = m.mk_or(m_soft[i].get(), m_aux[i].get());
s().assert_expr(tmp);
} }
lbool is_sat = l_true; lbool is_sat = l_true;

2
src/smt/theory_pb.cpp
View file

@ -1251,6 +1251,7 @@ namespace smt {
justification* cjs = cls.get_justification(); justification* cjs = cls.get_justification();
if (cjs) { if (cjs) {
IF_VERBOSE(0, verbose_stream() << "skipping justification for clause over: " << conseq << "\n";); IF_VERBOSE(0, verbose_stream() << "skipping justification for clause over: " << conseq << "\n";);
m_ineq_literals.push_back(conseq);
break; break;
} }
unsigned num_lits = cls.get_num_literals(); unsigned num_lits = cls.get_num_literals();
@ -1282,6 +1283,7 @@ namespace smt {
// only process pb justifications. // only process pb justifications.
if (j.get_from_theory() != get_id()) { if (j.get_from_theory() != get_id()) {
IF_VERBOSE(0, verbose_stream() << "skipping justification for " << conseq << "\n";); IF_VERBOSE(0, verbose_stream() << "skipping justification for " << conseq << "\n";);
m_ineq_literals.push_back(conseq);
break; break;
} }
pb_justification& pbj = dynamic_cast<pb_justification&>(j); pb_justification& pbj = dynamic_cast<pb_justification&>(j);