Parameter Make._

exception NODE_FREE

Raised when the matching pattern has no nodes.

val solver_type : Solver_intf.solver_t

The type of the solver.

val string_of_solver_t : string

String representation of a solver type.

val occurs : target:Big.t -> pattern:Big.t -> bool

occurs ~target ~pattern returns true if the ~pattern occurs in the ~target, false otherwise. A node-free pattern (no nodes) always returns true.

type param_filter = {
  1. n_p_orig : Big.nodes_t;
    (*

    Pattern nodes (unflattened), for pre-encoding parameter filtering.

    *)
  2. n_t_orig : Big.nodes_t;
    (*

    Target nodes (unflattened), for pre-encoding parameter filtering.

    *)
}
val param_filter_none : param_filter

Empty parameter filter: disables pre-encoding parameter compatibility filtering. Use when the original (unflattened) node maps are not available or when parameter filtering is not needed.

val occurrence : target:Big.t -> pattern:Big.t -> param_filter:param_filter -> Solver_intf.occ option

occurrence ~target ~pattern ~param_filter returns an occurrence if the ~pattern occurs in the ~target. The ~param_filter parameter allows the SAT solver to apply pre-encoding parameter compatibility filtering when the original (unflattened) node maps are available. Pass {n_p_orig = Nodes.empty; n_t_orig = Nodes.empty} to skip.

  • raises NODE_FREE

    when the ~pattern has an empty node set.

val auto : Big.t -> (Iso.t * Iso.t) list

Compute the non-trivial automorphisms of a bigraph. The elements of each output pair are an automorphism over the place graph and an automorphism over the link graph, respectively.

val occurrences : target:Big.t -> pattern:Big.t -> rname:string -> param_filter:param_filter -> Solver_intf.occ list

occurrences ~target ~pattern ~rname ~param_filter returns a list of all occurrences of ~pattern in ~target. No solver-level symmetry breaking or orbit filtering is applied: pruning occurrences related by a pattern automorphism is unsound for BRS when the rule's RHS distinguishes symmetric pattern nodes. The React layer applies the correct successor-based deduplication. The ~param_filter parameter allows the SAT solver to apply pre-encoding parameter compatibility filtering when the original (unflattened) node maps are available. Pass {n_p_orig = Nodes.empty; n_t_orig = Nodes.empty} to skip.

  • raises NODE_FREE

    when the ~pattern has an empty node set.

val occurrences_raw : target:Big.t -> pattern:Big.t -> Solver_intf.occ list

Same as Solver.M.occurrences but without filtering symmetric occurrences out.

  • raises NODE_FREE

    when the ~pattern has an empty node set.

val occurrences_wildcard : target:Big.t -> pattern:Big.t -> ?t_flat:Big.t -> group_lhs:Big.t list -> unit -> Solver_intf.occ list

Wildcard matching: match ignoring control parameter values. Caller must post-filter by control equality.

group_lhs must contain the LHS bigraphs of every rule in the caller's rule group (the rules sharing the structural key of pattern). SBC symmetry breaking is applied only to node swaps that are safe for every rule in the group: the full control at the two swapped positions must be equal across all group LHSes and carry no constraint (capture) parameter. An unsafe swap could prune the only occurrence that is valid for a single rule, since pruning is decided on the group representative's template while per-rule control validation happens afterwards in the caller.

  • raises NODE_FREE

    when the ~pattern has an empty node set.

val sbc_group_order_direct : pattern:Big.t -> n_p_orig:Big.nodes_t -> int

Order of the safe-automorphism group that the direct SAT path prunes with symmetry breaking (occurrences with ~param_filter). A set of SBC transposition generators is a subgroup of the symmetric group: a connected set of transpositions on k vertices generates S_k, so the group order is the product of (size)! over the connected components of the transposition graph. pattern must be the (already flattened) pattern passed to occurrences; n_p_orig the original LHS node table, so the same W2 filter is applied. Returns 1 for solvers that do not prune (GBS).

val sbc_group_order_wildcard : pattern:Big.t -> group_lhs:Big.t list -> int

Order of the safe-automorphism group that the wildcard SAT path prunes with symmetry breaking (occurrences_wildcard). pattern is the group representative's LHS (it is flattened here to mirror occurrences_wildcard); group_lhs the LHS of every rule in the group, so the same W2 filter is applied. Returns 1 for solvers that do not prune (GBS).

val equal : Big.t -> Big.t -> bool

equal a b returns true if bigraphs a and b are isomorphic, false otherwise.

val equal_no_key : Big.t -> Big.t -> bool

Same as equal but skips the structural key comparison. Use only when the caller has already verified both bigraphs share the same key.

val show_occ : Solver_intf.occ -> string

String representation of an occurrence.

val pp_occ : Stdlib.Format.formatter -> Solver_intf.occ -> unit
val occ_nodes : Solver_intf.occ -> Iso.t

Node mapping of an occurrence.

val occ_edges : Solver_intf.occ -> Iso.t

Edge mapping of an occurrence.

val occ_hyper_edges : Solver_intf.occ -> Fun.t

Hyper-edge mapping of an occurrence.

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

Construct an occurrence from its components.

val clear_caches : unit -> unit

Clear internal caches (flattened pattern automorphism cache). Call before each model run when using the solver as a library.