From 99ce25e74f54ed1759b633ff28a9d51879e3f324 Mon Sep 17 00:00:00 2001 From: Guillaume Bury Date: Mon, 3 Nov 2014 00:49:07 +0100 Subject: [PATCH] Added a module to represent resolution proof (not tested yet) --- msat.mlpack | 1 + msat.odocl | 2 + sat/res.ml | 90 +++++++++++++++++++++++++++++++++++++++++++++ sat/res.mli | 6 +++ sat/res_intf.ml | 13 +++++++ sat/sat.ml | 1 + sat/solver.ml | 1 + sat/solver_types.ml | 15 -------- sat/theory_intf.ml | 3 ++ 9 files changed, 117 insertions(+), 15 deletions(-) create mode 100644 sat/res.ml create mode 100644 sat/res.mli create mode 100644 sat/res_intf.ml diff --git a/msat.mlpack b/msat.mlpack index 802a391b..ad1bdbc5 100644 --- a/msat.mlpack +++ b/msat.mlpack @@ -1,5 +1,6 @@ Explanation Formula_intf +Res Sat Solver Solver_types diff --git a/msat.odocl b/msat.odocl index 657cfa43..b27aa779 100644 --- a/msat.odocl +++ b/msat.odocl @@ -1,6 +1,8 @@ sat/Formula_intf sat/Explanation sat/Explanation_intf +sat/Res +sat/Res_intf sat/Sat sat/Solver sat/Solver_types diff --git a/sat/res.ml b/sat/res.ml new file mode 100644 index 00000000..448e2f38 --- /dev/null +++ b/sat/res.ml @@ -0,0 +1,90 @@ +(* Copyright 2014 Guillaume Bury *) + +module type S = Res_intf.S + +module Make(St : Solver_types.S)(Proof : sig type t end) = struct + + (* Type definitions *) + type lemma = Proof.t + type clause = St.clause + type int_cl = St.atom list + + type node = + | Assumption + | Lemma of lemma + | Resolution of int_cl * int_cl + + exception Resolution_error of string + + (* Proof graph *) + module H = Hashtbl.Make(struct + type t = St.atom list + let hash= Hashtbl.hash + let equal = List.for_all2 (==) + end) + let proof : node H.t = H.create 1007;; + + (* Misc functions *) + let compare_atoms a b = + Pervasives.compare St.(a.var.vid) St.(b.var.vid) + + let equal_atoms a b = St.(a.aid) = St.(b.aid) + + let to_list c = + let v = St.(c.atoms) in + let l = ref [] in + for i = 0 to Vec.size v - 1 do + l := (Vec.get v i) :: !l + done; + List.sort_uniq compare_atoms !l + + (* Accesors to the proof graph *) + let add_hyp c = H.add proof c Assumption + let add_lemma c l = H.add proof c (Lemma l) + + let is_proved c = H.mem proof c + + (* New resolution node *) + let resolve l = + let rec aux resolved acc = function + | [] -> resolved, acc + | [a] -> resolved, a :: acc + | a :: b :: r -> + if a == b then + aux resolved (a :: acc) r + else if St.(a.neg) == b then + aux true acc r + else + aux resolved (a :: acc) (b :: r) + in + let b, l' = aux false [] l in + b, List.sort compare_atoms l' + + let merge c d = + let l = List.merge compare_atoms c d in + let b, l' = resolve l in + if not b then + raise (Resolution_error "No literal to resolve over"); + l' + + let add_res c d = + if not (is_proved c) || not (is_proved d) then + raise (Resolution_error "Unproven clause"); + let new_clause = merge c d in + H.add proof new_clause (Resolution (c, d)); + new_clause + + (* Wrappers *) + let proven c = is_proved (to_list c) + let add_assumption c = add_hyp (to_list c) + let add_th_lemma c l = add_lemma (to_list c) l + + let add_clause c history = + assert (List.length history > 1); + let l = List.map to_list history in + let res = List.fold_left add_res (List.hd l) (List.tl l) in + if not (List.for_all2 equal_atoms (to_list c) res) then + raise (Resolution_error "Clause cannot be derived from history"); + () + +end diff --git a/sat/res.mli b/sat/res.mli new file mode 100644 index 00000000..4df90fc7 --- /dev/null +++ b/sat/res.mli @@ -0,0 +1,6 @@ +(* Copyright 2014 Guillaume Bury *) + +module type S = Res_intf.S + +module Make : functor (St : Solver_types.S)(Proof : sig type t end) + -> S with type clause = St.clause and type lemma = Proof.t diff --git a/sat/res_intf.ml b/sat/res_intf.ml new file mode 100644 index 00000000..827eeaef --- /dev/null +++ b/sat/res_intf.ml @@ -0,0 +1,13 @@ +(* Copyright 2014 Guillaume Bury *) + +module type S = sig + type clause + type lemma + + val proven : clause -> bool + + val add_assumption : clause -> unit + val add_th_lemma : clause -> lemma -> unit + val add_clause : clause -> clause list -> unit + +end diff --git a/sat/sat.ml b/sat/sat.ml index fd7b1230..d39205de 100644 --- a/sat/sat.ml +++ b/sat/sat.ml @@ -61,6 +61,7 @@ module Tsat = struct type t = int type formula = Fsat.t type explanation = Exp.t + type proof = unit exception Inconsistent of explanation diff --git a/sat/solver.ml b/sat/solver.ml index 3a2a8f1a..1f0092f7 100644 --- a/sat/solver.ml +++ b/sat/solver.ml @@ -18,6 +18,7 @@ module Make (F : Formula_intf.S) (Th : Theory_intf.S with type formula = F.t and type explanation = Ex.t) = struct open St + module Res = Res.Make(St)(struct type t = Th.proof end) exception Sat exception Unsat of clause list diff --git a/sat/solver_types.ml b/sat/solver_types.ml index d70e2f2f..22da672d 100644 --- a/sat/solver_types.ml +++ b/sat/solver_types.ml @@ -13,14 +13,6 @@ open Printf -let ale = Hstring.make "<=" -let alt = Hstring.make "<" -let agt = Hstring.make ">" - -let is_le n = Hstring.compare n ale = 0 -let is_lt n = Hstring.compare n alt = 0 -let is_gt n = Hstring.compare n agt = 0 - module type S = Solver_types_intf.S module Make (F : Formula_intf.S) = struct @@ -86,13 +78,6 @@ module Make (F : Formula_intf.S) = struct module MA = Map.Make(F) type varmap = var MA.t - let ale = Hstring.make "<=" - let alt = Hstring.make "<" - let agt = Hstring.make ">" - let is_le n = Hstring.compare n ale = 0 - let is_lt n = Hstring.compare n alt = 0 - let is_gt n = Hstring.compare n agt = 0 - let normal_form = F.norm let cpt_mk_var = ref 0 diff --git a/sat/theory_intf.ml b/sat/theory_intf.ml index 3e5e649e..a6d1e169 100644 --- a/sat/theory_intf.ml +++ b/sat/theory_intf.ml @@ -25,6 +25,9 @@ module type S = sig (** The type of explanations. Should be compatible with Explanations.S.t with module St = Solver_types.S with type formula = fomula *) + type proof + (** A custom type for the proofs of lemmas produced by the theory. *) + exception Inconsistent of explanation (** Exception raised by the theory when assuming an incoherent set of formulas. *)