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