[Array] Added builtin op

colibri2/theories/array/array.ml

@@ -30,16 +30,40 @@ let convert ~subst =
   Colibri2_theories_quantifiers.Subst.convert ~subst_old:Ground.Subst.empty
     ~subst_new:subst
 
+let int_ty = Expr.Ty.int
+let array_ty = Expr.Ty.array int_ty int_ty
+
+(* Builtins *)
+module Builtin = struct
+  type _ Expr.t += Arr_diff
+
+  let arr_diff : Dolmen_std.Expr.term_cst =
+    Expr.Id.mk ~name:"arr_diff" ~builtin:Arr_diff
+      (Dolmen_std.Path.global "arr_diff")
+      (Expr.Ty.arrow [ array_ty; array_ty ] int_ty)
+
+  let () =
+    let app2 env s f =
+      `Term
+        (Dolmen_type.Base.term_app2
+           (module Dolmen_loop.Typer.T)
+           env s
+           (fun a b -> Expr.Term.apply_cst f [] [ a; b ]))
+    in
+    Expr.add_builtins (fun env s ->
+        match s with
+        | Dolmen_loop.Typer.T.Id { ns = Term; name = Simple "arr_diff" } ->
+            app2 env s arr_diff
+        | _ -> `Not_found)
+end
+
 (* Generalized, Efficient Array Decision Procedures. de Moura, Bjorner *)
 module Theory = struct
   open Colibri2_theories_quantifiers
 
   let term_of_var = Expr.Term.of_var
-  let mk_int_var name = Expr.Term.Var.mk name Expr.Ty.int
-
-  let mk_array_var name =
-    Expr.Term.Var.mk name (Expr.Ty.array Expr.Ty.int Expr.Ty.int)
-
+  let mk_int_var name = Expr.Term.Var.mk name int_ty
+  let mk_array_var name = Expr.Term.Var.mk name array_ty
   let vi = mk_int_var "i"
   let vj = mk_int_var "j"
   let vk = mk_int_var "k"
@@ -59,12 +83,8 @@ module Theory = struct
     Expr.Term._or
       [
         Expr.Term.eq ta tb;
-        (let kab_v = Expr.Term.Var.mk "k_a_b" Expr.Ty.int in
-         let kab_t = Expr.Term.of_var kab_v in
-         Expr.Term.ex ([], [ kab_v ])
-         @@ Expr.Term.neq
-              (Expr.Term.select ta kab_t)
-              (Expr.Term.select tb kab_t));
+        (let diff = Expr.Term.apply_cst Builtin.arr_diff [] [ ta; tb ] in
+         Expr.Term.neq (Expr.Term.select ta diff) (Expr.Term.select tb diff));
       ]
 
   (* ⇓: a ≡ b[i <- v], a[j] |> (i = j) \/ a[j] = b[j] *)