A  
abstraction [Term]  abstraction v tm is \v. tm .

add [Dl_number.T] 
Numberic addition.

add [Index.Set]  add s e adds element e to the set s in (amortized)
constant time.

add [Index.Map]  add m k x modifies m by mapping the index of k to x .

add [Bunch] 
Add an element to a bunch.

add [Bihashtbl.S]  add b k e adds an entry mapping k to e to b .

add_balanced [Bunch] 
Add an element to a bunch.

add_clause [Dpll_core] 
Adds the clause (disjunction of literals) to the solver.

add_interface_literal [Cc_core]  add_interface_literal s (x, y) records an interest in the
literals x = y and x != y .

add_interface_variable [Dpll_core]  add_interface_variables s v treats the variable v and its
negation as interface literals.

add_literal [Dl_core.T] 
Add an interface literal to the solver.

application [Term] 
The application of the given terms.

application [Smtlib_syntax] 
Application of a named function to a list of arguments.

application_argument [Term] 
The argument in an application.

application_function [Term] 
The function in an application.

arity [Symbol]  arity s is the arity declared for s .

arity [Constant] 
Arity of a constant.

assumptions [Smtlib_attribute] 
A list of all the assumptions in a collection of attributes.

B  
backjump [Dpll_core] 
Resolve a conflict by backjumping to undo conflicting
assignments from the current partial model.

backjump [Cc_core] 
Backjumps to the given level.

backjump_possible [Dpll_core] 
Might a backjump be used to resolve a conflict?

backtrack [Dl_core.T] 
Backtrack to the given decision level.

beta_normal_form [Term] 
The term obtained by reducing all betaredexes in a term.

binary_application [Term]  binary_application f x y is equivalent to application
(application f x) y .

bool_of_ternary [Ternary]  bool_of_ternary t is the boolean corresponding to a known ternary t .

C  
classify [Option] 
Classify a value by placing it in an option.

clear [Vec]  clear v removes all elements from v .

clear [Priority_queue] 
Removes all elements from the queue.

clear [Index.Set] 
Makes the set empty in (amortized) constant time.

clear [Bihashtbl.S] 
Remove all entries from a hash table.

compact_print_term [Term] 
Compactly print a term using
std_formatter .

compare [Variable] 
An arbitrary ordering on variables.

compare [Util.ComparedType] 
An arbitrary order on values.

compare [Symbol] 
An arbitrary ordering on symbols.

compare [Id.T]  compare x y is an arbitrary order for x and y

compare [Dl_number.T] 
Comparison of numbers.

compare [Constant] 
An arbitrary ordering on constants.

compose [Function] 
Function composition.

conditional [Term_logic.Constructor] 
Conditional expression: Boolean condition, and Boolean alternatives.

conditional [Term_constant] 
Logical ifthenelse.

conditional [Symbol.Primitive]  
conflict_clause [Cc_core] 
An explanation for a conflict.

conflict_detected [Dpll_core] 
Has the solver deduced that the current (partial) model cannot
be (extended to) a satisfying variable assignment?

conflict_detected [Dl_core.T] 
Has a conflict been detected in the solver?

conflict_detected [Cc_core] 
Has a conflict been detected in the current solver state?

conjunction [Ternary] 
Conjunction of ternary values.

conjunction [Term_logic.Constructor] 
Conjunction of two terms.

conjunction [Term_constant] 
Logical conjunction.

conjunction [Symbol.Primitive]  
connection [Smtlib_syntax] 
Application of a named logical connective to a list of arguments.

constant [Term] 
A constant.

constant [Smtlib_syntax] 
A symbolic constant.

constant [Function] 
Constant function.

constant_value [Term]  constant_value t is the value of a constant.

copy [Vec]  copy v is a copy of v ; the elements are shared by v and
the copy.

copy [Index.Map] 
A copy of the map.

copy [Bihashtbl.S] 
A copy of the given hash table.

count [List_util]  count p l is the number of elements in l for which p holds.

count [Id.Generator] 
The number of identifiers produced by this generator.

couple [Bunch] 
A bunch with the two elements provided.

create [Vec] 
Synonym for
Vec.make .

create [Union_find.S] 
A new unionfind data structure.

create [Priority_queue]  create c is a new priority queue, where the priority among
elements is defined by the comparison function c .

create [Index.PriorityQueue] 
An empty queue.

create [Index.Set] 
Create an empty set in constant time.

create [Index.Map2]  create n m creates a new, empty map.

create [Index.Map]  create x is a new, empty map.

create [Bihashtbl.S]  create n is a new, empty bijective hash table with capacity
for n entries.

