Module type Oracle.S

module type S = sig .. end

Interface for oracles

Oracles provide a way to discard candidate invariants. The safety and correctness of Cubicle does not depend on the oracle, so any answer can be returned. However the efficiency of BRAB does. So the more precise the oracle, the better !

val init : Ast.t_system -> unit

Initialize the oracle on a given system

val first_good_candidate : Node.t list -> Node.t option

Given a list of candidate invariants, returns the first one that seems to be indeed an invariant.