diff options
Diffstat (limited to 'src/trace/satAtom.mli')
| -rw-r--r-- | src/trace/satAtom.mli | 32 |
1 files changed, 0 insertions, 32 deletions
diff --git a/src/trace/satAtom.mli b/src/trace/satAtom.mli index 49bc590..92f9bc7 100644 --- a/src/trace/satAtom.mli +++ b/src/trace/satAtom.mli @@ -38,38 +38,6 @@ module Form : SmtForm.FORM with type hatom = Atom.t module Trace : sig - val share_value : Form.t SmtCertif.clause -> unit - module HashedHeadRes : - sig - type t = Form.t SmtCertif.resolution - val equal : - 'a SmtCertif.resolution -> 'b SmtCertif.resolution -> bool - val hash : 'a SmtCertif.resolution -> int - end - module HRtbl : - sig - type key = HashedHeadRes.t - type 'a t = 'a Hashtbl.Make(HashedHeadRes).t - val create : int -> 'a t - val clear : 'a t -> unit - val reset : 'a t -> unit - val copy : 'a t -> 'a t - val add : 'a t -> key -> 'a -> unit - val remove : 'a t -> key -> unit - val find : 'a t -> key -> 'a - val find_all : 'a t -> key -> 'a list - val replace : 'a t -> key -> 'a -> unit - val mem : 'a t -> key -> bool - val iter : (key -> 'a -> unit) -> 'a t -> unit - val fold : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b - val length : 'a t -> int - val stats : 'a t -> Hashtbl.statistics - end - val common_head : - 'a SmtCertif.clause list -> - 'b SmtCertif.clause list -> - 'a SmtCertif.clause list * 'a SmtCertif.clause list * - 'b SmtCertif.clause list val share_prefix : Form.t SmtCertif.clause -> int -> unit end module Cnf : |