_false [Fun]  
_true [Fun]  
A  
a_step [Tl_form.Form]  
abd_bi_substs [Sl_abduce]  
abd_substs [Sl_abduce]  abd_substs f f' returns an option result that consists of a pair of
formulas (g, g') and a list of substitutions substs such that: f entails g , g' entails f' , for all substitutions theta in substs , theta applied to g' is a
subformula of g , and if the optional argument allow_frame=true is
set to false, then also the spatial parts are equal.

add [Sl_rho]  
add [Sl_uf]  
add [Hashset.S]  
add_axiom [Sigs.PROOF]  
add_backlink [Sigs.PROOF]  
add_bindings [Utilsigs.OrderedMap] 
Add all bindings in provided list to map.

add_constraints [Sl_form]  add_constraints f cs returns the formula the results by adding cs to the
constraints already in f

add_deq [Sl_heap_rho]  
add_deq [Sl_heap]  
add_eq [Sl_heap_rho]  
add_eq [Sl_heap]  
add_ind [Sl_heap_rho]  
add_ind [Sl_heap]  
add_inf [Sigs.PROOF]  
add_pto [Sl_heap_rho]  
add_pto [Sl_heap]  
add_subprf [Sigs.PROOF]  add_subprf p idx p' replaces the node idx in p' with a copy of p .

all_nodes [Sigs.PROOFRULE] 
Readymade selection functions doing the obvious.

all_pairs [Ord_constraints]  all_pairs cs returns all of the tag pairs (a , b ) such that a <= b
is entailed by some constraint in cs

all_subheaps [Sl_heap_rho]  all_subheaps h returns a list of all the subheaps of h .

all_subheaps [Sl_heap]  all_subheaps h returns a list of all the subheaps of h .

ancestor_nodes [Sigs.PROOFRULE]  
anonymous [VarManager.I] 
An "unidentified" variable

anonymous [Tags]  
append [Blist] 
Catenate two ts.

apply [VarManager.SubstSig] 
Apply a substitution to a variable

apply [Pair] 
Apply a function taking two arguments to the members of a pair.

apply_to_tag [Tagpairs]  apply_to_tag tps t treats tps as a substitution and applies it to t .

args [Sl_tpred]  
args [Sl_pred]  
arity [Sl_indrule]  
arity [Sl_tpred]  
arity [Sl_pred]  
assoc [Blist]  assoc a l returns the value associated with key a in the t of
pairs l .

assq [Blist] 
Same as
List.assoc , but uses physical equality instead of structural
equality to compare keys.

attempt [Sigs.ABDRULE]  
attempt [Sigs.PROOFRULE] 
Try a rule and if it fails act as
identity .

attempt [Sigs.SEQTACTICS]  
avoid [VarManager.SubstSig]  avoid vars subvars
returns a substitution that takes all variables in subvars to
variables fresh in vars U subvars , respecting existential
quantification / free variables.

avoid_replacing_tags [Sl_unify.Unidirectional]  
avoid_replacing_trms [Sl_unify.Unidirectional] 
A state update check which prevents replacements of variables within the
given set of terms.

B  
backtrack [Unification]  backtrack u takes a cpsstyle unifier u and produces a
backtracking unifier that returns a list of all possible
solutions returned by u such that cont solution is not
None.

bfs [Sigs.ABDUCER]  
bind [Option]  
bind [Blist]  
bindings [Sl_rho] 
Return mapping as a list of pairs of terms and values
Additional guarantees: Pairs are ordered lexicographically, based on
Sl_term.compare .

bindings [Sl_uf] 
Return mapping as a list of pairs, where pair members are ordered by

biunify [Sl_tpreds]  
biunify [Sl_tpred]  
biunify [Sl_pred]  
biunify [Sl_ptos]  
biunify [Sl_pto]  
biunify [Sl_tpair]  
biunify [Sl_term.FList] 
Unifies two lists of terms by producing substitutions to act on each list respectively

biunify [Sl_term] 
Unifies two terms by producing substitutions to act on each term respectively

biunify [Tags.Elt] 
Unifies two tags by finding suitable substitutions (represented as a set of tag pairs)
for each tag which makes them equal.

biunify [Ord_constraints.Elt]  
biunify [Ord_constraints]  
biunify_partial [Sl_heap]  
biunify_partial [Sl_deqs]  
biunify_partial [Sl_uf]  
body [Sl_indrule]  
both [Pair] 
Alias for
conj

build_proof [Soundcheck]  
but_last [Blist] 
Return a list containing all elements apart from the last one.

C  
cardinal [Hashset.S]  
cartesian_hemi_square [Blist] 
Return a list of all pairs out of elements of a list, but without including
symmetric pairs.

cartesian_product [Blist]  
check [Sigs.PROOF] 
Check soundness.

check_proof [Soundcheck] 
Validate, minimise, check soundness of proof/graph and memoise.

choice [Sigs.ABDRULE]  
choice [Sigs.PROOFRULE] 
Apply a list of rules on current subgoal and return all applications.

choice [Sigs.SEQTACTICS]  
choose [Blist]  choose [[1;2;3]; [4;5]] returns [[1;4];[1;5];[2;4];[2;5];[3;4];[3;5]] .

classical_biunify [Sl_heap]  
classical_unify [Sl_heap_rho] 
Unify two heaps, by using
unify_partial for the pure (classical) part whilst
using unify for the spatial part.

classical_unify [Sl_heap] 
Unify two heaps, by using
unify_partial for the pure (classical) part whilst
using unify for the spatial part.

clear [Hashset.S]  
close [Ord_constraints]  close cs generates the set of all constraints entailed by cs

closed_nodes [Sigs.PROOFRULE]  
combine [Sl_heap_rho]  
combine [Blist] 
Transform a pair of ts into a t of pairs:
combine [a1; ...; an] [b1; ...; bn] is
[(a1,b1); ...; (an,bn)] .

combine_axioms [Sigs.PROOFRULE]  
combs [Blist]  combs n l returns all combinations of n elements from l .

compare [Tl_form_ltl.Form]  
compare [Tl_form.Form]  
compare [Utilsigs.BasicType] 
Standard comparator, return <0 if first less than second, 0 if equal, >0 if greater.

complete_tags [Tl_form_ltl.Form]  
complete_tags [Tl_form.Form]  
complete_tags [Sl_form]  complete_tags ts f returns the formula obtained from f by assigning
all untagged predicates a fresh existential tag, avoiding those in ts .

complete_tags [Sl_heap_rho]  complete_tags exist ts h returns the symbolic heap obtained from h
by assigning all untagged predicates a fresh existential tag avoiding
those in ts .

complete_tags [Sl_heap]  complete_tags exist ts h returns the symbolic heap obtained from h
by assigning all untagged predicates a fresh existential tag avoiding
those in ts .

compose [Tagpairs]  compose l r computes the relation representing the composition of l with r .

compose [Sigs.ABDRULE]  
compose [Sigs.PROOFRULE] 
Apply the list of rules in the second argument in a pairwise fashion to
the premises generated by applying the first rule

compose [Sigs.SEQTACTICS]  
compose_pairwise [Sigs.PROOFRULE]  
compute_frame [Sl_form]  compute_frame f f' , computes the portion of f' left over (the 'frame')
from f and returns None when f is not subsumed by f' .

concat [Blist] 
Concatenate a t of ts.

conditional [Sigs.PROOFRULE]  
conj [Fun]  
conj [Pair] 
Compute the conjunction of a pair of booleans.

cons [Blist] 
Equivalent to
:: .

constructively_valued [Sl_indrule]  constructively_valued r returns true iff the body of r is
constructively valued (see Sl_heap ).

constructively_valued [Sl_heap]  constructively_valued h returns true if all variables in h are
c.valued.

copy [Hashset.S]  
create [Hashset.S]  
curry [Fun]  
D  
decons [Blist] 
Destruct a nonempty list.

del_deq [Sl_heap_rho]  
del_deq [Sl_heap]  
del_first [Utilsigs.OrderedContainer] 
Remove first element satisfying the given predicate.

del_first [Blist] 
Delete first element satisfying a given predicate.

del_ind [Sl_heap_rho]  
del_ind [Sl_heap]  
del_pto [Sl_heap_rho]  
del_pto [Sl_heap]  
dest [Sl_indrule]  
dest [Sl_seq] 
If both LHS and RHS are symbolic heaps then return them else raise
Sl_form.Not_symheap .

dest [Sl_form_rho] 
Return the single disjunct, if there is exactly one, else raise
Not_symheap .

dest [Sl_form] 
Return the single disjunct, if there is exactly one, else raise
Not_symheap .

dest [Sl_heap_rho]  
dest [Sl_heap]  
dest [Option]  
dest [Sigs.NODE]  dest n returns (sequent, description).

dest_af [Tl_form.Form]  
dest_ag [Tl_form.Form]  
dest_and [Tl_form_ltl.Form]  
dest_and [Tl_form.Form]  
dest_atom [Tl_form_ltl.Form]  
dest_atom [Tl_form.Form]  
dest_backlink [Sigs.NODE]  dest_backlink n destroys a backlink node n , otherwise raises Invalid_arg .

dest_box [Tl_form.Form]  
dest_circle [Tl_form.Form]  
dest_diamond [Tl_form.Form]  
dest_ef [Tl_form.Form]  
dest_eg [Tl_form.Form]  
dest_f [Tl_form_ltl.Form]  
dest_g [Tl_form_ltl.Form]  
dest_inf [Sigs.NODE]  dest_inf n destroys an inference node n , otherwise raises Invalid_arg .

dest_lazily [Option]  
dest_next [Tl_form_ltl.Form]  
dest_or [Tl_form_ltl.Form]  
dest_or [Tl_form.Form]  
dest_singleton [Tagpairs]  dest_singleton tps returns Some(tp) if tp is the only element of tps , and None otherwise.

diff [Sl_heap_rho]  
diff [Sl_heap]  
diff [Sl_rho]  diff rho rho' returns the structure given by removing all variables in
rho' from rho

diff [Sl_uf]  diff eqs eqs' returns the structure given by removing all equalities in
eqs' from eqs

direct [Fun]  
disequates [Sl_heap_rho] 
Does a symbolic heap entail the disequality of two terms?

disequates [Sl_heap] 
Does a symbolic heap entail the disequality of two terms?

disj [Sl_form_rho] 
Or two formulas (listappend).

disj [Sl_form] 
Or two formulas (listappend).

disj [Fun]  
disj [Pair] 
Compute the disjunction of a pair of booleans.

disjoint [Utilsigs.OrderedContainer] 
Decide if there are no common elements.

drop [Blist]  drop n l returns the suffix of l after skipping n elements.

E  
e_step [Tl_form.Form]  
either [Pair] 
Alias for
disj

empty [Sl_form_rho] 
The formula
emp .

empty [Sl_form] 
The formula
emp .

empty [Sl_heap_rho]  
empty [Sl_heap]  
empty [Sl_rho]  
empty [Sl_uf]  
empty [VarManager.SubstSig] 
The empty substitution, which has no effect when applied.

empty [Blist] 
The empty list constant.

empty_state [Sl_unify.S] 
The unifier state consisting of the empty substitution and the empty set of
tag pairs

endomap [Utilsigs.OrderedMap] 
Convert a map to another, by enumerating bindings in key order,
converting them into new ones and adding them to a new map.

endomap [Utilsigs.OrderedContainer] 
Map a set of elements to another set of elements of the same type.

equal [Tl_form_ltl.Form]  
equal [Tl_form.Form]  
equal [Sl_heap_rho] 
Checks whether two symbolic heaps are equal.

equal [Sl_heap] 
Checks whether two symbolic heaps are equal.

equal [Utilsigs.BasicType] 
Standard equality predicate.

equal [Sigs.SEQUENT] 
"Syntactic" equality.

equal [Hashset.HashedType] 
The equality predicate used to compare elements.

equal [Blist]  equal eq l l' computes pointwise equality between l and l' assuming
eq computes equality between elements.

equal_upto_tags [Tl_form_ltl.Form]  
equal_upto_tags [Tl_form.Form]  
equal_upto_tags [Sl_seq] 
Like
equal but ignoring LHS tags as well as RHS ones.

equal_upto_tags [Sl_form_rho] 
Whilst
equal demands syntactic equality including tags, this version
ignores tag assignment.

equal_upto_tags [Sl_form] 
Whilst
equal demands syntactic equality including tags, this version
ignores tag assignment.

equal_upto_tags [Sl_heap_rho] 
Like
equal but ignoring tag assignment.

equal_upto_tags [Sl_heap] 
Like
equal but ignoring tag assignment.

equal_upto_tags [Sl_tpreds] 
Test whether the two arguments are the equal ignoring tags.

equal_upto_tags [Sl_tpred] 
Compare for equality two tagged predicates while ignoring tags.

equal_upto_tags [Sigs.SEQUENT] 
As
equal but ignoring tags.

equates [Sl_heap_rho] 
Does a symbolic heap entail the equality of two terms?

equates [Sl_heap] 
Does a symbolic heap entail the equality of two terms?

equates [Sl_rho] 
Does a stack struct holds a term with a val?

equates [Sl_uf] 
Does a UF struct make two terms equal?

existential_intro [Sl_unify.Unidirectional]  
existential_split_check [Sl_unify.Unidirectional]  
existentials_only [Sl_unify.Unidirectional]  
exists [Hashset.S]  
exists [Blist]  exists p [a1; ...; an] checks if at least one element of
the t satisfies the predicate p .

exists2 [Blist] 
Same as
List.exists , but for a twoargument predicate.

explode_deqs [Sl_heap]  
extract_checkable_slformula [Tl_form_ltl.Form]  
extract_checkable_slformula [Tl_form.Form]  
extract_subproof [Sigs.PROOF]  extract_subproof idx prf returns prf rearranged such that idx is
the root node.

F  
fail [Sigs.ABDRULE]  
fail [Sigs.PROOFRULE] 
The rule that always fails.

fast_sort [Blist] 
Same as
List.sort or List.stable_sort , whichever is faster
on typical input.

filter [Hashset.S]  
filter [Blist]  filter p l returns all the elements of the t l
that satisfy the predicate p .

filter_vars [Sl_term] 
Remove
nil from a set of terms.

find [Sl_rho]  
find [Sl_uf]  
find [Utilsigs.OrderedContainer]  find p set returns the first element of set
that satisfies the predicate p .

find [Sigs.PROOF]  
find [Blist]  find p l returns the first element of the t l
that satisfies the predicate p .

find_all [Blist]  find_all is another name for List.filter .

find_index [Blist]  find_index pred l returns the position of the first x in l such that pred x = true or throws Not_found .

find_indexes [Blist]  find_indexes pred l returns the list of positions of all x in l such that pred x = true .

find_lval [Sl_heap_rho] 
Find pto whose address is provably equal to given term.

find_lval [Sl_heap] 
Find pto whose address is provably equal to given term.

find_map [Utilsigs.OrderedMap] 
Optimisation for finding and converting at the same time.

find_map [Utilsigs.OrderedContainer] 
Optimisation for finding and converting at the same time.

find_map [Blist] 
Optimisation for finding and converting at the same time.

find_opt [Utilsigs.OrderedContainer]  find_opt pred set returns Some x for the first x in set such
that pred x = true , or None .

find_opt [Blist]  find_opt pred l returns Some x for the first x in l such that pred x = true , or None .

first [Sigs.ABDRULE]  
first [Sigs.PROOFRULE] 
Apply a sequence of rules iteratively through
compose .

first [Sigs.SEQTACTICS]  
fixpoint [Sl_heap_rho]  
fixpoint [Sl_heap]  
fixpoint [Utilsigs.OrderedMap]  fixpoint val_equal f map computes the fixpoint of f using val_equal
to compare *values*.

fixpoint [Utilsigs.OrderedContainer]  
flatten [Tagpairs] 
Produce a set of all the tags in the given set of tag pairs.

flatten [Option]  
flatten [Blist] 
Same as
concat .

fold [Sl_indrule]  fold r h returns a list of pairs of substitutions over the formal parameters of
the rule r such that its body, when one of these substitutions is applied,
becomes a subformula of h ; and the result of removing that subformula from h .

fold [Sl_rho]  
fold [Sl_uf]  
fold [Option]  
fold [Pair] 
Fold a function over the members of a pair.

fold [Hashset.S]  
fold_left [Blist]  List.fold_left f a [b1; ...; bn] is
f (... (f (f a b1) b2) ...) bn .

fold_left2 [Blist]  List.fold_left2 f a [b1; ...; bn] [c1; ...; cn] is
f (... (f (f a b1 c1) b2 c2) ...) bn cn .

fold_right [Blist]  List.fold_right f [a1; ...; an] b is
f a1 (f a2 (... (f an b) ...)) .

fold_right2 [Blist]  List.fold_right2 f [a1; ...; an] [b1; ...; bn] c is
f a1 b1 (f a2 b2 (... (f an bn c) ...)) .

foldl [Blist]  
foldr [Blist]  
for_all [Sl_rho]  
for_all [Sl_uf]  
for_all [Hashset.S]  
for_all [Blist]  for_all p [a1; ...; an] checks if all elements of the t
satisfy the predicate p .

for_all2 [Blist] 
Same as
List.for_all , but for a twoargument predicate.

formals [Sl_indrule]  
fresh_evar [Sl_term]  fresh_evar s returns an existentially quantified variable that is
fresh in s .

fresh_evar [VarManager.I]  fresh_evar s returns an existential variable that is fresh for the set of variables s .

fresh_evars [Sl_term]  fresh_evars s n returns a list of existentially quantified variables
of length n all of which are fresh in s .

fresh_evars [VarManager.I]  fresh_evars s n returns n distinct existential variables that are all fresh for the set of variables s .

fresh_fvar [Sl_term]  fresh_fvar s returns a free variable that is fresh in s .

fresh_fvar [VarManager.I]  fresh_uvar s returns a free variable that is fresh for the set of variables s .

fresh_fvars [Sl_term]  fresh_fvars s n returns a list of free variables of length n
all of which are fresh in s .

fresh_fvars [VarManager.I]  fresh_uvars s n returns n distinct free variables that are all fresh for the set of variables s .

fresh_idx [Sigs.PROOF]  
fresh_idxs [Sigs.PROOF]  
freshen [Sl_indrule] 
Replace all variables in rule such that they are disjoint with the set
provided.

freshen_tags [Sl_heap_rho]  freshen_tags f g will rename all tags in g such that they are disjoint
from those of f .

freshen_tags [Sl_heap]  freshen_tags f g will rename all tags in g such that they are disjoint
from those of f .

freshen_tags [Sl_tpreds] 
Rename tags in second argument so that they are disjoint to those in the first.

G  
generate [Ord_constraints]  generate avoid t ts returns a constraint set that constitutes an inductive
hypothesis corresponding to a case in the unfolding of a predicate tagged
with t that recursively depends on predicate instances tagged by labels
in ts ; any freshly generated labels are not contained in avoid .

get [Option]  
get_ancestry [Sigs.PROOF]  
get_seq [Sigs.PROOF]  
get_seq [Sigs.NODE] 
Get sequent labelling the node.

get_succs [Sigs.NODE] 
Get the successor node indices of this node.

get_tracepairs [Sl_seq] 
Get the tracepairs between two sequents

get_tracepairs [Sl_form]  get_tracepairs f f' will return the valid and progressing trace pairs
(t, t') specified by the constraints of f' such that t occurs in f

H  
has_untagged_preds [Sl_heap_rho]  
has_untagged_preds [Sl_heap]  
hash [Tl_form_ltl.Form]  
hash [Tl_form.Form]  
hash [Utilsigs.OrderedMap] 
Hash the map using the provided function for hashing *values*.

hash [Utilsigs.BasicType] 
Standard hash function.

hash [Hashset.HashedType] 
A hashing function on elements.

hd [Blist] 
Return the first element of the given t.

I  
id [Fun]  
identity [Sigs.PROOFRULE]  
idents [Sl_heap_rho] 
Get multiset of predicate identifiers.

idents [Sl_heap] 
Get multiset of predicate identifiers.

idents [Sl_tpreds] 
Return multiset of identifiers present.

idfs [Sigs.PROVER]  
inconsistent [Sl_form_rho] 
Do all disjuncts entail false in the sense of
Sl_heap_rho.inconsistent ?

inconsistent [Sl_form] 
Do all disjuncts entail false in the sense of
Sl_heap.inconsistent
or are the tag constraints inconsistent?

inconsistent [Sl_heap_rho] 
Trivially false if x=y * x!=y is provable for any x,y.

inconsistent [Sl_heap] 
Trivially false if heap contains t!=t for any term t, or if x=y * x!=y
is provable for any x,y.

inconsistent [Ord_constraints]  
indexes [Blist]  indexes l returns the list of integer positions of elements in l .

intersperse [Blist] 
Insert given element between elements of given list.

is_af [Tl_form.Form]  
is_ag [Tl_form.Form]  
is_and [Tl_form_ltl.Form]  
is_and [Tl_form.Form]  
is_anonymous [VarManager.I]  is_unnamed v returns true if and only if v is anonymous

is_atom [Tl_form_ltl.Form]  
is_atom [Tl_form.Form]  
is_axiom [Sigs.NODE]  
is_backlink [Sigs.NODE]  
is_box [Tl_form.Form]  
is_checkable [Tl_form_ltl.Form]  
is_checkable [Tl_form.Form]  
is_circle [Tl_form.Form]  
is_closed [Sigs.PROOF] 
Are all nodes not open?

is_closed_at [Sigs.PROOF]  
is_diamond [Tl_form.Form]  
is_ef [Tl_form.Form]  
is_eg [Tl_form.Form]  
is_empty [Sl_heap_rho]  is_empty h tests whether h is equal to the empty heap.

is_empty [Sl_heap]  is_empty h tests whether h is equal to the empty heap.

is_empty [Sl_rho]  
is_empty [Sl_uf]  
is_empty [Hashset.S]  
is_empty [Blist] 
Is the argument the empty list?

is_exist_var [Sl_term] 
Is the argument an existentially quantified variable?

is_exist_var [VarManager.I]  is_exist_var v returns true if and only if v is an existential variable.

is_f [Tl_form_ltl.Form]  
is_final [Tl_form.Form]  
is_free_var [Sl_term] 
Is the argument a free variable?

is_free_var [VarManager.I]  is_exist_var v returns true if and only if v is a free variable.

is_g [Tl_form_ltl.Form]  
is_inf [Sigs.NODE]  
is_next [Tl_form_ltl.Form]  
is_nil [Sl_term] 
Is the argument
nil ? Equivalent to equal nil x .

is_none [Option]  
is_open [Sigs.NODE]  
is_or [Tl_form_ltl.Form]  
is_or [Tl_form.Form]  
is_slformula [Tl_form_ltl.Form]  
is_slformula [Tl_form.Form]  
is_some [Option]  
is_substitution [Sl_unify.Unidirectional]  
is_symheap [Sl_form_rho] 
Returns true iff the formula has a single disjunct only

is_symheap [Sl_form] 
Returns true iff the formula has a single disjunct only

is_tagged [Sl_tpred]  
is_var [Sl_term]  is_nil x is equivalent to not (equal nil x) .

iter [Option]  
iter [Fun]  
iter [Hashset.S]  
iter [Blist]  List.iter f [a1; ...; an] applies function f in turn to
a1; ...; an .

iter2 [Blist]  List.iter2 f [a1; ...; an] [b1; ...; bn] calls in turn
f a1 b1; ...; f an bn .

iteri [Blist] 
Same as
List.iter , but the function is applied to the index of
the element as first argument (counting from 0), and the element
itself as second argument.

L  
last_search_depth [Sigs.PROVER]  
left [Pair] 
Pair destructor.

left_union [Hashset.S]  
length [Blist] 
Return the length (number of elements) of the given t.

lift [Sigs.ABDRULE]  
list_conj [Fun]  
list_disj [Fun]  
list_get [Option]  
lru_cache [Lru.Make]  lru_cache f n memoises the nonrecursive function f , using an LRU cache
(implemented as a hashtable) of up to n entries.

lru_cache_rec [Lru.Make]  lru_cache f n memoises the recursive function f , using an LRU cache
(implemented as a hashtable) of up to n entries.

M  
map [Option]  
map [Pair] 
Apply a function to both members individually and put results in a new pair.

map [Blist]  List.map f [a1; ...; an] applies function f to a1, ..., an ,
and builds the t [f a1; ...; f an]
with the results returned by f .

map2 [Blist]  List.map2 f [a1; ...; an] [b1; ...; bn] is
[f a1 b1; ...; f an bn] .

map_left [Pair] 
Apply a function to the lefthand component only

map_right [Pair] 
Apply a function to the righthand component only

map_to [Utilsigs.OrderedContainer]  map_to add empty f set converts every element of set using f ,
and then folds over the new collection of elements using as starting
value empty and folding operation add .

map_to [Hashset.S]  
map_to [Blist]  
map_to_list [Utilsigs.OrderedContainer]  map_to_list f set applies f to every element and constructs a list
of results.

mapi [Blist] 
Same as
List.map , but the function is applied to the index of
the element as first argument (counting from 0), and the element
itself as second argument.

max_depth [Sl_abduce] 
Returns the maximum depth for the underlying proof search

melt_proof [Sigs.ABDUCER]  
melt_proof [Sigs.PROVER]  
mem [Hashset.S]  
mem [Blist]  mem a l is true if and only if a is equal
to an element of l .

mem_assoc [Blist] 
Same as
List.assoc , but simply return true if a binding exists,
and false if no bindings exist for the given key.

mem_assq [Blist] 
Same as
List.mem_assoc , but uses physical equality instead of
structural equality to compare keys.

memory_consuming [Sl_indrule]  memory_consuming r returns true the body of r is memory consuming
(see Sl_heap ).

memory_consuming [Sl_heap]  memory_consuming h returns true iff whenever there is an inductive
predicate in h there is also a pointsto.

memq [Blist] 
Same as
List.mem , but uses physical equality instead of structural
equality to compare t elements.

merge [Blist] 
Merge two ts:
Assuming that
l1 and l2 are sorted according to the
comparison function cmp , merge cmp l1 l2 will return a
sorted t containting all the elements of l1 and l2 .

mk [Sl_indrule]  
mk [Sl_heap_rho]  
mk [Sl_heap]  
mk [VarManager.I]  mk_var n exist returns a variable with name n ; if exist is true then
the returned variable will be existential, otherwise it will be free.

mk [VarManager]  mk seed anon_str classify creates a new variable manager module where:
seed specifies a cyclic permutation of the alphabet, which is used
internally to create new variable names;
anon_str specifies how to represent "anonymous" variables as a string;
classify varname returns a value of type varname_class classifying varname .

mk [Tagpairs]  mk tags computes the identity relation over the set tags .

mk [Option]  
mk [Pair] 
Pair constructor.

mk [Sigs.PROOF] 
Constructor.

mk_abdbackrule [Sigs.ABDRULE]  
mk_abdgenrule [Sigs.ABDRULE]  
mk_abdinfrule [Sigs.ABDRULE]  
mk_abs_node [Soundcheck] 
Constructor for nodes.

mk_af [Tl_form.Form]  
mk_ag [Tl_form.Form]  
mk_and [Tl_form_ltl.Form]  
mk_and [Tl_form.Form]  
mk_assert_check [Sl_unify.S] 
Takes a state check and wraps it in an assert

mk_atom [Tl_form_ltl.Form]  
mk_atom [Tl_form.Form]  
mk_axiom [Sigs.PROOFRULE] 
Axioms are modeled as functions that return
Some string when the
input sequent is an instance of an axiom described by string , else
None .

mk_axiom [Sigs.NODE]  mk_axiom seq descr creates an axiom node labelled by
sequent seq and description descr .

mk_backlink [Sigs.NODE]  mk_backlink seq descr target vtts creates a backlink node labelled by
sequent seq , description descr , target index target and set of
valid tag transitions (as pairs) vtts .

mk_backrule [Sigs.PROOFRULE] 
Backlink rules take: a boolean
eager , a selection function s , a matching function m
The selection function is applied on the current subgoal and proof, and
a list of goal indices is returned that represents possible backlink
targets. This allows flexibility e.g., in changing from ancestralonly
backlinks to general ones.
Next, m is applied to every pair consisting of the current subgoal
and a goal returned from the selection function.

mk_box [Tl_form.Form]  
mk_circle [Tl_form.Form]  
mk_deq [Sl_heap_rho]  
mk_deq [Sl_heap]  
mk_diamond [Tl_form.Form]  
mk_ef [Tl_form.Form]  
mk_eg [Tl_form.Form]  
mk_eq [Sl_heap_rho]  
mk_eq [Sl_heap]  
mk_ex_subst [VarManager.SubstSig]  mk_ex_subst avoid vs produces a substitution of pairwise distinct existentially
quantified variables (fresh for all the variables in avoid ) for the variables in vs .

mk_ex_subst [Tagpairs]  mk_ex_subst avoid ts produces a set of tag pairs representing a substitution of pairwise distinct
existentially quantified tags (fresh for all the tags in avoid ) for the tags in ts .

mk_f [Tl_form_ltl.Form]  
mk_final [Tl_form.Form]  
mk_free_subst [VarManager.SubstSig]  mk_free_subst avoid vs produces a substitution of pairwise distinct
free variables (fresh for all the variables in avoid ) for the variables in vs .

mk_free_subst [Tagpairs]  mk_free_subst avoid ts produces a set of tag pairs representing a substitution of pairwise distinct
free tags (fresh for all the tags in avoid ) for the tags in ts .

mk_g [Tl_form_ltl.Form]  
mk_ind [Sl_heap_rho]  
mk_ind [Sl_heap]  
mk_inf [Sigs.NODE]  mk_inf seq descr subgoals back creates an inference node labelled by
sequent seq , description descr , a list of triples consisting of
subgoal index, valid tag transitions and progressing tag transitions
subgoals .

mk_infrule [Sigs.PROOFRULE] 
Rules are functions that break down a sequent to a choice of applications
where each application is a list of premises, including tag information,
and a description.

mk_lazily [Option]  
mk_next [Tl_form_ltl.Form]  
mk_open [Sigs.NODE]  mk_open seq creates an open Proof.t node labelled by seq .

mk_or [Tl_form_ltl.Form]  
mk_or [Tl_form.Form]  
mk_pto [Sl_heap_rho]  
mk_pto [Sl_heap]  
mk_rho [Sl_heap_rho]  
mk_unifier [Unification.MakeUnifier]  
mk_unifier [Utilsigs.OrderedContainer]  mk_unifier total linear elt_unifier produces a unifier u for a set of elements
using the unifier elt_unifier for a single element.

mk_update_check [Ord_constraints]  
mk_verifier [Sl_unify.S] 
Takes a state check function and converts it into a continuation which
returns None if the check fails

modulo_entl [Sl_unify.Unidirectional]  
N  
neg [Fun]  
nil [Sl_term] 
The
nil constant.

norm [Sl_seq] 
Replace all terms with their UF representatives in the respective formulas.`

norm [Sl_form_rho] 
Replace all terms with their UF representatives in the respective heaps.

norm [Sl_form] 
Replace all terms with their UF representatives in the respective heaps.

norm [Sl_heap_rho] 
Replace all terms with their UF representative (the UF in the heap).

norm [Sl_heap] 
Replace all terms with their UF representative (the UF in the heap).

norm [Sl_tpreds] 
Replace all terms with their UF representative.

norm [Sl_tpred] 
Replace all terms with their UF representative.

norm [Sl_pred] 
Replace all terms with their UF representative.

norm [Sl_ptos] 
Replace all terms with their UF representative.

norm [Sl_pto] 
Replace all terms with their UF representative.

norm [Sl_deqs] 
Rename all variables involved by their representative in the UF structure
and reorder pair members if necessary.

nth [Blist] 
Return the
n th element of the given t.

num_backlinks [Sigs.PROOF]  
O  
of_list [Sl_rho]  
of_list [Sl_uf]  Sl_term.compare .

of_list [VarManager.SubstSig] 
Make a substitution from a list of bindings

of_list [Utilsigs.OrderedMap] 
Create a map out of a list of pairs of (keys, values).

of_list [Utilsigs.OrderedContainer] 
Convert a list of elements to a container.

of_list [Hashset.S]  
of_list [Blist] 
Construct a
t list out of a primitive list.

of_string [Tl_form_ltl.Form]  
of_string [Tl_form.Form]  
of_string [Sl_seq]  
of_string [Sl_form_rho]  
of_string [Sl_form]  
of_string [Sl_heap_rho]  
of_string [Sl_heap]  
of_string [Sl_tpred]  
of_string [Sl_pred]  
of_string [Sl_term] 
Parse a term from a string.

of_string [Ord_constraints]  
opt_map_to [Utilsigs.OrderedContainer]  opt_map_to add empty f set converts every element of set using f ,
and then folds over the elements of the new collection which are Some
using as starting value empty and folding operation add .

opt_map_to [Blist]  opt_map_to oadd oempty f xs is equivalent to map_to (Option.dest Fun.id oadd) oempty f x

order [Sl_tpair] 
Return a permutation of the input that obeys the ordering
Sl_term.compare .

outermost_tag [Tl_form_ltl.Form]  
outermost_tag [Tl_form.Form]  
P  
pairs [Blist] 
Return a list of pairs of consecutive elements.

parse [Tl_form_ltl.Form]  
parse [Tl_form.Form]  
parse [Sl_indrule]  
parse [Sl_seq]  
parse [Sl_form_rho]  
parse [Sl_form]  
parse [Sl_heap_rho]  
parse [Sl_heap]  
parse [Sl_tpred]  
parse [Sl_pred]  
parse [Sl_pto]  
parse [Sl_deqs]  
parse [Sl_rho]  
parse [Sl_uf]  
parse [Sl_term] 
Parse a term.

parse [Tags.Elt]  
parse [Ord_constraints]  
partition [VarManager.SubstSig]  partition theta will partition theta into (theta_1 , theta_2 )
such that theta_1 contains all and only the mappings in theta from
a free variable to either an anonymous variable or another free variable;
that is theta_1 is the part of theta which is a proper
(prooftheoretic) substitution.

partition [Blist]  partition p l returns a pair of ts (l1, l2) , where
l1 is the t of all the elements of l that
satisfy the predicate p , and l2 is the t of all the
elements of l that do not satisfy p .

partition_subst [Tagpairs] 
Partition the set of tag pairs into those pairs containing only "free" tags, and all the rest

pp [Tl_form_ltl.Form]  
pp [Tl_form.Form]  
pp [VarManager.SubstSig] 
Pretty printer.

pp [Option]  
pp [Utilsigs.OrderedMap]  pp pp_val fmt map pretty prints map using pp_val to prettyprint
the *values* of map .

pp [Utilsigs.BasicType] 
Pretty printer.

pp [Soundcheck] 
Pretty print abstract proof.

pp [Sigs.PROOF]  
pp [Sigs.NODE]  
pp [Sigs.DEFS]  
pp [Sigs.SEQUENT]  
pp [Blist]  pp sep e fmt l pretty prints the list l .

pred [Option]  pred p x returns Some x if p x else None .

pred_dest [Option]  
predsym [Sl_indrule]  
predsym [Sl_tpred]  
predsym [Sl_pred]  
print_proof_stats [Sigs.ABDUCER]  
print_proof_stats [Sigs.PROVER]  
prog_pairs [Ord_constraints]  prog_pairs cs returns all of the tag pairs (a , b ) such that a <b
is entailed by some constraint in cs

proj_pure [Sl_heap_rho]  
proj_pure [Sl_heap]  
proj_sp [Sl_heap_rho]  
proj_sp [Sl_heap]  
project [Sl_heap_rho] 
See CSLLICS paper for explanation.

project [Sl_heap] 
See CSLLICS paper for explanation.

projectl [Tagpairs]  projectl tps computes the set of tags appearing in the left of pairs in tps .

projectr [Tagpairs]  projectr tps computes the set of tags appearing in the right of pairs in tps .

R  
range [Blist]  range n l returns a list of increasing integers li such that hd li = n
and length li = length l .

realize [Sl_unify.S]  
record_type [Sl_pto]  
reflect [Tagpairs] 
Reverse the relation.

relabel [Sigs.SEQTACTICS]  
remove [Sl_uf] 
FIXME why is this here?

remove [Hashset.S]  
remove_assoc [Blist]  remove_assoc a l returns the t of
pairs l without the first pair with key a , if any.

remove_assq [Blist] 
Same as
List.remove_assoc , but uses physical equality instead
of structural equality to compare keys.

remove_dup_substs [Sl_unify.Unidirectional]  remove_dup_substs states will remove any states in states where the
universal parts (i.e.

remove_nth [Blist]  
remove_schema [Ord_constraints]  remove_schema cs used will remove a (nonempty) subset cs' of cs
containing tags { t_1, ..., t_n } where at least one t_i does not occur in
used such that cs' does not affect the support of cs in the sense that

repeat [Sigs.SEQTACTICS]  
repeat [Blist]  repeat e n constructs a list of length n where all elements are physically
equal to e .

replace_nth [Blist]  
rev [Blist] 
List reversal.

rev_append [Blist]  List.rev_append l1 l2 reverses l1 and concatenates it to l2 .

rev_filter [Blist]  
rev_map [Blist]  List.rev_map f l gives the same result as
List.rev ( List.map f l) , but is tailrecursive and
more efficient.

rev_map2 [Blist]  List.rev_map2 f l1 l2 gives the same result as
List.rev ( List.map2 f l1 l2) , but is tailrecursive and
more efficient.

right [Pair] 
Pair destructor.

S  
satisfiable [Ord_constraints.Elt]  
sequence [Sigs.PROOFRULE]  
set_defs [Sl_abduce] 
Specify the set of inductive definitions available for the proof search

set_depth [Sl_abduce] 
Set the maximum depth for the underlying proof search

singleton [VarManager.SubstSig] 
Constructor for a substitution mapping one variable to a term.

singleton [Blist] 
Constructs a list with exactly one element, the argument provided.

size [Sigs.PROOF]  
some [Option]  
sort [Blist] 
Sort a t in increasing order according to a comparison
function.

sort_uniq [Blist] 
Same as
List.sort , but also remove duplicates.

split [Blist] 
Transform a t of pairs into a pair of ts:
split [(a1,b1); ...; (an,bn)] is ([a1; ...; an], [b1; ...; bn]) .

stable_sort [Blist] 
Same as
List.sort , but the sorting algorithm is guaranteed to
be stable (i.e.

star [Sl_form_rho] 
Star two formulas by distributing
* through \/ .

star [Sl_form] 
Star two formulas by distributing
* through \/ .

star [Sl_heap_rho]  
star [Sl_heap]  
step [Tl_form_ltl.Form]  
strip [VarManager.SubstSig] 
Removes all identity bindings from the substitution map

strip [Tagpairs]  strip tps removes all elements that are pairs of equal tags.

strip_tags [Sl_tpreds] 
Remove tags.

submap [Utilsigs.OrderedMap] 
Decide if a map is included in another, using the provided value equality
predicate.

subsets [Utilsigs.OrderedContainer] 
Generate all subsets of a set.

subst [Sl_indrule]  
subst [Sl_seq]  
subst [Sl_form_rho]  
subst [Sl_form]  
subst [Sl_heap_rho]  
subst [Sl_heap]  
subst [Sl_tpreds]  
subst [Sl_tpred]  
subst [Sl_pred]  
subst [Sl_ptos]  
subst [Sl_pto]  
subst [Sl_deqs]  
subst [Sl_rho]  
subst [Sl_uf]  
subst [Sl_tpair]  
subst [Sl_term.FList] 
Applies a substitution to the list

subst_existentials [Sl_form_rho] 
Like
Sl_heap_rho.subst_existentials applied to all disjuncts.

subst_existentials [Sl_form] 
Like
Sl_heap.subst_existentials applied to all disjuncts.

subst_existentials [Sl_heap_rho] 
For all equalities x'=t, remove the equality and do the substitution
t/x'

subst_existentials [Sl_heap] 
For all equalities x'=t, remove the equality and do the substitution
t/x'

subst_subsumed [Sl_uf] 
Compute whether a substitution could be obtained by rewriting under
equalities in first argument.

subst_tag [Sl_tpred] 
Substitute the tag according to the function represented by the set of
tag pairs provided.

subst_tags [Tl_form_ltl.Form]  
subst_tags [Tl_form.Form]  
subst_tags [Sl_seq] 
Substitute tags of the LHS.

subst_tags [Sl_form_rho] 
Like
Sl_heap_rho.subst_tags applied to all disjuncts.

subst_tags [Sl_form] 
Like
Sl_heap.subst_tags applied to all disjuncts.

subst_tags [Sl_heap_rho] 
Substitute tags according to the function represented by the set of
tag pairs provided.

subst_tags [Sl_heap] 
Substitute tags according to the function represented by the set of
tag pairs provided.

subst_tags [Sl_tpreds] 
Substitute tags according to the function represented by the set of
tag pairs provided.

subst_tags [Ord_constraints.Elt]  
subst_tags [Ord_constraints]  
subsumed [Sl_seq]  subsumed (l,r) (l',r') is true iff both Sl_form.subsumed l' l and
Sl_form.subsumed r r' are true.

subsumed [Sl_form_rho]  subsumed a b : is it the case that for any disjunct a' of a there a
disjunct b' of b such a' is subsumed by b' ?
If the optional argument ~total=true is set to false then relax the
check on the spatial part so that it is included rather than equal to that
of b .

subsumed [Sl_form]  subsumed a b : is it the case that
i) the constraints cs of a are subsumed by the constraints cs' of b
in the sense that Ord_constraints.subsumes cs' cs returns true
ii) for any disjunct a' of a there is a disjunct b' of b such that
a' is subsumed by b' ?
If the optional argument ~total=true is set to false then relax the
check on the spatial part so that it is included rather than equal to that
of b .

subsumed [Sl_heap_rho]  subsumed h h' is true iff h can be rewritten using the equalities
in h' such that its spatial part becomes equal to that of h'
and the pure part becomes a subset of that of h' .

subsumed [Sl_heap]  subsumed h h' is true iff h can be rewritten using the equalities
in h' such that its spatial part becomes equal to that of h'
and the pure part becomes a subset of that of h' .

subsumed [Sl_tpreds] 
Test whether the two arguments are the same modulo the provided equalities.

subsumed [Sl_ptos]  subsumed eqs ptos ptos' is true iff ptos can be rewritten using the
equalities eqs such that it becomes equal to ptos' .

subsumed [Sl_deqs]  subsumed eqs d d' is true iff d can be rewritten using the equalities
in eqs such that it becomes a subset of d' .

subsumed [Sl_rho]  subsumed rho rho' is true iff uf'  uf using the normal equality rules.

subsumed [Sl_uf]  subsumed uf uf' is true iff uf'  uf using the normal equality rules.

subsumed_upto_constraints [Sl_form] 
As above but does not check subsumption of constraints

subsumed_upto_tags [Sl_seq] 
Like
subsumed but ignoring all tags.

subsumed_upto_tags [Sl_form_rho] 
As above but ignoring tags.

subsumed_upto_tags [Sl_form] 
As above but ignoring tags.

subsumed_upto_tags [Sl_heap_rho] 
Like
subsumed but ignoring tag assignment.

subsumed_upto_tags [Sl_heap] 
Like
subsumed but ignoring tag assignment.

subsumed_upto_tags [Sl_tpreds] 
Test whether the two arguments are the same modulo the provided equalities.

subsumes [Ord_constraints]  subsumes cs cs' checks whether every constraint in cs' also occurs in
cs , ignoring any constraints in cs' which are universally valid
(e.g.

swap [Fun]  
swap [Pair] 
Swap around the members of a pair.

syntactically_equal_nodes [Sigs.PROOFRULE]  
T  
tag [Sl_tpred]  
tag_check [Sl_unify.Unidirectional]  
tag_is_exist [Sl_tpred]  
tag_is_free [Sl_tpred]  
tag_pairs [Sl_seq] 
Tag pairs constituting the identity relation on the tags in the LHS.

tag_pairs [Sl_form_rho] 
The proviso on tags applies here too.

tag_pairs [Sl_form] 
The proviso on tags applies here too.

tag_pairs [Sl_heap_rho] 
Return a set of pairs representing the identity function over the tags
of the formula.

tag_pairs [Sl_heap] 
Return a set of pairs representing the identity function over the tags
of the formula.

tag_pairs [Ord_constraints] 
Return a set of pairs representing the identity function over the tags
in the constraint set, to be used as preserving tag pairs.

tags [Tl_form_ltl.Form]  
tags [Tl_form.Form]  
tags [Sl_seq] 
Tags occurring in this sequent on both the LHS and RHS

tags [Sl_form_rho] 
NB no attempt is made to ensure that tags are disjoint between disjuncts.

tags [Sl_form] 
NB no attempt is made to ensure that tags are disjoint between disjuncts.

tags [Sl_heap_rho] 
Return set of tags assigned to predicates in heap.

tags [Sl_heap] 
Return set of tags assigned to predicates in heap.

tags [Sl_tpreds]  
tags [Sl_tpred]  
tags [Ord_constraints.Elt]  
tags [Ord_constraints]  
tags [Sigs.SEQUENT] 
Returns set of tags in sequent.

take [Blist]  take n l returns a list of the first n elements of l .

terms [Sl_form_rho]  
terms [Sl_form]  
terms [Sl_heap_rho]  
terms [Sl_heap]  
terms [Sl_tpreds]  
terms [Sl_tpred]  
terms [Sl_pred]  
terms [Sl_ptos]  
terms [Sl_pto]  
terms [Sl_deqs]  
terms [Sl_rho]  
terms [Sl_uf]  
terms [Sl_tpair.FList] 
Unify all pairs of the 1st argument with a part of the 2nd.

terms [Sl_term.FList] 
Convenience function converting the list to a set.

tl [Blist] 
Return the given t without its first element.

to_abstract_node [Sigs.NODE] 
Convert Proof.t node to abstract node as in
Soundcheck .

to_int [VarManager.S.Var] 
Returns an integer representation

to_int [Tags.Elt]  
to_ints [VarManager.S] 
Convenience method to return a set of integer representatives of a set of variables.

to_ints [Tags]  
to_list [Utilsigs.OrderedMap] 
Create a list of pairs (keys, values) out of a map.

to_list [Utilsigs.OrderedContainer] 
Convert to a list of unique, sorted elements.

to_list [Sigs.PROOF]  
to_list [Hashset.S]  
to_list [Blist] 
Construct a primitive list out of a
t list.

to_melt [Tl_form_ltl.Form]  
to_melt [Tl_form.Form]  
to_melt [Sl_seq]  
to_melt [Sl_form_rho]  
to_melt [Sl_form]  
to_melt [Sl_heap_rho]  
to_melt [Sl_heap]  
to_melt [Sl_tpreds]  
to_melt [Sl_tpred]  
to_melt [Sl_ptos]  
to_melt [Sl_pto]  
to_melt [Sl_deqs]  
to_melt [Sl_rho]  
to_melt [Sl_uf]  
to_melt [Sl_term] 
Convert term to LaTeX.

to_melt [Tags.Elt]  
to_melt [Ord_constraints]  
to_melt [Sigs.PROOF]  
to_melt [Sigs.NODE] 
Convert to Latex.

to_melt [Sigs.DEFS]  
to_melt [Sigs.SEQUENT]  
to_melt_sep [Sl_tpair]  
to_slformula [Tl_form_ltl.Form]  
to_slformula [Tl_form.Form]  
to_string [Tl_form_ltl.Form]  
to_string [Tl_form.Form]  
to_string [Sl_tpred]  
to_string [VarManager.SubstSig] 
Convert a substitution to a string

to_string [Utilsigs.OrderedMap]  to_string val_to_string map converts to a string, using val_to_string
to convert *values* to strings.

to_string [Utilsigs.BasicType] 
Convert to string.

to_string [Ord_constraints]  
to_string [Sigs.PROOF]  
to_string [Sigs.DEFS]  
to_string [Sigs.SEQUENT]  
to_string [Hashset.HashedType]  
to_string [Hashset.S]  
to_string [Blist]  to_string sep e l converts the list l to a string.

to_string_list [Sl_tpreds]  
to_string_list [Sl_ptos]  
to_string_list [Sl_deqs]  
to_string_list [Sl_rho]  
to_string_list [Sl_uf]  
to_string_list [Ord_constraints]  
to_string_sep [Sl_tpair]  
to_string_sep [Sl_term.FList]  to_string_sep sep ts converts ts to a string with each element separated by sep .

transform [Unification]  
trivial_continuation [Unification]  
trm_check [Sl_unify.Unidirectional] 
When used as state update check in a call to
Sl_heap.unify for unifying
heaps h and h' , ensures that the generated substitution, when applied
to h , produces a formula which is subsumed by h'

U  
uncurry [Fun]  
unfold [Sl_indrule]  unfold (vs, ts) p r returns the body of the inductive rule r with:
the formal parameters replaced by the arguments of p ;
the remaining variables freshened, avoiding those in vs ; and
the predicates assigned fresh existential tags avoiding those in ts ,
unless the optional argument gen_tags=true is set to false.

unfold_af [Tl_form.Form]  
unfold_ag [Tl_form.Form]  
unfold_and [Tl_form_ltl.Form]  
unfold_and [Tl_form.Form]  
unfold_ef [Tl_form.Form]  
unfold_eg [Tl_form.Form]  
unfold_f [Tl_form_ltl.Form]  
unfold_g [Tl_form_ltl.Form]  
unfold_or [Tl_form_ltl.Form]  
unfold_or [Tl_form.Form]  
unify [Sl_tpreds] 
Compute substitution that makes the two multisets equal up to tags.

unify [Sl_tpred] 
Unify two tagged predicates.

unify [Sl_pred] 
Compute substitution that unifies two predicates.

unify [Sl_ptos] 
Compute substitution that would make the two multisets equal.

unify [Sl_pto] 
Compute substitution that unifies two pointstos.

unify [Sl_tpair] 
Unify two pairs of terms, ignoring the pairs' internal ordering of members.

unify [Sl_term.FList] 
Unifies two lists of terms by producing a substitution to act on the first list

unify [Sl_term] 
Unifies two terms by producing a substitution to act on the first term

unify [Tags.Elt] 
Unifies two tags by finding a suitable substitution (represented as a set of tag pairs)
for the first tag which makes it equal to the second.

unify [Ord_constraints.Elt]  
unify [Ord_constraints]  unify check cs cs' cont init_state calculates a (minimal) extension theta
of init_state such that subsumes cs' (subst_tags theta cs) returns
true , then passes it to cont and returns the resulting (optional) value.

unify_partial [Sl_heap_rho] 
Unify two heaps such that the first becomes a subformula of the second.

unify_partial [Sl_heap] 
Unify two heaps such that the first becomes a subformula of the second.

unify_partial [Sl_deqs]  unify_partial d d' Unification.trivial_continuation Sl_unify.empty_state
computes a substitution theta such that d[theta] is a subset of d' .

unify_partial [Sl_uf]  unify_partial Option.some (Sl_term.empty_subst, ()) u u' computes a
substitution theta such that u'  u[theta] .

unify_tag [Sl_unify.S]  
unify_tag_constraints [Sl_unify.Bidirectional]  Ord_constraints.biunify lifted to the SL unifier type

unify_tag_constraints [Sl_unify.Unidirectional]  Ord_constraints.unify lifted to the SL unifier type

unify_trm [Sl_unify.S]  
unify_trm_list [Sl_unify.S]  
union [Sl_rho]  
union [Sl_uf]  
union [Utilsigs.OrderedMap] 
Union two maps.

union_of_list [Utilsigs.OrderedContainer] 
Union a list of sets.

uniq [Blist]  uniq eq l returns a list containing no duplicates w.r.t.

univ [Sl_heap_rho] 
Replace all existential variables with fresh universal variables.

univ [Sl_heap] 
Replace all existential variables with fresh universal variables.

unzip3 [Blist]  
updchk_inj_left [Sl_unify.Bidirectional]  
updchk_inj_right [Sl_unify.Bidirectional]  
upper_bounds [Ord_constraints]  upper_bounds ?strict t cs returns the set of tags b such that cs
contains a constraint of the form t <= b .

V  
valid [Ord_constraints.Elt]  
vars [Tl_form_ltl.Form]  
vars [Tl_form.Form]  
vars [Sl_indrule]  
vars [Sl_seq]  
vars [Sl_form_rho]  
vars [Sl_form]  
vars [Sl_heap_rho]  
vars [Sl_heap]  
vars [Sl_tpreds]  
vars [Sl_tpred]  
vars [Sl_pred]  
vars [Sl_ptos]  
vars [Sl_pto]  
vars [Sl_deqs]  
vars [Sl_rho]  
vars [Sl_uf]  
vars [Sl_term.FList] 
Returns the set of all elements of the list that are not nil

verify_schemas [Ord_constraints]  verify_schemas ts cs will return true when cs consists entirely of
tautological schemas.

W  
weave [Utilsigs.OrderedContainer] 
Weave combinator  used in the SL Model Checker.

weave [Blist] 
Weave combinator  used in the SL Model Checker.

with_constraints [Sl_form]  with_constraints f cs returns the formula that results by replacing f 's
tag constraints with cs

with_deqs [Sl_heap_rho]  
with_deqs [Sl_heap]  
with_eqs [Sl_heap_rho]  
with_eqs [Sl_heap]  
with_heaps [Sl_form]  with_heaps hs cs returns the formula that results by replacing f 's
disjunction of symbolic heaps with hs

with_inds [Sl_heap_rho]  
with_inds [Sl_heap]  
with_ptos [Sl_heap_rho]  
with_ptos [Sl_heap]  
with_rho [Sl_heap_rho]  
Z  
zip3 [Blist] 