Skip to content
Snippets Groups Projects
Commit edb3e413 authored by Arthur Correnson's avatar Arthur Correnson
Browse files

Extend Nodes.ml with conversion utilities

parent b64d0d36
No related branches found
No related tags found
1 merge request!12Feature/fp check
Pipeline #35715 passed
Stage: build
Hide whitespace changes
Inline Side-by-side
src_colibri2/core/structures/nodes.ml
+ 85
− 78
View file @ edb3e413
......@@ -29,8 +29,8 @@ exception AlreadyRedirected
let debug_create = Debug.register_info_flag
~desc:"for the core solver class creation information"
"index"
~desc:"for the core solver class creation information"
"index"
module ThTermKind = Keys.Make_key(struct end)
module ValueKind = Keys.Make_key(struct end)
......@@ -226,7 +226,7 @@ module RegisterThTerm (D:ThTerm) : RegisteredThTerm with type s = D.t = struct
let sem : t -> D.t =
fun (Node.ThTerm(_,sem,v)) ->
let Poly.Eq = ThTermKind.Eq.coerce_type sem D.key in v
let Poly.Eq = ThTermKind.Eq.coerce_type sem D.key in v
let thterm: t -> ThTerm.t = fun x -> x
......@@ -257,9 +257,9 @@ module Value = struct
let value : type a. a ValueKind.t -> t -> a option =
fun value (Node.Value(_,value',v)) ->
match ValueKind.Eq.eq_type value value' with
| Poly.Neq -> None
| Poly.Eq -> Some v
match ValueKind.Eq.eq_type value value' with
| Poly.Neq -> None
| Poly.Eq -> Some v
type kind =
| Value: 'a ValueKind.t * 'a -> kind
......@@ -286,10 +286,14 @@ module type RegisteredValue = sig
(** Return the value from a nodevalue *)
val nodevalue: t -> Value.t
val of_nodevalue: Value.t -> t option
val of_value: s -> t
val coerce_nodevalue: Value.t -> t
val coerce_value: Value.t -> s
end
......@@ -310,78 +314,81 @@ module RegisterValue (D:Value) : RegisteredValue with type s = D.t = struct
module All = struct
module V = D
module HC = Hashcons.MakeTag(struct
open Node
type t = nodevalue
let next_tag = Node.next_tag
let incr_tag = Node.incr_tag
let equal: t -> t -> bool = fun a b ->
match a, b with
| Value(_,valuea,va), Value(_,valueb,vb) ->
match ValueKind.Eq.coerce_type valuea D.key,
ValueKind.Eq.coerce_type valueb D.key with
| Poly.Eq, Poly.Eq -> D.equal va vb
let hash: t -> int = fun a ->
match a with
| Value(_,valuea,va) ->
let Poly.Eq = ValueKind.Eq.coerce_type valuea D.key in
(D.hash va)
let set_tag: int -> t -> t = fun tag x ->
match x with
| Value(_,value,v) -> Value(tag,value,v)
let tag: t -> int = function
| Value(tag,_,_) -> tag
let pp fmt x =
Format.pp_print_char fmt '@';
Format.pp_print_string fmt (Simple_vector.get names (tag x))
end)
include HC
type s = D.t
let key = D.key
let tag: t -> int = function
| Node.Value(tag,_,_) -> tag
let index ?(basename="") v =
let node =
HC.hashcons2
(fun tag value v -> Node.Value(tag,value,v))
D.key v in
let i = tag node in
Simple_vector.inc_size (i+1) Node.names;
begin
if Simple_vector.is_uninitialized Node.names i then
let s = Strings.find_new_name Node.used_names basename in
Debug.dprintf3 debug_create "[Egraph] @[@@%s is %a@]"
s D.pp v;
Simple_vector.set Node.names i s
end;
node
let node = Node.of_nodevalue
let value : t -> D.t = function
| Node.Value(_,value,v) ->
let Poly.Eq = ValueKind.Eq.coerce_type value D.key in v
let nodevalue: t -> Value.t = fun x -> x
let of_nodevalue: Value.t -> t option = function
| Node.Value(_,value',_) as v when ValueKind.equal value' D.key -> Some v
| _ -> None
let coerce_nodevalue: Value.t -> t = function
| Node.Value(_,value',_) as v -> assert (ValueKind.equal value' D.key); v
module V = D
module HC = Hashcons.MakeTag(struct
open Node
type t = nodevalue
let next_tag = Node.next_tag
let incr_tag = Node.incr_tag
let equal: t -> t -> bool = fun a b ->
match a, b with
| Value(_,valuea,va), Value(_,valueb,vb) ->
match ValueKind.Eq.coerce_type valuea D.key,
ValueKind.Eq.coerce_type valueb D.key with
| Poly.Eq, Poly.Eq -> D.equal va vb
let hash: t -> int = fun a ->
match a with
| Value(_,valuea,va) ->
let Poly.Eq = ValueKind.Eq.coerce_type valuea D.key in
(D.hash va)
let set_tag: int -> t -> t = fun tag x ->
match x with
| Value(_,value,v) -> Value(tag,value,v)
let tag: t -> int = function
| Value(tag,_,_) -> tag
let pp fmt x =
Format.pp_print_char fmt '@';
Format.pp_print_string fmt (Simple_vector.get names (tag x))
end)
include HC
type s = D.t
let key = D.key
let tag: t -> int = function
| Node.Value(tag,_,_) -> tag
let index ?(basename="") v =
let node =
HC.hashcons2
(fun tag value v -> Node.Value(tag,value,v))
D.key v in
let i = tag node in
Simple_vector.inc_size (i+1) Node.names;
begin
if Simple_vector.is_uninitialized Node.names i then
let s = Strings.find_new_name Node.used_names basename in
Debug.dprintf3 debug_create "[Egraph] @[@@%s is %a@]"
s D.pp v;
Simple_vector.set Node.names i s
end;
node
let node = Node.of_nodevalue
let value : t -> D.t = function
| Node.Value(_,value,v) ->
let Poly.Eq = ValueKind.Eq.coerce_type value D.key in v
let nodevalue: t -> Value.t = fun x -> x
let of_nodevalue: Value.t -> t option = function
| Node.Value(_,value',_) as v when ValueKind.equal value' D.key -> Some v
| _ -> None
let of_value v = nodevalue (index v)
let coerce_nodevalue: Value.t -> t = function
| Node.Value(_,value',_) as v -> assert (ValueKind.equal value' D.key); v
let coerce_value x = value (coerce_nodevalue x)
end
include All
......
src_colibri2/core/structures/nodes.mli
+ 14
− 9
View file @ edb3e413
......@@ -141,11 +141,11 @@ module Value: sig
val value: 'a ValueKind.t -> t -> 'a option
type kind =
| Value: 'a ValueKind.t * 'a -> kind
| Value: 'a ValueKind.t * 'a -> kind
val kind: t -> kind
(** give the value associated with a node, make sense only for not merged
class. So only the module solver can use it *)
(** give the value associated with a node, make sense only for not merged
class. So only the module solver can use it *)
end
......@@ -171,10 +171,15 @@ module type RegisteredValue = sig
(** Return the value from a nodevalue *)
val nodevalue: t -> Value.t
val of_nodevalue: Value.t -> t option
val of_value: s -> t
val coerce_nodevalue: Value.t -> t
val coerce_value: Value.t -> s
end
module RegisterValue (D:Value) : RegisteredValue with type s = D.t
......@@ -192,18 +197,18 @@ module Only_for_solver: sig
val thterm:
Node.t -> ThTerm.t option
(** give the sem associated with a node, make sense only for not merged
class. So only the module solver can use it *)
(** give the sem associated with a node, make sense only for not merged
class. So only the module solver can use it *)
val sem_of_node:
ThTerm.t -> sem_of_node
(** give the sem associated with a node, make sense only for not merged
class. So only the module solver can use it *)
(** give the sem associated with a node, make sense only for not merged
class. So only the module solver can use it *)
val nodevalue:
Node.t -> Value.t option
(** give the value associated with a node, make sense only for not merged
class. So only the module solver can use it *)
(** give the value associated with a node, make sense only for not merged
class. So only the module solver can use it *)
val node_of_thterm: ThTerm.t -> Node.t
val node_of_nodevalue: Value.t -> Node.t
......
src_colibri2/theories/FP/float32.ml
+ 3
− 3
View file @ edb3e413
......@@ -50,9 +50,9 @@ let init_ty d =
let interp d n = Opt.get_exn Impossible (Egraph.get_value d n)
let compute_ground d t =
let (!>>>) t = RealValue.value (RealValue.coerce_nodevalue (interp d t)) in
let (!>>) t = Rounding_mode.value (Rounding_mode.coerce_nodevalue (interp d t)) in
let (!>) t = Float32.value (Float32.coerce_nodevalue (interp d t)) in
let (!>>>) t = RealValue.coerce_value (interp d t) in
let (!>>) t = Rounding_mode.coerce_value (interp d t) in
let (!>) t = Float32.coerce_value (interp d t) in
let (!<) v = `Some (Float32.nodevalue (Float32.index v)) in
let (!<<) v = `Some (Boolean.BoolValue.nodevalue (Boolean.BoolValue.index v)) in
match Ground.sem t with
......
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