1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
|
$ifndef _SMT
$define _SMT
// see http://smtlib.cs.uiowa.edu/theories-Ints.shtml
/*! Euclidean division */
val ediv_int = {
ocaml: "quotient",
interpreter: "quotient",
lem: "integerDiv",
c: "ediv_int",
coq: "ediv_with_eq"
} : forall 'n 'm. (int('n), int('m)) -> int(div('n, 'm))
val emod_int = {
ocaml: "modulus",
interpreter: "modulus",
lem: "integerMod",
c: "emod_int",
coq: "emod_with_eq"
} : forall 'n 'm. (int('n), int('m)) -> int(mod('n, 'm))
val abs_int_atom = {
ocaml: "abs_int",
interpreter: "abs_int",
lem: "integerAbs",
c: "abs_int",
coq: "abs_with_eq"
} : forall 'n. int('n) -> int(abs('n))
overload abs_int = {abs_int_atom}
$ifdef TEST
let __smt_x : int(div(4, 2)) = div(8, 4)
$endif
$endif
|
