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

avoid big pivots

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2020-04-11 11:49:25 -07:00
parent 20d72e5d97
commit 38c73090d8
2 changed files with 60 additions and 55 deletions
Download patch file Download diff file Expand all files Collapse all files

18
src/math/lp/lp_primal_core_solver.h
View file

@ -280,8 +280,8 @@ public:
// a short row produces short infeasibility explanation and benefits at least one pivot operation // a short row produces short infeasibility explanation and benefits at least one pivot operation
int choice = -1; int choice = -1;
int nchoices = 0; int nchoices = 0;
unsigned num_of_non_free_basics = 1000000; unsigned prev_damage = UINT_MAX;
unsigned len = 100000000; unsigned len = UINT_MAX;
unsigned bj = this->m_basis[i]; unsigned bj = this->m_basis[i];
bool bj_needs_to_grow = needs_to_grow(bj); bool bj_needs_to_grow = needs_to_grow(bj);
for (unsigned k = 0; k < this->m_A.m_rows[i].size(); k++) { for (unsigned k = 0; k < this->m_A.m_rows[i].size(); k++) {
@ -296,14 +296,18 @@ public:
if (!monoid_can_increase(rc)) if (!monoid_can_increase(rc))
continue; continue;
} }
unsigned damage = get_number_of_basic_vars_that_might_become_inf(j); unsigned damage = numeric_traits<T>::is_big(rc.coeff())? prev_damage:
if (damage < num_of_non_free_basics) { get_number_of_basic_vars_that_might_become_inf(j);
num_of_non_free_basics = damage; if (damage < prev_damage) {
prev_damage = damage;
len = this->m_A.m_columns[j].size(); len = this->m_A.m_columns[j].size();
choice = k; choice = k;
nchoices = 1; nchoices = 1;
} else if (damage == num_of_non_free_basics && } else if (damage == prev_damage
this->m_A.m_columns[j].size() <= len && (this->m_settings.random_next() % (++nchoices))) { &&
this->m_A.m_columns[j].size() <= len
&&
(this->m_settings.random_next() % (++nchoices))) {
choice = k; choice = k;
len = this->m_A.m_columns[j].size(); len = this->m_A.m_columns[j].size();
} }

97
src/math/lp/numeric_pair.h
View file

@ -1,22 +1,22 @@
/*++ /*++
Copyright (c) 2017 Microsoft Corporation Copyright (c) 2017 Microsoft Corporation
Module Name: Module Name:
<name> <name>
Abstract: Abstract:
<abstract> <abstract>
Author: Author:
Lev Nachmanson (levnach) Lev Nachmanson (levnach)
Revision History: Revision History:
--*/ --*/
#pragma once #pragma once
#define lp_for_z3 #define lp_for_z3
#include <string> #include <string>
@ -27,14 +27,14 @@ Revision History:
#include "util/sstream.h" #include "util/sstream.h"
#include "util/z3_exception.h" #include "util/z3_exception.h"
#else #else
// include "util/numerics/mpq.h" // include "util/numerics/mpq.h"
// include "util/numerics/numeric_traits.h" // include "util/numerics/numeric_traits.h"
#endif #endif
namespace lp { namespace lp {
#ifdef lp_for_z3 // rename rationals #ifdef lp_for_z3 // rename rationals
typedef rational mpq; typedef rational mpq;
#else #else
typedef lp::mpq mpq; typedef lp::mpq mpq;
#endif #endif
@ -70,41 +70,42 @@ public:
template <> class numeric_traits<double> { template <> class numeric_traits<double> {
public: public:
static bool precise() { return false; } static bool precise() { return false; }
static double g_zero; static double g_zero;
static double const &zero() { return g_zero; } static double const &zero() { return g_zero; }
static double g_one; static double g_one;
static double const &one() { return g_one; } static double const &one() { return g_one; }
static bool is_zero(double v) { return v == 0.0; } static bool is_zero(double v) { return v == 0.0; }
static double const & get_double(double const & d) { return d;} static double const & get_double(double const & d) { return d;}
static double log(double const & d) { NOT_IMPLEMENTED_YET(); return d;} static double log(double const & d) { NOT_IMPLEMENTED_YET(); return d;}
static double from_string(std::string const & str) { return atof(str.c_str()); } static double from_string(std::string const & str) { return atof(str.c_str()); }
static bool is_pos(const double & d) {return d > 0.0;} static bool is_pos(const double & d) {return d > 0.0;}
static bool is_neg(const double & d) {return d < 0.0;} static bool is_neg(const double & d) {return d < 0.0;}
}; static bool is_big(const double & d) { return false; }
};
template<> template<>
class numeric_traits<rational> { class numeric_traits<rational> {
public: public:
static bool precise() { return true; } static bool precise() { return true; }
static rational const & zero() { return rational::zero(); } static rational const & zero() { return rational::zero(); }
static rational const & one() { return rational::one(); } static rational const & one() { return rational::one(); }
static bool is_zero(const rational & v) { return v.is_zero(); } static bool is_zero(const rational & v) { return v.is_zero(); }
static double get_double(const rational & d) { return d.get_double();} static double get_double(const rational & d) { return d.get_double();}
static rational log(rational const& r) { UNREACHABLE(); return r; } static rational log(rational const& r) { UNREACHABLE(); return r; }
static rational from_string(std::string const & str) { return rational(str.c_str()); } static rational from_string(std::string const & str) { return rational(str.c_str()); }
static bool is_pos(const rational & d) {return d.is_pos();} static bool is_pos(const rational & d) {return d.is_pos();}
static bool is_neg(const rational & d) {return d.is_neg();} static bool is_neg(const rational & d) {return d.is_neg();}
static bool is_int(const rational & d) {return d.is_int();} static bool is_int(const rational & d) {return d.is_int();}
static mpq ceil_ratio(const mpq & a, const mpq & b) { static bool is_big(const rational & d) {return d.is_big();}
return ceil(a / b); static mpq ceil_ratio(const mpq & a, const mpq & b) {
} return ceil(a / b);
static mpq floor_ratio(const mpq & a, const mpq & b) { }
return floor(a / b); static mpq floor_ratio(const mpq & a, const mpq & b) {
} return floor(a / b);
}
}; };
#endif #endif
template <typename X, typename Y> template <typename X, typename Y>
@ -295,7 +296,7 @@ numeric_pair<T> operator/(const numeric_pair<T> & r, const X & a) {
template <typename T> double get_double(const lp::numeric_pair<T> & ) { /* lp_unreachable(); */ return 0;} template <typename T> double get_double(const lp::numeric_pair<T> & ) { /* lp_unreachable(); */ return 0;}
template <typename T> template <typename T>
class numeric_traits<lp::numeric_pair<T>> { class numeric_traits<lp::numeric_pair<T>> {
public: public:
static bool precise() { return numeric_traits<T>::precise();} static bool precise() { return numeric_traits<T>::precise();}
static lp::numeric_pair<T> zero() { return lp::numeric_pair<T>(numeric_traits<T>::zero(), numeric_traits<T>::zero()); } static lp::numeric_pair<T> zero() { return lp::numeric_pair<T>(numeric_traits<T>::zero(), numeric_traits<T>::zero()); }
static bool is_zero(const lp::numeric_pair<T> & v) { return numeric_traits<T>::is_zero(v.x) && numeric_traits<T>::is_zero(v.y); } static bool is_zero(const lp::numeric_pair<T> & v) { return numeric_traits<T>::is_zero(v.x) && numeric_traits<T>::is_zero(v.y); }