Coverage for datesat / core.py: 59.2%
151 statements
« prev ^ index » next coverage.py v7.13.4, created at 2026-02-10 23:47 +0000
1"""
2Core Date and Period classes for DateSAT.
4These classes represent the basic data structures used by all approaches.
5The difference between approaches is in how these are converted to Z3 constraints,
6not in the data representation itself.
7"""
9import warnings
10from datetime import date, timedelta
11from dateutil.relativedelta import relativedelta
12from z3 import *
15class Date:
16 """Date class with year/month/day representation."""
18 def __init__(self, year: int, month: int, day: int, bounded: bool = True):
19 """Initialize a Date with year, month, day components.
21 Args:
22 year: Year component
23 month: Month component
24 day: Day component
25 bounded: If True (default), validates that the date is within the allowed
26 range [1900-03-01 to 2100-02-28]. If False, only validates
27 calendar correctness but not range.
28 """
29 self._year = year
30 self._month = month
31 self._day = day
32 self._bounded = bounded
33 self._validate()
35 @property
36 def year(self) -> int:
37 """Get the year component."""
38 return self._year
40 @property
41 def month(self) -> int:
42 """Get the month component."""
43 return self._month
45 @property
46 def day(self) -> int:
47 """Get the day component."""
48 return self._day
50 def _validate(self) -> None:
51 """Validate that the date components are valid."""
52 # Validate input format first: all components must be integers (no bools allowed)
53 date_components = (self._year, self._month, self._day)
54 if not all(isinstance(v, int) and not isinstance(v, bool) for v in date_components):
55 raise ValueError(
56 "Invalid date format: year, month, and day must be integers"
57 )
59 # First, validate calendar correctness
60 try:
61 date(self._year, self._month, self._day)
62 except ValueError as e:
63 raise ValueError(
64 f"Invalid date: {self._year}-{self._month:02d}-{self._day:02d}"
65 ) from e
67 # Next, enforce allowed window [1900-03-01 - 2100-02-28] only if bounded
68 if self._bounded: 68 ↛ exitline 68 didn't return from function '_validate' because the condition on line 68 was always true
69 min_allowed = (1900, 3, 1)
70 max_allowed = (2100, 2, 28)
72 if date_components < min_allowed or date_components > max_allowed:
73 raise ValueError(
74 f"Date outside allowed range: {self._year}-{self._month:02d}-{self._day:02d} (allowed [1900-03-01..2100-02-28])"
75 )
77 def __str__(self) -> str:
78 """Return a string representation of the Date."""
79 return f"Date({self.year}, {self.month}, {self.day})"
81 def __hash__(self) -> int:
82 """Return hash value for Date object."""
83 return hash((self.year, self.month, self.day))
85 def __eq__(self, other: "Date") -> bool:
86 """Check if two dates are equal."""
87 if isinstance(other, Date): 87 ↛ 95line 87 didn't jump to line 95 because the condition on line 87 was always true
88 return (
89 self.year == other.year
90 and self.month == other.month
91 and self.day == other.day
92 )
93 # Allow DateVar implementations to handle reflected comparison
94 # Includes: symbolic DateVar, EvalDateVar (validation), EnumerationDateVar (baseline)
95 other_cls = other.__class__
96 other_name = other_cls.__name__
97 if (other_name in ("DateVar", "EvalDateVar", "EnumerationDateVar") or
98 (other_name == "DateVar" and getattr(other_cls, "__module__", "").startswith("datesat.symbolic"))):
99 return NotImplemented
100 raise TypeError(f"Cannot compare Date with {type(other)}")
102 def __ne__(self, other: "Date") -> bool:
103 """Check if two dates are not equal."""
104 if isinstance(other, Date):
105 return not self.__eq__(other)
106 # Allow DateVar implementations to handle reflected comparison
107 other_cls = other.__class__
108 other_name = other_cls.__name__
109 if (other_name in ("DateVar", "EvalDateVar", "EnumerationDateVar") or 109 ↛ 111line 109 didn't jump to line 111 because the condition on line 109 was never true
110 (other_name == "DateVar" and getattr(other_cls, "__module__", "").startswith("datesat.symbolic"))):
111 return NotImplemented
112 raise TypeError(f"Cannot compare Date with {type(other)}")
114 def __lt__(self, other: "Date"):
115 """Check if this date is less than another."""
116 if isinstance(other, Date):
117 return self.to_python_date() < other.to_python_date()
118 # Allow DateVar implementations to handle reflected comparison
119 other_cls = other.__class__
120 other_name = other_cls.__name__
121 if (other_name in ("DateVar", "EvalDateVar", "EnumerationDateVar") or
122 (other_name == "DateVar" and getattr(other_cls, "__module__", "").startswith("datesat.symbolic"))):
123 return NotImplemented
124 raise TypeError(f"Cannot compare Date with {type(other)}")
126 def __le__(self, other: "Date"):
127 """Check if this date is less than or equal to another."""
128 if isinstance(other, Date):
129 return self.to_python_date() <= other.to_python_date()
130 # Allow DateVar implementations to handle reflected comparison
131 other_cls = other.__class__
132 other_name = other_cls.__name__
133 if (other_name in ("DateVar", "EvalDateVar", "EnumerationDateVar") or
134 (other_name == "DateVar" and getattr(other_cls, "__module__", "").startswith("datesat.symbolic"))):
135 return NotImplemented
136 raise TypeError(f"Cannot compare Date with {type(other)}")
138 def __gt__(self, other: "Date"):
139 """Check if this date is greater than another."""
140 if isinstance(other, Date):
141 return self.to_python_date() > other.to_python_date()
142 # Allow DateVar implementations to handle reflected comparison
143 other_cls = other.__class__
144 other_name = other_cls.__name__
145 if (other_name in ("DateVar", "EvalDateVar", "EnumerationDateVar") or
146 (other_name == "DateVar" and getattr(other_cls, "__module__", "").startswith("datesat.symbolic"))):
147 return NotImplemented
148 raise TypeError(f"Cannot compare Date with {type(other)}")
150 def __ge__(self, other: "Date"):
151 """Check if this date is greater than or equal to another."""
152 if isinstance(other, Date):
153 return self.to_python_date() >= other.to_python_date()
154 # Allow DateVar implementations to handle reflected comparison
155 other_cls = other.__class__
156 other_name = other_cls.__name__
157 if (other_name in ("DateVar", "EvalDateVar", "EnumerationDateVar") or
158 (other_name == "DateVar" and getattr(other_cls, "__module__", "").startswith("datesat.symbolic"))):
159 return NotImplemented
160 raise TypeError(f"Cannot compare Date with {type(other)}")
162 def to_python_date(self) -> date:
163 """Convert to Python date object."""
164 return date(self.year, self.month, self.day)
166 @classmethod
167 def from_python_date(cls, d: date) -> "Date":
168 """Create Date from Python date object."""
169 return cls(d.year, d.month, d.day)
171 def __add__(self, other: "Period"):
172 """
173 Date + Period using Python's datetime library with relativedelta.
174 This provides the same semantics as the symbolic DateVar operations.
176 Intermediate dates must be within the allowed range [1900-03-01, 2100-02-28].
177 If the result is outside this range, raises ValueError to ensure consistency
178 with symbolic DateVar bounds enforcement (which makes constraints UNSAT).
179 This error should be caught during constraint building and converted to an UNSAT constraint.
180 """
181 if not isinstance(other, Period):
182 raise TypeError(f"Cannot add {type(other)} to Date")
184 # Convert to Python date and use relativedelta for years/months/days
185 py_date = self.to_python_date()
186 result_date = py_date + relativedelta(
187 years=other.years, months=other.months, days=other.days
188 )
190 # Try to convert back to Date (will validate the result and enforce bounds)
191 # This ensures intermediate dates are bounded, consistent with symbolic DateVars
192 # If out of bounds, ValueError is raised and should be caught during constraint building
193 # to convert to an UNSAT constraint
194 return Date.from_python_date(result_date)
196 def __sub__(self, other: "Period"):
197 """
198 Date - Period implemented as Date + (-Period).
200 Intermediate dates must be within the allowed range [1900-03-01, 2100-02-28].
201 If the result is outside this range, raises ValueError to ensure consistency
202 with symbolic DateVar bounds enforcement (which makes constraints UNSAT).
203 """
204 if not isinstance(other, Period):
205 raise TypeError(f"Cannot subtract {type(other)} from Date")
207 neg_period = Period(-other.years, -other.months, -other.days)
208 return self.__add__(neg_period)
211class Period:
212 """Period class for representing time periods."""
214 # Period bounds based on date range [1900-03-01 to 2100-02-28]
215 # These match the allowed date range to ensure periods are semantically valid
216 MAX_PERIOD_DAYS = 73048 # abs(EPOCH_DAYS_MAX - EPOCH_DAYS_MIN) = abs(36523 - (-36525))
217 MAX_PERIOD_YEARS = 200 # YEAR_MAX - YEAR_MIN = 2100 - 1900
218 MAX_PERIOD_MONTHS = 2400 # MAX_PERIOD_YEARS * 12 = 200 * 12
220 def __init__(self, years: int, months: int, days: int):
221 """Initialize a Period with years, months, days components."""
222 # Validate input format: exactly three integer components (no bools allowed)
223 period_components = (years, months, days)
224 if not all(isinstance(v, int) and not isinstance(v, bool) for v in period_components):
225 raise ValueError(
226 "Invalid Period format: years, months, and days must be integers"
227 )
229 # Validate period bounds: ensure periods fit within the allowed date range
230 if abs(years) > self.MAX_PERIOD_YEARS:
231 raise ValueError(
232 f"Period years out of range: {years} (max ±{self.MAX_PERIOD_YEARS})"
233 )
234 if abs(months) > self.MAX_PERIOD_MONTHS:
235 raise ValueError(
236 f"Period months out of range: {months} (max ±{self.MAX_PERIOD_MONTHS})"
237 )
238 if abs(days) > self.MAX_PERIOD_DAYS:
239 raise ValueError(
240 f"Period days out of range: {days} (max ±{self.MAX_PERIOD_DAYS})"
241 )
243 self._years = years
244 self._months = months
245 self._days = days
247 @property
248 def years(self) -> int:
249 """Get the years component."""
250 return self._years
252 @property
253 def months(self) -> int:
254 """Get the months component."""
255 return self._months
257 @property
258 def days(self) -> int:
259 """Get the days component."""
260 return self._days
262 def __str__(self) -> str:
263 return f"Period({self.years}, {self.months}, {self.days})"
265 def __hash__(self) -> int:
266 """Return hash value for Period object."""
267 return hash((self.years, self.months, self.days))
269 def __eq__(self, other: "Period") -> bool:
270 raise TypeError(f"Cannot compare Period with {type(other)}")
272 def __ne__(self, other: "Period") -> bool:
273 raise TypeError(f"Cannot compare Period with {type(other)}")
275 def __mul__(self, other: int) -> "Period":
276 """Support Period * Int multiplication."""
277 if isinstance(other, int): 277 ↛ 284line 277 didn't jump to line 284 because the condition on line 277 was always true
278 return Period(
279 self.years * other,
280 self.months * other,
281 self.days * other
282 )
283 else:
284 raise TypeError(f"Cannot multiply Period with {type(other)}")
286 def __rmul__(self, other: int) -> "Period":
287 """Support Int * Period multiplication."""
288 if isinstance(other, int):
289 return self.__mul__(other)
290 else:
291 raise TypeError(f"Cannot multiply Period with {type(other)}")
293 def __add__(self, other: "Period") -> "Period":
294 """Support Period + Period addition."""
295 if isinstance(other, Period): 295 ↛ 303line 295 didn't jump to line 303 because the condition on line 295 was always true
296 return Period(
297 self.years + other.years,
298 self.months + other.months,
299 self.days + other.days
300 )
301 else:
302 # Delegate to the right operand's __radd__ method
303 return NotImplemented
305 def __sub__(self, other: "Period") -> "Period":
306 """Support Period - Period subtraction."""
307 if isinstance(other, Period):
308 return Period(
309 self.years - other.years,
310 self.months - other.months,
311 self.days - other.days
312 )
313 else:
314 return NotImplemented