diff --git a/.vscode/tasks.json b/.vscode/tasks.json
new file mode 100644
index 0000000000000000000000000000000000000000..40afd29e1176384633a3af8ad0bb69a193a433ce
--- /dev/null
+++ b/.vscode/tasks.json
@@ -0,0 +1,16 @@
+{
+ "version": "2.0.0",
+ "tasks": [
+ {
+ "type": "dune",
+ "problemMatcher": [
+ "$ocamlc"
+ ],
+ "group": {
+ "kind": "build",
+ "isDefault": true
+ },
+ "label": "dune: build @runtest"
+ }
+ ]
+}
\ No newline at end of file
diff --git a/CHANGES b/CHANGES
index e11b4d6918add2c85160afdf6a248390a94f50d8..b9ffa7b8ba2a6d7ae9113b8fe7a22dbde785a9b9 100644
--- a/CHANGES
+++ b/CHANGES
@@ -1,3 +1,12 @@
+## Release 0.4
+ * Decision: Fix delayed decisions handling
+ * Array: experimental theory
+ * Quantifier: Improve eager instanciation heuristic
+ * Quantifier: Avoid creating new term
+ * Simplex: Fix redundant run
+ * Fix compilation in 32bit
+ * Fix sign of sqrt
+
## Release 0.3.3
* Bump cmdliner version
* Bump OCaml version
diff --git a/colibri2.opam b/colibri2.opam
index e6d656934a70d34c99e813c0f19e3c79490b4ae8..767dc0d27c16fd71c082d383d729d6434146575f 100644
--- a/colibri2.opam
+++ b/colibri2.opam
@@ -8,8 +8,9 @@ authors: [
"Bruno Marre"
"Guillaume Bury"
"Stéphane Graham-Lengrand"
+ "Hichem Rami Ait El Hara"
]
-license: "LGPL-2.1"
+license: "LGPL-2.1-only"
homepage: "https://colibri.frama-c.com"
bug-reports: "https://git.frama-c.com/pub/colibrics/issues"
depends: [
diff --git a/colibri2/popop_lib/bag.ml b/colibri2/popop_lib/bag.ml
index 4f3ff8024fb7dbe3b3c88893d3bc481ed99c7b97..70e985ec69c3f965f9388f4a92586bbac4d9bf52 100644
--- a/colibri2/popop_lib/bag.ml
+++ b/colibri2/popop_lib/bag.ml
@@ -31,6 +31,7 @@ type 'a t =
| App of 'a t * 'a
| List of 'a list
| Concat of 'a t * 'a t
+ [@@ deriving eq]
let empty = Empty
let elt x = Elt x
@@ -222,4 +223,4 @@ let rec collect t xs =
let elements t = collect t []
-let pp sep pelt fmt t = Pp.iter1 iter sep pelt fmt t
+let pp pelt fmt t = Pp.iter1 iter Pp.comma pelt fmt t
diff --git a/colibri2/popop_lib/bag.mli b/colibri2/popop_lib/bag.mli
index 20a788d2bd59af8cc4b0ef9fc335cd47ad59ddd2..87c7382d682f834d89b17c5cd5c2246d7de8523b 100644
--- a/colibri2/popop_lib/bag.mli
+++ b/colibri2/popop_lib/bag.mli
@@ -24,7 +24,8 @@
@since Carbon-20101201
*)
-type 'a t
+type 'a t [@@ deriving eq]
+
val empty : 'a t
val elt : 'a -> 'a t
@@ -58,6 +59,5 @@ val elements : 'a t -> 'a list
val choose: 'a t -> 'a
val pp:
- (unit Pp.pp) ->
('a Pp.pp) ->
'a t Pp.pp
diff --git a/colibri2/theories/LRA/dom_polynome.ml b/colibri2/theories/LRA/dom_polynome.ml
index a5e5679f337b467b98e7a1cb7e829131a832aa66..e0ed82c8bc0802494e5ec340208a31f86577f348 100644
--- a/colibri2/theories/LRA/dom_polynome.ml
+++ b/colibri2/theories/LRA/dom_polynome.ml
@@ -136,4 +136,11 @@ let init env =
let cl = RealValue.node value in
let p1 = Polynome.of_list v [] in
assume_equality d cl p1);
- Ground.register_converter env converter
+ Ground.register_converter env converter;
+ Disequality.register_disequal env (fun d n1 n2 ->
+ match (get_repr d n1, get_repr d n2) with
+ | Some p1, Some p2 -> (
+ match Polynome.is_cst (Polynome.sub p1 p2) with
+ | Some c when A.is_not_zero c -> true
+ | _ -> false)
+ | _ -> false)
diff --git a/colibri2/theories/LRA/pivot.ml b/colibri2/theories/LRA/pivot.ml
index 006ab309406a6487eba94f756ffaf53c44879b21..e726eb092e81b731f9f54ca3bc4569b9be4b53b1 100644
--- a/colibri2/theories/LRA/pivot.ml
+++ b/colibri2/theories/LRA/pivot.ml
@@ -446,7 +446,7 @@ end = struct
end)
let used_in_poly : Node.t Bag.t Node.HC.t =
- Node.HC.create (Bag.pp Pp.semi Node.pp) "used_in_poly"
+ Node.HC.create (Bag.pp Node.pp) "used_in_poly"
let set_poly d cl old_ new_ =
Egraph.set_dom d dom cl new_;
diff --git a/colibri2/theories/bool/.ocamlformat b/colibri2/theories/bool/.ocamlformat
deleted file mode 100644
index e69de29bb2d1d6434b8b29ae775ad8c2e48c5391..0000000000000000000000000000000000000000
diff --git a/colibri2/theories/bool/disequality.ml b/colibri2/theories/bool/disequality.ml
new file mode 100644
index 0000000000000000000000000000000000000000..92c9d5bcc23bd63c2c54667bb13ccb83c999ecac
--- /dev/null
+++ b/colibri2/theories/bool/disequality.ml
@@ -0,0 +1,40 @@
+(*************************************************************************)
+(* 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_core
+
+let disequal_hook = Datastructure.Push.create Fmt.nop "disequal_hook"
+
+let register_disequal d f = Datastructure.Push.push disequal_hook d f
+
+let update_hook = Datastructure.Push.create Fmt.nop "update_hook"
+
+let register_update d f = Datastructure.Push.push update_hook d f
+
+let is_disequal d n1 n2 =
+ try
+ Datastructure.Push.iter ~f:(fun f -> if f d n1 n2 then raise Exit)
+ disequal_hook d;
+ false
+ with Exit -> true
+
+let update_disequality d n1 check =
+ Datastructure.Push.iter ~f:(fun f -> f d n1 check )
+ update_hook d;
diff --git a/colibri2/theories/bool/disequality.mli b/colibri2/theories/bool/disequality.mli
new file mode 100644
index 0000000000000000000000000000000000000000..0773a4ba57fe4d519e9fa95b1252db0cea860998
--- /dev/null
+++ b/colibri2/theories/bool/disequality.mli
@@ -0,0 +1,42 @@
+(*************************************************************************)
+(* 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 is_disequal: Egraph.wt -> Node.t -> Node.t -> bool
+(** [is_disequal d n1 n2] indicates if n1 and n2 are known to be distinct *)
+
+val register_disequal: Egraph.wt ->
+ (Egraph.wt -> Node.t -> Node.t -> bool)
+ -> unit
+(** [register_disequal f d] Register function [f] to test disequality *)
+
+val update_disequality:
+ Egraph.wt -> Node.t -> (Egraph.wt -> Node.t -> bool) ->
+ unit
+(** [update_disequality upd d n] warn that the disequality with [n] could have
+ changed
+ *)
+
+val register_update:
+Egraph.wt -> (Egraph.wt -> Node.t -> (Egraph.wt -> Node.t -> bool) -> unit) -> unit
+
+(** [new_daemon d f] registers a function [f] where [f n1 g] is called when the
+ disequalities of n1 could have changed, [g] allows to check for such
+ new or not disequalities.
+*)
diff --git a/colibri2/theories/bool/dune b/colibri2/theories/bool/dune
index 8927926f2c775a5fa79ac81ab3d7e1b30a4ac3d1..c42c056bb9781f2ba9b9521a2aba4d9318363ee0 100644
--- a/colibri2/theories/bool/dune
+++ b/colibri2/theories/bool/dune
@@ -2,7 +2,6 @@
(name colibri2_theories_bool)
(public_name colibri2.theories.bool)
(synopsis "theories for colibri2")
- (modules Boolean Equality)
(libraries
containers
ocamlgraph
diff --git a/colibri2/theories/bool/equality.ml b/colibri2/theories/bool/equality.ml
index 7d180b4804c10ba69cf4f13654160bc7168c35f2..e2400105bff7bd817ad60527bab37026cfe39955 100644
--- a/colibri2/theories/bool/equality.ml
+++ b/colibri2/theories/bool/equality.ml
@@ -560,6 +560,7 @@ let th_register env =
Ground.register_converter env converter;
bool_init_diff_to_value env;
Check.init_check env;
+ Disequality.register_disequal env is_disequal;
()
let () = Init.add_default_theory th_register
diff --git a/colibri2/theories/bool/equality.mli b/colibri2/theories/bool/equality.mli
index a06a047a6e5d33636cdf62852780132aa4fe15cd..7eca02ac86fbe70d31a16259d9efa5d613ae516a 100644
--- a/colibri2/theories/bool/equality.mli
+++ b/colibri2/theories/bool/equality.mli
@@ -31,3 +31,5 @@ val register_hook_new_disequality :
(** register a hook that is called each time a set of nodes is known to be disequal *)
val th_register : Egraph.wt -> unit
+
+
diff --git a/colibri2/theories/quantifier/definitions.ml b/colibri2/theories/quantifier/definitions.ml
index aaaaea2b72b92996181947d67033593cf1b7b7a4..260f3f55c5b2ed1d4cce9692bb1eefd07b5370b1 100644
--- a/colibri2/theories/quantifier/definitions.ml
+++ b/colibri2/theories/quantifier/definitions.ml
@@ -131,9 +131,12 @@ module Defs = struct
| { app = tc; _ } -> (
match Expr.Term.Const.HC.find fundefs d tc with
| exception Not_found -> ()
- | _ ->
- if not (ThTermH.mem levels d th) then
- ThTermH.set levels d th (1 + level)))
+ | _ -> (
+ match ThTermH.find_opt levels d th with
+ | None -> ThTermH.set levels d th (1 + level)
+ | Some level' when 1 + level < level' ->
+ ThTermH.set levels d th (1 + level)
+ | _ -> ())))
(fun d th ->
if level <= level_dec then
Choice.Group.make_choosable d
diff --git a/colibrics.opam b/colibrics.opam
index 47f8778756b886bc9efe541ba207e010bdd646a0..8ff2e03beee63bc4f136bb588638b698c17b789f 100644
--- a/colibrics.opam
+++ b/colibrics.opam
@@ -4,7 +4,7 @@ synopsis: "A CP solver proved in Why3"
description: "The core of Colibrics is formally proved using Why3."
maintainer: ["François Bobot"]
authors: ["François Bobot"]
-license: "LGPL-2.1"
+license: "LGPL-2.1-only"
homepage: "https://colibri.frama-c.com"
bug-reports: "https://git.frama-c.com/pub/colibrics/issues"
depends: [
diff --git a/colibrilib.opam b/colibrilib.opam
index 0df2c5f153c881466c57414f0f36c3d2e1059dbb..017f127cca24e26baf042855a5dfacf73217f3c2 100644
--- a/colibrilib.opam
+++ b/colibrilib.opam
@@ -4,7 +4,7 @@ synopsis: "A library of domains and propagators proved in Why3"
description: "Interval, and union of interval domains defined formally"
maintainer: ["François Bobot"]
authors: ["François Bobot"]
-license: "LGPL-2.1"
+license: "LGPL-2.1-only"
homepage: "https://colibri.frama-c.com"
bug-reports: "https://git.frama-c.com/pub/colibrics/issues"
depends: [
diff --git a/dune-project b/dune-project
index 37ef02e9f16b951b5d2ee79d4d8c2d2b67635d4c..03ad5c94155a413486e762460ca1af8fd98291cf 100644
--- a/dune-project
+++ b/dune-project
@@ -8,7 +8,7 @@
(source (uri "git+https://git.frama-c.com/pub/colibrics.git"))
(homepage "https://colibri.frama-c.com")
(bug_reports "https://git.frama-c.com/pub/colibrics/issues")
-(license "LGPL-2.1")
+(license "LGPL-2.1-only")
(name colibri2)
(package
@@ -49,7 +49,7 @@
(package (name colibri2)
- (authors "François Bobot" "Bruno Marre" "Guillaume Bury" "Stéphane Graham-Lengrand")
+ (authors "François Bobot" "Bruno Marre" "Guillaume Bury" "Stéphane Graham-Lengrand" "Hichem Rami Ait El Hara")
(maintainers "François Bobot")
(synopsis "A CP solver for smtlib")
(description "A reimplementation of COLIBRI in OCaml")