diff --git a/jsi-client-rs/src/main.rs b/jsi-client-rs/src/main.rs index fd7de11..fdd75b0 100644 --- a/jsi-client-rs/src/main.rs +++ b/jsi-client-rs/src/main.rs @@ -36,7 +36,7 @@ fn main() { let args: Vec = env::args().collect(); if args.len() < 2 { - eprintln!("Usage: {} ", args[0]); + eprintln!("Usage: {} ", args[0]); process::exit(1); } diff --git a/src/jsi/cli.py b/src/jsi/cli.py index 3ed1370..2b8c43e 100644 --- a/src/jsi/cli.py +++ b/src/jsi/cli.py @@ -284,7 +284,8 @@ def main(args: list[str] | None = None) -> int: # build the commands to run the solvers # run the solvers in the specified sequence, or fallback to the default order - enabled_solvers = [s for s in solver_definitions if solver_definitions[s].enabled] + defs = solver_definitions + enabled_solvers = [solver for solver in defs if defs[solver].enabled] commands: list[Command] = base_commands( config.sequence or enabled_solvers, diff --git a/src/jsi/config/definitions.json b/src/jsi/config/definitions.json index bab6b9d..a45cef5 100644 --- a/src/jsi/config/definitions.json +++ b/src/jsi/config/definitions.json @@ -1,8 +1,9 @@ { "bitwuzla": { "executable": "bitwuzla", - "model": "--produce-models", - "args": [] + "model": null, + "args": ["--produce-models"], + "meta": "we enable models by default, needed to produce unsat cores 🤷‍♂️" }, "boolector": { "executable": "boolector", diff --git a/src/jsi/core.py b/src/jsi/core.py index 6796a95..b2e5a7d 100644 --- a/src/jsi/core.py +++ b/src/jsi/core.py @@ -543,6 +543,7 @@ class ProcessController: task: Task commands: list[Command] config: Config + start_callback: Callable[[Command, Task], None] | None exit_callback: Callable[[Command, Task], None] | None _monitors: list[threading.Thread] _launchers: list[threading.Timer] @@ -552,11 +553,13 @@ def __init__( task: Task, commands: list[Command], config: Config, + start_callback: Callable[[Command, Task], None] | None = None, exit_callback: Callable[[Command, Task], None] | None = None, ): self.task = task self.commands = commands self.config = config + self.start_callback = start_callback self.exit_callback = exit_callback self._monitors = [] self._launchers = [] @@ -618,6 +621,9 @@ def _launch_process(self, command: Command): self._monitors.append(monitor) monitor.start() + if self.start_callback: + self.start_callback(command, task) + def _monitor_process(self, command: Command): """Monitor the given process for completion, wait until configured timeout. diff --git a/src/jsi/server.py b/src/jsi/server.py index cd66120..60ea265 100644 --- a/src/jsi/server.py +++ b/src/jsi/server.py @@ -45,7 +45,7 @@ base_commands, set_input_output, ) -from jsi.utils import get_consoles, pid_exists, unexpand_home +from jsi.utils import get_consoles, logger, pid_exists, unexpand_home SERVER_HOME = Path.home() / ".jsi" / "daemon" SOCKET_PATH = SERVER_HOME / "server.sock" @@ -82,14 +82,15 @@ def __init__(self): self._result: str | None = None def exit_callback(self, command: Command, task: Task): + name, result, elapsed = command.name, command.result(), command.elapsed() + logger.info(f"{name} returned {result} in {elapsed:.03f}s") + if self.event.is_set(): return if command.done() and command.ok() and (stdout_text := command.stdout_text): self.event.set() self._result = f"{stdout_text.strip()}\n; (result from {command.name})" - name, result = command.name, command.result() - print(f"{name} returned {result} in {command.elapsed():.03f}s") @property def result(self) -> str: @@ -106,17 +107,19 @@ def __init__(self, path: Path): # by the time we enter the context manager def __enter__(self): + path_str = unexpand_home(self.path) try: with open(self.path) as fd: - print(f"pid file already exists: {self.path}") + logger.info(f"pid file already exists: {path_str}") other_pid = fd.read() - if pid_exists(int(other_pid)): - print(f"killing existing daemon ({other_pid=})") - os.kill(int(other_pid), signal.SIGKILL) + other_pid_int = int(other_pid) if other_pid.isdigit() else None + if other_pid_int and pid_exists(other_pid_int): + logger.info(f"killing existing daemon (other_pid={other_pid_int})") + os.kill(other_pid_int, signal.SIGKILL) else: - print(f"pid file points to dead daemon ({other_pid=})") + logger.info(f"pid file points to dead daemon ({other_pid=})") except FileNotFoundError: # pid file doesn't exist, we're good to go pass @@ -126,17 +129,21 @@ def __enter__(self): with open(self.path, "w") as fd: fd.write(str(pid)) - print(f"created pid file: {self.path} ({pid=})") + logger.info(f"created pid file: {path_str} ({pid=})") return self.path def __exit__(self, exc_type, exc_value, traceback): # type: ignore - print(f"removing pid file: {self.path}") + logger.info(f"removing pid file: {self.path}") # ignore if the file was already removed with contextlib.suppress(FileNotFoundError): os.remove(self.path) +def start_logger(command: Command, task: Task): + logger.info(f"command started: {command.parts()}") + + class Server: solver_definitions: dict[str, SolverDefinition] available_solvers: dict[str, str] @@ -153,7 +160,7 @@ async def start(self): ) async with server: - print(f"server started on {unexpand_home(SOCKET_PATH)}") + logger.info(f"server listening on {unexpand_home(SOCKET_PATH)}") await server.serve_forever() async def handle_client( @@ -167,7 +174,7 @@ async def handle_client( writer.write(result.encode()) await writer.drain() except Exception as e: - print(f"Error handling client: {e}") + logger.info(f"Error handling client: {e}") finally: writer.close() await writer.wait_closed() @@ -186,8 +193,11 @@ def sync_solve(self, file: str) -> str: self.config.input_file = file self.config.output_dir = os.path.dirname(file) + defs = self.solver_definitions + enabled_solvers = [solver for solver in defs if defs[solver].enabled] + commands = base_commands( - self.config.sequence or list(self.available_solvers.keys()), + self.config.sequence or enabled_solvers, self.solver_definitions, self.available_solvers, self.config, @@ -196,11 +206,16 @@ def sync_solve(self, file: str) -> str: listener = ResultListener() controller = ProcessController( - task, commands, self.config, exit_callback=listener.exit_callback + task, commands, self.config, + start_callback=start_logger, + exit_callback=listener.exit_callback ) controller.start() - return listener.result + result = listener.result + controller.kill() + + return result def daemonize(config: Config):