Module Oracle

module Oracle: 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 !


module type S = sig .. end