curry [Function] 
Curries a function.

D  
decide [Dpll_core] 
Makes an arbitrary assignment to an unassigned variable.

decision_level [Dpll_core] 
The number of variables assigned arbitrarily by
Dpll_core.decide in the
current solver state.

decision_level [Dl_core.T] 
The decision level of the solver.

decision_level [Cc_core] 
Decision level of the solver.

decision_possible [Dpll_core] 
Might further arbitrary variable assignment decisions be
attempted?

declare [Symbol]  declare n a declares a new symbol with the name n and arity a
which is interpreted by some theory.

declare_constant [Smtlib_syntax]  declare_constant c declares a function symbol.

declare_predicate [Smtlib_syntax]  declare_predicate p declares a predicate symbol.

declare_uninterpreted [Symbol] 
like
declare , but for an uninterpreted symbol

default [Option] 
The value contained in an option, or a default if there is none.

delete [Vec]  delete v i removes the element at position i of v , pulling
elements above down by 1 .

dequeue [Index.PriorityQueue]  dequeue q removes the highest priority element from q .

difference [Term_logic.Constructor] 
Logical disequivalence of two (Boolean) terms.

difference [Term_constant] 
Exclusive or.

difference [Symbol.Primitive]  
disjunction [Ternary] 
Disjunction of ternary values.

disjunction [Term_logic.Constructor] 
Disjunction of two terms.

disjunction [Term_constant] 
Logical disjunction.

disjunction [Symbol.Primitive]  
divide [Term_constant] 
Arithmetic division.

divide [Symbol.Primitive]  
drop [Index.PriorityQueue]  drop q removes the highest priority element from q .

E  
empty [Bunch] 
An empty bunch.

enqueue [Index.PriorityQueue]  enqueue q e enqueues the element e .

epoch [Time] 
Dawn of processor time.

epsilon [Dl_number.T] 
A small number.

equal [Variable] 
Are two variables equal?

equal [Util.ComparedType] 
Are two values equal?

equal [Symbol] 
Are two symbols equal?

equal [Id.T] 
Are two identifiers equal?

equal [Dl_number.T] 
Are the numbers equal? .

equal [Dl_core.L] 
Are the two literals equal?

equal [Constant] 
Are two constants equal?

equal [Cc_literal]  equal l m literals l and m equal (understands that
equality and disequality are commutative)?

equality [Term_logic.Constructor] 
Equality of two nonBoolean terms.

equality [Term_constant] 
Equality

equality [Symbol.Primitive]  
equivalence [Term_logic.Constructor] 
Logical equivalence of two (Boolean) terms.

equivalence [Term_constant] 
Logical equivalence.

equivalence [Symbol.Primitive]  
equivalent [Union_find.S] 
Are the two elements equivalent?

exists [Vec]  exists p v holds if some element of v satisfies p .

exists [Subarray]  exists p a i j is true when there is a k in the range
i ...

exists [Bunch]  exists p b is true if p x holds for any x in b .

exists [Array_util]  exists p a is true when there is some x in a p x .

exists_const [Vec]  
exists_const [Subarray]  exists_const p x a i j is the same as Subarray.exists (p
x) a i j , only faster because applying closures is slow.

exists_const [Array_util]  exists_const p x a is the same as Array_util.exists (p x)
a , only faster because applying closures is slow.

exists_unique [List_util]  exists_unique p l holds when p for exactly one element of l .

explain [Dl_core.T] 
Clause explaining the propagated literal.

explain_conflict [Dl_core.T] 
Conflict clause.

explode [Util.String]  explode "abc..." is ['a';'b';'c';...] .

F  
falsity [Ternary] 
false value.

falsity [Term_constant] 
Logical false.

falsity [Symbol.Primitive]  
fast_filter [Vec] 
Like
Vec.filter , but does not preserve the order of elements.

fast_filter_const [Vec]  
filter [Vec]  filter p v removes those elements of v not satisfying p

filter [Option] 
Filter the value in an option.

filter [Bunch]  filter p b is a bunch containing all elements of b that
satisfy predicate b .

filter_const [Vec]  
filter_const [Bunch]  
filteri [Vec] 
Like
Vec.filter , but the predicate takes the index of the
element as the first argument.

filteri_const [Vec]  
final_check [Cc_core] 
Determine consistency before we declare satisfiability.

find [Vec]  find p v is the first element of v satisfying p .

find [Symbol]  find n is the symbol declared with name n .

find [Index.Map2]  find m i j is the element m maps i and j to.

find [Index.Map]  find m k is the mapping for the index of k in m .

