module type S =
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.