Index of values

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 all bindings in provided list to map.

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

add_subprf p idx p' replaces the node idx in p' with a copy of p.

Ready-made selection functions doing the obvious.

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

all_subheaps h returns a list of all the subheaps of h.

all_subheaps h returns a list of all the subheaps of h.

An "unidentified" variable

Catenate two ts.

Apply a substitution to a variable

Apply a function taking two arguments to the members of a pair.

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

assoc a l returns the value associated with key a in the t of pairs l.

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

Try a rule and if it fails act as identity.

avoid vars subvars returns a substitution that takes all variables in subvars to variables fresh in vars U subvars, respecting existential quantification / free variables.

A state update check which prevents replacements of variables within the given set of terms.

backtrack u takes a cps-style 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.

Return mapping as a list of pairs of terms and values Additional guarantees: Pairs are ordered lexicographically, based on Sl_term.compare.

Return mapping as a list of pairs, where pair members are ordered by

Unifies two lists of terms by producing substitutions to act on each list respectively

Unifies two terms by producing substitutions to act on each term respectively

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

Alias for conj

Return a list containing all elements apart from the last one.

Return a list of all pairs out of elements of a list, but without including symmetric pairs.

Check soundness.

Validate, minimise, check soundness of proof/graph and memoise.

Apply a list of rules on current subgoal and return all applications.

choose [[1;2;3]; [4;5]] returns [[1;4];[1;5];[2;4];[2;5];[3;4];[3;5]].

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

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

close cs generates the set of all constraints entailed by cs

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

combs n l returns all combinations of n elements from l.

Standard comparator, return <0 if first less than second, 0 if equal, >0 if greater.

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 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 exist ts h returns the symbolic heap obtained from h by assigning all untagged predicates a fresh existential tag avoiding those in ts.

compose l r computes the relation representing the composition of l with r.

Apply the list of rules in the second argument in a pairwise fashion to the premises generated by applying the first rule

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'.

Concatenate a t of ts.

Compute the conjunction of a pair of booleans.

Equivalent to ::.

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

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

Destruct a non-empty list.

Remove first element satisfying the given predicate.

Delete first element satisfying a given predicate.

If both LHS and RHS are symbolic heaps then return them else raise Sl_form.Not_symheap.

Return the single disjunct, if there is exactly one, else raise Not_symheap.

Return the single disjunct, if there is exactly one, else raise Not_symheap.

dest n returns (sequent, description).

dest_backlink n destroys a back-link node n, otherwise raises Invalid_arg.

dest_inf n destroys an inference node n, otherwise raises Invalid_arg.

dest_singleton tps returns Some(tp) if tp is the only element of tps, and None otherwise.

diff rho rho' returns the structure given by removing all variables in rho' from rho

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

Does a symbolic heap entail the disequality of two terms?

Does a symbolic heap entail the disequality of two terms?

Or two formulas (list-append).

Or two formulas (list-append).

Compute the disjunction of a pair of booleans.

Decide if there are no common elements.

drop n l returns the suffix of l after skipping n elements.

Alias for disj

The formula emp.

The formula emp.

The empty substitution, which has no effect when applied.

The empty list constant.

The unifier state consisting of the empty substitution and the empty set of tag pairs

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

Map a set of elements to another set of elements of the same type.

Checks whether two symbolic heaps are equal.

Checks whether two symbolic heaps are equal.

Standard equality predicate.

"Syntactic" equality.

The equality predicate used to compare elements.

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

Like equal but ignoring LHS tags as well as RHS ones.

Whilst equal demands syntactic equality including tags, this version ignores tag assignment.

Whilst equal demands syntactic equality including tags, this version ignores tag assignment.

Like equal but ignoring tag assignment.

Like equal but ignoring tag assignment.

Test whether the two arguments are the equal ignoring tags.

Compare for equality two tagged predicates while ignoring tags.

As equal but ignoring tags.

Does a symbolic heap entail the equality of two terms?

Does a symbolic heap entail the equality of two terms?

Does a stack struct holds a term with a val?

Does a UF struct make two terms equal?

exists p [a1; ...; an] checks if at least one element of the t satisfies the predicate p.

Same as List.exists, but for a two-argument predicate.

extract_subproof idx prf returns prf rearranged such that idx is the root node.

The rule that always fails.

Same as List.sort or List.stable_sort, whichever is faster on typical input.

filter p l returns all the elements of the t l that satisfy the predicate p.

Remove nil from a set of terms.

find p set returns the first element of set that satisfies the predicate p.

find p l returns the first element of the t l that satisfies the predicate p.

find_all is another name for List.filter.

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

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

Find pto whose address is provably equal to given term.

Find pto whose address is provably equal to given term.

Optimisation for finding and converting at the same time.

Optimisation for finding and converting at the same time.

Optimisation for finding and converting at the same time.

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

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

Apply a sequence of rules iteratively through compose.

fixpoint val_equal f map computes the fixpoint of f using val_equal to compare *values*.

Produce a set of all the tags in the given set of tag pairs.

