An abduction rule used in an abductive cyclic prover.
A cyclic abducer (cf.
A list of term pairs.
A functorised list.
Combinators for manipulating functions.
This module implements imperative sets as hash tables.
A set of term pairs
A list-based set container.
Implementation of an LRU cache for memoising functions.
Functor putting together the different containers.
Create an ordered container.
Create functions for equality, comparison, hashing and printing for a pair of types.
Create an ordered map using a tree-based representation.
Create an ordered container whose underlying representation is a list.
Create an ordered container that behaves like a bag (
Given a type with comparison, equality and printing facilities, build the same facilities for lists of that type.
Implementation of an LRU cache for memoising functions whose arguments can be compared for equality and can be hashed.
Functor building an implementation of the hashtable structure.
This functor makes a mk_unifier function for a particular implementation of a container.
An ordered map with terms as keys.
A multiset container.
Functions for manipulating optional values.
A structure representing a set of constraints on ordinal-valued variables.
Operations on pairs.
A cyclic proof object.
A node in a cyclic proof.
A proofrule used by a cyclic prover.
A cyclic prover object.
Tactics for combining sequent-level rules.
An ordered set of terms.
Core module signatures used in Cyclist.
This module contains functions to answer various abduction questions for use in program verification.
Sets of disequalities over terms.
SL formula, basically a list of symbolic heaps, denoting their disjunction, along with a set of contraints on predicate ordinal labels (tags).
SL formula, basically a list of symbolic heaps, denoting their disjunction.
Inductive rule type consisting of a symbolic heap and a predicate head.
Predicate occurrences consisting of a predicate identifier and a list of terms as parameters.
Points-to atom, consisting of a pair of a term and a list of terms.
Multiset of points-tos.
A stack structure for prophecy variables.
SL sequent, as a pair of SL formulas.
Module providing SL term substitution-related functionality.
Module defining SL terms, which consist of variables (free or existentially quantified), or the constant
An ordered pair of SL terms.
Tagged predicate, as a pair of an integer and a predicate.
Multiset of tagged predicates.
A union-find structure for SL terms.
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
Provides an abstract view of a proof as a graph and allows checking its soundness.
Substitutions over terms
A set of tag pairs with a few convenience functions.
A set of tags.
A CTL temporal logic formula
An LTL temporal logic formula
An ordered map using the standard
An ordered container based on the standard
A library of types and combinators supporting continuation-passing-style unifiers
Signatures for containers and essential types.
Abstract type of variables
An abstract datatype for managing variables.