1(* ========================================================================= *)
2(* THE RESOLUTION PROOF PROCEDURE                                            *)
3(* Copyright (c) 2001-2004 Joe Hurd.                                         *)
4(* ========================================================================= *)
5
6(*
7app load
8 ["Moscow", "mlibUseful", "mlibTerm", "mlibThm", "mlibCanon", "mlibSupport",
9  "mlibStream", "mlibSolver", "mlibMeter", "mlibUnits", "mlibClauseset"];
10*)
11
12(*
13*)
14structure mlibResolution :> mlibResolution =
15struct
16
17open mlibUseful mlibTerm mlibMeter mlibSolver;
18
19structure I = Intset; local open Intset in end;
20structure S = mlibStream; local open mlibStream in end;
21
22type clause = mlibClause.clause;
23type distance = mlibSupport.distance;
24
25(* ------------------------------------------------------------------------- *)
26(* Chatting.                                                                 *)
27(* ------------------------------------------------------------------------- *)
28
29val module = "mlibResolution";
30val () = add_trace {module = module, alignment = I}
31fun chatting l = tracing {module = module, level = l};
32fun chat s = (trace s; true)
33
34(* ------------------------------------------------------------------------- *)
35(* Parameters.                                                               *)
36(* ------------------------------------------------------------------------- *)
37
38type parameters =
39  {clause_parm : mlibClause.parameters,
40   set_parm    : mlibClauseset.parameters,
41   sos_parm    : mlibSupport.parameters};
42
43val defaults : parameters =
44  {clause_parm = mlibClause.defaults,
45   set_parm    = mlibClauseset.defaults,
46   sos_parm    = mlibSupport.defaults};
47
48type 'a parmupdate = ('a -> 'a) -> parameters -> parameters;
49
50fun update_clause_parm f (parm : parameters) : parameters =
51  let val {clause_parm = c, sos_parm = a, set_parm = b} = parm
52  in {clause_parm = f c, sos_parm = a, set_parm = b}
53  end;
54
55fun update_set_parm f (parm : parameters) : parameters =
56  let val {clause_parm = c, sos_parm = a, set_parm = b} = parm
57  in {clause_parm = c, sos_parm = a, set_parm = f b}
58  end;
59
60fun update_sos_parm f (parm : parameters) : parameters =
61  let val {clause_parm = c, sos_parm = a, set_parm = b} = parm
62  in {clause_parm = c, sos_parm = f a, set_parm = b}
63  end;
64
65(* ------------------------------------------------------------------------- *)
66(* Helper functions                                                          *)
67(* ------------------------------------------------------------------------- *)
68
69fun ofilt _ NONE = NONE | ofilt p (s as SOME x) = if p x then s else NONE;
70
71local fun ins (c,i) = Intmap.insert (i, #id (mlibClause.dest_clause c), c);
72in fun insert cls init = foldl ins init cls;
73end;
74
75val thm_to_formula = list_mk_disj o mlibThm.clause;
76
77val clause_id = #id o mlibClause.dest_clause;
78
79fun clause_to_string cl =
80  PP.pp_to_string (!LINE_LENGTH) mlibClause.pp_clause cl;
81
82fun clauses_to_string cls =
83  PP.pp_to_string (!LINE_LENGTH) (pp_list mlibClause.pp_clause) cls;
84
85(* ------------------------------------------------------------------------- *)
86(* mlibResolution                                                                *)
87(* ------------------------------------------------------------------------- *)
88
89datatype resolution = RES of {set : mlibClauseset.clauseset, sos : mlibSupport.sos};
90
91fun update_set b res =
92  let val RES {set = _, sos = a} = res
93  in RES {set = b, sos = a}
94  end;
95
96fun update_sos a res =
97  let val RES {set = b, sos = _} = res
98  in RES {set = b, sos = a}
99  end;
100
101fun dest (RES r) = r;
102
103fun size (RES {set,sos,...}) =
104  {used = mlibClauseset.size set, waiting = mlibSupport.size sos,
105   rewrites = mlibClause.size (mlibClauseset.rewrites set)};
106
107fun units (RES {set,...}) = mlibClauseset.units set;
108
109fun new_units units (res as RES {set,...}) =
110  update_set (mlibClauseset.new_units units set) res;
111
112fun mk_axioms thms hyps =
113  let
114    val thms = map thm_to_formula thms
115    and hyps = map thm_to_formula hyps
116  in
117    if null thms then hyps else thms @ map Not hyps
118  end;
119
120fun mk_thms_hyps (clause_parm : mlibClause.parameters) thms hyps =
121  let
122    val thms = map (mlibClause.mk_clause clause_parm) thms
123    and hyps = map (mlibClause.mk_clause clause_parm) hyps
124  in
125    if #literal_order clause_parm then ([], hyps @ thms) else
126      let val (noneqs,eqs) = List.partition (null o mlibClause.largest_eqs) thms
127      in (noneqs, hyps @ eqs)
128      end
129  end;
130
131fun new (parm : parameters, units, thms, hyps) =
132  let
133    val {clause_parm,sos_parm,set_parm,...} = parm
134    val axioms = mk_axioms thms hyps
135    val (thms,hyps) = mk_thms_hyps clause_parm thms hyps
136    val set = mlibClauseset.empty (clause_parm,set_parm)
137    val set = mlibClauseset.new_units units set
138    val (thms,set) = mlibClauseset.factor thms set
139    val set = foldl (fn (c,s) => mlibClauseset.add c s) set thms
140    val (hyps,set) = mlibClauseset.factor hyps set
141    val sos = mlibSupport.new sos_parm axioms hyps
142  in
143    RES {set = set, sos = sos}
144  end;
145
146local
147  fun beef_up set = mlibClauseset.strengthen set o mlibClauseset.simplify set;
148
149  fun get_clause set sos n =
150    case mlibSupport.remove sos of NONE => (n,NONE)
151    | SOME (dcl,sos) => check set sos n dcl
152  and check set sos n (d,cl) =
153    case ofilt (not o mlibClauseset.subsumed set) (beef_up set cl) of
154      NONE => get_clause set sos (n + 1)
155    | SOME cl => (n, SOME ((d,cl),sos));
156in
157  fun select res =
158    let
159      val RES {set,sos,...} = res
160      val (n,dcl_sos) = get_clause set sos 0
161      val _ = 0 < n andalso chatting 2 andalso chat ("x" ^ int_to_string n)
162    in
163      case dcl_sos of NONE => NONE
164      | SOME ((d,cl),sos) =>
165      let
166        val res = update_sos sos res
167        val {order_stickiness, ...} = #parm (mlibClause.dest_clause cl)
168        val cl = if order_stickiness <= 2 then mlibClause.drop_order cl else cl
169        val set = mlibClauseset.add cl set
170        val res = update_set set res
171      in
172        SOME ((d,cl),res)
173      end
174    end;
175end;
176
177fun deduce cl res =
178  let
179    val _ = chatting 4 andalso
180            chat ("\ngiven clause:\n" ^ clause_to_string cl ^ "\n")
181    val RES {set,...} = res
182    val cl = mlibClause.FRESH_VARS cl
183    val cls = mlibClauseset.deduce set cl
184  in
185    cls
186  end;
187
188fun factor cls res =
189  let
190    val RES {set,...} = res
191    val (cls,set) = mlibClauseset.factor cls set
192    val res = update_set set res
193    val _ = chatting 4 andalso
194            chat ("\nnew clauses:\n" ^ clauses_to_string cls ^ "\n")
195  in
196    (cls,res)
197  end;
198
199fun add (dist,cls) res =
200  let
201    val RES {sos,...} = res
202    val sos = mlibSupport.add (dist,cls) sos
203    val res = update_sos sos res
204  in
205    res
206  end;
207
208fun advance res =
209  case select res of NONE => NONE
210  | SOME ((d,cl),res) =>
211    let
212      val cls = deduce cl res
213      val (cls,res) = factor cls res
214      val res = add (d,cls) res
215    in
216      SOME res
217    end;
218
219fun resolution_to_string res =
220  let
221    val {used = u, waiting = w, rewrites = r} = size res
222  in
223    "(" ^ int_to_string u ^ "<-" ^ int_to_string w
224    ^ (if r = 0 then "" else "=" ^ int_to_string r) ^ ")"
225  end;
226
227val pp_resolution = pp_map resolution_to_string pp_string;
228
229(* ------------------------------------------------------------------------- *)
230(* The resolution procedure as a solver_node                                 *)
231(* ------------------------------------------------------------------------- *)
232
233fun resolution_stream slice_ref units_ref =
234  let
235    fun stat func res () =
236      (chatting 3 andalso chat (resolution_to_string res); func res)
237
238    fun sq f x =
239      let
240        val _ = chatting 1 andalso chat "["
241        val y = f x
242        val _ = chatting 1 andalso chat "]"
243      in
244        y
245      end
246
247    fun shove res = new_units (!units_ref) res
248
249    fun swipe res = units_ref := units res (* OK *)
250
251    fun record infs = record_infs (!slice_ref) infs
252
253    fun f res =
254      case select res of NONE => (swipe res; S.NIL)
255      | SOME dcl_res => g dcl_res
256    and g (dcl as (_,cl), res) =
257      if not (mlibClause.is_empty cl) then h dcl res
258      else (swipe res; S.CONS (SOME cl, stat (h dcl o shove) res))
259    and h (d,cl) res =
260      let
261        val cls = deduce cl res
262        val (cls,res) = factor cls res
263        val () = record (length cls + #rewrites (size res))
264        val res = add (d,cls) res
265      in
266        if check_meter (!slice_ref) then f res
267        else (swipe res; S.CONS (NONE, stat (f o shove) res))
268      end;
269  in
270    fn (parm,thms,hyps) => stat f (sq new (parm,!units_ref,thms,hyps)) ()
271  end;
272
273fun resolution' (name, parm : parameters) =
274  mk_solver_node
275  {name = name,
276   solver_con =
277   fn {slice = slice_ref, units = units_ref, thms, hyps} =>
278   let
279     val _ = chatting 3 andalso chat
280       (name ^ "--initializing--#thms=" ^ int_to_string (length thms) ^
281        "--#hyps=" ^ int_to_string (length hyps) ^ ".\n")
282     val solution_stream =
283       S.map (Option.map (sing o #thm o mlibClause.dest_clause)) o
284       resolution_stream slice_ref units_ref
285   in
286     fn [False] => solution_stream (parm,thms,hyps) | _ => S.NIL
287   end};
288
289val resolution = resolution' ("resolution",defaults);
290
291end
292