module type LITERAL = sig       (* tip modul = interfata *)
  type t
  val compare: t -> t -> int          (* necesar pt. multimi *)
  val neg: t -> t
end

module Sat(L: LITERAL) = struct        (* modul parametrizat *)
  module S = Set.Make(L)

  exception Unsat

  let filter_clause ones =
    List.filter (
        fun e -> if S.mem e ones then raise Exit  (* clauza e adevarata *)
                 else not (S.mem (L.neg e) ones)  (* cele care nu sunt false *)
      )
                
  let rec simplify ones =
    List.fold_left (
        fun (ones, clist) cl -> 
        try (match filter_clause ones cl with
             | [] -> raise Unsat        (* clauza vida -> nerealizabila *)
             | [lit] -> simplify (S.add lit ones) clist (* reia cu lit=true *)
             | newcl -> (ones, newcl :: clist))
        with Exit -> (ones, clist) (* clauza adevarata -> nu modifica *)
      ) (ones, [])
                   
  let sat =
    let rec sat1 ones clist =
    match simplify ones clist with
    | (ones, []) -> S.elements ones        (* nu mai sunt clauze: gata *)
    | (ones, (lit::cls)::clist) ->        (* incearca lit cu ambele valori *)
       try sat1 (S.add (L.neg lit) ones) (cls::clist)
       with Unsat -> sat1 (S.add lit ones) clist
    in sat1 S.empty                        (* initial, fara atribuiri *)
end

module StrLit = struct
  type t = P of string | N of string
  let compare = compare
  let neg = function
    | P s -> N s
    | N s -> P s
end

open StrLit
module SatS = Sat(StrLit)
;;
SatS.sat [[P "a"; P "b"; N "c"]; [N "a"; P "c"]; [P "a"; N "b"]]

This document was generated using caml2html