Coverage for datesat/symbolic_int/epoch_days

1"""

2Epoch_days DateSAT implementation using epoch-based conversion.

4This module implements the epoch_days approach where dates are represented

5as days since an epoch, and period arithmetic is done using approximate

6day conversions.

7"""

9from datetime import date, timedelta

10from typing import List, Tuple, Union

12from z3 import (

13 And,

14 ArithRef,

15 BoolRef,

16 CheckSatResult,

17 If,

18 Int,

19 IntVal,

20 ModelRef,

21 Not,

22 Optimize,

23 Solver,

24 sat,

25 unsat,

26)

27from ..core import Date, Period

28from .naive_int import (

29 eom_clamp,

30 normalize_month

31)

33_EPOCH = date(2000, 3, 1)

35def _ymd_from_days_since_epoch_z3(days_term: ArithRef) -> Tuple[ArithRef, ArithRef, ArithRef]:

36 """

37 Decode (y,m,d) from a Z3 Int 'days since 2000-03-01', directly.

39 Uses March-based civil-from-days arithmetic anchored at 2000-03-01, which is:

40 - the start of a March-based year, and

41 - in year 2000, which is divisible by 400 (cycle boundary).

42 So we can do pure 400/100/4/1 block decomposition + a constant-time month/day formula.

43 """

44 # Constants

45 D400, D100, D4, D1 = IntVal(146097), IntVal(36524), IntVal(1461), IntVal(365)

47 # Split into 400-year cycles (Z3 div/mod with positive divisor gives 0 <= r < D400 even for negative days_term)

48 q400, r400 = days_term / D400, days_term % D400

50 # 100-year blocks within the 400-year cycle (clamp the last block)

51 q100_raw = r400 / D100

52 q100 = If(q100_raw >= IntVal(4), IntVal(3), q100_raw) # 0..3

53 r100 = r400 - q100 * D100

55 # 4-year blocks

56 q4, r4 = r100 / D4, r100 % D4

58 # 1-year blocks (clamp the last block)

59 q1_raw = r4 / D1

60 q1 = If(q1_raw >= IntVal(4), IntVal(3), q1_raw) # 0..3

61 r1 = r4 - q1 * D1 # day-of-year in March-based year, 0..365

63 # March-based year (starts at Mar 1). Day 0 == 2000-03-01.

64 y = IntVal(2000) + q400 * IntVal(400) + q100 * IntVal(100) + q4 * IntVal(4) + q1

66 # Convert March-based day-of-year to month/day using 153-day month blocks

67 # mp: 0..11 corresponds to Mar..Feb

68 mp = (IntVal(5) * r1 + IntVal(2)) / IntVal(153)

69 d = r1 - (IntVal(153) * mp + IntVal(2)) / IntVal(5) + IntVal(1)

71 m = mp + IntVal(3) # Mar=3,...,Dec=12,Jan=13,Feb=14

72 m = If(m > IntVal(12), m - IntVal(12), m) # wrap Jan/Feb back to 1/2

74 # If month is Jan/Feb, it belongs to the next Gregorian year

75 y = y + If(m <= IntVal(2), IntVal(1), IntVal(0))

77 return y, m, d

79_EPOCH_MARCH_BASED_ABS = IntVal(730485) # days_from_civil(2000,3,1) in March-based absolute days

81def _days_since_epoch_from_ymd_z3(y: ArithRef, m: ArithRef, d: ArithRef) -> ArithRef:

82 D400 = IntVal(146097)

84 # Shift Jan/Feb into previous year to make Mar the first month

85 y_adj = y - If(m <= IntVal(2), IntVal(1), IntVal(0))

86 m_adj = m + If(m <= IntVal(2), IntVal(12), IntVal(0)) # now 3..14

87 mp = m_adj - IntVal(3) # 0..11 (Mar..Feb)

89 # 400-year era decomposition (Z3 div is Euclidean for positive divisor)

90 era = y_adj / IntVal(400)

91 yoe = y_adj - era * IntVal(400) # 0..399 (within era)

93 # Day-of-year within March-based year

