server: better logs, explicit kill on good result

jsi-client-rs/src/main.rs

@@ -36,7 +36,7 @@ fn main() {
     let args: Vec<String> = env::args().collect();
 
     if args.len() < 2 {
-        eprintln!("Usage: {} <command>", args[0]);
+        eprintln!("Usage: {} <path/to/file.smt2>", args[0]);
         process::exit(1);
     }
 

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,

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",

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.
 

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):