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

details

Browse source
This commit is contained in:
Simon Cruanes 2016-01-29 14:34:45 +01:00
parent 383afcf19f
commit e8162fdaf4
3 changed files with 3 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
sat/sat.ml
View file

@ -31,7 +31,7 @@ module Fsat = struct
let apply_sign b i = if b then i else neg i 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 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 equal (a:int) b = a=b
let compare (a:int) b = Pervasives.compare a b let compare (a:int) b = Pervasives.compare a b

2
solver/formula_intf.ml
View file

@ -17,7 +17,7 @@ module type S = sig
(** Formula constants. A valid formula should never be physically equal to [dummy] *) (** Formula constants. A valid formula should never be physically equal to [dummy] *)
val fresh : unit -> t 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 val neg : t -> t
(** Formula negation *) (** Formula negation *)

2
solver/theory_intf.ml
View file

@ -27,7 +27,7 @@ module type S = sig
get : int -> formula; get : int -> formula;
push : formula list -> proof -> unit; 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]. [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. *) [push clause proof] allows to add a tautological clause to the sat solver. *)