Rewrite z3 executor using ex_cmd since porcelain is causing problems on Windows

Author: EpicOrange

lib/ex_smt/solver.ex

@@ -1,224 +1,70 @@
 defmodule ExSMT.Solver do
-  require Logger
+  use GenServer
 
   def start_link(init_data) do
     # IO.puts("Starting z3 solver for #{inspect(Keyword.get(init_data, :room_code))} #{inspect(Keyword.get(init_data, :ruleset))}")
-    state = %{
-      room_code: Keyword.get(init_data, :room_code),
-      ruleset: Keyword.get(init_data, :ruleset)
-    }
-    GenServer.start_link(__MODULE__, state, name: Keyword.get(init_data, :name))
+    GenServer.start_link(__MODULE__, [], name: Keyword.get(init_data, :name))
   end
 
-  # def stop do
-  #   case GenServer.whereis(__MODULE__) do
-  #     pid when is_pid(pid) ->
-  #       GenServer.call(pid, :graceful_stop, :infinity)
-  #       :ok = Supervisor.terminate_child(ExSMT.Supervisor, __MODULE__)
-  #       true
-  #     nil ->
-  #       false
-  #   end
-  # end
-
-  # def restart do
-  #   case GenServer.whereis(__MODULE__) do
-  #     nil ->
-  #       Supervisor.restart_child(ExSMT.Supervisor, __MODULE__)
-  #     pid when is_pid(pid) ->
-  #       GenServer.call(pid, :graceful_stop, :infinity)
-  #   end
-  # end
-
-  # def alive? do
-  #   case GenServer.whereis(__MODULE__) do
-  #     nil -> false
-  #     pid when is_pid(pid) -> GenServer.call(__MODULE__, :alive?, 5000)
-  #   end
-  # end
-
-  # def query(iodata, reset \\ true) do
-  #   case GenServer.whereis(__MODULE__) do
-  #     nil -> {:error, :not_running}
-  #     pid when is_pid(pid) ->
-  #       {:ok, response_lns} = GenServer.call(__MODULE__, {:query, iodata, reset}, 5000)
-  #       ExSMT.Solver.ResponseParser.parse(response_lns)
-  #   end
-  # end
-
-  # def query_continue(iodata) do
-  #   query(iodata, false)
-  # end
-
-  use GenServer
-
-  defstruct [
-    mode: :not_running,
-    process: nil,
-    launch_cfg: %{},
-    queries: :queue.new(),
-    reply: nil
-  ]
-
   def init(_state) do
-    opts = Map.new(Application.get_env(:ex_smt, :z3, []))
-
-    z3_path = case Map.fetch(opts, :path) do
-      {:ok, path} ->
-        path = Path.expand(path)
-        cond do
-          File.dir?(path) ->
-            {:prefix, path}
-          File.regular?(path) ->
-            {:binary, path}
-        end
-      :error ->
-        case :os.find_executable(~c"z3") do
-          chars when is_list(chars) ->
-            {:binary, IO.iodata_to_binary(chars)}
-          false ->
-            {:prefix, Path.join([:code.priv_dir(:ex_smt), "z3"])}
-        end
-    end
-
-    z3_bin_path = case z3_path do
-      {:prefix, prefix} ->
-        Path.join([prefix, "bin", "z3"])
-      {:binary, bin_path} ->
-        case File.read_link(bin_path) do
-          {:ok, real_path} -> Path.expand(real_path, Path.dirname(bin_path))
-          {:error, :einval} -> Path.expand(bin_path)
-        end
-    end
-    
-    # make sure that this genserver calls terminate() when killed
-    Process.flag(:trap_exit, true)
-
-    if File.regular?(z3_bin_path) do
-      launch_cfg = %{
-        binary: z3_bin_path,
-      }
-
-      {:ok, %__MODULE__{launch_cfg: launch_cfg}, {:continue, :first_start}}
-    else
-      :ignore
-    end
-  end
-
-  def handle_continue(:first_start, %{mode: :not_running} = state0) do
-    state1 = do_start_node(state0)
-    {:noreply, state1}
-  end
-
-  def handle_continue(:restart_after_error, %{mode: :not_running} = state0) do
-    state1 = do_start_node(state0)
-    {:noreply, state1}
-  end
-
-  def handle_call(:alive?, _from, %{mode: :not_running} = state) do
-    {:reply, false, state}
-  end
-  def handle_call(:alive?, _from, %{mode: :running} = state) do
-    {:reply, true, state}
-  end
+    {:ok, z3} = ExCmd.Process.start_link(~w(z3 -smt2 -in))
 
