Coverage for datesat / solver.py: 12.9%
50 statements
« prev ^ index » next coverage.py v7.13.4, created at 2026-02-10 23:47 +0000
1"""
2High-level solver API for DateSAT.
4This module provides a simple interface for solving date constraints.
5"""
7import json
8from typing import Any, Dict, List, Union
9from z3 import BoolVal
10from .api import DateSATBuilder
11from .constraint_parser import ConstraintParser
12from .core import Date, Period
15def solve(
16 constraints: Union[List[str], Dict[str, Any]],
17 declarations: List[str] = None,
18 approach: str = "epoch_days",
19 implementation: str = "int",
20 timeout_ms: int = 600000,
21 verbose: bool = True,
22 use_maxsat: bool = False,
23) -> Dict[str, Any]:
24 """
25 Solve date constraints and return the result.
27 This is the main high-level API for DateSAT. It accepts constraints in either
28 a simple list format or the full JSON format used in DateSATBench.
30 Args:
31 constraints: Either:
32 - A list of constraint strings, e.g., ["x >= Date(2000,1,1)", "x < y"]
33 - A dict with "constraints" and "declarations" fields (JSON format)
34 declarations: Optional list of variable declarations, e.g., ["x: date", "y: date"]
35 Only used if constraints is a list. If constraints is a dict, declarations
36 are taken from the dict.
37 approach: Solver approach - "naive", "epoch_days", "hybrid", "alpha_beta", or "alpha_beta_table"
38 implementation: Implementation type - "int" or "bitvector"
39 timeout_ms: Timeout in milliseconds (default: 600000 = 10 minutes)
40 verbose: If True, print results to stdout (default: True)
42 Returns:
43 Dictionary with:
44 - status: "sat" or "unsat"
45 - dates: Dict mapping date variable names to Date objects (if sat)
46 - ints: Dict mapping int variable names to int values (if sat)
47 - bools: Dict mapping bool variable names to bool values (if sat)
48 - execution_time: Time taken to solve in seconds
49 - approach: The approach used
50 - implementation: The implementation used
52 Examples:
53 >>> # Simple API usage
54 >>> result = datesat.solve(
55 ... constraints=["x >= Date(2000,1,1)", "x < Date(2000,12,31)"],
56 ... declarations=["x: date"]
57 ... )
59 >>> # JSON format usage
60 >>> result = datesat.solve({
61 ... "declarations": ["x: date", "y: date"],
62 ... "constraints": ["x >= Date(2000,1,1)", "y == x + Period(0,1,0)"]
63 ... })
65 >>> # With integer variables
66 >>> result = datesat.solve({
67 ... "declarations": ["x: date", "n: int"],
68 ... "constraints": ["x == Date(2000,1,1) + Period(0,0,n)", "n > 5", "n < 10"]
69 ... })
70 """
71 import time
73 # Parse constraint format
74 if isinstance(constraints, dict):
75 constraint_data = constraints
76 else:
77 constraint_data = {
78 "constraints": constraints,
79 "declarations": declarations or []
80 }
82 # Parse constraints into executable code
83 parser = ConstraintParser()
84 constraint_code = parser.parse_constraint_data(constraint_data)
86 # Create builder and execution context
87 start_time = time.time()
89 # Create a builder factory that will be used in the executed code
90 def create_builder():
91 return DateSATBuilder(
92 approach=approach,
93 implementation=implementation,
94 timeout_ms=timeout_ms,
95 use_maxsat=use_maxsat
96 )
98 # Set up execution context with all necessary imports and the builder factory
99 exec_globals = {
100 "DateSATBuilder": create_builder,
101 "Date": Date,
102 "Period": Period,
103 }
105 # Execute the constraint code, catching ValueError for out-of-bounds dates and converting to UNSAT
106 try:
107 exec(constraint_code, exec_globals)
108 except ValueError as e:
109 # Check if this is a date out of bounds error
110 if "Date outside allowed range" in str(e):
111 # Intermediate date went out of bounds - add a False constraint to make it UNSAT
112 builder = exec_globals.get("builder")
113 if builder:
114 builder.add_constraint(BoolVal(False))
115 else:
116 # If builder doesn't exist yet, we can't add constraint, so re-raise
117 raise RuntimeError(f"Date out of bounds during constraint setup: {e}") from e
118 else:
119 # Re-raise if it's a different ValueError
120 raise
122 # Get the builder from executed code
123 builder = exec_globals.get("builder")
124 if not builder:
125 raise RuntimeError("Failed to create constraint solver")
127 # Temporarily disable builder's verbose output if verbose=False
128 if not verbose:
129 original_solve = builder.solve
130 def quiet_solve():
131 # Capture and suppress output
132 import sys
133 from io import StringIO
134 old_stdout = sys.stdout
135 sys.stdout = StringIO()
136 try:
137 result = original_solve()
138 finally:
139 sys.stdout = old_stdout
140 return result
141 builder.solve = quiet_solve
143 # Solve the constraints
144 solve_result = builder.solve()
146 # Calculate execution time
147 execution_time = time.time() - start_time
149 # Add metadata to result
150 result = {
151 **solve_result,
152 "execution_time": execution_time,
153 "approach": approach,
154 "implementation": implementation,
155 }
157 return result
160def solve_from_json(json_data: Union[str, Dict[str, Any]], **kwargs) -> Dict[str, Any]:
161 """
162 Solve constraints from JSON data.
164 Args:
165 json_data: Either a JSON string or a parsed dictionary
166 **kwargs: Additional arguments to pass to solve()
168 Returns:
169 Dictionary with solution results
171 Examples:
172 >>> # From JSON string
173 >>> result = datesat.solve_from_json('''
174 ... {
175 ... "declarations": ["x: date"],
176 ... "constraints": ["x >= Date(2000,1,1)"]
177 ... }
178 ... ''')
180 >>> # From file
181 >>> with open('constraints.json') as f:
182 ... result = datesat.solve_from_json(f.read())
183 """
184 if isinstance(json_data, str):
185 constraint_data = json.loads(json_data)
186 else:
187 constraint_data = json_data
189 return solve(constraint_data, **kwargs)