Index of values


(%!) [Gmp41(Z(Infixes]
(*!) [Gmp41(Z(Infixes]
(*) [Euclid(Rat]
(*/) [Gmp41(Q(Infixes]
(+!) [Gmp41(Z(Infixes]
(+) [Euclid(Rat]
(+/) [Gmp41(Q(Infixes]
(-!) [Gmp41(Z(Infixes]
(-) [Euclid(Make]
(-/) [Gmp41(Q(Infixes]
(/!) [Gmp41(Z(Infixes]
(/) [Euclid(Rat]
(//) [Gmp41(Q(Infixes]
( [Gmp41(Q(Infixes]
( [Gmp41(Z(Infixes]
(<<<) [Term]
(<<<) [Var]
(<=!) [Gmp41(Q(Infixes]
(<=!) [Gmp41(Z(Infixes]
(<>!) [Gmp41(Q(Infixes]
(<>!) [Gmp41(Z(Infixes]
(=!) [Gmp41(Q(Infixes]
(=!) [Gmp41(Z(Infixes]
(=/=) [Hashcons]
(===) [Hashcons]
(>!) [Gmp41(Q(Infixes]
(>!) [Gmp41(Z(Infixes]
(>=!) [Gmp41(Q(Infixes]
(>=!) [Gmp41(Z(Infixes]
__ocaml_lex_token_rec [Lexer]

A
abs [Apply]
abs [Mpa.Q]
abs [Gmp41.Z]
abs [Gmp41.Z2]
add [Symtab]
add [Prop]
add [Context]
add [Partition]
Adding a constraint
add [C]
add [D]
add [Use]
add [Bitvector]
add [Coproduct]
add [Pair]
add [Arith]
add [Sign]
add [Sym]
add [Interval]
Adding two intervals
add [Trace]
add [Hashcons.Make]
add [Hashcons]
add [Mpa.Q]
add [Mpa.Z]
add [Gmp41.Q]
add [Gmp41.Z]
add [Gmp41.Z2]
add_at_exit [Tools]
add_at_reset [Tools]
add_scratch_context [Prop]
add_ui [Gmp41.Z]
addl [Sign]
addl [Interval]
addq [Interval]
Shifting by a rational.
all [Th]
all_ones [Bitv]
all_zeros [Bitv]
app [Th]
append [Bitv]
apply [Prop]
apply [Context]
apply [Sl]
apply [Solution]
apply [C]
apply [V]
apply [Use]
apply [Apply]
apply [Arith]
Application of a substitution.
apply [Term]
apply1 [Bitvector]
args [Context.Abstract]
args_of [Term]
arith [Context.Can]
arity [Symtab]
arr [Th]
array_too_small [Hashcons]
arrays_diseq [Context]
arrays_diseq1 [Context]
i <> j implies a[i:=x][j] = a[j].
arrays_diseq2 [Context]
i <> j and i <> k implies a[j:=x][i] = a[k:=y][i].
arrays_diseq3 [Context]
a[j:=x] = b[k:=y], i <> j, i <> k implies a[i] = b[i].
arrays_equal [Context]
arrays_equal1 [Context]
i = j implies a[i:= x][j] = x.
arrays_equal2 [Context]
a[i:=x] = b[i := y] implies x = y.
arrays_equal3 [Context]
a[j:=x] = b[k:=y], i <> j, i <> k implies a[i] = b[i].
assign [Pretty]
assignment [Prop]
assoc [Solution]
assq [Term]
Association lists for terms.
at_exit_functions [Tools]
at_reset_functions [Tools]
atom [Context.Process]
atom [Context.Abstract]
atom [Context.Can]
atom_is_negatable [Ics]
atom_mk_diseq [Ics]
atom_mk_equal [Ics]
atom_mk_false [Ics]
atom_mk_ge [Ics]
atom_mk_gt [Ics]
atom_mk_in [Ics]
atom_mk_le [Ics]
atom_mk_lt [Ics]
atom_mk_true [Ics]
atom_negate [Ics]
atom_of_string [Ics]
atom_pp [Ics]
atom_pp [Prop]
atom_to_icsat_id [Prop]
atom_to_id [Prop]
atom_to_string [Ics]
atomeof [Parser]
atoms_add [Ics]
atoms_empty [Ics]
atoms_singleton [Ics]
atoms_to_list [Ics]
atomtbl [Prop]

B
band [Gmp41.Z]
bcom [Gmp41.Z]
bin_ui [Gmp41.Z]
bin_uiui [Gmp41.Z]
bior [Gmp41.Z]
bit_j [Bitv]
bit_not_j [Bitv]
bitwise [Bitvector]
blit [Bitv]
blit_bits [Bitv]
blit_int [Bitv]
blit_ones [Bitv]
blit_zeros [Bitv]
bool [Pretty]
bpi [Bitv]
bucketlist_length [Hashcons]
build [Bitvector]
build_fun [Bitvector]
bv [Th]
bv_diseq [Context]
bvarith [Th]
bvarith_equal [Context]
bw_and [Bitv]
bw_not [Bitv]
bw_or [Bitv]
bw_xor [Bitv]
bxor [Gmp41.Z]
byName [Apply]
byValue [Apply]

C
c [Context]
c [Partition]
Constraint of a variable.
c_of [Context]
c_of [Partition]
call [Trace]
can [Ics]
can [Istate]
can [Context.Can]
can [Context]
canrepr [V]
Set of canonical representatives with non-trivial equivalence classes.
car [Pair]
cdiv_q [Gmp41.Z]
cdiv_q [Gmp41.Z2]
cdiv_q_2exp [Gmp41.Z]
cdiv_q_ui [Gmp41.Z]
cdiv_qr [Gmp41.Z]
cdiv_qr_ui [Gmp41.Z]
cdiv_r [Gmp41.Z]
cdiv_r [Gmp41.Z2]
cdiv_r_2exp [Gmp41.Z]
cdiv_r_ui [Gmp41.Z]
cdiv_ui [Gmp41.Z]
cdr [Pair]
ceil [Mpa.Q]
changed [C]
channel_stderr [Ics]
channel_stdin [Ics]
channel_stdout [Ics]
choose [V]
clear [Hashcons.S]
clear [Hashcons.Make]
clear [Hashcons]
close_c [Context]
close_d [Context]
close_i [Context]
Propagate changes in the variable partitioning.
close_p [Context]
Propagate changes in the variable partitioning.
close_v [Context]
cmd_batch [Ics]
cmd_endmarker [Ics]
cmd_error [Ics]
cmd_output [Ics]
cmd_quit [Ics]
cmd_rep [Ics]
cmp [Pp]
cmp [Term]
cmp [Sym]
cmp [Var]
cmp [Name]
cmp [Dom]
cmp [Mpa.Q]
cmp [Gmp41.Q]
cmp [Gmp41.Z]
cmp1 [Pp]
cmp_si [Gmp41.Z]
cmp_ui [Gmp41.Q]
cmpl [Term]
cnstrnt [Ics]
cnstrnt [Context.Abstract]
cnstrnt [Context]
cnstrnt [C]
cnstrnt_disjoint [Ics]
cnstrnt_eq [Ics]
cnstrnt_inter [Ics]
cnstrnt_is_empty [Ics]
cnstrnt_is_neg [Ics]
cnstrnt_is_nonneg [Ics]
cnstrnt_is_nonpos [Ics]
cnstrnt_is_pos [Ics]
cnstrnt_mk_neg [Ics]
cnstrnt_mk_nonneg [Ics]
cnstrnt_mk_nonpos [Ics]
cnstrnt_mk_pos [Ics]
cnstrnt_mk_zero [Ics]
cnstrnt_pp [Ics]
cnstrnt_sub [Ics]
cnstrnts [C]
cofactors [Bitvector]
commands [Parser]
commands [Help]
commandseof [Parser]
commandsequence [Parser]
compactify [Context]
compare [Mpa.Q]
compare [Mpa.Z]
compare [Gmp41.Q]
compare [Gmp41.Z]
compare_int [Gmp41.Z]
compare_si [Gmp41.Z]
complement [Sign]
complement [Interval]
complementable [Sign]
compose [Context]
compose [Solution]
conc [Bitvector]
concat [Bitv]
cons [Ics]
cons [Pair]
const [Bitvector]
context_apply [Ics]
context_ctxt_of [Ics]
context_ctxt_pp [Ics]
context_empty [Ics]
context_eq [Ics]
context_find [Ics]
context_inv [Ics]
context_mem [Ics]
context_of [Istate]
context_pp [Ics]
context_solution_of [Ics]
context_use [Ics]
cop [Th]
copy [Context]
Shallow copying.
copy [Partition]
Shallow copy for protecting against destructive updates.
copy [Th.Array]
copy [Bitv]
copy [Gmp41.Z2]
create [Th.Array]
create [Arr]
create [Bitv]
create [Hashcons.S]
create [Hashcons.Make]
create [Hashcons]
create [Gmp41.Q]
create [Gmp41.Z2]
crossmultiply [Context.Can]
crossmultiply1 [Context.Can]
ctxt_of [Istate]
ctxt_of [Context]
current [Istate]
cut [Bitvector]

D
d [Context]
d [Partition]
All disequalities of some variable x.
d [D]
d_add [Arith]
d_bitwise [Bitvector]
d_bvsym [Bitvector]
d_cnstrnt [Fact]
d_conc [Bitvector]
d_consistent [Ics]
d_const [Bitvector]
d_diseq [Fact]
d_disj [Prop]
d_equal [Fact]
d_free [Var]
d_interp [Bitvector]
d_multq [Arith]
d_num [Arith]
d_of [Context]
d_of [Partition]
d_select [Context]
d_singleton [Interval]
d_sub [Bitvector]
d_uninterp [App]
d_update [Context]
debug [Prop]
decompose [Bitvector]
deduce [Context]
Deduce new constraints from an equality
deduce_bvarith [Context]
deduce_la [Context]
deduce_la1 [Context]
deduce_nonlin [Context]
deduce_nonlin2 [Context]
def [Istate]
def [Symtab]
default [Gmp41.RNG]
denominator [Mpa.Q]
denumerator [Pp]
deq [D]
deq_of [D]
destruct [Pp]
destruct [Term]
destructure [Interval]
diseq [Istate]
diseq [Context.Abstract]
diseq [Context.Can]
diseq [Context]
Merging variable equality/disequalities/constraints
diseq [Partition]
Add and propagate disequalities of the form x <> y.
diseq [C]
diseq1 [C]
disjoint [Sign]
disjoint [Dom]
Testing for disjointness.
div [Pp]
div [Sign]
div [Interval]
Division of interverals.
div [Mpa.Q]
div [Gmp41.Q]
divexact [Mpa.Z]
divexact [Gmp41.Z]
divexact [Gmp41.Z2]
dmod [Gmp41.Z]
dmod_ui [Gmp41.Z]
do_at_exit [Ics]
do_at_exit [Tools]
do_at_reset [Tools]
dom [Istate]
dom [Context]
dom [Interval]
dom_of [Var]
drop [Bitvector]
dup [Prop]
dynamic_let [Tools]

E
empty [Symtab]
empty [Context]
empty [Sl]
empty [Solution]
empty [Partition]
Empty partition.
empty [C]
empty [V]
The empty context.
empty [D]
empty [Use]
empty_name [Symtab]
entry_of [Istate]
eot [Istate]
eq [Context.Can]
eq [Context]
Equality test.
eq [Sl]
eq [Solution]
eq [Partition]
Test if states are unchanged.
eq [C]
eq [V]
eq [D]
eq [Atom]
eq [Th]
eq [Euclid.Rat]
eq [Sign]
eq [Term]
eq [Sym]
eq [Var]
eq [Name]
eq [Interval]
eq [Dom]
eq_apply [Sym]
eq_arith [Sym]
eq_arrays [Sym]
eq_bv [Sym]
eq_interp [Sym]
eq_pair [Sym]
eq_pp [Sym]
eql [Term]
eqn [Pretty]
eqs [Solution]
eqs_of [Context]
equal [Context.Abstract]
equal [Context.Can]
equal [Bitv]
equal [Hashcons.HashedType]
equal [Mpa.Q]
equal [Mpa.Z]
equal [Gmp41.Q]
equal [Gmp41.Z]
equal_int [Gmp41.Z]
equal_width_of [Parser]
equality [Context]
Processing an equality over pure terms.
equality [Solution]
equality [V]
equation [Context]
euclid [Euclid.S]
euclid [Euclid.Make]
Given two rational numbers a, b, euclid finds integers , y0 satisfying a * x0 + b * y0 = (a, b), where (a, b) denotes the greatest common divisor of a, b.
euclidean_division [Gmp41.Z]
eval [Apply]
exists [V]
exit [Trace]
expt [Pp]
expt [Sign]
expt [Interval]
Exponentiation of an interval.
expt [Mpa.Q]
expt [Mpa.Z]
ext [V]
Extension of the equivalence class for x.
extend [Context]
extend [Solution]

F
fac_ui [Gmp41.Z]
fdiv_q [Gmp41.Z]
fdiv_q [Gmp41.Z2]
fdiv_q_2exp [Gmp41.Z]
fdiv_q_ui [Gmp41.Z]
fdiv_qr [Gmp41.Z]
fdiv_qr_ui [Gmp41.Z]
fdiv_r [Gmp41.Z]
fdiv_r [Gmp41.Z2]
fdiv_r_2exp [Gmp41.Z]
fdiv_r_ui [Gmp41.Z]
fdiv_ui [Gmp41.Z]
fib_ui [Gmp41.Z]
fill [Bitv]
filter [Symtab]
final_sep [Pretty]
finalize [Prop]
find [Istate]
find [Context]
find [Sl]
find [Solution]
find [V]
find [Use]
find [Hashcons.Make]
find [Hashcons]
findequiv [Context.Can]
float_from [Gmp41.Q]
float_from [Gmp41.Z]
floor [Euclid.Rat]
floor [Mpa.Q]
flush [Ics]
flush [Istate]
fnd [Context.Can]
fold [Context]
fold [Sl]
Fold over the find structure.
fold [Solution]
fold [V]
Starting from the canonical representative x' = find s x, the function f is applied to each y in inv s x' and the results are accumulated.
fold [Pp]
fold [Bitvector]
fold [Coproduct]
fold [Arith]
fold [Term]
Iteration over terms.
fold_left [Th.Array]
fold_left [Bitv]
fold_right [Th.Array]
fold_right [Bitv]
for_all [V]
for_all [Th.Array]
for_all [Term]
for_all2 [Th.Array]
forget [Istate]
fourth_of_quadruple [Ics]
fresh_state_name [Istate]
from_float [Gmp41.Q]
from_float [Gmp41.Z]
from_float [Gmp41.Z2]
from_int [Gmp41.Q]
from_int [Gmp41.Z]
from_int [Gmp41.Z2]
from_ints [Gmp41.Q]
from_si [Gmp41.Q]
from_string [Bitv]
from_string [Gmp41.Z]
from_string_base [Gmp41.Z]
from_string_base [Gmp41.Z2]
from_z [Gmp41.Q]
from_zs [Gmp41.Q]
fst [Ics]
fst_of_quadruple [Ics]
fst_of_triple [Ics]
func [Trace]
fuse [Context]
fuse [Solution]

G
gc [Ics]
gc [Context]
gc [Partition]
Garbage collection.
gc [V]
gcd [Pp]
gcd [Mpa.Z]
gcd [Gmp41.Z]
gcd_ui [Gmp41.Z]
gcdext [Gmp41.Z]
ge [Mpa.Q]
ge [Mpa.Z]
general [Arith]
Compute the general solution of a linear Diophantine equation with coefficients al, the gcd d of al and a particular solution pl.
gentag [Hashcons]
get [Th.Array]
get [Bitv]
get [Trace]
get_context [Istate]
get_den [Gmp41.Q]
get_gmp_compile_version [Gmp41]
get_gmp_runtime_version [Gmp41]
get_num [Gmp41.Q]
gt [Mpa.Q]
gt [Mpa.Z]

H
hamdist [Gmp41.Z]
hash [Term]
hash [Sym]
hash [Var]
hash [Name]
hash [Hashcons.HashedType]
hash [Mpa.Q]
hashcons [Hashcons.S]
hashcons [Hashcons.Make]
hashcons [Hashcons]
head [Ics]
head [Prop]
hi [Interval]
high_mask [Bitv]
hnf [Apply]
ht [Bitvector]

I
icsat_d_atom [Prop]
icsat_d_not [Prop]
icsat_d_var [Prop]
icsat_finalize [Prop]
icsat_get_argument [Prop]
icsat_get_assignment [Prop]
icsat_initialize [Prop]
icsat_is_atom [Prop]
icsat_is_false [Prop]
icsat_is_iff [Prop]
icsat_is_ite [Prop]
icsat_is_not [Prop]
icsat_is_or [Prop]
icsat_is_true [Prop]
icsat_is_var [Prop]
icsat_mk_and [Prop]
icsat_mk_atom [Prop]
icsat_mk_false [Prop]
icsat_mk_iff [Prop]
icsat_mk_implies [Prop]
icsat_mk_ite [Prop]
icsat_mk_not [Prop]
icsat_mk_or [Prop]
icsat_mk_true [Prop]
icsat_mk_var [Prop]
icsat_mk_xor [Prop]
icsat_num_arguments [Prop]
icsat_print_statistics [Prop]
icsat_sat [Prop]
id [Prop]
id_to_atom [Prop]
idtbl [Prop]
inchannel [Istate]
inchannel_of_string [Ics]
inconsistent [Bitvector]
indent [Trace]
infer [Context]
Infer new disequalities from equalities.
infer_bv [Context]
infer_cop [Context]
If x = a, y = b are in the coproduct solution set, and if a and b are diseq in this theory, then deduce x <> y.
infer_la [Context]
If x = q and y = p with q, p numerical constraints, then deduce x <> y.
infix [Pretty]
infixl [Pretty]
init [Ics]
init [Istate]
init [Prop]
init [Bitv]
initial [Prop]
initialize [Istate]
inl [Coproduct]
inr [Coproduct]
insert [Pp]
insert1 [Pp]
inste [Bitvector]
insts [Bitvector]
int_from [Gmp41.Z]
integer_solve [Arith]
inter [Sign]
inter [Interval]
inter [Dom]
inter [Three]
interp [Context]
interp [Th]
ints_of_num [Ics]
inttbl [Prop]
inv [Istate]
inv [Context]
inv [Solution]
inv [V]
inv [Euclid.Rat]
inv [Sign]
inv [Interval]
Inverse of an Interval
inv [Mpa.Q]
inv [Gmp41.Q]
inv_pprod [Context]
inverse [Gmp41.Z]
is_active [Trace]
is_app [Term]
is_bitwise [Bitvector]
is_bvbdd [Bitvector]
is_bvsym [Bitvector]
is_car [Pair]
is_cdr [Pair]
is_complementable [Interval]
is_connected [Prop]
is_connected [Atom]
is_cons [Pair]
is_consistent [Ics]
is_const [Bitvector]
is_const [Term]
is_diophantine [Pp]
is_diophantine [Arith]
is_diseq [Context]
is_diseq [D]
is_diseq [Coproduct]
is_disjoint [Interval]
is_disjoint [Three]
is_empty [Context]
is_empty [Sl]
is_empty [Solution]
is_empty [V]
is_empty [Interval]
is_eps [Bitvector]
is_eq [Context]
is_equal [Istate]
is_equal [Context]
is_equal [Partition]
is_equal [V]
Variable equality modulo s.
is_equal [Term]
is_expt [Pp]
is_false [Boolean]
is_free [Var]
is_fresh [Term]
is_fresh [Var]
is_fresh_bv_var [Bitvector]
is_full [Interval]
is_fully_interp [Th]
is_fully_uninterp [Th]
is_inconsistent [Ics]
is_int [Context]
is_int [Euclid.Rat]
is_integer [Mpa.Q]
is_internal [Term]
is_interp [Bvarith]
is_interp [Pp]
is_interp [Bitvector]
is_interp [Coproduct]
is_interp [Pair]
is_interp [Arith]
is_interp [Term]
is_interp_const [Term]
is_intvar [Term]
is_mult [Pp]
is_multq [Arith]
is_neg [Mpa.Q]
is_negatable [Atom]
is_negone [Mpa.Q]
is_nil [Ics]
is_nil [Prop]
is_none [Ics]
is_num [Arith]
is_one [Pp]
is_one [Bitvector]
is_one [Arith]
is_one [Mpa.Q]
is_perfect_power [Gmp41.Z]
is_perfect_square [Gmp41.Z]
is_pos [Mpa.Q]
is_prime [Gmp41.Z]
is_probab_prime [Gmp41.Z]
is_q [Arith]
is_realvar [Term]
is_redundant [Ics]
is_rename [Term]
is_rename [Var]
is_slack [Term]
is_slack [Var]
is_some [Ics]
is_sub [Interval]
is_sub [Three]
is_true [Boolean]
is_unchanged [Partition]
is_uninterp [App]
is_uninterpreted [Term]
is_var [Term]
is_var [Var]
is_zero [Bitvector]
is_zero [Arith]
is_zero [Mpa.Q]
is_zero [Gmp41.Q]
is_zero [Gmp41.Z]
isolate [Arith]
Isolate y in a solved equality x = a.
iter [V]
iter [Th.Array]
iter [Bitvector]
iter [Term]
iter [Bitv]
iter [Hashcons.S]
iter [Hashcons.Make]
iter [Hashcons]
iteri [Bitv]

J
jacobi [Gmp41.Z]
justification [Solution]

K
k [Var]
keep_highest_bits [Bitv]
keep_lowest_bits [Bitv]
keyword [Lexer]
kronecker_si [Gmp41.Z]

L
la [Th]
lastresult [Parser]
lazy_sigma [App]
lcm [Pp]
lcm [Mpa.Z]
lcm [Gmp41.Z]
le [Mpa.Q]
le [Mpa.Z]
legendre [Gmp41.Z]
length [Prop]
length [Bitv]
levels [Trace]
lex_tables [Lexer]
lift [Apply]
lift [Bitvector]
liftl [Apply]
linenumber [Tools]
list [Pretty]
list' [Pretty]
list_of_vars [Atom]
lo [Interval]
lookup [Symtab]
lookup [Context]
low_mask [Bitv]
lt [Mpa.Q]
lt [Mpa.Z]

M
make [Interval]
map [Th]
map [App]
map [Apply]
map [Sig]
Mapping a term transformer f over a.
map [Bvarith]
map [Arr]
map [Pp]
map [Bitvector]
map [Coproduct]
map [Pair]
Apply term transformer f at uninterpreted positions.
map [Arith]
Mapping a term transformer f over a.
map [Bitv]
map [Pretty]
mapi [Bitv]
mapl [Term]
Mapping over list of terms.
maps [Th]
max [Pp]
max [Term]
max [Mpa.Q]
max [Gmp41.Z]
max_length [Bitv]
mem [Context]
mem [Sl]
mem [Solution]
mem [C]
mem [Use]
mem [Sign]
mem [Interval]
mem [Dom]
mem [Hashcons.S]
mem [Hashcons.Make]
mem [Hashcons]
merge [Partition]
Merge a variable equality.
merge [C]
Propagating a variable equality.
merge [V]
Adding a binding a |-> b to a context s.
merge [D]
merge [Pp]
merge [Bitvector]
merge1 [C]
merge_i [Context]
Processing of an interpreted equality.
merge_v [Context]
Processing of a variable equality.
min [Pp]
min [Term]
min [Mpa.Q]
min [Gmp41.Z]
minus [Mpa.Q]
mk_abs [Apply]
mk_add [Arith]
mk_addl [Arith]
mk_addq [Arith]
mk_app [Term]
mk_apply [Apply]
mk_axiom [Fact]
mk_bitwise [Bitvector]
mk_bwconj [Bitvector]
mk_bwdisj [Bitvector]
mk_bwiff [Bitvector]
mk_bwimp [Bitvector]
mk_bwneg [Bitvector]
mk_car [Pair]
car(cons(a, _)) reduces to a.
mk_cdr [Pair]
cdr(cons(_, b)) reduces to b.
mk_cnstrnt [Fact]
mk_conc [Bitvector]
mk_conc3 [Bitvector]
mk_conj [Prop]
mk_conj [Boolean]
mk_cons [Pair]
cons(car(x), cdr(x)) reduces to x.
mk_const [Bitvector]
mk_const [Term]
mk_create [Arr]
mk_diseq [Atom]
mk_diseq [Fact]
mk_disj [Prop]
mk_disj [Boolean]
mk_div [Sig]
mk_dom [Interval]
mk_empty [Interval]
mk_eps [Bitvector]
mk_equal [Atom]
mk_equal [Fact]
mk_expt [Sig]
mk_expt [Pp]
mk_expt_add [Sig]
mk_expt_arith [Sig]
mk_false [Prop]
mk_false [Atom]
mk_false [Boolean]
mk_free [Var]
mk_fresh [Bitvector]
mk_fresh [Pair]
Fresh variables.
mk_fresh [Arith]
mk_fresh [Term]
mk_fresh [Var]
mk_ge [Atom]
mk_gt [Atom]
mk_iff [Prop]
mk_in [Atom]
mk_incr [Arith]
mk_inj [Sig]
mk_inj [Coproduct]
mk_inl [Coproduct]
mk_inr [Coproduct]
mk_int [Interval]
mk_inv [Sig]
mk_inv [Pp]
mk_ite [Prop]
mk_iterate [Bitvector]
mk_le [Atom]
mk_let [Prop]
mk_lt [Atom]
mk_mult [Sig]
mk_mult [Pp]
mk_mult_add [Sig]
mk_mult_arith [Sig]
mk_mult_with_expt [Pp]
mk_mult_with_pp [Pp]
mk_multl [Sig]
mk_multl [Pp]
mk_multq [Arith]
mk_nat [Interval]
mk_neg [Prop]
mk_neg [Boolean]
mk_neg [Arith]
mk_neg [Interval]
mk_neglit [Prop]
mk_nonneg [Interval]
mk_nonpos [Interval]
mk_num [Arith]
mk_num [Term]
mk_one [Pp]
mk_one [Bitvector]
mk_one [Arith]
mk_one [Interval]
mk_out [Coproduct]
mk_outl [Coproduct]
mk_outr [Coproduct]
mk_pos [Interval]
mk_poslit [Prop]
mk_proj [Pair]
mk_real [Interval]
mk_rename [Term]
mk_rename [Var]
mk_rule [Fact]
mk_select [Arr]
mk_singleton [Interval]
mk_slack [Term]
mk_slack [Var]
mk_sub [Bitvector]
mk_sub [Arith]
mk_true [Prop]
mk_true [Atom]
mk_true [Boolean]
mk_tuple [Pair]
mk_two [Arith]
mk_unsigned [Bvarith]
mk_update [Arr]
mk_var [Prop]
mk_var [Term]
mk_var [Var]
mk_xor [Boolean]
mk_zero [Bitvector]
mk_zero [Arith]
mk_zero [Interval]
mode [Tools]
model [Istate]
model [Context]
modulo [Gmp41.Z]
mono_of [Arith]
monomials [Arith]
msg [Trace]
mul [Gmp41.Q]
mul [Gmp41.Z]
mul [Gmp41.Z2]
mul2exp [Gmp41.Z]
mul_2exp [Gmp41.Z]
mul_ui [Gmp41.Z]
mult [Pp]
mult [Sign]
mult [Interval]
mult [Mpa.Q]
mult [Mpa.Z]
multl [Sign]
multl [Interval]
multq [Arith]
multq [Sign]
multq [Interval]
Multiply by a rational.

N
name [Context]
name [Solution]
name_eq [Ics]
name_of [Term]
name_of [Var]
name_of_nonstrict_slack [Parser]
name_of_strict_slack [Parser]
name_of_string [Ics]
name_to_string [Ics]
names [Th]
neg [Gmp41.Q]
neg [Gmp41.Z]
neg [Gmp41.Z2]
negate [Atom]
negone [Mpa.Q]
nextprime [Gmp41.Z]
nl [Parser]
nl [Istate]
nochange [Partition]
nonlin_equal [Context]
norm [Solution]
normalize [Context]
normalize [Bitv]
nrm [Solution]
num [Arith]
num [Sign]
num_of_int [Ics]
num_of_ints [Ics]
num_of_string [Ics]
num_of_theories [Th]
number [Pretty]
numerator [Pp]
numerator [Mpa.Q]

O
occurs [Prop]
occurs [Solution]
occurs [Atom]
occurs [Bitvector]
occurs [Term]
occurs_as_arg_of_a_cons [Pair]
occurs_as_arg_of_a_proj [Pair]
of_cnstrnt [Fact]
of_diseq [Fact]
of_equal [Fact]
of_float [Gmp41.Z]
of_int [Th]
of_int [Mpa.Q]
of_int [Mpa.Z]
of_int [Gmp41.Z]
of_ints [Mpa.Q]
of_list [Th.Array]
of_list [Pp]
of_mono [Arith]
of_poly [Arith]
of_prop [Prop]
of_q [Sign]
of_q [Dom]
of_string [Th]
of_string [Name]
of_string [Mpa.Q]
of_sym [Th]
of_term [Sign]
of_z [Mpa.Q]
on_help [Help]
one [Euclid.Rat]
one [Mpa.Q]
one [Mpa.Z]
one [Gmp41.Z]
option [Pretty]
orient [Term]
out [Parser]
outchannel [Istate]
outchannel_of_string [Ics]
outl [Coproduct]
output [Result]
output [Gmp41.Q]
output [Gmp41.Z]
outr [Coproduct]

P
p [Th]
p_of [Context]
pair [Ics]
pair [Pretty]
partition [V]
Representation of the equivalence classes as a map with the canonical representatives as domain and the corresponding extensions in the codomain.
perfect_power_p [Gmp41.Z]
perfect_square_p [Gmp41.Z]
poly_of [Arith]
poly_of [Term]
pop [Prop]
popcount [Gmp41.Z]
pos [Bitv]
pow [Mpa.Z]
pow_ui [Gmp41.Z]
pow_ui_ui [Gmp41.Z]
powm [Gmp41.Z]
powm_ui [Gmp41.Z]
pp [Symtab]
pp [Prop.Assignment]
pp [Prop]
pp [Context.Status]
pp [Context]
pp [Sl]
pp [Solution]
pp [Partition]
Pretty-printing
pp [C]
pp [V]
Pretty-printing.
pp [D]
pp [Use]
pp [Atom]
pp [Th]
pp [Fact]
pp [Sign]
pp [Term]
pp [Sym]
pp [Var]
pp [Name]
pp [Interval]
pp [Dom]
pp [Mpa.Q]
pp [Mpa.Z]
pp [Three]
pp_cnstrnt [Fact]
pp_diseq [Fact]
pp_diseq [Term]
pp_entry [Symtab]
pp_equal [Fact]
pp_equal [Term]
pp_map [Name]
pprod [Context.Can]
pprod [Th]
pr [Parser]
pred [Gmp41.Z]
pretty [Term]
pretty [Var]
print [Gmp41.Z]
probab_prime_p [Gmp41.Z]
proc [Trace]
process [Ics]
process [Istate]
process [Context.Process]
profile [Tools]
prop_mk_conj [Ics]
prop_mk_disj [Ics]
prop_mk_false [Ics]
prop_mk_iff [Ics]
prop_mk_ite [Ics]
prop_mk_neg [Ics]
prop_mk_neglit [Ics]
prop_mk_poslit [Ics]
prop_mk_true [Ics]
prop_mk_var [Ics]
prop_sat [Ics]
protect [Context.Process]
push [Prop]

Q
q_initialize [Gmp41.Q]
qsolve [Arith]

R
randinit [Gmp41.RNG]
randinit_lc [Gmp41.RNG]
read_from_channel [Ics]
read_from_string [Ics]
refine [Context]
removable [V]
remove [Istate]
remove [Symtab]
remove [Use]
remove [Trace]
remove [Gmp41.Z]
replace [Context]
replace [Solution]
replace [Arith]
Replacing a variable with a term.
replace_proj [Pair]
reset [Ics]
reset [Istate]
reset [Th.Array]
reset [Trace]
reset_scratch_context [Prop]
resize [Hashcons]
restore [Istate]
restrict [Sl]
restrict [Solution]
restrict [C]
Restrict the map.
restrict [V]
root [Gmp41.Z]
rrandomb [Gmp41.Z]

S
s [Istate]
sat [Istate]
sat [Prop]
save [Istate]
scan0 [Gmp41.Z]
scan1 [Gmp41.Z]
scratch [Prop]
select [Arr]
set [Use]
set [Th.Array]
set [Bitv]
set [Pretty]
set_clause_relevance [Prop]
set_cleanup_period [Prop]
set_inchannel [Istate]
set_num_refinements [Prop]
set_outchannel [Istate]
set_polarity_optimization [Prop]
set_remove_subsumed_clauses [Prop]
set_validate_counter_example [Prop]
set_verbose [Prop]
sgn [Istate]
sgn [Gmp41.Q]
sgn [Gmp41.Z]
shiftl [Bitv]
shiftr [Bitv]
si_kronecker [Gmp41.Z]
sigma [Istate]
sigma [Context]
sigma [Th]
sigma [App]
sigma [Apply]
sigma [Bvarith]
sigma [Arr]
sigma [Pp]
sigma [Bitvector]
sigma [Coproduct]
sigma [Pair]
Canonization.
sigma [Arith]
Interface for sigmatizing arithmetic terms.
sign [Istate]
sign [Context.Can]
sign [Context]
sleep [Ics]
snd [Ics]
snd_of_quadruple [Ics]
snd_of_triple [Ics]
solution [Istate]
solution [Pretty]
solution_to_list [Ics]
solve [Istate]
solve [Th]
solve [Bitvector]
solve [Coproduct]
solve [Pair]
Solving tuples.
solve [Arith]
solve [Euclid.S]
solve [Euclid.Make]
Solving a linear diophantine equation with nonzero, rational coefficients ci, for i = 1,...,n with n >= 1: c0*x_0 + \ldots c_n * xn = b The algorithm proceeds by recursion on n.
solve1 [Coproduct]
solve1 [Pair]
solve_bitwise [Bitvector]
solve_sub_sub [Bitvector]
solvel [Bitvector]
solvel [Coproduct]
solvel [Pair]
solvers [Th]
solvevar [Coproduct]
split [Ics]
split [Istate]
split [Context]
split [Pp]
split_arrays [Context]
split_cnstrnt [Context]
sprintf [Gmp41.Q]
sprintf [Gmp41.Z]
sqrt [Gmp41.Z]
sqrtrem [Gmp41.Z]
stack [Prop]
stack_reset [Prop]
stackpp [Prop]
stat [Hashcons.S]
stat [Hashcons.Make]
stat [Hashcons]
state [Symtab]
statistics [Prop]
status [Interval]
string [Pretty]
string_from [Gmp41.Z]
string_of_num [Ics]
sub [Bitvector]
sub [Sign]
sub [Interval]
Subtraction of intervals
sub [Dom]
Testing for subdomains.
sub [Bitv]
sub [Mpa.Q]
sub [Mpa.Z]
sub [Gmp41.Q]
sub [Gmp41.Z]
sub [Gmp41.Z2]
sub_ui [Gmp41.Z]
subst [Apply]
subst1 [Coproduct]
subst1 [Pair]
substl [Apply]
substl [Coproduct]
substl [Pair]
subterm [Term]
succ [Mpa.Z]
succ [Gmp41.Z]
sym_cmp [Ics]
sym_d_apply [Ics]
sym_d_bv_bitwise [Ics]
sym_d_bv_conc [Ics]
sym_d_bv_sub [Ics]
sym_d_expt [Ics]
sym_d_multq [Ics]
sym_d_num [Ics]
sym_d_uninterp [Ics]
sym_eq [Ics]
sym_is_abs [Ics]
sym_is_add [Ics]
sym_is_apply [Ics]
sym_is_bv_bitwise [Ics]
sym_is_bv_conc [Ics]
sym_is_bv_const [Ics]
sym_is_bv_sub [Ics]
sym_is_car [Ics]
sym_is_cdr [Ics]
sym_is_cons [Ics]
sym_is_expt [Ics]
sym_is_inl [Ics]
sym_is_inr [Ics]
sym_is_mult [Ics]
sym_is_multq [Ics]
sym_is_num [Ics]
sym_is_outl [Ics]
sym_is_outr [Ics]
sym_is_select [Ics]
sym_is_uninterp [Ics]
sym_is_unsigned [Ics]
sym_is_update [Ics]
sym_mk_abs [Ics]
sym_mk_add [Ics]
sym_mk_apply [Ics]
sym_mk_bv_bitwise [Ics]
sym_mk_bv_conc [Ics]
sym_mk_bv_const [Ics]
sym_mk_bv_sub [Ics]
sym_mk_car [Ics]
sym_mk_cdr [Ics]
sym_mk_cons [Ics]
sym_mk_expt [Ics]
sym_mk_inl [Ics]
sym_mk_inr [Ics]
sym_mk_mult [Ics]
sym_mk_multq [Ics]
sym_mk_num [Ics]
sym_mk_outl [Ics]
sym_mk_outr [Ics]
sym_mk_select [Ics]
sym_mk_unsigned [Ics]
sym_mk_update [Ics]
sym_of [Term]
sym_theory_of [Ics]
symtab [Istate]
syntax [Help]

T
tail [Ics]
tail [Prop]
tau [Arith]
Domain interpretation.
tdiv_q [Gmp41.Z]
tdiv_q [Gmp41.Z2]
tdiv_q_2exp [Gmp41.Z]
tdiv_q_ui [Gmp41.Z]
tdiv_qr [Gmp41.Z]
tdiv_qr_ui [Gmp41.Z]
tdiv_r [Gmp41.Z]
tdiv_r [Gmp41.Z2]
tdiv_r_2exp [Gmp41.Z]
tdiv_r_ui [Gmp41.Z]
tdiv_ui [Gmp41.Z]
term [Context.Abstract]
term [Context.Can]
term_cmp [Ics]
term_eq [Ics]
term_input [Ics]
term_is_arith [Ics]
term_is_false [Ics]
term_is_true [Ics]
term_mk_add [Ics]
term_mk_addl [Ics]
term_mk_apply [Ics]
term_mk_bvconc [Ics]
term_mk_bvconst [Ics]
term_mk_bvsub [Ics]
term_mk_bwand [Ics]
term_mk_bwite [Ics]
term_mk_bwnot [Ics]
term_mk_bwor [Ics]
term_mk_div [Ics]
term_mk_expt [Ics]
term_mk_false [Ics]
term_mk_inj [Ics]
term_mk_mult [Ics]
term_mk_multl [Ics]
term_mk_multq [Ics]
term_mk_num [Ics]
term_mk_out [Ics]
term_mk_proj [Ics]
term_mk_select [Ics]
term_mk_sub [Ics]
term_mk_true [Ics]
term_mk_tuple [Ics]
term_mk_unary_minus [Ics]
term_mk_uninterp [Ics]
term_mk_unsigned [Ics]
term_mk_update [Ics]
term_mk_var [Ics]
term_of_string [Ics]
term_output [Ics]
term_pp [Ics]
term_to_string [Ics]
termeof [Parser]
terms_of_list [Ics]
terms_to_list [Ics]
th_of_string [Ics]
th_to_string [Ics]
third_of_quadruple [Ics]
third_of_triple [Ics]
timers [Tools]
to_float [Gmp41.Q]
to_float [Gmp41.Z]
to_int [Th]
to_int [Gmp41.Z]
to_list [Sl]
Solution set
to_list [Solution]
to_list [C]
to_list [D]
to_list [Use]
to_list [Pp]
Normalize a power product to a list.
to_prop [Prop]
to_stderr [Pretty]
to_stdout [Pretty]
to_string [Th]
to_string [Term]
to_string [Name]
to_string [Bitv]
to_string [Pretty]
to_string [Mpa.Q]
to_string [Mpa.Z]
to_string [Gmp41.Q]
to_string [Gmp41.Z]
to_string_base [Gmp41.Z]
to_var [Term]
to_z [Mpa.Q]
token [Lexer]
top [Prop]
topvar [Bitvector]
trace_add [Ics]
trace_get [Ics]
trace_remove [Ics]
trace_reset [Ics]
triple [Ics]
triple [Pretty]
tt [Context]
tuple [Pretty]
two [Mpa.Q]
two [Mpa.Z]
typ [Istate]
typ [Symtab]
type_of [Istate]

U
u [Th]
ui_pow_ui [Gmp41.Z]
union [Solution]
union [V]
union [Dom]
Union of two domains
union [Three]
unit [Pretty]
unsafe_blit [Bitv]
unsafe_get [Bitv]
unsafe_set [Bitv]
unsat [Istate]
unsigned [Context.Can]
unsigned [Bvarith]
unsigned_interp_of [Bvarith]
update [Context]
Destructive updates.
update [Sl]
update [Solution]
update [C]
update [Arr]
update_c [Partition]
update_d [Partition]
update_v [Partition]
upper_of [Context]
urandomb [Gmp41.Z]
urandomm [Gmp41.Z]
use [Istate]
use [Context]
use [Solution]
utime [Tools]

V
v [Context]
v [Partition]
Canonical variables module s.
v_of [Context]
v_of [Partition]
valid [Istate]
value_of [Ics]
var_cmp [Ics]
var_d_bound [Ics]
var_eq [Ics]
var_is_bound [Ics]
var_is_external [Ics]
var_mk_bound [Ics]
var_mk_external [Ics]
var_name_of [Ics]
var_to_icsat_id [Prop]
vars_of [Atom]
vars_of [Term]
Set of variables.
vartbl [Prop]
vectorize [Arith]

W
whitespace [Trace]
width [Bitvector]
width [Sym]
Width of bitvector function symbols.
width_bv [Sym]
width_of [Istate]

Y
yyact [Parser]
yycheck [Parser]
yydefred [Parser]
yydgoto [Parser]
yygindex [Parser]
yylen [Parser]
yylhs [Parser]
yynames_block [Parser]
yynames_const [Parser]
yyrindex [Parser]
yysindex [Parser]
yytable [Parser]
yytables [Parser]
yytablesize [Parser]
yytransl_block [Parser]
yytransl_const [Parser]

Z
z_initialize [Gmp41.Z2]
zero [Euclid.Rat]
zero [Mpa.Q]
zero [Mpa.Z]
zero [Gmp41.Q]
zero [Gmp41.Z]
zsolve [Arith]