diff --git a/Makefile b/Makefile
index d1cabbf78844f69d847416dd61408adadb3bdaed..470e3507bc8bab739f971d93d349f8a2b9d5727a 100644
--- a/Makefile
+++ b/Makefile
@@ -1,12 +1,21 @@
##########################################################################
+# This file is part of Colibri2. #
# #
-# Copyright (C) 2019-2019 #
-# CEA (Commissariat à l'énergie atomique et aux énergies #
-# alternatives) #
+# Copyright (C) 2014-2021 #
+# CEA (Commissariat à l'énergie atomique et aux énergies #
+# alternatives) #
# #
-# All rights reserved. #
-# Contact CEA LIST for licensing. #
+# 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). #
##########################################################################
all:
@@ -73,13 +82,13 @@ uninstall:
# file headers
###############
-WHY3_FILES = $(addprefix src_colibri2/popop_lib/, cmdline.ml cmdline.mli debug.ml \
- debug.mli exn_printer.ml exn_printer.mli hashcons.ml \
- hashcons.mli lists.ml lists.mli loc.ml loc.mli number.ml \
- number.mli opt.ml opt.mli plugin.ml plugin.mli pp.ml pp.mli \
- print_tree.ml print_tree.mli stdlib.ml stdlib.mli strings.ml \
- strings.mli sysutil.ml sysutil.mli util.ml util.mli \
- warning.ml warning.mli weakhtbl.ml weakhtbl.mli )
+WHY3_FILES = $(addprefix src_colibri2/popop_lib/, cmdline.ml cmdline.mli \
+ debug.ml debug.mli exn_printer.ml exn_printer.mli hashcons.ml \
+ hashcons.mli lists.ml lists.mli loc.ml loc.mli number.ml number.mli \
+ opt.ml opt.mli pp.ml pp.mli print_tree.ml print_tree.mli \
+ popop_stdlib.ml popop_stdlib.mli strings.ml strings.mli sysutil.ml \
+ sysutil.mli util.ml util.mli warning.ml warning.mli weakhtbl.ml \
+ weakhtbl.mli )
OCAML_FILES = $(addprefix src_colibri2/popop_lib/, map_intf.ml exthtbl.ml \
exthtbl.mli extmap.ml extmap.mli extset.ml extset.mli )
@@ -89,22 +98,28 @@ FRAMAC_FILES = $(addprefix src_colibri2/popop_lib/, intmap.ml intmap_hetero.ml \
JC_FILES = $(addprefix src_colibri2/popop_lib/, leftistheap.ml leftistheap.mli)
-WITAN_FILES = src_colibri2/bin/typecheck.ml src_colibri2/stdlib/std.ml src_colibri2/stdlib/std.mli \
- src_colibri2/stdlib/hashtbl_hetero.ml src_colibri2/stdlib/hashtbl_hetero.mli \
- src_colibri2/stdlib/hashtbl_hetero_sig.ml \
- src_colibri2/stdlib/map_hetero.ml src_colibri2/stdlib/map_hetero.mli \
- src_colibri2/stdlib/map_hetero_sig.ml \
- src_colibri2/stdlib/keys.mli src_colibri2/stdlib/keys_sig.ml \
- src_colibri2/stdlib/comp_keys.mli src_colibri2/stdlib/comp_keys.mli
-
-COLIBRICS_FILES = Makefile \
- $(filter-out $(WHY3_FILES) $(OCAML_FILES) $(FRAMAC_FILES) $(JC_FILES) \
+WITAN_FILES = src_colibri2/stdlib/std.ml src_colibri2/stdlib/std.mli \
+ src_colibri2/stdlib/hashtbl_hetero.ml \
+ src_colibri2/stdlib/hashtbl_hetero.mli \
+ src_colibri2/stdlib/hashtbl_hetero_sig.ml \
+ src_colibri2/stdlib/map_hetero.ml src_colibri2/stdlib/map_hetero.mli \
+ src_colibri2/stdlib/map_hetero_sig.ml src_colibri2/stdlib/keys.mli \
+ src_colibri2/stdlib/keys_sig.ml src_colibri2/stdlib/comp_keys.ml \
+ src_colibri2/stdlib/comp_keys.mli src_colibri2/bin/options.ml
+
+COLIBRI2_FILES = Makefile \
+ $(filter-out $(WHY3_FILES) $(OCAML_FILES) $(FRAMAC_FILES) $(JC_FILES) $(WITAN_FILES) \
, $(wildcard src_colibri2/*/*/*.ml* src_colibri2/*/*.ml* src_colibri2/*.ml*))
+COLIBRICS_FILES =
+
+
headers:
headache -c misc/headache_config.txt -h misc/header_colibrics.txt \
$(COLIBRICS_FILES)
headache -c misc/headache_config.txt -h misc/header_colibri2.txt \
+ $(COLIBRI2_FILES)
+ headache -c misc/headache_config.txt -h misc/header_witan.txt \
$(WITAN_FILES)
headache -c misc/headache_config.txt -h misc/header_why3.txt \
$(WHY3_FILES)
diff --git a/misc/header_colibri2.txt b/misc/header_colibri2.txt
new file mode 100644
index 0000000000000000000000000000000000000000..743f8bbba9930d030c0d05f07eca2643ba7837c2
--- /dev/null
+++ b/misc/header_colibri2.txt
@@ -0,0 +1,17 @@
+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).
diff --git a/misc/header_colibrics.txt b/misc/header_colibrics.txt
index 7c2e7896077193a11448144ed5d5806370334ab2..bf1e8ba82b314c424cd5319eb26f91405e6f6031 100644
--- a/misc/header_colibrics.txt
+++ b/misc/header_colibrics.txt
@@ -1,6 +1,6 @@
This file is part of Colibrics.
-Copyright (C) 2017
+Copyright (C) 2019-2021
CEA (Commissariat à l'énergie atomique et aux énergies
alternatives)
diff --git a/misc/header_witan.txt b/misc/header_witan.txt
index 50a403db9cf0806b8895577ea398de91cfca8d4e..ffe19af33d17354a07622c7c74c5f0dfe2d45545 100644
--- a/misc/header_witan.txt
+++ b/misc/header_witan.txt
@@ -1,6 +1,6 @@
This file is part of Colibri2.
-Copyright (C) 2017
+Copyright (C) 2017-2021
CEA (Commissariat à l'énergie atomique et aux énergies
alternatives)
INRIA (Institut National de Recherche en Informatique et en
diff --git a/src_colibri2/bin/main.ml b/src_colibri2/bin/main.ml
index 056b57e28e193c0c050eb8b2b72ad99721ffc772..457225cbfb4456e9484f8d97b8b065b5f06e16f0 100644
--- a/src_colibri2/bin/main.ml
+++ b/src_colibri2/bin/main.ml
@@ -1,3 +1,23 @@
+(*************************************************************************)
+(* 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). *)
+(*************************************************************************)
+
(* This file is free software, copied from dolmen. See file "LICENSE" for more information *)
let () =
diff --git a/src_colibri2/bin/options.ml b/src_colibri2/bin/options.ml
index 50396f714e7c2296bed6edacbb11a82c98d83759..f2c54316aea9b16803a70f49e52a21200b367108 100644
--- a/src_colibri2/bin/options.ml
+++ b/src_colibri2/bin/options.ml
@@ -1,3 +1,25 @@
+(*************************************************************************)
+(* This file is part of Colibri2. *)
+(* *)
+(* Copyright (C) 2017-2021 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* INRIA (Institut National de Recherche en Informatique et en *)
+(* Automatique) *)
+(* CNRS (Centre national de la recherche scientifique) *)
+(* *)
+(* 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). *)
+(*************************************************************************)
(* This file is free software, part of dolmen. See file "LICENSE" for more information *)
diff --git a/src_colibri2/core/colibri2_core.ml b/src_colibri2/core/colibri2_core.ml
index 00ad7f365278ef18f760480630c7a152317840d3..f4b1d10b39f53367d031381f1eeb2558f19de618 100644
--- a/src_colibri2/core/colibri2_core.ml
+++ b/src_colibri2/core/colibri2_core.ml
@@ -1,7 +1,7 @@
(*************************************************************************)
-(* This file is part of Colibrics. *)
+(* This file is part of Colibri2. *)
(* *)
-(* Copyright (C) 2017 *)
+(* Copyright (C) 2014-2021 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
diff --git a/src_colibri2/core/datastructure.ml b/src_colibri2/core/datastructure.ml
index ae03ab0d6d061327768b3a0713f2e3b0f9fc300c..7817ab033999890a71d35e35d581e2fd4689ae3b 100644
--- a/src_colibri2/core/datastructure.ml
+++ b/src_colibri2/core/datastructure.ml
@@ -1,7 +1,7 @@
(*************************************************************************)
-(* This file is part of Colibrics. *)
+(* This file is part of Colibri2. *)
(* *)
-(* Copyright (C) 2017 *)
+(* Copyright (C) 2014-2021 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
diff --git a/src_colibri2/core/datastructure.mli b/src_colibri2/core/datastructure.mli
index 07a79d56793e03f5f31097f500dda4baca301145..63cc3222a1b45c791447560005ee9a388aae4774 100644
--- a/src_colibri2/core/datastructure.mli
+++ b/src_colibri2/core/datastructure.mli
@@ -1,7 +1,7 @@
(*************************************************************************)
-(* This file is part of Colibrics. *)
+(* This file is part of Colibri2. *)
(* *)
-(* Copyright (C) 2017 *)
+(* Copyright (C) 2014-2021 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
diff --git a/src_colibri2/core/demon.ml b/src_colibri2/core/demon.ml
index 11bd1dacdd668af2d78044b339b374b82eccb0a2..9e58359bf0209f2755758bf06ee7d9b270532cda 100644
--- a/src_colibri2/core/demon.ml
+++ b/src_colibri2/core/demon.ml
@@ -1,7 +1,7 @@
(*************************************************************************)
-(* This file is part of Colibrics. *)
+(* This file is part of Colibri2. *)
(* *)
-(* Copyright (C) 2017 *)
+(* Copyright (C) 2014-2021 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
diff --git a/src_colibri2/core/demon.mli b/src_colibri2/core/demon.mli
index d44791dd1b499c5bee5c3aba399abad6abff323e..fb97f735420695f6eb5bbd396b8eacfe1b9d90f8 100644
--- a/src_colibri2/core/demon.mli
+++ b/src_colibri2/core/demon.mli
@@ -1,7 +1,7 @@
(*************************************************************************)
-(* This file is part of Colibrics. *)
+(* This file is part of Colibri2. *)
(* *)
-(* Copyright (C) 2017 *)
+(* Copyright (C) 2014-2021 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
diff --git a/src_colibri2/core/egraph.ml b/src_colibri2/core/egraph.ml
index a16452301b6f26c1db224c28c602fc489227ceda..243c9cb655bae5f308d8f4195b0d8cf88c9ca0c3 100644
--- a/src_colibri2/core/egraph.ml
+++ b/src_colibri2/core/egraph.ml
@@ -1,7 +1,7 @@
(*************************************************************************)
-(* This file is part of Colibrics. *)
+(* This file is part of Colibri2. *)
(* *)
-(* Copyright (C) 2017 *)
+(* Copyright (C) 2014-2021 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
diff --git a/src_colibri2/core/egraph.mli b/src_colibri2/core/egraph.mli
index 6cf8108ced2036e4b99209986d3098215c533c09..fbbea422cbcc69705d277376ae2ad2b168b24917 100644
--- a/src_colibri2/core/egraph.mli
+++ b/src_colibri2/core/egraph.mli
@@ -1,7 +1,7 @@
(*************************************************************************)
-(* This file is part of Colibrics. *)
+(* This file is part of Colibri2. *)
(* *)
-(* Copyright (C) 2017 *)
+(* Copyright (C) 2014-2021 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
diff --git a/src_colibri2/core/env.ml b/src_colibri2/core/env.ml
index e2722fca8a76859a926ecbf1c6907b820c776e41..2b44678ce7d1bfa381637c9bf5b92e5081e314f9 100644
--- a/src_colibri2/core/env.ml
+++ b/src_colibri2/core/env.ml
@@ -1,7 +1,7 @@
(*************************************************************************)
-(* This file is part of Colibrics. *)
+(* This file is part of Colibri2. *)
(* *)
-(* Copyright (C) 2017 *)
+(* Copyright (C) 2014-2021 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
diff --git a/src_colibri2/core/env.mli b/src_colibri2/core/env.mli
index 21da18a3cf1d21750b07d9988d93cac0c7724076..192884becd4e8affc754a54aa35e9dd8f6299971 100644
--- a/src_colibri2/core/env.mli
+++ b/src_colibri2/core/env.mli
@@ -1,7 +1,7 @@
(*************************************************************************)
-(* This file is part of Colibrics. *)
+(* This file is part of Colibri2. *)
(* *)
-(* Copyright (C) 2017 *)
+(* Copyright (C) 2014-2021 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
diff --git a/src_colibri2/core/events.ml b/src_colibri2/core/events.ml
index 0398fdf738bcd71ffc3eb477a55bad620f251eae..a6d69ec436f37134bba1be9e12d39dd3bec10006 100644
--- a/src_colibri2/core/events.ml
+++ b/src_colibri2/core/events.ml
@@ -1,7 +1,7 @@
(*************************************************************************)
-(* This file is part of Colibrics. *)
+(* This file is part of Colibri2. *)
(* *)
-(* Copyright (C) 2017 *)
+(* Copyright (C) 2014-2021 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
diff --git a/src_colibri2/core/events.mli b/src_colibri2/core/events.mli
index a0f82a433dd06cf267e738a6d42aff8013657643..1ea2393049b9d076400d0623bbf65d0410adebb0 100644
--- a/src_colibri2/core/events.mli
+++ b/src_colibri2/core/events.mli
@@ -1,7 +1,7 @@
(*************************************************************************)
-(* This file is part of Colibrics. *)
+(* This file is part of Colibri2. *)
(* *)
-(* Copyright (C) 2017 *)
+(* Copyright (C) 2014-2021 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
diff --git a/src_colibri2/core/ground.ml b/src_colibri2/core/ground.ml
index 26a9f958eafe4e1e14b440b38152b48146bf1d47..fb4ca294f7276b4bc460d3bd175c42518e81118f 100644
--- a/src_colibri2/core/ground.ml
+++ b/src_colibri2/core/ground.ml
@@ -1,3 +1,23 @@
+(*************************************************************************)
+(* 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). *)
+(*************************************************************************)
+
open Colibri2_popop_lib
open Nodes
diff --git a/src_colibri2/core/ground.mli b/src_colibri2/core/ground.mli
index 0466e1e3b493b93682f4e0acdfbc3556c900239e..d0a830f244e5d4021cdd2391a386c81f2a909439 100644
--- a/src_colibri2/core/ground.mli
+++ b/src_colibri2/core/ground.mli
@@ -1,3 +1,23 @@
+(*************************************************************************)
+(* 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). *)
+(*************************************************************************)
+
open Colibri2_popop_lib
open Nodes
diff --git a/src_colibri2/core/interp.ml b/src_colibri2/core/interp.ml
index eca08223ad2e17d053c739dcf4dc99e0820c4cf1..ca255f6b892dca94b6c7f7a624b2fdd95b39df66 100644
--- a/src_colibri2/core/interp.ml
+++ b/src_colibri2/core/interp.ml
@@ -1,7 +1,7 @@
(*************************************************************************)
-(* This file is part of Colibrics. *)
+(* This file is part of Colibri2. *)
(* *)
-(* Copyright (C) 2017 *)
+(* Copyright (C) 2014-2021 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
diff --git a/src_colibri2/core/interp.mli b/src_colibri2/core/interp.mli
index ec5491375600e21b9d2c058dde5c1aa5ef4e70a3..3dcfe4ba32a6028fca99df1b202467ec8a2001c6 100644
--- a/src_colibri2/core/interp.mli
+++ b/src_colibri2/core/interp.mli
@@ -1,7 +1,7 @@
(*************************************************************************)
-(* This file is part of Colibrics. *)
+(* This file is part of Colibri2. *)
(* *)
-(* Copyright (C) 2017 *)
+(* Copyright (C) 2014-2021 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
diff --git a/src_colibri2/core/structures/domKind.ml b/src_colibri2/core/structures/domKind.ml
index 006a458eb5bb992a7d79e7a6ce28f85cf4906e47..df4d01380a6f4021e0ebc42599dbe63c2ad375f8 100644
--- a/src_colibri2/core/structures/domKind.ml
+++ b/src_colibri2/core/structures/domKind.ml
@@ -1,7 +1,7 @@
(*************************************************************************)
-(* This file is part of Colibrics. *)
+(* This file is part of Colibri2. *)
(* *)
-(* Copyright (C) 2017 *)
+(* Copyright (C) 2014-2021 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
diff --git a/src_colibri2/core/structures/domKind.mli b/src_colibri2/core/structures/domKind.mli
index 71cc718a0a29e93796b76515f0ac082f1f5dd8d8..2198cf2ebc35a04a14c2c1062028e46bc1fb6d57 100644
--- a/src_colibri2/core/structures/domKind.mli
+++ b/src_colibri2/core/structures/domKind.mli
@@ -1,7 +1,7 @@
(*************************************************************************)
-(* This file is part of Colibrics. *)
+(* This file is part of Colibri2. *)
(* *)
-(* Copyright (C) 2017 *)
+(* Copyright (C) 2014-2021 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
diff --git a/src_colibri2/core/structures/expr.ml b/src_colibri2/core/structures/expr.ml
index d8b4c18cea3d5a8d6a39496a75e9affccc996a41..e2b5c132731e62c9b813ad2f4ea7920eda1bc64c 100644
--- a/src_colibri2/core/structures/expr.ml
+++ b/src_colibri2/core/structures/expr.ml
@@ -1,3 +1,23 @@
+(*************************************************************************)
+(* 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). *)
+(*************************************************************************)
+
include Dolmen_std.Expr
module Ty = struct
diff --git a/src_colibri2/core/structures/nodes.ml b/src_colibri2/core/structures/nodes.ml
index 7c455376fef42bd042c614e204710847d41b06d1..5e6239f6a12cee646f716971f28fcba9485884df 100644
--- a/src_colibri2/core/structures/nodes.ml
+++ b/src_colibri2/core/structures/nodes.ml
@@ -1,7 +1,7 @@
(*************************************************************************)
-(* This file is part of Colibrics. *)
+(* This file is part of Colibri2. *)
(* *)
-(* Copyright (C) 2017 *)
+(* Copyright (C) 2014-2021 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
diff --git a/src_colibri2/core/structures/nodes.mli b/src_colibri2/core/structures/nodes.mli
index 6ab60caa3be159f57bb566eca0c24c025064e9d3..200d5181a5de5ca588fc39f4a0065106d2d92ad9 100644
--- a/src_colibri2/core/structures/nodes.mli
+++ b/src_colibri2/core/structures/nodes.mli
@@ -1,7 +1,7 @@
(*************************************************************************)
-(* This file is part of Colibrics. *)
+(* This file is part of Colibri2. *)
(* *)
-(* Copyright (C) 2017 *)
+(* Copyright (C) 2014-2021 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
diff --git a/src_colibri2/core/structures/term.ml b/src_colibri2/core/structures/term.ml
index 8755f361597707d31ff5603d34fbda53a6d4c5aa..e3212573b19aa8d8e430d85878cfc6fb296a4797 100644
--- a/src_colibri2/core/structures/term.ml
+++ b/src_colibri2/core/structures/term.ml
@@ -1,7 +1,7 @@
(*************************************************************************)
-(* This file is part of Colibrics. *)
+(* This file is part of Colibri2. *)
(* *)
-(* Copyright (C) 2017 *)
+(* Copyright (C) 2014-2021 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
diff --git a/src_colibri2/core/theory.ml b/src_colibri2/core/theory.ml
index add74dd0a39ee0b0eea055f47a3f031e6717e541..a2ae686a50119761f2f12edfabbf34e98a913a9c 100644
--- a/src_colibri2/core/theory.ml
+++ b/src_colibri2/core/theory.ml
@@ -1,7 +1,7 @@
(*************************************************************************)
-(* This file is part of Colibrics. *)
+(* This file is part of Colibri2. *)
(* *)
-(* Copyright (C) 2017 *)
+(* Copyright (C) 2014-2021 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
diff --git a/src_colibri2/popop_lib/IArray.ml b/src_colibri2/popop_lib/IArray.ml
index cf071ce33ef7b2ba0c1c05c7bcd9ef32d4e81229..b81cd06030d4d7484d021a1691fdf3f4a9aa6d59 100644
--- a/src_colibri2/popop_lib/IArray.ml
+++ b/src_colibri2/popop_lib/IArray.ml
@@ -1,7 +1,7 @@
(*************************************************************************)
-(* This file is part of Colibrics. *)
+(* This file is part of Colibri2. *)
(* *)
-(* Copyright (C) 2017 *)
+(* Copyright (C) 2014-2021 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
diff --git a/src_colibri2/popop_lib/IArray.mli b/src_colibri2/popop_lib/IArray.mli
index bb21e7d189444a498a9cf53218143a7fa9623873..cacc44434a62c42467b7792dce1b2cbe4cae61b1 100644
--- a/src_colibri2/popop_lib/IArray.mli
+++ b/src_colibri2/popop_lib/IArray.mli
@@ -1,7 +1,7 @@
(*************************************************************************)
-(* This file is part of Colibrics. *)
+(* This file is part of Colibri2. *)
(* *)
-(* Copyright (C) 2017 *)
+(* Copyright (C) 2014-2021 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
diff --git a/src_colibri2/popop_lib/TimeWheel.ml b/src_colibri2/popop_lib/TimeWheel.ml
index 6f606a1aaf48273f3857e392eaaf4cca62fa8f76..66c9667d00dce3f4c5edea203e4b6dcf320a9acc 100644
--- a/src_colibri2/popop_lib/TimeWheel.ml
+++ b/src_colibri2/popop_lib/TimeWheel.ml
@@ -1,3 +1,23 @@
+(*************************************************************************)
+(* 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). *)
+(*************************************************************************)
+
open Base
(** TimeWheel *)
diff --git a/src_colibri2/popop_lib/TimeWheel.mli b/src_colibri2/popop_lib/TimeWheel.mli
index 1e15834515ee9823e8f16b49ece918ba15b6d48d..47d9fc34929c5ee1474a625e215e9e0b992d80c3 100644
--- a/src_colibri2/popop_lib/TimeWheel.mli
+++ b/src_colibri2/popop_lib/TimeWheel.mli
@@ -1,3 +1,23 @@
+(*************************************************************************)
+(* 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). *)
+(*************************************************************************)
+
(** Time Wheel *)
(** Allows to add timestamp in the futur and get the next timestamp.
diff --git a/src_colibri2/popop_lib/enum.ml b/src_colibri2/popop_lib/enum.ml
index 3d7eb0c17a840e9873b0a81a93fa049550bfd25f..188e08b18428e8f00c45600157bfcffbd05a0c55 100644
--- a/src_colibri2/popop_lib/enum.ml
+++ b/src_colibri2/popop_lib/enum.ml
@@ -1,7 +1,7 @@
(*************************************************************************)
-(* This file is part of Colibrics. *)
+(* This file is part of Colibri2. *)
(* *)
-(* Copyright (C) 2017 *)
+(* Copyright (C) 2014-2021 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
diff --git a/src_colibri2/popop_lib/enum.mli b/src_colibri2/popop_lib/enum.mli
index 01200b460241210c47e5d30aca623a391f7dd59b..9abb7a9b72f10c631d8aa84ebd65c6d704d27637 100644
--- a/src_colibri2/popop_lib/enum.mli
+++ b/src_colibri2/popop_lib/enum.mli
@@ -1,7 +1,7 @@
(*************************************************************************)
-(* This file is part of Colibrics. *)
+(* This file is part of Colibri2. *)
(* *)
-(* Copyright (C) 2017 *)
+(* Copyright (C) 2014-2021 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
diff --git a/src_colibri2/popop_lib/popop_stdlib.ml b/src_colibri2/popop_lib/popop_stdlib.ml
index 8d981e9e37e57eb8a300796bbbaf5ec133c3a2f8..74bfc53b814c86111713799587f50679d834e398 100644
--- a/src_colibri2/popop_lib/popop_stdlib.ml
+++ b/src_colibri2/popop_lib/popop_stdlib.ml
@@ -1,22 +1,13 @@
-(*************************************************************************)
-(* This file is part of Colibrics. *)
-(* *)
-(* Copyright (C) 2017 *)
-(* 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). *)
-(*************************************************************************)
+(********************************************************************)
+(* *)
+(* The Why3 Verification Platform / The Why3 Development Team *)
+(* Copyright 2010-2017 -- INRIA - CNRS - Paris-Sud University *)
+(* *)
+(* This software is distributed under the terms of the GNU Lesser *)
+(* General Public License version 2.1, with the special exception *)
+(* on linking described in file LICENSE. *)
+(* *)
+(********************************************************************)
module Map = Extmap
module XHashtbl = Exthtbl.Hashtbl
diff --git a/src_colibri2/popop_lib/popop_stdlib.mli b/src_colibri2/popop_lib/popop_stdlib.mli
index 5223769cc60fb9c7299a55933030908697546439..48930dafdfcc6a31a37fa23fd2fbdda97679d66d 100644
--- a/src_colibri2/popop_lib/popop_stdlib.mli
+++ b/src_colibri2/popop_lib/popop_stdlib.mli
@@ -1,22 +1,13 @@
-(*************************************************************************)
-(* This file is part of Colibrics. *)
-(* *)
-(* Copyright (C) 2017 *)
-(* 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). *)
-(*************************************************************************)
+(********************************************************************)
+(* *)
+(* The Why3 Verification Platform / The Why3 Development Team *)
+(* Copyright 2010-2017 -- INRIA - CNRS - Paris-Sud University *)
+(* *)
+(* This software is distributed under the terms of the GNU Lesser *)
+(* General Public License version 2.1, with the special exception *)
+(* on linking described in file LICENSE. *)
+(* *)
+(********************************************************************)
module Map : module type of Extmap
module XHashtbl : Exthtbl.Hashtbl
diff --git a/src_colibri2/popop_lib/refo.ml b/src_colibri2/popop_lib/refo.ml
index 7fe2a4629335e8de9334abd4b7a4a4200490b1ba..fc8883e629ee750f1301c6962a041088bdf0f1b8 100644
--- a/src_colibri2/popop_lib/refo.ml
+++ b/src_colibri2/popop_lib/refo.ml
@@ -1,7 +1,7 @@
(*************************************************************************)
-(* This file is part of Colibrics. *)
+(* This file is part of Colibri2. *)
(* *)
-(* Copyright (C) 2017 *)
+(* Copyright (C) 2014-2021 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
diff --git a/src_colibri2/popop_lib/refo.mli b/src_colibri2/popop_lib/refo.mli
index a8c8a7076993f054fff72110fb5e93eafdd6f95f..97b08c18f9dee1cfc98171737856fc46c6f05715 100644
--- a/src_colibri2/popop_lib/refo.mli
+++ b/src_colibri2/popop_lib/refo.mli
@@ -1,7 +1,7 @@
(*************************************************************************)
-(* This file is part of Colibrics. *)
+(* This file is part of Colibri2. *)
(* *)
-(* Copyright (C) 2017 *)
+(* Copyright (C) 2014-2021 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
diff --git a/src_colibri2/popop_lib/simple_vector.ml b/src_colibri2/popop_lib/simple_vector.ml
index eec41b667a5a9dc59d0085b1bfd744f44b133993..cad47da225e509499ac71b47a51bcfec248ae19b 100644
--- a/src_colibri2/popop_lib/simple_vector.ml
+++ b/src_colibri2/popop_lib/simple_vector.ml
@@ -1,7 +1,7 @@
(*************************************************************************)
-(* This file is part of Colibrics. *)
+(* This file is part of Colibri2. *)
(* *)
-(* Copyright (C) 2017 *)
+(* Copyright (C) 2014-2021 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
diff --git a/src_colibri2/popop_lib/simple_vector.mli b/src_colibri2/popop_lib/simple_vector.mli
index bb41c8bb072dfe4555e84fcbbfe17b363c23d411..07d1723af2251613a847c0332c8c069a27a2e5ec 100644
--- a/src_colibri2/popop_lib/simple_vector.mli
+++ b/src_colibri2/popop_lib/simple_vector.mli
@@ -1,7 +1,7 @@
(*************************************************************************)
-(* This file is part of Colibrics. *)
+(* This file is part of Colibri2. *)
(* *)
-(* Copyright (C) 2017 *)
+(* Copyright (C) 2014-2021 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
diff --git a/src_colibri2/popop_lib/unit.ml b/src_colibri2/popop_lib/unit.ml
index d02f635a0071735c90af22a68d3eb6e6b190f244..10787b6fed28f319f5be6f6270ff355eb7fe696a 100644
--- a/src_colibri2/popop_lib/unit.ml
+++ b/src_colibri2/popop_lib/unit.ml
@@ -1,7 +1,7 @@
(*************************************************************************)
-(* This file is part of Colibrics. *)
+(* This file is part of Colibri2. *)
(* *)
-(* Copyright (C) 2017 *)
+(* Copyright (C) 2014-2021 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
diff --git a/src_colibri2/popop_lib/unit.mli b/src_colibri2/popop_lib/unit.mli
index 43c11eaeb51cfae742aac3baaf62dc094405d962..330cdac420d85e6ce2ee0b5f57145e038269418a 100644
--- a/src_colibri2/popop_lib/unit.mli
+++ b/src_colibri2/popop_lib/unit.mli
@@ -1,7 +1,7 @@
(*************************************************************************)
-(* This file is part of Colibrics. *)
+(* This file is part of Colibri2. *)
(* *)
-(* Copyright (C) 2017 *)
+(* Copyright (C) 2014-2021 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
diff --git a/src_colibri2/popop_lib/vector_hetero.ml b/src_colibri2/popop_lib/vector_hetero.ml
index e003f2b72c9af2981bf99f275fff47d2eac75ff7..aa991a4d8cc8b894947b1bc9920432c4611cf282 100644
--- a/src_colibri2/popop_lib/vector_hetero.ml
+++ b/src_colibri2/popop_lib/vector_hetero.ml
@@ -1,7 +1,7 @@
(*************************************************************************)
-(* This file is part of Colibrics. *)
+(* This file is part of Colibri2. *)
(* *)
-(* Copyright (C) 2017 *)
+(* Copyright (C) 2014-2021 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
diff --git a/src_colibri2/popop_lib/vector_hetero.mli b/src_colibri2/popop_lib/vector_hetero.mli
index b5d610f42b4f050e0df7295411149f6910d44ef0..64705542bc8f8dfaa842d68f8b1cabf75043738e 100644
--- a/src_colibri2/popop_lib/vector_hetero.mli
+++ b/src_colibri2/popop_lib/vector_hetero.mli
@@ -1,7 +1,7 @@
(*************************************************************************)
-(* This file is part of Colibrics. *)
+(* This file is part of Colibri2. *)
(* *)
-(* Copyright (C) 2017 *)
+(* Copyright (C) 2014-2021 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
diff --git a/src_colibri2/solver/input.ml b/src_colibri2/solver/input.ml
index d2533125a0bc37aa8c63ab54c74c366d0c8f1314..dfd18558fab4d5aacbaa10166ff0ac67f8fbcc6c 100644
--- a/src_colibri2/solver/input.ml
+++ b/src_colibri2/solver/input.ml
@@ -1,7 +1,7 @@
(*************************************************************************)
-(* This file is part of Colibrics. *)
+(* This file is part of Colibri2. *)
(* *)
-(* Copyright (C) 2017 *)
+(* Copyright (C) 2014-2021 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
diff --git a/src_colibri2/solver/scheduler.ml b/src_colibri2/solver/scheduler.ml
index 267e8528a90a388c93a68f0a2a2fd5edcdaa9148..ae30079caf52c3ae6828cf6cb735aae7caa85613 100644
--- a/src_colibri2/solver/scheduler.ml
+++ b/src_colibri2/solver/scheduler.ml
@@ -1,7 +1,7 @@
(*************************************************************************)
-(* This file is part of Colibrics. *)
+(* This file is part of Colibri2. *)
(* *)
-(* Copyright (C) 2017 *)
+(* Copyright (C) 2014-2021 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
diff --git a/src_colibri2/solver/scheduler.mli b/src_colibri2/solver/scheduler.mli
index 2bf87eabaf9c5d65079cac2a26e6a8a6406b6d1a..d4c7ee4ea0b32dd02401929f1bdedc3a19184301 100644
--- a/src_colibri2/solver/scheduler.mli
+++ b/src_colibri2/solver/scheduler.mli
@@ -1,7 +1,7 @@
(*************************************************************************)
-(* This file is part of Colibrics. *)
+(* This file is part of Colibri2. *)
(* *)
-(* Copyright (C) 2017 *)
+(* Copyright (C) 2014-2021 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
diff --git a/src_colibri2/solver/solver.ml b/src_colibri2/solver/solver.ml
index 25c5bee75fe9b8e3c78fdeda2a09a7f092210b9b..c393bb9f82bc00f50d2f10fe6ef83494d0a42f70 100644
--- a/src_colibri2/solver/solver.ml
+++ b/src_colibri2/solver/solver.ml
@@ -1,7 +1,7 @@
(*************************************************************************)
-(* This file is part of Colibrics. *)
+(* This file is part of Colibri2. *)
(* *)
-(* Copyright (C) 2017 *)
+(* Copyright (C) 2014-2021 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
diff --git a/src_colibri2/stdlib/comp_keys.ml b/src_colibri2/stdlib/comp_keys.ml
index 1c00173b64d06ba38756a555895ef4249adbaf0a..619d2c43d09760a0003f5ec6dfc29c116d18d138 100644
--- a/src_colibri2/stdlib/comp_keys.ml
+++ b/src_colibri2/stdlib/comp_keys.ml
@@ -1,9 +1,12 @@
(*************************************************************************)
-(* This file is part of Colibrics. *)
+(* This file is part of Colibri2. *)
(* *)
-(* Copyright (C) 2017 *)
+(* Copyright (C) 2017-2021 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
+(* INRIA (Institut National de Recherche en Informatique et en *)
+(* Automatique) *)
+(* CNRS (Centre national de la recherche scientifique) *)
(* *)
(* you can redistribute it and/or modify it under the terms of the GNU *)
(* Lesser General Public License as published by the Free Software *)
diff --git a/src_colibri2/stdlib/comp_keys.mli b/src_colibri2/stdlib/comp_keys.mli
index 5dc6875c9573c98a6933672a986a2eeab3d385a5..b7cf2fca4b45acb9fcd04e10ba7d530c0386f28d 100644
--- a/src_colibri2/stdlib/comp_keys.mli
+++ b/src_colibri2/stdlib/comp_keys.mli
@@ -1,7 +1,7 @@
(*************************************************************************)
-(* This file is part of Colibri2. *)
+(* This file is part of Colibri2. *)
(* *)
-(* Copyright (C) 2017 *)
+(* Copyright (C) 2017-2021 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* INRIA (Institut National de Recherche en Informatique et en *)
diff --git a/src_colibri2/stdlib/config.ml b/src_colibri2/stdlib/config.ml
index 4c0c4ea637e32653d0761d8aa126625cd72c54dc..0d942b9dd66ff030f3f52d521f9cbcd88b7da0ec 100644
--- a/src_colibri2/stdlib/config.ml
+++ b/src_colibri2/stdlib/config.ml
@@ -1,7 +1,7 @@
(*************************************************************************)
-(* This file is part of Colibrics. *)
+(* This file is part of Colibri2. *)
(* *)
-(* Copyright (C) 2017 *)
+(* Copyright (C) 2014-2021 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
diff --git a/src_colibri2/stdlib/context.ml b/src_colibri2/stdlib/context.ml
index d890f6f21414b7b64b1f25a403b5d8ce5b103233..a189dcb3e0880fe90adde5f1da2a80baae0d7570 100644
--- a/src_colibri2/stdlib/context.ml
+++ b/src_colibri2/stdlib/context.ml
@@ -1,7 +1,7 @@
(*************************************************************************)
-(* This file is part of Colibrics. *)
+(* This file is part of Colibri2. *)
(* *)
-(* Copyright (C) 2017 *)
+(* Copyright (C) 2014-2021 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
diff --git a/src_colibri2/stdlib/context.mli b/src_colibri2/stdlib/context.mli
index 8fb3f8b6567efde54a749127313f50bc12f28a7c..bd74832fbbdad707c3e3180b29e13606600cad48 100644
--- a/src_colibri2/stdlib/context.mli
+++ b/src_colibri2/stdlib/context.mli
@@ -1,7 +1,7 @@
(*************************************************************************)
-(* This file is part of Colibrics. *)
+(* This file is part of Colibri2. *)
(* *)
-(* Copyright (C) 2017 *)
+(* Copyright (C) 2014-2021 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
diff --git a/src_colibri2/stdlib/hashtbl_hetero.ml b/src_colibri2/stdlib/hashtbl_hetero.ml
index f83555bf4872209c43037606c047347bf0afe54d..ecca80e99837dd79f522048ab2803504ca297ef5 100644
--- a/src_colibri2/stdlib/hashtbl_hetero.ml
+++ b/src_colibri2/stdlib/hashtbl_hetero.ml
@@ -1,7 +1,7 @@
(*************************************************************************)
-(* This file is part of Colibri2. *)
+(* This file is part of Colibri2. *)
(* *)
-(* Copyright (C) 2017 *)
+(* Copyright (C) 2017-2021 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* INRIA (Institut National de Recherche en Informatique et en *)
diff --git a/src_colibri2/stdlib/hashtbl_hetero.mli b/src_colibri2/stdlib/hashtbl_hetero.mli
index ee817fff925afefc060ccbd228b583e628583111..fe2f788ad739a1ae91bd1a139b2d47db1203d8fc 100644
--- a/src_colibri2/stdlib/hashtbl_hetero.mli
+++ b/src_colibri2/stdlib/hashtbl_hetero.mli
@@ -1,7 +1,7 @@
(*************************************************************************)
-(* This file is part of Colibri2. *)
+(* This file is part of Colibri2. *)
(* *)
-(* Copyright (C) 2017 *)
+(* Copyright (C) 2017-2021 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* INRIA (Institut National de Recherche en Informatique et en *)
diff --git a/src_colibri2/stdlib/hashtbl_hetero_sig.ml b/src_colibri2/stdlib/hashtbl_hetero_sig.ml
index 7f32aed6333bcd9119fb2da54beb45dc78ee93b4..9aa896b0ba47880160c8cc0ff2b8b051213e15e0 100644
--- a/src_colibri2/stdlib/hashtbl_hetero_sig.ml
+++ b/src_colibri2/stdlib/hashtbl_hetero_sig.ml
@@ -1,7 +1,7 @@
(*************************************************************************)
-(* This file is part of Colibri2. *)
+(* This file is part of Colibri2. *)
(* *)
-(* Copyright (C) 2017 *)
+(* Copyright (C) 2017-2021 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* INRIA (Institut National de Recherche en Informatique et en *)
diff --git a/src_colibri2/stdlib/keys.ml b/src_colibri2/stdlib/keys.ml
index cf4545104a196c751fdc6bde4c6d92cabb9c1c00..dfc1c0624a6f4eb475412cc91f9d7e621908102a 100644
--- a/src_colibri2/stdlib/keys.ml
+++ b/src_colibri2/stdlib/keys.ml
@@ -1,7 +1,7 @@
(*************************************************************************)
-(* This file is part of Colibrics. *)
+(* This file is part of Colibri2. *)
(* *)
-(* Copyright (C) 2017 *)
+(* Copyright (C) 2014-2021 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
diff --git a/src_colibri2/stdlib/keys.mli b/src_colibri2/stdlib/keys.mli
index 5d6670ccf28ef60131984e319c95e296c1714b71..084a1ee91e266906fa74d0578d08dee51dbca68f 100644
--- a/src_colibri2/stdlib/keys.mli
+++ b/src_colibri2/stdlib/keys.mli
@@ -1,7 +1,7 @@
(*************************************************************************)
-(* This file is part of Colibri2. *)
+(* This file is part of Colibri2. *)
(* *)
-(* Copyright (C) 2017 *)
+(* Copyright (C) 2017-2021 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* INRIA (Institut National de Recherche en Informatique et en *)
diff --git a/src_colibri2/stdlib/keys_sig.ml b/src_colibri2/stdlib/keys_sig.ml
index 6ae7792bd0a994c238fe64ff615e98ec967406de..8db21311c6f01872bc3f459637d553d577ba6ce4 100644
--- a/src_colibri2/stdlib/keys_sig.ml
+++ b/src_colibri2/stdlib/keys_sig.ml
@@ -1,7 +1,7 @@
(*************************************************************************)
-(* This file is part of Colibri2. *)
+(* This file is part of Colibri2. *)
(* *)
-(* Copyright (C) 2017 *)
+(* Copyright (C) 2017-2021 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* INRIA (Institut National de Recherche en Informatique et en *)
diff --git a/src_colibri2/stdlib/map_hetero.ml b/src_colibri2/stdlib/map_hetero.ml
index 1563821d920e6d2a834ba3bf44ba46ecc5fa6cf0..306ff33ff935ffe8da9f2dc94aa1e1f7102b0a2c 100644
--- a/src_colibri2/stdlib/map_hetero.ml
+++ b/src_colibri2/stdlib/map_hetero.ml
@@ -1,7 +1,7 @@
(*************************************************************************)
-(* This file is part of Colibri2. *)
+(* This file is part of Colibri2. *)
(* *)
-(* Copyright (C) 2017 *)
+(* Copyright (C) 2017-2021 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* INRIA (Institut National de Recherche en Informatique et en *)
diff --git a/src_colibri2/stdlib/map_hetero.mli b/src_colibri2/stdlib/map_hetero.mli
index 870cdd7574343e6cf1db994576f68ccb1636d304..dc1fceb0f757d38c6684da92c9d180f77fdcce3d 100644
--- a/src_colibri2/stdlib/map_hetero.mli
+++ b/src_colibri2/stdlib/map_hetero.mli
@@ -1,7 +1,7 @@
(*************************************************************************)
-(* This file is part of Colibri2. *)
+(* This file is part of Colibri2. *)
(* *)
-(* Copyright (C) 2017 *)
+(* Copyright (C) 2017-2021 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* INRIA (Institut National de Recherche en Informatique et en *)
diff --git a/src_colibri2/stdlib/map_hetero_sig.ml b/src_colibri2/stdlib/map_hetero_sig.ml
index a6e27e7e0656f657a027b2f2b05631916b89883b..ada023913d3155e65b002d8c59bcf999eeedcb26 100644
--- a/src_colibri2/stdlib/map_hetero_sig.ml
+++ b/src_colibri2/stdlib/map_hetero_sig.ml
@@ -1,7 +1,7 @@
(*************************************************************************)
-(* This file is part of Colibri2. *)
+(* This file is part of Colibri2. *)
(* *)
-(* Copyright (C) 2017 *)
+(* Copyright (C) 2017-2021 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* INRIA (Institut National de Recherche en Informatique et en *)
diff --git a/src_colibri2/stdlib/shuffle.ml b/src_colibri2/stdlib/shuffle.ml
index 8d127a4174dc4a03bb69a10029bbd64ac9e84cc8..4001bd632a1af086ccfc7fb882141684e73127ef 100644
--- a/src_colibri2/stdlib/shuffle.ml
+++ b/src_colibri2/stdlib/shuffle.ml
@@ -1,7 +1,7 @@
(*************************************************************************)
-(* This file is part of Colibrics. *)
+(* This file is part of Colibri2. *)
(* *)
-(* Copyright (C) 2017 *)
+(* Copyright (C) 2014-2021 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
diff --git a/src_colibri2/stdlib/shuffle.mli b/src_colibri2/stdlib/shuffle.mli
index e014b41807709272a149dafecfba85e6f5f9f0e5..15f48f2b142fe3ff0251daf4d85c8f799d38099b 100644
--- a/src_colibri2/stdlib/shuffle.mli
+++ b/src_colibri2/stdlib/shuffle.mli
@@ -1,7 +1,7 @@
(*************************************************************************)
-(* This file is part of Colibrics. *)
+(* This file is part of Colibri2. *)
(* *)
-(* Copyright (C) 2017 *)
+(* Copyright (C) 2014-2021 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
diff --git a/src_colibri2/stdlib/std.ml b/src_colibri2/stdlib/std.ml
index c9f8302dcfae89ffa0985c68c3cbcea51bbae1ac..f3764175d97a29220591f0b8fa309a5bc95ff601 100644
--- a/src_colibri2/stdlib/std.ml
+++ b/src_colibri2/stdlib/std.ml
@@ -1,7 +1,7 @@
(*************************************************************************)
-(* This file is part of Colibri2. *)
+(* This file is part of Colibri2. *)
(* *)
-(* Copyright (C) 2017 *)
+(* Copyright (C) 2017-2021 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* INRIA (Institut National de Recherche en Informatique et en *)
diff --git a/src_colibri2/stdlib/std.mli b/src_colibri2/stdlib/std.mli
index 8433dd5b77d778fec4b7fe20003917cb56055ac0..625d917cd3b884731b1d33082882e3fc77bf8564 100644
--- a/src_colibri2/stdlib/std.mli
+++ b/src_colibri2/stdlib/std.mli
@@ -1,7 +1,7 @@
(*************************************************************************)
-(* This file is part of Colibri2. *)
+(* This file is part of Colibri2. *)
(* *)
-(* Copyright (C) 2017 *)
+(* Copyright (C) 2017-2021 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* INRIA (Institut National de Recherche en Informatique et en *)
diff --git a/src_colibri2/stdlib/std_sig.ml b/src_colibri2/stdlib/std_sig.ml
index 42862b932b3fdb5c68bd6147d4fb7673063501d1..5c73e0f567e9cf9d7ce20c6537d9d59a99f7c343 100644
--- a/src_colibri2/stdlib/std_sig.ml
+++ b/src_colibri2/stdlib/std_sig.ml
@@ -1,7 +1,7 @@
(*************************************************************************)
-(* This file is part of Colibrics. *)
+(* This file is part of Colibri2. *)
(* *)
-(* Copyright (C) 2017 *)
+(* Copyright (C) 2014-2021 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
diff --git a/src_colibri2/stdlib/wto.ml b/src_colibri2/stdlib/wto.ml
index f7a4d3d58a8896bac14b34227d46b43c254393e4..09fa2038d92a67192ce4d693db9a34badfc859dd 100644
--- a/src_colibri2/stdlib/wto.ml
+++ b/src_colibri2/stdlib/wto.ml
@@ -1,24 +1,22 @@
-(**************************************************************************)
-(* *)
-(* This file is part of Frama-C. *)
-(* *)
-(* Copyright (C) 2007-2020 *)
-(* 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). *)
-(* *)
-(**************************************************************************)
+(*************************************************************************)
+(* 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). *)
+(*************************************************************************)
(** Each component of the graph is either an individual node of the graph
(without) self loop, or a strongly connected component where a node is
diff --git a/src_colibri2/stdlib/wto.mli b/src_colibri2/stdlib/wto.mli
index a4226b3b926b18f9f1510658c4a0b42bb713adfb..d3e6ad31ff95de6db0c8a4256612cf91cf14b7a2 100644
--- a/src_colibri2/stdlib/wto.mli
+++ b/src_colibri2/stdlib/wto.mli
@@ -1,24 +1,22 @@
-(**************************************************************************)
-(* *)
-(* This file is part of Frama-C. *)
-(* *)
-(* Copyright (C) 2007-2020 *)
-(* 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). *)
-(* *)
-(**************************************************************************)
+(*************************************************************************)
+(* 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). *)
+(*************************************************************************)
(** Weak topological orderings (WTOs) are a hierarchical decomposition of the
a graph where each layer is topologically ordered and strongly connected
diff --git a/src_colibri2/tests/generate_tests/generate_dune_tests.ml b/src_colibri2/tests/generate_tests/generate_dune_tests.ml
index 0c848087852ca710ad7909a1f5467b02ec55f71b..7094b142db460c1b6d8d82ecb8055c6bee67f387 100644
--- a/src_colibri2/tests/generate_tests/generate_dune_tests.ml
+++ b/src_colibri2/tests/generate_tests/generate_dune_tests.ml
@@ -1,3 +1,23 @@
+(*************************************************************************)
+(* 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). *)
+(*************************************************************************)
+
let dir = Sys.argv.(1)
let result = Sys.argv.(2)
diff --git a/src_colibri2/tests/test.ml b/src_colibri2/tests/test.ml
index 5d8d12caaa72e440cee488e754e81fab8a8edaf2..216770b538cbf2494cdd5da563165887b753e273 100644
--- a/src_colibri2/tests/test.ml
+++ b/src_colibri2/tests/test.ml
@@ -1,7 +1,7 @@
(*************************************************************************)
-(* This file is part of Colibrics. *)
+(* This file is part of Colibri2. *)
(* *)
-(* Copyright (C) 2017 *)
+(* Copyright (C) 2014-2021 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
diff --git a/src_colibri2/tests/tests.ml b/src_colibri2/tests/tests.ml
index ef4d208e1d2d772299fabe39799866cf6304795c..63215c388beea4463120e38ff2ca26ec8ccb7dc3 100644
--- a/src_colibri2/tests/tests.ml
+++ b/src_colibri2/tests/tests.ml
@@ -1,7 +1,7 @@
(*************************************************************************)
-(* This file is part of Colibrics. *)
+(* This file is part of Colibri2. *)
(* *)
-(* Copyright (C) 2017 *)
+(* Copyright (C) 2014-2021 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
diff --git a/src_colibri2/tests/tests_LRA.ml b/src_colibri2/tests/tests_LRA.ml
index 0f2074808912beced31eca8cd6e8f7cc56bcf5fd..16087451d9950dcb21c7806c277637e0552fd791 100644
--- a/src_colibri2/tests/tests_LRA.ml
+++ b/src_colibri2/tests/tests_LRA.ml
@@ -1,7 +1,7 @@
(*************************************************************************)
-(* This file is part of Colibrics. *)
+(* This file is part of Colibri2. *)
(* *)
-(* Copyright (C) 2017 *)
+(* Copyright (C) 2014-2021 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
diff --git a/src_colibri2/tests/tests_bool.ml b/src_colibri2/tests/tests_bool.ml
index 07cdfb4e1e70421b09e12b9bc6345250adc6814f..6be56a2d5fda3dcea9bb95b9393ddec74e3939d2 100644
--- a/src_colibri2/tests/tests_bool.ml
+++ b/src_colibri2/tests/tests_bool.ml
@@ -1,7 +1,7 @@
(*************************************************************************)
-(* This file is part of Colibrics. *)
+(* This file is part of Colibri2. *)
(* *)
-(* Copyright (C) 2017 *)
+(* Copyright (C) 2014-2021 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
diff --git a/src_colibri2/tests/tests_lib.ml b/src_colibri2/tests/tests_lib.ml
index 54d7784e0ea0c6968f2e64e6d9929ea784a9976e..25c9d95bf011d27222f74a0f8e3276d50b6352e0 100644
--- a/src_colibri2/tests/tests_lib.ml
+++ b/src_colibri2/tests/tests_lib.ml
@@ -1,7 +1,7 @@
(*************************************************************************)
-(* This file is part of Colibrics. *)
+(* This file is part of Colibri2. *)
(* *)
-(* Copyright (C) 2017 *)
+(* Copyright (C) 2014-2021 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
diff --git a/src_colibri2/tests/tests_uf.ml b/src_colibri2/tests/tests_uf.ml
index af42f372e511e40c7ac8716dd78379b1a75ef12e..c694356f3ce80f45138352c284a5941eb3fb41cd 100644
--- a/src_colibri2/tests/tests_uf.ml
+++ b/src_colibri2/tests/tests_uf.ml
@@ -1,7 +1,7 @@
(*************************************************************************)
-(* This file is part of Colibrics. *)
+(* This file is part of Colibri2. *)
(* *)
-(* Copyright (C) 2017 *)
+(* Copyright (C) 2014-2021 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
diff --git a/src_colibri2/theories/ADT/adt.ml b/src_colibri2/theories/ADT/adt.ml
index e8b62ee4055d68c711bb292358b4656e1d83a736..8f4925404afe5b0c4b675b35898d33a7145645e9 100644
--- a/src_colibri2/theories/ADT/adt.ml
+++ b/src_colibri2/theories/ADT/adt.ml
@@ -1,3 +1,23 @@
+(*************************************************************************)
+(* 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). *)
+(*************************************************************************)
+
open Colibri2_popop_lib
open Colibri2_popop_lib.Popop_stdlib
module Case = DInt
diff --git a/src_colibri2/theories/ADT/adt.mli b/src_colibri2/theories/ADT/adt.mli
index 091896da139eb27dbd21aa95722d14114421c306..f7e23aa700953a217073d8a4934754d03bb3af4b 100644
--- a/src_colibri2/theories/ADT/adt.mli
+++ b/src_colibri2/theories/ADT/adt.mli
@@ -1 +1,21 @@
+(*************************************************************************)
+(* 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). *)
+(*************************************************************************)
+
val init : Egraph.t -> unit
diff --git a/src_colibri2/theories/ADT/adt_value.ml b/src_colibri2/theories/ADT/adt_value.ml
index eb1c0974e58a6de1363353ce95801588004260d6..eb7b4f9e3c3b4fabdcc5b90e437c4a0b4d2a3797 100644
--- a/src_colibri2/theories/ADT/adt_value.ml
+++ b/src_colibri2/theories/ADT/adt_value.ml
@@ -1,3 +1,23 @@
+(*************************************************************************)
+(* 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). *)
+(*************************************************************************)
+
open Base
open Colibri2_core
open Colibri2_popop_lib.Popop_stdlib
diff --git a/src_colibri2/theories/ADT/adt_value.mli b/src_colibri2/theories/ADT/adt_value.mli
index 7ebbb8b70b43ea56ddcba85d26960002ae30d950..65b7b63746c381d8b3cac34aa42f78d6a31cb360 100644
--- a/src_colibri2/theories/ADT/adt_value.mli
+++ b/src_colibri2/theories/ADT/adt_value.mli
@@ -1,3 +1,23 @@
+(*************************************************************************)
+(* 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). *)
+(*************************************************************************)
+
open Colibri2_popop_lib.Popop_stdlib
module Case = DInt
module Field = DInt
diff --git a/src_colibri2/theories/LRA/LRA.ml b/src_colibri2/theories/LRA/LRA.ml
index 3065286b53b42ae216d10d6958d30d31935cba1f..b9f35ca932fd77632bf33a7731ec0c7586b5bb2d 100644
--- a/src_colibri2/theories/LRA/LRA.ml
+++ b/src_colibri2/theories/LRA/LRA.ml
@@ -1,7 +1,7 @@
(*************************************************************************)
-(* This file is part of Colibrics. *)
+(* This file is part of Colibri2. *)
(* *)
-(* Copyright (C) 2017 *)
+(* Copyright (C) 2014-2021 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
diff --git a/src_colibri2/theories/LRA/LRA.mli b/src_colibri2/theories/LRA/LRA.mli
index 47b7125b426920ee532c6690eadc103da3b60555..040771d54e0d48c4e944fafa3da4bc4bbff7b026 100644
--- a/src_colibri2/theories/LRA/LRA.mli
+++ b/src_colibri2/theories/LRA/LRA.mli
@@ -1,7 +1,7 @@
(*************************************************************************)
-(* This file is part of Colibrics. *)
+(* This file is part of Colibri2. *)
(* *)
-(* Copyright (C) 2017 *)
+(* Copyright (C) 2014-2021 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
diff --git a/src_colibri2/theories/LRA/delta.ml b/src_colibri2/theories/LRA/delta.ml
index c5e9c5649e27955b50d2b419a7854ee8445df609..dc3448d58e676f3f3a93defce435f2840242cd2b 100644
--- a/src_colibri2/theories/LRA/delta.ml
+++ b/src_colibri2/theories/LRA/delta.ml
@@ -1,3 +1,23 @@
+(*************************************************************************)
+(* 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). *)
+(*************************************************************************)
+
(** Currently the distance graph only store information and reacts to change, it
doesn't compute distances *)
diff --git a/src_colibri2/theories/LRA/delta.mli b/src_colibri2/theories/LRA/delta.mli
index 3724460a6481e911d7e113c59e6fd36e4d57b13f..ff733676e1419c612fbb9bcf6402178613ac3b48 100644
--- a/src_colibri2/theories/LRA/delta.mli
+++ b/src_colibri2/theories/LRA/delta.mli
@@ -1,3 +1,23 @@
+(*************************************************************************)
+(* 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). *)
+(*************************************************************************)
+
(** Distance Graph *)
diff --git a/src_colibri2/theories/LRA/dom_interval.ml b/src_colibri2/theories/LRA/dom_interval.ml
index b362031ac2d2427a188ec0aee5440b3f3359178a..863fd7a35e897d65a1b4d733a9dcb2dfca673119 100644
--- a/src_colibri2/theories/LRA/dom_interval.ml
+++ b/src_colibri2/theories/LRA/dom_interval.ml
@@ -1,7 +1,7 @@
(*************************************************************************)
-(* This file is part of Colibrics. *)
+(* This file is part of Colibri2. *)
(* *)
-(* Copyright (C) 2017 *)
+(* Copyright (C) 2014-2021 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
diff --git a/src_colibri2/theories/LRA/dom_interval.mli b/src_colibri2/theories/LRA/dom_interval.mli
index 3a4919febede97a7d386690b7cce48a468505ff9..d610137c389c06797c86bd4540d4f8b1dcb2fa97 100644
--- a/src_colibri2/theories/LRA/dom_interval.mli
+++ b/src_colibri2/theories/LRA/dom_interval.mli
@@ -1,3 +1,23 @@
+(*************************************************************************)
+(* 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). *)
+(*************************************************************************)
+
val init: Egraph.t -> unit
module D: sig type t end
diff --git a/src_colibri2/theories/LRA/dom_polynome.ml b/src_colibri2/theories/LRA/dom_polynome.ml
index 55052ceef36ff1b5566fcf560817dbe1a1acfd72..a1ad365b619cb201f1d53e80f558b582db671332 100644
--- a/src_colibri2/theories/LRA/dom_polynome.ml
+++ b/src_colibri2/theories/LRA/dom_polynome.ml
@@ -1,7 +1,7 @@
(*************************************************************************)
-(* This file is part of Colibrics. *)
+(* This file is part of Colibri2. *)
(* *)
-(* Copyright (C) 2017 *)
+(* Copyright (C) 2014-2021 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
diff --git a/src_colibri2/theories/LRA/dom_polynome.mli b/src_colibri2/theories/LRA/dom_polynome.mli
index 4c35181721c0457f13343a18e28f870b0c98400e..1b28c48f4a6b1caa39bbc569fd08eb67edcfcf0b 100644
--- a/src_colibri2/theories/LRA/dom_polynome.mli
+++ b/src_colibri2/theories/LRA/dom_polynome.mli
@@ -1,7 +1,7 @@
(*************************************************************************)
-(* This file is part of Colibrics. *)
+(* This file is part of Colibri2. *)
(* *)
-(* Copyright (C) 2017 *)
+(* Copyright (C) 2014-2021 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
diff --git a/src_colibri2/theories/LRA/dom_product.ml b/src_colibri2/theories/LRA/dom_product.ml
index 5907e5f0eb6c24d8ae6eccb5be051c2381cead1b..e0d5b4280336e337bacada303bd13464f378ea4f 100644
--- a/src_colibri2/theories/LRA/dom_product.ml
+++ b/src_colibri2/theories/LRA/dom_product.ml
@@ -1,7 +1,7 @@
(*************************************************************************)
-(* This file is part of Colibrics. *)
+(* This file is part of Colibri2. *)
(* *)
-(* Copyright (C) 2017 *)
+(* Copyright (C) 2014-2021 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
diff --git a/src_colibri2/theories/LRA/dom_product.mli b/src_colibri2/theories/LRA/dom_product.mli
index 79b40b11eaf52bb56014efe779125e21237c893f..06de5f286628f1df6f0ae564b9260b9243b97757 100644
--- a/src_colibri2/theories/LRA/dom_product.mli
+++ b/src_colibri2/theories/LRA/dom_product.mli
@@ -1,7 +1,7 @@
(*************************************************************************)
-(* This file is part of Colibrics. *)
+(* This file is part of Colibri2. *)
(* *)
-(* Copyright (C) 2017 *)
+(* Copyright (C) 2014-2021 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
diff --git a/src_colibri2/theories/LRA/fourier.ml b/src_colibri2/theories/LRA/fourier.ml
index f6e37854985117f4c7366e2ff107401ca448ae1e..118bcebca32fecf7c798f426af4e3355c2203566 100644
--- a/src_colibri2/theories/LRA/fourier.ml
+++ b/src_colibri2/theories/LRA/fourier.ml
@@ -1,3 +1,23 @@
+(*************************************************************************)
+(* 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). *)
+(*************************************************************************)
+
open Colibri2_popop_lib
open Colibri2_core
diff --git a/src_colibri2/theories/LRA/fourier.mli b/src_colibri2/theories/LRA/fourier.mli
index d8be888cc36ed8675a495c4a6d0be604b343f714..13235f23e5aa83b2c72176f55a447150e456da14 100644
--- a/src_colibri2/theories/LRA/fourier.mli
+++ b/src_colibri2/theories/LRA/fourier.mli
@@ -1 +1,21 @@
+(*************************************************************************)
+(* 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). *)
+(*************************************************************************)
+
val init: Egraph.t -> unit
diff --git a/src_colibri2/theories/LRA/integer_sign_domain.ml b/src_colibri2/theories/LRA/integer_sign_domain.ml
index e521eea13acec1a1ce79c4b391ae0a8f2ae6f5ef..69981140f7b9381b9a17cd76b713885f705bdd10 100644
--- a/src_colibri2/theories/LRA/integer_sign_domain.ml
+++ b/src_colibri2/theories/LRA/integer_sign_domain.ml
@@ -1,24 +1,22 @@
-(**************************************************************************)
-(* *)
-(* This file is part of Frama-C. *)
-(* *)
-(* Copyright (C) 2007-2020 *)
-(* 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). *)
-(* *)
-(**************************************************************************)
+(*************************************************************************)
+(* 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). *)
+(*************************************************************************)
(** Sign domain with integer. *)
diff --git a/src_colibri2/theories/LRA/integer_sign_domain.mli b/src_colibri2/theories/LRA/integer_sign_domain.mli
index c2dec4a2df31b4a40a4b296e559c0eefa0b90910..265e418b6ee3ed1051d1590b76e83cff5fac6818 100644
--- a/src_colibri2/theories/LRA/integer_sign_domain.mli
+++ b/src_colibri2/theories/LRA/integer_sign_domain.mli
@@ -1,3 +1,23 @@
+(*************************************************************************)
+(* 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). *)
+(*************************************************************************)
+
include Interval_sig.S
type split_heuristic =
diff --git a/src_colibri2/theories/LRA/interval.ml b/src_colibri2/theories/LRA/interval.ml
index 1086386e90ed0a155ffefdb26ae15e6a13fc9aa8..e1815973636164b5560f038c87404a6283900377 100644
--- a/src_colibri2/theories/LRA/interval.ml
+++ b/src_colibri2/theories/LRA/interval.ml
@@ -1,7 +1,7 @@
(*************************************************************************)
-(* This file is part of Colibrics. *)
+(* This file is part of Colibri2. *)
(* *)
-(* Copyright (C) 2017 *)
+(* Copyright (C) 2014-2021 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
diff --git a/src_colibri2/theories/LRA/interval.mli b/src_colibri2/theories/LRA/interval.mli
index 92d6acbc9d22a7c07d1d57056c86d21c80d06064..6625bb4cef16a785a89793536cc1fafc04bcd54d 100644
--- a/src_colibri2/theories/LRA/interval.mli
+++ b/src_colibri2/theories/LRA/interval.mli
@@ -1,7 +1,7 @@
(*************************************************************************)
-(* This file is part of Colibrics. *)
+(* This file is part of Colibri2. *)
(* *)
-(* Copyright (C) 2017 *)
+(* Copyright (C) 2014-2021 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
diff --git a/src_colibri2/theories/LRA/interval_sig.ml b/src_colibri2/theories/LRA/interval_sig.ml
index 741b47a969d492ccecff27c4270dc74f9e58b211..b318a09f2321469cb9b37a3220dc9d2c09edcac2 100644
--- a/src_colibri2/theories/LRA/interval_sig.ml
+++ b/src_colibri2/theories/LRA/interval_sig.ml
@@ -1,7 +1,7 @@
(*************************************************************************)
-(* This file is part of Colibrics. *)
+(* This file is part of Colibri2. *)
(* *)
-(* Copyright (C) 2017 *)
+(* Copyright (C) 2014-2021 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
diff --git a/src_colibri2/theories/LRA/mul.ml b/src_colibri2/theories/LRA/mul.ml
index 50d80ce3532ac65d55263a8106cbe8a8b91003ad..1cdfdc52d8e9a1e25c95f6c0b5e4d9f34c6c06f8 100644
--- a/src_colibri2/theories/LRA/mul.ml
+++ b/src_colibri2/theories/LRA/mul.ml
@@ -1,3 +1,23 @@
+(*************************************************************************)
+(* 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). *)
+(*************************************************************************)
+
let init,attach =
Demon.Fast.register_get_value_daemon
~name:"Mul.get_value"
diff --git a/src_colibri2/theories/LRA/mul.mli b/src_colibri2/theories/LRA/mul.mli
index d8be888cc36ed8675a495c4a6d0be604b343f714..13235f23e5aa83b2c72176f55a447150e456da14 100644
--- a/src_colibri2/theories/LRA/mul.mli
+++ b/src_colibri2/theories/LRA/mul.mli
@@ -1 +1,21 @@
+(*************************************************************************)
+(* 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). *)
+(*************************************************************************)
+
val init: Egraph.t -> unit
diff --git a/src_colibri2/theories/LRA/polynome.ml b/src_colibri2/theories/LRA/polynome.ml
index 8a7900a48fd398cc9f0e3dc200fbda5543a9b46c..fcec24d7290dc5ee23a52e4f859d126edb3e92f9 100644
--- a/src_colibri2/theories/LRA/polynome.ml
+++ b/src_colibri2/theories/LRA/polynome.ml
@@ -1,7 +1,7 @@
(*************************************************************************)
-(* This file is part of Colibrics. *)
+(* This file is part of Colibri2. *)
(* *)
-(* Copyright (C) 2017 *)
+(* Copyright (C) 2014-2021 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
diff --git a/src_colibri2/theories/LRA/polynome.mli b/src_colibri2/theories/LRA/polynome.mli
index bd9ada2d33d7ad18311f08858158832a6b6a9605..48ac392039a0aa07e17dc3d80308aaf405f5df87 100644
--- a/src_colibri2/theories/LRA/polynome.mli
+++ b/src_colibri2/theories/LRA/polynome.mli
@@ -1,7 +1,7 @@
(*************************************************************************)
-(* This file is part of Colibrics. *)
+(* This file is part of Colibri2. *)
(* *)
-(* Copyright (C) 2017 *)
+(* Copyright (C) 2014-2021 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
diff --git a/src_colibri2/theories/LRA/product.ml b/src_colibri2/theories/LRA/product.ml
index 40da25d94773b4b51fad55937604c40dbd42a4d7..c971e576b0faca9c954ba11e49eb8ac4bb2630ca 100644
--- a/src_colibri2/theories/LRA/product.ml
+++ b/src_colibri2/theories/LRA/product.ml
@@ -1,7 +1,7 @@
(*************************************************************************)
-(* This file is part of Colibrics. *)
+(* This file is part of Colibri2. *)
(* *)
-(* Copyright (C) 2017 *)
+(* Copyright (C) 2014-2021 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
diff --git a/src_colibri2/theories/LRA/product.mli b/src_colibri2/theories/LRA/product.mli
index ae36c765482a33245017f8b0d21cbd0a9e9450e1..dfca11762cac524ef13d534df3469072cad08f74 100644
--- a/src_colibri2/theories/LRA/product.mli
+++ b/src_colibri2/theories/LRA/product.mli
@@ -1,7 +1,7 @@
(*************************************************************************)
-(* This file is part of Colibrics. *)
+(* This file is part of Colibri2. *)
(* *)
-(* Copyright (C) 2017 *)
+(* Copyright (C) 2014-2021 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
diff --git a/src_colibri2/theories/LRA/realValue.ml b/src_colibri2/theories/LRA/realValue.ml
index 4410b095a39f37a255ba00dcec974c93aa892804..4cb58a9943986b5a2d21a2f143facaa5b010e238 100644
--- a/src_colibri2/theories/LRA/realValue.ml
+++ b/src_colibri2/theories/LRA/realValue.ml
@@ -1,7 +1,7 @@
(*************************************************************************)
-(* This file is part of Colibrics. *)
+(* This file is part of Colibri2. *)
(* *)
-(* Copyright (C) 2017 *)
+(* Copyright (C) 2014-2021 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
diff --git a/src_colibri2/theories/LRA/realValue.mli b/src_colibri2/theories/LRA/realValue.mli
index 00551a1e1eb0b18a6c45598bb51cc08900d495f1..4bfd3fa336fa206dc010cf97db1ed7af15cb0b69 100644
--- a/src_colibri2/theories/LRA/realValue.mli
+++ b/src_colibri2/theories/LRA/realValue.mli
@@ -1,7 +1,7 @@
(*************************************************************************)
-(* This file is part of Colibrics. *)
+(* This file is part of Colibri2. *)
(* *)
-(* Copyright (C) 2017 *)
+(* Copyright (C) 2014-2021 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
diff --git a/src_colibri2/theories/LRA/sign_domain.ml b/src_colibri2/theories/LRA/sign_domain.ml
index 5d4cb69a8caf4ca0581c15e3109b698b0afb1454..a4df04b23638d781cd1150ed942323e5f42ed2c4 100644
--- a/src_colibri2/theories/LRA/sign_domain.ml
+++ b/src_colibri2/theories/LRA/sign_domain.ml
@@ -1,24 +1,22 @@
-(**************************************************************************)
-(* *)
-(* This file is part of Frama-C. *)
-(* *)
-(* Copyright (C) 2007-2020 *)
-(* 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). *)
-(* *)
-(**************************************************************************)
+(*************************************************************************)
+(* 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). *)
+(*************************************************************************)
(** Sign domain: abstraction of integer numerical values by their signs. *)
(** From frama-c *)
diff --git a/src_colibri2/theories/LRA/sign_domain.mli b/src_colibri2/theories/LRA/sign_domain.mli
index 65ed7df7e9ee27b6b3d8b6cf3c773fa6f59e3be1..f8a18f2a9b49ad745234c9cd2432fff3bc21b02e 100644
--- a/src_colibri2/theories/LRA/sign_domain.mli
+++ b/src_colibri2/theories/LRA/sign_domain.mli
@@ -1,3 +1,23 @@
+(*************************************************************************)
+(* 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). *)
+(*************************************************************************)
+
type t = private {
pos: bool;
zero: bool;
diff --git a/src_colibri2/theories/bool/boolean.ml b/src_colibri2/theories/bool/boolean.ml
index 7b8ce5a3032c9b12f4cf78d376cf1ccf5c29e9e8..77e415502a0a0215ff3ad303d6de3c4dadb97a9c 100644
--- a/src_colibri2/theories/bool/boolean.ml
+++ b/src_colibri2/theories/bool/boolean.ml
@@ -1,7 +1,7 @@
(*************************************************************************)
-(* This file is part of Colibrics. *)
+(* This file is part of Colibri2. *)
(* *)
-(* Copyright (C) 2017 *)
+(* Copyright (C) 2014-2021 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
diff --git a/src_colibri2/theories/bool/boolean.mli b/src_colibri2/theories/bool/boolean.mli
index c170d909a91cbf1b4d9e1c134194952667f24cca..b44c27b845cb39f81a58dc55d464365e65fba9e6 100644
--- a/src_colibri2/theories/bool/boolean.mli
+++ b/src_colibri2/theories/bool/boolean.mli
@@ -1,7 +1,7 @@
(*************************************************************************)
-(* This file is part of Colibrics. *)
+(* This file is part of Colibri2. *)
(* *)
-(* Copyright (C) 2017 *)
+(* Copyright (C) 2014-2021 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
diff --git a/src_colibri2/theories/bool/equality.ml b/src_colibri2/theories/bool/equality.ml
index b0234ea78d25d869cbfbb0ee016579919fe5ff4e..e30cfc12bb799508e48094becdc5b08f46faa4ad 100644
--- a/src_colibri2/theories/bool/equality.ml
+++ b/src_colibri2/theories/bool/equality.ml
@@ -1,7 +1,7 @@
(*************************************************************************)
-(* This file is part of Colibrics. *)
+(* This file is part of Colibri2. *)
(* *)
-(* Copyright (C) 2017 *)
+(* Copyright (C) 2014-2021 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
diff --git a/src_colibri2/theories/bool/equality.mli b/src_colibri2/theories/bool/equality.mli
index 9cabfdec56988d640632da5fdd913006a125c820..c9cbc7b0fbf16c1aa381443bd10d751ac3e123a6 100644
--- a/src_colibri2/theories/bool/equality.mli
+++ b/src_colibri2/theories/bool/equality.mli
@@ -1,7 +1,7 @@
(*************************************************************************)
-(* This file is part of Colibrics. *)
+(* This file is part of Colibri2. *)
(* *)
-(* Copyright (C) 2017 *)
+(* Copyright (C) 2014-2021 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
diff --git a/src_colibri2/theories/quantifier/F.ml b/src_colibri2/theories/quantifier/F.ml
index 5808c457a971f835439327de691ea08d85f10171..6f94c1d7dba6f9a6d7856b0843c5dc20decdbcdb 100644
--- a/src_colibri2/theories/quantifier/F.ml
+++ b/src_colibri2/theories/quantifier/F.ml
@@ -1,2 +1,22 @@
+(*************************************************************************)
+(* 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). *)
+(*************************************************************************)
+
include Expr.Term.Const
module EnvApps = Datastructure.Memo (Expr.Term.Const)
diff --git a/src_colibri2/theories/quantifier/FA.ml b/src_colibri2/theories/quantifier/FA.ml
index 3e0c8f7612b4da815f36cdea2974d1144c1e322d..513ee4dd50f706cf2c65d43a5e4468a37a730ea7 100644
--- a/src_colibri2/theories/quantifier/FA.ml
+++ b/src_colibri2/theories/quantifier/FA.ml
@@ -1,3 +1,23 @@
+(*************************************************************************)
+(* 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). *)
+(*************************************************************************)
+
(** instantiated function symbol *)
module T = struct
let hash_fold_list = Base.hash_fold_list
diff --git a/src_colibri2/theories/quantifier/F_Pos.ml b/src_colibri2/theories/quantifier/F_Pos.ml
index 129677c36ef3b8d9b3d1814504ae94f3a6be1722..8b6d370faa5addaf52a1e04a9dde87341ebb25bb 100644
--- a/src_colibri2/theories/quantifier/F_Pos.ml
+++ b/src_colibri2/theories/quantifier/F_Pos.ml
@@ -1,3 +1,23 @@
+(*************************************************************************)
+(* 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). *)
+(*************************************************************************)
+
open Colibri2_popop_lib
(** A position inside a function symbol *)
diff --git a/src_colibri2/theories/quantifier/F_Pos.mli b/src_colibri2/theories/quantifier/F_Pos.mli
index 147e5028a5b0f1c5dfa9e808e40a55323364fa3d..eb5281b9b4c53b98f5e74c93cc52ff441ec5552a 100644
--- a/src_colibri2/theories/quantifier/F_Pos.mli
+++ b/src_colibri2/theories/quantifier/F_Pos.mli
@@ -1,3 +1,23 @@
+(*************************************************************************)
+(* 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). *)
+(*************************************************************************)
+
(** A position inside a function symbol *)
type t = { f : F.t; pos : int }
diff --git a/src_colibri2/theories/quantifier/InvertedPath.ml b/src_colibri2/theories/quantifier/InvertedPath.ml
index 7cfbd188b89b626c02b7e1cac3c19b2f12fde9d5..3949f617514b4d1091bc934c2f4a486f9f46e772 100644
--- a/src_colibri2/theories/quantifier/InvertedPath.ml
+++ b/src_colibri2/theories/quantifier/InvertedPath.ml
@@ -1,3 +1,23 @@
+(*************************************************************************)
+(* 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). *)
+(*************************************************************************)
+
open Colibri2_popop_lib
open Common
diff --git a/src_colibri2/theories/quantifier/InvertedPath.mli b/src_colibri2/theories/quantifier/InvertedPath.mli
index 9c0eda7e93c61d16d63c13b49ebd8603892dd1d7..c2a1ed3b00e6a45e23b63414a4faf088e0d904b6 100644
--- a/src_colibri2/theories/quantifier/InvertedPath.mli
+++ b/src_colibri2/theories/quantifier/InvertedPath.mli
@@ -1,3 +1,23 @@
+(*************************************************************************)
+(* 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). *)
+(*************************************************************************)
+
type t
(** An InvertedPath is a way to go from one subterm of patterns to substitution
of triggers. It allows to know which nodes merge can create new substitutions
diff --git a/src_colibri2/theories/quantifier/PC.ml b/src_colibri2/theories/quantifier/PC.ml
index 76c828be09f150182287660eb1929be3ed50281c..beb25bb7372b4351b0aa6288056255aaa4720d17 100644
--- a/src_colibri2/theories/quantifier/PC.ml
+++ b/src_colibri2/theories/quantifier/PC.ml
@@ -1,3 +1,23 @@
+(*************************************************************************)
+(* 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). *)
+(*************************************************************************)
+
open Colibri2_popop_lib
module T = struct
diff --git a/src_colibri2/theories/quantifier/PC.mli b/src_colibri2/theories/quantifier/PC.mli
index f6c39f6f0cd9609dfb88e94812f6be59255c4803..aea6513bec8d673ca3a54058f3c8dbbf33750b3f 100644
--- a/src_colibri2/theories/quantifier/PC.mli
+++ b/src_colibri2/theories/quantifier/PC.mli
@@ -1,3 +1,23 @@
+(*************************************************************************)
+(* 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). *)
+(*************************************************************************)
+
type t = { parent : F_Pos.t; child : F.t }
include Colibri2_popop_lib.Popop_stdlib.Datatype with type t := t
diff --git a/src_colibri2/theories/quantifier/PN.ml b/src_colibri2/theories/quantifier/PN.ml
index 608538eee64be34a3ba710a916e1da17e8443051..5990eb675cf8781a70fc434a9099a66e4014dd94 100644
--- a/src_colibri2/theories/quantifier/PN.ml
+++ b/src_colibri2/theories/quantifier/PN.ml
@@ -1,3 +1,23 @@
+(*************************************************************************)
+(* 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). *)
+(*************************************************************************)
+
open Colibri2_popop_lib
module T = struct
diff --git a/src_colibri2/theories/quantifier/PN.mli b/src_colibri2/theories/quantifier/PN.mli
index d3a676cbfc8cd76096d719beb2780c611e061bea..48104c257805f314e0c166226900fd2f2466d0f7 100644
--- a/src_colibri2/theories/quantifier/PN.mli
+++ b/src_colibri2/theories/quantifier/PN.mli
@@ -1,3 +1,23 @@
+(*************************************************************************)
+(* 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). *)
+(*************************************************************************)
+
type t = { parent : F_Pos.t; node : Node.t }
include Colibri2_popop_lib.Popop_stdlib.Datatype with type t := t
diff --git a/src_colibri2/theories/quantifier/PP.ml b/src_colibri2/theories/quantifier/PP.ml
index 903815458c0456c1ff3e7a3ad570e1f8e5564212..4a664df579c5a2a8f3fdce125906f4a167ac76bc 100644
--- a/src_colibri2/theories/quantifier/PP.ml
+++ b/src_colibri2/theories/quantifier/PP.ml
@@ -1,3 +1,23 @@
+(*************************************************************************)
+(* 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). *)
+(*************************************************************************)
+
open Colibri2_popop_lib
module T = struct
diff --git a/src_colibri2/theories/quantifier/PP.mli b/src_colibri2/theories/quantifier/PP.mli
index 3302a3c13bfa8ae939ea5f0d7672e103defdf366..64acb2a2e05358ff1700ac6fc21d04f730b0267f 100644
--- a/src_colibri2/theories/quantifier/PP.mli
+++ b/src_colibri2/theories/quantifier/PP.mli
@@ -1,3 +1,23 @@
+(*************************************************************************)
+(* 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). *)
+(*************************************************************************)
+
type t = private { parent1 : F_Pos.t; parent2 : F_Pos.t }
include Colibri2_popop_lib.Popop_stdlib.Datatype with type t := t
diff --git a/src_colibri2/theories/quantifier/common.ml b/src_colibri2/theories/quantifier/common.ml
index 694237dad67d2ad624c69dbdda3297947169d63b..21405040cbc515923e3598c6dc50d84b9a0741a2 100644
--- a/src_colibri2/theories/quantifier/common.ml
+++ b/src_colibri2/theories/quantifier/common.ml
@@ -1,3 +1,23 @@
+(*************************************************************************)
+(* 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). *)
+(*************************************************************************)
+
open Colibri2_popop_lib
let debug =
diff --git a/src_colibri2/theories/quantifier/info.ml b/src_colibri2/theories/quantifier/info.ml
index df42bb012d5d6047d81ffcea5544d31acc4146d4..632f809a725f105ee129c8f8dc530b3bd4ef786f 100644
--- a/src_colibri2/theories/quantifier/info.ml
+++ b/src_colibri2/theories/quantifier/info.ml
@@ -1,3 +1,23 @@
+(*************************************************************************)
+(* 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). *)
+(*************************************************************************)
+
open Colibri2_popop_lib
(** information added on nodes *)
diff --git a/src_colibri2/theories/quantifier/info.mli b/src_colibri2/theories/quantifier/info.mli
index 2b8dc01718aa3bd8b69be51c34b18e880cce7614..700c2c538a4cbe16f3b91485ac9b686258d70c5a 100644
--- a/src_colibri2/theories/quantifier/info.mli
+++ b/src_colibri2/theories/quantifier/info.mli
@@ -1,3 +1,23 @@
+(*************************************************************************)
+(* 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). *)
+(*************************************************************************)
+
type t = {
parents : Ground.S.t F_Pos.M.t; (** parents *)
apps : Ground.S.t F.M.t; (** parent parent *)
diff --git a/src_colibri2/theories/quantifier/pattern.ml b/src_colibri2/theories/quantifier/pattern.ml
index 3412d3f4e3665d485736a329adc11c464131ca39..3128b8e30edba07caaddf9be88160243e4edbf2b 100644
--- a/src_colibri2/theories/quantifier/pattern.ml
+++ b/src_colibri2/theories/quantifier/pattern.ml
@@ -1,3 +1,23 @@
+(*************************************************************************)
+(* 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). *)
+(*************************************************************************)
+
open Colibri2_popop_lib
open Common
diff --git a/src_colibri2/theories/quantifier/pattern.mli b/src_colibri2/theories/quantifier/pattern.mli
index b820c35f9c8544e239cdd913d32398f0b3a68c07..235ef0f2243a9c8cc6f759e6600a6fe4504ba68c 100644
--- a/src_colibri2/theories/quantifier/pattern.mli
+++ b/src_colibri2/theories/quantifier/pattern.mli
@@ -1,3 +1,23 @@
+(*************************************************************************)
+(* 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). *)
+(*************************************************************************)
+
open Colibri2_popop_lib
(** Pattern *)
diff --git a/src_colibri2/theories/quantifier/quantifier.ml b/src_colibri2/theories/quantifier/quantifier.ml
index aff0944fd316b4c6e51e3b22add75dba38c18ddf..6f9e1f57f6c5fdb4cc7b53a4ce40e3a57411fad7 100644
--- a/src_colibri2/theories/quantifier/quantifier.ml
+++ b/src_colibri2/theories/quantifier/quantifier.ml
@@ -1,3 +1,23 @@
+(*************************************************************************)
+(* 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). *)
+(*************************************************************************)
+
(** Cf Efficient E-Matching paper *)
open Colibri2_popop_lib
diff --git a/src_colibri2/theories/quantifier/quantifier.mli b/src_colibri2/theories/quantifier/quantifier.mli
index 884026c74ee750b2b496458a099a43bc544199eb..164992ff9d314b8f5fddd6a1590b44eda2fea37a 100644
--- a/src_colibri2/theories/quantifier/quantifier.mli
+++ b/src_colibri2/theories/quantifier/quantifier.mli
@@ -1 +1,21 @@
+(*************************************************************************)
+(* 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). *)
+(*************************************************************************)
+
val th_register : Egraph.t -> unit
diff --git a/src_colibri2/theories/quantifier/trigger.ml b/src_colibri2/theories/quantifier/trigger.ml
index d8f35bb6fe4f6765172eafe3c049228186a8b3a7..c4c447bfef6cfa98f2ea6249eadb446df9f710f8 100644
--- a/src_colibri2/theories/quantifier/trigger.ml
+++ b/src_colibri2/theories/quantifier/trigger.ml
@@ -1,3 +1,23 @@
+(*************************************************************************)
+(* 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). *)
+(*************************************************************************)
+
open Colibri2_popop_lib
open Common
diff --git a/src_colibri2/theories/quantifier/trigger.mli b/src_colibri2/theories/quantifier/trigger.mli
index f1cffad60119edd3722a7759d38c383a7174dde6..8dca75064344fd38259726a93fb7f547e878a07d 100644
--- a/src_colibri2/theories/quantifier/trigger.mli
+++ b/src_colibri2/theories/quantifier/trigger.mli
@@ -1,3 +1,23 @@
+(*************************************************************************)
+(* 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). *)
+(*************************************************************************)
+
(** Trigger *)
type t = {
diff --git a/src_colibri2/theories/quantifier/uninterp.ml b/src_colibri2/theories/quantifier/uninterp.ml
index a20932dd6e3327da0d9cb355d099fcdb57f4c42b..a4e4615acb714becba5019404e8ee69603944eb1 100644
--- a/src_colibri2/theories/quantifier/uninterp.ml
+++ b/src_colibri2/theories/quantifier/uninterp.ml
@@ -1,7 +1,7 @@
(*************************************************************************)
-(* This file is part of Colibrics. *)
+(* This file is part of Colibri2. *)
(* *)
-(* Copyright (C) 2017 *)
+(* Copyright (C) 2014-2021 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
diff --git a/src_colibri2/theories/quantifier/uninterp.mli b/src_colibri2/theories/quantifier/uninterp.mli
index 952f5027f455f345b23dc94a86afd6618e392910..f3a82959478d744b5ebece6c54e7e623ca228b1d 100644
--- a/src_colibri2/theories/quantifier/uninterp.mli
+++ b/src_colibri2/theories/quantifier/uninterp.mli
@@ -1,7 +1,7 @@
(*************************************************************************)
-(* This file is part of Colibrics. *)
+(* This file is part of Colibri2. *)
(* *)
-(* Copyright (C) 2017 *)
+(* Copyright (C) 2014-2021 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)