Module Fixpoint.FixpointList (.ml)

module FixpointList: sig .. end

Fixpoint tests on list structures

val check : Node.t -> Node.t list -> int list option

check s v returns the tags of nodes in v that were used if s implies the disjunction of the nodes in v. Otherwise, it returns None.

val pure_smt_check : Node.t -> Node.t list -> int list option

Same as check but only uses the SMT solver. Only use for benchmarking purposes or for reference implementation.