Module Bigraph.Solver

type solver_t =
| MSAT

MiniSAT

| MCARD

MiniCARD

Solver type.

type stats = {
v : int;

Number of variables.

c : int;

Number of clauses.

mem : float;

Memory used in MB.

cpu : float;

CPU time in seconds.

}

Solver statistics.

type solution =
| SAT
| UNSAT

Type of solver solutions.

type value =
| False
| True
| Unknown

Type of solver values.

val string_of_value : value -> string

String representation of a solver value.

type occ = {
nodes : Iso.t;

One-to-one mapping over nodes.

edges : Iso.t;

One-to-one mapping over edges.

hyper_edges : Fun.t;

Mapping over hyper-edges.

}

The type of occurrences.

val pp_occ : Stdlib.Format.formatter -> occ -> unit

Pretty printer

module type E = sig ... end

External solver interface.

module type S = sig ... end

Solver interface.

module MS : S

Instance of MiniSat solver.

module MC : S

Instance of MiniCARD solver.

module type M = sig ... end

The type of a bigraph matching engine.

module Make_SAT : functor (S : S) -> M

Bigraph matching engine based on solver S