94 doy = (IntVal(153) * mp + IntVal(2)) / IntVal(5) + (d - IntVal(1)) # 0..365

96 # Day-of-era: days from start of era to start of year yoe

97 # Formula: yoe * 365 + yoe/4 - yoe/100 + yoe/400

98 # This accounts for leap years: every 4 years, except centuries, except 400-year cycles

99 doe = yoe * IntVal(365) + (yoe / IntVal(4)) - (yoe / IntVal(100)) + (yoe / IntVal(400)) + doy

100

101 # Absolute days since 0000-03-01, then shift so 2000-03-01 is 0

102 abs_days = era * D400 + doe

103 return abs_days - _EPOCH_MARCH_BASED_ABS

104

105

106def ymd_from_days_since_epoch(days_term):

107 """

108 Overload:

109 - ymd_from_days_since_epoch(int) -> Date

110 - ymd_from_days_since_epoch(ArithRef) -> (y,m,d) ArithRefs

111 """

112 if isinstance(days_term, int):

113 return date_from_days_since_epoch(days_term)

114 return _ymd_from_days_since_epoch_z3(days_term)

115

116

117def days_since_epoch_from_ymd(*args):

118 """

119 Overload:

120 - days_since_epoch_from_ymd(Date) -> int

121 - days_since_epoch_from_ymd(y,m,d) -> ArithRef

122 """

123 if len(args) == 1 and isinstance(args[0], Date):

124 return days_since_epoch_from_date(args[0])

125 if len(args) == 3: 125 ↛ 128line 125 didn't jump to line 128 because the condition on line 125 was always true

126 y, m, d = args

127 return _days_since_epoch_from_ymd_z3(y, m, d)

128 raise TypeError("days_since_epoch_from_ymd expects (Date) or (y, m, d)")

129

130def date_from_days_since_epoch(days: int) -> Date:

131 """Convert concrete days since epoch to a concrete Date."""

132 result_date = _EPOCH + timedelta(days=days)

133 return Date(result_date.year, result_date.month, result_date.day)

134

135

136def days_since_epoch_from_date(date_obj: Date) -> int:

137 """Convert a concrete Date to concrete days since epoch (March 1, 2000)."""

138 target_python = date(date_obj.year, date_obj.month, date_obj.day)

139 return (target_python - _EPOCH).days

140

141def add_days_ordinal(y, m, d, delta_days) -> ArithRef:

142 """

143 Exact ordinal-based addition via a single ordinal add.

144 """

145 z = days_since_epoch_from_ymd(y, m, d)

146 return z + delta_days

147

148class DateVar:

149 """Symbolic date variable for epoch_days implementation."""

150

151 def __init__(self, name: str):

152 """Create a symbolic date variable."""

153 self.name = name

154 # Use a single Z3 integer variable for days since epoch

155 self.days_var = Int(f"{name}_days")

156 # Solver reference for adding bounds to intermediate dates (set after creation if needed)

157 self._solver = None

158

159 def __str__(self) -> str:

160 return f"DateVar({self.name})"

161

162 @property

163 def year(self) -> ArithRef:

164 """Get symbolic year component (decodes from days_var)."""

165 y, _, _ = ymd_from_days_since_epoch(self.days_var)

166 return y

167

168 @property

169 def month(self) -> ArithRef:

170 """Get symbolic month component (decodes from days_var)."""

171 _, m, _ = ymd_from_days_since_epoch(self.days_var)

172 return m

173

174 @property

175 def day(self) -> ArithRef:

176 """Get symbolic day component (decodes from days_var)."""

177 _, _, d = ymd_from_days_since_epoch(self.days_var)

178 return d

179

180 def to_concrete_date(self, model: ModelRef) -> Date:

181 """Convert Z3 model to concrete Date."""

182 days = model.evaluate(self.days_var, model_completion=True).as_long()

183 return date_from_days_since_epoch(days)

184

185 def __ge__(self, other) -> BoolRef:

186 """Support x >= date comparison."""

187 if isinstance(other, Date):

188 return self.days_var >= days_since_epoch_from_date(other)

