mirror of
https://github.com/c-cube/sidekick.git
synced 2025-12-07 03:35:38 -05:00
fix: add missig module Value
This commit is contained in:
parent
83edbe7b48
commit
225afb624e
2 changed files with 43 additions and 0 deletions
21
src/smt/Value.ml
Normal file
21
src/smt/Value.ml
Normal file
|
|
@ -0,0 +1,21 @@
|
||||||
|
|
||||||
|
(** {1 Value} *)
|
||||||
|
|
||||||
|
open Solver_types
|
||||||
|
|
||||||
|
type t = value
|
||||||
|
|
||||||
|
let true_ = V_bool true
|
||||||
|
let false_ = V_bool false
|
||||||
|
let bool v = V_bool v
|
||||||
|
|
||||||
|
let mk_elt id ty : t = V_element {id; ty}
|
||||||
|
|
||||||
|
let is_bool = function V_bool _ -> true | _ -> false
|
||||||
|
let is_true = function V_bool true -> true | _ -> false
|
||||||
|
let is_false = function V_bool false -> true | _ -> false
|
||||||
|
|
||||||
|
let equal = eq_value
|
||||||
|
let hash = hash_value
|
||||||
|
let pp = pp_value
|
||||||
|
|
||||||
22
src/smt/Value.mli
Normal file
22
src/smt/Value.mli
Normal file
|
|
@ -0,0 +1,22 @@
|
||||||
|
|
||||||
|
(** {1 Value}
|
||||||
|
|
||||||
|
Semantic value *)
|
||||||
|
|
||||||
|
type t = Solver_types.value
|
||||||
|
|
||||||
|
val true_ : t
|
||||||
|
val false_ : t
|
||||||
|
val bool : bool -> t
|
||||||
|
|
||||||
|
val mk_elt : ID.t -> Ty.t -> t
|
||||||
|
|
||||||
|
val is_bool : t -> bool
|
||||||
|
val is_true : t -> bool
|
||||||
|
val is_false : t -> bool
|
||||||
|
|
||||||
|
include Intf.EQ with type t := t
|
||||||
|
include Intf.HASH with type t := t
|
||||||
|
include Intf.PRINT with type t := t
|
||||||
|
|
||||||
|
|
||||||
Loading…
Add table
Reference in a new issue