PathBound (astral.Astral_internal.PathBound)

module TermSet = SL.Term.Set

module Logger : Logger_sig.LOGGER

exception NoPath

module M : sig ... end

val bound_cache : (int * int) M.t Stdlib.ref

val cache_add : 
  (SL.Term.t * SL.Term.t * MemoryModel.Field.t) ->
  (int * int) ->
  unit

val cache_find : (SL.Term.t * SL.Term.t * MemoryModel.Field.t) -> int * int

val cache_reset : unit -> unit

val path_lower_bound : 
  SL_graph0.t ->
  MemoryModel.Field.t ->
  SL.Term.t ->
  SL.Term.t ->
  int

val path_upper_bound : 
  SL_graph0.G.t ->
  MemoryModel.Field.t ->
  SL.Term.t ->
  SL.Term.t ->
  int ->
  int

val partial_path : 
  SL_graph0.G.t ->
  MemoryModel.Field.t ->
  SL.Term.t ->
  SL.Term.t ->
  SL_graph0.G.vertex list

val root_weight : 
  SL_graph0.G.t ->
  SL.t ->
  HeapSort.t ->
  SL_graph0.G.vertex ->
  int

val alloc_bound : 
  SL_graph0.G.t ->
  SL.t ->
  HeapSort.t ->
  MemoryModel.Field.t ->
  Astral_internal.SL_graph.G.vertex ->
  SL.Term.t ->
  int ->
  int

val compute : 
  SL_graph0.G.t ->
  SL.t ->
  HeapSort.t ->
  MemoryModel.Field.t ->
  SL.Term.t ->
  SL.Term.t ->
  int ->
  int * int