SMTLIB_printer (astral.Astral_internal.SMTLIB

val declare_sort : Astral_internal.SL.Sort.t -> string

val declare_struct : MemoryModel.StructDef.t -> string

val declare_pred : InductiveDefinition.t -> string

val used_predicates : SL.t -> InductiveDefinition.t list

Compute the minimal set of predicates that need to be defined: 1. It appears directly in formula. 2. It is used to define another predicate already in the set.

val used_structures : 
  SL.t ->
  InductiveDefinition.t list ->
  MemoryModel.StructDef.MonoList.t

Compute the minimal set of structures that need to be defined: 1. It appears in a points-to in formula. 2. It appears in a points-to in some defined predicate.

val used_sorts : 
  SL.t ->
  MemoryModel.StructDef.t list ->
  Astral_internal.SL.Sort.MonoList.t

val generate_logic_string : SL.t -> string

val declare_heap_sort : HeapSort.t -> string

val generate_definitions : SL.t -> HeapSort.t -> string

val output_benchmark : 
  ?source:string ->
  ?status:[< `Sat | `Unknown | `Unsat ] ->
  string ->
  ParserContext.t ->
  unit