|
(%!) [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] |
|