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

In sat/sat, replaced theory state with type unit

Browse source
This commit is contained in:
Guillaume Bury 2014-11-06 00:20:40 +01:00
parent f9fde897e0
commit f36aa78a35
1 changed files with 4 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
sat/sat.ml
View file

@ -58,16 +58,16 @@ module Tsat = struct
(* We don't have anything to do since the SAT Solver already (* We don't have anything to do since the SAT Solver already
* does propagation and conflict detection *) * does propagation and conflict detection *)
type t = int type t = unit
type formula = Fsat.t type formula = Fsat.t
type explanation = Exp.t type explanation = Exp.t
type proof = unit type proof = unit
exception Inconsistent of explanation exception Inconsistent of explanation
let dummy = -1 let dummy = ()
let empty () = 0 let empty () = ()
let assume ~cs:_ _ _ _ = 0 let assume ~cs:_ _ _ _ = ()
end end
module Make(Dummy : sig end) = struct module Make(Dummy : sig end) = struct