189 elif isinstance(other, DateVar): 189 ↛ 192line 189 didn't jump to line 192 because the condition on line 189 was always true

190 return self.days_var >= other.days_var

191 else:

192 raise TypeError(f"Cannot compare DateVar with {type(other)}")

193

194 def __le__(self, other) -> BoolRef:

195 """Support x <= date comparison."""

196 if isinstance(other, Date):

197 return self.days_var <= days_since_epoch_from_date(other)

198 elif isinstance(other, DateVar): 198 ↛ 201line 198 didn't jump to line 201 because the condition on line 198 was always true

199 return self.days_var <= other.days_var

200 else:

201 raise TypeError(f"Cannot compare DateVar with {type(other)}")

202

203 def __lt__(self, other) -> BoolRef:

204 """Support x < date comparison."""

205 if isinstance(other, (Date, DateVar)): 205 ↛ 208line 205 didn't jump to line 208 because the condition on line 205 was always true

206 return Not(self.__ge__(other))

207 else:

208 raise TypeError(f"Cannot compare DateVar with {type(other)}")

209

210 def __gt__(self, other) -> BoolRef:

211 """Support x > date comparison."""

212 if isinstance(other, (Date, DateVar)): 212 ↛ 215line 212 didn't jump to line 215 because the condition on line 212 was always true

213 return Not(self.__le__(other))

214 else:

215 raise TypeError(f"Cannot compare DateVar with {type(other)}")

216

217 def __eq__(self, other) -> BoolRef:

218 """Support x == date comparison."""

219 if isinstance(other, Date):

220 return self.days_var == days_since_epoch_from_date(other)

221 elif isinstance(other, DateVar): 221 ↛ 224line 221 didn't jump to line 224 because the condition on line 221 was always true

222 return self.days_var == other.days_var

223 else:

224 raise TypeError(f"Cannot compare DateVar with {type(other)}")

225

226 def __ne__(self, other) -> BoolRef:

227 """Support x != date comparison."""

228 if isinstance(other, (Date, DateVar)): 228 ↛ 231line 228 didn't jump to line 231 because the condition on line 228 was always true

229 return Not(self.__eq__(other))

230 else:

231 raise TypeError(f"Cannot compare DateVar with {type(other)}")

232

233 def _add_bounds(self) -> None:

234 """Add date validation bounds to this DateVar if solver is available."""

235 if self._solver is None: 235 ↛ 236line 235 didn't jump to line 236 because the condition on line 235 was never true

236 return

237

238 # Add constraints for valid date ranges [1900-03-01 to 2100-02-28]

239 # Epoch is March 1, 2000

240 # 1900-03-01 = -36525 days from epoch

241 # 2100-02-28 = 36523 days from epoch

242 self._solver.add(self.days_var >= IntVal(-36525))

243 self._solver.add(self.days_var <= IntVal(36523))

244

245 def __add__(self, other) -> "DateVar":

246 """

247 DateVar + Period following semantics.

248 Steps: normalize Y/M, EOM clamp, then add D days in ordinal space.

249 """

250 if isinstance(other, Period): 250 ↛ 289line 250 didn't jump to line 289 because the condition on line 250 was always true

251 result = DateVar(f"{self.name}_plus")

252

253 # Fast-path: only days component (check at Python level since Period components are concrete)

254 if other.years == 0 and other.months == 0:

255 days_expr = self.days_var + IntVal(other.days)

256 else:

257 oy, om, od = (

258 IntVal(other.years),

259 IntVal(other.months),

260 IntVal(other.days),

261 )

262

263 # Decode current date to Y/M/D

264 y0, m0, d0 = ymd_from_days_since_epoch(self.days_var)

265

266 # Step 1: Combine Y and M with normalization (carry years)

267 period_total_months = oy * IntVal(12) + om

268 total_months = m0 + period_total_months

269 y1, m1 = normalize_month(y0, total_months)

270

271 # Step 2: EOM clamp

272 d1 = eom_clamp(y1, m1, d0)

273

274 if od == 0:

275 # Encode back to days-since-epoch

276 days_expr = days_since_epoch_from_ymd(y1, m1, d1)

