Index of values

abstraction v tm is \v. tm.

Numberic addition.

add s e adds element e to the set s in (amortized) constant time.

add m k x modifies m by mapping the index of k to x.

Add an element to a bunch.

add b k e adds an entry mapping k to e to b.

Add an element to a bunch.

Adds the clause (disjunction of literals) to the solver.

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

add_interface_variables s v treats the variable v and its negation as interface literals.

Add an interface literal to the solver.

The application of the given terms.

Application of a named function to a list of arguments.

The argument in an application.

The function in an application.

arity s is the arity declared for s.

Arity of a constant.

A list of all the assumptions in a collection of attributes.

Resolve a conflict by backjumping to undo conflicting assignments from the current partial model.

Backjumps to the given level.

Might a backjump be used to resolve a conflict?

Backtrack to the given decision level.

The term obtained by reducing all beta-redexes in a term.

binary_application f x y is equivalent to application (application f x) y.

bool_of_ternary t is the boolean corresponding to a known ternary t.

Classify a value by placing it in an option.

clear v removes all elements from v.

Removes all elements from the queue.

Makes the set empty in (amortized) constant time.

Remove all entries from a hash table.

Compactly print a term using std_formatter.

An arbitrary ordering on variables.

An arbitrary order on values.

An arbitrary ordering on symbols.

compare x y is an arbitrary order for x and y

Comparison of numbers.

An arbitrary ordering on constants.

Function composition.

Conditional expression: Boolean condition, and Boolean alternatives.

Logical if-then-else.

An explanation for a conflict.

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

Has a conflict been detected in the solver?

Has a conflict been detected in the current solver state?

Conjunction of ternary values.

Conjunction of two terms.

Logical conjunction.

Application of a named logical connective to a list of arguments.

A constant.

A symbolic constant.

Constant function.

constant_value t is the value of a constant.

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

A copy of the map.

A copy of the given hash table.

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

The number of identifiers produced by this generator.

A bunch with the two elements provided.

Synonym for Vec.make.

A new union-find data structure.

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

An empty queue.

Create an empty set in constant time.

create n m creates a new, empty map.

create x is a new, empty map.

create n is a new, empty bijective hash table with capacity for n entries.

Curries a function.

Makes an arbitrary assignment to an unassigned variable.

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

The decision level of the solver.

Decision level of the solver.

Might further arbitrary variable assignment decisions be attempted?

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

declare_constant c declares a function symbol.

declare_predicate p declares a predicate symbol.

like declare, but for an uninterpreted symbol

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

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

dequeue q removes the highest priority element from q.

Logical dis-equivalence of two (Boolean) terms.

Exclusive or.

Disjunction of ternary values.

Disjunction of two terms.

Logical disjunction.

Arithmetic division.

drop q removes the highest priority element from q.

An empty bunch.

enqueue q e enqueues the element e.

Dawn of processor time.

A small number.

Are two variables equal?

Are two values equal?

Are two symbols equal?

Are two identifiers equal?

Are the numbers equal? .

Are the two literals equal?

Are two constants equal?

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

Equality of two non-Boolean terms.

Equality

Logical equivalence of two (Boolean) terms.

Logical equivalence.

Are the two elements equivalent?

exists p v holds if some element of v satisfies p.

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

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

exists p a is true when there is some x in a p x.

exists p x v is Vec.exists (p x) v, but faster since applying closures is slow.

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 p x a is the same as Array_util.exists (p x) a, only faster because applying closures is slow.

exists_unique p l holds when p for exactly one element of l.

Clause explaining the propagated literal.

Conflict clause.

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

false value.

Logical false.

Like Vec.filter, but does not preserve the order of elements.

fast_filter_const p x v is Vec.fast_filter (p x) v, only faster since applying closures is slow.

filter p v removes those elements of v not satisfying p

Filter the value in an option.

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

filter_const p x v is Vec.filter (p x) v, only faster since applying closures is slow.

filter_const p c b is Bunch.filter (p c) b, only faster since applying closures is slow.

Like Vec.filter, but the predicate takes the index of the element as the first argument.

filteri_const p x v is Vec.filteri (p x) v, only faster since applying closures is slow.

Determine consistency before we declare satisfiability.

find p v is the first element of v satisfying p.

find n is the symbol declared with name n.

