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