From 225afb624eab74f47523bb4314a9b47fcd30aa2a Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Sun, 17 Jun 2018 14:26:07 -0500 Subject: [PATCH] fix: add missig module Value --- src/smt/Value.ml | 21 +++++++++++++++++++++ src/smt/Value.mli | 22 ++++++++++++++++++++++ 2 files changed, 43 insertions(+) create mode 100644 src/smt/Value.ml create mode 100644 src/smt/Value.mli diff --git a/src/smt/Value.ml b/src/smt/Value.ml new file mode 100644 index 00000000..3f2d9181 --- /dev/null +++ b/src/smt/Value.ml @@ -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 + diff --git a/src/smt/Value.mli b/src/smt/Value.mli new file mode 100644 index 00000000..c44fe86b --- /dev/null +++ b/src/smt/Value.mli @@ -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 + +