Module Solver.Make_SAT

Parameters

• S : S

Signature

exception NODE_FREE

Raised when the matching pattern has no nodes.

val solver_type : 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.

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

occurrence ~target ~pattern returns an occurrence if the ~pattern occurs in the ~target. Different occurrences might be returned depending on which external solver is used.

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 -> occ list

occurrences ~target ~pattern returns a list of occurrences. Each occurrence is normalised by picking the smallest occurrence (lexicographic ordering) in the symmetry group.

raises NODE_FREE

when the ~pattern has an empty node set.

val occurrences_raw : target:Big.t -> pattern:Big.t -> 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 equal : Big.t -> Big.t -> bool

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

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

Same as Solver.M.equal but with fewer checks prior to the solver invocation. This function is intended to be used after equality over keys has already failed.

module Memo : sig ... end

Memoised interface.