mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 01:24:08 +00:00
Code Activity

#6523

Browse source 
regressions from changes inside math/lp/int_solver
This commit is contained in:
Nikolaj Bjorner 2023-11-13 14:28:03 -08:00
parent 3de5af3cb0
commit 8a4e857294
2 changed files with 16 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

19
src/math/lp/gomory.cpp
View file

@ -139,7 +139,7 @@ class create_cut {
std::ostream& dump_coeff_val(std::ostream & out, const mpq & a) const {
if (a.is_int())
out << a;
else if ( a >= zero_of_type<mpq>())
else if (a >= zero_of_type<mpq>())
out << "(/ " << numerator(a) << " " << denominator(a) << ")";
else
out << "(- (/ " << numerator(-a) << " " << denominator(-a) << "))";
@ -148,9 +148,7 @@ class create_cut {
template <typename T>
void dump_coeff(std::ostream & out, const T& c) const {
out << "(* ";
dump_coeff_val(out, c.coeff());
out << " " << var_name(c.column().index()) << ")";
dump_coeff_val(out << "(* ", c.coeff()) << " " << var_name(c.column().index()) << ")";
}
std::ostream& dump_row_coefficients(std::ostream & out) const {
@ -178,9 +176,8 @@ class create_cut {
dump_declaration(out, p.var());
for (lar_term::ival p : m_t) {
auto t = lia.lra.column2tv(p.column());
if (t.is_term()) {
dump_declaration(out, t.id());
}
if (t.is_term())
dump_declaration(out, t.id());
}
}
@ -352,6 +349,14 @@ public:
}
m_k *= m_lcm_den;
}
// ax + by >= k
// b > 0, c1 <= y <= c2
// ax + b*c2 >= ax + by >= k
// =>
// ax >= k - by >= k - b*c1
// b < 0
// ax + b*c1 >= ax + by >= k
//
unsigned j = 0, i = 0;
for (auto & [c, v] : pol) {
if (lia.is_fixed(v)) {

4
src/sat/smt/arith_solver.cpp
View file

@ -323,6 +323,10 @@ namespace arith {
return false;
theory_var uv = lp().local_to_external(u); // variables that are returned should have external representations
theory_var vv = lp().local_to_external(v); // so maybe better to have them already transformed to external form
if (uv == euf::null_theory_var)
return false;
if (vv == euf::null_theory_var)
return false;
if (is_equal(uv, vv))
return false;
enode* n1 = var2enode(uv);