find [Bihashtbl.S]  find b k is the element to which k is mapped by b .

find_const [Vec]  
find_index [List_util]  find_index p l is the index of the first element in l that
satisfies p .

find_inv [Bihashtbl.S]  find_inv b e is the key that b maps to e .

first [Vec]  first p v is the index of the first element of v satisfying
p .

first [Subarray]  first p v is the index of the first element of a in the
range i ...

first_const [Vec]  
first_const [Subarray]  first_const p x a i j is the same as Subarray.first (p x)
a i j , only faster because applying closures is slow.

fix [Function] 
Computes the fixpoint for the function transformer.

flatten [Option] 
Flatten a doubly optional value.

flip [Function] 
Flips the order of the first two argument.

fold [Index.Set]  fold f a s applies f to an accumulated value and each
element in the set s .

fold [Index.Map]  fold f a m applies f to an accumulated value and each
keyvalue pair in the mapping m .

fold [Id.Generator] 
Fold over all identifiers produced by the generator.

fold [Bunch]  fold f a b folds f over every element of b using a as an
initial value.

fold [Bihashtbl.S]  fold f b a is (f kN eN ... (f k1 e1 a) ... ) , where b is
a collection of entries {(k1,e1) ... (kN,eN)} ordered with
respect to Bihashtbl.S.key .

