Coverage for datesat / api.py: 74.0%
121 statements
« prev ^ index » next coverage.py v7.13.4, created at 2026-02-10 23:47 +0000
1"""
2Unified API for DateSAT.
4This module provides a unified interface for both bitvector and integer
5approaches to DateSAT constraint solving.
6"""
8from typing import Any, Dict, List, Union
10from z3 import BoolRef
12from .core import Date, Period
15class DateSATBuilder:
16 """Unified API for DateSAT constraint solving."""
18 def __init__(
19 self,
20 approach: str = "epoch_days",
21 implementation: str = "int",
22 timeout_ms: int = 600000,
23 use_maxsat: bool = False,
24 ):
25 """Initialize the builder with the specified approach, implementation, and timeout.
27 Args:
28 approach: Either "naive", "epoch_days", "hybrid", "alpha_beta", or "alpha_beta_table"
29 implementation: Either "int" or "bitvector" (default: "int")
30 timeout_ms: Timeout in milliseconds (default: 600000 = 10 minutes)
31 use_maxsat: If True, use MaxSAT optimization with soft constraints for dates near today
32 """
33 self.approach = approach
34 self.implementation = implementation
35 self.timeout_ms = timeout_ms
36 self.use_maxsat = use_maxsat
38 # Import the appropriate solver based on implementation
39 if implementation == "bitvector":
40 from .symbolic_bitvector.alpha_beta_bv import AlphaBetaSolver
41 from .symbolic_bitvector.alpha_beta_table_bv import AlphaBetaTableSolver
42 from .symbolic_bitvector.naive_bv import NaiveSolver
43 from .symbolic_bitvector.epoch_days_bv import EpochDaysSolver
44 from .symbolic_bitvector.hybrid_bv import HybridSolver
45 elif implementation == "int": 45 ↛ 52line 45 didn't jump to line 52 because the condition on line 45 was always true
46 from .symbolic_int.alpha_beta_int import AlphaBetaSolver
47 from .symbolic_int.alpha_beta_table_int import AlphaBetaTableSolver
48 from .symbolic_int.naive_int import NaiveSolver
49 from .symbolic_int.epoch_days_int import EpochDaysSolver
50 from .symbolic_int.hybrid_int import HybridSolver
51 else:
52 raise ValueError(
53 f"Unknown implementation: {implementation}. Must be 'int' or 'bitvector'"
54 )
56 # Initialize the appropriate solver
57 if approach == "naive":
58 self.solver = NaiveSolver(timeout_ms=timeout_ms, use_maxsat=use_maxsat)
59 elif approach == "epoch_days":
60 self.solver = EpochDaysSolver(timeout_ms=timeout_ms, use_maxsat=use_maxsat)
61 elif approach == "hybrid":
62 self.solver = HybridSolver(timeout_ms=timeout_ms, use_maxsat=use_maxsat)
63 elif approach == "alpha_beta":
64 self.solver = AlphaBetaSolver(timeout_ms=timeout_ms, use_maxsat=use_maxsat)
65 elif approach == "alpha_beta_table": 65 ↛ 68line 65 didn't jump to line 68 because the condition on line 65 was always true
66 self.solver = AlphaBetaTableSolver(timeout_ms=timeout_ms, use_maxsat=use_maxsat)
67 else:
68 raise ValueError(
69 f"Unknown approach: {approach}. Must be 'naive', 'epoch_days', 'hybrid', 'alpha_beta', or 'alpha_beta_table'"
70 )
72 self.constraints = []
73 self._print_smt_on_solve = False
75 # Track Int and Bool variables for complete solution extraction
76 self.int_vars = {} # name -> z3 var
77 self.bool_vars = {} # name -> z3 var
79 def add_date_var(self, name: str) -> "DateVar":
80 """Solver handles date variables internally."""
81 return self.solver.add_date_var(name)
83 def add_int_var(self, name: str, min_value: int = None, max_value: int = None) -> Any:
84 """Add a symbolic int variable compatible with the current implementation.
86 In bitvector mode, creates a BitVec with automatic bounds to prevent overflow.
87 In int mode, creates an Int (unbounded by default).
89 Args:
90 name: Variable name
91 min_value: Optional minimum value (default: 0 in bitvector mode, unbounded in int mode)
92 max_value: Optional maximum value (default: 8000 in bitvector mode, unbounded in int mode)
93 """
94 if self.implementation == "bitvector": 94 ↛ 111line 94 didn't jump to line 111 because the condition on line 94 was always true
95 from z3 import BitVec, BitVecVal
96 from .symbolic_bitvector.bitwidths import INT_VAR_BITS
97 var = BitVec(name, INT_VAR_BITS)
99 # Add automatic bounds to prevent bitvector overflow artifacts
100 # These bounds prevent Z3 from finding spurious solutions due to modular wraparound
101 # Keep values within 21-bit signed range (±1,048,575) to avoid overflow in arithmetic
102 if min_value is None: 102 ↛ 104line 102 didn't jump to line 104 because the condition on line 102 was always true
103 min_value = 0 # Most integer variables represent non-negative quantities (counts, periods, etc.)
104 if max_value is None: 104 ↛ 108line 104 didn't jump to line 108 because the condition on line 104 was always true
105 max_value = 8000 # Conservative bound to prevent arithmetic overflow in expressions like x*125
107 # Add bound constraints
108 self.solver.add_constraint(var >= BitVecVal(min_value, INT_VAR_BITS))
109 self.solver.add_constraint(var <= BitVecVal(max_value, INT_VAR_BITS))
110 else:
111 from z3 import Int
112 var = Int(name)
114 # Add optional bounds in int mode if specified
115 if min_value is not None:
116 self.solver.add_constraint(var >= min_value)
117 if max_value is not None:
118 self.solver.add_constraint(var <= max_value)
120 # Track this variable for solution extraction
121 self.int_vars[name] = var
122 return var
124 def add_bool_var(self, name: str) -> Any:
125 """Add a symbolic bool variable."""
126 from z3 import Bool
127 var = Bool(name)
129 # Track this variable for solution extraction
130 self.bool_vars[name] = var
131 return var
133 def add_constraint(self, constraint: Any) -> None:
134 """Add a constraint to the solver.
136 Accepts both Z3 BoolRef (for symbolic solvers) and ConstraintWrapper
137 (for enumeration baseline).
138 """
139 # Guard against None constraints
140 if constraint is None: 140 ↛ 141line 140 didn't jump to line 141 because the condition on line 140 was never true
141 raise TypeError(
142 "Constraint is None. Ensure expressions return a valid constraint."
143 )
144 self.constraints.append(constraint)
145 self.solver.add_constraint(constraint)
147 def solve(self) -> Dict[str, Any]:
148 """Solve the constraints and return results."""
149 if self._print_smt_on_solve: 149 ↛ 150line 149 didn't jump to line 150 because the condition on line 149 was never true
150 print("\n; SMT-LIB dump (generated by DateSAT)")
151 print(self.to_smt2())
152 result = self.solver.solve()
153 if result["status"] == "sat":
154 # Extract Int and Bool variables from the Z3 model
155 model = self.solver.model()
156 int_values = {}
157 bool_values = {}
159 # Explicitly evaluate all tracked Int variables with model_completion=True
160 # to ensure we get values for unconstrained variables
161 for name, var in self.int_vars.items():
162 try:
163 value = model.evaluate(var, model_completion=True)
164 if value is not None: 164 ↛ 161line 164 didn't jump to line 161 because the condition on line 164 was always true
165 # Check if it's a BitVec or Int
166 from z3 import is_bv
167 if is_bv(value): 167 ↛ 170line 167 didn't jump to line 170 because the condition on line 167 was always true
168 int_values[name] = value.as_signed_long()
169 else:
170 int_values[name] = value.as_long()
171 except Exception:
172 # Skip if we can't extract the value
173 pass
175 # Explicitly evaluate all tracked Bool variables with model_completion=True
176 for name, var in self.bool_vars.items():
177 try:
178 value = model.evaluate(var, model_completion=True)
179 if value is not None: 179 ↛ 176line 179 didn't jump to line 176 because the condition on line 179 was always true
180 bool_values[name] = bool(value)
181 except Exception:
182 # Skip if we can't extract the value
183 pass
185 # Add Int and Bool values to result
186 if int_values:
187 result["ints"] = int_values
188 if bool_values:
189 result["bools"] = bool_values
191 print(f"✅ SATISFIABLE:")
192 for name, date in result["dates"].items():
193 print(f" {name} = {date}")
194 for name, value in result.get("ints", {}).items():
195 print(f" {name} = {value}")
196 for name, value in result.get("bools", {}).items():
197 print(f" {name} = {value}")
198 else:
199 print("❌ UNSATISFIABLE")
200 return result
202 def get_constraints(self) -> List[BoolRef]:
203 """Get all constraints."""
204 return self.constraints
206 def to_smt2(self) -> str:
207 """Return the current problem in SMT-LIB v2 format."""
208 # In MaxSAT mode many solvers use Z3 Optimize, which may not expose `to_smt2()`
209 # depending on Z3 build/bindings. Fall back to `sexpr()` so callers (e.g. benchmarks)
210 # can still persist a textual solver dump.
211 inner = getattr(self.solver, "solver", None)
212 if inner is not None:
213 to_smt2 = getattr(inner, "to_smt2", None)
214 if callable(to_smt2):
215 return to_smt2()
216 sexpr = getattr(inner, "sexpr", None)
217 if callable(sexpr):
218 return sexpr()
219 # Fallback to the solver wrapper API (legacy)
220 return self.solver.to_smt2()
222 def enable_smtlib_print(self, enabled: bool = True) -> None:
223 """Enable or disable printing SMT-LIB when solving."""
224 self._print_smt_on_solve = enabled