mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
fix bugs exposed by testSolver
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
5566965a5a
commit
97b2fc9ee7
|
@ -419,7 +419,7 @@ namespace opt {
|
|||
for (unsigned i = 0; i < m_objectives.size(); ++i) {
|
||||
objective const& obj = m_objectives[i];
|
||||
display_objective(out, obj);
|
||||
out << get_upper(i) << "\n";
|
||||
out << "|-> " << get_upper(i) << "\n";
|
||||
}
|
||||
}
|
||||
|
||||
|
@ -427,7 +427,7 @@ namespace opt {
|
|||
for (unsigned i = 0; i < m_objectives.size(); ++i) {
|
||||
objective const& obj = m_objectives[i];
|
||||
display_objective(out, obj);
|
||||
out << " [" << get_lower(i) << ":" << get_upper(i) << "]\n";
|
||||
out << " |-> [" << get_lower(i) << ":" << get_upper(i) << "]\n";
|
||||
}
|
||||
}
|
||||
|
||||
|
@ -496,13 +496,25 @@ namespace opt {
|
|||
expr_ref_vector args(m);
|
||||
arith_util a(m);
|
||||
if (!inf.is_zero()) {
|
||||
args.push_back(a.mk_mul(a.mk_numeral(inf, inf.is_int()), m.mk_const(symbol("oo"), a.mk_int())));
|
||||
expr* oo = m.mk_const(symbol("oo"), a.mk_int());
|
||||
if (inf.is_one()) {
|
||||
args.push_back(oo);
|
||||
}
|
||||
else {
|
||||
args.push_back(a.mk_mul(a.mk_numeral(inf, inf.is_int()), oo));
|
||||
}
|
||||
}
|
||||
if (!r.is_zero()) {
|
||||
args.push_back(a.mk_numeral(r, r.is_int()));
|
||||
}
|
||||
if (!eps.is_zero()) {
|
||||
args.push_back(a.mk_mul(a.mk_numeral(eps, eps.is_int()), m.mk_const(symbol("epsilon"), a.mk_int())));
|
||||
expr* ep = m.mk_const(symbol("epsilon"), a.mk_int());
|
||||
if (eps.is_one()) {
|
||||
args.push_back(ep);
|
||||
}
|
||||
else {
|
||||
args.push_back(a.mk_mul(a.mk_numeral(eps, eps.is_int()), ep));
|
||||
}
|
||||
}
|
||||
switch(args.size()) {
|
||||
case 0: return expr_ref(a.mk_numeral(rational(0), true), m);
|
||||
|
|
|
@ -79,6 +79,12 @@ namespace opt {
|
|||
if (m_cancel || is_sat == l_undef) {
|
||||
return l_undef;
|
||||
}
|
||||
|
||||
// set the solution tight.
|
||||
for (unsigned i = 0; i < m_lower.size(); ++i) {
|
||||
m_upper[i] = m_lower[i];
|
||||
}
|
||||
|
||||
return l_true;
|
||||
}
|
||||
|
||||
|
@ -102,6 +108,12 @@ namespace opt {
|
|||
if (m_cancel || is_sat == l_undef) {
|
||||
return l_undef;
|
||||
}
|
||||
|
||||
// set the solution tight.
|
||||
for (unsigned i = 0; i < m_lower.size(); ++i) {
|
||||
m_upper[i] = m_lower[i];
|
||||
}
|
||||
|
||||
return l_true;
|
||||
}
|
||||
|
||||
|
|
|
@ -163,6 +163,9 @@ public:
|
|||
}
|
||||
|
||||
expr* mk_le(unsigned sz, rational const* weights, expr* const* args, rational const& w) {
|
||||
if (sz == 0) {
|
||||
return w.is_neg()?m.mk_false():m.mk_true();
|
||||
}
|
||||
if (sz == 1 && weights[0].is_one() && w >= rational::one()) {
|
||||
return m.mk_true();
|
||||
}
|
||||
|
@ -173,6 +176,9 @@ public:
|
|||
}
|
||||
|
||||
expr* mk_ge(unsigned sz, rational const* weights, expr* const* args, rational const& w) {
|
||||
if (sz == 0) {
|
||||
return w.is_pos()?m.mk_false():m.mk_true();
|
||||
}
|
||||
if (sz == 1 && weights[0].is_one() && w.is_one()) {
|
||||
return args[0];
|
||||
}
|
||||
|
|
Loading…
Reference in a new issue