find m i j is the element m maps i and j to.

find m k is the mapping for the index of k in m.

find b k is the element to which k is mapped by b.

find_const p x v is Vec.find (p x) v, but faster since applying closures is slow.

find_index p l is the index of the first element in l that satisfies p.

find_inv b e is the key that b maps to e.

first p v is the index of the first element of v satisfying p.

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

first_const p x v is Vec.first (p x) v, but faster since applying closures is slow.

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.

Computes the fix-point for the function transformer.

Flatten a doubly optional value.

Flips the order of the first two argument.

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

fold f a m applies f to an accumulated value and each key-value pair in the mapping m.

Fold over all identifiers produced by the generator.

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

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 f x a s is Index.Set.fold (f x) a s, only faster since applying closures is slow.

fold_const f x a m is Index.Map.fold (f x) a m, only faster since applying closures is slow.

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 f a "ijk...z" is f (... (f (f a 'i') 'j') ...) 'z'.

fold_left f l a i j computes f (... (f (f l a.(i)) a.(i+1)) ...) a.(j-1).

fold_left_const f x l v is Vec.fold_left (f x) l v, only faster since applying closures is slow.

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 f v r computes f (Vec.get v i) (... (f (Vec.get v (j-2)) (f (Vec.get v (Vec.length v - 1)) r)) ...)

fold_right f "ijk...z" a is f 'i' (f 'j' (... (f 'z' a) ...)).

fold_right f a i j r computes f a.(i) (... (f a.(j-2) (f a.(j-1) r)) ...)

fold_right_const f x v r is Vec.fold_right (f x) v r, only faster since applying closures is slow.

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.

fold_lefti f l v computes f (... (f (f l i (Vec.get v i)) (i+1) (Vec.get v (i+1))) ...) (j-1) (Vec.get v (Vec.length v - 1)).

fold_lefti f l a i j computes f (... (f (f l i a.(i)) (i+1) a.(i+1)) ...) (j-1) a.(j-1).

fold_lefti f x l v is Vec.foldi_left (f x) l v, only faster since applying closures is slow.

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 f v r computes f i (Vec.get v i) (... (f (j-2) (Vec.get v (j-2)) (f (j-1) (Vec.get v (Vec.length v - 1)) r)) ...)

foldi_right f a i j r computes f i a.(i) (... (f (j-2) a.(j-2) (f (j-1) a.(j-1) r)) ...)

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 f x a i j r is Subarray.foldi_right (f x) a i j r, only faster since applying closures is slow.

all p v holds if every element of v satisfies p.

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

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

for_all p a is true when for every x in a p x.

for_all_const p x v is Vec.for_all (p x) v, but faster since applying closures is slow.

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 p x a is the same as Array_util.for_all (p x) a, only faster because applying closures is slow.

Forget some clauses learned by the solver though conflict analysis.

Formula attribute value from a collection of attributes.

The free variables of a term.

A fresh variable.

An identifier not previously produced by the generator.

Fresh variable in the given solver.

A fresh variable for the solver.

A fresh variable in the given solver.

get v i is the ith element v.

Get a lemma from the solver.

Choose an inferred lemma that has not been chosen before.

Does the solver have a lemma to propagate?

Are there any lemmas waiting to be dispatched?

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

Get a literal from the solver.

Choose an inferred interface literal that has not been chosen before.

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

Does the solver have a literal to propagate?

Are there any inferred interface literals waiting to be dispatched?

Greater-than relation.

Greater-than-or-equal relation.

grow v n x grows the size of v to n, filling in the newly created slots with x.

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

Hash code of a variable.

Hash code of a value.

Hash code of a symbol.

hash x is the hash code for x

Hash value for number.

Hash function for literals.

Hash code of a constant.

head q is the highest priority element of q.

The identity function.

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

Implication of two terms.

Logical implication.

implode ['a';'b';'c';...] is "abc...".

inc_priority q e x adds x to the priority of element e.

Increment the decision level of the solver.

Increment decision_level.

Indexing function for objects of type t.

Attempt to infer a unit propagation or a conflict.

Attempt to make some inferences.

Attempt to make inferences from currently assigned literals.

Might an inference be made?

Might the solver attempt to make an inference?

Might an inference be made?

init n f is a vector with length n.

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

