use crate::{Rational, RationalStorageClass, Real, RealSign, ZeroKnowledge};
#[derive(Clone, Copy, Debug, Eq, PartialEq)]
pub enum RealExactSetDenominatorKind {
Dyadic,
SharedNonDyadic,
}
#[derive(Clone, Copy, Debug, Eq, PartialEq)]
pub enum RealExactSetDyadicExponentClass {
Integer,
Small,
Medium,
Large,
}
#[derive(Clone, Copy, Debug, Eq, PartialEq)]
pub enum RealExactSetSignPattern {
Empty,
AllZero,
AllPositive,
AllNegative,
MixedKnown,
Unknown,
}
#[derive(Clone, Copy, Debug, Eq, PartialEq)]
pub struct RealExactSetFacts {
pub len: usize,
pub exact_rational_count: usize,
pub exact_integer_count: usize,
pub exact_power_of_two_count: usize,
pub known_one_count: usize,
pub known_minus_one_count: usize,
pub all_exact_rational: bool,
pub all_dyadic: bool,
pub shared_denominator: bool,
pub max_rational_storage: Option<RationalStorageClass>,
pub max_dyadic_exponent_class: Option<RealExactSetDyadicExponentClass>,
pub known_zero_count: usize,
pub known_nonzero_count: usize,
pub unknown_zero_count: usize,
pub known_positive_count: usize,
pub known_negative_count: usize,
}
impl RealExactSetFacts {
pub fn from_reals<'a, I>(values: I) -> Self
where
I: IntoIterator<Item = &'a Real>,
{
crate::trace_dispatch!("real", "exact_set_facts", "scan");
let mut len = 0_usize;
let mut exact_rational_count = 0_usize;
let mut exact_integer_count = 0_usize;
let mut exact_power_of_two_count = 0_usize;
let mut known_one_count = 0_usize;
let mut known_minus_one_count = 0_usize;
let mut all_dyadic = true;
let mut shared_denominator = true;
let mut first_rational = None::<&Rational>;
let mut max_rational_storage = None::<RationalStorageClass>;
let mut max_dyadic_shift = Some(0_u64);
let mut known_zero_count = 0_usize;
let mut known_nonzero_count = 0_usize;
let mut unknown_zero_count = 0_usize;
let mut known_positive_count = 0_usize;
let mut known_negative_count = 0_usize;
for value in values {
len += 1;
let structural = value.structural_facts();
match structural.zero {
ZeroKnowledge::Zero => known_zero_count += 1,
ZeroKnowledge::NonZero => known_nonzero_count += 1,
ZeroKnowledge::Unknown => unknown_zero_count += 1,
}
match structural.sign {
Some(RealSign::Positive) => known_positive_count += 1,
Some(RealSign::Negative) => known_negative_count += 1,
Some(RealSign::Zero) | None => {}
}
let Some(rational) = value.exact_rational_ref() else {
all_dyadic = false;
shared_denominator = false;
max_dyadic_shift = None;
continue;
};
exact_rational_count += 1;
let rational_facts = rational.detailed_rational_facts();
if rational_facts.exact_integer {
exact_integer_count += 1;
}
if rational_facts.power_of_two {
exact_power_of_two_count += 1;
}
if rational.is_one() {
known_one_count += 1;
}
if rational.is_minus_one() {
known_minus_one_count += 1;
}
let dyadic_shift = rational.dyadic_denominator_shift();
all_dyadic &= dyadic_shift.is_some();
max_dyadic_shift = match (max_dyadic_shift, dyadic_shift) {
(Some(current), Some(next)) => Some(current.max(next)),
_ => None,
};
max_rational_storage = max_storage_class(max_rational_storage, rational_facts.storage);
if let Some(first) = first_rational {
shared_denominator &= first.same_denominator(rational);
} else {
first_rational = Some(rational);
}
}
let all_exact_rational = len != 0 && exact_rational_count == len;
Self {
len,
exact_rational_count,
exact_integer_count,
exact_power_of_two_count,
known_one_count,
known_minus_one_count,
all_exact_rational,
all_dyadic: all_exact_rational && all_dyadic,
shared_denominator: all_exact_rational && shared_denominator,
max_rational_storage,
max_dyadic_exponent_class: (all_exact_rational && all_dyadic)
.then(|| dyadic_exponent_class(max_dyadic_shift.unwrap_or(0))),
known_zero_count,
known_nonzero_count,
unknown_zero_count,
known_positive_count,
known_negative_count,
}
}
#[inline]
pub fn is_nonempty_exact_rational(self) -> bool {
self.len != 0 && self.all_exact_rational
}
#[inline]
pub fn has_dyadic_schedule(self) -> bool {
self.is_nonempty_exact_rational() && self.all_dyadic
}
#[inline]
pub fn has_integer_grid_schedule(self) -> bool {
self.is_nonempty_exact_rational() && self.exact_integer_count == self.len
}
#[inline]
pub fn has_signed_unit_schedule(self) -> bool {
self.len != 0
&& self.unknown_zero_count == 0
&& self.known_zero_count + self.known_one_count + self.known_minus_one_count == self.len
}
#[inline]
pub fn has_shared_denominator_schedule(self) -> bool {
self.is_nonempty_exact_rational() && self.shared_denominator
}
#[inline]
pub fn shared_denominator_kind(self) -> Option<RealExactSetDenominatorKind> {
if !self.has_shared_denominator_schedule() {
return None;
}
if self.all_dyadic {
Some(RealExactSetDenominatorKind::Dyadic)
} else {
Some(RealExactSetDenominatorKind::SharedNonDyadic)
}
}
#[inline]
pub fn sign_pattern(self) -> RealExactSetSignPattern {
if self.len == 0 {
return RealExactSetSignPattern::Empty;
}
if self.unknown_zero_count != 0
|| self.known_zero_count + self.known_positive_count + self.known_negative_count
!= self.len
{
return RealExactSetSignPattern::Unknown;
}
if self.known_zero_count == self.len {
RealExactSetSignPattern::AllZero
} else if self.known_positive_count == self.len {
RealExactSetSignPattern::AllPositive
} else if self.known_negative_count == self.len {
RealExactSetSignPattern::AllNegative
} else {
RealExactSetSignPattern::MixedKnown
}
}
}
fn max_storage_class(
current: Option<RationalStorageClass>,
next: RationalStorageClass,
) -> Option<RationalStorageClass> {
Some(match current {
Some(current) if storage_rank(current) >= storage_rank(next) => current,
_ => next,
})
}
fn storage_rank(storage: RationalStorageClass) -> u8 {
match storage {
RationalStorageClass::Zero => 0,
RationalStorageClass::WordSized => 1,
RationalStorageClass::MultiLimb => 2,
RationalStorageClass::VeryLarge => 3,
}
}
fn dyadic_exponent_class(shift: u64) -> RealExactSetDyadicExponentClass {
match shift {
0 => RealExactSetDyadicExponentClass::Integer,
1..=32 => RealExactSetDyadicExponentClass::Small,
33..=128 => RealExactSetDyadicExponentClass::Medium,
_ => RealExactSetDyadicExponentClass::Large,
}
}