Module Fixpoint.FixpointTrie (.ml)

module FixpointTrie: sig .. end

Fixpoint tests on trie structures

val easy_fixpoint : Node.t -> Node.t Cubetrie.t -> int list option

easy fixpoint test with subset tests

val peasy_fixpoint : Node.t -> Node.t Cubetrie.t -> int list option

easy fixpoint test including permutations

val hard_fixpoint : Node.t -> Node.t Cubetrie.t -> int list option

full semantic fixpoint test with SMT solver

val check : Node.t -> Node.t Cubetrie.t -> 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.