From e8162fdaf4bfa14c0fa26384946d260c62db68bf Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Fri, 29 Jan 2016 14:34:45 +0100 Subject: [PATCH] details --- sat/sat.ml | 2 +- solver/formula_intf.ml | 2 +- solver/theory_intf.ml | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/sat/sat.ml b/sat/sat.ml index 6c806f22..227ffcec 100644 --- a/sat/sat.ml +++ b/sat/sat.ml @@ -31,7 +31,7 @@ module Fsat = struct let apply_sign b i = if b then i else neg i let set_sign b i = if b then abs i else neg (abs i) - let hash (a:int) = Hashtbl.hash a + let hash (a:int) = a land max_int let equal (a:int) b = a=b let compare (a:int) b = Pervasives.compare a b diff --git a/solver/formula_intf.ml b/solver/formula_intf.ml index d8da5664..f879529f 100644 --- a/solver/formula_intf.ml +++ b/solver/formula_intf.ml @@ -17,7 +17,7 @@ module type S = sig (** Formula constants. A valid formula should never be physically equal to [dummy] *) val fresh : unit -> t - (** Returns a fresh litteral, distinct from any other literal (used in cnf conversion) *) + (** Returns a fresh literal, distinct from any other literal (used in cnf conversion) *) val neg : t -> t (** Formula negation *) diff --git a/solver/theory_intf.ml b/solver/theory_intf.ml index 68f90f74..3923ff0e 100644 --- a/solver/theory_intf.ml +++ b/solver/theory_intf.ml @@ -27,7 +27,7 @@ module type S = sig get : int -> formula; push : formula list -> proof -> unit; } - (** The type for a slice of litterals to assume/propagate in the theory. + (** The type for a slice of literals to assume/propagate in the theory. [get] operations should only be used for integers [ start <= i < start + length]. [push clause proof] allows to add a tautological clause to the sat solver. *)