A  
Abdrule 
An abduction rule used in an abductive cyclic prover.

Abducer 
A cyclic abducer (cf.

B  
Bidirectional [Sl_unify]  
Blist 
List operations.

C  
Containers 
Given a
BasicType build a module with several containers for it.

E  
Elt [Tags]  
Elt [Ord_constraints]  
F  
FList [Sl_tpair] 
A list of term pairs.

FList [Sl_term]  
FList [Containers.S]  
Flist 
A functorised list.

Form [Tl_form_ltl]  
Form [Tl_form]  
Fun 
Combinators for manipulating functions.

H  
Hashmap [Containers.S]  
Hashset [Containers.S]  
Hashset 
This module implements imperative sets as hash tables.

I  
Int 
Int
BasicType with assorted containers.

L  
ListSet [Sl_tpair] 
A set of term pairs

Listset 
A listbased set container.

Lru 
Implementation of an LRU cache for memoising functions.

M  
MSet [Sl_pred]  
MSet [Containers.S]  
Make [Containers] 
Functor putting together the different containers.

Make [Treeset] 
Create an ordered container.

Make [Pair] 
Create functions for equality, comparison, hashing and printing for a
pair of types.

Make [Treemap] 
Create an ordered map using a treebased representation.

Make [Listset] 
Create an ordered container whose underlying representation is a list.

Make [Multiset] 
Create an ordered container that behaves like a bag (
add always increases
size by one).

Make [Flist] 
Given a type with comparison, equality and printing facilities, build
the same facilities for lists of that type.

Make [Abducer]  
Make [Abdrule]  
Make [Seqtactics]  
Make [Prover]  
Make [Proof]  
Make [Proofrule]  
Make [Proofnode]  
Make [Lru] 
Implementation of an LRU cache for memoising functions whose arguments
can be compared for equality and can be hashed.

Make [Hashset] 
Functor building an implementation of the hashtable structure.

MakeUnifier [Unification] 
This functor makes a mk_unifier function for a particular implementation of
a container.

Map [Sl_term] 
An ordered map with terms as keys.

Map [Containers.S]  
Multiset 
A multiset container.

O  
Option 
Functions for manipulating optional values.

Ord_constraints 
A structure representing a set of constraints on ordinalvalued variables.

P  
Pair 
Operations on pairs.

Proof 
A cyclic proof object.

Proof [Sigs.ABDUCER]  
Proof [Sigs.PROVER]  
Proofnode 
A node in a cyclic proof.

Proofrule 
A proofrule used by a cyclic prover.

Prover 
A cyclic prover object.

S  
Seq [Sigs.ABDUCER]  
Seq [Sigs.PROVER]  
Seqtactics 
Tactics for combining sequentlevel rules.

Set [Sl_term] 
An ordered set of terms.

Set [Containers.S]  
Sigs 
Core module signatures used in Cyclist.

Sl_abduce 
This module contains functions to answer various abduction questions for
use in program verification.

Sl_deqs 
Sets of disequalities over terms.

Sl_form 
SL formula, basically a list of symbolic heaps, denoting their disjunction,
along with a set of contraints on predicate ordinal labels (tags).

Sl_form_rho 
SL formula, basically a list of symbolic heaps, denoting their disjunction.

Sl_heap 
Symbolic heaps.

Sl_heap_rho 
Symbolic heaps.

Sl_indrule 
Inductive rule type consisting of a symbolic heap and a predicate head.

Sl_pred 
Predicate occurrences consisting of a predicate identifier and a list of
terms as parameters.

Sl_pto 
Pointsto atom, consisting of a pair of a term and a list of terms.

Sl_ptos 
Multiset of pointstos.

Sl_rho 
A stack structure for prophecy variables.

Sl_seq 
SL sequent, as a pair of SL formulas.

Sl_subst 
Module providing SL term substitutionrelated functionality.

Sl_term 
Module defining SL terms, which consist of variables (free
or existentially quantified), or the constant
nil .

Sl_tpair 
An ordered pair of SL terms.

Sl_tpred 
Tagged predicate, as a pair of an integer and a predicate.

Sl_tpreds 
Multiset of tagged predicates.

Sl_uf 
A unionfind structure for SL terms.

Sl_unify 
This module specialises the generic Unification module to the SL
instantiation of cyclist and provides extra functionality to support the
unification of its various elements

Soundcheck 
Provides an abstract view of a proof as a graph and allows checking its
soundness.

Strng 
String
BasicType with assorted containers.

Subst [Sl_term] 
Substitutions over terms

Subst [VarManager.S]  
T  
Tagpairs 
A set of tag pairs with a few convenience functions.

Tags 
A set of tags.

Tl_form 
A CTL temporal logic formula

Tl_form_ltl 
An LTL temporal logic formula

Treemap 
An ordered map using the standard
Map module.

Treeset 
An ordered container based on the standard
Set module.

U  
Unidirectional [Sl_unify]  
Unification 
A library of types and combinators supporting
continuationpassingstyle unifiers

Unifier [Tags.Elt]  
Utilsigs 
Signatures for containers and essential types.

V  
Var [VarManager.S] 
Abstract type of variables

VarManager 
An abstract datatype for managing variables.
