Coverage for datesat / symbolic_bitvector / hybrid_bv.py: 72.6%
270 statements
« prev ^ index » next coverage.py v7.13.4, created at 2026-02-10 23:47 +0000
1"""
2Hybrid DateSAT implementation using dual-lazy representation.
4This module implements a hybrid approach where dates can be represented by
5either epoch days or (Y, M, D), and each side is materialized and kept
6consistent lazily on demand:
7- epoch_var: Z3 BitVec, days since 2000-03-01
8- year/month/day vars: created lazily when needed
10Rules:
11- We track which representation is currently consistent via flags.
12- No automatic forward-link is added when Y/M/D are materialized.
13- When an operation requires epoch, we use the epoch expression derived from
14 whichever side is currently consistent.
15- When an operation requires Y/M/D, we use Y/M/D terms derived similarly.
16- Comparisons prefer Y/M/D when both sides have consistent Y/M/D; otherwise
17 prefer epoch if both have consistent epoch; otherwise derive epoch terms
18 on the fly and compare.
19"""
21from datetime import date, timedelta
22from typing import List, Tuple, Union
24from z3 import (
25 UGE,
26 UGT,
27 ULE,
28 ULT,
29 And,
30 BitVec,
31 BitVecRef,
32 BitVecVal,
33 BoolRef,
34 CheckSatResult,
35 ModelRef,
36 Not,
37 Optimize,
38 Or,
39 Solver,
40 sat,
41 unsat,
42)
43from ..core import Date, Period
44from .bitwidths import LEGACY_BITS
45from .naive_bv import (
46 eom_clamp,
47 normalize_month,
48 days_in_month
49)
50from .epoch_days_bv import (
51 date_from_days_since_epoch,
52 days_since_epoch_from_date,
53 add_days_ordinal,
54 days_since_epoch_from_ymd,
55 ymd_from_days_since_epoch
56)
58class DateVar:
59 """Symbolic date variable with lazy dual representation (epoch + Y/M/D)."""
61 def __init__(self, ctx, name: str, is_user_var: bool = True):
62 """Create a symbolic date variable.
64 Args:
65 ctx: Solver context (HybridSolver instance)
66 name: Name of the date variable
67 is_user_var: If True, this is a user-declared variable (for filtering in get_concrete_dates)
68 """
69 self.ctx = ctx
70 self.name = name
71 # Track if this is a user-declared variable (needs bounds) vs intermediate result
72 self._is_user_var = is_user_var
73 # Solver reference for adding bounds to intermediate dates
74 self._solver = ctx.solver if ctx else None
75 # Primary epoch representation
76 self.epoch_var = BitVec(f"{name}_epoch", LEGACY_BITS)
77 # Lazy YMD vars
78 self._ymd_exists = False
79 self._year_var = None
80 self._month_var = None
81 self._day_var = None
82 # Consistency flags
83 self._epoch_consistent = True
84 self._ymd_consistent = False
86 def __str__(self) -> str:
87 return f"DateVar({self.name})"
89 # Back-compat property name used in some places
90 @property
91 def days_var(self) -> BitVecRef:
92 return self.epoch_var
94 @property
95 def year_var(self) -> BitVecRef:
96 """Get year component, deriving from epoch if needed."""
97 y, _, _ = self._ymd_expr()
98 return y
100 @property
101 def month_var(self) -> BitVecRef:
102 """Get month component, deriving from epoch if needed."""
103 _, m, _ = self._ymd_expr()
104 return m
106 @property
107 def day_var(self) -> BitVecRef:
108 """Get day component, deriving from epoch if needed."""
109 _, _, d = self._ymd_expr()
110 return d
112 # Alias properties for compatibility with parser-generated code
113 # The parser generates code like "x.year == y" which expects .year attribute
114 @property
115 def year(self) -> BitVecRef:
116 """Alias for year_var for compatibility with parser-generated code."""
117 return self.year_var
119 @property
120 def month(self) -> BitVecRef:
121 """Alias for month_var for compatibility with parser-generated code."""
122 return self.month_var
124 @property
125 def day(self) -> BitVecRef:
126 """Alias for day_var for compatibility with parser-generated code."""
127 return self.day_var
129 def _ensure_ymd(self) -> None:
130 """Ensure Y/M/D variables exist. Creates them if they don't exist.
132 Note: This only creates the vars and links them to epoch. It does NOT
133 set consistency flags - that should be done by the caller based on
134 which representation is the source of truth.
135 """
136 if self._ymd_exists: 136 ↛ 137line 136 didn't jump to line 137 because the condition on line 136 was never true
137 return
138 self._year_var = BitVec(f"{self.name}_year", LEGACY_BITS)
139 self._month_var = BitVec(f"{self.name}_month", LEGACY_BITS)
140 self._day_var = BitVec(f"{self.name}_day", LEGACY_BITS)
141 self._ymd_exists = True
142 # Link YMD to epoch (bidirectional constraint)
143 # The epoch bounds (added in add_date_var) ensure Y/M/D stays within valid range
144 # Add constraint: epoch_var == days_since_epoch_from_ymd(year_var, month_var, day_var)
145 self.ctx.solver.add(
146 self.epoch_var
147 == days_since_epoch_from_ymd(self._year_var, self._month_var, self._day_var)
148 )
149 # Note: Consistency flags are NOT set here - caller should set them based on source of truth
151 def _epoch_expr(self) -> BitVecRef:
152 """Return an epoch-days expression consistent with current state (lazy).
154 If epoch is consistent, return epoch_var directly.
155 Otherwise, derive epoch from Y/M/D (Y/M/D must exist when epoch_consistent is False),
156 store it, and update consistency flags.
157 """
158 if self._epoch_consistent:
159 return self.epoch_var
160 # derive from Y/M/D lazily
161 y, m, d = self._year_var, self._month_var, self._day_var
162 epoch_expr = days_since_epoch_from_ymd(y, m, d)
163 # Store the derived representation and update consistency
164 self.ctx.solver.add(self.epoch_var == epoch_expr)
165 self._epoch_consistent = True
166 return self.epoch_var
168 def _ymd_expr(self) -> Tuple[BitVecRef, BitVecRef, BitVecRef]:
169 """Return Y/M/D expressions consistent with current state (lazy).
171 If Y/M/D is consistent, return Y/M/D vars directly.
172 Otherwise, derive Y/M/D from epoch, store them, and update consistency flags.
173 """
174 if self._ymd_consistent and self._ymd_exists:
175 return self._year_var, self._month_var, self._day_var
176 # derive from epoch lazily
177 epoch = self._epoch_expr()
178 y, m, d = ymd_from_days_since_epoch(epoch)
179 # Ensure Y/M/D vars exist
180 if not self._ymd_exists: 180 ↛ 189line 180 didn't jump to line 189 because the condition on line 180 was always true
181 self._ensure_ymd()
182 # _ensure_ymd() links epoch to Y/M/D, but since epoch is source of truth,
183 # we need to set Y/M/D values from epoch
184 self.ctx.solver.add(self._year_var == y)
185 self.ctx.solver.add(self._month_var == m)
186 self.ctx.solver.add(self._day_var == d)
187 else:
188 # Y/M/D vars exist but not consistent - derive and store
189 self.ctx.solver.add(self._year_var == y)
190 self.ctx.solver.add(self._month_var == m)
191 self.ctx.solver.add(self._day_var == d)
192 # Update consistency flag
193 self._ymd_consistent = True
194 return self._year_var, self._month_var, self._day_var
196 def to_concrete_date(self, model: ModelRef) -> Date:
197 if self._ymd_consistent and self._ymd_exists:
198 y = model.evaluate(self._year_var, model_completion=True).as_signed_long()
199 m = model.evaluate(self._month_var, model_completion=True).as_signed_long()
200 d = model.evaluate(self._day_var, model_completion=True).as_signed_long()
201 try:
202 return Date(y, m, d)
203 except ValueError:
204 # Intermediate result went out of bounds - use unbounded date
205 return Date(y, m, d, bounded=False)
206 # Otherwise evaluate epoch variable directly
207 # If epoch is consistent, epoch_var is the source of truth
208 if self._epoch_consistent: 208 ↛ 212line 208 didn't jump to line 212 because the condition on line 208 was always true
209 e = model.evaluate(self.epoch_var, model_completion=True).as_signed_long()
210 else:
211 # Epoch not consistent, need to derive from Y/M/D
212 e = model.evaluate(self._epoch_expr(), model_completion=True).as_signed_long()
213 try:
214 return date_from_days_since_epoch(e)
215 except ValueError:
216 # Epoch out of bounds - convert to Y/M/D then create unbounded date
217 from datetime import date, timedelta
219 _EPOCH = date(2000, 3, 1)
220 result_date = _EPOCH + timedelta(days=e)
221 return Date(result_date.year, result_date.month, result_date.day, bounded=False)
223 def __ge__(self, other) -> BoolRef:
224 """Support x >= date comparison.
226 Comparison strategy (dual-lazy):
227 1. If both have consistent epoch: compare on epoch_var
228 2. Else if both have consistent Y/M/D: compare lexicographically on (Y, M, D)
229 3. Else: derive epoch expressions for both sides (converting Y/M/D to epoch if needed) and compare
230 """
231 if isinstance(other, Date):
232 # If we have consistent Y/M/D, use Y/M/D comparison (more efficient)
233 if self._ymd_consistent and self._ymd_exists:
234 y1, m1, d1 = self._year_var, self._month_var, self._day_var
235 y2, m2, d2 = BitVecVal(other.year, LEGACY_BITS), BitVecVal(other.month, LEGACY_BITS), BitVecVal(other.day, LEGACY_BITS)
236 return Or(
237 UGT(y1, y2),
238 And(y1 == y2, Or(UGT(m1, m2), And(m1 == m2, UGE(d1, d2)))),
239 )
240 # Otherwise, use epoch comparison
241 return self._epoch_expr() >= BitVecVal(
242 days_since_epoch_from_date(other), LEGACY_BITS
243 )
244 elif isinstance(other, DateVar): 244 ↛ 264line 244 didn't jump to line 264 because the condition on line 244 was always true
245 # Case 1: Both have consistent epoch - use epoch comparison
246 if self._epoch_consistent and other._epoch_consistent: 246 ↛ 249line 246 didn't jump to line 249 because the condition on line 246 was always true
247 return self.epoch_var >= other.epoch_var
248 # Case 2: Both have consistent Y/M/D - use Y/M/D comparison
249 if (
250 self._ymd_consistent
251 and self._ymd_exists
252 and other._ymd_consistent
253 and other._ymd_exists
254 ):
255 y1, m1, d1 = self._year_var, self._month_var, self._day_var
256 y2, m2, d2 = other._year_var, other._month_var, other._day_var
257 return Or(
258 UGT(y1, y2),
259 And(y1 == y2, Or(UGT(m1, m2), And(m1 == m2, UGE(d1, d2)))),
260 )
261 # Case 3: Inconsistent - derive epoch expressions for both and compare
262 return self._epoch_expr() >= other._epoch_expr()
263 else:
264 raise TypeError(f"Cannot compare DateVar with {type(other)}")
266 def __le__(self, other) -> BoolRef:
267 """Support x <= date comparison.
269 Comparison strategy (dual-lazy):
270 1. If both have consistent epoch: compare on epoch_var
271 2. Else if both have consistent Y/M/D: compare lexicographically on (Y, M, D)
272 3. Else: derive epoch expressions for both sides (converting Y/M/D to epoch if needed) and compare
273 """
274 if isinstance(other, Date):
275 # If we have consistent Y/M/D, use Y/M/D comparison (more efficient)
276 if self._ymd_consistent and self._ymd_exists:
277 y1, m1, d1 = self._year_var, self._month_var, self._day_var
278 y2, m2, d2 = BitVecVal(other.year, LEGACY_BITS), BitVecVal(other.month, LEGACY_BITS), BitVecVal(other.day, LEGACY_BITS)
279 return Or(
280 ULT(y1, y2),
281 And(y1 == y2, Or(ULT(m1, m2), And(m1 == m2, ULE(d1, d2)))),
282 )
283 # Otherwise, use epoch comparison
284 return self._epoch_expr() <= BitVecVal(
285 days_since_epoch_from_date(other), LEGACY_BITS
286 )
287 elif isinstance(other, DateVar): 287 ↛ 307line 287 didn't jump to line 307 because the condition on line 287 was always true
288 # Case 1: Both have consistent epoch - use epoch comparison
289 if self._epoch_consistent and other._epoch_consistent: 289 ↛ 292line 289 didn't jump to line 292 because the condition on line 289 was always true
290 return self.epoch_var <= other.epoch_var
291 # Case 2: Both have consistent Y/M/D - use Y/M/D comparison
292 if (
293 self._ymd_consistent
294 and self._ymd_exists
295 and other._ymd_consistent
296 and other._ymd_exists
297 ):
298 y1, m1, d1 = self._year_var, self._month_var, self._day_var
299 y2, m2, d2 = other._year_var, other._month_var, other._day_var
300 return Or(
301 ULT(y1, y2),
302 And(y1 == y2, Or(ULT(m1, m2), And(m1 == m2, ULE(d1, d2)))),
303 )
304 # Case 3: Inconsistent - derive epoch expressions for both and compare
305 return self._epoch_expr() <= other._epoch_expr()
306 else:
307 raise TypeError(f"Cannot compare DateVar with {type(other)}")
309 def __lt__(self, other) -> BoolRef:
310 """Support x < date comparison."""
311 if isinstance(other, (Date, DateVar)): 311 ↛ 314line 311 didn't jump to line 314 because the condition on line 311 was always true
312 return Not(self.__ge__(other))
313 else:
314 raise TypeError(f"Cannot compare DateVar with {type(other)}")
316 def __gt__(self, other) -> BoolRef:
317 """Support x > date comparison."""
318 if isinstance(other, (Date, DateVar)): 318 ↛ 321line 318 didn't jump to line 321 because the condition on line 318 was always true
319 return Not(self.__le__(other))
320 else:
321 raise TypeError(f"Cannot compare DateVar with {type(other)}")
323 def __eq__(self, other) -> BoolRef:
324 """Support x == date comparison.
326 Comparison strategy (dual-lazy):
327 1. If both have consistent epoch: compare on epoch_var
328 2. Else if both have consistent Y/M/D: compare on (Y, M, D) components
329 3. Else: derive epoch expressions for both sides (converting Y/M/D to epoch if needed) and compare
330 """
331 if isinstance(other, Date):
332 # If we have consistent Y/M/D, use Y/M/D comparison (more efficient)
333 if self._ymd_consistent and self._ymd_exists:
334 return And(
335 self._year_var == BitVecVal(other.year, LEGACY_BITS),
336 self._month_var == BitVecVal(other.month, LEGACY_BITS),
337 self._day_var == BitVecVal(other.day, LEGACY_BITS),
338 )
339 # Otherwise, use epoch comparison
340 return self._epoch_expr() == BitVecVal(days_since_epoch_from_date(other), LEGACY_BITS)
341 elif isinstance(other, DateVar): 341 ↛ 383line 341 didn't jump to line 383 because the condition on line 341 was always true
342 # Case 1: Both have consistent epoch - use epoch comparison
343 if self._epoch_consistent and other._epoch_consistent:
344 return self.epoch_var == other.epoch_var
345 # Case 2: Both have consistent Y/M/D - use Y/M/D comparison
346 if ( 346 ↛ 352line 346 didn't jump to line 352 because the condition on line 346 was never true
347 self._ymd_consistent
348 and self._ymd_exists
349 and other._ymd_consistent
350 and other._ymd_exists
351 ):
352 return And(
353 self._year_var == other._year_var,
354 self._month_var == other._month_var,
355 self._day_var == other._day_var,
356 )
357 # Case 3: Inconsistent - derive missing representation and compare on common representation
358 # If self has epoch consistent, derive other's epoch from Y/M/D and compare on epoch
359 if self._epoch_consistent: 359 ↛ 368line 359 didn't jump to line 368 because the condition on line 359 was always true
360 # other must have Y/M/D consistent (otherwise we'd be in Case 1 or 2)
361 # Derive other's epoch from its Y/M/D
362 other._epoch_expr() # This will derive epoch and set other._epoch_consistent = True
363 # Also derive self's Y/M/D from epoch so both are properly linked
364 # This ensures that when self.month is accessed later, it uses Y/M/D derived from epoch
365 self._ymd_expr() # This will derive Y/M/D from epoch and set self._ymd_consistent = True
366 return self.epoch_var == other.epoch_var
367 # If other has epoch consistent, derive self's epoch from Y/M/D and compare on epoch
368 elif other._epoch_consistent:
369 # self must have Y/M/D consistent (otherwise we'd be in Case 1 or 2)
370 # Derive self's epoch from its Y/M/D
371 self._epoch_expr() # This will derive epoch and set self._epoch_consistent = True
372 # Also derive other's Y/M/D from epoch so both are properly linked
373 # This ensures that when other.month is accessed later, it uses Y/M/D derived from epoch
374 other._ymd_expr() # This will derive Y/M/D from epoch and set other._ymd_consistent = True
375 return self.epoch_var == other.epoch_var
376 else:
377 # Neither has epoch consistent - both should have Y/M/D consistent (Case 2 should have caught this)
378 # But if we get here, derive both epochs and compare
379 self._epoch_expr()
380 other._epoch_expr()
381 return self.epoch_var == other.epoch_var
382 else:
383 raise TypeError(f"Cannot compare DateVar with {type(other)}")
385 def __ne__(self, other) -> BoolRef:
386 """Support x != date comparison."""
387 if isinstance(other, (Date, DateVar)): 387 ↛ 390line 387 didn't jump to line 390 because the condition on line 387 was always true
388 return Not(self.__eq__(other))
389 else:
390 raise TypeError(f"Cannot compare DateVar with {type(other)}")
392 def _add_bounds(self) -> None:
393 """Add date validation bounds to this DateVar if solver is available."""
394 if self._solver is None: 394 ↛ 395line 394 didn't jump to line 395 because the condition on line 394 was never true
395 return
397 # Prioritize epoch bounds when epoch is consistent (more efficient)
398 # Fall back to Y/M/D bounds only if epoch is not consistent but Y/M/D is
399 if self._epoch_consistent:
400 # Add constraints for valid date ranges [1900-03-01 to 2100-02-28]
401 # Epoch is March 1, 2000
402 # 1900-03-01 = -36525 days from epoch
403 # 2100-02-28 = 36523 days from epoch
404 self._solver.add(self.epoch_var >= BitVecVal(-36525, LEGACY_BITS))
405 self._solver.add(self.epoch_var <= BitVecVal(36523, LEGACY_BITS))
406 elif self._ymd_consistent and self._ymd_exists: 406 ↛ 441line 406 didn't jump to line 441 because the condition on line 406 was always true
407 # Add comprehensive date validation constraints directly to Y/M/D
408 # Valid range is 1900-03-01 to 2100-02-28
409 self._solver.add(
410 Or(
411 # 1900-03-01 to 1900-12-31
412 And(
413 self._year_var == BitVecVal(1900, LEGACY_BITS),
414 self._month_var >= BitVecVal(3, LEGACY_BITS),
415 self._month_var <= BitVecVal(12, LEGACY_BITS),
416 self._day_var >= BitVecVal(1, LEGACY_BITS),
417 self._day_var <= days_in_month(self._year_var, self._month_var),
418 ),
419 # 1901-01-01 to 2099-12-31
420 And(
421 self._year_var >= BitVecVal(1901, LEGACY_BITS),
422 self._year_var <= BitVecVal(2099, LEGACY_BITS),
423 self._month_var >= BitVecVal(1, LEGACY_BITS),
424 self._month_var <= BitVecVal(12, LEGACY_BITS),
425 self._day_var >= BitVecVal(1, LEGACY_BITS),
426 self._day_var <= days_in_month(self._year_var, self._month_var),
427 ),
428 # 2100-01-01 to 2100-02-28
429 And(
430 self._year_var == BitVecVal(2100, LEGACY_BITS),
431 self._month_var >= BitVecVal(1, LEGACY_BITS),
432 self._month_var <= BitVecVal(2, LEGACY_BITS),
433 self._day_var >= BitVecVal(1, LEGACY_BITS),
434 self._day_var <= days_in_month(self._year_var, self._month_var),
435 ),
436 )
437 )
438 else:
439 # Neither representation is consistent yet - add bounds to epoch_var as fallback
440 # (epoch_var always exists, even if not consistent)
441 self._solver.add(self.epoch_var >= BitVecVal(-36525, LEGACY_BITS))
442 self._solver.add(self.epoch_var <= BitVecVal(36523, LEGACY_BITS))
444 def __add__(self, other) -> "DateVar":
445 """Hybrid date + Period: mirror epoch_days semantics, but avoid epoch encode unless days-only.
447 - days-only: epoch add (O(1))
448 - months/years (and mixed): decode epoch→YMD, normalize months, clamp, add days via ordinal,
449 then set result's Y/M/D; epoch derives later when needed.
450 """
451 if not isinstance(other, Period): 451 ↛ 452line 451 didn't jump to line 452 because the condition on line 451 was never true
452 raise TypeError(f"Cannot add {type(other)} to DateVar")
454 # Create intermediate result with bounds (following naive/epoch_days pattern)
455 # Ensure unique name to avoid collisions
456 base_name = f"{self.name}_plus_{other.years}y_{other.months}m_{other.days}d"
457 name = base_name
458 suffix = 0
459 while name in self.ctx.date_vars: 459 ↛ 460line 459 didn't jump to line 460 because the condition on line 459 was never true
460 suffix += 1
461 name = f"{base_name}_{suffix}"
463 # Create DateVar for intermediate result
464 result = DateVar(
465 self.ctx,
466 name,
467 is_user_var=False # Intermediate result, not user-declared
468 )
469 self.ctx.date_vars[name] = result
471 # Fast-path: only days component (check at Python level since Period components are concrete)
472 if other.years == 0 and other.months == 0:
473 # Direct assignment
474 result.epoch_var = self._epoch_expr() + BitVecVal(other.days, LEGACY_BITS)
475 # Result now has epoch consistent; YMD not yet
476 result._epoch_consistent = True
477 result._ymd_consistent = False
478 else:
479 oy, om, od = (
480 BitVecVal(other.years, LEGACY_BITS),
481 BitVecVal(other.months, LEGACY_BITS),
482 BitVecVal(other.days, LEGACY_BITS),
483 )
485 # Decode current date to Y/M/D
486 y0, m0, d0 = self._ymd_expr()
488 # Step 1: Combine Y and M with normalization (carry years)
489 period_total_months = oy * BitVecVal(12, LEGACY_BITS) + om
490 total_months = m0 + period_total_months
491 year_carry, m1 = normalize_month(BitVecVal(0, LEGACY_BITS), total_months)
492 y1 = y0 + year_carry
494 # Step 2: EOM clamp
495 d1 = eom_clamp(y1, m1, d0)
497 if od == BitVecVal(0, LEGACY_BITS):
498 # Assign the computed Y/M/D expressions directly
499 # (avoiding _ensure_ymd() which would create unused variables and a redundant constraint)
500 result._year_var = y1
501 result._month_var = m1
502 result._day_var = d1
503 result._ymd_exists = True
504 # Link epoch_var to the Y/M/D values (needed for dual representation consistency)
505 # This constraint is essential because:
506 # 1. It links epoch_var to the actual Y/M/D values (y1, m1, d1)
507 # 2. Without it, epoch_var would be unconstrained, breaking operations that use it
508 # 3. It ensures bounds on Y/M/D also constrain epoch_var (via the constraint)
509 result.ctx.solver.add(
510 result.epoch_var == days_since_epoch_from_ymd(y1, m1, d1)
511 )
512 result._epoch_consistent = False
513 result._ymd_consistent = True
514 else:
515 # Direct assignment for epoch_var
516 result.epoch_var = add_days_ordinal(y1, m1, d1, od)
517 result._epoch_consistent = True
518 result._ymd_consistent = False
520 # Add bounds to intermediate result
521 result._solver = self._solver
522 result._add_bounds()
523 return result
525 def __sub__(self, other) -> "DateVar":
526 """DateVar - Period implemented as DateVar + (-Period)."""
527 if isinstance(other, Period): 527 ↛ 531line 527 didn't jump to line 531 because the condition on line 527 was always true
528 neg = Period(-other.years, -other.months, -other.days)
529 return self.__add__(neg)
530 else:
531 raise TypeError(f"Cannot subtract {type(other)} from DateVar")
534class HybridSolver:
535 """Hybrid date constraint solver using dual representation (epoch + YMD)."""
537 def __init__(self, timeout_ms=600000, use_maxsat=False):
538 """Initialize the solver with timeout.
540 Args:
541 timeout_ms: Timeout in milliseconds (default: 60 seconds)
542 use_maxsat: If True, use MaxSAT optimization with soft constraints
543 """
544 self.use_maxsat = use_maxsat
545 if use_maxsat: 545 ↛ 546line 545 didn't jump to line 546 because the condition on line 545 was never true
546 self.solver = Optimize()
547 else:
548 self.solver = Solver()
549 self.solver.set("timeout", timeout_ms)
550 self.date_vars = {}
551 self.constraints = []
552 self.timeout_ms = timeout_ms
554 def add_date_var(self, name: str, add_bounds: bool = True) -> DateVar:
555 if name is None: 555 ↛ 556line 555 didn't jump to line 556 because the condition on line 555 was never true
556 name = f"d{len(self.date_vars)}"
557 # Ensure uniqueness to avoid collisions when creating multiple temporaries
558 base_name = name
559 suffix = 0
560 while name in self.date_vars: 560 ↛ 561line 560 didn't jump to line 561 because the condition on line 560 was never true
561 suffix += 1
562 name = f"{base_name}_{suffix}"
563 # Create DateVar (always bounded for user variables)
564 dv = DateVar(self, name, is_user_var=add_bounds)
565 dv._solver = self.solver
566 self.date_vars[name] = dv
568 # Add bounds using _add_bounds method (following naive/epoch_days pattern)
569 dv._add_bounds()
570 return dv
572 def add_constraint(self, constraint: BoolRef) -> None:
573 """Add a constraint to the solver."""
574 self.constraints.append(constraint)
575 self.solver.add(constraint)
577 def check(self) -> CheckSatResult:
578 """Check if constraints are satisfiable."""
579 return self.solver.check()
581 def model(self) -> ModelRef:
582 """Get the model if satisfiable."""
583 return self.solver.model()
585 def get_concrete_dates(self, model: ModelRef) -> dict:
586 """Get concrete dates from the model.
588 Only returns user-declared variables, filtering out intermediate results
589 from arithmetic operations (consistent with other implementations).
590 """
591 return {
592 name: var.to_concrete_date(model)
593 for name, var in self.date_vars.items()
594 if var._is_user_var
595 }
597 def solve(self) -> Union[bool, dict]:
598 """Solve the constraints."""
599 # Add MaxSAT soft constraints if enabled
600 if self.use_maxsat: 600 ↛ 601line 600 didn't jump to line 601 because the condition on line 600 was never true
601 from datetime import date
603 from .epoch_days_bv import days_since_epoch_from_date
605 today = date.today()
606 today_days = days_since_epoch_from_date(Date.from_python_date(today))
608 # Calculate ±50 years and ±10 years in days (approximate)
609 # Using 365.25 days per year for accuracy
610 days_50_years = int(50 * 365.25)
611 days_10_years = int(10 * 365.25)
613 # Add soft constraints for each date variable (only user-declared ones)
614 for name, date_var in self.date_vars.items():
615 if date_var._is_user_var:
616 # High weight: today ± 50 years
617 within_50_years = And(
618 date_var.epoch_var
619 >= BitVecVal(today_days - days_50_years, LEGACY_BITS),
620 date_var.epoch_var
621 <= BitVecVal(today_days + days_50_years, LEGACY_BITS),
622 )
623 self.solver.add_soft(within_50_years, weight=100)
625 # Low weight: today ± 10 years
626 within_10_years = And(
627 date_var.epoch_var
628 >= BitVecVal(today_days - days_10_years, LEGACY_BITS),
629 date_var.epoch_var
630 <= BitVecVal(today_days + days_10_years, LEGACY_BITS),
631 )
632 self.solver.add_soft(within_10_years, weight=10)
634 result = self.check()
635 if result == sat:
636 model = self.model()
637 return {
638 "status": "sat",
639 "dates": self.get_concrete_dates(model),
640 }
641 elif result == unsat: 641 ↛ 645line 641 didn't jump to line 645 because the condition on line 641 was always true
642 return {"status": "unsat", "dates": {}}
643 else:
644 # result == unknown (timeout or resource limit)
645 return {"status": "timeout", "dates": {}}
647 def to_smt2(self) -> str:
648 """Return the current problem in SMT-LIB v2 format."""
649 return self.solver.to_smt2()
651 def get_assertions(self) -> List[BoolRef]:
652 """Return the list of current Z3 assertions (BoolRef)."""
653 return list(self.solver.assertions())