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

fix more bugs with compilation of pb equalities

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-02-04 09:51:45 -08:00
parent 354c16454a
commit 20fe08d80c
3 changed files with 11 additions and 25 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/sat/ba_solver.cpp
View file

@ -1571,7 +1571,7 @@ namespace sat {
m_constraints.push_back(c); m_constraints.push_back(c);
} }
literal lit = c->lit(); literal lit = c->lit();
if (c->learned() && !s().at_base_lvl()) { if (c->learned() && m_solver && !s().at_base_lvl()) {
SASSERT(lit == null_literal); SASSERT(lit == null_literal);
// gets initialized after backjump. // gets initialized after backjump.
m_constraint_to_reinit.push_back(c); m_constraint_to_reinit.push_back(c);

17
src/sat/tactic/goal2sat.cpp
View file

@ -495,8 +495,8 @@ struct goal2sat::imp {
SASSERT(k.is_unsigned()); SASSERT(k.is_unsigned());
svector<wliteral> wlits; svector<wliteral> wlits;
convert_pb_args(t, wlits); convert_pb_args(t, wlits);
sat::bool_var v1 = root ? sat::null_bool_var : m_solver.mk_var(true); sat::bool_var v1 = (root && !sign) ? sat::null_bool_var : m_solver.mk_var(true);
sat::bool_var v2 = root ? sat::null_bool_var : m_solver.mk_var(true); sat::bool_var v2 = (root && !sign) ? sat::null_bool_var : m_solver.mk_var(true);
m_ext->add_pb_ge(v1, wlits, k.get_unsigned()); m_ext->add_pb_ge(v1, wlits, k.get_unsigned());
k.neg(); k.neg();
for (wliteral& wl : wlits) { for (wliteral& wl : wlits) {
@ -505,7 +505,7 @@ struct goal2sat::imp {
} }
check_unsigned(k); check_unsigned(k);
m_ext->add_pb_ge(v2, wlits, k.get_unsigned()); m_ext->add_pb_ge(v2, wlits, k.get_unsigned());
if (root) { if (root && !sign) {
m_result_stack.reset(); m_result_stack.reset();
} }
else { else {
@ -516,7 +516,8 @@ struct goal2sat::imp {
mk_clause(~l, l2); mk_clause(~l, l2);
mk_clause(~l1, ~l2, l); mk_clause(~l1, ~l2, l);
m_result_stack.shrink(m_result_stack.size() - t->get_num_args()); m_result_stack.shrink(m_result_stack.size() - t->get_num_args());
m_result_stack.push_back(l); m_result_stack.push_back(sign ? ~l : l);
if (root) mk_clause(~l);
} }
} }
@ -564,8 +565,8 @@ struct goal2sat::imp {
SASSERT(k.is_unsigned()); SASSERT(k.is_unsigned());
sat::literal_vector lits; sat::literal_vector lits;
convert_pb_args(t->get_num_args(), lits); convert_pb_args(t->get_num_args(), lits);
sat::bool_var v1 = root ? sat::null_bool_var : m_solver.mk_var(true); sat::bool_var v1 = (root && !sign) ? sat::null_bool_var : m_solver.mk_var(true);
sat::bool_var v2 = root ? sat::null_bool_var : m_solver.mk_var(true); sat::bool_var v2 = (root && !sign) ? sat::null_bool_var : m_solver.mk_var(true);
m_ext->add_at_least(v1, lits, k.get_unsigned()); m_ext->add_at_least(v1, lits, k.get_unsigned());
for (sat::literal& l : lits) { for (sat::literal& l : lits) {
l.neg(); l.neg();
@ -573,7 +574,7 @@ struct goal2sat::imp {
m_ext->add_at_least(v2, lits, lits.size() - k.get_unsigned()); m_ext->add_at_least(v2, lits, lits.size() - k.get_unsigned());
if (root) { if (root && !sign) {
m_result_stack.reset(); m_result_stack.reset();
} }
else { else {
@ -585,7 +586,7 @@ struct goal2sat::imp {
mk_clause(~l1, ~l2, l); mk_clause(~l1, ~l2, l);
m_result_stack.shrink(m_result_stack.size() - t->get_num_args()); m_result_stack.shrink(m_result_stack.size() - t->get_num_args());
m_result_stack.push_back(sign ? ~l : l); m_result_stack.push_back(sign ? ~l : l);
if (root) mk_clause(~l);
} }
} }

15
src/tactic/arith/lia2card_tactic.cpp
View file

@ -103,21 +103,6 @@ class lia2card_tactic : public tactic {
} }
TRACE("pbsum", tout << expr_ref(m.mk_app(f, sz, es), m) << " ==>\n" << result << "\n";); TRACE("pbsum", tout << expr_ref(m.mk_app(f, sz, es), m) << " ==>\n" << result << "\n";);
#if 0
expr_ref vc(m);
vc = m.mk_not(m.mk_eq(m.mk_app(f, sz, es), result));
ast_pp_util pp(m);
pp.collect(vc);
std::cout
<< "(push)\n"
<< "(echo \"" << result << "\")\n"
;
pp.display_decls(std::cout);
std::cout
<< "(assert " << vc << ")\n"
<< "(check-sat)\n"
<< "(pop)\n";
#endif
return BR_DONE; return BR_DONE;
} }