-  def handle_call({:query, _, _}, _from, %{mode: :not_runinng} = state) do
-    {:reply, {:error, :not_running}, state}
-  end
-  def handle_call({:query, iodata, reset}, from, %{mode: :running, process: proc, queries: q} = state) do
-    script = [
-      if reset do "(reset)\n" else "" end,
-      iodata, "\n",
-      "(echo \"__EOT__\")\n"
-    ]
-    # Logger.debug(["writing:\n", script])
-    Porcelain.Process.send_input(proc, script)
-    {:noreply, %{state | queries: :queue.in(from, q)}}
-  end
+    # ex_cmd doesn't want you to trap exit, so don't do that
+    # unless you are debugging
+    # Process.flag(:trap_exit, true)
 
-  def handle_call(:graceful_stop, _from, state) do
-    {:stop, :normal, :ok, state}
+    {:ok, %{process: z3}}
   end
 
-  def handle_info({_from, :data, :out, iodata}, %{reply: nil, queries: q} = state) do
-    case :queue.out(q) do
-      {:empty, _} ->
-        log_ln = IO.iodata_to_binary(iodata)
-        Logger.info(IO.ANSI.format([:blue, "z3: ", :reset, inspect(log_ln)]))
-        {:noreply, state}
-      {{:value, waiter}, new_q} ->
-        reply = handle_reply_chunk(iodata, {waiter, []})
-        {:noreply, %{state | queries: new_q, reply: reply}}
-    end
-  end
-  def handle_info({_from, :data, :out, iodata}, %{reply: reply0} = state) do
-    reply1 = handle_reply_chunk(iodata, reply0)
-    {:noreply, %{state | reply: reply1}}
+  # this is the main thing you call
+  def handle_call({:query, query, reset?}, _from, %{process: z3} = state) do
+    msg = mk_msg(query, reset?, true)
+    # |> IO.inspect(label: "call")
+    ExCmd.Process.write(z3, msg)
+    {:ok, out} = poll_z3(z3, "")
+    ret = out
+    |> String.split("\n", trim: true)
+    {:reply, {:ok, ret}, state}
   end
 
-  def handle_info({_from, :data, :err, iodata}, state) do
-    log_ln = IO.iodata_to_binary(iodata) |> String.trim()
-    Logger.error(IO.ANSI.format([:red, "z3: ", :reset, log_ln]))
+  # this is for when you need no reply
+  def handle_cast({:query, query, reset?}, %{process: z3} = state) do
+    msg = mk_msg(query, reset?, false)
+    # |> IO.inspect(label: "cast")
+    ExCmd.Process.write(z3, msg)
     {:noreply, state}
   end
 
-  def handle_info({_from, :result, %Porcelain.Result{status: 0}}, %{mode: :running} = state), do:
-    {:noreply, %{state | mode: :not_running, process: nil}}
-  def handle_info({_from, :result, %Porcelain.Result{status: status}}, %{mode: :running} = state) do
-    Logger.error("z3 terminated with exit-code #{status}")
-    {:noreply, %{state | mode: :not_running, process: nil}, {:continue, :restart_after_error}}
-  end
-
-  def handle_info({_from, :result, _result}, %{mode: :not_running} = state) do
+  # this is called exclusively when z3 crashes, but requires trapping exits
+  def handle_info({:EXIT, _pid, reason}, state) do
+    IO.inspect(reason, label: "Z3 crashed with reason")
     {:noreply, state}
   end
 
