From df1274e0da758189fc3e8383f5559293bae3d9b7 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Bobot?= <francois.bobot@cea.fr>
Date: Mon, 9 Nov 2020 16:19:00 +0100
Subject: [PATCH] Rename Witan module into Colibri2
---
Makefile | 2 +-
TODO | 2 +-
witan.opam => colibri2.opam | 8 ++---
compare_smt2.sh | 2 +-
dune-project | 6 ++--
misc/header.txt | 2 +-
misc/header_witan.txt | 2 +-
src/core/{witan_core.ml => colibri2_core.ml} | 2 +-
src/core/demon.ml | 2 +-
src/core/demon.mli | 2 +-
src/core/dune | 12 ++++----
src/core/egraph.ml | 4 +--
src/core/egraph.mli | 2 +-
src/core/events.ml | 2 +-
src/core/events.mli | 2 +-
src/core/interp.ml | 2 +-
src/core/structures/domKind.ml | 2 +-
src/core/structures/dune | 10 +++---
src/core/structures/expr.ml | 4 +--
src/core/structures/nodes.ml | 2 +-
src/core/structures/nodes.mli | 2 +-
src/core/structures/ty.ml | 2 +-
src/core/structures/ty.mli | 2 +-
src/core/synTerm.ml | 4 +--
src/core/synTerm.mli | 2 +-
src/popop_lib/dune | 6 ++--
src/solver/dune | 12 ++++----
src/solver/scheduler.ml | 4 +--
src/stdlib/comp_keys.ml | 2 +-
src/stdlib/comp_keys.mli | 4 +--
src/stdlib/dune | 8 ++---
src/stdlib/hashtbl_hetero.ml | 2 +-
src/stdlib/hashtbl_hetero.mli | 2 +-
src/stdlib/hashtbl_hetero_sig.ml | 2 +-
src/stdlib/keys.ml | 6 ++--
src/stdlib/keys.mli | 2 +-
src/stdlib/keys_sig.ml | 2 +-
src/stdlib/map_hetero.ml | 4 +--
src/stdlib/map_hetero.mli | 2 +-
src/stdlib/map_hetero_sig.ml | 2 +-
src/stdlib/std.ml | 6 ++--
src/stdlib/std.mli | 4 +--
src/tests/dune | 4 +--
src/tests/test.ml | 6 ++--
src/tests/tests.ml | 22 +++++++-------
src/tests/tests_LRA.ml | 12 ++++----
src/tests/tests_bool.ml | 6 ++--
src/tests/tests_lib.ml | 32 ++++++++++----------
src/tests/tests_uf.ml | 4 +--
src/theories/LRA/LRA.ml | 8 ++---
src/theories/LRA/dune | 14 ++++-----
src/theories/LRA/interval.ml | 4 +--
src/theories/LRA/interval.mli | 2 +-
src/theories/LRA/interval_sig.ml | 2 +-
src/theories/LRA/polynome.ml | 4 +--
src/theories/LRA/polynome.mli | 4 +--
src/theories/bool/boolean.ml | 6 ++--
src/theories/bool/dune | 12 ++++----
src/theories/bool/equality.ml | 8 ++---
src/theories/bool/uninterp.ml | 4 +--
src/theories/bool/uninterp.mli | 2 +-
tests/Makefile | 4 +--
tests/parsing/Makefile | 2 +-
63 files changed, 159 insertions(+), 157 deletions(-)
rename witan.opam => colibri2.opam (79%)
rename src/core/{witan_core.ml => colibri2_core.ml} (97%)
diff --git a/Makefile b/Makefile
index 41301c8a8..b0cc4f226 100644
--- a/Makefile
+++ b/Makefile
@@ -74,7 +74,7 @@ COLIBRICS_FILES = Makefile \
headers:
headache -c misc/headache_config.txt -h misc/header_colibrics.txt \
$(COLIBRICS_FILES)
- headache -c misc/headache_config.txt -h misc/header_witan.txt \
+ headache -c misc/headache_config.txt -h misc/header_colibri2.txt \
$(WITAN_FILES)
headache -c misc/headache_config.txt -h misc/header_why3.txt \
$(WHY3_FILES)
diff --git a/TODO b/TODO
index ae0024e7c..40be70549 100644
--- a/TODO
+++ b/TODO
@@ -1,5 +1,5 @@
- .header file for easy inclusion to new files
-- separate witan into two packages (witan-lib and witan-bin)
+- separate colibri2 into two packages (colibri2-lib and colibri2-bin)
- naming:
diff --git a/witan.opam b/colibri2.opam
similarity index 79%
rename from witan.opam
rename to colibri2.opam
index 003c44222..6b7ae8991 100644
--- a/witan.opam
+++ b/colibri2.opam
@@ -1,5 +1,5 @@
opam-version: "1.2"
-name: "witan"
+name: "colibri2"
license: "LGPL v3"
version: "dev"
author: ["François Bobot" "Guillaume Bury" "Simon Cruanes" "Stéphane Graham-Lengrand"]
@@ -37,6 +37,6 @@ available: [
ocaml-version >= "4.03.0"
]
tags: [ "sat" "smt" "mcsat" ]
-homepage: "https://github.com/Gbury/witan"
-dev-repo: "https://github.com/Gbury/witan.git"
-bug-reports: "https://github.com/Gbury/witan/issues/"
+homepage: "https://github.com/Gbury/colibri2"
+dev-repo: "https://github.com/Gbury/colibri2.git"
+bug-reports: "https://github.com/Gbury/colibri2/issues/"
diff --git a/compare_smt2.sh b/compare_smt2.sh
index 917796462..b068c4af8 100755
--- a/compare_smt2.sh
+++ b/compare_smt2.sh
@@ -25,7 +25,7 @@ else
fi
-if test "$CVC4" = "$(_build/default/src/bin/witan.exe $SEED $STEP --input=smt2 $1 2>&1)"; then
+if test "$CVC4" = "$(_build/default/src/bin/colibri2.exe $SEED $STEP --input=smt2 $1 2>&1)"; then
exit $OK
else
exit $BAD
diff --git a/dune-project b/dune-project
index 51d5c322e..be360b9f1 100644
--- a/dune-project
+++ b/dune-project
@@ -1,5 +1,7 @@
-(lang dune 2.0)
+(lang dune 2.7)
-(name witan)
+(name colibri2)
+
+(package (name colibri2))
(formatting disabled)
diff --git a/misc/header.txt b/misc/header.txt
index 1bfa61664..50a403db9 100644
--- a/misc/header.txt
+++ b/misc/header.txt
@@ -1,4 +1,4 @@
-This file is part of Witan.
+This file is part of Colibri2.
Copyright (C) 2017
CEA (Commissariat à l'énergie atomique et aux énergies
diff --git a/misc/header_witan.txt b/misc/header_witan.txt
index 1bfa61664..50a403db9 100644
--- a/misc/header_witan.txt
+++ b/misc/header_witan.txt
@@ -1,4 +1,4 @@
-This file is part of Witan.
+This file is part of Colibri2.
Copyright (C) 2017
CEA (Commissariat à l'énergie atomique et aux énergies
diff --git a/src/core/witan_core.ml b/src/core/colibri2_core.ml
similarity index 97%
rename from src/core/witan_core.ml
rename to src/core/colibri2_core.ml
index 0092fca85..f8db92ec3 100644
--- a/src/core/witan_core.ml
+++ b/src/core/colibri2_core.ml
@@ -18,7 +18,7 @@
(* for more details (enclosed in the file licenses/LGPLv2.1). *)
(*************************************************************************)
-(** Witan core: define basic types and the solver *)
+(** Colibri2 core: define basic types and the solver *)
module Expr = Expr
module Term = Expr.Term
diff --git a/src/core/demon.ml b/src/core/demon.ml
index 09d1ff4d4..eb2fecf18 100644
--- a/src/core/demon.ml
+++ b/src/core/demon.ml
@@ -18,7 +18,7 @@
(* for more details (enclosed in the file licenses/LGPLv2.1). *)
(*************************************************************************)
-open Witan_popop_lib
+open Colibri2_popop_lib
open Nodes
let debug = Debug.register_info_flag
diff --git a/src/core/demon.mli b/src/core/demon.mli
index 6e35c272e..b08972866 100644
--- a/src/core/demon.mli
+++ b/src/core/demon.mli
@@ -18,7 +18,7 @@
(* for more details (enclosed in the file licenses/LGPLv2.1). *)
(*************************************************************************)
-open Witan_popop_lib
+open Colibri2_popop_lib
open Nodes
module Create : sig
diff --git a/src/core/dune b/src/core/dune
index 8d1fbe7c8..e278424fd 100644
--- a/src/core/dune
+++ b/src/core/dune
@@ -1,12 +1,12 @@
(library
- (name witan_core)
- (public_name witan.core)
- (synopsis "core for witan, e.g. trail, egraph")
- (libraries containers ocamlgraph str witan.stdlib witan.popop_lib
- witan_core_structures)
+ (name colibri2_core)
+ (public_name colibri2.core)
+ (synopsis "core for colibri2, e.g. trail, egraph")
+ (libraries containers ocamlgraph str colibri2.stdlib colibri2.popop_lib
+ colibri2_core_structures)
(preprocess
(pps ppx_deriving.std))
(flags :standard -w +a-4-42-44-48-50-58-32-60-40-9@8 -color always -open
- Containers -open Witan_stdlib -open Std -open Witan_core_structures)
+ Containers -open Colibri2_stdlib -open Std -open Colibri2_core_structures)
(ocamlopt_flags :standard -O3 -bin-annot -unbox-closures
-unbox-closures-factor 20))
diff --git a/src/core/egraph.ml b/src/core/egraph.ml
index 676983319..465a0e1ed 100644
--- a/src/core/egraph.ml
+++ b/src/core/egraph.ml
@@ -18,7 +18,7 @@
(* for more details (enclosed in the file licenses/LGPLv2.1). *)
(*************************************************************************)
-open Witan_popop_lib
+open Colibri2_popop_lib
open Popop_stdlib
open Nodes
@@ -1145,4 +1145,4 @@ let () = Exn_printer.register (fun fmt exn ->
| exn -> raise exn
)
-let print_decision = Witan_popop_lib.Debug.register_flag ~desc:"Print@ information@ about@ the@ decisions@ made" "decision"
+let print_decision = Colibri2_popop_lib.Debug.register_flag ~desc:"Print@ information@ about@ the@ decisions@ made" "decision"
diff --git a/src/core/egraph.mli b/src/core/egraph.mli
index b140de46f..3321434f6 100644
--- a/src/core/egraph.mli
+++ b/src/core/egraph.mli
@@ -182,4 +182,4 @@ module Backtrackable: sig
val output_graph : string -> t -> unit
end
-val print_decision: Witan_popop_lib.Debug.flag
+val print_decision: Colibri2_popop_lib.Debug.flag
diff --git a/src/core/events.ml b/src/core/events.ml
index 1018ab6ee..a6ae04a86 100644
--- a/src/core/events.ml
+++ b/src/core/events.ml
@@ -18,7 +18,7 @@
(* for more details (enclosed in the file licenses/LGPLv2.1). *)
(*************************************************************************)
-open Witan_popop_lib
+open Colibri2_popop_lib
open Nodes
let debug = Debug.register_info_flag ~desc:"for the events" "Egraph.events"
diff --git a/src/core/events.mli b/src/core/events.mli
index b0cc4b93c..b072b79ab 100644
--- a/src/core/events.mli
+++ b/src/core/events.mli
@@ -18,7 +18,7 @@
(* for more details (enclosed in the file licenses/LGPLv2.1). *)
(*************************************************************************)
-open Witan_popop_lib
+open Colibri2_popop_lib
open Nodes
module Fired : sig
diff --git a/src/core/interp.ml b/src/core/interp.ml
index e2733450d..541ffa3ec 100644
--- a/src/core/interp.ml
+++ b/src/core/interp.ml
@@ -18,7 +18,7 @@
(* for more details (enclosed in the file licenses/LGPLv2.1). *)
(*************************************************************************)
-open Witan_popop_lib
+open Colibri2_popop_lib
open Std
module Register = struct
diff --git a/src/core/structures/domKind.ml b/src/core/structures/domKind.ml
index 554a11367..006a458eb 100644
--- a/src/core/structures/domKind.ml
+++ b/src/core/structures/domKind.ml
@@ -18,7 +18,7 @@
(* for more details (enclosed in the file licenses/LGPLv2.1). *)
(*************************************************************************)
-open Witan_popop_lib
+open Colibri2_popop_lib
open Nodes
let debug = Debug.register_info_flag
diff --git a/src/core/structures/dune b/src/core/structures/dune
index 4325fb4ac..c2f3e18fa 100644
--- a/src/core/structures/dune
+++ b/src/core/structures/dune
@@ -1,12 +1,12 @@
(library
- (name witan_core_structures)
- (public_name witan.core.structures)
+ (name colibri2_core_structures)
+ (public_name colibri2.core.structures)
(synopsis
- "core structures for witan, e.g. terms, semantic terms, values, etc")
- (libraries containers ocamlgraph witan.stdlib witan.popop_lib str dolmen.std)
+ "core structures for colibri2, e.g. terms, semantic terms, values, etc")
+ (libraries containers ocamlgraph colibri2.stdlib colibri2.popop_lib str dolmen.std)
(preprocess
(pps ppx_deriving.std))
(flags :standard -w +a-4-42-44-48-50-58-32-60-40-9@8 -color always -open
- Containers -open Witan_stdlib -open Std)
+ Containers -open Colibri2_stdlib -open Std)
(ocamlopt_flags :standard -O3 -bin-annot -unbox-closures
-unbox-closures-factor 20))
diff --git a/src/core/structures/expr.ml b/src/core/structures/expr.ml
index 35ec88fcc..d6b5be6b6 100644
--- a/src/core/structures/expr.ml
+++ b/src/core/structures/expr.ml
@@ -6,7 +6,7 @@ module Ty = struct
let pp = print
let hash_fold_t state t = Base.Hash.fold_int state (hash t)
- include Witan_popop_lib.Popop_stdlib.MkDatatype(struct
+ include Colibri2_popop_lib.Popop_stdlib.MkDatatype(struct
type nonrec t = t
let equal = equal
let compare = compare
@@ -20,7 +20,7 @@ module Term = struct
include Dolmen_std.Expr.Term
let pp = print
- include Witan_popop_lib.Popop_stdlib.MkDatatype(struct
+ include Colibri2_popop_lib.Popop_stdlib.MkDatatype(struct
type nonrec t = t
let equal = equal
let compare = compare
diff --git a/src/core/structures/nodes.ml b/src/core/structures/nodes.ml
index 34954cb3b..ad82ca99c 100644
--- a/src/core/structures/nodes.ml
+++ b/src/core/structures/nodes.ml
@@ -18,7 +18,7 @@
(* for more details (enclosed in the file licenses/LGPLv2.1). *)
(*************************************************************************)
-open Witan_popop_lib
+open Colibri2_popop_lib
open Popop_stdlib
exception BrokenInvariant of string
diff --git a/src/core/structures/nodes.mli b/src/core/structures/nodes.mli
index 149bf12ec..45ca30607 100644
--- a/src/core/structures/nodes.mli
+++ b/src/core/structures/nodes.mli
@@ -20,7 +20,7 @@
(** Define the Node, and the related types semantic terms and value *)
-open Witan_popop_lib
+open Colibri2_popop_lib
open Popop_stdlib
(** {2 General exceptions (to move away) } *)
diff --git a/src/core/structures/ty.ml b/src/core/structures/ty.ml
index 54a99f843..64377ee75 100644
--- a/src/core/structures/ty.ml
+++ b/src/core/structures/ty.ml
@@ -24,7 +24,7 @@ include Dolmen_std.Expr.Ty
let pp = Dolmen_std.Expr.Ty.print
-include Witan_popop_lib.Popop_stdlib.MkDatatype(struct
+include Colibri2_popop_lib.Popop_stdlib.MkDatatype(struct
type nonrec t = t
let equal = equal
let compare = compare
diff --git a/src/core/structures/ty.mli b/src/core/structures/ty.mli
index 87ff9fe6e..958ea89fa 100644
--- a/src/core/structures/ty.mli
+++ b/src/core/structures/ty.mli
@@ -18,7 +18,7 @@
(* for more details (enclosed in the file licenses/LGPLv2.1). *)
(*************************************************************************)
-open Witan_popop_lib
+open Colibri2_popop_lib
open Popop_stdlib
(** {2 Types} *)
diff --git a/src/core/synTerm.ml b/src/core/synTerm.ml
index 2dacf209c..9161e0cad 100644
--- a/src/core/synTerm.ml
+++ b/src/core/synTerm.ml
@@ -1,5 +1,5 @@
(*************************************************************************)
-(* This file is part of Witan. *)
+(* This file is part of Colibri2. *)
(* *)
(* Copyright (C) 2017 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
@@ -21,7 +21,7 @@
(* for more details (enclosed in the file licenses/LGPLv2.1). *)
(*************************************************************************)
-open Witan_popop_lib
+open Colibri2_popop_lib
open Nodes
let synsem = ThTermKind.create_key (module struct type t = Expr.Term.t let name = "syntax" end)
diff --git a/src/core/synTerm.mli b/src/core/synTerm.mli
index 17bf2bce8..60f4fda96 100644
--- a/src/core/synTerm.mli
+++ b/src/core/synTerm.mli
@@ -1,5 +1,5 @@
(*************************************************************************)
-(* This file is part of Witan. *)
+(* This file is part of Colibri2. *)
(* *)
(* Copyright (C) 2017 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
diff --git a/src/popop_lib/dune b/src/popop_lib/dune
index c3b02b218..85fbd0542 100644
--- a/src/popop_lib/dune
+++ b/src/popop_lib/dune
@@ -1,9 +1,9 @@
; library to replace by containers
(library
- (name witan_popop_lib)
- (public_name witan.popop_lib)
- (synopsis "Temporary for witan (intended to be replaced by another library)")
+ (name colibri2_popop_lib)
+ (public_name colibri2.popop_lib)
+ (synopsis "Temporary for colibri2 (intended to be replaced by another library)")
(libraries str unix zarith base)
(flags :standard -w +a-4-42-44-48-50-58-32-60-40-9@8 -color always)
(ocamlopt_flags :standard -O3 -bin-annot -unbox-closures
diff --git a/src/solver/dune b/src/solver/dune
index d22b11cfc..9202fb656 100644
--- a/src/solver/dune
+++ b/src/solver/dune
@@ -1,12 +1,12 @@
(library
- (name witan_solver)
- (public_name witan.solver)
- (synopsis "witan's solver")
- (libraries containers zarith ocamlgraph gen dolmen spelll witan.stdlib
- witan.popop_lib str witan.core witan.core.structures dolmen_loop)
+ (name colibri2_solver)
+ (public_name colibri2.solver)
+ (synopsis "colibri2's solver")
+ (libraries containers zarith ocamlgraph gen dolmen spelll colibri2.stdlib
+ colibri2.popop_lib str colibri2.core colibri2.core.structures dolmen_loop)
(preprocess
(pps ppx_deriving.std))
(flags :standard -w +a-4-42-44-48-50-58-32-60-40-9@8 -color always -open
- Witan_stdlib -open Witan_core)
+ Colibri2_stdlib -open Colibri2_core)
(ocamlopt_flags :standard -O3 -bin-annot -unbox-closures
-unbox-closures-factor 20))
diff --git a/src/solver/scheduler.ml b/src/solver/scheduler.ml
index e5a5352f7..50c8a377e 100644
--- a/src/solver/scheduler.ml
+++ b/src/solver/scheduler.ml
@@ -18,8 +18,8 @@
(* for more details (enclosed in the file licenses/LGPLv2.1). *)
(*************************************************************************)
-open Witan_popop_lib
-open Witan_core
+open Colibri2_popop_lib
+open Colibri2_core
let debug = Debug.register_info_flag
~desc:"for the scheduler in the simple version"
diff --git a/src/stdlib/comp_keys.ml b/src/stdlib/comp_keys.ml
index 4d91321fe..1c00173b6 100644
--- a/src/stdlib/comp_keys.ml
+++ b/src/stdlib/comp_keys.ml
@@ -18,7 +18,7 @@
(* for more details (enclosed in the file licenses/LGPLv2.1). *)
(*************************************************************************)
-open Witan_popop_lib
+open Colibri2_popop_lib
open Popop_stdlib
open Std
diff --git a/src/stdlib/comp_keys.mli b/src/stdlib/comp_keys.mli
index 88f37bfbc..35c486811 100644
--- a/src/stdlib/comp_keys.mli
+++ b/src/stdlib/comp_keys.mli
@@ -1,5 +1,5 @@
(*************************************************************************)
-(* This file is part of Witan. *)
+(* This file is part of Colibri2. *)
(* *)
(* Copyright (C) 2017 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
@@ -26,7 +26,7 @@
(** Keys are the main programming tools used for implementing
extensible types (sem, value, dom, pexp, ...) *)
-open Witan_popop_lib
+open Colibri2_popop_lib
open Popop_stdlib
open Std
diff --git a/src/stdlib/dune b/src/stdlib/dune
index 55423e337..9211aaf66 100644
--- a/src/stdlib/dune
+++ b/src/stdlib/dune
@@ -1,8 +1,8 @@
(library
- (name witan_stdlib)
- (public_name witan.stdlib)
- (synopsis "Stdlib for witan")
- (libraries zarith containers witan_popop_lib)
+ (name colibri2_stdlib)
+ (public_name colibri2.stdlib)
+ (synopsis "Stdlib for colibri2")
+ (libraries zarith containers colibri2_popop_lib)
(preprocess
(pps ppx_optcomp ppx_deriving.std ppx_hash))
(flags :standard -w +a-4-42-44-48-50-58-32-60-40-9@8 -color always -open
diff --git a/src/stdlib/hashtbl_hetero.ml b/src/stdlib/hashtbl_hetero.ml
index 836b43b0f..f83555bf4 100644
--- a/src/stdlib/hashtbl_hetero.ml
+++ b/src/stdlib/hashtbl_hetero.ml
@@ -1,5 +1,5 @@
(*************************************************************************)
-(* This file is part of Witan. *)
+(* This file is part of Colibri2. *)
(* *)
(* Copyright (C) 2017 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
diff --git a/src/stdlib/hashtbl_hetero.mli b/src/stdlib/hashtbl_hetero.mli
index 13d65943a..ee817fff9 100644
--- a/src/stdlib/hashtbl_hetero.mli
+++ b/src/stdlib/hashtbl_hetero.mli
@@ -1,5 +1,5 @@
(*************************************************************************)
-(* This file is part of Witan. *)
+(* This file is part of Colibri2. *)
(* *)
(* Copyright (C) 2017 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
diff --git a/src/stdlib/hashtbl_hetero_sig.ml b/src/stdlib/hashtbl_hetero_sig.ml
index aad9c5c31..7f32aed63 100644
--- a/src/stdlib/hashtbl_hetero_sig.ml
+++ b/src/stdlib/hashtbl_hetero_sig.ml
@@ -1,5 +1,5 @@
(*************************************************************************)
-(* This file is part of Witan. *)
+(* This file is part of Colibri2. *)
(* *)
(* Copyright (C) 2017 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
diff --git a/src/stdlib/keys.ml b/src/stdlib/keys.ml
index cc80c6e58..19ba8d71d 100644
--- a/src/stdlib/keys.ml
+++ b/src/stdlib/keys.ml
@@ -24,9 +24,9 @@
open Std
-module Strings = Witan_popop_lib.Strings
-module StringH = Witan_popop_lib.Popop_stdlib.DStr.H
-module Exn_printer = Witan_popop_lib.Exn_printer
+module Strings = Colibri2_popop_lib.Strings
+module StringH = Colibri2_popop_lib.Popop_stdlib.DStr.H
+module Exn_printer = Colibri2_popop_lib.Exn_printer
include Keys_sig
diff --git a/src/stdlib/keys.mli b/src/stdlib/keys.mli
index ccaac1447..30a534cd4 100644
--- a/src/stdlib/keys.mli
+++ b/src/stdlib/keys.mli
@@ -1,5 +1,5 @@
(*************************************************************************)
-(* This file is part of Witan. *)
+(* This file is part of Colibri2. *)
(* *)
(* Copyright (C) 2017 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
diff --git a/src/stdlib/keys_sig.ml b/src/stdlib/keys_sig.ml
index 4db140df3..6ae7792bd 100644
--- a/src/stdlib/keys_sig.ml
+++ b/src/stdlib/keys_sig.ml
@@ -1,5 +1,5 @@
(*************************************************************************)
-(* This file is part of Witan. *)
+(* This file is part of Colibri2. *)
(* *)
(* Copyright (C) 2017 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
diff --git a/src/stdlib/map_hetero.ml b/src/stdlib/map_hetero.ml
index c389e5fff..1563821d9 100644
--- a/src/stdlib/map_hetero.ml
+++ b/src/stdlib/map_hetero.ml
@@ -1,5 +1,5 @@
(*************************************************************************)
-(* This file is part of Witan. *)
+(* This file is part of Colibri2. *)
(* *)
(* Copyright (C) 2017 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
@@ -22,7 +22,7 @@
(*************************************************************************)
open Std
-open Witan_popop_lib
+open Colibri2_popop_lib
include Map_hetero_sig
diff --git a/src/stdlib/map_hetero.mli b/src/stdlib/map_hetero.mli
index 346474949..870cdd757 100644
--- a/src/stdlib/map_hetero.mli
+++ b/src/stdlib/map_hetero.mli
@@ -1,5 +1,5 @@
(*************************************************************************)
-(* This file is part of Witan. *)
+(* This file is part of Colibri2. *)
(* *)
(* Copyright (C) 2017 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
diff --git a/src/stdlib/map_hetero_sig.ml b/src/stdlib/map_hetero_sig.ml
index 65b913c97..a6e27e7e0 100644
--- a/src/stdlib/map_hetero_sig.ml
+++ b/src/stdlib/map_hetero_sig.ml
@@ -1,5 +1,5 @@
(*************************************************************************)
-(* This file is part of Witan. *)
+(* This file is part of Colibri2. *)
(* *)
(* Copyright (C) 2017 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
diff --git a/src/stdlib/std.ml b/src/stdlib/std.ml
index 2b0a8bc46..bed8dab10 100644
--- a/src/stdlib/std.ml
+++ b/src/stdlib/std.ml
@@ -1,5 +1,5 @@
(*************************************************************************)
-(* This file is part of Witan. *)
+(* This file is part of Colibri2. *)
(* *)
(* Copyright (C) 2017 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
@@ -72,7 +72,7 @@ module Q = struct
)
end
include Arg
- include Witan_popop_lib.Popop_stdlib.MkDatatype(Arg)
+ include Colibri2_popop_lib.Popop_stdlib.MkDatatype(Arg)
let two = Q.of_int 2
let ge = Q.geq
let le = Q.leq
@@ -95,7 +95,7 @@ module Q = struct
let l = String.length dec in
let dec = Q.of_string dec in
let ten = Q.of_int 10 in
- Witan_popop_lib.Util.foldi (fun acc _ -> Q.(acc * ten)) dec 1 l
+ Colibri2_popop_lib.Util.foldi (fun acc _ -> Q.(acc * ten)) dec 1 l
in
Q.(sgn * (int_part + dec_part))
diff --git a/src/stdlib/std.mli b/src/stdlib/std.mli
index 2ec37f57c..041b1e0d9 100644
--- a/src/stdlib/std.mli
+++ b/src/stdlib/std.mli
@@ -1,5 +1,5 @@
(*************************************************************************)
-(* This file is part of Witan. *)
+(* This file is part of Colibri2. *)
(* *)
(* Copyright (C) 2017 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
@@ -52,7 +52,7 @@ end
module Q : sig
include module type of Q
- include Witan_popop_lib.Popop_stdlib.Datatype with type t := t
+ include Colibri2_popop_lib.Popop_stdlib.Datatype with type t := t
val two : t
val ge : t -> t -> bool
val le : t -> t -> bool
diff --git a/src/tests/dune b/src/tests/dune
index 6d4e4271a..010bdcbd5 100644
--- a/src/tests/dune
+++ b/src/tests/dune
@@ -1,8 +1,8 @@
(executable
(modes byte exe)
(name tests)
- (libraries containers witan.core witan.theories.bool witan.theories.LRA
- ounit2 witan.solver witan.stdlib)
+ (libraries containers colibri2.core colibri2.theories.bool colibri2.theories.LRA
+ ounit2 colibri2.solver colibri2.stdlib)
(flags :standard -w +a-4-42-44-48-50-58-32-60-9@8 -color always)
(ocamlopt_flags :standard -O3 -unbox-closures -unbox-closures-factor 20))
diff --git a/src/tests/test.ml b/src/tests/test.ml
index 779a2037e..5d8d12caa 100644
--- a/src/tests/test.ml
+++ b/src/tests/test.ml
@@ -19,8 +19,8 @@
(*************************************************************************)
let () =
- (* let solver = Witan_core.Egraph.new_t () in *)
- (* let d = Witan_core.Egraph. *)
- (* Witan_theories_bool.Bool.th_register solver; *)
+ (* let solver = Colibri2_core.Egraph.new_t () in *)
+ (* let d = Colibri2_core.Egraph. *)
+ (* Colibri2_theories_bool.Bool.th_register solver; *)
Format.printf "All tests OK ! (total: 0)@."
diff --git a/src/tests/tests.ml b/src/tests/tests.ml
index 9c0630752..9a3751374 100644
--- a/src/tests/tests.ml
+++ b/src/tests/tests.ml
@@ -19,8 +19,8 @@
(*************************************************************************)
open OUnit2
-(* open Witan_stdlib
- * open Witan_core
+(* open Colibri2_stdlib
+ * open Colibri2_core
* open Tests_lib *)
@@ -32,7 +32,7 @@ let print_seed fmt = function
| _ -> assert false
let make_tests acc seed =
- let test = ((Witan_popop_lib.Pp.sprintf "seed %a" print_seed seed) >:::
+ let test = ((Colibri2_popop_lib.Pp.sprintf "seed %a" print_seed seed) >:::
[ Tests_bool.tests; Tests_uf.tests; Tests_LRA.tests ])
in
(* let test = test_decorate
@@ -40,7 +40,7 @@ let make_tests acc seed =
test::acc
let tests () =
- let l = Witan_popop_lib.Util.foldi (fun acc i -> make_tests acc (Some [|i|])) []
+ let l = Colibri2_popop_lib.Util.foldi (fun acc i -> make_tests acc (Some [|i|])) []
(!opt_seed + 1) (!opt_seed + 9)in
make_tests l None
@@ -53,7 +53,7 @@ let tests () =
* try f ()
* with
* | exn ->
- * Format.fprintf (Witan_popop_lib.Debug.get_debug_formatter ()) "%s"
+ * Format.fprintf (Colibri2_popop_lib.Debug.get_debug_formatter ()) "%s"
* (Printexc.get_backtrace ());
* raise exn
* )) (test_list (tests ()))
@@ -102,8 +102,8 @@ let tests () =
* (fun x -> raise (Arg.Bad ("Bad argument : " ^ x)))
* ("usage: " ^ Sys.argv.(0) ^ " [-verbose] [-only-test path]*")
* in
- * let () = Witan_popop_lib.Debug.Args.set_flags_selected () in
- * let verbose = Witan_popop_lib.Debug.test_flag debug in
+ * let () = Colibri2_popop_lib.Debug.Args.set_flags_selected () in
+ * let verbose = Colibri2_popop_lib.Debug.test_flag debug in
* let nsuite =
* if !only_test = [] then
* suite ()
@@ -135,11 +135,11 @@ let tests () =
* run_test_tt_main
* ~arg_specs:(["--seed",Arg.Set_int opt_seed,
* " Base seed used for shuffling the arbitrary decision";
- * Witan_popop_lib.Debug.Args.desc_debug_all]@
- * Witan_popop_lib.Debug.Args.desc_debug)
+ * Colibri2_popop_lib.Debug.Args.desc_debug_all]@
+ * Colibri2_popop_lib.Debug.Args.desc_debug)
* tests
- * with e when not (Witan_popop_lib.Debug.test_flag Witan_popop_lib.Debug.stack_trace) ->
- * Format.eprintf "%a" Witan_popop_lib.Exn_printer.exn_printer e;
+ * with e when not (Colibri2_popop_lib.Debug.test_flag Colibri2_popop_lib.Debug.stack_trace) ->
+ * Format.eprintf "%a" Colibri2_popop_lib.Exn_printer.exn_printer e;
* exit 1 *)
let () = run_test_tt_main (tests ())
diff --git a/src/tests/tests_LRA.ml b/src/tests/tests_LRA.ml
index 493318dbb..ca8db34a7 100644
--- a/src/tests/tests_LRA.ml
+++ b/src/tests/tests_LRA.ml
@@ -20,12 +20,12 @@
open OUnit2
open Tests_lib
-open Witan_theories_bool
-open Witan_theories_LRA
-open Witan_solver
-open Witan_core
-open Witan_stdlib.Std
-open Witan_stdlib
+open Colibri2_theories_bool
+open Colibri2_theories_LRA
+open Colibri2_solver
+open Colibri2_core
+open Colibri2_stdlib.Std
+open Colibri2_stdlib
let theories = [Boolean.th_register; Equality.th_register; Uninterp.th_register; LRA.th_register]
diff --git a/src/tests/tests_bool.ml b/src/tests/tests_bool.ml
index e2958df8d..13502dfbf 100644
--- a/src/tests/tests_bool.ml
+++ b/src/tests/tests_bool.ml
@@ -19,10 +19,10 @@
(*************************************************************************)
open OUnit2
-open Witan_stdlib
-open Witan_core
+open Colibri2_stdlib
+open Colibri2_core
open Tests_lib
-open Witan_theories_bool
+open Colibri2_theories_bool
let theories = [(* Uninterp.th_register; *) Boolean.th_register]
diff --git a/src/tests/tests_lib.ml b/src/tests/tests_lib.ml
index 3ae0cca61..7654a26c1 100644
--- a/src/tests/tests_lib.ml
+++ b/src/tests/tests_lib.ml
@@ -19,8 +19,8 @@
(*************************************************************************)
open OUnit2
-open Witan_popop_lib
-open Witan_core
+open Colibri2_popop_lib
+open Colibri2_core
let debug = Debug.register_flag
~desc:" Run the test in verbose mode." "ounit"
@@ -44,15 +44,15 @@ let is_equal = Egraph.is_equal
type t =
{ wakeup_daemons : Events.Wait.daemon_key Queue.t;
solver_state : Egraph.Backtrackable.t;
- context : Witan_stdlib.Context.context;
+ context : Colibri2_stdlib.Context.context;
}
let new_solver () =
- let context = Witan_stdlib.Context.create () in
+ let context = Colibri2_stdlib.Context.create () in
{
wakeup_daemons = Queue.create ();
- solver_state = Egraph.Backtrackable.new_t (Witan_stdlib.Context.creator context);
+ solver_state = Egraph.Backtrackable.new_t (Colibri2_stdlib.Context.creator context);
context;
}
@@ -64,22 +64,22 @@ let new_delayed t =
exception ReachStepLimit
exception Contradiction
-let run_exn = Witan_solver.Scheduler.run_exn
+let run_exn = Colibri2_solver.Scheduler.run_exn
let check_file ?limit ~theories filename =
let st =
- Witan_solver.Input.mk_state
+ Colibri2_solver.Input.mk_state
~input:(`File filename)
theories
~bt:false
in
- Witan_solver.Input.read
+ Colibri2_solver.Input.read
~show_checksat_result:false
?limit
- ~set_true:Witan_theories_bool.Boolean.set_true
- ~handle_exn:Witan_solver.Input.handle_exn_with_error
+ ~set_true:Colibri2_theories_bool.Boolean.set_true
+ ~handle_exn:Colibri2_solver.Input.handle_exn_with_error
st;
- let r = st.Witan_solver.Input.State.solve_state.Witan_solver.Input.state in
+ let r = st.Colibri2_solver.Input.State.solve_state.Colibri2_solver.Input.state in
match r with
| `Sat _ -> `Sat
| `Unsat -> `Unsat
@@ -97,19 +97,19 @@ let tests_file ?limit ~theories expected dir =
s >: test_case (fun _ ->
begin match check_file ?limit ~theories (Filename.concat dir s) with
| `Sat ->
- Witan_popop_lib.Debug.dprintf1 debug "@[%s: Sat@]" s;
+ Colibri2_popop_lib.Debug.dprintf1 debug "@[%s: Sat@]" s;
assert_bool s (`Sat = expected)
| `Unsat ->
- Witan_popop_lib.Debug.dprintf1 debug "@[%s: Unsat@]" s;
+ Colibri2_popop_lib.Debug.dprintf1 debug "@[%s: Unsat@]" s;
assert_bool s (`Unsat = expected)
| `Unknown ->
- Witan_popop_lib.Debug.dprintf1 debug "@[%s: Unknown@]" s;
+ Colibri2_popop_lib.Debug.dprintf1 debug "@[%s: Unknown@]" s;
assert_bool s (`Unknown = expected)
| `StepLimitReached ->
- Witan_popop_lib.Debug.dprintf0 debug "StepLimit Reached@.";
+ Colibri2_popop_lib.Debug.dprintf0 debug "StepLimit Reached@.";
assert_bool s false
| exception exn ->
- Witan_popop_lib.Debug.dprintf2 debug "@.Error: %s@.%s@."
+ Colibri2_popop_lib.Debug.dprintf2 debug "@.Error: %s@.%s@."
(Printexc.to_string exn)
(Printexc.get_backtrace ());
assert_bool s false;
diff --git a/src/tests/tests_uf.ml b/src/tests/tests_uf.ml
index 831c3e37e..1d7005b4d 100644
--- a/src/tests/tests_uf.ml
+++ b/src/tests/tests_uf.ml
@@ -20,9 +20,9 @@
open OUnit2
-open Witan_core
+open Colibri2_core
open Tests_lib
-open Witan_theories_bool
+open Colibri2_theories_bool
let theories = [Boolean.th_register; Equality.th_register; Uninterp.th_register ]
let run = Tests_lib.run_exn ~theories ~nodec:()
diff --git a/src/theories/LRA/LRA.ml b/src/theories/LRA/LRA.ml
index 976d80a1b..afbfacf8e 100644
--- a/src/theories/LRA/LRA.ml
+++ b/src/theories/LRA/LRA.ml
@@ -19,9 +19,9 @@
(*************************************************************************)
(** This module use one domain and two semantic values. *)
-open Witan_popop_lib
-open Witan_core
-open Witan_stdlib.Std
+open Colibri2_popop_lib
+open Colibri2_core
+open Colibri2_stdlib.Std
let debug = Debug.register_info_flag
~desc:"for the arithmetic theory"
@@ -666,7 +666,7 @@ let default_value = Q.zero
(* let () =
* Interp.Register.model Term._Real (fun d n ->
* let v = Egraph.get_value d real n in
- * let v = Witan_popop_lib.Opt.get_def default_value v in
+ * let v = Colibri2_popop_lib.Opt.get_def default_value v in
* let v = RealValue.nodevalue (RealValue.index v Term._Real) in
* v) *)
diff --git a/src/theories/LRA/dune b/src/theories/LRA/dune
index 5e065072a..5a2ed7841 100644
--- a/src/theories/LRA/dune
+++ b/src/theories/LRA/dune
@@ -1,13 +1,13 @@
(library
- (name witan_theories_LRA)
- (public_name witan.theories.LRA)
- (synopsis "theories for witan")
- (libraries containers ocamlgraph witan.stdlib witan.popop_lib
- witan.core.structures witan.core witan.theories.bool)
+ (name colibri2_theories_LRA)
+ (public_name colibri2.theories.LRA)
+ (synopsis "theories for colibri2")
+ (libraries containers ocamlgraph colibri2.stdlib colibri2.popop_lib
+ colibri2.core.structures colibri2.core colibri2.theories.bool)
(preprocess
(pps ppx_deriving.std))
(flags :standard -w +a-4-42-44-48-50-58-32-60-40-9@8 -color always -open
- Containers -open Witan_stdlib -open Std -open Witan_core -open
- Witan_theories_bool)
+ Containers -open Colibri2_stdlib -open Std -open Colibri2_core -open
+ Colibri2_theories_bool)
(ocamlopt_flags :standard -O3 -bin-annot -unbox-closures
-unbox-closures-factor 20))
diff --git a/src/theories/LRA/interval.ml b/src/theories/LRA/interval.ml
index 9d6981004..3713d6c89 100644
--- a/src/theories/LRA/interval.ml
+++ b/src/theories/LRA/interval.ml
@@ -18,8 +18,8 @@
(* for more details (enclosed in the file licenses/LGPLv2.1). *)
(*************************************************************************)
-open Witan_popop_lib
-open Witan_stdlib.Std
+open Colibri2_popop_lib
+open Colibri2_stdlib.Std
type bound = Interval_sig.bound = Strict | Large [@@deriving eq]
diff --git a/src/theories/LRA/interval.mli b/src/theories/LRA/interval.mli
index c174fcf53..b6ca6b7b7 100644
--- a/src/theories/LRA/interval.mli
+++ b/src/theories/LRA/interval.mli
@@ -18,7 +18,7 @@
(* for more details (enclosed in the file licenses/LGPLv2.1). *)
(*************************************************************************)
-open Witan_popop_lib
+open Colibri2_popop_lib
type bound = Interval_sig.bound = Strict | Large
diff --git a/src/theories/LRA/interval_sig.ml b/src/theories/LRA/interval_sig.ml
index 2a5dbc342..0b16c1049 100644
--- a/src/theories/LRA/interval_sig.ml
+++ b/src/theories/LRA/interval_sig.ml
@@ -18,7 +18,7 @@
(* for more details (enclosed in the file licenses/LGPLv2.1). *)
(*************************************************************************)
-open Witan_popop_lib
+open Colibri2_popop_lib
type bound = Strict | Large
diff --git a/src/theories/LRA/polynome.ml b/src/theories/LRA/polynome.ml
index c9ffe4ff5..db919d46d 100644
--- a/src/theories/LRA/polynome.ml
+++ b/src/theories/LRA/polynome.ml
@@ -18,8 +18,8 @@
(* for more details (enclosed in the file licenses/LGPLv2.1). *)
(*************************************************************************)
-open Witan_popop_lib
-open Witan_core
+open Colibri2_popop_lib
+open Colibri2_core
module T = struct
type t = { cst : Q.t; poly : Q.t Node.M.t}
diff --git a/src/theories/LRA/polynome.mli b/src/theories/LRA/polynome.mli
index 5f68c9980..3f5a6f053 100644
--- a/src/theories/LRA/polynome.mli
+++ b/src/theories/LRA/polynome.mli
@@ -18,8 +18,8 @@
(* for more details (enclosed in the file licenses/LGPLv2.1). *)
(*************************************************************************)
-open Witan_popop_lib
-open Witan_core
+open Colibri2_popop_lib
+open Colibri2_core
(** Polynome *)
type t = private { cst : Q.t; poly : Q.t Node.M.t}
diff --git a/src/theories/bool/boolean.ml b/src/theories/bool/boolean.ml
index 3121fa1d8..51cc5d579 100644
--- a/src/theories/bool/boolean.ml
+++ b/src/theories/bool/boolean.ml
@@ -18,10 +18,10 @@
(* for more details (enclosed in the file licenses/LGPLv2.1). *)
(*************************************************************************)
-open Witan_popop_lib
+open Colibri2_popop_lib
open Popop_stdlib
open Std
-open Witan_core
+open Colibri2_core
let lazy_propagation = false
@@ -488,7 +488,7 @@ let default_value = true
(* let () =
* Interp.Register.model ty (fun d n ->
* let v = Egraph.get_value d dom n in
- * let v = Witan_popop_lib.Opt.get_def default_value v in
+ * let v = Colibri2_popop_lib.Opt.get_def default_value v in
* let v = if v then values_true else values_false in
* v) *)
diff --git a/src/theories/bool/dune b/src/theories/bool/dune
index 382900492..4d9ae2883 100644
--- a/src/theories/bool/dune
+++ b/src/theories/bool/dune
@@ -1,13 +1,13 @@
(library
- (name witan_theories_bool)
- (public_name witan.theories.bool)
- (synopsis "theories for witan")
+ (name colibri2_theories_bool)
+ (public_name colibri2.theories.bool)
+ (synopsis "theories for colibri2")
(modules Boolean Equality Uninterp)
- (libraries containers ocamlgraph witan.stdlib witan.popop_lib
- witan.core.structures witan.core dolmen.std)
+ (libraries containers ocamlgraph colibri2.stdlib colibri2.popop_lib
+ colibri2.core.structures colibri2.core dolmen.std)
(preprocess
(pps ppx_deriving.std ppx_hash))
(flags :standard -w +a-4-42-44-48-50-58-32-60-40-9@8 -color always -open
- Containers -open Witan_stdlib -open Std -open Witan_core)
+ Containers -open Colibri2_stdlib -open Std -open Colibri2_core)
(ocamlopt_flags :standard -O3 -bin-annot -unbox-closures
-unbox-closures-factor 20))
diff --git a/src/theories/bool/equality.ml b/src/theories/bool/equality.ml
index 9776c7aff..925afc195 100644
--- a/src/theories/bool/equality.ml
+++ b/src/theories/bool/equality.ml
@@ -18,9 +18,9 @@
(* for more details (enclosed in the file licenses/LGPLv2.1). *)
(*************************************************************************)
-open Witan_popop_lib
+open Colibri2_popop_lib
open Popop_stdlib
-open Witan_core
+open Colibri2_core
let debug = Debug.register_info_flag
~desc:"for the equality and disequality predicate"
@@ -477,7 +477,7 @@ module RDaemonInitITE = Demon.Fast.Register(DaemonInitITE)
let iter_on_value_different
(type a)
(type b)
- ((module Val): (module Witan_core.ValueKind.Registered with type s = a and type t = b))
+ ((module Val): (module Colibri2_core.ValueKind.Registered with type s = a and type t = b))
~they_are_different
(d:Egraph.t)
(own:Node.t) =
@@ -498,7 +498,7 @@ let iter_on_value_different
let init_diff_to_value (type a) (type b)
?(already_registered=([]: b list))
d0
- ((module Val): (module Witan_core.ValueKind.Registered with type s = a and type t = b))
+ ((module Val): (module Colibri2_core.ValueKind.Registered with type s = a and type t = b))
~(they_are_different:(Egraph.t -> Node.t -> a -> unit)) =
let propagate_diff d v =
diff --git a/src/theories/bool/uninterp.ml b/src/theories/bool/uninterp.ml
index d00c58666..ddf336ff5 100644
--- a/src/theories/bool/uninterp.ml
+++ b/src/theories/bool/uninterp.ml
@@ -18,9 +18,9 @@
(* for more details (enclosed in the file licenses/LGPLv2.1). *)
(*************************************************************************)
-open Witan_popop_lib
+open Colibri2_popop_lib
open Popop_stdlib
-open Witan_core
+open Colibri2_core
let debug = Debug.register_info_flag
~desc:"for the uninterpreted function theory"
diff --git a/src/theories/bool/uninterp.mli b/src/theories/bool/uninterp.mli
index 92a2ddf1d..0b1398ace 100644
--- a/src/theories/bool/uninterp.mli
+++ b/src/theories/bool/uninterp.mli
@@ -18,7 +18,7 @@
(* for more details (enclosed in the file licenses/LGPLv2.1). *)
(*************************************************************************)
-open Witan_core
+open Colibri2_core
module Th: sig
type t =
diff --git a/tests/Makefile b/tests/Makefile
index 45609a4fa..ceb4b6c39 100644
--- a/tests/Makefile
+++ b/tests/Makefile
@@ -1,5 +1,5 @@
-BIN=witan.exe
+BIN=colibri2.exe
all: $(BIN)
@cd parsing && $(MAKE) --no-print-directory
@@ -9,5 +9,5 @@ clean:
cd parsing && $(MAKE) clean
$(BIN):
- @ln -f -s ../_build/default/src/bin/witan.exe witan.exe
+ @ln -f -s ../_build/default/src/bin/colibri2.exe colibri2.exe
diff --git a/tests/parsing/Makefile b/tests/parsing/Makefile
index 00160b8e3..f0998128c 100644
--- a/tests/parsing/Makefile
+++ b/tests/parsing/Makefile
@@ -1,5 +1,5 @@
-BIN=../witan.exe
+BIN=../colibri2.exe
TESTS=$(patsubst %.p,%.res,$(wildcard *.p))
all: $(TESTS)
--
GitLab