From e2ebc1fb2abd850b22c3b001aa1785c7a95b242a Mon Sep 17 00:00:00 2001
From: hra687261 <hichem.ait-el-hara@ocamlpro.com>
Date: Tue, 18 Oct 2022 09:25:52 +0200
Subject: [PATCH] [Array] Added builtin op
---
colibri2/theories/array/array.ml | 42 +++++++++++++++++++++++---------
1 file changed, 31 insertions(+), 11 deletions(-)
diff --git a/colibri2/theories/array/array.ml b/colibri2/theories/array/array.ml
index 55457fbb6..3b8b62379 100644
--- a/colibri2/theories/array/array.ml
+++ b/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] *)
--
GitLab