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 listrelevant ~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 listSame as Instantiation.relevant but does not performs any checks