Same as concat.

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 a function over the members of a pair.

List.fold_left f a [b1; ...; bn] is f (... (f (f a b1) b2) ...) bn.

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

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

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

for_all p [a1; ...; an] checks if all elements of the t satisfy the predicate p.

Same as List.for_all, but for a two-argument predicate.

fresh_evar s returns an existentially quantified variable that is fresh in s.

fresh_evar s returns an existential variable that is fresh for the set of variables s.

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

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

fresh_fvar s returns a free variable that is fresh in s.

fresh_uvar s returns a free variable that is fresh for the set of variables s.

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

fresh_uvars s n returns n distinct free variables that are all fresh for the set of variables s.

Replace all variables in rule such that they are disjoint with the set provided.

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

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

Rename tags in second argument so that they are disjoint to those in the first.

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 sequent labelling the node.

Get the successor node indices of this node.

Get the tracepairs between two sequents

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

Hash the map using the provided function for hashing *values*.

Standard hash function.

A hashing function on elements.

Return the first element of the given t.

Get multiset of predicate identifiers.

Get multiset of predicate identifiers.

Return multiset of identifiers present.

Do all disjuncts entail false in the sense of Sl_heap_rho.inconsistent?

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

Trivially false if x=y * x!=y is provable for any x,y.

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

indexes l returns the list of integer positions of elements in l.

Insert given element between elements of given list.

is_unnamed v returns true if and only if v is anonymous

Are all nodes not open?

is_empty h tests whether h is equal to the empty heap.

is_empty h tests whether h is equal to the empty heap.

Is the argument the empty list?

Is the argument an existentially quantified variable?

is_exist_var v returns true if and only if v is an existential variable.

Is the argument a free variable?

is_exist_var v returns true if and only if v is a free variable.

Is the argument nil? Equivalent to equal nil x.

Returns true iff the formula has a single disjunct only

Returns true iff the formula has a single disjunct only

is_nil x is equivalent to not (equal nil x).

List.iter f [a1; ...; an] applies function f in turn to a1; ...; an.

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

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.

Pair destructor.

Return the length (number of elements) of the given t.

lru_cache f n memoises the non-recursive function f, using an LRU cache (implemented as a hashtable) of up to n entries.

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

Apply a function to both members individually and put results in a new pair.

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.

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

Apply a function to the left-hand component only

Apply a function to the right-hand component only

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_list f set applies f to every element and constructs a list of results.

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.

Returns the maximum depth for the underlying proof search

mem a l is true if and only if a is equal to an element of l.

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

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

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

memory_consuming h returns true iff whenever there is an inductive predicate in h there is also a points-to.

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

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_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 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 tags computes the identity relation over the set tags.

Pair constructor.

Constructor.

Constructor for nodes.

Takes a state check and wraps it in an assert

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 seq descr creates an axiom node labelled by sequent seq and description descr.

mk_backlink seq descr target vtts creates a back-link node labelled by sequent seq, description descr, target index target and set of valid tag transitions (as pairs) vtts.

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 back-link targets. This allows flexibility e.g., in changing from ancestral-only back-links to general ones. Next, m is applied to every pair consisting of the current subgoal and a goal returned from the selection function.

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 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_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 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_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.

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_open seq creates an open Proof.t node labelled by seq.

mk_unifier total linear elt_unifier produces a unifier u for a set of elements using the unifier elt_unifier for a single element.

Takes a state check function and converts it into a continuation which returns None if the check fails

The nil constant.

