From a58c940c6d322031813647a3b659ad7353cac0fb Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Sat, 26 Jan 2019 13:07:46 -0600 Subject: [PATCH] feat: ask less from values in mcsat --- src/core/Solver_intf.ml | 7 ------- 1 file changed, 7 deletions(-) diff --git a/src/core/Solver_intf.ml b/src/core/Solver_intf.ml index d615d8c8..76724b76 100644 --- a/src/core/Solver_intf.ml +++ b/src/core/Solver_intf.ml @@ -174,13 +174,6 @@ module type EXPR = sig type t (** The type of semantic values (domain elements) *) - val equal : t -> t -> bool - (** Equality over values. *) - - val hash : t -> int - (** Hashing function for values. Should be such that two terms equal according - to {!equal} have the same hash. *) - val pp : t printer (** Printing function used among other for debugging. *) end