[Array] DiffGraph and foreign_dom inetroperation

In addition, added interface files and headers

Makefile

@@ -106,7 +106,9 @@ WITAN_FILES = colibri2/stdlib/std.ml colibri2/stdlib/std.mli		\
 	colibri2/stdlib/keys_sig.ml colibri2/stdlib/comp_keys.ml	\
 	colibri2/stdlib/comp_keys.mli colibri2/bin/options.ml
 
-OCAMLPRO_FILES = $(filter-out colibri2/theories/array/dune, $(wildcard colibri2/theories/array/*))
+OCAMLPRO_FILES = \
+	$(filter-out colibri2/theories/array/dune colibri2/theories/nseq/dune, \
+		$(wildcard colibri2/theories/array/* colibri2/theories/nseq/*))
 
 
 COLIBRI2_FILES = Makefile $(filter-out $(WHY3_FILES) $(OCAML_FILES)	\

colibri2/tests/solve/smt_array/errors/ite_1.txt

+(set-logic QF_AX)
+(declare-sort I 0)
+(declare-sort E 0)
+(declare-fun i () I)
+(declare-fun a () (Array I E))
+(declare-fun j () I)
+(declare-fun v1 () E)
+(declare-fun v2 () E)
+(assert (not
+  (ite
+    (= (store a j v1) (store (store a i v2) j v1))
+    (= i j)
+    true
+  )))
+(check-sat)
\ No newline at end of file

colibri2/tests/solve/smt_array/errors/ite_2.txt

+(set-logic ALL)
+(declare-fun i () Int)
+(declare-fun a () (Array Int Int))
+(declare-fun j () Int)
+(declare-fun v1 () Int)
+(declare-fun v2 () Int)
+(assert (not
+  (ite
+    (= (store a j v1) (store (store a i v2) j v1))
+    (= i j)
+    true
+  )))
+(check-sat)
\ No newline at end of file

colibri2/tests/solve/smt_array/errors/notes.txt

+
+- eq.txt: timeout
+- ite_1.txt: unsound (--array-res-ext)
+- ite_2.txt: timeout (--array-res-ext)

colibri2/theories/LRA/LRA_build.mli

+(*************************************************************************)
+(*  This file is part of Colibri2.                                       *)
+(*                                                                       *)
+(*  Copyright (C) 2014-2021                                              *)
+(*    CEA   (Commissariat à l'énergie atomique et aux énergies           *)
+(*           alternatives)                                               *)
+(*                                                                       *)
+(*  you can redistribute it and/or modify it under the terms of the GNU  *)
+(*  Lesser General Public License as published by the Free Software      *)
+(*  Foundation, version 2.1.                                             *)
+(*                                                                       *)
+(*  It is distributed in the hope that it will be useful,                *)
+(*  but WITHOUT ANY WARRANTY; without even the implied warranty of       *)
+(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the        *)
+(*  GNU Lesser General Public License for more details.                  *)
+(*                                                                       *)
+(*  See the GNU Lesser General Public License version 2.1                *)
+(*  for more details (enclosed in the file licenses/LGPLv2.1).           *)
+(*************************************************************************)
+
 module LastEffort : sig
   val add' : _ Egraph.t -> A.t -> Node.t -> A.t -> Node.t -> Node.t
   val add : _ Egraph.t -> Node.t -> Node.t -> Node.t

colibri2/theories/array/DiffGraph.ml

+(*************************************************************************)
+(*  This file is part of Colibri2.                                       *)
+(*                                                                       *)
+(*  Copyright (C) 2014-2021                                              *)
+(*    CEA   (Commissariat à l'énergie atomique et aux énergies           *)
+(*           alternatives)                                               *)
+(*    OCamlPro                                                           *)
+(*                                                                       *)
+(*  you can redistribute it and/or modify it under the terms of the GNU  *)
+(*  Lesser General Public License as published by the Free Software      *)
+(*  Foundation, version 2.1.                                             *)
+(*                                                                       *)
+(*  It is distributed in the hope that it will be useful,                *)
+(*  but WITHOUT ANY WARRANTY; without even the implied warranty of       *)
+(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the        *)
+(*  GNU Lesser General Public License for more details.                  *)
+(*                                                                       *)
+(*  See the GNU Lesser General Public License version 2.1                *)
+(*  for more details (enclosed in the file licenses/LGPLv2.1).           *)
+(*************************************************************************)
+
 open Colibri2_core
 open Colibri2_popop_lib
 open Popop_stdlib
+open Common
 
 module NP = struct
   module T = struct
@@ -28,4 +50,50 @@ module DG = struct
   let remove (env : Egraph.wt) = HT.remove diff_graph env
 end
 
+let mk_np id node = { id; node }
 let get_neighbours env a = DG.find env a
+
+let rm_edge env { id; node } rnp k =
+  Debug.dprintf6 debug "DiffGraph: Removing the edge %a linking %a to %a"
+    Node.pp k Node.pp node Node.pp rnp.node;
+  DG.change env id ~f:(function
+    | None ->
+        failwith
+          (Fmt.str
+             "%a is supposed to be a neighbour of %a, it's neighbour map \
+              mustn't be empty"
+             Node.pp node Node.pp rnp.node)
+    | Some m -> (
+        match NP.M.find_opt rnp m with
+        | None ->
+            failwith
+              (Fmt.str "There is no edge from %a to the node %a." Node.pp node
+                 Node.pp rnp.node)
+        | Some k' ->
+            assert (Egraph.is_equal env k k');
+            Some (NP.M.remove rnp m)))
+
+let add_neighbour env src dest k ind_ty =
+  Debug.dprintf6 debug "DiffGraph: adding %a as a neighbour to %a through %a"
+    Node.pp dest.node Node.pp src.node Node.pp k;
+  DG.change env src.id ~f:(function
+    | None -> Some (NP.M.singleton dest k)
+    | Some m -> (
+        match NP.M.find_opt dest m with
+        | Some k' ->
+            if Egraph.is_equal env k k' then Some m
+            else
+              (* if a and b are already neighbours and k and k' are not equal
+                 then set (k = k') to true *)
+              let eqn = sem_to_node (mk_eq env k k' ind_ty) in
+              Egraph.register env eqn;
+              Boolean.set_true env eqn;
+              Some m
+        | None -> Some (NP.M.add dest k m)))
+
+let add_edge env a b k =
+  Debug.dprintf6 debug "DiffGraph: adding the edge %a between %a and %a" Node.pp
+    k Node.pp a.node Node.pp b.node;
+  let ind_ty, _ = array_gty_args (get_node_ty env a.node) in
+  add_neighbour env a b k ind_ty;
+  add_neighbour env b a k ind_ty

colibri2/theories/array/DiffGraph.mli

+(*************************************************************************)
+(*  This file is part of Colibri2.                                       *)
+(*                                                                       *)
+(*  Copyright (C) 2014-2021                                              *)
+(*    CEA   (Commissariat à l'énergie atomique et aux énergies           *)
+(*           alternatives)                                               *)
+(*    OCamlPro                                                           *)
+(*                                                                       *)
+(*  you can redistribute it and/or modify it under the terms of the GNU  *)
+(*  Lesser General Public License as published by the Free Software      *)
+(*  Foundation, version 2.1.                                             *)
+(*                                                                       *)
+(*  It is distributed in the hope that it will be useful,                *)
+(*  but WITHOUT ANY WARRANTY; without even the implied warranty of       *)
+(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the        *)
+(*  GNU Lesser General Public License for more details.                  *)
+(*                                                                       *)
+(*  See the GNU Lesser General Public License version 2.1                *)
+(*  for more details (enclosed in the file licenses/LGPLv2.1).           *)
+(*************************************************************************)
+
+include sig
+  module T : sig
+    type t = { id : int; node : Node.t }
+  end
+
+  module M : Colibri2_popop_lib.Map_intf.PMap with type key = T.t
+end
+
+type t = T.t = { id : int; node : Node.t }
+
+module DG : sig
+  module HT : sig
+    type 'a t = 'a Datastructure.Hashtbl(Colibri2_popop_lib.Popop_stdlib.DInt).t
+  end
+
+  val diff_graph : Node.t M.t HT.t
+  val find : Egraph.wt -> int -> Node.t M.t option
+
+  val change :
+    f:(Node.t M.t option -> Node.t M.t option) -> 'a Egraph.t -> int -> unit
+
+  val remove : Egraph.wt -> int -> unit
+end
+
+val mk_np : int -> Node.t -> t
+val get_neighbours : Egraph.wt -> int -> Node.t M.t option
+val rm_edge : 'a Egraph.t -> t -> t -> Node.t -> unit
+val add_edge : Egraph.wt -> t -> t -> Node.t -> unit

colibri2/theories/array/GE_Array_DP.mli

+(*************************************************************************)
+(*  This file is part of Colibri2.                                       *)
+(*                                                                       *)
+(*  Copyright (C) 2014-2021                                              *)
+(*    CEA   (Commissariat à l'énergie atomique et aux énergies           *)
+(*           alternatives)                                               *)
+(*    OCamlPro                                                           *)
+(*                                                                       *)
+(*  you can redistribute it and/or modify it under the terms of the GNU  *)
+(*  Lesser General Public License as published by the Free Software      *)
+(*  Foundation, version 2.1.                                             *)
+(*                                                                       *)
+(*  It is distributed in the hope that it will be useful,                *)
+(*  but WITHOUT ANY WARRANTY; without even the implied warranty of       *)
+(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the        *)
+(*  GNU Lesser General Public License for more details.                  *)
+(*                                                                       *)
+(*  See the GNU Lesser General Public License version 2.1                *)
+(*  for more details (enclosed in the file licenses/LGPLv2.1).           *)
+(*************************************************************************)
+
+val init : Egraph.wt -> unit
+val converter : Egraph.wt -> Ground.t -> unit

colibri2/theories/array/SharingIsCaring.ml

+(*************************************************************************)
+(*  This file is part of Colibri2.                                       *)
+(*                                                                       *)
+(*  Copyright (C) 2014-2021                                              *)
+(*    CEA   (Commissariat à l'énergie atomique et aux énergies           *)
+(*           alternatives)                                               *)
+(*    OCamlPro                                                           *)
+(*                                                                       *)
+(*  you can redistribute it and/or modify it under the terms of the GNU  *)
+(*  Lesser General Public License as published by the Free Software      *)
+(*  Foundation, version 2.1.                                             *)
+(*                                                                       *)
+(*  It is distributed in the hope that it will be useful,                *)
+(*  but WITHOUT ANY WARRANTY; without even the implied warranty of       *)
+(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the        *)
+(*  GNU Lesser General Public License for more details.                  *)
+(*                                                                       *)
+(*  See the GNU Lesser General Public License version 2.1                *)
+(*  for more details (enclosed in the file licenses/LGPLv2.1).           *)
+(*************************************************************************)
+
 open Colibri2_core
 open Colibri2_popop_lib
 open Common
 open DiffGraph
 
-let use_diff_graph =
-  Options.register ~pp:Fmt.bool "Array.diff-graph"
-    Cmdliner.Arg.(
-      value & flag
-      & info [ "array-diff-graph" ] ~doc:"Use the array's diff graph")
-
-let rm_edge env { id; node } rnp k =
-  Debug.dprintf6 debug "DiffGraph: Removing the edge %a linking %a to %a"
-    Node.pp k Node.pp node Node.pp rnp.node;
-  DG.change env id ~f:(function
-    | None ->
-        failwith
-          (Fmt.str
-             "%a is supposed to be a neighbour of %a, it's neighbour map \
-              mustn't be empty"
-             Node.pp node Node.pp rnp.node)
-    | Some m -> (
-        match NP.M.find_opt rnp m with
-        | None ->
-            failwith
-              (Fmt.str "There is no edge from %a to the node %a." Node.pp node
-                 Node.pp rnp.node)
-        | Some k' ->
-            assert (Egraph.is_equal env k k');
-            Some (NP.M.remove rnp m)))
-
-let add_neighbour env src dest k ind_ty =
-  Debug.dprintf6 debug "DiffGraph: adding %a as a neighbour to %a through %a"
-    Node.pp dest.node Node.pp src.node Node.pp k;
-  DG.change env src.id ~f:(function
-    | None -> Some (NP.M.singleton dest k)
-    | Some m -> (
-        match NP.M.find_opt dest m with
-        | Some k' ->
-            if Egraph.is_equal env k k' then Some m
-            else
-              (* if a and b are already neighbours and k and k' are not equal
-                 then set (k = k') to true *)
-              let eqn = sem_to_node (mk_eq env k k' ind_ty) in
-              Egraph.register env eqn;
-              Boolean.set_true env eqn;
-              Some m
-        | None -> Some (NP.M.add dest k m)))
-
-(** if (a = b[k <- _]) then the edge a--k--b is added to the graph.  *)
-let add_edge env a b k =
-  Debug.dprintf6 debug "DiffGraph: adding the edge %a between %a and %a" Node.pp
-    k Node.pp a.node Node.pp b.node;
-  let ind_ty, _ = array_gty_args (get_node_ty env a.node) in
-  add_neighbour env a b k ind_ty;
-  add_neighbour env b a k ind_ty
-
-let neighbours_union env knp rnp { id; node } kk_opt kr_opt acc =
+let merge_node_neighbours env knp rnp { id; node } kk_opt kr_opt acc =
   match (kk_opt, kr_opt) with
   | Some k1, Some k2 ->
       (* if a node X is a neighbour of both A and B through the edges
@@ -67,12 +36,12 @@ let neighbours_union env knp rnp { id; node } kk_opt kr_opt acc =
         Egraph.register env eqn;
         Boolean.set_true env eqn);
       rm_edge env { id; node } rnp k2;
-      NP.M.add knp k1 acc
-  | Some k, None -> NP.M.add knp k acc
+      M.add knp k1 acc
+  | Some k, None -> M.add knp k acc
   | None, Some k ->
       rm_edge env { id; node } rnp k;
       add_edge env { id; node } knp k;
-      NP.M.add knp k acc
+      M.add knp k acc
   | None, None ->
       failwith
         (Fmt.str
@@ -97,7 +66,7 @@ let eq_arrays_norm env (a : t) (b : t) =
   in
   (* iterate over all the neighbours *)
   let abns =
-    NP.M.fold2_union (neighbours_union env knp rnp) knm rnm NP.M.empty
+    M.fold2_union (merge_node_neighbours env knp rnp) knm rnm M.empty
   in
   DG.remove env rnp.id;
   DG.change env knp.id ~f:(function

colibri2/theories/array/SharingIsCaring.mli

+(*************************************************************************)
+(*  This file is part of Colibri2.                                       *)
+(*                                                                       *)
+(*  Copyright (C) 2014-2021                                              *)
+(*    CEA   (Commissariat à l'énergie atomique et aux énergies           *)
+(*           alternatives)                                               *)
+(*    OCamlPro                                                           *)
+(*                                                                       *)
+(*  you can redistribute it and/or modify it under the terms of the GNU  *)
+(*  Lesser General Public License as published by the Free Software      *)
+(*  Foundation, version 2.1.                                             *)
+(*                                                                       *)
+(*  It is distributed in the hope that it will be useful,                *)
+(*  but WITHOUT ANY WARRANTY; without even the implied warranty of       *)
+(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the        *)
+(*  GNU Lesser General Public License for more details.                  *)
+(*                                                                       *)
+(*  See the GNU Lesser General Public License version 2.1                *)
+(*  for more details (enclosed in the file licenses/LGPLv2.1).           *)
+(*************************************************************************)
+
+val init : Egraph.wt -> unit
+val converter : Egraph.wt -> Ground.t -> unit

colibri2/theories/array/common.ml

+(*************************************************************************)
+(*  This file is part of Colibri2.                                       *)
+(*                                                                       *)
+(*  Copyright (C) 2014-2021                                              *)
+(*    CEA   (Commissariat à l'énergie atomique et aux énergies           *)
+(*           alternatives)                                               *)
+(*    OCamlPro                                                           *)
+(*                                                                       *)
+(*  you can redistribute it and/or modify it under the terms of the GNU  *)
+(*  Lesser General Public License as published by the Free Software      *)
+(*  Foundation, version 2.1.                                             *)
+(*                                                                       *)
+(*  It is distributed in the hope that it will be useful,                *)
+(*  but WITHOUT ANY WARRANTY; without even the implied warranty of       *)
+(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the        *)
+(*  GNU Lesser General Public License for more details.                  *)
+(*                                                                       *)
+(*  See the GNU Lesser General Public License version 2.1                *)
+(*  for more details (enclosed in the file licenses/LGPLv2.1).           *)
+(*************************************************************************)
+
 open Colibri2_core
 open Colibri2_popop_lib
 open Popop_stdlib
-module NHT = Datastructure.Hashtbl (Node)
-module IHT = Datastructure.Hashtbl (DInt)
-module GHT = Datastructure.Hashtbl (Ground)
-module GTHT = Datastructure.Hashtbl (Ground.Ty)
 
+let use_diff_graph =
+  Options.register ~pp:Fmt.bool "Array.diff-graph"
+    Cmdliner.Arg.(
+      value & flag
+      & info [ "array-diff-graph" ] ~doc:"Use the array's diff graph")
 
 let debug =
   Debug.register_info_flag ~desc:"Debugging messages of the array theory"
@@ -15,22 +37,41 @@ let convert ~subst =
   Colibri2_theories_quantifiers.Subst.convert ~subst_old:Ground.Subst.empty
     ~subst_new:subst
 
-let ind_ty_var = Expr.Ty.Var.mk "ind_ty"
-let val_ty_var = Expr.Ty.Var.mk "val_ty"
-let alpha_ty_var = Expr.Ty.Var.mk "alpha"
-let a_ty_var = Expr.Ty.Var.mk "a"
-let b_ty_var = Expr.Ty.Var.mk "b"
-let c_ty_var = Expr.Ty.Var.mk "c"
-let ind_ty = Expr.Ty.of_var ind_ty_var
-let val_ty = Expr.Ty.of_var val_ty_var
-let a_ty = Expr.Ty.of_var a_ty_var
-let b_ty = Expr.Ty.of_var b_ty_var
-let c_ty = Expr.Ty.of_var c_ty_var
-let alpha_ty = Expr.Ty.of_var alpha_ty_var
-let array_ty = Expr.Ty.array ind_ty val_ty
-let array_ty_ab = Expr.Ty.array a_ty b_ty
-let array_ty_ac = Expr.Ty.array a_ty c_ty
-let array_ty_alpha = Expr.Ty.array ind_ty alpha_ty
+module STV = struct
+  let ind_ty_var = Expr.Ty.Var.mk "ind_ty"
+  let val_ty_var = Expr.Ty.Var.mk "val_ty"
+  let alpha_ty_var = Expr.Ty.Var.mk "alpha"
+  let a_ty_var = Expr.Ty.Var.mk "a"
+  let b_ty_var = Expr.Ty.Var.mk "b"
+  let c_ty_var = Expr.Ty.Var.mk "c"
+  let ind_ty = Expr.Ty.of_var ind_ty_var
+  let val_ty = Expr.Ty.of_var val_ty_var
+  let a_ty = Expr.Ty.of_var a_ty_var
+  let b_ty = Expr.Ty.of_var b_ty_var
+  let c_ty = Expr.Ty.of_var c_ty_var
+  let alpha_ty = Expr.Ty.of_var alpha_ty_var
+  let array_ty = Expr.Ty.array ind_ty val_ty
+  let array_ty_ab = Expr.Ty.array a_ty b_ty
+  let array_ty_ac = Expr.Ty.array a_ty c_ty
+  let array_ty_alpha = Expr.Ty.array ind_ty alpha_ty
+  let term_of_var = Expr.Term.of_var
+  let mk_index_var name = Expr.Term.Var.mk name ind_ty
+  let mk_value_var name = Expr.Term.Var.mk name val_ty
+  let mk_array_var name = Expr.Term.Var.mk name array_ty
+  let vi = mk_index_var "i"
+  let vj = mk_index_var "j"
+  let vk = mk_index_var "k"
+  let vv = mk_value_var "v"
+  let ti = term_of_var vi
+  let tj = term_of_var vj
+  let tk = term_of_var vk
+  let tv = term_of_var vv
+  let va = mk_array_var "a"
+  let vb = mk_array_var "b"
+  let ta = term_of_var va
+  let tb = term_of_var vb
+end
+
 let replicate n v = List.init n (fun _ -> v)
 let mk_store_term = Expr.Term.Array.store
 let mk_select_term = Expr.Term.Array.select
@@ -46,19 +87,22 @@ let array_gty_args : Ground.Ty.t -> Ground.Ty.t * Ground.Ty.t = function
       (ind_gty, val_gty)
   | ty -> failwith (Fmt.str "'%a' is not an array ground type!" Ground.Ty.pp ty)
 
-let node_tyl env n = Ground.Ty.S.elements (Ground.tys env n)
-
 let get_node_ty env n =
   (* TODO: fix somehow *)
   match Ground.Ty.S.elements (Ground.tys env n) with
   | h :: _ -> h
   | [] -> failwith (Fmt.str "The type of the node %a was not set" Node.pp n)
 
+exception Not_An_Array
+
 let get_array_gty env n =
-  List.find
-    (function
-      | Ground.Ty.{ app = { builtin = Expr.Array; _ }; _ } -> true | _ -> false)
-    (Ground.Ty.S.elements (Ground.tys env n))
+  try
+    List.find
+      (function
+        | Ground.Ty.{ app = { builtin = Expr.Array; _ }; _ } -> true
+        | _ -> false)
+      (Ground.Ty.S.elements (Ground.tys env n))
+  with Not_found -> raise Not_An_Array
 
 let get_array_gty_args env n = array_gty_args (get_array_gty env n)
 
@@ -81,14 +125,15 @@ module Builtin = struct
   let array_diff : Dolmen_std.Expr.term_cst =
     Expr.Id.mk ~name:"colibri2_array_diff" ~builtin:Array_diff
       (Dolmen_std.Path.global "colibri2_array_diff")
-      (Expr.Ty.pi [ a_ty_var; b_ty_var ]
-         (Expr.Ty.arrow [ array_ty_ab; array_ty_ab ] a_ty))
+      (Expr.Ty.pi
+         [ STV.a_ty_var; STV.b_ty_var ]
+         (Expr.Ty.arrow [ STV.array_ty_ab; STV.array_ty_ab ] STV.a_ty))
 
   let array_const : Dolmen_std.Expr.term_cst =
     Expr.Id.mk ~name:"colibri2_array_const" ~builtin:Array_const
       (Dolmen_std.Path.global "colibri2_array_const")
-      (Expr.Ty.pi [ b_ty_var ]
-         (Expr.Ty.arrow [ b_ty ] (Expr.Ty.array ind_ty b_ty)))
+      (Expr.Ty.pi [ STV.b_ty_var ]
+         (Expr.Ty.arrow [ STV.b_ty ] (Expr.Ty.array STV.ind_ty STV.b_ty)))
 
   let array_map : int -> Dolmen_std.Expr.term_cst =
     let cache = DInt.H.create 13 in
@@ -98,8 +143,9 @@ module Builtin = struct
       | exception Not_found ->
           let ty =
             Expr.Ty.arrow
-              (Expr.Ty.arrow (replicate i b_ty) c_ty :: replicate i array_ty_ab)
-              array_ty_ac
+              (Expr.Ty.arrow (replicate i STV.b_ty) STV.c_ty
+              :: replicate i STV.array_ty_ab)
+              STV.array_ty_ac
           in
           DInt.H.add cache i ty;
           ty
@@ -107,17 +153,23 @@ module Builtin = struct
     fun i ->
       Expr.Id.mk ~name:"colibri2_array_map" ~builtin:Array_map
         (Dolmen_std.Path.global "colibri2_array_map")
-        (Expr.Ty.pi [ a_ty_var; b_ty_var; c_ty_var ] (get_ty i))
+        (Expr.Ty.pi
+           [ STV.a_ty_var; STV.b_ty_var; STV.c_ty_var ]
+           (get_ty i))
 
   let array_default_index : Dolmen_std.Expr.term_cst =
     Expr.Id.mk ~name:"colibri2_array_default_index" ~builtin:Array_default_index
       (Dolmen_std.Path.global "colibri2_array_default_index")
-      (Expr.Ty.pi [ a_ty_var; b_ty_var ] (Expr.Ty.arrow [ array_ty_ab ] a_ty))
+      (Expr.Ty.pi
+         [ STV.a_ty_var; STV.b_ty_var ]
+         (Expr.Ty.arrow [ STV.array_ty_ab ] STV.a_ty))
 
   let array_default_value : Dolmen_std.Expr.term_cst =
     Expr.Id.mk ~name:"colibri2_array_default_value" ~builtin:Array_default_value
       (Dolmen_std.Path.global "colibri2_array_default_value")
-      (Expr.Ty.pi [ a_ty_var; b_ty_var ] (Expr.Ty.arrow [ array_ty_ab ] b_ty))
+      (Expr.Ty.pi
+         [ STV.a_ty_var; STV.b_ty_var ]
+         (Expr.Ty.arrow [ STV.array_ty_ab ] STV.b_ty))
 
   let apply_array_diff a b =
     let ind_ty, val_ty = array_ty_args a.Expr.term_ty in
@@ -205,22 +257,3 @@ let distinct_arrays a b =
   Expr.Term.distinct [ mk_select_term a diff; mk_select_term b diff ]
 
 let sem_to_node s = Ground.node (Ground.index s)
-
-module Terms = struct
-  let term_of_var = Expr.Term.of_var
-  let mk_index_var name = Expr.Term.Var.mk name ind_ty
-  let mk_value_var name = Expr.Term.Var.mk name val_ty
-  let mk_array_var name = Expr.Term.Var.mk name array_ty
-  let vi = mk_index_var "i"
-  let vj = mk_index_var "j"
-  let vk = mk_index_var "k"
-  let vv = mk_value_var "v"
-  let ti = term_of_var vi
-  let tj = term_of_var vj
-  let tk = term_of_var vk
-  let tv = term_of_var vv
-  let va = mk_array_var "a"
-  let vb = mk_array_var "b"
-  let ta = term_of_var va
-  let tb = term_of_var vb
-end

colibri2/theories/array/common.mli

+(*************************************************************************)
+(*  This file is part of Colibri2.                                       *)
+(*                                                                       *)
+(*  Copyright (C) 2014-2021                                              *)
+(*    CEA   (Commissariat à l'énergie atomique et aux énergies           *)
+(*           alternatives)                                               *)
+(*    OCamlPro                                                           *)
+(*                                                                       *)
+(*  you can redistribute it and/or modify it under the terms of the GNU  *)
+(*  Lesser General Public License as published by the Free Software      *)
+(*  Foundation, version 2.1.                                             *)
+(*                                                                       *)
+(*  It is distributed in the hope that it will be useful,                *)
+(*  but WITHOUT ANY WARRANTY; without even the implied warranty of       *)
+(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the        *)
+(*  GNU Lesser General Public License for more details.                  *)
+(*                                                                       *)
+(*  See the GNU Lesser General Public License version 2.1                *)
+(*  for more details (enclosed in the file licenses/LGPLv2.1).           *)
+(*************************************************************************)
+
+val use_diff_graph : bool Options.t
+val debug : Debug.flag
+val convert : subst:Ground.Subst.t -> 'a Egraph.t -> Expr.term -> Node.t
+
+module STV : sig
+  val ind_ty_var : Dolmen_std.Expr.ty_var
+  val val_ty_var : Dolmen_std.Expr.ty_var
+  val alpha_ty_var : Dolmen_std.Expr.ty_var
+  val a_ty_var : Dolmen_std.Expr.ty_var
+  val b_ty_var : Dolmen_std.Expr.ty_var
+  val c_ty_var : Dolmen_std.Expr.ty_var
+  val ind_ty : Expr.ty
+  val val_ty : Expr.ty
+  val a_ty : Expr.ty
+  val b_ty : Expr.ty
+  val c_ty : Expr.ty
+  val alpha_ty : Expr.ty
+  val array_ty : Expr.ty
+  val array_ty_ab : Expr.ty
+  val array_ty_ac : Expr.ty
+  val array_ty_alpha : Expr.ty
+  val term_of_var : Dolmen_std.Expr.term_var -> Expr.term
+  val mk_index_var : string -> Dolmen_std.Expr.term_var
+  val mk_value_var : string -> Dolmen_std.Expr.term_var
+  val mk_array_var : string -> Dolmen_std.Expr.term_var
+  val vi : Dolmen_std.Expr.term_var
+  val vj : Dolmen_std.Expr.term_var
+  val vk : Dolmen_std.Expr.term_var
+  val vv : Dolmen_std.Expr.term_var
+  val ti : Expr.term
+  val tj : Expr.term
+  val tk : Expr.term
+  val tv : Expr.term
+  val va : Dolmen_std.Expr.term_var
+  val vb : Dolmen_std.Expr.term_var
+  val ta : Expr.term
+  val tb : Expr.term
+end
+
+val replicate : int -> 'a -> 'a list
+val mk_store_term : Expr.term -> Expr.term -> Expr.term -> Expr.term
+val mk_select_term : Expr.term -> Expr.term -> Expr.term
+
+val apply_cst :
+  Dolmen_std.Expr.term_cst -> Expr.ty list -> Expr.term list -> Expr.term
+
+val array_gty_args : Ground.Ty.t -> Ground.Ty.t * Ground.Ty.t
+val get_node_ty : 'a Egraph.t -> Node.t -> Ground.Ty.t
+
+exception Not_An_Array
+
+val get_array_gty : 'a Egraph.t -> Node.t -> Ground.Ty.t
+val get_array_gty_args : 'a Egraph.t -> Node.t -> Ground.Ty.t * Ground.Ty.t
+val add_array_gty : Egraph.wt -> Node.t -> Ground.Ty.t -> Ground.Ty.t -> unit
+
+module Builtin : sig
+  type 'a Builtin.t +=
+    | Array_diff
+    | Array_const
+    | Array_map
+    | Array_default_index
+    | Array_default_value
+
+  val array_diff : Dolmen_std.Expr.term_cst
+  val array_const : Dolmen_std.Expr.term_cst
+  val array_map : int -> Dolmen_std.Expr.term_cst
+  val array_default_index : Dolmen_std.Expr.term_cst
+  val array_default_value : Dolmen_std.Expr.term_cst
+  val apply_array_diff : Expr.term -> Expr.term -> Expr.term
+  val apply_array_const : Expr.term -> Expr.term
+  val apply_array_def_index : Expr.term -> Expr.term
+  val apply_array_def_value : Expr.term -> Expr.term
+  val apply_array_map : int -> Expr.term -> Expr.term list -> Expr.term
+end
+
+val mk_subst :
+  (Dolmen_std.Expr.term_var * Node.t) list ->
+  (Dolmen_std.Expr.ty_var * Ground.Ty.t) list ->
+  Ground.Subst.t
+
+val mk_eq : 'a Egraph.t -> Node.t -> Node.t -> Ground.Ty.t -> Ground.s
+val distinct_arrays : Expr.term -> Expr.term -> Expr.term
+val sem_to_node : Ground.s -> Node.t

colibri2/theories/nseq/nseq.ml

@@ -152,7 +152,7 @@ module Builtin = struct
     in
     Expr.add_builtins (fun env s ->
         match s with
-        | Dolmen_loop.Typer.T.Id { ns = Sort; name = Simple "seq" } ->
+        | Dolmen_loop.Typer.T.Id { ns = Sort; name = Simple "NSeq" } ->
             ty_app1 env s nseq_ty_const
         | Dolmen_loop.Typer.T.Id { ns = Term; name = Simple "nseq_first" } ->
             app1 env s nseq_first

colibri2/theories/nseq/nseq.mli

@@ -18,3 +18,4 @@
 (*  See the GNU Lesser General Public License version 2.1                *)
 (*  for more details (enclosed in the file licenses/LGPLv2.1).           *)
 (*************************************************************************)
+