Module type Bwd.Strategy

module type Strategy = sig .. end

val search : ?invariants:Node.t list ->
?candidates:Node.t list -> Ast.t_system -> Bwd.result

Backward reachability search on a system. The user can also provide invariants that are true of the system to help the search. Candidate invariants can also be provided, they will be proven as real invariants if necessary.