Has the parser been initialized?

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

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

integer i is an integer constant with value i.

Arbitrary precision integer constant.

Integer constant.

integer_value t is the value of an integer constant.

integer_value c is the integer value of c.

A distinguished invalid identifier, useful for dummy values.

An invalid literal.

inverse i is the x such that index x = i.

Is a term an abstraction?

Is a term an application?

Is the term a constant?

Has the literal been assigned by arbitrary decision?

is_empty v holds if and only if Vec.length v = 0.

is_empty q holds if and only if the queue q is empty.

is_empty q is true iff there are no elements enqueued in q.

Is a set empty?

is_empty m holds if the map is empty.

Is a bunch empty?

Has the literal been inferred by unit propagation?

Can the solver produce an explanation for a literal?

Is a constant an integer value?

Is a term an integer constant.

Is the variable an interface_variable?

Holds when a term is a variable or the negation of a variable.

Does an option contain no value?

Does the term represent a number?

is_positive l holds if the literal term t is positive.

is_positive l is true when l is a literal positive.

Is a constant a rational value

Is a term a rational constant.

Is the element the representative for its class?

Does an option contain a value?

Is a constant symbolic?.

Is a term a symbolic constant.

Is the literal assigned true?

Is the literal true in the current state of the solver?

Is the literal assigned true in the solver state?

Is an identifier valid?

Is a literal valid.

Is the term a variable?

Conditional expression: Boolean condition, non-Boolean alternatives.

If-then-else

iter c v evaluates c on each element of v.

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

iter c s applies c to all elements of s.

iter f m applies f to all mappings in m.

Iterate over all identifiers produced by the generator.

iter f b evaluates f on all the elements of b.

iter c t applies c to every entry in b.

iter_const c x v is Vec.iter (c x) v, only faster since applying closures is slow.

iter_const c x a i j is Subarray.iter (c x) a i j, only faster because applying closures is slow.

iter_const c x s is Index.Set.iter (c x) s, only faster since applying closures is slow.

iter_const f x m is Index.Map.iter (f x) m, only faster since applying closures is slow.

iter_const f c b is Bunch.iter (f c) b, only faster since applying closures is slow.

iter_pairwise f l applies f to all pairs (a,b) such that a occurs in l and b occurs after a in l.

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

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

iteri_const c x v is Vec.iteri (c x) v, only faster since applying closures is slow.

iteri_const c x a i j is Subarray.iteri (c x) a i j, only faster because applying closures is slow.

The constant time union of two bunches.

Constant function constructor.

length v is the number of elements in v.

length q is the number of elements in the queue.

Number of entries in a bijective hash table.

Less-than relation.

Less-than-or-equal relation.

The decision level at which a literal was assigned.

Maximum number of elements possible in this vector.

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

literal v is the positive literal term with variable v.

literal v is the positive literal corresponding to variable v.

An explanation clause for an assigned interface literal.

Returns the next conflict literal to explain for conflict resolution.

Local binding of a formula variable.

Local binding of an expression variable.

log level c is equivalent to Log.log level pp_print c

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

Output the number to the log.

log level c is equivalent to Log.log level pp_print c

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

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

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

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

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

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

log_term level tm is equivalent to Log.log level pp_print_term tm

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

The logic attribute of a collection of attributes.

make n x is a vector of length n, with each element equal to x.

Map a function over the value in an option.

map f a maps every element of a using f.

mem x v holds if x is an element of v.

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

mem q e is true iff e is enqueued in q.

Determine whether element is a member of the set in constant time.

mem m i j if m maps the keys i and j to some value.

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

mem b k holds when there is an entry for k in b.

mem x a is true when x is an element of a

mem_inv b e holds when an entry in b maps some key to e.

members s x is the bunch of all elements in the class of x.

Arithmetic subtraction.

Array constants

A model satisfying the problem.

modify f v replaces each element of v with f of that element.

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

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

modify_const f x v is Vec.modify (f x) v, only faster since applying closures is slow.

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

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

The name attribute of a collection of attributes.

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

named n variable with the name n.

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

nary_application f args is equivalent to List.fold_left application f args.

Decompose a term to yield a function and a list of arguments.

Negation of a ternary.

Negation of a term.

Negation of a term literal.

Logical negation.

negation l is the negation of literal l.

The negation of the literal.

