Module Bigraph.Solver

Unified interface to external solvers.

type nonrec solver_t = Solver_intf.solver_t =
  1. | MSAT
  2. | MCARD
  3. | GBS
type nonrec solution = Solver_intf.solution =
  1. | SAT
  2. | UNSAT
val pp_solution : Ppx_deriving_runtime.Format.formatter -> solution -> Ppx_deriving_runtime.unit
val show_solution : solution -> Ppx_deriving_runtime.string
type nonrec value = Solver_intf.value =
  1. | False
  2. | True
  3. | Unknown
val pp_value : Ppx_deriving_runtime.Format.formatter -> value -> Ppx_deriving_runtime.unit
val show_value : value -> Ppx_deriving_runtime.string
type nonrec occ = Solver_intf.occ

The type of occurrences.

val occ_to_yojson : occ -> Yojson.Safe.t
val occ_of_yojson : Yojson.Safe.t -> occ Ppx_deriving_yojson_runtime.error_or
val occ_nodes : occ -> Iso.t

Node mapping of an occurrence.

val occ_edges : occ -> Iso.t

Edge mapping of an occurrence.

val occ_hyper_edges : occ -> Fun.t

Hyper-edge mapping of an occurrence.

val occ_make : nodes:Iso.t -> edges:Iso.t -> hyper_edges:Fun.t -> occ

Construct an occurrence from its components.

val pp_occ : Stdlib.Format.formatter -> occ -> unit
val show_occ : occ -> string
module type E = Solver_intf.E
module type S = Solver_intf.S
module type M = Solver_intf.M
module MS : S

Instance of MiniSat solver.

module MC : S

Instance of MiniCARD solver.

module GBS : M

Instance of GBS solver.

module Make_SAT (_ : S) : M
type match_metrics = {
  1. mutable filtered_occs : int;
  2. mutable solver_vars : int;
  3. mutable solver_clauses : int;
  4. mutable solver_max_enc : int;
  5. mutable solver_max_clauses : int;
  6. mutable solver_matches : int;
  7. mutable solver_time_ms : float;
  8. mutable trivial_matches : int;
}

Accumulated metrics for matching operations. The solver_vars and solver_clauses fields total SAT encoding size across all matching calls; solver_max_enc tracks the largest single encoding (peak variable count); solver_max_clauses tracks the largest clause count in a single encoding; solver_matches counts encoding calls; solver_time_ms is total CPU time (milliseconds), measured by the solver's own C getrusage clock, spent inside SAT solve/solve_all calls, and is 0 under the GBS backend (which never invokes the SAT solver); trivial_matches counts matches resolved without SAT (1-2 node, no-edge patterns). Reset after reading via get_and_reset_metrics.

val get_and_reset_metrics : unit -> match_metrics

Read accumulated matching metrics and reset the counter. Call after each model run to collect stats.

val set_metrics_enabled : bool -> unit

Enable or disable benchmark-metrics recording. Enabled only when the --metrics-json flag is requested, so an unrequested run performs no counter writes. Call before a model run.

val clear_caches : unit -> unit

Clear all solver caches (SBC generator cache). Call before each model run when using the solver as a library to avoid stale entries.