Replace all terms with their UF representatives in the respective formulas.`

Replace all terms with their UF representatives in the respective heaps.

Replace all terms with their UF representatives in the respective heaps.

Replace all terms with their UF representative (the UF in the heap).

Replace all terms with their UF representative (the UF in the heap).

Replace all terms with their UF representative.

Replace all terms with their UF representative.

Replace all terms with their UF representative.

Replace all terms with their UF representative.

Replace all terms with their UF representative.

Rename all variables involved by their representative in the UF structure and re-order pair members if necessary.

Return the n-th element of the given t.

Sl_term.compare.

Make a substitution from a list of bindings

Create a map out of a list of pairs of (keys, values).

Convert a list of elements to a container.

Construct a t list out of a primitive list.

Parse a term from a string.

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 oadd oempty f xs is equivalent to map_to (Option.dest Fun.id oadd) oempty f x

Return a permutation of the input that obeys the ordering Sl_term.compare.

Return a list of pairs of consecutive elements.

Parse a term.

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 (proof-theoretic) substitution.

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 the set of tag pairs into those pairs containing only "free" tags, and all the rest

Pretty printer.

pp pp_val fmt map pretty prints map using pp_val to pretty-print the *values* of map.

Pretty printer.

Pretty print abstract proof.

pp sep e fmt l pretty prints the list l.

pred p x returns Some x if p x else None.

prog_pairs cs returns all of the tag pairs (a, b) such that a <b is entailed by some constraint in cs

See CSL-LICS paper for explanation.

See CSL-LICS paper for explanation.

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

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

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

Reverse the relation.

FIXME why is this here?

remove_assoc a l returns the t of pairs l without the first pair with key a, if any.

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

remove_dup_substs states will remove any states in states where the universal parts (i.e.

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 e n constructs a list of length n where all elements are physically equal to e.

List reversal.

List.rev_append l1 l2 reverses l1 and concatenates it to l2.

List.rev_map f l gives the same result as List.rev (List.map f l), but is tail-recursive and more efficient.

List.rev_map2 f l1 l2 gives the same result as List.rev (List.map2 f l1 l2), but is tail-recursive and more efficient.

Pair destructor.

Specify the set of inductive definitions available for the proof search

Set the maximum depth for the underlying proof search

Constructor for a substitution mapping one variable to a term.

Constructs a list with exactly one element, the argument provided.

Sort a t in increasing order according to a comparison function.

Same as List.sort, but also remove duplicates.

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

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

Star two formulas by distributing * through \/.

Star two formulas by distributing * through \/.

Removes all identity bindings from the substitution map

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

Remove tags.

Decide if a map is included in another, using the provided value equality predicate.

Generate all subsets of a set.

Applies a substitution to the list

Like Sl_heap_rho.subst_existentials applied to all disjuncts.

Like Sl_heap.subst_existentials applied to all disjuncts.

For all equalities x'=t, remove the equality and do the substitution t/x'

For all equalities x'=t, remove the equality and do the substitution t/x'

Compute whether a substitution could be obtained by rewriting under equalities in first argument.

Substitute the tag according to the function represented by the set of tag pairs provided.

Substitute tags of the LHS.

Like Sl_heap_rho.subst_tags applied to all disjuncts.

Like Sl_heap.subst_tags applied to all disjuncts.

Substitute tags according to the function represented by the set of tag pairs provided.

Substitute tags according to the function represented by the set of tag pairs provided.

Substitute tags according to the function represented by the set of tag pairs provided.

subsumed (l,r) (l',r') is true iff both Sl_form.subsumed l' l and Sl_form.subsumed r r' are true.

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 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 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 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'.

Test whether the two arguments are the same modulo the provided equalities.

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

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 rho rho' is true iff uf' |- uf using the normal equality rules.

subsumed uf uf' is true iff uf' |- uf using the normal equality rules.

As above but does not check subsumption of constraints

Like subsumed but ignoring all tags.

As above but ignoring tags.

As above but ignoring tags.

Like subsumed but ignoring tag assignment.

Like subsumed but ignoring tag assignment.

Test whether the two arguments are the same modulo the provided equalities.

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 around the members of a pair.

Tag pairs constituting the identity relation on the tags in the LHS.

The proviso on tags applies here too.

The proviso on tags applies here too.

Return a set of pairs representing the identity function over the tags of the formula.

Return a set of pairs representing the identity function over the tags of the formula.

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

Tags occurring in this sequent on both the LHS and RHS

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

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

Return set of tags assigned to predicates in heap.

Return set of tags assigned to predicates in heap.

Returns set of tags in sequent.

take n l returns a list of the first n elements of l.

Unify all pairs of the 1st argument with a part of the 2nd.

Convenience function converting the list to a set.

Return the given t without its first element.

Convert Proof.t node to abstract node as in Soundcheck.

Returns an integer representation

Convenience method to return a set of integer representatives of a set of variables.

Create a list of pairs (keys, values) out of a map.

Convert to a list of unique, sorted elements.

Construct a primitive list out of a t list.

Convert term to LaTeX.

Convert to Latex.

Convert a substitution to a string

to_string val_to_string map converts to a string, using val_to_string to convert *values* to strings.

Convert to string.

to_string sep e l converts the list l to a string.

to_string_sep sep ts converts ts to a string with each element separated by sep.

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'

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.

Compute substitution that makes the two multisets equal up to tags.

Unify two tagged predicates.

Compute substitution that unifies two predicates.

Compute substitution that would make the two multisets equal.

Compute substitution that unifies two points-tos.

Unify two pairs of terms, ignoring the pairs' internal ordering of members.

Unifies two lists of terms by producing a substitution to act on the first list

Unifies two terms by producing a substitution to act on the first term

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 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 two heaps such that the first becomes a subformula of the second.

Unify two heaps such that the first becomes a subformula of the second.

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 Option.some (Sl_term.empty_subst, ()) u u' computes a substitution theta such that u' |- u[theta].

Ord_constraints.biunify lifted to the SL unifier type

Ord_constraints.unify lifted to the SL unifier type

Union two maps.

Union a list of sets.

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

Replace all existential variables with fresh universal variables.

Replace all existential variables with fresh universal variables.

upper_bounds ?strict t cs returns the set of tags b such that cs contains a constraint of the form t <= b.

Returns the set of all elements of the list that are not nil

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

Weave combinator - used in the SL Model Checker.

Weave combinator - used in the SL Model Checker.

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

with_heaps hs cs returns the formula that results by replacing f's disjunction of symbolic heaps with hs