fold_const [Index.Set]  
fold_const [Index.Map]  
fold_left [Vec]  fold_left f l v computes f (... (f (f l ( Vec.get v i))
( Vec.get v (i+1)) ...) (Vec.get v ( Vec.length v  1)) .

fold_left [Util.String]  fold f a "ijk...z" is f (... (f (f a 'i') 'j') ...)
'z' .

fold_left [Subarray]  fold_left f l a i j computes
f (... (f (f l a.(i)) a.(i+1)) ...) a.(j1) .

fold_left_const [Vec]  
fold_left_const [Subarray]  fold_left_const f x l a i j is Subarray.fold_left (f x) l
a i j , only faster since applying closures is slow.

fold_right [Vec]  fold_right f v r computes f ( Vec.get v i) (... (f
( Vec.get v (j2)) (f ( Vec.get v ( Vec.length v 
1)) r)) ...)

fold_right [Util.String]  fold_right f "ijk...z" a is f 'i' (f 'j' (... (f 'z' a)
...)) .

fold_right [Subarray]  fold_right f a i j r computes
f a.(i) (... (f a.(j2) (f a.(j1) r)) ...)

fold_right_const [Vec]  
fold_right_const [Subarray]  fold_right_const f x a i j r is Subarray.fold_right (f x)
a i j r , only faster since applying closures is slow.

foldi_left [Vec]  fold_lefti f l v computes f (... (f (f l i ( Vec.get v
i)) (i+1) ( Vec.get v (i+1))) ...) (j1) ( Vec.get v
( Vec.length v  1)) .

foldi_left [Subarray]  fold_lefti f l a i j computes
f (... (f (f l i a.(i)) (i+1) a.(i+1)) ...) (j1) a.(j1) .

foldi_left_const [Vec]  
foldi_left_const [Subarray]  fold_lefti f x l a i j is Subarray.foldi_left (f x) l a i
j , only faster since applying closures is slow.

foldi_right [Vec]  foldi_right f v r computes f i ( Vec.get v i) (... (f
(j2) ( Vec.get v (j2)) (f (j1) ( Vec.get v
( Vec.length v  1)) r)) ...)

foldi_right [Subarray]  foldi_right f a i j r computes
f i a.(i) (... (f (j2) a.(j2) (f (j1) a.(j1) r)) ...)

foldi_right_const [Vec]  foldi_right_const f x v r is Vec.foldi_right (f x) v r , only
faster since applying closures is slow.

foldi_right_const [Subarray]  foldi_right_const f x a i j r is Subarray.foldi_right (f
x) a i j r , only faster since applying closures is slow.

for_all [Vec]  all p v holds if every element of v satisfies p .

for_all [Subarray]  for_all p a i j is true when for every k in the range
i ...

for_all [Bunch]  for_all p b is true if p x holds for every x in b .

for_all [Array_util]  for_all p a is true when for every x in a p x .

for_all_const [Vec]  
for_all_const [Subarray]  for_all_const p x a i j is the same as Subarray.for_all (p
x) a i j , only faster because applying closures is slow.

for_all_const [Array_util]  for_all_const p x a is the same as Array_util.for_all (p
x) a , only faster because applying closures is slow.

forget_some_learned_clauses [Dpll_core] 
Forget some clauses learned by the solver though conflict
analysis.

formula [Smtlib_attribute] 
Formula attribute value from a collection of attributes.

free_variables [Term] 
The free variables of a term.

fresh [Variable] 
A fresh variable.

fresh [Id.Generator] 
An identifier not previously produced by the generator.

fresh_variable [Dpll_core] 
Fresh variable in the given solver.

fresh_variable [Dl_core.T] 
A fresh variable for the solver.

fresh_variable [Cc_core] 
A fresh variable in the given solver.

G  
get [Vec]  get v i is the i th element v .

get_lemma [Dl_core.T] 
Get a lemma from the solver.

get_lemma [Cc_core] 
Choose an inferred lemma that has not been chosen before.

get_lemma_possible [Dl_core.T] 
Does the solver have a lemma to propagate?

get_lemma_possible [Cc_core] 
Are there any lemmas waiting to be dispatched?

get_literal [Dpll_core] 
Choose an interface literal assigned true in the current partial
model that has not been chosen since it was assigned.

get_literal [Dl_core.T] 
Get a literal from the solver.

get_literal [Cc_core] 
Choose an inferred interface literal that has not been chosen
before.

get_literal_possible [Dpll_core] 
Is there an interface literal in the current partial model that
has not been dispatched by
Dpll_core.get_literal since it was
assigned?

get_literal_possible [Dl_core.T] 
Does the solver have a literal to propagate?

get_literal_possible [Cc_core] 
Are there any inferred interface literals waiting to be
dispatched?

greater [Term_constant] 
Greaterthan relation.

greater [Symbol.Primitive]  
greater_or_equal [Term_constant] 
Greaterthanorequal relation.

greater_or_equal [Symbol.Primitive]  
grow [Vec]  grow v n x grows the size of v to n , filling in the newly
created slots with x .

grow_init [Vec]  grow_init v n f grows the size of v to n , filling in each newly
created slots i with f i .

H  
hash [Variable] 
Hash code of a variable.

hash [Util.ComparedType] 
Hash code of a value.

hash [Symbol] 
Hash code of a symbol.

hash [Id.T]  hash x is the hash code for x

hash [Dl_number.T] 
Hash value for number.

hash [Dl_core.L] 
Hash function for literals.

hash [Constant] 
Hash code of a constant.

head [Index.PriorityQueue]  head q is the highest priority element of q .

I  
identity [Function] 
The identity function.

imbalance [Bunch] 
The worst imbalance in the internal tree representation of a
bunch.

implication [Term_logic.Constructor] 
Implication of two terms.

implication [Term_constant] 
Logical implication.

implication [Symbol.Primitive]  
implode [Util.String]  implode ['a';'b';'c';...] is "abc..." .

inc_priority [Index.PriorityQueue]  inc_priority q e x adds x to the priority of element e .

increment_level [Dl_core.T] 
Increment the decision level of the solver.

increment_level [Cc_core] 
Increment decision_level.

index [Index.IndexedType] 
Indexing function for objects of type
t .

infer [Dpll_core] 
Attempt to infer a unit propagation or a conflict.

infer [Dl_core.T] 
Attempt to make some inferences.

infer [Cc_core] 
Attempt to make inferences from currently assigned literals.

inference_possible [Dpll_core] 
Might an inference be made?

inference_possible [Dl_core.T] 
Might the solver attempt to make an inference?

inference_possible [Cc_core] 
Might an inference be made?

init [Vec]  init n f is a vector with length n .

initialize [Smtlib_parser]  initialize smtlib tokenizer theory_parser logic_parser
benchmark_parser initializes the combined smtlib file parser.

initialized [Smtlib_parser] 
Has the parser been initialized?

insert [Vec]  insert v i x inserts x into position i of v , pushing
elements at position i and above up by 1 .

insert [Priority_queue]  insert q e inserts element e into the priority queue q , if
it is not already a member.

integer [Smtlib_syntax]  integer i is an integer constant with value i.

integer [Constant] 
Arbitrary precision integer constant.

integer_constant [Term] 
Integer constant.

integer_value [Term]  integer_value t is the value of an integer constant.

integer_value [Constant]  integer_value c is the integer value of c.

interpreted [Symbol]  
invalid [Id.T] 
A distinguished invalid identifier, useful for dummy values.

invalid_literal [Cc_literal] 
An invalid literal.

inverse [Index.IndexedType]  inverse i is the x such that index x = i .

is_abstraction [Term] 
Is a term an abstraction?

is_application [Term] 
Is a term an application?

is_boolean_constant [Term_constant]  
is_constant [Term] 
Is the term a constant?

is_decided [Dpll_core] 
Has the literal been assigned by arbitrary decision?

is_empty [Vec]  
is_empty [Priority_queue]  is_empty q holds if and only if the queue q is empty.

is_empty [Index.PriorityQueue]  is_empty q is true iff there are no elements enqueued in q .

is_empty [Index.Set] 
Is a set empty?

is_empty [Index.Map]  is_empty m holds if the map is empty.

is_empty [Bunch] 
Is a bunch empty?

is_inferred [Dpll_core] 
Has the literal been inferred by unit propagation?

is_inferred [Cc_core] 
Can the solver produce an explanation for a literal?

is_integer [Constant] 
Is a constant an integer value?

is_integer_constant [Term] 
Is a term an integer constant.

is_interface_variable [Dpll_core] 
Is the variable an interface_variable?

is_literal [Term_literal] 
Holds when a term is a variable or the negation of a variable.

is_logical_constant [Term_constant]  
is_none [Option] 
Does an option contain no value?

is_number [Dl_number.T] 
Does the term represent a number?

is_positive [Term_literal]  is_positive l holds if the literal term t is positive.

is_positive [Dpll_literal]  is_positive l is true when l is a literal positive.

is_rational [Constant] 
Is a constant a rational value

is_rational_constant [Term] 
Is a term a rational constant.

is_representative [Union_find.S] 
Is the element the representative for its class?

is_some [Option] 
Does an option contain a value?

is_symbolic [Constant] 
Is a constant symbolic?.

is_symbolic_constant [Term] 
Is a term a symbolic constant.

is_true [Dpll_core] 
Is the literal assigned true?

is_true [Dl_core.T] 
Is the literal true in the current state of the solver?

is_true [Cc_core] 
Is the literal assigned true in the solver state?

is_valid [Id.T] 
Is an identifier valid?

is_valid_literal [Cc_literal] 
Is a literal valid.

is_variable [Term] 
Is the term a variable?

ite [Term_logic.Constructor] 
Conditional expression: Boolean condition, nonBoolean alternatives.

ite [Term_constant] 
Ifthenelse

ite [Symbol.Primitive]  
iter [Vec]  iter c v evaluates c on each element of v .

iter [Subarray]  iter c a i j evaluates c a.(k) for each k in the range
i ...

iter [Index.Set]  iter c s applies c to all elements of s .

iter [Index.Map]  iter f m applies f to all mappings in m .

iter [Id.Generator] 
Iterate over all identifiers produced by the generator.

iter [Bunch]  iter f b evaluates f on all the elements of b .

iter [Bihashtbl.S]  iter c t applies c to every entry in b .

iter_const [Vec]  
iter_const [Subarray]  
iter_const [Index.Set]  
iter_const [Index.Map]  
iter_const [Bunch]  
iter_pairwise [List_util]  iter_pairwise f l applies f to all pairs (a,b) such
that a occurs in l and b occurs after a in l .

iteri [Vec] 
Like
Vec.iter , but the command takes the index of the element
as the first argument

iteri [Subarray]  iter c a i j evaluates c k a.(k) for each k in the range
i ...

iteri_const [Vec]  
iteri_const [Subarray]  
J  
join [Bunch] 
The constant time union of two bunches.

K  
k [Term_constant] 
Constant function constructor.

k [Symbol.Primitive]  
L  
length [Vec]  length v is the number of elements in v .

length [Index.PriorityQueue]  length q is the number of elements in the queue.

length [Bihashtbl.S] 
Number of entries in a bijective hash table.

less [Term_constant] 
Lessthan relation.

less [Symbol.Primitive]  
less_or_equal [Term_constant] 
Lessthanorequal relation.

less_or_equal [Symbol.Primitive]  
level [Dpll_core] 
The decision level at which a literal was assigned.

limit [Vec] 
Maximum number of elements possible in this vector.

limit_for [Vec]  limit_for x is the maximum number of elements of the same type
as x that may be stored in a vector.

literal [Term_literal]  literal v is the positive literal term with variable v .

literal [Dpll_literal]  literal v is the positive literal corresponding to variable v .

literal_explanation [Cc_core] 
An explanation clause for an assigned interface literal.

literal_to_explain [Dpll_core] 
Returns the next conflict literal to explain for conflict
resolution.

local_flet [Smtlib_syntax] 
Local binding of a formula variable.

local_let [Smtlib_syntax] 
Local binding of an expression variable.

log [Variable]  log level c is equivalent to
Log.log level pp_print c

log [Log]  Log.log print level x outputs x using print , if
level <= current log level

log [Dl_number.T] 
Output the number to the log.

log [Constant]  log level c is equivalent to
Log.log level pp_print c

log_bool [Log]  Log.log_bool level b logs b , if level <= current log level

log_float [Log]  Log.log_float level j logs j , if level <= current log level

log_flush [Log]  Log.log_flush level () flushes the log output, if level
<= current log level

log_int [Log]  Log.log_int level i logs i , if level <= current log level

log_newline [Log]  Log.log_newline level () outputs a new line and flushes
the log output, if level <= current log level

log_string [Log]  Log.log_string level s logs s , if level <= current log level

log_term [Term]  log_term level tm is equivalent to
Log.log level pp_print_term tm

log_time [Log]  Log.log_time level t logs seconds of processor time since
t , if level <= current log level

logic [Smtlib_attribute] 
The logic attribute of a collection of attributes.

M  
make [Vec]  make n x is a vector of length n , with each element equal to
x .

map [Option] 
Map a function over the value in an option.

map [Bunch]  map f a maps every element of a using f .

mem [Vec]  mem x v holds if x is an element of v .

mem [Subarray]  mem x a i j is true when there is a k in the range
i ...

mem [Index.PriorityQueue]  mem q e is true iff e is enqueued in q .

mem [Index.Set] 
Determine whether element is a member of the set in constant time.

mem [Index.Map2]  mem m i j if m maps the keys i and j to some value.

mem [Index.Map]  mem m k is true iff there is a mapping for index k in m ,
i.e.

mem [Bihashtbl.S]  mem b k holds when there is an entry for k in b .

mem [Array_util]  mem x a is true when x is an element of a

mem_inv [Bihashtbl.S]  mem_inv b e holds when an entry in b maps some key to e .

members [Union_find.S]  members s x is the bunch of all elements in the class of x .

minus [Term_constant] 
Arithmetic subtraction.

minus [Symbol.Primitive]  
mk_array [Term_constant] 
Array constants

mk_array [Symbol.Primitive]  
model [Dpll_core] 
A model satisfying the problem.

modify [Vec]  modify f v replaces each element of v with f of that element.

modify [Subarray]  modify f a i j sets a.(k) to f a.(k) for each k in the
range i ...

modify [Index.Map]  modify f m modifies a map so that each index maps to f of its
prior value.

modify_const [Vec]  
modify_const [Subarray]  modify_const f x a i j is Subarray.modify (f x) a i j ,
only faster because applying closures is slow.

modify_const [Index.Map]  modify_const f x v is modify (f x) v , only faster since applying
closures is slow.

N  
name [Smtlib_attribute] 
The name attribute of a collection of attributes.

name_declared [Symbol]  name_declared n is true when a symbol has been declared with name n.

named [Variable]  named n variable with the name n .

nary_abstraction [Term]  nary_abstraction [v0, ... ,vn] tm is \v0. ... \vn.tm .

nary_application [Term]  nary_application f args is equivalent to List.fold_left
application f args .

nary_application_decomposition [Term] 
Decompose a term to yield a function and a list of arguments.

negation [Ternary] 
Negation of a ternary.

negation [Term_logic.Constructor] 
Negation of a term.

negation [Term_literal] 
Negation of a term literal.

negation [Term_constant] 
Logical negation.

negation [Symbol.Primitive]  
negation [Dpll_literal]  negation l is the negation of literal l .

negation [Dl_core.T] 
The negation of the literal.

negation [Cc_literal]  negation l is the nation of l .

new_generator [Id.Generator] 
A new fresh identifier generator.

new_solver [Dpll_core] 
New DPLL solver.

new_solver [Dl_core.T] 
A new solver for difference logic over nums.

new_solver [Cc_core] 
A new solver.

now [Time] 
Current processor time.

num_clauses [Dpll_core] 
Number of added clauses that are tracked in current state.

num_conflicts [Dpll_core] 
Number of conflicts encountered.

num_decisions [Dpll_core] 
Number of arbitrary variable assignment ever tried.

num_externally_set [Dpll_core] 
Number of variable assignments ever made by
Dpll_core.set_literal .

num_inferences [Dpll_core] 
Number of variable assignment ever made by unit propagation.

num_learneds [Dpll_core] 
Number of clauses learned through conflict analysis in current
state.

num_vars [Dpll_core] 
Number of variables created.

number [Dl_number.T] 
The number represented by term.

O  
of_array [Vec]  of_array a is a vector with the elements of a .

of_list [Vec]  of_list l is a vector of the elements of l in their
positional order.

of_list [Bunch] 
A bunch with all the elements in the list.

P  
parse_benchmark [Smtlib_parser]  parse_logic path parses the SMTLIB benchmark file at the
specified path and returns the attributes of benchmark.

parse_logic [Smtlib_parser]  parse_logic path parses the SMTLIB logic file at the
specified path and returns the attributes of logic.

parse_theory [Smtlib_parser]  parse_theory path parses the SMTLIB theory file at the
specified path and returns the attributes of theory.

partition [Bunch]  partition p b is a pair of bunches (b1, b2) such that b1
contains all elements of b that satisfy predicate b , and
b2 contains the rest.

partition_const [Bunch]  
perform [Option] 
Perform a command on the value in an option.

plus [Term_constant] 
Arithmetic addition.

plus [Symbol.Primitive]  
pop [Vec]  pop v removes the last element of v .

pop [Priority_queue]  pop q removes the highest priority from the queue q .

potential [Dl_core.T] 
The (negation of) the value assignment to variables in the
current model.

pp_compact_print_term [Term] 
Prettyprint a term, compactly by defining local lets to avoid
repetitiously printing shared subterms.

pp_print [Variable] 
Print a variable.

pp_print [Symbol] 
Pretty print a symbol.

pp_print [Constant] 
Print a constant.

pp_print_list [List_util] 
Given a function for printing a list element and a function for
printing a list element seperater, print a list.

pp_print_term [Term] 
Prettyprint a term.

predicate [Smtlib_syntax] 
Application of a named predicate to a list of arguments.

prefix [Util.String]  prefix s0 s1 holds if s0 is a prefix of s1 .

print [Dl_number.T] 
Prints the number.

print_term [Term] 
Print a term using
std_formatter .

priority [Index.PriorityQueue] 
The priority of an element.

promote [Priority_queue]  promote q e reorganizes the priority queue q to take into
account the newly raised priority of element e .

proxy_app [Cc_core]  proxy_app s f x returns a proxy y for the application
of f to x .

proxy_k [Cc_core]  proxy_k s x returns a proxy a for the constant function
evaluating to x .

proxy_u [Cc_core]  proxy_u s a i x returns a proxy b for the update of a at
i with x .

push [Vec]  push v x extends the length of the v by 1 .

Q  
quantification [Smtlib_syntax] 
A named quantification over a list of variables.

R  
rational [Smtlib_syntax]  rational r creates a rational constant with value r.

rational [Constant] 
Arbitrary precision rational constant.

rational_constant [Term] 
Arbitrary precision rational constant.

rational_value [Term]  rational_value t is the value of a rational constant.

rational_value [Constant]  rational_value c is the rational value of c.

reduce [Equality_propagation]  
remove [Index.Set]  remove s e removes element e from the set s in constant time.

remove [Index.Map2]  remove m i j removes any value associated with i and j by m .

remove_elt [Bihashtbl.S]  remove_key b y removes any entry that maps to the element
e from b .

remove_key [Bihashtbl.S]  remove_key b k removes any entry that maps the key k from
b .

remove_sorted_duplicates [List_util] 
A list sorted in ascending order according to a comparison
function, with duplicate elements removed.

replace [Index.Map]  replace m k x updates m by mapping the index of k to x .

replace [Bihashtbl.S]  replace b k e updates the entries in b so that k is
mapped to e .

representative [Union_find.S] 
A representative for the class containing the element.

restart [Dpll_core] 
Undo all arbitrary variable assignment decisions.

restart [Cc_core] 
Backjumps to level 0 if not already there.

rev [Vec]  rev v reverses the order of elements in v .

rev [Subarray]  rev a i j reverses the order of the elements in the range i ...

rewrite [Term_logic.Rewriter] 
A term transformation.

S  
satisfied [Dpll_core] 
Has the solver deduced that the current model is a satisfying
assignment for every variable?

scale [Index.PriorityQueue]  scale q x multiplies the priority of every element by the constant
factor x .

select [Term_constant] 
Array select.

select [Symbol.Primitive]  
set [Vec]  set v i x stores x as element i of v .

set [Index.Map2]  set m i j x modifies m by mapping the keys i and j to x .

set_all [Vec]  set_all v i j x stores x in elements i ...

set_all [Subarray]  set_all a i j x sets all the elements in the range i ...

set_all [Index.Map]  set_all m x updates m by mapping every key to x .

set_conflict_clause [Dpll_core]  set_conflict_clause ls initializes the conflict clause with
the disjoined literals.

set_fun [Subarray]  set_fun a i j f sets each element k in the range i ...

set_literal [Dpll_core] 
Attempt to make a variable assignment inferred by an external
agent.

set_literal [Dl_core.T] 
Add a literal assertion to the solver.

set_literal [Cc_core] 
Make a literal assignment obtained from another solver.

set_literal_explanation [Dpll_core]  set_literal_explanation s ls removes Dpll_core.literal_to_explain
from the set of conflict literals using the provided explanation
ls .

set_log_formatter [Log] 
Set the output destination for messages

set_log_level [Log] 
Set current log level

shrink [Vec]  shrink v n shrinks the size of v to n .

since [Time]  since t () is user processor time, in seconds, elapsed since
t .

singleton [Bunch] 
A singleton bunch.

size [Index.Set] 
Cardinality of the set.

size [Index.Map]  size m is the number of indices mapped by m .

size [Bunch] 
Number of elements in a bunch.

smtlib_logic_file [Smtlib_parser]  smtlib_logic_file name is the path to the SMTLIB logic file
describing the logic called name .

smtlib_theory_file [Smtlib_parser]  smtlib_theory_file name is the path to the SMTLIB theory file
describing the theory called name .

sort [Vec]  sort c v sorts elements of v in ascending order as defined by
the comparison function c.

sort [Subarray]  sort c a i j sorts elements of a in the range i ...

stable_sort [Vec]  stable_sort c v sorts elements of v in ascending order as
defined by the comparison function c.

stable_sort [Subarray]  stable_sort c a i j sorts elements of a in the range
i ...

status [Smtlib_attribute] 
The status attribute of a collection of attributes.

store [Term_constant] 
Array store.

store [Symbol.Primitive]  
string_of [Variable] 
string representation of a variable.

string_of [Constant] 
String representation of a constant.

string_of_symbol [Symbol] 
String representation (name) of a symbol.

string_of_term [Term] 
String representation of term.

subtract [Dl_number.T] 
Numeric subtraction.

swap [Vec]  swap v i j swaps the elements at positions i and j of v .

swap [Subarray]  swap a i j swaps the elements at positions i and j of a .

swap_out [Vec]  swap_out v i replaces the element at position i of v with
the last element of v , and decreases the length of v by 1 .

symbolic [Constant] 
A symbolic constant.

symbolic_constant [Term] 
A symbolic constant.

symbolic_value [Term]  symbolic_value t is the value of a symbolic constant.

symbolic_value [Constant]  symbolic_value c is the symbol underlying a symbolic constant.

T  
term_compare [Term] 
An arbitrary ordering on terms.

term_equal [Term] 
Are two terms equal?

term_hash [Term] 
A hash key for the term.

ternary_application [Term]  ternary_application f x y z is equivalent to application
(application (application f x) y) z .

ternary_of_bool [Ternary] 
Injection of a regular boolean into a ternary boolean.

times [Term_constant] 
Arithmetic multiplication.

times [Symbol.Primitive]  
to_array [Vec]  to_array v is an array with the elements of v .

to_list [Vec]  to_list v is a list of the elements of v in their
positional order.

to_list [Bunch] 
A list of all elements in the bunch.

token [Smtlib_lexer] 
Match the next token in the lexing buffer.

top [Vec]  top v is the last element of v .

transform [Rational_num]  
transform [Ite_removal]  
truth [Ternary] 
true value.

truth [Term_constant] 
Logical true.

truth [Symbol.Primitive]  
U  
unary_minus [Term_constant] 
Arithmetic unary minus.

unary_minus [Symbol.Primitive]  
unary_minus [Dl_number.T] 
Numeric unary minus.

uncurry [Function] 
Uncurry a function.

uninterpret [Term]  uninterpret p tbl tm replaces "uninterpreted constants",
i.e.

union [Union_find.S]  union s x y merges the equivalence classes for x and y .

unknown [Ternary] 
unknown value.

unsatisfiable [Dpll_core] 
Has the solver deduced that the problem is unsatisfiable?

until [Function]  until p f x applies f repeatedly, starting with x ,
until the predicate p evaluates to true .

update [Term_constant] 
Function update operator.

update [Symbol.Primitive]  
V  
v [Dl_number.Integral_value]  
value [Option] 
The value contained in an option.

variable [Term_literal]  variable l is the variable contained in a literal term.

variable [Term] 
A variable.

variable [Smtlib_syntax] 
A variable.

variable [Dpll_literal]  variable l is the variable in literal l .

variant [Variable]  variant avoid v is a variable with a name that of v , but not
occurring in avoid .

Z  
zero [Dl_number.T] 
The representation of zero.
