simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2025-12-08 12:15:48 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

feat: ask less from values in mcsat

Browse source
This commit is contained in:
Simon Cruanes 2019-01-26 13:07:46 -06:00 • committed by Guillaume Bury
parent 4fbaae7d2d
commit a58c940c6d
1 changed files with 0 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
src/core/Solver_intf.ml
View file

@ -174,13 +174,6 @@ module type EXPR = sig
type t type t
(** The type of semantic values (domain elements) *) (** 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 val pp : t printer
(** Printing function used among other for debugging. *) (** Printing function used among other for debugging. *)
end end