277 else:

278 # Step 3: add D days in ordinal space

279 days_expr = add_days_ordinal(y1, m1, d1, od)

280

281 # Direct assignment

282 result.days_var = days_expr

283

284 # Add bounds to intermediate result

285 result._solver = self._solver

286 result._add_bounds()

287 return result

288 else:

289 raise TypeError(f"Cannot add {type(other)} to DateVar")

290

291 def __sub__(self, other) -> "DateVar":

292 """DateVar - Period implemented as DateVar + (-Period)."""

293 if isinstance(other, Period): 293 ↛ 297line 293 didn't jump to line 297 because the condition on line 293 was always true

294 neg = Period(-other.years, -other.months, -other.days)

295 return self.__add__(neg)

296 else:

297 raise TypeError(f"Cannot subtract {type(other)} from DateVar")

298

299

300class EpochDaysSolver:

301 """Epoch_days date constraint solver using epoch-based conversion."""

302

303 def __init__(self, timeout_ms=600000, use_maxsat=False):

304 """Initialize the solver with timeout.

305

306 Args:

307 timeout_ms: Timeout in milliseconds (default: 60 seconds)

308 use_maxsat: If True, use MaxSAT optimization with soft constraints

309 """

310 self.use_maxsat = use_maxsat

311 if use_maxsat: 311 ↛ 312line 311 didn't jump to line 312 because the condition on line 311 was never true

312 self.solver = Optimize()

313 else:

314 self.solver = Solver()

315 self.solver.set("timeout", timeout_ms)

316 self.date_vars = {}

317 self.constraints = []

318 self.timeout_ms = timeout_ms

319

320 def add_date_var(self, name: str) -> DateVar:

321 """Add a symbolic date variable with basic constraints."""

322 date_var = DateVar(name)

323 date_var._solver = self.solver

324 self.date_vars[name] = date_var

325

326 # Add bounds using _add_bounds method

327 date_var._add_bounds()

328 return date_var

329

330 def add_constraint(self, constraint: BoolRef) -> None:

331 """Add a constraint to the solver."""

332 self.constraints.append(constraint)

333 self.solver.add(constraint)

334

335 def check(self) -> CheckSatResult:

336 """Check if constraints are satisfiable."""

337 return self.solver.check()

338

339 def model(self) -> ModelRef:

340 """Get the model if satisfiable."""

341 return self.solver.model()

342

343 def get_concrete_dates(self, model: ModelRef) -> dict:

344 """Get concrete dates from the model."""

345 return {

346 name: var.to_concrete_date(model) for name, var in self.date_vars.items()

347 }

348

349 def solve(self) -> Union[bool, dict]:

350 """Solve the constraints."""

351 # Add MaxSAT soft constraints if enabled

352 if self.use_maxsat: 352 ↛ 353line 352 didn't jump to line 353 because the condition on line 352 was never true

353 from datetime import date

354

355 today = date.today()

356 today_days = days_since_epoch_from_date(Date.from_python_date(today))

357

358 # Calculate ±50 years and ±10 years in days (approximate)

359 # Using 365.25 days per year for accuracy

360 days_50_years = int(50 * 365.25)

361 days_10_years = int(10 * 365.25)

362

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.days_var >= IntVal(today_days - days_50_years),

368 date_var.days_var <= IntVal(today_days + days_50_years),

369 )

370 self.solver.add_soft(within_50_years, weight=100)

371

372 # Low weight: today ± 10 years

373 within_10_years = And(

374 date_var.days_var >= IntVal(today_days - days_10_years),

375 date_var.days_var <= IntVal(today_days + days_10_years),

376 )

377 self.solver.add_soft(within_10_years, weight=10)

378

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": {}}

391

392 def to_smt2(self) -> str:

393 """Return the current problem in SMT-LIB v2 format."""

394 return self.solver.to_smt2()

395

396 def get_assertions(self) -> List[BoolRef]:

397 """Return the list of current Z3 assertions (BoolRef)."""

398 return list(self.solver.assertions())

Coverage for datesat / symbolic_int / epoch_days_int.py: 82.5%

184 statements