View Source cure_smt_process (cure v0.1.0)

Cure SMT Solver Process Manager

Manages external SMT solver processes (Z3, CVC5) using Erlang ports. Provides process pooling, timeout enforcement, and resource management.

Features

  • Port-based communication with solvers
  • Process pool for performance
  • Timeout enforcement
  • Automatic crash recovery
  • Resource limits
  • Query execution with model extraction

Usage 

% Start a solver
{ok, Pid} = cure_smt_process:start_solver(z3, 5000).

% Execute a query
Query = \"(set-logic QF_LIA)\\n(check-sat)\\n\",
{sat, Lines} = cure_smt_process:execute_query(Pid, Query).

% Stop solver
cure_smt_process:stop_solver(Pid).

Summary

Functions

code_change(OldVsn, State, Extra)
execute_query(Pid, Query)

Execute an SMT-LIB query on a solver process.

execute_query(Pid, Query, Timeout)
get_pooled_solver(PoolPid, Solver)

Get a solver from the pool.

get_stats(Pid)

Get solver statistics.

handle_call/3
handle_cast/2
handle_info/2
init/1
reset_solver(Pid)

Reset a solver process (clear all assertions).

return_solver(PoolPid, SolverPid)

Return a solver to the pool.

start_pool(Opts)

Start a solver process pool.

start_solver(Solver, Timeout)

Start a solver process.

start_solver(Solver, Timeout, Opts)
stop_pool(Pid)

Stop the solver pool.

stop_solver(Pid)

Stop a solver process.

terminate/2

Functions

code_change(OldVsn, State, Extra)

execute_query(Pid, Query)

-spec execute_query(pid(), iolist()) -> {sat | unsat | unknown, [binary()]} | {error, term()}.

Execute an SMT-LIB query on a solver process.

Arguments

  • Pid - Solver process PID
  • Query - SMT-LIB query string or iolist

Returns

  • {sat, Lines} - Satisfiable with model lines
  • {unsat, []} - Unsatisfiable
  • {unknown, []} - Solver couldn't determine
  • {error, Reason} - Execution error

execute_query(Pid, Query, Timeout)

-spec execute_query(pid(), iolist(), timeout()) -> {sat | unsat | unknown, [binary()]} | {error, term()}.

get_pooled_solver(PoolPid, Solver)

-spec get_pooled_solver(pid(), z3 | cvc5) -> {ok, pid()} | {error, term()}.

Get a solver from the pool.

get_stats(Pid)

-spec get_stats(pid()) -> map().

Get solver statistics.

handle_call/3

handle_cast/2

handle_info/2

init/1

reset_solver(Pid)

-spec reset_solver(pid()) -> ok | {error, term()}.

Reset a solver process (clear all assertions).

return_solver(PoolPid, SolverPid)

-spec return_solver(pid(), pid()) -> ok.

Return a solver to the pool.

start_pool(Opts)

-spec start_pool(map()) -> {ok, pid()}.

Start a solver process pool.

start_solver(Solver, Timeout)

-spec start_solver(z3 | cvc5, integer()) -> {ok, pid()} | {error, term()}.

Start a solver process.

Arguments

  • Solver - Solver type (z3 or cvc5)
  • Timeout - Query timeout in milliseconds

Returns

  • {ok, Pid} - Solver process PID
  • {error, Reason} - Error starting solver

start_solver(Solver, Timeout, Opts)

-spec start_solver(z3 | cvc5, integer(), list()) -> {ok, pid()} | {error, term()}.

stop_pool(Pid)

-spec stop_pool(pid()) -> ok.

Stop the solver pool.

stop_solver(Pid)

-spec stop_solver(pid()) -> ok.

Stop a solver process.

terminate/2