Compress (kind2dev@731decdf5fb1.Compress)

val function_symbol_name : unit -> string

val init : (UfSymbol.t -> unit) -> TransSys.t -> unit

Initialize compression

The first argument is the function to declare an uninterpreted function symbol in a solver instance, the second the transition system.

val incr_k : unit -> unit

val check_and_block : 
  (UfSymbol.t -> unit) ->
  TransSys.t ->
  Model.path ->
  Term.t list

Given an inductive counterexample return a list of terms to force those states on the path to be different that are equivalent under some simulation relations.

val only_bv : TransSys.t -> bool