Module Compress

module Compress: sig .. end
Path compression for k-induction
Author(s): Christoph Sticksel

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.