-  def handle_info(msg, state) do
-    Logger.info("z3: got other msg: #{inspect msg}")
-    {:noreply, state}
-  end
-
-  def terminate(_reason, %{mode: :not_running}), do:
-    :ok
-  def terminate(_reason, %{mode: :running, process: proc}) do
-    Porcelain.Process.stop(proc)
-  end
-
-  defp do_start_node(%{mode: :not_running, launch_cfg: launch_cfg} = state0) do
-    proc = Porcelain.spawn(
-      launch_cfg.binary,
-      ["-smt2", "-in"],
-      in: :receive,
-      out: {:send, self()},
-      err: {:send, self()},
-      result: :keep
-    )
+  @eot "__EOT__"
+  def mk_msg(query, reset?, eot?), do: [
+      if reset? do "(reset)\n" else "" end,
+      query,
+      "\n",
+      if eot? do "(echo \"#{@eot}\")\n" else "" end
+    ]
 
-    %{state0 | mode: :running, process: proc}
+  def poll_z3(z3, acc) do
+    case ExCmd.Process.read(z3) do
+      {:ok, output} ->
+        acc = String.trim_trailing(acc <> "\n" <> output) # support \r\n and \n
+        if String.ends_with?(acc, @eot) do
+          {:ok, String.slice(acc, 0, byte_size(acc) - byte_size(@eot))}
+        else
+          poll_z3(z3, acc)
+        end
+      err -> {:error, err}
+    end
   end
 
-  defp handle_reply_chunk(iodata, {waiter, prev_lns}) do
-    {:ok, reply_lns} =
-      IO.iodata_to_binary(iodata)
-      |> StringIO.open(fn io ->
-        IO.stream(io, :line)
-        |> Stream.filter(&not(match?("\n", &1)))
-        |> Enum.to_list()
-      end)
-
-    handle_reply_lines(reply_lns, prev_lns, waiter)
+  def terminate(_reason, %{process: z3}) do
+    ExCmd.Process.close_stdin(z3)
+    ExCmd.Process.await_exit(z3)
   end
 
-  defp handle_reply_lines([], acc, waiter) do
-    {waiter, acc}
-  end
-  defp handle_reply_lines(["__EOT__\n"], acc, waiter) do
-    response_lns = Enum.reverse(acc)
-    # Logger.debug(["read back:\n", response_lns])
-    GenServer.reply(waiter, {:ok, response_lns})
-    nil
-  end
-  defp handle_reply_lines([ln | lns], acc, waiter) do
-    handle_reply_lines(lns, [ln | acc], waiter)
-  end
 end

lib/ex_smt/solver/response_parser.ex

@@ -95,7 +95,7 @@ defmodule ExSMT.Solver.ResponseParser do
     sexpr,
   ])
 
-  newline = ignore(ascii_char([?\n]))
+  newline = optional(ignore(ascii_char([?\n])))
 
   defparsec :response, repeat(
     optional(flexible_space)

lib/riichi_advanced/game/smt.ex

@@ -779,7 +779,7 @@ defmodule RiichiAdvanced.SMT do
       IO.puts(smt)
       # IO.inspect(encoding)
     end
-    {:ok, _response} = GenServer.call(solver_pid, {:query, smt, true}, 60000)
+    GenServer.cast(solver_pid, {:query, smt, true})
 
     # stream responses
     obtain_all_solutions(solver_pid, encoding, encoding_r, joker_ixs, hand ++ call_tiles, tile_behavior, System.system_time(:millisecond))

mix.exs

@@ -58,7 +58,7 @@ defmodule RiichiAdvanced.MixProject do
       {:hackney, "~> 1.9"},
       {:decimal, "~> 2.0"},
       {:nimble_parsec, "~> 1.4.0"},
-      {:porcelain, github: "walkr/porcelain"},
+      {:porcelain, github: "walkr/porcelain"}, # now unused
       {:temp, "~> 0.4"},
       {:diff_match_patch, github: "pzingg/diff_match_patch"},
       {:diffy, "~> 1.1"},
@@ -69,6 +69,7 @@ defmodule RiichiAdvanced.MixProject do
       {:plug_attack, "~> 0.4.2"},
       {:sobelow, "~> 0.13", only: [:dev, :test], runtime: false},
       {:mix_audit, "~> 2.1", only: [:dev, :test], runtime: false},
+      {:ex_cmd, "~> 0.18.0"},
     ]
   end
 

