AnalyzeCFG.Slvrmodule EqSys : sig ... endmodule VH : sig ... endmodule Sol' : sig ... endmodule Splitter : sig ... endtype marshal = Sol'.marshalval copy_marshal : Sol'.marshal -> Sol'.marshalval relift_marshal : Sol'.marshal -> Sol'.marshalval solve :
(SpecSys.EQSys.LVar.t * SpecSys.EQSys.D.t) list ->
(SpecSys.EQSys.GVar.t * SpecSys.EQSys.G.t) list ->
SpecSys.EQSys.LVar.t list ->
Sol'.marshal option ->
(SpecSys.EQSys.D.t SpecSys.LHT.t * SpecSys.EQSys.G.t SpecSys.GHT.t)
* Sol'.marshal