Skip to content
Snippets Groups Projects
Commit 5bef85ce authored by Hichem R. A.'s avatar Hichem R. A. Committed by Hichem R. A.
Browse files

[Array] Use integers for vertices, added eq_indices_norm

parent 06bb8b5c
No related branches found
No related tags found
1 merge request!32Update ocplib-simplex, some fixes
Expand all Hide whitespace changes
Inline Side-by-side
Showing
with 307 additions and 245 deletions
colibri2/theories/array/DiffGraph.ml
+ 254
− 124
View file @ 5bef85ce
This diff is collapsed.
colibri2/theories/array/DiffGraph.mli
+ 12
− 24
View file @ 5bef85ce
......@@ -23,34 +23,22 @@ open Colibri2_core
open Colibri2_popop_lib
open Popop_stdlib
module NHT : sig
val set : Egraph.wt -> int -> Node.t -> unit
val find : Egraph.wt -> int -> Node.t
val find_opt : Egraph.wt -> int -> Node.t option
val change : f:(Node.t option -> Node.t option) -> Egraph.wt -> int -> unit
val remove : Egraph.wt -> int -> unit
end
module DG : sig
val set : Egraph.wt -> int -> DInt.S.t Node.M.t * Node.t DInt.M.t -> unit
val find_opt :
Egraph.wt -> int -> (DInt.S.t Node.M.t * Node.t DInt.M.t) option
Egraph.wt -> int -> (DInt.S.t DInt.M.t * DInt.t DInt.M.t) option
end
module Id_dom : sig
val set_id : Egraph.wt -> Node.t -> unit
val get_id : Egraph.wt -> Node.t -> int
val change :
f:
((DInt.S.t Node.M.t * Node.t DInt.M.t) option ->
(DInt.S.t Node.M.t * Node.t DInt.M.t) option) ->
val register_merge_hook :
Egraph.wt ->
int ->
(Egraph.wt -> Node.t * int -> Node.t * int -> bool -> unit) ->
unit
val remove : Egraph.wt -> int -> unit
val diffgraph_opt : Colibri2_stdlib.Debug.flag
val pp_dot_diffgraph : Egraph.wt -> ?msg:string -> unit -> unit
end
module Id_dom : sig
module Index_Id_dom : sig
val set_id : Egraph.wt -> Node.t -> unit
val get_id : Egraph.wt -> Node.t -> int
......@@ -60,7 +48,7 @@ module Id_dom : sig
unit
end
val pp_nid : Egraph.wt -> Format.formatter -> int -> unit
val add_edge : Egraph.wt -> int -> int -> Node.t -> unit
val merge_neighbours : Egraph.wt -> Node.t * int -> Node.t * int -> bool -> unit
val eq_arrays_norm : Egraph.wt -> Node.t * int -> Node.t * int -> bool -> unit
val eq_indices_norm : Egraph.wt -> Node.t * int -> Node.t * int -> bool -> unit
val update : Egraph.wt -> Node.t -> Node.t -> Node.t -> Node.t -> unit
val get_neighbours : Egraph.wt -> int -> DInt.S.t
colibri2/theories/array/SharingIsCaring.ml deleted 100644 → 0
+ 0
− 49
View file @ 06bb8b5c
(*************************************************************************)
(* This file is part of Colibri2. *)
(* *)
(* Copyright (C) 2014-2021 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* OCamlPro *)
(* *)
(* you can redistribute it and/or modify it under the terms of the GNU *)
(* Lesser General Public License as published by the Free Software *)
(* Foundation, version 2.1. *)
(* *)
(* It is distributed in the hope that it will be useful, *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
(* GNU Lesser General Public License for more details. *)
(* *)
(* See the GNU Lesser General Public License version 2.1 *)
(* for more details (enclosed in the file licenses/LGPLv2.1). *)
(*************************************************************************)
open Common
module NHT = DiffGraph.NHT
module DG = DiffGraph.DG
(* if _b is true then kn is the representative, otherwise, it's rid *)
let eq_arrays_norm env (kn, kid) (rn, rid) b =
Debug.dprintf4 debug "DiffGraph: eq_arrays_norm %a %a" (DiffGraph.pp_nid env)
kid (DiffGraph.pp_nid env) rid;
DiffGraph.merge_neighbours env (kn, kid) (rn, rid) b;
if Debug.test_flag DG.diffgraph_opt then
DG.pp_dot_diffgraph
~msg:
(Fmt.str "eq_arrays_norm %a{%d} %a{%d} " Node.pp (NHT.find env kid) kid
Node.pp (NHT.find env rid) rid)
env ()
let update_np_dp env a b k =
let aid = DiffGraph.Id_dom.get_id env a in
let bid = DiffGraph.Id_dom.get_id env b in
Debug.dprintf6 debug "DiffGraph: update_np_dp %a %a %a" (DiffGraph.pp_nid env)
aid (DiffGraph.pp_nid env) bid Node.pp k;
DiffGraph.add_edge env aid bid k;
if Debug.test_flag DG.diffgraph_opt then
DG.pp_dot_diffgraph
~msg:
(Fmt.str "update_np_dp %a %a %a" (DiffGraph.pp_nid env) aid
(DiffGraph.pp_nid env) bid Node.pp k)
env ()
colibri2/theories/array/SharingIsCaring.mli deleted 100644 → 0
+ 0
− 23
View file @ 06bb8b5c
(*************************************************************************)
(* This file is part of Colibri2. *)
(* *)
(* Copyright (C) 2014-2021 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* OCamlPro *)
(* *)
(* you can redistribute it and/or modify it under the terms of the GNU *)
(* Lesser General Public License as published by the Free Software *)
(* Foundation, version 2.1. *)
(* *)
(* It is distributed in the hope that it will be useful, *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
(* GNU Lesser General Public License for more details. *)
(* *)
(* See the GNU Lesser General Public License version 2.1 *)
(* for more details (enclosed in the file licenses/LGPLv2.1). *)
(*************************************************************************)
val eq_arrays_norm : Egraph.wt -> Node.t * int -> Node.t * int -> bool -> unit
val update_np_dp : Egraph.wt -> Node.t -> Node.t -> Node.t -> unit
colibri2/theories/array/array.ml
+ 13
− 14
View file @ 5bef85ce
......@@ -24,21 +24,18 @@ open Colibri2_popop_lib
open Common
open Colibri2_theories_quantifiers
open GE_Array_DP
open SharingIsCaring
(*
Command line options:
- "None": uses RW1(adown), RW2(aup), idx and extensionality
GE_Array_DP:
- "--array-res-ext": restricts the extrensionality rule using the foreign
domain
- "--array-res-aup": restricts the RW2 rule using the linearity domain
- "--array-ext-comb": to support additional combinators
(const, map, def_ind, def_val)
- "--array-blast-rule": uses the blast rule when it suits
- "--array-def-values": suppots the rules on the default values
SharingIsCaring:
- "--array-diff-graph": uses the diff graph
- "--array-res-ext": restricts the extrensionality rule using the foreign
domain
- "--array-res-aup": restricts the RW2 rule using the linearity domain
- "--array-ext-comb": to support additional combinators
(const, map, def_ind, def_val)
- "--array-blast-rule": uses the blast rule when it suits
- "--array-def-values": suppots the rules on the default values
- "--array-diff-graph": uses the diff graph
*)
let converter env (f : Ground.t) =
......@@ -134,6 +131,7 @@ let converter env (f : Ground.t) =
add_array_gty env b ind_gty val_gty;
DiffGraph.Id_dom.set_id env a;
DiffGraph.Id_dom.set_id env b;
DiffGraph.Index_Id_dom.set_id env k;
(* update of the Linearity domain *)
if Options.get env restrict_aup then
Linearity_dom.upd_dom env fn (Linear b);
......@@ -165,7 +163,7 @@ let converter env (f : Ground.t) =
let eqn = mk_eq env a b (Ground.Ty.array ind_gty val_gty) in
Egraph.register env eqn;
Boolean.set_true env eqn)
else update_np_dp env a b k)
else DiffGraph.update env a b k v)
| {
app = { builtin = Builtin.Array_diff; _ };
args;
......@@ -223,8 +221,9 @@ let init env =
Array_value.init_ty env;
Array_value.init_check env;
Ground.register_converter env converter;
if Options.get env use_diff_graph then
DiffGraph.Id_dom.register_merge_hook env eq_arrays_norm;
if Options.get env use_diff_graph then (
DiffGraph.Id_dom.register_merge_hook env DiffGraph.eq_arrays_norm;
DiffGraph.Index_Id_dom.register_merge_hook env DiffGraph.eq_indices_norm);
(* extᵣ (restricted extensionality):
- (a = b) ≡ false |> (a[k] ≠ b[k])
- a, b, {a,b} ⊆ foreign |> (a = b) ⋁ (a[k] ≠ b[k]) *)
......
colibri2/theories/array/common.ml
+ 15
− 2
View file @ 5bef85ce
......@@ -338,13 +338,26 @@ let distinct_arrays_term a b =
let diff = Builtin.apply_array_diff a b in
Expr.Term.distinct [ mk_select_term a diff; mk_select_term b diff ]
module type HTS = sig
type t
val set : Egraph.wt -> int -> t -> unit
val find : Egraph.wt -> int -> t
val find_opt : Egraph.wt -> int -> t option
val change : f:(t option -> t option) -> Egraph.wt -> int -> unit
val remove : Egraph.wt -> int -> unit
val iter : f:(int -> t -> unit) -> Egraph.wt -> unit
val fold : (int -> t -> 'a -> 'a) -> Egraph.wt -> 'a -> 'a
end
module MkIHT (V : sig
type t
val pp : t Pp.pp
val name : string
end) =
struct
end) : HTS with type t = V.t = struct
type t = V.t
let db = HT.create V.pp V.name
let set (env : Egraph.wt) = HT.set db env
let find (env : Egraph.wt) = HT.find db env
......
colibri2/theories/array/common.mli
+ 13
− 9
View file @ 5bef85ce
......@@ -134,20 +134,24 @@ val mk_distinct_arrays :
val mk_array_const : 'a Egraph.t -> Node.t -> Ground.Ty.t -> Node.t
val distinct_arrays_term : Expr.term -> Expr.term -> Expr.term
module type HTS = sig
type t
val set : Egraph.wt -> int -> t -> unit
val find : Egraph.wt -> int -> t
val find_opt : Egraph.wt -> int -> t option
val change : f:(t option -> t option) -> Egraph.wt -> int -> unit
val remove : Egraph.wt -> int -> unit
val iter : f:(int -> t -> unit) -> Egraph.wt -> unit
val fold : (int -> t -> 'a -> 'a) -> Egraph.wt -> 'a -> 'a
end
module MkIHT (V : sig
type t
val pp : t Colibri2_popop_lib.Pp.pp
val name : string
end) : sig
val set : Egraph.wt -> int -> V.t -> unit
val find : Egraph.wt -> int -> V.t
val find_opt : Egraph.wt -> int -> V.t option
val change : f:(V.t option -> V.t option) -> Egraph.wt -> int -> unit
val remove : Egraph.wt -> int -> unit
val iter : f:(int -> V.t -> unit) -> Egraph.wt -> unit
val fold : (int -> V.t -> 'a -> 'a) -> Egraph.wt -> 'a -> 'a
end
end) : HTS with type t = V.t
module MkIdDom (_ : sig
val n1 : string
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment