NLS (astral.Astral_internal.NLS)

val loc_nls : Sort.t

val struct_nls : MemoryModel.StructDef.t

val mk_pto : SL.Term.t -> top:SL.Term.t -> next:SL.Term.t -> SL.t

val mk : SL.Term.t -> sink:SL.Term.t -> bottom:SL.Term.t -> SL.t

val register : unit -> unit

include ID_sig.BUILTIN

include ID_sig.BUILTIN_BASE

val name : string

Name of the inductive predicate.

val signature : Sort.t list

val default_instantiation : MemoryModel.StructDef.t list

val must_allocated : SL.Term.t list -> SL.Term.t list

val unique_footprint : bool

True iff the predicate has unique footprint.

val struct_defs : MemoryModel.StructDef.t list

val heap_sort : HeapSort.t

val term_bound : SL.t -> HeapSort.t -> SL.Term.t -> float

val sl_graph : ID_sig.instance -> SL_graph0.t

val additional_bound : SL.t -> LocationBounds0.t

val rules : (SL.Variable.t list * MemoryModel.StructDef.t list) -> SL.t list

val global_preprocessing : SL.t -> SL.t

module Bound : sig ... end

module Translation (E : Translation_sig.ENCODING) : sig ... end

Preprocessing

val preprocess : SL_graph0.t -> SL.Term.t list -> SL.t option

Model checking

val model_check : ID_sig.instance -> StackHeapModel.t -> bool

val compute_footprints : 
  ID_sig.instance ->
  StackHeapModel.t ->
  StackHeapModel.Footprint.t

val instantiate : 
  HeapSort.t ->
  SL.Term.t list ->
  (SL.t, string) Stdlib.Result.t

This function may return arbitrary SL formula, not necessary containing the predicate. For example, ls(nil, x) will be instantiated as nil = x to prevent problems with nil.