[wiki:IR]

The CIVL core libraries include:

* `civlc`: the basic library of CIVL, usually included in a CIVL-C program, defining types and functions that are frequently used;
* `pointer`: providing utility functions dealing with pointers;
* `concurrency`: providing concurrency utilities such as barrier and collective record;
* `bundle`: defining bundle types and their operations;
* `comm`: defining communicators and their operations;
* `domain`: providing operations on domains;
* `seq`: providing operations on sequences which is realized using arrays.

=== `civlc` : basic functions ===
Types:
* `$operation`: an enumeration type of operations

Functions:
* `fun[lib="civlc"] $elaborate(x: Integer)`
 * elaborate an integer expression
* `fun[lib="civlc"] $next_time_count(): Integer`
 * gets a unique non-negative integer for time count
* `fun[lib="civlc", pure] $pathCondition()`
 * prints path condition of the current state
* `fun[lib="civlc"] $choose_int(n: Integer): Integer;`
 * non-deterministic choice of integer
 * this function takes as input a positive integer `n` and nondeterministicaly returns an integer in the range `[0, n − 1]`.
* `fun[lib="scope"] $scope_parent(s: Scope): Scope`
 * gets the parent of a scope `s`
 * If `s` is the root dynamic scope, it returns `scope_null`.

=== Pointer utilities `pointer.cvh` ===
The header `pointer.cvh` declares functions taking pointers as the arguments for different purposes, including:

* `fun[lib="pointer"] $set_default(obj: Pointer)`
 * sets the leaf nodes of a variable to be the default value of zero
* `fun[lib="pointer"] $apply(obj1: Pointer, op: Operation, obj2: Pointer, result: Pointer)`
 * applies a binary operator `op` to two objects
* `fun[lib="pointer"] $equals(x: Pointer, y: Pointer): Bool`
 * equality checking
 * this function returns true iff the objects pointed to by the pointers `x` and `y` have the same type and value.
* `fun[lib="pointer"] $assert_equals(x: Pointer, y: Pointer, ...)`
 * asserts that two objects are equal to each other
 * takes additional arguments for error message if the assertion is violated
* `fun[lib="pointer"] $contains(ptr1: Pointer, ptr2: Pointer): Bool`
 * membership testing
 * returns true iff the object pointed to by `ptr1` contains the object pointed to by `ptr2`. For example, `$contains(&a, &a[1].x)` would return true.
* `fun[lib="pointer"] $translate_ptr(ptr: Pointer, obj: Pointer): Pointer`
 * pointer translation
 * returns a pointer which is the result of translating the pointer `ptr` (a pointer into one object) to a pointer into a different object `obj` with similar structure.
* `fun[lib="pointer"] $copy(ptr: Pointer, value: pointer)`
 * copies the value pointed to by `value` to the memory location specified by `ptr`.
* `fun[lib="pointer"] $leaf_node_ptrs(array: Pointer, obj: Pointer)`
 * copies the references to the leaf nodes of `obj` to the given `array`
 * Suppose the type of `obj` is `Pointer[T']`, all leaf nodes of `T'` should have the same type `T`, and `array` should have type `Pointer[Array[T]]`. 
 * For example, `T'` could be `Tuple[<Integer, Array[Integer], Integer>]`.
* `fun[lib="pointer"] $set_leaf_nodes(obj: Pointer, value: Integer)`
 * sets leaf nodes with the given value
* `fun[lib="pointer"] $is_identity_ref(obj: Pointer)`
 * checks if the given pointer is pointing to a variable
* `fun[lib="pointer"] $leaf_nodes_equal_to(obj: Pointer, value: Integer)`
 * checks if the leaf nodes of the given object are equal to the given integer value
* `fun[lib="pointer"] $has_leaf_node_equal_to(obj: Pointer, value: Integer)`
 * checks if the given object has a leaf node whose value is equal to the given integer value
* `fun[lib="pointer"] $is_derefable_pointer(ptr: Pointer)`
 * checks if the given pointer could be safely dereferenced
* `fun[lib="pointer"] $pointer_add(ptr: Pointer,  offset: Integer, type_size: Integer)`
 * pointer addition
  
=== `bundle` utility ===
* Types
 * `Bundle`: a union type of all system types and user-defined types of a given program
* `fun[lib="bundle", pure] $bundle_size(b: Bundle): Integer`
 * returns the size of the given bundle
* `fun[lib="bundle"] $bundle_pack(ptr: Pointer, size: Integer): Bundle`
 * packs data into a bundle
* `fun[lib="bundle"] $bundle_unpack(bundle: Bundle, ptr: Pointer)`
 * unpack a bundle
* `fun[lib="bundle"] $bundle_unpack_apply(data: Bundle, buf: Pointer, size: Integer, op: Operation)`
 * unpack a bundle and apply some operation to the data

=== concurrency utility `concurrency` ===

==== barrier operations ====
* `fun[lib="concurrency"] $gbarrier_create(scope: Scope, size: Integer): GBarrier`
 * global barrier creation
