Module Smtgraph

module Smtgraph: sig .. end

Graph of formulas

Each nodes is a conjunction (list) of boolean formulas with an id (for uniqueness purposes).

The implementation is functorized to hide Z3's context. Here is the typical way to use this module :

      module ZZ3 = ZZ3.Make (struct let ctx = Z3.mk_context [] end)

      module Smtg = Smtgraph.Make (ZZ3)

    

module Make (ZZ3 : ZZ3_sigs.S) : sig .. end