Coverage for datesat / symbolic_bitvector / bitwidths.py: 100.0%

1""" 

2Bit width constants for date components in Z3 bitvector operations. 

3 

4This module defines the minimum bit widths needed for various date components 

5to avoid unnecessary overhead while ensuring all valid values can be represented. 

6""" 

7LEGACY_BITS = 21 

8 

9# User-defined integer variable bit width 

10# Keep at 21 bits to match other date components, use bounds to prevent overflow 

11INT_VAR_BITS = LEGACY_BITS 

12 

13# Date component bit widths 

14YEAR_BITS = 12 # 4096 > 2100 

15MONTH_BITS = 12 # Because in the implementation, we multiply YEAR by 12 and add to MONTH 

16DAY_BITS = 20 # Because we add Period.days to the date, and Period.days can be large 

17 

18# Epoch-based bit widths 

19EPOCH_DAYS_BITS = 17 # -36525 to 36523 (~73k days) -> 2^17 = 131,072 > 73,000 

20 

21# Absolute ordinal bit widths (for representing absolute day numbers since 0001-01-01) 

22ORD_BITS = max(20, DAY_BITS) # 730179 needs 20 bits (2^19 < 730179 < 2^20) 

23 

24# Alpha-beta bit widths 

25ALPHA_BITS = 12 # (2100-1900)*12 + (2-3) = 2399 -> 2^12 = 4096 > 2399 

26BETA_BITS = 5 # 0-30 (day within month) -> 2^5 = 32 > 30 

27 

28# Validation ranges 

29YEAR_MIN = 1900 

30YEAR_MAX = 2100 

31MONTH_MIN = 1 

32MONTH_MAX = 12 

33DAY_MIN = 1 

34DAY_MAX = 31 

35 

36# Epoch bounds (2000-03-01 as epoch) 

37EPOCH_DAYS_MIN = -36525 # 1900-03-01 

38EPOCH_DAYS_MAX = 36523 # 2100-02-28 

39 

40# Months since epoch bounds 

41MONTHS_SINCE_EPOCH_MIN = (1900 - 2000) * 12 + (3 - 3) # -1200 

42MONTHS_SINCE_EPOCH_MAX = (2100 - 2000) * 12 + (2 - 3) # 2399 

43 

44# Beta bounds 

45BETA_MIN = 0 

46BETA_MAX = 30 # 0-30 for day within month (0-based)