Coverage for datesat / symbolic_bitvector / epoch_days_bv.py: 83.7%
196 statements
« prev ^ index » next coverage.py v7.13.4, created at 2026-02-10 23:47 +0000
1"""
2Epoch_days DateSAT implementation using epoch-based conversion.
4This module implements the epoch_days approach where dates are represented
5as days since an epoch, and period arithmetic is done using approximate
6day conversions.
7"""
9from datetime import date, timedelta
10from typing import List, Tuple, Union
12from z3 import (
13 And,
14 BitVec,
15 BitVecRef,
16 BitVecVal,
17 BoolRef,
18 CheckSatResult,
19 If,
20 ModelRef,
21 Not,
22 Optimize,
23 Solver,
24 sat,
25 unsat,
26)
27from ..core import Date, Period
28from .bitwidths import LEGACY_BITS
29from .naive_bv import (
30 eom_clamp,
31 normalize_month,
32 is_leap
33)
34# -------------------------------
35# Epoch binding: 2000-03-01
36# -------------------------------
37# _ORD_EPOCH = to_ordinal(BitVecVal(2000, LEGACY_BITS), BitVecVal(3, LEGACY_BITS), BitVecVal(1, LEGACY_BITS)) # original ground Z3 term
38_ORD_EPOCH = BitVecVal(
39 730179, LEGACY_BITS
40) # precomputed ordinal of 2000-03-01 (0001-01-01 = 0)
42_EPOCH = date(2000, 3, 1)
44_NONLEAP_PREFIX = [0, 31, 59, 90, 120, 151, 181, 212, 243, 273, 304, 334]
45_LEAP_PREFIX = [0, 31, 60, 91, 121, 152, 182, 213, 244, 274, 305, 335]
47def date_from_days_since_epoch(days: int) -> Date:
48 """Convert concrete days since epoch to a concrete Date."""
49 result_date = _EPOCH + timedelta(days=days)
50 return Date(result_date.year, result_date.month, result_date.day)
52def days_since_epoch_from_date(date_obj: Date) -> int:
53 """Convert a concrete Date to concrete days since epoch (March 1, 2000)."""
54 target_python = date(date_obj.year, date_obj.month, date_obj.day)
55 return (target_python - _EPOCH).days
57def add_days_ordinal(y, m, d, delta_days) -> BitVecRef:
58 """
59 Exact ordinal-based addition via a single ordinal add.
60 """
61 z = _days_since_epoch_from_ymd_bv(y, m, d)
62 return z + delta_days
64def days_before_year(y) -> BitVecRef:
65 """
66 Days from 0001-01-01 to Jan 1 of year y (0-based), Gregorian rules.
67 """
68 y1 = y - BitVecVal(1, LEGACY_BITS)
69 return (
70 BitVecVal(365, LEGACY_BITS) * y1
71 + y1 / BitVecVal(4, LEGACY_BITS)
72 - y1 / BitVecVal(100, LEGACY_BITS)
73 + y1 / BitVecVal(400, LEGACY_BITS)
74 )
76def days_before_month(y, m) -> BitVecRef:
77 """Z3 piecewise selection (no Python control over symbolic m)."""
78 expr = BitVecVal(0, LEGACY_BITS)
79 for i in range(1, 13):
80 expr = If(m == BitVecVal(i, LEGACY_BITS), _dbm_index(y, i), expr)
81 return expr
83def to_ordinal(y, m, d) -> BitVecRef:
84 """Z3-pure ordinal conversion (day 0 = 0001-01-01)."""
85 return (
86 days_before_year(y) + days_before_month(y, m) + (d - BitVecVal(1, LEGACY_BITS))
87 )
90def from_ordinal(n) -> Tuple[BitVecRef, BitVecRef, BitVecRef]:
91 """Z3-pure ordinal to date conversion using 400/100/4/1 year block decomposition."""
92 # 400/100/4/1 year block decomposition
93 D400, D100, D4, D1 = (
94 BitVecVal(146097, LEGACY_BITS),
95 BitVecVal(36524, LEGACY_BITS),
96 BitVecVal(1461, LEGACY_BITS),
97 BitVecVal(365, LEGACY_BITS),
98 )
99 q400, r400 = n / D400, n % D400
101 q100_raw = r400 / D100
102 q100 = If(
103 q100_raw >= BitVecVal(4, LEGACY_BITS), BitVecVal(3, LEGACY_BITS), q100_raw
104 ) # clamp 0..3
105 r100 = r400 - q100 * D100
107 q4, r4 = r100 / D4, r100 % D4
109 q1_raw = r4 / D1
110 q1 = If(
111 q1_raw >= BitVecVal(4, LEGACY_BITS), BitVecVal(3, LEGACY_BITS), q1_raw
112 ) # clamp 0..3
113 r1 = r4 - q1 * D1 # day-of-year (0..365)
115 year = (
116 q400 * BitVecVal(400, LEGACY_BITS)
117 + q100 * BitVecVal(100, LEGACY_BITS)
118 + q4 * BitVecVal(4, LEGACY_BITS)
119 + q1
120 + BitVecVal(1, LEGACY_BITS)
121 )
123 # month = max i with r1 >= DBM(year, i)
124 dbm = [_dbm_index(year, i) for i in range(1, 13)]
125 month = BitVecVal(1, LEGACY_BITS)
126 for i in range(2, 13):
127 month = If(r1 >= dbm[i - 1], BitVecVal(i, LEGACY_BITS), month)
129 # day = r1 - DBM(year, month) + 1
130 day_expr = r1 - dbm[0] + BitVecVal(1, LEGACY_BITS)
131 for i in range(2, 13):
132 day_expr = If(
133 r1 >= dbm[i - 1], r1 - dbm[i - 1] + BitVecVal(1, LEGACY_BITS), day_expr
134 )
136 return year, month, day_expr
138def _ymd_from_days_since_epoch_bv(days_term: BitVecRef) -> Tuple[BitVecRef, BitVecRef, BitVecRef]:
139 """Decode (y,m,d) from a Z3 BitVec 'days since 2000-03-01'."""
140 return from_ordinal(days_term + _ORD_EPOCH)
142def _days_since_epoch_from_ymd_bv(y: BitVecRef, m: BitVecRef, d: BitVecRef) -> BitVecRef:
143 """Encode (y,m,d) to Z3 BitVec 'days since 2000-03-01'."""
144 return to_ordinal(y, m, d) - _ORD_EPOCH
146def ymd_from_days_since_epoch(days_term):
147 """
148 Overload:
149 - ymd_from_days_since_epoch(int) -> Date
150 - ymd_from_days_since_epoch(BitVecRef) -> (y,m,d) BitVecRefs
151 """
152 if isinstance(days_term, int):
153 return date_from_days_since_epoch(days_term)
154 return _ymd_from_days_since_epoch_bv(days_term)
156def days_since_epoch_from_ymd(*args):
157 """
158 Overload:
159 - days_since_epoch_from_ymd(Date) -> int
160 - days_since_epoch_from_ymd(y,m,d) -> BitVecRef
161 """
162 if len(args) == 1 and isinstance(args[0], Date):
163 return days_since_epoch_from_date(args[0])
164 if len(args) == 3: 164 ↛ 167line 164 didn't jump to line 167 because the condition on line 164 was always true
165 y, m, d = args
166 return _days_since_epoch_from_ymd_bv(y, m, d)
167 raise TypeError("days_since_epoch_from_ymd expects (Date) or (y, m, d)")
169def _dbm_index(y, idx) -> BitVecRef:
170 """days_before_month for fixed idx∈{1..12} as a Z3 term."""
171 non = BitVecVal(_NONLEAP_PREFIX[idx - 1], LEGACY_BITS)
172 lep = BitVecVal(_LEAP_PREFIX[idx - 1], LEGACY_BITS)
173 return If(is_leap(y), lep, non)
175class DateVar:
176 """Symbolic date variable for epoch_days implementation."""
178 def __init__(self, name: str):
179 """Create a symbolic date variable."""
180 self.name = name
181 # Use a single Z3 bitvector variable for days since epoch
182 self.days_var = BitVec(f"{name}_days", LEGACY_BITS)
183 # Solver reference for adding bounds to intermediate dates (set after creation if needed)
184 self._solver = None
186 def __str__(self) -> str:
187 return f"DateVar({self.name})"
189 @property
190 def year(self) -> BitVecRef:
191 """Get symbolic year component (decodes from days_var)."""
192 y, _, _ = ymd_from_days_since_epoch(self.days_var)
193 return y
195 @property
196 def month(self) -> BitVecRef:
197 """Get symbolic month component (decodes from days_var)."""
198 _, m, _ = ymd_from_days_since_epoch(self.days_var)
199 return m
201 @property
202 def day(self) -> BitVecRef:
203 """Get symbolic day component (decodes from days_var)."""
204 _, _, d = ymd_from_days_since_epoch(self.days_var)
205 return d
207 def to_concrete_date(self, model: ModelRef) -> Date:
208 """Convert Z3 model to concrete Date."""
209 days = model.evaluate(self.days_var, model_completion=True).as_signed_long()
210 return date_from_days_since_epoch(days)
212 def __ge__(self, other) -> BoolRef:
213 """Support x >= date comparison."""
214 if isinstance(other, Date):
215 return self.days_var >= BitVecVal(days_since_epoch_from_date(other), LEGACY_BITS)
216 elif isinstance(other, DateVar): 216 ↛ 219line 216 didn't jump to line 219 because the condition on line 216 was always true
217 return self.days_var >= other.days_var
218 else:
219 raise TypeError(f"Cannot compare DateVar with {type(other)}")
221 def __le__(self, other) -> BoolRef:
222 """Support x <= date comparison."""
223 if isinstance(other, Date):
224 return self.days_var <= BitVecVal(days_since_epoch_from_date(other), LEGACY_BITS)
225 elif isinstance(other, DateVar): 225 ↛ 228line 225 didn't jump to line 228 because the condition on line 225 was always true
226 return self.days_var <= other.days_var
227 else:
228 raise TypeError(f"Cannot compare DateVar with {type(other)}")
230 def __lt__(self, other) -> BoolRef:
231 """Support x < date comparison."""
232 if isinstance(other, (Date, DateVar)): 232 ↛ 235line 232 didn't jump to line 235 because the condition on line 232 was always true
233 return Not(self.__ge__(other))
234 else:
235 raise TypeError(f"Cannot compare DateVar with {type(other)}")
237 def __gt__(self, other) -> BoolRef:
238 """Support x > date comparison."""
239 if isinstance(other, (Date, DateVar)): 239 ↛ 242line 239 didn't jump to line 242 because the condition on line 239 was always true
240 return Not(self.__le__(other))
241 else:
242 raise TypeError(f"Cannot compare DateVar with {type(other)}")
244 def __eq__(self, other) -> BoolRef:
245 """Support x == date comparison."""
246 if isinstance(other, Date):
247 return self.days_var == BitVecVal(days_since_epoch_from_date(other), LEGACY_BITS)
248 elif isinstance(other, DateVar): 248 ↛ 251line 248 didn't jump to line 251 because the condition on line 248 was always true
249 return self.days_var == other.days_var
250 else:
251 raise TypeError(f"Cannot compare DateVar with {type(other)}")
253 def __ne__(self, other) -> BoolRef:
254 """Support x != date comparison."""
255 if isinstance(other, (Date, DateVar)): 255 ↛ 258line 255 didn't jump to line 258 because the condition on line 255 was always true
256 return Not(self.__eq__(other))
257 else:
258 raise TypeError(f"Cannot compare DateVar with {type(other)}")
260 def _add_bounds(self) -> None:
261 """Add date validation bounds to this DateVar if solver is available."""
262 if self._solver is None: 262 ↛ 263line 262 didn't jump to line 263 because the condition on line 262 was never true
263 return
265 # Add constraints for valid date ranges [1900-03-01 to 2100-02-28]
266 # Epoch is March 1, 2000
267 # 1900-03-01 = -36525 days from epoch
268 # 2100-02-28 = 36523 days from epoch
269 self._solver.add(self.days_var >= BitVecVal(-36525, LEGACY_BITS))
270 self._solver.add(self.days_var <= BitVecVal(36523, LEGACY_BITS))
272 def __add__(self, other) -> "DateVar":
273 """
274 DateVar + Period following semantics.
275 Steps: normalize Y/M, EOM clamp, then add D days in ordinal space.
276 """
277 if isinstance(other, Period): 277 ↛ 316line 277 didn't jump to line 316 because the condition on line 277 was always true
278 result = DateVar(f"{self.name}_plus")
280 # Fast-path: only days component (check at Python level since Period components are concrete)
281 if other.years == 0 and other.months == 0:
282 days_expr = self.days_var + BitVecVal(other.days, LEGACY_BITS)
283 else:
284 oy, om, od = (
285 BitVecVal(other.years, LEGACY_BITS),
286 BitVecVal(other.months, LEGACY_BITS),
287 BitVecVal(other.days, LEGACY_BITS),
288 )
290 # Decode current date to Y/M/D
291 y0, m0, d0 = ymd_from_days_since_epoch(self.days_var)
293 # Step 1: Combine Y and M with normalization (carry years)
294 period_total_months = oy * BitVecVal(12, LEGACY_BITS) + om
295 total_months = m0 + period_total_months
296 y1, m1 = normalize_month(y0, total_months)
298 # Step 2: EOM clamp
299 d1 = eom_clamp(y1, m1, d0)
301 if other.days == 0:
302 # Encode back to days-since-epoch
303 days_expr = days_since_epoch_from_ymd(y1, m1, d1)
304 else:
305 # Step 3: add D days in ordinal space
306 days_expr = add_days_ordinal(y1, m1, d1, od)
308 # Direct assignment
309 result.days_var = days_expr
311 # Add bounds to intermediate result
312 result._solver = self._solver
313 result._add_bounds()
314 return result
315 else:
316 raise TypeError(f"Cannot add {type(other)} to DateVar")
318 def __sub__(self, other) -> "DateVar":
319 """DateVar - Period implemented as DateVar + (-Period)."""
320 if isinstance(other, Period): 320 ↛ 324line 320 didn't jump to line 324 because the condition on line 320 was always true
321 neg = Period(-other.years, -other.months, -other.days)
322 return self.__add__(neg)
323 else:
324 raise TypeError(f"Cannot subtract {type(other)} from DateVar")
327class EpochDaysSolver:
328 """Epoch_days date constraint solver using epoch-based conversion."""
330 def __init__(self, timeout_ms=600000, use_maxsat=False):
331 """Initialize the solver with timeout.
333 Args:
334 timeout_ms: Timeout in milliseconds (default: 60 seconds)
335 use_maxsat: If True, use MaxSAT optimization with soft constraints
336 """
337 self.use_maxsat = use_maxsat
338 if use_maxsat: 338 ↛ 339line 338 didn't jump to line 339 because the condition on line 338 was never true
339 self.solver = Optimize()
340 else:
341 self.solver = Solver()
342 self.solver.set("timeout", timeout_ms)
343 self.date_vars = {}
344 self.constraints = []
345 self.timeout_ms = timeout_ms
347 def add_date_var(self, name: str) -> DateVar:
348 """Add a symbolic date variable with basic constraints."""
349 date_var = DateVar(name)
350 date_var._solver = self.solver
351 self.date_vars[name] = date_var
353 # Add bounds using _add_bounds method
354 date_var._add_bounds()
355 return date_var
357 def add_constraint(self, constraint: BoolRef) -> None:
358 """Add a constraint to the solver."""
359 self.constraints.append(constraint)
360 self.solver.add(constraint)
362 def check(self) -> CheckSatResult:
363 """Check if constraints are satisfiable."""
364 return self.solver.check()
366 def model(self) -> ModelRef:
367 """Get the model if satisfiable."""
368 return self.solver.model()
370 def get_concrete_dates(self, model: ModelRef) -> dict:
371 """Get concrete dates from the model."""
372 return {
373 name: var.to_concrete_date(model) for name, var in self.date_vars.items()
374 }
376 def solve(self) -> Union[bool, dict]:
377 """Solve the constraints."""
378 # Add MaxSAT soft constraints if enabled
379 if self.use_maxsat: 379 ↛ 380line 379 didn't jump to line 380 because the condition on line 379 was never true
380 from datetime import date
382 today = date.today()
383 today_days = days_since_epoch_from_date(Date.from_python_date(today))
385 # Calculate ±50 years and ±10 years in days (approximate)
386 # Using 365.25 days per year for accuracy
387 days_50_years = int(50 * 365.25)
388 days_10_years = int(10 * 365.25)
390 # Add soft constraints for each date variable
391 for name, date_var in self.date_vars.items():
392 # High weight: today ± 50 years
393 within_50_years = And(
394 date_var.days_var
395 >= BitVecVal(today_days - days_50_years, LEGACY_BITS),
396 date_var.days_var
397 <= BitVecVal(today_days + days_50_years, LEGACY_BITS),
398 )
399 self.solver.add_soft(within_50_years, weight=100)
401 # Low weight: today ± 10 years
402 within_10_years = And(
403 date_var.days_var
404 >= BitVecVal(today_days - days_10_years, LEGACY_BITS),
405 date_var.days_var
406 <= BitVecVal(today_days + days_10_years, LEGACY_BITS),
407 )
408 self.solver.add_soft(within_10_years, weight=10)
410 result = self.check()
411 if result == sat:
412 model = self.model()
413 return {
414 "status": "sat",
415 "dates": self.get_concrete_dates(model),
416 }
417 elif result == unsat: 417 ↛ 421line 417 didn't jump to line 421 because the condition on line 417 was always true
418 return {"status": "unsat", "dates": {}}
419 else:
420 # result == unknown (timeout or resource limit)
421 return {"status": "timeout", "dates": {}}
423 def to_smt2(self) -> str:
424 """Return the current problem in SMT-LIB v2 format."""
425 return self.solver.to_smt2()
427 def get_assertions(self) -> List[BoolRef]:
428 """Return the list of current Z3 assertions (BoolRef)."""
429 return list(self.solver.assertions())