Merge branch 'master' into feature/array_theory

.vscode/tasks.json

+{
+	"version": "2.0.0",
+	"tasks": [
+		{
+			"type": "dune",
+			"problemMatcher": [
+				"$ocamlc"
+			],
+			"group": {
+				"kind": "build",
+				"isDefault": true
+			},
+			"label": "dune: build @runtest"
+		}
+	]
+}
\ No newline at end of file

CHANGES

+## 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

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: [

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

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

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)

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_;

colibri2/theories/bool/disequality.ml

+(*************************************************************************)
+(*  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;

colibri2/theories/bool/disequality.mli

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

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

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

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
+
+

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

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: [

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: [

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")