* `fun[lib="concurreny"] $gbarrier_destroy(barrier: Gbarrier)`
 * global barrier destroy
* `fun[lib="concurrency"] $barrier_create(scope: Scope, gbarrier: Gbarrier, place: Integer): Barrier`
 * local barrier creation
* `fun[lib="concurrency"] $barrier_destroy(barrier: Barrier)`
 * local barrier destroy
*  `fun $barrier_call(barrier: Barrier)`
 * barrier call
  
==== collective records ====
* Types 
 * `Collect_record`
 * `GCollect_checker`
 * `Collect_checker`
* `fun[lib="concurrency"] $gcollect_checker_create(scope: Scope): Gcollect_checker`
 * global collective checker creation
* `fun[lib="concurrency"] $gcollect_checker_destroy(gchecker: Gcollect_checker)`
 * global collective checker destroy
* `fun[lib="concurrency"] $collect_checker_create(scope: Scope, gchecker: Gcollect_checker)`
 * collective checker creation
* `fun[lib="concurrency"] $collect_checker_destroy(checker: Collect_checker)`
 * collective checker destroy
* `fun[lib="concurrency"] $collect_check(checker: Collect_checker, place: Integer, nprocs: Integer, entries: Bundle)`
 * collective records checking

=== communication `comm` ===
* Types
 * `Message`
 * `Queue`
 * `GComm`
 * `Comm`
* message operations
 * `fun[lib="comm"] $message_pack(src: Integer, dst: Integer, tag: Integer, dt: Pointer, sz: Integer): Message`
   * pack a message
 * `fun[lib="comm"] $message_unpack(msg: Message, buf: Pointer, sz: Integer)`
   * unpack a message
 * `fun[lib="comm", pure] $message_source(msg: Message): Integer`
   * source of a message
 * `fun[lib="comm", pure] $message_tag(msg: Message): Integer`
   * tag of a message
 *  `fun[lib="comm", pure] $message_dest(msg: Message): Integer`
   * destination of a message
 * `fun[lib="comm", pure] $message_size(msg: Message): Integer`
   * size of a message
* global communicator operations
 * `fun[lib="comm"] $gcomm_create(scope: Scope, size: Integer): GComm`
   * creation
 * `fun[lib="comm"] $gcomm_destroy(gcomm: GComm)`
   * destroy
 *  `fun[lib="comm"] $gcomm_dup(old: Comm, new: Comm)`
   * duplication
* local communicator operations
 * `fun[lib="comm"] $comm_create(scope: Scope, gcomm: GComm, place: Integer): Comm`
   * creation
 * `fun[lib="comm"] $comm_destroy(comm: Comm)`
   * destroy
 * `fun[lib="comm", pure] $comm_size(comm: Comm): Integer`
   * returns the size of a communicator
 * `fun[lib="comm", pure] $comm_place(comm: Comm): Integer`
   * returns the place of the local communicator in the corresponding global communicator 
 * `fun[lib="comm"] $comm_enqueue(comm: Comm, msg: Message)`
   * enqueue
 * `fun[lib="comm", pure] $comm_probe(comm: Comm, src: Integer, tag: Integer): Bool`
   * probe
 * `fun[lib="comm"] $comm_seek(comm: Comm, src: Integer, tag: Integer): Message`
   * seek
 * `fun[lib="comm"] $comm_dequeue(comm: Comm, src: Integer, tag: Integer): Message`
   * dequeue

=== domain utility `domain` ===

* Types
 * `Domain_strategy`
 * `Domain_decomposition`
* `fun[lib="domain"] $domain_partition(dom: Domain, s: Domain_strategy, n: Integer): Domain_decomposition`
 * domain decomposition
* `funl[lib="domain"] $is_rectangular_domain(dom: Domain): Bool`
 * checks if domain is rectangular
* `fun[lib="domain", pure] $dimension_of(dom: Domain): Integer`
 * returns the dimension of a domain 
* `fun[lib="domain"] $domain_size(dom: Domain): Integer`
 * returns the size of a domain (i.e., total number of tuples)

=== sequence operations `seq` ===
* `fun[lib="seq"] $seq_init(seq: Pointer, count: Integer, value: Pointer)`
 * sequence initialization
 * given a pointer to an object of `Array[T]`, sets that object to be the array of length count in which every element has the same value, specified by the given pointer value.Parameters:
    1. array: pointer-to-incomplete-array-of-T
    1. count: any integer type, must be nonnegative
    1.value: pointer-to-T
* `fun[lib="seq", pure] $seq_length(seq: Pointer): Integer`
 * returns the length of a sequence
* `fun[lib="seq"] $seq_insert(seq: Pointer, index: Integer, values: Pointer, count: Integer)`
 * insertion
* `fun[lib="seq"] $seq_remove(seq: Pointer, index: Integer, values: Pointer, count: Integer)`
 * removal
* `fun[lib="seq"] $seq_append(seq: Pointer, values: Pointer, count: Integer)`
 * appending