Coverage for datesat / symbolic_int / naive_int.py: 81.9%
161 statements
« prev ^ index » next coverage.py v7.13.4, created at 2026-02-10 23:47 +0000
1"""
2Naive DateSAT implementation using component-based representation.
4This module implements the naive approach where dates are represented
5as separate year, month, and day variables, and period arithmetic is done
6component-wise with proper normalization.
7"""
9from typing import List, Tuple, Union
11from z3 import (
12 And,
13 ArithRef,
14 BoolRef,
15 CheckSatResult,
16 If,
17 Int,
18 IntVal,
19 ModelRef,
20 Not,
21 Optimize,
22 Or,
23 Solver,
24 sat,
25 unsat,
26)
27from ..core import Date, Period
29_NONLEAP_PREFIX = [0, 31, 59, 90, 120, 151, 181, 212, 243, 273, 304, 334]
30_LEAP_PREFIX = [0, 31, 60, 91, 121, 152, 182, 213, 244, 274, 305, 335]
31# -------------------------------
32# Epoch binding: 2000-03-01
33# -------------------------------
34# _ORD_EPOCH = to_ordinal(IntVal(2000), IntVal(3), IntVal(1)) # original ground Z3 term
35_ORD_EPOCH = IntVal(730179) # precomputed ordinal of 2000-03-01 (0001-01-01 = 0)
38def is_leap(year) -> BoolRef:
39 """Check if a year is a leap year."""
40 return Or(And(year % 4 == 0, year % 100 != 0), year % 400 == 0)
43def days_in_month(year, month) -> ArithRef:
44 """Get the number of days in a month, accounting for leap years."""
45 return If(
46 month == 2,
47 If(is_leap(year), 29, 28),
48 If(Or(month == 4, month == 6, month == 9, month == 11), 30, 31),
49 )
52def normalize_month(y, m) -> Tuple[ArithRef, ArithRef]:
53 """
54 NormMonth(y,m) = (y + ((m-1) div 12), ((m-1) mod 12) + 1)
55 Works for concrete and symbolic inputs.
56 """
57 t = m - 1
58 q = t / 12 # Z3 integer division
59 r = t % 12 # Z3 modulo
60 return y + q, r + 1
62def eom_clamp(year, month, day) -> ArithRef:
63 """
64 End-of-month clamp: ensure day is valid for the given year/month.
65 """
66 max_day = days_in_month(year, month)
67 return If(day < 1, 1, If(day > max_day, max_day, day))
69def add_days_componentwise(y, m, d, delta_days: int) -> Tuple[ArithRef, ArithRef, ArithRef]:
70 """
71 Add a concrete day offset by iteratively carrying into months/years.
72 """
73 if delta_days == 0:
74 return y, m, d
76 one = IntVal(1)
77 twelve = IntVal(12)
78 cur_y, cur_m, cur_d = y, m, d
80 if delta_days > 0:
81 for _ in range(delta_days):
82 max_day = days_in_month(cur_y, cur_m)
83 next_day = cur_d + one
84 overflow = next_day > max_day
85 month_plus_one = cur_m + one
86 month_wrap = month_plus_one > twelve
88 new_day = If(overflow, one, next_day)
89 new_month = If(
90 overflow,
91 If(month_wrap, one, month_plus_one),
92 cur_m,
93 )
94 new_year = If(
95 overflow,
96 If(month_wrap, cur_y + one, cur_y),
97 cur_y,
98 )
100 cur_y, cur_m, cur_d = new_year, new_month, new_day
101 return cur_y, cur_m, cur_d
103 for _ in range(-delta_days):
104 prev_day = cur_d - one
105 underflow = prev_day < one
106 month_minus_one = cur_m - one
107 month_wrap = month_minus_one < one
109 prev_year = If(month_wrap, cur_y - one, cur_y)
110 normalized_month = If(month_wrap, twelve, month_minus_one)
111 prev_max_day = days_in_month(prev_year, normalized_month)
113 new_day = If(underflow, prev_max_day, prev_day)
114 new_month = If(underflow, normalized_month, cur_m)
115 new_year = If(underflow, prev_year, cur_y)
117 cur_y, cur_m, cur_d = new_year, new_month, new_day
119 return cur_y, cur_m, cur_d
122class DateVar:
123 """Symbolic date variable for naive implementation."""
125 def __init__(self, name: str):
126 """Create a symbolic date variable."""
127 self.name = name
128 # Create separate Z3 integer variables for year, month, day
129 self.year = Int(f"{name}_year")
130 self.month = Int(f"{name}_month")
131 self.day = Int(f"{name}_day")
132 # Solver reference for adding bounds to intermediate dates (set after creation if needed)
133 self._solver = None
135 def __str__(self) -> str:
136 return f"DateVar({self.name})"
138 def to_concrete_date(self, model: ModelRef) -> Date:
139 """Convert Z3 model to concrete Date."""
140 year = model.evaluate(self.year, model_completion=True).as_long()
141 month = model.evaluate(self.month, model_completion=True).as_long()
142 day = model.evaluate(self.day, model_completion=True).as_long()
143 return Date(year, month, day)
145 def __ge__(self, other) -> BoolRef:
146 """Support x >= date comparison."""
147 if isinstance(other, (Date, DateVar)): 147 ↛ 159line 147 didn't jump to line 159 because the condition on line 147 was always true
148 return Or(
149 self.year > other.year,
150 And(
151 self.year == other.year,
152 Or(
153 self.month > other.month,
154 And(self.month == other.month, self.day >= other.day),
155 ),
156 ),
157 )
158 else:
159 raise TypeError(f"Cannot compare DateVar with {type(other)}")
161 def __le__(self, other) -> BoolRef:
162 """Support x <= date comparison."""
163 if isinstance(other, (Date, DateVar)): 163 ↛ 175line 163 didn't jump to line 175 because the condition on line 163 was always true
164 return Or(
165 self.year < other.year,
166 And(
167 self.year == other.year,
168 Or(
169 self.month < other.month,
170 And(self.month == other.month, self.day <= other.day),
171 ),
172 ),
173 )
174 else:
175 raise TypeError(f"Cannot compare DateVar with {type(other)}")
177 def __lt__(self, other) -> BoolRef:
178 """Support x < date comparison."""
179 if isinstance(other, (Date, DateVar)): 179 ↛ 182line 179 didn't jump to line 182 because the condition on line 179 was always true
180 return Not(self.__ge__(other))
181 else:
182 raise TypeError(f"Cannot compare DateVar with {type(other)}")
184 def __gt__(self, other) -> BoolRef:
185 """Support x > date comparison."""
186 if isinstance(other, (Date, DateVar)): 186 ↛ 189line 186 didn't jump to line 189 because the condition on line 186 was always true
187 return Not(self.__le__(other))
188 else:
189 raise TypeError(f"Cannot compare DateVar with {type(other)}")
191 def __eq__(self, other) -> BoolRef:
192 """Support x == date comparison."""
193 if isinstance(other, (Date, DateVar)): 193 ↛ 200line 193 didn't jump to line 200 because the condition on line 193 was always true
194 return And(
195 self.year == other.year,
196 self.month == other.month,
197 self.day == other.day,
198 )
199 else:
200 raise TypeError(f"Cannot compare DateVar with {type(other)}")
202 def __ne__(self, other) -> BoolRef:
203 """Support x != date comparison."""
204 if isinstance(other, (Date, DateVar)): 204 ↛ 207line 204 didn't jump to line 207 because the condition on line 204 was always true
205 return Not(self.__eq__(other))
206 else:
207 raise TypeError(f"Cannot compare DateVar with {type(other)}")
209 def _add_bounds(self) -> None:
210 """Add date validation bounds to this DateVar if solver is available."""
211 if self._solver is None: 211 ↛ 212line 211 didn't jump to line 212 because the condition on line 211 was never true
212 return
214 # Add comprehensive date validation constraints
215 # Valid range is 1900-03-01 to 2100-02-28
216 self._solver.add(
217 Or(
218 # 1900-03-01 to 1900-12-31
219 And(
220 self.year == 1900,
221 self.month >= 3,
222 self.month <= 12,
223 self.day >= 1,
224 self.day <= days_in_month(self.year, self.month),
225 ),
226 # 1901-01-01 to 2099-12-31
227 And(
228 self.year >= 1901,
229 self.year <= 2099,
230 self.month >= 1,
231 self.month <= 12,
232 self.day >= 1,
233 self.day <= days_in_month(self.year, self.month),
234 ),
235 # 2100-01-01 to 2100-02-28
236 And(
237 self.year == 2100,
238 self.month >= 1,
239 self.month <= 2,
240 self.day >= 1,
241 self.day <= days_in_month(self.year, self.month),
242 ),
243 )
244 )
246 def __add__(self, other) -> 'DateVar':
247 """
248 DateVar + Period following naive semantics:
249 1) Combine Y and M (normalize months into 1..12 with year carry)
250 2) Apply EOM clamp: day := min(original_day, days_in_month(new_year,new_month))
251 3) Add D days via iterative day carry (month/year rollover as required)
253 Optimizations:
254 - Fast path: If period is days-only (years=0, months=0), skip month normalization
255 """
256 if isinstance(other, Period): 256 ↛ 294line 256 didn't jump to line 294 because the condition on line 256 was always true
257 result = DateVar(f"{self.name}_plus")
259 # Extract period components
260 period_years = other.years
261 period_months = other.months
262 period_days = other.days
264 # Fast path: days-only period (skip month normalization and EOM clamp)
265 # Check at Python level since Period components are concrete integers
266 if period_years == 0 and period_months == 0:
267 # Days-only path: directly add days
268 y2, m2, d2 = add_days_componentwise(
269 self.year, self.month, self.day, period_days
270 )
271 else:
272 # Full path: Step 1: Combine Y and M (normalize months into 1..12 with year carry)
273 # Convert period years to months and combine with period months
274 period_total_months = IntVal(period_years) * IntVal(12) + IntVal(period_months)
275 # Add to current month and normalize
276 total_months = self.month + period_total_months
277 year_carry, m1 = normalize_month(IntVal(0), total_months)
278 y1 = self.year + year_carry
280 # Step 2: Apply EOM clamp: day := min(original_day, days_in_month(new_year,new_month))
281 d1 = eom_clamp(y1, m1, self.day)
283 # Step 3: Add D days via iterative carry across month/year boundaries
284 y2, m2, d2 = add_days_componentwise(y1, m1, d1, period_days)
286 # Direct assignment
287 result.year, result.month, result.day = y2, m2, d2
289 # Add bounds to intermediate result
290 result._solver = self._solver
291 result._add_bounds()
292 return result
293 else:
294 raise TypeError(f"Cannot add {type(other)} to DateVar")
296 def __sub__(self, other) -> "DateVar":
297 """DateVar - Period implemented as DateVar + (-Period)."""
298 if isinstance(other, Period): 298 ↛ 302line 298 didn't jump to line 302 because the condition on line 298 was always true
299 neg = Period(-other.years, -other.months, -other.days)
300 return self.__add__(neg)
301 else:
302 raise TypeError(f"Cannot subtract {type(other)} from DateVar")
305class NaiveSolver:
306 """Naive date constraint solver using component-based representation."""
308 def __init__(self, timeout_ms=600000, use_maxsat=False):
309 """Initialize the solver with optional year bounds and timeout.
311 Args:
312 timeout_ms: Timeout in milliseconds (default: 60 seconds)
313 use_maxsat: If True, use MaxSAT optimization with soft constraints
314 """
315 self.use_maxsat = use_maxsat
316 if use_maxsat: 316 ↛ 317line 316 didn't jump to line 317 because the condition on line 316 was never true
317 self.solver = Optimize()
318 else:
319 self.solver = Solver()
320 self.solver.set("timeout", timeout_ms)
321 self.date_vars = {}
322 self.constraints = []
323 self.timeout_ms = timeout_ms
325 def add_date_var(self, name: str) -> DateVar:
326 """Add a symbolic date variable with comprehensive date validation."""
327 date_var = DateVar(name)
328 date_var._solver = self.solver
329 self.date_vars[name] = date_var
331 # Add bounds using _add_bounds method
332 date_var._add_bounds()
333 return date_var
335 def add_constraint(self, constraint: BoolRef) -> None:
336 """Add a constraint to the solver."""
337 self.constraints.append(constraint)
338 self.solver.add(constraint)
340 def check(self) -> CheckSatResult:
341 """Check if constraints are satisfiable."""
342 return self.solver.check()
344 def model(self) -> ModelRef:
345 """Get the model if satisfiable."""
346 return self.solver.model()
348 def get_concrete_dates(self, model: ModelRef) -> dict:
349 """Get concrete dates from the model."""
350 return {
351 name: var.to_concrete_date(model) for name, var in self.date_vars.items()
352 }
354 def solve(self) -> Union[bool, dict]:
355 """Solve the constraints."""
356 # Add MaxSAT soft constraints if enabled
357 if self.use_maxsat: 357 ↛ 358line 357 didn't jump to line 358 because the condition on line 357 was never true
358 from datetime import date
360 today = date.today()
361 today_year = today.year
363 # Add soft constraints for each date variable
364 for name, date_var in self.date_vars.items():
365 # High weight: today ± 50 years
366 within_50_years = And(
367 date_var.year >= IntVal(today_year - 50),
368 date_var.year <= IntVal(today_year + 50),
369 )
370 self.solver.add_soft(within_50_years, weight=100)
372 # Low weight: today ± 10 years
373 within_10_years = And(
374 date_var.year >= IntVal(today_year - 10),
375 date_var.year <= IntVal(today_year + 10),
376 )
377 self.solver.add_soft(within_10_years, weight=10)
379 result = self.check()
380 if result == sat:
381 model = self.model()
382 return {
383 "status": "sat",
384 "dates": self.get_concrete_dates(model),
385 }
386 elif result == unsat: 386 ↛ 390line 386 didn't jump to line 390 because the condition on line 386 was always true
387 return {"status": "unsat", "dates": {}}
388 else:
389 # result == unknown (timeout or resource limit)
390 return {"status": "timeout", "dates": {}}
392 def to_smt2(self) -> str:
393 """Return the current problem in SMT-LIB v2 format."""
394 return self.solver.to_smt2()
396 def get_assertions(self) -> List[BoolRef]:
397 """Return the list of current Z3 assertions (BoolRef)."""
398 return list(self.solver.assertions())