negation l is the nation of l.

A new fresh identifier generator.

New DPLL solver.

A new solver for difference logic over nums.

A new solver.

Current processor time.

Number of added clauses that are tracked in current state.

Number of conflicts encountered.

Number of arbitrary variable assignment ever tried.

Number of variable assignments ever made by Dpll_core.set_literal.

Number of variable assignment ever made by unit propagation.

Number of clauses learned through conflict analysis in current state.

Number of variables created.

The number represented by term.

of_array a is a vector with the elements of a.

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

A bunch with all the elements in the list.

parse_logic path parses the SMT-LIB benchmark file at the specified path and returns the attributes of benchmark.

parse_logic path parses the SMT-LIB logic file at the specified path and returns the attributes of logic.

parse_theory path parses the SMT-LIB theory file at the specified path and returns the attributes of theory.

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 p c b is Bunch.partition (p c) b, only faster since applying closures is slow.

Perform a command on the value in an option.

Arithmetic addition.

pop v removes the last element of v.

pop q removes the highest priority from the queue q.

The (negation of) the value assignment to variables in the current model.

Pretty-print a term, compactly by defining local lets to avoid repetitiously printing shared sub-terms.

Print a variable.

Pretty print a symbol.

Print a constant.

Given a function for printing a list element and a function for printing a list element seperater, print a list.

Pretty-print a term.

Application of a named predicate to a list of arguments.

prefix s0 s1 holds if s0 is a prefix of s1.

Prints the number.

Print a term using std_formatter.

The priority of an element.

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

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

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

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

push v x extends the length of the v by 1.

A named quantification over a list of variables.

rational r creates a rational constant with value r.

Arbitrary precision rational constant.

Arbitrary precision rational constant.

rational_value t is the value of a rational constant.

rational_value c is the rational value of c.

remove s e removes element e from the set s in constant time.

remove m i j removes any value associated with i and j by m.

remove_key b y removes any entry that maps to the element e from b.

remove_key b k removes any entry that maps the key k from b.

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

replace m k x updates m by mapping the index of k to x.

replace b k e updates the entries in b so that k is mapped to e.

A representative for the class containing the element.

Undo all arbitrary variable assignment decisions.

Backjumps to level 0 if not already there.

rev v reverses the order of elements in v.

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

A term transformation.

Has the solver deduced that the current model is a satisfying assignment for every variable?

scale q x multiplies the priority of every element by the constant factor x.

Array select.

set v i x stores x as element i of v.

set m i j x modifies m by mapping the keys i and j to x.

set_all v i j x stores x in elements i...

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

set_all m x updates m by mapping every key to x.

set_conflict_clause ls initializes the conflict clause with the disjoined literals.

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

Attempt to make a variable assignment inferred by an external agent.

Add a literal assertion to the solver.

Make a literal assignment obtained from another solver.

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

Set the output destination for messages

Set current log level

shrink v n shrinks the size of v to n.

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

A singleton bunch.

Cardinality of the set.

size m is the number of indices mapped by m.

Number of elements in a bunch.

smtlib_logic_file name is the path to the SMT-LIB logic file describing the logic called name.

smtlib_theory_file name is the path to the SMT-LIB theory file describing the theory called name.

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

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

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

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

The status attribute of a collection of attributes.

Array store.

string representation of a variable.

String representation of a constant.

String representation (name) of a symbol.

String representation of term.

Numeric subtraction.

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

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

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.

A symbolic constant.

A symbolic constant.

symbolic_value t is the value of a symbolic constant.

symbolic_value c is the symbol underlying a symbolic constant.

An arbitrary ordering on terms.

Are two terms equal?

A hash key for the term.

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

Injection of a regular boolean into a ternary boolean.

Arithmetic multiplication.

to_array v is an array with the elements of v.

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

A list of all elements in the bunch.

Match the next token in the lexing buffer.

top v is the last element of v.

true value.

Logical true.

Arithmetic unary minus.

Numeric unary minus.

Uncurry a function.

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

union s x y merges the equivalence classes for x and y.

unknown value.

Has the solver deduced that the problem is unsatisfiable?

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

Function update operator.

The value contained in an option.

variable l is the variable contained in a literal term.

A variable.

A variable.

variable l is the variable in literal l.

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

The representation of zero.