1 files changed, 30 insertions, 0 deletions
diff --git a/lib/smt.sail b/lib/smt.sail
new file mode 100644
index 00000000..702b82c6
--- /dev/null
+++ b/lib/smt.sail
@@ -0,0 +1,30 @@
+$ifndef _SMT
+$define _SMT
+
+// see http://smtlib.cs.uiowa.edu/theories-Ints.shtml
+
+val div = {
+  smt: "div",
+  ocaml: "quotient",
+  lem: "integerDiv"
+} : forall 'n 'm. (atom('n), atom('m)) -> {'o, 'o = div('n, 'm). atom('o)}
+
+val mod = {
+  smt: "mod",
+  ocaml: "modulus",
+  lem: "integerMod"
+} : forall 'n 'm. (atom('n), atom('m)) -> {'o, 'o = mod('n, 'm). atom('o)}
+
+val abs = {
+  smt : "abs",
+  ocaml: "abs_int",
+  lem: "abs_int"
+} : forall 'n. atom('n) -> {'o, 'o = abs('n). atom('o)}
+
+$ifdef TEST
+
+let __smt_x : atom(div(4, 2)) = div(8, 4)
+
+$endif
+
+$endif