Module `C2ICandidate`

Wraps the candidate invariants with info about their cost etc.

type t: Contains the info needed for the moves on a candidate.

val mk : TransSys.t -> t: Creates a new candidate that can be randomly moved. Should be called only once as it mines the init and trans predicates. Use reset to launch a new C2I run.

val reset : t -> t: Resets a candidate.

val terms_of : t -> Term.t list list: Term of a candidate as a Term.t list list (dnf).

val term_of : t -> Term.t: Term of a candidate as a Term.t.

val move : t -> t: Makes a move on a candidate.

type rated_t: A candidate augmented with a cost and a rating.

val cost_of_rated : rated_t -> int: The cost of a rated candidate.

val candidate_of_rated : rated_t -> t: The candidate of a rated candidate.

val rated_cost_function : t -> Model.t list -> (Model.t * Model.t) list -> Model.t list -> rated_t: Computes the cost of a candidate and rates its atoms.

val rated_move : rated_t -> t: Moves a rated candidate.