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

Added some convenience functions in pure sat solver

Browse source
This commit is contained in:
Guillaume Bury 2015-02-18 16:45:36 +01:00
parent d58c5c0756
commit e20876ad02
2 changed files with 14 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
sat/sat.ml
View file

@ -25,6 +25,10 @@ module Fsat = struct
let neg a = - a let neg a = - a
let norm a = abs a, a < 0 let norm a = abs a, a < 0
let abs = abs
let sign i = i > 0
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) = Hashtbl.hash a
let equal (a:int) b = a=b let equal (a:int) b = a=b
@ -110,7 +114,12 @@ module Make(Log : Log_intf.S) = struct
with Fsat.Dummy _ -> with Fsat.Dummy _ ->
raise Bad_atom raise Bad_atom
let abs = Fsat.abs
let neg = Fsat.neg let neg = Fsat.neg
let sign = Fsat.sign
let apply_sign = Fsat.apply_sign
let set_sign = Fsat.set_sign
let hash = Fsat.hash let hash = Fsat.hash
let equal = Fsat.equal let equal = Fsat.equal

5
sat/sat.mli
View file

@ -37,6 +37,11 @@ module Make(Log: Log_intf.S) : sig
val neg : atom -> atom val neg : atom -> atom
(** [neg a] returns the negation of a literal. Involutive, i.e [neg (neg a) = a]. *) (** [neg a] returns the negation of a literal. Involutive, i.e [neg (neg a) = a]. *)
val abs : atom -> atom
val sign : atom -> bool
val apply_sign : bool -> atom -> atom
val set_sign : bool -> atom -> atom
val hash : atom -> int val hash : atom -> int
val equal : atom -> atom -> bool val equal : atom -> atom -> bool
val compare : atom -> atom -> int val compare : atom -> atom -> int