Index of values


( ** ) [Dimacs]	These notations notably allow to write `let x = Dimacs.(make (2io))` to create a two-dimensional array of size 2 on dimension 1 and size `i` on dimension 2, i.e.
A
add_clause [Dimacs]	Add a clause to the problem.
all_directions [Hex]	List of all possible directions.
B
bigor [Dimacs]	`bigor n f` returns the clause `f 0 \/ ... \/ f (n-1)`.
F
from_channel [Hex]	Read a grid and initial position from some input channel.
G
get_clauses [Dimacs]	Get the current problem as a list of clauses.
I
input [Dimacs]	Read a SAT problem in DIMACS format from some input channel.
M
make [Dimacs]	Create an n-dimensional array of variables (i.e.
move [Hex]	`move p d` indicates the position obtained when moving from `p` in direction `d` with just one step.
move_n [Hex]	Compute the position resulting from an arbitrary move.
N
nb_variables [Dimacs]	Number of variables currently declared.
not [Dimacs]	Negation of a literal.
O
o [Dimacs]
output [Dimacs]	Output the problem in DIMACS format on some output channel.
P
pp_bool_grid [Hex]
pp_char_grid [Hex]
pp_solution [Hex]	`pp_solution fmt grid path` displays the grid on `fmt`, and shows a path (list of positions) on it.
R
read_model [Dimacs]	Read model from some input channel in DIMACS format.
run [Dimacs]
run_int [Dimacs]
S
sat [Dimacs]	Tell whether a literal is satisfied in some model.
T
to_int [Dimacs]	Convert a literal to an integer: positive literals are mapped to positive integers that are less or equal to `nb_variables ()`; negative literals are mapped to the opposite negative integers.