Generic_smtlib (astral.Astral_internal.Generic

exception NonStandardTerm of string

val translate_var : SMT.Variable.t -> string

val translate_header : 
  (Astral_internal.SMT.Variable.Sort.t -> string) ->
  SMT.Variable.t list ->
  string

val translate_std : 
  (SMT.t -> string) ->
  (Astral_internal.SMT.Variable.Sort.t -> string) ->
  SMT.t ->
  Stdlib.String.t

Translation of standard terms. Translation of non-standard term raises exception that should be handled by concrete solver.

val translate_std_sort : (Sort.t -> string) -> Sort.t -> string

val translate_expr_list : (SMT.t -> string) -> SMT.t list -> string

val declare_std_sort : 'a -> string

All currently used standard sort do not need any declaration.