mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-24 14:53:40 +00:00
Code Activity

ensure pb on lex > 1 constraints

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2015-08-08 14:10:11 +02:00
parent 8505ca843b
commit aa431bb67f
2 changed files with 20 additions and 18 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/opt/opt_context.cpp
View file

@ -482,7 +482,8 @@ namespace opt {
m_opt_solver->set_logic(m_logic); m_opt_solver->set_logic(m_logic);
m_solver = m_opt_solver.get(); m_solver = m_opt_solver.get();
} }
if (opt_params(m_params).priority() == symbol("pareto")) { if (opt_params(m_params).priority() == symbol("pareto") ||
(opt_params(m_params).priority() == symbol("lex") && m_objectives.size() > 1)) {
m_opt_solver->ensure_pb(); m_opt_solver->ensure_pb();
} }
} }

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

@ -34,32 +34,33 @@ class lia2card_tactic : public tactic {
vector<rational> coeffs; vector<rational> coeffs;
rational coeff; rational coeff;
bool is_le(expr* x, expr* y, expr_ref& result) {
if (t.get_pb_sum(x, rational::one(), args, coeffs, coeff) &&
t.get_pb_sum(y, -rational::one(), args, coeffs, coeff)) {
result = t.mk_le(coeffs.size(), coeffs.c_ptr(), args.c_ptr(), -coeff);
return true;
}
else {
return false;
}
}
br_status mk_app_core(func_decl* f, unsigned sz, expr*const* es, expr_ref& result) { br_status mk_app_core(func_decl* f, unsigned sz, expr*const* es, expr_ref& result) {
args.reset(); args.reset();
coeffs.reset(); coeffs.reset();
coeff.reset(); coeff.reset();
if (is_decl_of(f, a.get_family_id(), OP_LE) && if (is_decl_of(f, a.get_family_id(), OP_LE) && is_le(es[0], es[1], result)) {
t.get_pb_sum(es[0], rational::one(), args, coeffs, coeff) &&
t.get_pb_sum(es[1], -rational::one(), args, coeffs, coeff)) {
result = t.mk_le(coeffs.size(), coeffs.c_ptr(), args.c_ptr(), -coeff);
return BR_DONE; return BR_DONE;
} }
if (is_decl_of(f, a.get_family_id(), OP_GE) && if (is_decl_of(f, a.get_family_id(), OP_GE) && is_le(es[1], es[0], result)) {
t.get_pb_sum(es[1], rational::one(), args, coeffs, coeff) &&
t.get_pb_sum(es[0], -rational::one(), args, coeffs, coeff)) {
result = t.mk_le(coeffs.size(), coeffs.c_ptr(), args.c_ptr(), -coeff);
return BR_DONE; return BR_DONE;
} }
if (is_decl_of(f, a.get_family_id(), OP_LT) && if (is_decl_of(f, a.get_family_id(), OP_LT) && is_le(es[1], es[0], result)) {
t.get_pb_sum(es[1], rational::one(), args, coeffs, coeff) && result = m.mk_not(result);
t.get_pb_sum(es[0], -rational::one(), args, coeffs, coeff)) {
result = m.mk_not(t.mk_le(coeffs.size(), coeffs.c_ptr(), args.c_ptr(), -coeff));
return BR_DONE; return BR_DONE;
} }
if (is_decl_of(f, a.get_family_id(), OP_GT) && if (is_decl_of(f, a.get_family_id(), OP_GT) && is_le(es[0], es[1], result)) {
t.get_pb_sum(es[0], rational::one(), args, coeffs, coeff) && result = m.mk_not(result);
t.get_pb_sum(es[1], -rational::one(), args, coeffs, coeff)) {
result = m.mk_not(t.mk_le(coeffs.size(), coeffs.c_ptr(), args.c_ptr(), -coeff));
return BR_DONE; return BR_DONE;
} }
if (m.is_eq(f) && if (m.is_eq(f) &&