@@ -81,6 +81,7 @@ pub(crate) enum Class {
8181 // representation small while still preserving a lightweight symbolic form.
8282 LnProduct ( Box < LnProductClass > ) , // Product of two logarithms, ordered by base
8383 Log10 ( Rational ) , // Rational > 1 and never a multiple of ten
84+ Log2 ( Rational ) , // Rational > 1 and never a power of two
8485 SinPi ( Rational ) , // 0 < Rational < 1/2 also never 1/6 or 1/4 or 1/3
8586 TanPi ( Rational ) , // 0 < Rational < 1/2 also never 1/6 or 1/4 or 1/3
8687 Irrational ,
@@ -135,6 +136,7 @@ impl PartialEq for Class {
135136 left. left == right. left && left. right == right. right
136137 }
137138 ( Log10 ( r) , Log10 ( s) ) => r == s,
139+ ( Log2 ( r) , Log2 ( s) ) => r == s,
138140 ( SinPi ( r) , SinPi ( s) ) => r == s,
139141 ( TanPi ( r) , TanPi ( s) ) => r == s,
140142 ( _, _) => false ,
@@ -541,6 +543,9 @@ impl Class {
541543 Log10 ( base) => {
542544 Self :: ln_computable ( base) . multiply ( Self :: ln_computable ( & rationals:: TEN ) . inverse ( ) )
543545 }
546+ Log2 ( base) => {
547+ Self :: ln_computable ( base) . multiply ( Self :: ln_computable ( & * rationals:: TWO ) . inverse ( ) )
548+ }
544549 SinPi ( rational) => {
545550 let argument =
546551 Computable :: multiply ( Computable :: pi ( ) , Computable :: rational ( rational. clone ( ) ) ) ;
@@ -1528,7 +1533,7 @@ impl Real {
15281533 Irrational => "scaled-computable" ,
15291534 Pi | PiPow ( _) | PiInv | PiExp ( _) | PiInvExp ( _) | PiSqrt ( _) | ConstProduct ( _)
15301535 | ConstOffset ( _) | ConstProductSqrt ( _) | Sqrt ( _) | Exp ( _) | Ln ( _) | LnAffine ( _)
1531- | LnProduct ( _) | Log10 ( _) | SinPi ( _) | TanPi ( _) => "symbolic-nonzero-scale" ,
1536+ | LnProduct ( _) | Log10 ( _) | Log2 ( _ ) | SinPi ( _) | TanPi ( _) => "symbolic-nonzero-scale" ,
15321537 }
15331538 ) ;
15341539
@@ -1537,7 +1542,7 @@ impl Real {
15371542 One => Some ( real_sign_from_num ( rational_sign) ) ,
15381543 Pi | PiPow ( _) | PiInv | PiExp ( _) | PiInvExp ( _) | PiSqrt ( _) | ConstProduct ( _)
15391544 | ConstOffset ( _) | ConstProductSqrt ( _) | Sqrt ( _) | Exp ( _) | Ln ( _) | LnAffine ( _)
1540- | LnProduct ( _) | Log10 ( _) | SinPi ( _) | TanPi ( _) => {
1545+ | LnProduct ( _) | Log10 ( _) | Log2 ( _ ) | SinPi ( _) | TanPi ( _) => {
15411546 // Exact symbolic classes are positive by construction, so the
15421547 // outer rational scale alone determines sign. Additive classes
15431548 // such as ConstOffset/LnAffine are admitted only when this
@@ -3295,6 +3300,61 @@ impl Real {
32953300 } )
32963301 }
32973302
3303+ /// The base 2 logarithm of this Real or Problem::NotANumber if this Real is not positive.
3304+ pub fn log2 ( self ) -> Result < Real , Problem > {
3305+ // Domain check uses structural sign first. Refinement-forced sign
3306+ // (`best_sign`) is reserved for the case where cheap inspection cannot
3307+ // decide; rejecting structurally known nonpositive inputs avoids
3308+ // ~2µs of computable work on the typical hot path.
3309+ match self . structural_facts ( ) . sign {
3310+ Some ( RealSign :: Positive ) => { }
3311+ Some ( RealSign :: Zero | RealSign :: Negative ) => {
3312+ crate :: trace_dispatch!( "real" , "log2" , "domain-not-positive" ) ;
3313+ return Err ( Problem :: NotANumber ) ;
3314+ }
3315+ None => {
3316+ if self . best_sign ( ) != Sign :: Plus {
3317+ crate :: trace_dispatch!( "real" , "log2" , "domain-not-positive" ) ;
3318+ return Err ( Problem :: NotANumber ) ;
3319+ }
3320+ }
3321+ }
3322+ if let One = & self . class {
3323+ return Self :: log2_rational ( self . rational ) ;
3324+ }
3325+ crate :: trace_dispatch!( "real" , "log2" , "ln-div-cached-ln2" ) ;
3326+ self . ln ( ) ? / constants:: scaled_ln ( 2 , 1 ) . unwrap ( )
3327+ }
3328+
3329+ fn log2_rational ( r : Rational ) -> Result < Real , Problem > {
3330+ match r. cmp_one_structural ( ) {
3331+ std:: cmp:: Ordering :: Less => {
3332+ let inv = r. inverse ( ) ?;
3333+ return Ok ( -Self :: log2_rational ( inv) ?) ;
3334+ }
3335+ std:: cmp:: Ordering :: Equal => return Ok ( Self :: zero ( ) ) ,
3336+ std:: cmp:: Ordering :: Greater => { }
3337+ }
3338+
3339+ if let Some ( n) = r. integer_magnitude ( )
3340+ && let Some ( log) = Self :: integer_log ( n, 2 )
3341+ {
3342+ crate :: trace_dispatch!( "real" , "log2" , "rational-power-of-two" ) ;
3343+ return Ok ( Self :: new ( Rational :: new ( log as i64 ) ) ) ;
3344+ }
3345+
3346+ crate :: trace_dispatch!( "real" , "log2" , "rational-log2-special-form" ) ;
3347+ let computable =
3348+ Class :: ln_computable ( & r) . multiply ( Class :: ln_computable ( & * rationals:: TWO ) . inverse ( ) ) ;
3349+ Ok ( Self {
3350+ rational : Rational :: one ( ) ,
3351+ class : Log2 ( r) ,
3352+ computable : Some ( computable) ,
3353+ signal : None ,
3354+ primitive_approx_cache : Cell :: new ( PrimitiveApproxCache :: Empty ) ,
3355+ } )
3356+ }
3357+
32983358 // Find Some(m) integral log with respect to this base or else None
32993359 // n should be positive (not zero) and base should be >= 2
33003360 fn integer_log ( n : & BigUint , base : u32 ) -> Option < u64 > {
@@ -4651,7 +4711,7 @@ fn structural_kind_for_class(class: &Class) -> StructuralKind {
46514711 Pi | PiPow ( _) | PiInv => StructuralKind :: PiLike ,
46524712 Exp ( _) | PiExp ( _) | PiInvExp ( _) => StructuralKind :: ExpLike ,
46534713 Sqrt ( _) | PiSqrt ( _) => StructuralKind :: SqrtLike ,
4654- Ln ( _) | LnAffine ( _) | LnProduct ( _) | Log10 ( _) => StructuralKind :: LogLike ,
4714+ Ln ( _) | LnAffine ( _) | LnProduct ( _) | Log10 ( _) | Log2 ( _ ) => StructuralKind :: LogLike ,
46554715 SinPi ( _) | TanPi ( _) => StructuralKind :: TrigExact ,
46564716 ConstProduct ( _) | ConstOffset ( _) | ConstProductSqrt ( _) => StructuralKind :: ProductConstant ,
46574717 Irrational => StructuralKind :: ComputableOpaque ,
@@ -4663,7 +4723,7 @@ fn symbolic_degree_for_class(class: &Class) -> ExpressionDegree {
46634723 Irrational => ExpressionDegree :: Unknown ,
46644724 One | Pi | PiPow ( _) | PiInv | PiExp ( _) | PiInvExp ( _) | PiSqrt ( _) | ConstProduct ( _)
46654725 | ConstOffset ( _) | ConstProductSqrt ( _) | Sqrt ( _) | Exp ( _) | Ln ( _) | LnAffine ( _)
4666- | LnProduct ( _) | Log10 ( _) | SinPi ( _) | TanPi ( _) => ExpressionDegree :: Constant ,
4726+ | LnProduct ( _) | Log10 ( _) | Log2 ( _ ) | SinPi ( _) | TanPi ( _) => ExpressionDegree :: Constant ,
46674727 }
46684728}
46694729
@@ -4679,7 +4739,7 @@ fn symbolic_dependencies_for_class(class: &Class) -> SymbolicDependencyMask {
46794739 ConstProductSqrt ( product) => pi_exp_dependency_mask ( product. pi_power , & product. exp_power )
46804740 . union ( SymbolicDependencyMask :: SQRT ) ,
46814741 Sqrt ( _) => SymbolicDependencyMask :: SQRT ,
4682- Ln ( _) | LnAffine ( _) | LnProduct ( _) | Log10 ( _) => SymbolicDependencyMask :: LOG ,
4742+ Ln ( _) | LnAffine ( _) | LnProduct ( _) | Log10 ( _) | Log2 ( _ ) => SymbolicDependencyMask :: LOG ,
46834743 SinPi ( _) | TanPi ( _) => SymbolicDependencyMask :: TRIG . union ( SymbolicDependencyMask :: PI ) ,
46844744 Irrational => SymbolicDependencyMask :: OPAQUE ,
46854745 }
@@ -4779,6 +4839,7 @@ impl fmt::Display for Real {
47794839 write ! ( f, " x ln({}) x ln({})" , product. left, product. right)
47804840 }
47814841 Log10 ( n) => write ! ( f, " x log10({})" , & n) ,
4842+ Log2 ( n) => write ! ( f, " x log2({})" , & n) ,
47824843 Sqrt ( n) => write ! ( f, " √({})" , & n) ,
47834844 SinPi ( n) => write ! ( f, " x sin({} x Pi)" , & n) ,
47844845 TanPi ( n) => write ! ( f, " x tan({} x Pi)" , & n) ,
@@ -6033,6 +6094,25 @@ impl<T: AsRef<Real>> Div<T> for &Real {
60336094 ..self . clone ( )
60346095 } ) ;
60356096 }
6097+ if s == * rationals:: TWO {
6098+ // Same rationale as the log10 fold: keep two-log quotients
6099+ // anchored on a single Log2 certificate.
6100+ let Ln ( r) = & self . class else {
6101+ unreachable ! ( ) ;
6102+ } ;
6103+ let rational = & self . rational / & other. rational ;
6104+ let ln2 = constants:: scaled_ln ( 2 , 1 ) . unwrap ( ) ;
6105+ let computable = self
6106+ . computable_clone ( )
6107+ . multiply ( ln2. computable_clone ( ) . inverse ( ) ) ;
6108+ return Ok ( Real {
6109+ rational,
6110+ class : Log2 ( r. clone ( ) ) ,
6111+ computable : Some ( computable) ,
6112+ signal : self . signal . clone ( ) ,
6113+ primitive_approx_cache : Cell :: new ( PrimitiveApproxCache :: Empty ) ,
6114+ } ) ;
6115+ }
60366116 } else {
60376117 unreachable ! ( ) ;
60386118 }
0 commit comments