Module Instantiation (.ml)

module Instantiation: sig .. end

Exhaustive Instantiation features

Because the SMT solver only takes as input ground formulas, we need to do the instantiation of quantifiers inside the model checker. The simplest (and complete) way to do this is to saturate exhaustively with the process varialbles (skolems).

val relevant : of_cube:Cube.t -> to_cube:Cube.t -> Variable.subst list

relevant ~of_cube:a ~to_cube:b returns the list of relevant instantiations of the quantifiers of b for the test exists i1,... b => exists z1,... a. Eliminates trivial useless (because they make the goal inconsistent) instantiations with simple checks.

Quadratic in the size of the largest contiguous subset of a and b of atoms with terms of the same type.

val exhaustive : of_cube:Cube.t -> to_cube:Cube.t -> Variable.subst list

Same as Instantiation.relevant but does not performs any checks