Functor Smtgraph.Make

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

Parameters:

ZZ3 : ZZ3_sigs.S

include Graph.Sig.P

val get_clauses : V.t -> ZZ3.zbool ZZ3.term list

val from_llvm : (Llvmcfg.vertex -> ZZ3.zbool ZZ3.term list) -> Llvmcfg.vertex -> vertex

Dot export

module Dot: sig .. end

Pretty print to dot graphviz format.

val to_smt : t -> [> ZZ3.zbool ] ZZ3.term

Gather all the formulas of the graph in one big smt formula.