Coverage for datesat / enumeration_baseline.py: 53.2%
676 statements
« prev ^ index » next coverage.py v7.13.4, created at 2026-02-10 23:47 +0000
1"""
2Enumeration baseline implementation for comparison with DateSAT.
4This module provides a baseline solver that enumerates all valid dates
5in the allowed range [1900-03-01 to 2100-02-28] for date variables and
6checks which assignments satisfy the constraints.
7This is a brute-force approach that guarantees
8finding a solution if one exists, but may be very slow.
9"""
11from datetime import date, timedelta
12from dateutil.relativedelta import relativedelta
13from typing import Any, Dict, Optional, Union, List, Tuple
14import time
15from .core import Date, Period
16import itertools
17import builtins
19# Module-level wrapper functions for Z3 boolean operators that work with ConstraintWrapper objects
20def _wrap_constraint_for_enumeration(constraint: Any) -> "ConstraintWrapper":
21 """Wrap a constraint in ConstraintWrapper if it's not already wrapped."""
22 if isinstance(constraint, ConstraintWrapper):
23 return constraint
24 elif isinstance(constraint, bool):
25 # Use default argument to capture value, not reference
26 return ConstraintWrapper(lambda c=constraint: c)
27 elif callable(constraint):
28 return ConstraintWrapper(constraint)
29 else:
30 # Check if this is a variable object with get_value() method (EvalBoolVar, EvalIntVar, etc.)
31 # These should be evaluated by calling get_value(), not by calling the object itself
32 if hasattr(constraint, "get_value"):
33 # Capture the object with a default argument and call get_value()
34 return ConstraintWrapper(lambda obj=constraint: bool(obj.get_value()))
35 # Try to convert to bool, capture value with default argument
36 return ConstraintWrapper(lambda c=constraint: bool(c))
39def Or_enumeration(*args) -> "ConstraintWrapper":
40 """Wrapper for Z3's Or() that works with enumeration baseline ConstraintWrapper objects."""
41 wrapped_args = [_wrap_constraint_for_enumeration(arg) for arg in args]
42 # Create tuple and capture as default argument to prevent closure issues
43 wrapped_args_tuple = tuple(wrapped_args)
44 return ConstraintWrapper(
45 func=lambda wrapped=wrapped_args_tuple: any(c.evaluate() for c in wrapped),
46 or_constraints=list(wrapped_args_tuple),
47 )
50def And_enumeration(*args) -> "ConstraintWrapper":
51 """Wrapper for Z3's And() that works with enumeration baseline ConstraintWrapper objects."""
52 wrapped_args = [_wrap_constraint_for_enumeration(arg) for arg in args]
53 # Create a tuple instead of list to ensure immutability and prevent accidental sharing
54 wrapped_args_tuple = tuple(wrapped_args)
55 return ConstraintWrapper(
56 func=lambda wrapped=wrapped_args_tuple: all(c.evaluate() for c in wrapped)
57 )
60def Not_enumeration(arg) -> "ConstraintWrapper":
61 """Wrapper for Z3's Not() that works with enumeration baseline ConstraintWrapper objects."""
62 wrapped_arg = _wrap_constraint_for_enumeration(arg)
63 # Capture as default argument to prevent closure issues
64 return ConstraintWrapper(func=lambda wrapped=wrapped_arg: not wrapped.evaluate())
67def Implies_enumeration(antecedent, consequent) -> "ConstraintWrapper":
68 """Wrapper for Z3's Implies() that works with enumeration baseline ConstraintWrapper objects."""
69 wrapped_antecedent = _wrap_constraint_for_enumeration(antecedent)
70 wrapped_consequent = _wrap_constraint_for_enumeration(consequent)
71 # Explicitly capture as default arguments to avoid closure issues
72 return ConstraintWrapper(
73 func=lambda ant=wrapped_antecedent, cons=wrapped_consequent: not ant.evaluate()
74 or cons.evaluate()
75 )
78class ConstraintWrapper:
79 """Wrapper for deferred constraint evaluation."""
81 def __init__(
82 self, func, var_ref=None, concrete_value=None, rhs_ref=None, or_constraints=None
83 ):
84 self.func = func
85 self.var_ref = var_ref
86 self.concrete_value = concrete_value
87 self.rhs_ref = rhs_ref # For equality constraints: x == expr, store expr here
88 self.or_constraints = (
89 or_constraints # For OR constraints: list of ConstraintWrapper objects
90 )
92 def evaluate(self) -> bool:
93 try:
94 # If this is an OR constraint, evaluate any of the sub-constraints
95 if self.or_constraints is not None: 95 ↛ 96line 95 didn't jump to line 96 because the condition on line 95 was never true
96 return any(c.evaluate() for c in self.or_constraints)
97 return bool(self.func())
98 except (ValueError, TypeError):
99 return False
101 # ★ prevent accidental boolean usage like: if (x == y): ...
102 def __bool__(self):
103 raise TypeError(
104 "Constraint objects are not truthy. Add them to the solver via add_constraint()."
105 )
108class EnumerationComponentVar:
109 """Symbolic date component variable (year, month, or day) for use inside Date() constructor."""
111 def __init__(self, name: str, min_val: int, max_val: int, component_type: str):
112 self.name = name
113 self.min_val = min_val
114 self.max_val = max_val
115 self.component_type = component_type # 'year', 'month', or 'day'
116 self._value = None
118 def set_value(self, val: int) -> None:
119 if self.min_val <= val <= self.max_val: 119 ↛ 122line 119 didn't jump to line 122 because the condition on line 119 was always true
120 self._value = val
121 else:
122 raise ValueError(
123 f"{self.component_type} value {val} out of range [{self.min_val}, {self.max_val}]"
124 )
126 def get_value(self) -> Optional[int]:
127 return self._value
129 def clear_value(self) -> None:
130 self._value = None
132 def __str__(self) -> str:
133 return f"EnumerationComponentVar({self.name}, {self.component_type})"
135 # Arithmetic operations for expressions like year_var + 1
136 def __add__(self, other: int) -> "EnumerationComponentExpr":
137 if not isinstance(other, int): 137 ↛ 138line 137 didn't jump to line 138 because the condition on line 137 was never true
138 raise TypeError(f"Cannot add {type(other)} to EnumerationComponentVar")
139 return EnumerationComponentExpr(self, "add", other)
141 def __sub__(self, other: int) -> "EnumerationComponentExpr":
142 if not isinstance(other, int):
143 raise TypeError(
144 f"Cannot subtract {type(other)} from EnumerationComponentVar"
145 )
146 return EnumerationComponentExpr(self, "sub", other)
148 def __mul__(self, other: int) -> "EnumerationComponentExpr":
149 if not isinstance(other, int):
150 raise TypeError(f"Cannot multiply {type(other)} by EnumerationComponentVar")
151 return EnumerationComponentExpr(self, "mul", other)
153 def __mod__(self, other: int) -> "EnumerationComponentExpr":
154 if not isinstance(other, int):
155 raise TypeError(
156 f"Cannot compute modulo with {type(other)} on EnumerationComponentVar"
157 )
158 return EnumerationComponentExpr(self, "mod", other)
160 # Comparison operations for integer variables
161 def _compare(
162 self,
163 op: str,
164 other: Union[int, "EnumerationComponentVar", "EnumerationComponentExpr"],
165 ) -> ConstraintWrapper:
166 """Compare this component variable with an integer, another variable, or expression."""
168 def compare():
169 lhs_val = self.get_value()
170 if lhs_val is None:
171 return False
173 # Handle EnumerationComponentVar
174 if isinstance(other, EnumerationComponentVar):
175 rhs_val = other.get_value()
176 # Handle EnumerationComponentExpr
177 elif isinstance(other, EnumerationComponentExpr):
178 rhs_val = other.evaluate()
179 # Handle int
180 else:
181 try:
182 rhs_val = int(other)
183 except (ValueError, TypeError):
184 return False
186 if rhs_val is None:
187 return False
189 try:
190 return getattr(lhs_val, f"__{op}__")(rhs_val)
191 except (ValueError, TypeError):
192 return False
194 return ConstraintWrapper(compare)
196 def __eq__(self, other: Union[int, "EnumerationComponentVar", "EnumerationComponentExpr"]) -> ConstraintWrapper: # type: ignore[override]
197 return self._compare("eq", other)
199 def __ne__(self, other: Union[int, "EnumerationComponentVar", "EnumerationComponentExpr"]) -> ConstraintWrapper: # type: ignore[override]
200 return self._compare("ne", other)
202 def __lt__(
203 self, other: Union[int, "EnumerationComponentVar", "EnumerationComponentExpr"]
204 ) -> ConstraintWrapper:
205 return self._compare("lt", other)
207 def __le__(
208 self, other: Union[int, "EnumerationComponentVar", "EnumerationComponentExpr"]
209 ) -> ConstraintWrapper:
210 return self._compare("le", other)
212 def __gt__(
213 self, other: Union[int, "EnumerationComponentVar", "EnumerationComponentExpr"]
214 ) -> ConstraintWrapper:
215 return self._compare("gt", other)
217 def __ge__(
218 self, other: Union[int, "EnumerationComponentVar", "EnumerationComponentExpr"]
219 ) -> ConstraintWrapper:
220 return self._compare("ge", other)
223class EnumerationComponentExpr:
224 """Expression involving a component variable and a constant (e.g., year_var + 1, or x.year + 4)."""
226 def __init__(self, var: EnumerationComponentVar, op: str, constant: int):
227 self.var = var
228 self.op = op
229 self.constant = constant
231 def evaluate(self) -> Optional[int]:
232 # Check if this expression is based on a parent component (from a date variable)
233 if hasattr(self.var, "_parent_component"):
234 val = self.var._parent_component._get_component_value()
235 else:
236 val = self.var.get_value()
238 if val is None:
239 return None
240 if self.op == "add":
241 return val + self.constant
242 elif self.op == "sub":
243 return val - self.constant
244 elif self.op == "mul":
245 return val * self.constant
246 elif self.op == "mod":
247 if self.constant == 0:
248 return None # Division by zero
249 return val % self.constant
250 elif self.op == "floordiv":
251 if self.constant == 0:
252 return None # Division by zero
253 return val // self.constant
254 elif self.op == "sub_component":
255 # Subtraction of another component: val - other_component_value
256 # self.constant is not used, other_component is stored separately
257 if hasattr(self, "_other_component"):
258 other_val = self._other_component._get_component_value()
259 if other_val is None:
260 return None
261 return val - other_val
262 return None
263 return None
265 def get_base_var(self) -> EnumerationComponentVar:
266 return self.var
268 def _compare(
269 self,
270 op: str,
271 other: Union[int, "EnumerationDateComponent", "EnumerationComponentExpr"],
272 ) -> ConstraintWrapper:
273 """Compare this expression with an integer, date component, or another expression."""
275 def compare():
276 expr_val = self.evaluate()
277 if expr_val is None:
278 return False
280 # Handle EnumerationDateComponent
281 if isinstance(other, EnumerationDateComponent):
282 other_val = other._get_component_value()
283 # Handle EnumerationComponentExpr
284 elif isinstance(other, EnumerationComponentExpr):
285 other_val = other.evaluate()
286 # Handle int
287 else:
288 try:
289 other_val = int(other)
290 except (ValueError, TypeError):
291 return False
293 if other_val is None:
294 return False
296 try:
297 return getattr(expr_val, f"__{op}__")(other_val)
298 except (ValueError, TypeError):
299 return False
301 return ConstraintWrapper(compare)
303 def __eq__(self, other: Union[int, "EnumerationDateComponent", "EnumerationComponentExpr"]) -> ConstraintWrapper: # type: ignore[override]
304 return self._compare("eq", other)
306 def __ne__(self, other: Union[int, "EnumerationDateComponent", "EnumerationComponentExpr"]) -> ConstraintWrapper: # type: ignore[override]
307 return self._compare("ne", other)
309 def __lt__(
310 self, other: Union[int, "EnumerationDateComponent", "EnumerationComponentExpr"]
311 ) -> ConstraintWrapper:
312 return self._compare("lt", other)
314 def __le__(
315 self, other: Union[int, "EnumerationDateComponent", "EnumerationComponentExpr"]
316 ) -> ConstraintWrapper:
317 return self._compare("le", other)
319 def __gt__(
320 self, other: Union[int, "EnumerationDateComponent", "EnumerationComponentExpr"]
321 ) -> ConstraintWrapper:
322 return self._compare("gt", other)
324 def __ge__(
325 self, other: Union[int, "EnumerationDateComponent", "EnumerationComponentExpr"]
326 ) -> ConstraintWrapper:
327 return self._compare("ge", other)
330class EnumerationDateVar:
331 """Date variable for enumeration baseline that evaluates constraints concretely."""
333 def __init__(self, name: str):
334 self.name = name
335 self._year = None
336 self._month = None
337 self._day = None
338 self._value = None
340 def __str__(self) -> str:
341 return f"EnumerationDateVar({self.name})"
343 def _hard_reset_value(self) -> None:
344 """★ Reset cached concrete value for lazy nodes safely."""
345 self._value = None
346 # do NOT blindly clear year/month/day for base variables; only lazy nodes call this
348 def set_value(self, year: int, month: int, day: int) -> None:
349 self._year = year
350 self._month = month
351 self._day = day
352 try:
353 self._value = Date(year, month, day)
354 except ValueError:
355 self._value = None
357 def get_value(self) -> Optional[Date]:
358 # Handle lazy operations
359 if self._value is None and hasattr(self, "_lazy_op"):
360 op_type, left, right = self._lazy_op
361 # Evaluate left first (this recursively handles nested lazy operations)
362 left_val = left.get_value()
363 if left_val is None:
364 return None
365 # Apply the operation to the left value
366 py_date = left_val.to_python_date()
367 if op_type == "add":
368 result_date = py_date + relativedelta(
369 years=right.years, months=right.months, days=right.days
370 )
371 elif op_type == "sub": 371 ↛ 379line 371 didn't jump to line 379 because the condition on line 371 was always true
372 neg_period = Period(-right.years, -right.months, -right.days)
373 result_date = py_date + relativedelta(
374 years=neg_period.years,
375 months=neg_period.months,
376 days=neg_period.days,
377 )
378 else: # defensive
379 return None
380 try:
381 result = Date.from_python_date(result_date)
382 self.set_value(result.year, result.month, result.day)
383 except ValueError:
384 # Date outside allowed range - return None instead of raising
385 # This allows the solver to properly return UNSAT
386 return None
387 return self._value
389 def to_concrete_date(self) -> Date:
390 if self._value is None:
391 raise ValueError(f"Date variable {self.name} has no concrete value")
392 return self._value
394 def _get_comparison_func(self, op: str, other: Union[Date, "EnumerationDateVar"]):
395 if isinstance(other, Date):
396 other_date = other
398 def compare():
399 self_val = self.get_value()
400 if self_val is None: 400 ↛ 401line 400 didn't jump to line 401 because the condition on line 400 was never true
401 return False
402 return getattr(self_val.to_python_date(), f"__{op}__")(
403 other_date.to_python_date()
404 )
406 return compare
407 elif isinstance(other, EnumerationDateVar): 407 ↛ 421line 407 didn't jump to line 421 because the condition on line 407 was always true
408 other_ref = other
410 def compare():
411 self_val = self.get_value()
412 other_val = other_ref.get_value()
413 if self_val is None or other_val is None: 413 ↛ 414line 413 didn't jump to line 414 because the condition on line 413 was never true
414 return False
415 return getattr(self_val.to_python_date(), f"__{op}__")(
416 other_val.to_python_date()
417 )
419 return compare
420 else:
421 raise TypeError(f"Cannot compare EnumerationDateVar with {type(other)}")
423 def _get_equality_binding(
424 self, other: Union[Date, "EnumerationDateVar"]
425 ) -> Optional[Date]:
426 if isinstance(other, Date):
427 return other
428 elif isinstance(other, EnumerationDateVar): 428 ↛ 430line 428 didn't jump to line 430 because the condition on line 428 was always true
429 return other.get_value() # may be None now; will be propagated later
430 return None
432 def __ge__(self, other: Union[Date, "EnumerationDateVar"]) -> ConstraintWrapper:
433 return ConstraintWrapper(
434 self._get_comparison_func("ge", other), var_ref=self, rhs_ref=other
435 )
437 def __le__(self, other: Union[Date, "EnumerationDateVar"]) -> ConstraintWrapper:
438 return ConstraintWrapper(
439 self._get_comparison_func("le", other), var_ref=self, rhs_ref=other
440 )
442 def __lt__(self, other: Union[Date, "EnumerationDateVar"]) -> ConstraintWrapper:
443 return ConstraintWrapper(
444 self._get_comparison_func("lt", other), var_ref=self, rhs_ref=other
445 )
447 def __gt__(self, other: Union[Date, "EnumerationDateVar"]) -> ConstraintWrapper:
448 return ConstraintWrapper(
449 self._get_comparison_func("gt", other), var_ref=self, rhs_ref=other
450 )
452 def __eq__(self, other: Union[Date, "EnumerationDateVar"]) -> ConstraintWrapper: # type: ignore[override]
453 concrete_value = self._get_equality_binding(other)
454 return ConstraintWrapper(
455 self._get_comparison_func("eq", other),
456 var_ref=self,
457 concrete_value=concrete_value,
458 rhs_ref=other,
459 )
461 def __ne__(self, other: Union[Date, "EnumerationDateVar"]) -> ConstraintWrapper: # type: ignore[override]
462 return ConstraintWrapper(
463 self._get_comparison_func("ne", other), var_ref=self, rhs_ref=other
464 )
466 def __add__(self, other: Period) -> "EnumerationDateVar":
467 if not isinstance(other, Period): 467 ↛ 468line 467 didn't jump to line 468 because the condition on line 467 was never true
468 raise TypeError(f"Cannot add {type(other)} to EnumerationDateVar")
469 result_var = EnumerationDateVar(
470 f"{self.name}_plus_{other.years}y_{other.months}m_{other.days}d"
471 )
472 result_var._lazy_op = ("add", self, other)
473 if self._value is not None:
474 py_date = self._value.to_python_date()
475 result_date = py_date + relativedelta(
476 years=other.years, months=other.months, days=other.days
477 )
478 result = Date.from_python_date(result_date)
479 result_var.set_value(result.year, result.month, result.day)
480 return result_var
482 def __sub__(self, other: Period) -> "EnumerationDateVar":
483 if not isinstance(other, Period): 483 ↛ 484line 483 didn't jump to line 484 because the condition on line 483 was never true
484 raise TypeError(f"Cannot subtract {type(other)} from EnumerationDateVar")
485 result_var = EnumerationDateVar(
486 f"{self.name}_minus_{other.years}y_{other.months}m_{other.days}d"
487 )
488 result_var._lazy_op = ("sub", self, other)
489 if self._value is not None: 489 ↛ 490line 489 didn't jump to line 490 because the condition on line 489 was never true
490 py_date = self._value.to_python_date()
491 neg_period = Period(-other.years, -other.months, -other.days)
492 result_date = py_date + relativedelta(
493 years=neg_period.years, months=neg_period.months, days=neg_period.days
494 )
495 result = Date.from_python_date(result_date)
496 result_var.set_value(result.year, result.month, result.day)
497 return result_var
499 # Expose year/month/day components for constraint building (date-only support)
500 @property
501 def year(self) -> "EnumerationDateComponent":
502 return EnumerationDateComponent(self, "year")
504 @property
505 def month(self) -> "EnumerationDateComponent":
506 return EnumerationDateComponent(self, "month")
508 @property
509 def day(self) -> "EnumerationDateComponent":
510 return EnumerationDateComponent(self, "day")
513class EnumerationDateComponent:
514 """Int-like view for a date component (year/month/day) used only in date constraints."""
516 def __init__(self, parent: EnumerationDateVar, attr: str):
517 self.parent = parent
518 self.attr = attr
520 def _get_component_value(self) -> Optional[int]:
521 """Get the current value of this component."""
522 d = self.parent.get_value()
523 if d is None: 523 ↛ 524line 523 didn't jump to line 524 because the condition on line 523 was never true
524 return None
525 return getattr(d, self.attr)
527 def _compare(
528 self,
529 op: str,
530 other: Union[int, "EnumerationDateComponent", "EnumerationComponentExpr"],
531 ):
532 def compare():
533 lhs_val = self._get_component_value()
534 if lhs_val is None: 534 ↛ 535line 534 didn't jump to line 535 because the condition on line 534 was never true
535 return False
537 # Handle EnumerationDateComponent
538 if isinstance(other, EnumerationDateComponent): 538 ↛ 539line 538 didn't jump to line 539 because the condition on line 538 was never true
539 rhs_val = other._get_component_value()
540 if rhs_val is None:
541 return False
542 return getattr(lhs_val, f"__{op}__")(rhs_val)
543 # Handle EnumerationComponentExpr
544 elif isinstance(other, EnumerationComponentExpr): 544 ↛ 545line 544 didn't jump to line 545 because the condition on line 544 was never true
545 rhs_val = other.evaluate()
546 if rhs_val is None:
547 return False
548 return getattr(lhs_val, f"__{op}__")(rhs_val)
549 # Handle int
550 else:
551 return getattr(lhs_val, f"__{op}__")(int(other))
553 return compare
555 def __eq__(self, other: Union[int, "EnumerationDateComponent", "EnumerationComponentExpr"]) -> ConstraintWrapper: # type: ignore[override]
556 return ConstraintWrapper(self._compare("eq", other))
558 def __ne__(self, other: Union[int, "EnumerationDateComponent", "EnumerationComponentExpr"]) -> ConstraintWrapper: # type: ignore[override]
559 return ConstraintWrapper(self._compare("ne", other))
561 def __lt__(
562 self, other: Union[int, "EnumerationDateComponent", "EnumerationComponentExpr"]
563 ) -> ConstraintWrapper:
564 return ConstraintWrapper(self._compare("lt", other))
566 def __le__(
567 self, other: Union[int, "EnumerationDateComponent", "EnumerationComponentExpr"]
568 ) -> ConstraintWrapper:
569 return ConstraintWrapper(self._compare("le", other))
571 def __gt__(
572 self, other: Union[int, "EnumerationDateComponent", "EnumerationComponentExpr"]
573 ) -> ConstraintWrapper:
574 return ConstraintWrapper(self._compare("gt", other))
576 def __ge__(
577 self, other: Union[int, "EnumerationDateComponent", "EnumerationComponentExpr"]
578 ) -> ConstraintWrapper:
579 return ConstraintWrapper(self._compare("ge", other))
581 # Arithmetic operations for expressions like x.year + 4
582 def __add__(self, other: int) -> "EnumerationComponentExpr":
583 if not isinstance(other, int):
584 raise TypeError(f"Cannot add {type(other)} to EnumerationDateComponent")
585 # Create a wrapper that evaluates the component value and adds the constant
586 base_var = EnumerationComponentVar(
587 f"{self.parent.name}_{self.attr}",
588 1900 if self.attr == "year" else 1,
589 2100 if self.attr == "year" else (12 if self.attr == "month" else 31),
590 self.attr,
591 )
592 # Store reference to the parent component for lazy evaluation
593 base_var._parent_component = self
594 return EnumerationComponentExpr(base_var, "add", other)
596 def __sub__(
597 self, other: Union[int, "EnumerationDateComponent"]
598 ) -> "EnumerationComponentExpr":
599 # Handle subtraction of another EnumerationDateComponent (e.g., y.year - x.year)
600 if isinstance(other, EnumerationDateComponent):
601 base_var = EnumerationComponentVar(
602 f"{self.parent.name}_{self.attr}",
603 1900 if self.attr == "year" else 1,
604 2100 if self.attr == "year" else (12 if self.attr == "month" else 31),
605 self.attr,
606 )
607 base_var._parent_component = self
608 expr = EnumerationComponentExpr(base_var, "sub_component", 0)
609 expr._other_component = other
610 return expr
611 # Handle subtraction of an integer
612 elif isinstance(other, int):
613 base_var = EnumerationComponentVar(
614 f"{self.parent.name}_{self.attr}",
615 1900 if self.attr == "year" else 1,
616 2100 if self.attr == "year" else (12 if self.attr == "month" else 31),
617 self.attr,
618 )
619 base_var._parent_component = self
620 return EnumerationComponentExpr(base_var, "sub", other)
621 else:
622 raise TypeError(
623 f"Cannot subtract {type(other)} from EnumerationDateComponent"
624 )
626 def __mul__(self, other: int) -> "EnumerationComponentExpr":
627 if not isinstance(other, int):
628 raise TypeError(
629 f"Cannot multiply {type(other)} by EnumerationDateComponent"
630 )
631 base_var = EnumerationComponentVar(
632 f"{self.parent.name}_{self.attr}",
633 1900 if self.attr == "year" else 1,
634 2100 if self.attr == "year" else (12 if self.attr == "month" else 31),
635 self.attr,
636 )
637 base_var._parent_component = self
638 return EnumerationComponentExpr(base_var, "mul", other)
640 def __mod__(self, other: int) -> "EnumerationComponentExpr":
641 if not isinstance(other, int):
642 raise TypeError(
643 f"Cannot compute modulo with {type(other)} on EnumerationDateComponent"
644 )
645 base_var = EnumerationComponentVar(
646 f"{self.parent.name}_{self.attr}",
647 1900 if self.attr == "year" else 1,
648 2100 if self.attr == "year" else (12 if self.attr == "month" else 31),
649 self.attr,
650 )
651 base_var._parent_component = self
652 return EnumerationComponentExpr(base_var, "mod", other)
654 def __truediv__(self, other: int) -> "EnumerationComponentExpr":
655 """Integer division using / operator (implements floor division semantics)."""
656 if not isinstance(other, int):
657 raise TypeError(f"Cannot divide {type(other)} by EnumerationDateComponent")
658 base_var = EnumerationComponentVar(
659 f"{self.parent.name}_{self.attr}",
660 1900 if self.attr == "year" else 1,
661 2100 if self.attr == "year" else (12 if self.attr == "month" else 31),
662 self.attr,
663 )
664 base_var._parent_component = self
665 return EnumerationComponentExpr(base_var, "floordiv", other)
668class EnumerationSolver:
669 """Solver that enumerates all valid dates and checks constraints."""
671 MIN_DATE = date(1900, 3, 1)
672 MAX_DATE = date(2100, 2, 28)
674 def __init__(self, timeout_ms: int = 60000):
675 self.date_vars: Dict[str, EnumerationDateVar] = {}
676 self.component_vars: Dict[str, EnumerationComponentVar] = (
677 {}
678 ) # Component variables - e.x. Date(y, 1, 1)
679 self.constraints: List[Any] = []
680 self.timeout_ms = timeout_ms
681 self._cached_valid_dates: Optional[List[date]] = None
683 def add_date_var(self, name: str) -> EnumerationDateVar:
684 """Declare a new symbolic date variable.
686 The variable will enumerate all valid dates in the allowed range.
688 Args:
689 name: Variable name (must be unique)
691 Returns:
692 The created EnumerationDateVar
694 Raises:
695 ValueError: If a variable with this name already exists
696 """
697 if name in self.date_vars: 697 ↛ 698line 697 didn't jump to line 698 because the condition on line 697 was never true
698 raise ValueError(f"Date variable '{name}' already declared")
700 date_var = EnumerationDateVar(name)
701 self.date_vars[name] = date_var
702 return date_var
704 def add_year_var(self, name: str) -> EnumerationComponentVar:
705 """Declare a symbolic year variable that enumerates from 1900 to 2100.
707 Raises:
708 ValueError: If a component variable with this name already exists
709 """
710 if name in self.component_vars: 710 ↛ 711line 710 didn't jump to line 711 because the condition on line 710 was never true
711 raise ValueError(f"Component variable '{name}' already declared")
713 var = EnumerationComponentVar(name, 1900, 2100, "year")
714 self.component_vars[name] = var
715 return var
717 def add_month_var(self, name: str) -> EnumerationComponentVar:
718 """Declare a symbolic month variable that enumerates from 1 to 12.
720 Raises:
721 ValueError: If a component variable with this name already exists
722 """
723 if name in self.component_vars: 723 ↛ 724line 723 didn't jump to line 724 because the condition on line 723 was never true
724 raise ValueError(f"Component variable '{name}' already declared")
726 var = EnumerationComponentVar(name, 1, 12, "month")
727 self.component_vars[name] = var
728 return var
730 def add_day_var(self, name: str) -> EnumerationComponentVar:
731 """Declare a symbolic day variable that enumerates from 1 to 31.
733 Raises:
734 ValueError: If a component variable with this name already exists
735 """
736 if name in self.component_vars: 736 ↛ 737line 736 didn't jump to line 737 because the condition on line 736 was never true
737 raise ValueError(f"Component variable '{name}' already declared")
739 var = EnumerationComponentVar(name, 1, 31, "day")
740 self.component_vars[name] = var
741 return var
743 def add_int_var(
744 self,
745 name: str,
746 min_value: int = None,
747 max_value: int = None,
748 component_type: str = None,
749 ) -> EnumerationComponentVar:
750 """Declare a symbolic integer variable for use in Date() constructors.
752 Integer variables should only be used in Date() constructors (e.g., Date(l, 1, 1)).
753 The bounds are automatically set based on the component type:
754 - 'year': 1900-2100
755 - 'month': 1-12
756 - 'day': 1-31
758 Args:
759 name: Variable name (must be unique)
760 min_value: Optional minimum value (overrides component_type defaults if provided)
761 max_value: Optional maximum value (overrides component_type defaults if provided)
762 component_type: Optional component type ('year', 'month', 'day'). If provided,
763 sets appropriate bounds. If not provided, uses min_value/max_value
764 or defaults to 0-8000.
766 Returns:
767 The created EnumerationComponentVar
769 Raises:
770 ValueError: If a component variable with this name already exists
771 """
772 if name in self.component_vars:
773 raise ValueError(f"Integer variable '{name}' already declared")
775 # Set bounds based on component type if provided
776 if component_type == "year":
777 if min_value is None:
778 min_value = 1900
779 if max_value is None:
780 max_value = 2100
781 elif component_type == "month":
782 if min_value is None:
783 min_value = 1
784 if max_value is None:
785 max_value = 12
786 elif component_type == "day":
787 if min_value is None:
788 min_value = 1
789 if max_value is None:
790 max_value = 31
791 else:
792 # Default bounds (should not be used for Date() components)
793 if min_value is None:
794 min_value = 0
795 if max_value is None:
796 max_value = 8000
798 var = EnumerationComponentVar(
799 name, min_value, max_value, component_type or "int"
800 )
801 self.component_vars[name] = var
802 return var
804 def SymbolicDate(self, year, month, day) -> EnumerationDateVar:
805 """Create a date with symbolic components.
807 Args:
808 year: int, EnumerationComponentVar, or EnumerationComponentExpr
809 month: int, EnumerationComponentVar, or EnumerationComponentExpr
810 day: int, EnumerationComponentVar, or EnumerationComponentExpr
812 Returns:
813 EnumerationDateVar that will be enumerated based on symbolic components
815 Example:
816 year_var = solver.add_year_var("y")
817 d = solver.SymbolicDate(year_var, 1, 1) # Only enumerates years
818 solver.add_constraint(x < d)
819 """
820 # Generate a unique name for this symbolic date
821 symbolic_parts = []
822 if isinstance(year, (EnumerationComponentVar, EnumerationComponentExpr)):
823 symbolic_parts.append("y")
824 if isinstance(month, (EnumerationComponentVar, EnumerationComponentExpr)):
825 symbolic_parts.append("m")
826 if isinstance(day, (EnumerationComponentVar, EnumerationComponentExpr)):
827 symbolic_parts.append("d")
829 name = f"symdate_{''.join(symbolic_parts)}_{len(self.date_vars)}"
830 date_var = EnumerationDateVar(name)
832 # Store component specifications (can be int, EnumerationComponentVar, or EnumerationComponentExpr)
833 date_var._year_spec = year
834 date_var._month_spec = month
835 date_var._day_spec = day
837 self.date_vars[name] = date_var
838 return date_var
840 def add_constraint(self, constraint: Any) -> None:
841 self.constraints.append(constraint)
843 def Or(self, *args) -> ConstraintWrapper:
844 """Wrapper for Z3's Or() that creates a ConstraintWrapper with or_constraints."""
845 return Or_enumeration(*args)
847 def And(self, *args) -> ConstraintWrapper:
848 """Wrapper for Z3's And() that creates a ConstraintWrapper."""
849 return And_enumeration(*args)
851 def Not(self, arg) -> ConstraintWrapper:
852 """Wrapper for Z3's Not() that creates a ConstraintWrapper."""
853 return Not_enumeration(arg)
855 def Implies(self, antecedent, consequent) -> ConstraintWrapper:
856 """Wrapper for Z3's Implies() that creates a ConstraintWrapper."""
857 return Implies_enumeration(antecedent, consequent)
859 def get_execution_context(self) -> Dict[str, Any]:
860 """Get execution context dictionary for running generated constraint code.
862 This sets up Or, And, Not, Implies to use the enumeration baseline's
863 wrapper functions instead of Z3's functions, so boolean operators work
864 correctly with ConstraintWrapper objects.
866 Returns:
867 Dictionary suitable for use as exec_globals when executing generated code
868 """
870 # Create a mock z3 module with our wrapper functions
871 class MockZ3:
872 Or = self.Or
873 And = self.And
874 Not = self.Not
875 Implies = self.Implies
876 Int = lambda *args: None # Not used by enumeration baseline solving
877 Bool = lambda *args: None # Not used by enumeration baseline solving
879 # Override __import__ to return our mock z3 module
880 original_import = builtins.__import__
882 def mock_import(name, *args, **kwargs):
883 if name == "z3":
884 return MockZ3()
885 return original_import(name, *args, **kwargs)
887 return {
888 "Date": Date,
889 "Period": Period,
890 "SymbolicDate": self.SymbolicDate,
891 "DateSATBuilder": lambda: self,
892 "builder": self,
893 "__builtins__": {**builtins.__dict__, "__import__": mock_import},
894 "And": self.And,
895 "Or": self.Or,
896 "Not": self.Not,
897 "Implies": self.Implies,
898 }
900 def check(self) -> str:
901 try:
902 solution = self._find_solution()
903 return "sat" if solution is not None else "unsat"
904 except TimeoutError:
905 return "timeout" # ★ cleaner status
907 def solve(self) -> Dict[str, Any]:
908 try:
909 solution = self._find_solution()
910 if solution is not None: 910 ↛ 913line 910 didn't jump to line 913 because the condition on line 910 was always true
911 return {"status": "sat", "dates": solution}
912 else:
913 return {"status": "unsat", "dates": {}}
914 except TimeoutError as e:
915 return {"status": "timeout", "reason": str(e), "dates": {}}
917 def model(self) -> Dict[str, Any]:
918 out = self.solve()
919 return out
921 def get_concrete_dates(self) -> Dict[str, Date]:
922 out = self.solve()
923 return out.get("dates", {})
925 def to_smt2(self) -> str:
926 return "; Enumeration baseline - no SMT-LIB output"
928 def get_assertions(self) -> list:
929 return self.constraints
931 # ------------------------- internals -------------------------
933 def _find_solution(self) -> Optional[Dict[str, Date]]:
934 """Brute-force enumeration: enumerate all possible dates for all variables.
936 Pure enumeration baseline - no optimizations. Enumerates all combinations
937 of dates for all base variables and checks which satisfy the constraints.
939 Supports both full date variables and dates with symbolic components.
940 For dates with symbolic components (e.g., Date(year_var, 1, 1)), only
941 the symbolic components are enumerated, making it much more efficient.
943 If no variables are declared, evaluate constraints concretely using datetime.
944 Otherwise, enumerate all possible date combinations for all declared variables.
945 """
946 var_names = list(self.date_vars.keys())
948 # If no variables, evaluate constraints concretely using datetime
949 if not var_names: 949 ↛ 950line 949 didn't jump to line 950 because the condition on line 949 was never true
950 return {} if self._evaluate_constraints({}) else None
952 # Register intermediate lazy nodes (created by operations like x + Period)
953 # These are derived variables, not base variables
954 for c in self.constraints:
955 if isinstance(c, ConstraintWrapper): 955 ↛ 954line 955 didn't jump to line 954 because the condition on line 955 was always true
956 targets = c.or_constraints if c.or_constraints is not None else [c]
957 for sub_c in targets:
958 # Only register lazy nodes (have _lazy_op), not undeclared base variables
959 if sub_c.var_ref is not None and isinstance(
960 sub_c.var_ref, EnumerationDateVar
961 ):
962 if ( 962 ↛ 966line 962 didn't jump to line 966 because the condition on line 962 was never true
963 hasattr(sub_c.var_ref, "_lazy_op")
964 and sub_c.var_ref.name not in self.date_vars
965 ):
966 self.date_vars[sub_c.var_ref.name] = sub_c.var_ref
967 if sub_c.rhs_ref is not None and isinstance(
968 sub_c.rhs_ref, EnumerationDateVar
969 ):
970 if (
971 hasattr(sub_c.rhs_ref, "_lazy_op")
972 and sub_c.rhs_ref.name not in self.date_vars
973 ):
974 self.date_vars[sub_c.rhs_ref.name] = sub_c.rhs_ref
976 # Get all base variables (skip intermediate lazy nodes)
977 # NO BINDING OPTIMIZATION - enumerate all base variables
978 base_vars: List[str] = []
979 for name in list(self.date_vars.keys()):
980 var = self.date_vars[name]
981 # skip intermediate lazy nodes (they have _lazy_op attribute)
982 if hasattr(var, "_lazy_op"):
983 continue
984 base_vars.append(name)
986 if not base_vars: 986 ↛ 988line 986 didn't jump to line 988 because the condition on line 986 was never true
987 # No base variables to enumerate - evaluate constraints with empty assignment
988 return {} if self._evaluate_constraints({}) else None
990 # Build candidate lists for each variable
991 # Variables with symbolic components get specialized enumeration
992 candidate_lists = []
993 for vname in base_vars:
994 var = self.date_vars[vname]
995 candidates = self._generate_candidates_for_var(var)
996 candidate_lists.append(candidates)
998 # Calculate search space
999 space = 1
1000 for candidates in candidate_lists:
1001 space *= len(candidates)
1002 if space > 1_000_000:
1003 print(f"Warning: Large search space ({space} combinations).")
1005 start = time.time()
1006 timeout_s = self.timeout_ms / 1000.0
1008 # Enumerate all combinations - pure brute force
1009 for combo in itertools.product(*candidate_lists): 1009 ↛ 1096line 1009 didn't jump to line 1096 because the loop on line 1009 didn't complete
1010 if (time.time() - start) > timeout_s:
1011 raise TimeoutError(
1012 f"Enumeration timeout after {time.time() - start:.2f}s (limit: {timeout_s:.2f}s)"
1013 )
1015 # Create assignment: map each variable to a date
1016 assignment: Dict[str, Date] = {}
1017 valid_assignment = True
1019 for vname, candidate in zip(base_vars, combo):
1020 var = self.date_vars[vname]
1022 # Handle symbolic component dates
1023 if hasattr(var, "_year_spec"):
1024 # Check if any component is symbolic
1025 has_symbolic = (
1026 isinstance(
1027 var._year_spec,
1028 (EnumerationComponentVar, EnumerationComponentExpr),
1029 )
1030 or isinstance(
1031 var._month_spec,
1032 (EnumerationComponentVar, EnumerationComponentExpr),
1033 )
1034 or isinstance(
1035 var._day_spec,
1036 (EnumerationComponentVar, EnumerationComponentExpr),
1037 )
1038 )
1040 if has_symbolic: 1040 ↛ 1078line 1040 didn't jump to line 1078 because the condition on line 1040 was always true
1041 # candidate is a tuple (year, month, day, base_year, base_month, base_day)
1042 # The base values are for setting the component variables
1043 year, month, day, base_year, base_month, base_day = candidate
1044 # Set component variable values (use base values, not expression results)
1045 if isinstance(
1046 var._year_spec,
1047 (EnumerationComponentVar, EnumerationComponentExpr),
1048 ):
1049 base_var = self._get_base_component_var(var._year_spec)
1050 if base_var: 1050 ↛ 1052line 1050 didn't jump to line 1052 because the condition on line 1050 was always true
1051 base_var.set_value(base_year)
1052 if isinstance(
1053 var._month_spec,
1054 (EnumerationComponentVar, EnumerationComponentExpr),
1055 ):
1056 base_var = self._get_base_component_var(var._month_spec)
1057 if base_var: 1057 ↛ 1059line 1057 didn't jump to line 1059 because the condition on line 1057 was always true
1058 base_var.set_value(base_month)
1059 if isinstance(
1060 var._day_spec,
1061 (EnumerationComponentVar, EnumerationComponentExpr),
1062 ):
1063 base_var = self._get_base_component_var(var._day_spec)
1064 if base_var: 1064 ↛ 1067line 1064 didn't jump to line 1067 because the condition on line 1064 was always true
1065 base_var.set_value(base_day)
1067 try:
1068 date_obj = Date(year, month, day)
1069 assignment[vname] = date_obj
1070 var.set_value(year, month, day)
1071 except ValueError:
1072 # Invalid date (e.g., Feb 31), skip this combination
1073 valid_assignment = False
1074 break
1075 else:
1076 # SymbolicDate but no symbolic components - shouldn't happen
1077 # Regular date variable - candidate is already a python date
1078 assignment[vname] = Date(
1079 candidate.year, candidate.month, candidate.day
1080 )
1081 var.set_value(candidate.year, candidate.month, candidate.day)
1082 else:
1083 # Regular date variable - candidate is already a python date
1084 assignment[vname] = Date(
1085 candidate.year, candidate.month, candidate.day
1086 )
1087 var.set_value(candidate.year, candidate.month, candidate.day)
1089 if not valid_assignment:
1090 continue
1092 # Evaluate constraints with this assignment
1093 if self._evaluate_constraints(assignment):
1094 return assignment
1096 return None
1098 def _generate_all_valid_dates(self) -> List[date]:
1099 if self._cached_valid_dates is None:
1100 dates: List[date] = []
1101 current = self.MIN_DATE
1102 while current <= self.MAX_DATE:
1103 try:
1104 Date(current.year, current.month, current.day)
1105 dates.append(current)
1106 except ValueError:
1107 pass
1108 current += timedelta(days=1)
1109 self._cached_valid_dates = dates
1110 return self._cached_valid_dates
1112 def _get_base_component_var(self, component) -> Optional[EnumerationComponentVar]:
1113 """Get the base component variable from a component (handles expressions too)."""
1114 if isinstance(component, EnumerationComponentVar):
1115 return component
1116 elif isinstance(component, EnumerationComponentExpr): 1116 ↛ 1118line 1116 didn't jump to line 1118 because the condition on line 1116 was always true
1117 return component.get_base_var()
1118 return None
1120 def _evaluate_component(self, component) -> Optional[int]:
1121 """Evaluate a component to get its integer value."""
1122 if isinstance(component, int):
1123 return component
1124 elif isinstance(component, EnumerationComponentVar):
1125 return component.get_value()
1126 elif isinstance(component, EnumerationComponentExpr):
1127 return component.evaluate()
1128 return None
1130 def _generate_candidates_for_var(
1131 self, var: EnumerationDateVar
1132 ) -> List[Union[date, Tuple[int, int, int, int, int, int]]]:
1133 """Generate candidate values for a variable.
1135 For regular date variables, returns list of python dates.
1136 For symbolic component dates, returns list of (year, month, day, base_year, base_month, base_day) tuples.
1137 The base values are what the underlying component variables should be set to.
1138 """
1139 # Check if this is a symbolic component date
1140 if not hasattr(var, "_year_spec"):
1141 # Regular date variable - enumerate all valid dates
1142 return self._generate_all_valid_dates()
1144 # Check if any component is symbolic
1145 has_symbolic = (
1146 isinstance(
1147 var._year_spec, (EnumerationComponentVar, EnumerationComponentExpr)
1148 )
1149 or isinstance(
1150 var._month_spec, (EnumerationComponentVar, EnumerationComponentExpr)
1151 )
1152 or isinstance(
1153 var._day_spec, (EnumerationComponentVar, EnumerationComponentExpr)
1154 )
1155 )
1157 if not has_symbolic: 1157 ↛ 1159line 1157 didn't jump to line 1159 because the condition on line 1157 was never true
1158 # SymbolicDate but no symbolic components - shouldn't happen
1159 return self._generate_all_valid_dates()
1161 # Symbolic component date - enumerate only symbolic components
1162 year_ranges = self._get_component_ranges(var._year_spec, "year")
1163 month_ranges = self._get_component_ranges(var._month_spec, "month")
1164 day_ranges = self._get_component_ranges(var._day_spec, "day")
1166 # Generate all combinations of (year, month, day, base_year, base_month, base_day)
1167 # Note: We don't validate here, validation happens during enumeration
1168 # This allows us to skip invalid dates like Feb 31
1169 candidates = []
1170 for y_tuple in year_ranges:
1171 for m_tuple in month_ranges:
1172 for d_tuple in day_ranges:
1173 y_val, y_base = y_tuple
1174 m_val, m_base = m_tuple
1175 d_val, d_base = d_tuple
1176 candidates.append((y_val, m_val, d_val, y_base, m_base, d_base))
1178 return candidates
1180 def _get_component_ranges(
1181 self, component_spec, component_type: str
1182 ) -> List[Tuple[int, int]]:
1183 """Get the range of values for a date component.
1185 Args:
1186 component_spec: int, EnumerationComponentVar, or EnumerationComponentExpr
1187 component_type: 'year', 'month', or 'day' (for fallback ranges)
1189 Returns list of (evaluated_value, base_value) tuples.
1190 - evaluated_value: the actual value to use in the Date() constructor
1191 - base_value: the value to set in the underlying EnumerationComponentVar
1192 """
1193 if isinstance(
1194 component_spec, (EnumerationComponentVar, EnumerationComponentExpr)
1195 ):
1196 # Symbolic component - get base variable and enumerate its range
1197 base_var = self._get_base_component_var(component_spec)
1198 if base_var: 1198 ↛ 1241line 1198 didn't jump to line 1241 because the condition on line 1198 was always true
1199 base_range = range(base_var.min_val, base_var.max_val + 1)
1201 if isinstance(component_spec, EnumerationComponentExpr):
1202 # For expressions like year_var + 1, enumerate base variable
1203 # and compute the expression result
1204 results = []
1205 for base_val in base_range:
1206 if component_spec.op == "add": 1206 ↛ 1208line 1206 didn't jump to line 1208 because the condition on line 1206 was always true
1207 eval_val = base_val + component_spec.constant
1208 elif component_spec.op == "sub":
1209 eval_val = base_val - component_spec.constant
1210 elif component_spec.op == "mul":
1211 eval_val = base_val * component_spec.constant
1212 elif component_spec.op == "mod":
1213 if component_spec.constant == 0:
1214 continue # Skip division by zero
1215 eval_val = base_val % component_spec.constant
1216 elif component_spec.op == "floordiv":
1217 if component_spec.constant == 0:
1218 continue # Skip division by zero
1219 eval_val = base_val // component_spec.constant
1220 elif component_spec.op == "sub_component":
1221 # This is a subtraction of another component (e.g., y.year - x.year)
1222 # We can't enumerate this directly since it depends on two different parents
1223 # Return a placeholder - the actual value will be computed during constraint evaluation
1224 # For enumeration, we'll use a wide range that covers all possible differences
1225 # The actual difference will be computed when both parent components have values
1226 # Use a conservative range based on component type
1227 if component_type == "year":
1228 # Year differences can range from -200 to 200 (2100 - 1900)
1229 eval_val = base_val # Placeholder, will be evaluated at constraint time
1230 else:
1231 eval_val = base_val
1232 else:
1233 eval_val = base_val
1234 results.append((eval_val, base_val))
1235 return results
1236 else:
1237 # Simple variable, base value and evaluated value are the same
1238 return [(v, v) for v in base_range]
1240 # Concrete component (int) - single value, no base variable
1241 if isinstance(component_spec, int): 1241 ↛ 1245line 1241 didn't jump to line 1245 because the condition on line 1241 was always true
1242 return [(component_spec, component_spec)]
1244 # Fallback - shouldn't happen but be safe
1245 if component_type == "year":
1246 vals = list(range(1900, 2101))
1247 elif component_type == "month":
1248 vals = list(range(1, 13))
1249 else: # day
1250 vals = list(range(1, 32))
1251 return [(v, v) for v in vals]
1253 def _evaluate_constraints(self, assignment: Dict[str, Date]) -> bool:
1254 try:
1255 # Register intermediate lazy nodes for evaluation
1256 for c in self.constraints:
1257 if isinstance(c, ConstraintWrapper): 1257 ↛ 1256line 1257 didn't jump to line 1256 because the condition on line 1257 was always true
1258 # Handle OR constraints - check all sub-constraints
1259 targets = c.or_constraints if c.or_constraints is not None else [c]
1260 for sub_c in targets:
1261 # Only register lazy nodes, not undeclared base variables
1262 if sub_c.var_ref is not None and isinstance(
1263 sub_c.var_ref, EnumerationDateVar
1264 ):
1265 if ( 1265 ↛ 1269line 1265 didn't jump to line 1269 because the condition on line 1265 was never true
1266 hasattr(sub_c.var_ref, "_lazy_op")
1267 and sub_c.var_ref.name not in self.date_vars
1268 ):
1269 self.date_vars[sub_c.var_ref.name] = sub_c.var_ref
1270 if sub_c.rhs_ref is not None and isinstance(
1271 sub_c.rhs_ref, EnumerationDateVar
1272 ):
1273 if ( 1273 ↛ 1277line 1273 didn't jump to line 1277 because the condition on line 1273 was never true
1274 hasattr(sub_c.rhs_ref, "_lazy_op")
1275 and sub_c.rhs_ref.name not in self.date_vars
1276 ):
1277 self.date_vars[sub_c.rhs_ref.name] = sub_c.rhs_ref
1279 # Reset lazy nodes so they recompute from base values
1280 for _, var in list(self.date_vars.items()):
1281 if hasattr(var, "_lazy_op"):
1282 var._hard_reset_value() # ★
1284 # Set all base variable values for this assignment
1285 for name, val in assignment.items():
1286 if name in self.date_vars and isinstance(val, Date): 1286 ↛ 1285line 1286 didn't jump to line 1285 because the condition on line 1286 was always true
1287 self.date_vars[name].set_value(val.year, val.month, val.day)
1289 # Evaluate
1290 for c in self.constraints:
1291 if isinstance(c, bool): 1291 ↛ 1292line 1291 didn't jump to line 1292 because the condition on line 1291 was never true
1292 if not c:
1293 return False
1294 elif isinstance(c, ConstraintWrapper): 1294 ↛ 1297line 1294 didn't jump to line 1297 because the condition on line 1294 was always true
1295 if not c.evaluate():
1296 return False
1297 elif callable(c):
1298 if not c():
1299 return False
1300 else:
1301 # last resort: bool() — but many types (like ConstraintWrapper) forbid __bool__
1302 if not bool(c):
1303 return False
1304 return True
1305 except (ValueError, TypeError):
1306 return False