mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

more dead code

Browse source
This commit is contained in:
Lev Nachmanson 2023-03-07 16:58:49 -08:00
parent c8c0a00190
commit c6be67bf3b
1 changed files with 0 additions and 75 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -112,18 +112,6 @@ struct convert_struct {
}; };
template <>
struct convert_struct<double, mpq> {
static double convert(const mpq & q) {return q.get_double();}
};
template <>
struct convert_struct<mpq, unsigned> {
static mpq convert(unsigned q) {return mpq(q);}
};
template <typename T> template <typename T>
struct numeric_pair { struct numeric_pair {
@ -308,71 +296,8 @@ public:
} }
}; };
template <>
struct convert_struct<double, numeric_pair<double>> {
static double convert(const numeric_pair<double> & q) {return q.x;}
};
typedef numeric_pair<mpq> impq; typedef numeric_pair<mpq> impq;
template <typename T>
struct convert_struct<numeric_pair<T>, double> {
static numeric_pair<T> convert(const double & q) {
return numeric_pair<T>(convert_struct<T, double>::convert(q), numeric_traits<T>::zero());
}
static bool below_bound_numeric(const numeric_pair<T> &, const numeric_pair<T> &, const double &) {
// lp_unreachable();
return false;
}
static bool above_bound_numeric(const numeric_pair<T> &, const numeric_pair<T> &, const double &) {
// lp_unreachable();
return false;
}
};
template <>
struct convert_struct<numeric_pair<double>, double> {
static numeric_pair<double> convert(const double & q) {
return numeric_pair<double>(q, 0.0);
}
static int compare_on_coord(const double & x, const double & bound, const double eps) {
if (bound == 0) return (x < - eps)? -1: (x > eps? 1 : 0); // it is an important special case
double relative = (bound > 0)? - eps: eps;
return (x < bound * (1.0 + relative) - eps)? -1 : ((x > bound * (1.0 - relative) + eps)? 1 : 0);
}
static bool below_bound_numeric(const numeric_pair<double> & x, const numeric_pair<double> & bound, const double & eps) {
int r = compare_on_coord(x.x, bound.x, eps);
if (r == 1) return false;
if (r == -1) return true;
// the first coordinates are almost the same
return compare_on_coord(x.y, bound.y, eps) == -1;
}
static bool above_bound_numeric(const numeric_pair<double> & x, const numeric_pair<double> & bound, const double & eps) {
int r = compare_on_coord(x.x, bound.x, eps);
if (r == -1) return false;
if (r == 1) return true;
// the first coordinates are almost the same
return compare_on_coord(x.y, bound.y, eps) == 1;
}
};
template <>
struct convert_struct<double, double> {
static double convert(const double & y){ return y;}
static bool below_bound_numeric(const double & x, const double & bound, const double & eps) {
if (bound == 0) return x < - eps;
double relative = (bound > 0)? - eps: eps;
return x < bound * (1.0 + relative) - eps;
}
static bool above_bound_numeric(const double & x, const double & bound, const double & eps) {
if (bound == 0) return x > eps;
double relative = (bound > 0)? eps: - eps;
return x > bound * (1.0 + relative) + eps;
}
};
template <typename X> bool below_bound_numeric(const X & x, const X & bound, const double& eps) { return convert_struct<X, double>::below_bound_numeric(x, bound, eps);} template <typename X> bool below_bound_numeric(const X & x, const X & bound, const double& eps) { return convert_struct<X, double>::below_bound_numeric(x, bound, eps);}
template <typename X> bool above_bound_numeric(const X & x, const X & bound, const double& eps) { return convert_struct<X, double>::above_bound_numeric(x, bound, eps);} template <typename X> bool above_bound_numeric(const X & x, const X & bound, const double& eps) { return convert_struct<X, double>::above_bound_numeric(x, bound, eps);}
template <typename T> T floor(const numeric_pair<T> & r) { template <typename T> T floor(const numeric_pair<T> & r) {