mix.lock

@@ -11,6 +11,7 @@
   "dns_cluster": {:hex, :dns_cluster, "0.1.3", "0bc20a2c88ed6cc494f2964075c359f8c2d00e1bf25518a6a6c7fd277c9b0c66", [:mix], [], "hexpm", "46cb7c4a1b3e52c7ad4cbe33ca5079fbde4840dedeafca2baf77996c2da1bc33"},
   "ecto": {:hex, :ecto, "3.12.5", "4a312960ce612e17337e7cefcf9be45b95a3be6b36b6f94dfb3d8c361d631866", [:mix], [{:decimal, "~> 2.0", [hex: :decimal, repo: "hexpm", optional: false]}, {:jason, "~> 1.0", [hex: :jason, repo: "hexpm", optional: true]}, {:telemetry, "~> 0.4 or ~> 1.0", [hex: :telemetry, repo: "hexpm", optional: false]}], "hexpm", "6eb18e80bef8bb57e17f5a7f068a1719fbda384d40fc37acb8eb8aeca493b6ea"},
   "esbuild": {:hex, :esbuild, "0.9.0", "f043eeaca4932ca8e16e5429aebd90f7766f31ac160a25cbd9befe84f2bc068f", [:mix], [{:jason, "~> 1.4", [hex: :jason, repo: "hexpm", optional: false]}], "hexpm", "b415027f71d5ab57ef2be844b2a10d0c1b5a492d431727f43937adce22ba45ae"},
+  "ex_cmd": {:hex, :ex_cmd, "0.18.0", "791b42b864c099b67254ca909243e2f60a6e091c802f608d4ae2e3da27b0ade9", [:mix], [], "hexpm", "fd4ec30607a7c789cd53b5fb09189bd0a4922eae5b4fadf70176c19bcd19fb76"},
   "expo": {:hex, :expo, "1.1.0", "f7b9ed7fb5745ebe1eeedf3d6f29226c5dd52897ac67c0f8af62a07e661e5c75", [:mix], [], "hexpm", "fbadf93f4700fb44c331362177bdca9eeb8097e8b0ef525c9cc501cb9917c960"},
   "file_system": {:hex, :file_system, "1.1.0", "08d232062284546c6c34426997dd7ef6ec9f8bbd090eb91780283c9016840e8f", [:mix], [], "hexpm", "bfcf81244f416871f2a2e15c1b515287faa5db9c6bcf290222206d120b3d43f6"},
   "finch": {:hex, :finch, "0.19.0", "c644641491ea854fc5c1bbaef36bfc764e3f08e7185e1f084e35e0672241b76d", [:mix], [{:mime, "~> 1.0 or ~> 2.0", [hex: :mime, repo: "hexpm", optional: false]}, {:mint, "~> 1.6.2 or ~> 1.7", [hex: :mint, repo: "hexpm", optional: false]}, {:nimble_options, "~> 0.4 or ~> 1.0", [hex: :nimble_options, repo: "hexpm", optional: false]}, {:nimble_pool, "~> 1.1", [hex: :nimble_pool, repo: "hexpm", optional: false]}, {:telemetry, "~> 0.4 or ~> 1.0", [hex: :telemetry, repo: "hexpm", optional: false]}], "hexpm", "fc5324ce209125d1e2fa0fcd2634601c52a787aff1cd33ee833664a5af4ea2b6"},