1(* ========================================================================= *)
2(* THE METIS COMBINATION OF PROOF PROCEDURES FOR FIRST-ORDER LOGIC           *)
3(* Copyright (c) 2001-2004 Joe Hurd.                                         *)
4(* ========================================================================= *)
5
6(*
7app load
8 ["mlibUseful", "Mosml", "mlibTerm", "mlibThm", "mlibCanon",
9  "mlibSolver", "mlibMeson", "mlibResolution"];
10*)
11
12(*
13*)
14structure mlibMetis :> mlibMetis =
15struct
16
17open mlibUseful mlibTerm mlibThm mlibMeter mlibSolver;
18
19structure M = mlibMeson; local open mlibMeson in end;
20structure R = mlibResolution; local open mlibResolution in end;
21
22(* ------------------------------------------------------------------------- *)
23(* Aligning trace levels.                                                    *)
24(* ------------------------------------------------------------------------- *)
25
26(* mlibMetis trace levels:
27   0: No output
28   1: Status information during proof search
29   2: More status information
30   3: More detailed prover information: slice by slice
31   4: High-level proof search information
32   5: Log of every inference during proof search
33   6: mlibSupport infrastructure such as mlibTermorder *)
34
35val aligned_traces =
36  [{module = "mlibTermorder",  alignment = fn n => n + 5},
37   {module = "mlibModel",      alignment = fn n => n + 5},
38   {module = "mlibRewrite",    alignment = fn n => n + 4},
39   {module = "mlibClause",     alignment = fn n => n + 4},
40   {module = "mlibSolver",     alignment = I},
41   {module = "mlibMeson",      alignment = I},
42   {module = "mlibClauseset",  alignment = I},
43   {module = "mlibSupport",    alignment = I},
44   {module = "mlibResolution", alignment = I}];
45
46val () = trace_level := 1 (* OK *)
47val () = set_traces aligned_traces
48
49(* ------------------------------------------------------------------------- *)
50(* Helper functions                                                          *)
51(* ------------------------------------------------------------------------- *)
52
53(* ------------------------------------------------------------------------- *)
54(* Tuning parameters                                                         *)
55(* ------------------------------------------------------------------------- *)
56
57datatype prover =
58  mlibResolution of R.parameters
59| mlibMeson of M.parameters
60| Delta of M.parameters;
61
62type prover_parameters = prover * mlibSolver.sos_filter option * mlibSolver.cost_fn;
63
64type parameters = prover_parameters list;
65
66local
67  val rl = R.update_clause_parm o mlibClause.update_literal_order o K;
68  fun rm ns =
69    (R.update_sos_parm o mlibSupport.update_model_parms)
70    (fn l => l @ map (fn n => mlibModel.update_size (K n) mlibModel.defaults) ns);
71in
72  fun R_ordered ns = (rm ns o rl true) R.defaults;
73end;
74
75val default_meson : prover_parameters =
76  (mlibMeson M.defaults, SOME (only_if_everything all_negative), Time 1.0);
77
78val default_delta : prover_parameters =
79  (Delta M.defaults, NONE, Time 0.25);
80
81val default_resolution : prover_parameters =
82  (mlibResolution R.defaults, SOME everything, Time 2.0);
83
84val ordered_resolution : prover_parameters =
85  (mlibResolution (R_ordered [3,4,5]), NONE, Time 4.0);
86
87val defaults = [default_resolution, default_meson, ordered_resolution];
88
89local
90  fun b2s true = "on" | b2s false = "off";
91  val i2s = mlibUseful.int_to_string;
92  fun io2s NONE = "NONE" | io2s (SOME i) = "SOME " ^ i2s i;
93  val r2s = mlibUseful.real_to_string;
94  fun mp2s {size, perts = (p,q)} = i2s size ^ "(" ^ i2s p ^ "+" ^ i2s q ^ ")";
95  fun mpl2s l = "[" ^ join "," (map (int_to_string o #size) l) ^ "]";
96
97  fun f2s (f : mlibClauseset.filter) =
98    "      subsumption ...... " ^ b2s (#subsumption f) ^ "\n" ^
99    "      simplification ... " ^ i2s (#simplification f) ^ "\n" ^
100    "      splitting ........ " ^ b2s (#splitting f) ^ "\n";
101
102  fun raw_rp2s (parm : R.parameters) =
103    let
104      val {clause_parm = c, sos_parm = a, set_parm = b} = parm
105      val {termorder_parm = t, ...} = c
106    in
107      "  clause_parm:\n" ^
108      "    term_order ......... " ^ b2s (#term_order c) ^ "\n" ^
109      "    literal_order ...... " ^ b2s (#literal_order c) ^ "\n" ^
110      "    order_stickiness ... " ^ i2s (#order_stickiness c) ^ "\n" ^
111      "    termorder_parm:\n" ^
112      "      precision ........ " ^ i2s (#precision t) ^ "\n" ^
113      "  sos_parm:\n" ^
114      "    size_power ......... " ^ r2s (#size_power a) ^ "\n" ^
115      "    literal_power ...... " ^ r2s (#literal_power a) ^ "\n" ^
116      "    model_power ........ " ^ r2s (#model_power a) ^ "\n" ^
117      "    model_perts ........ " ^ i2s (#model_perts a) ^ "\n" ^
118      "    model_checks ....... " ^ i2s (#model_checks a) ^ "\n" ^
119      "    model_parms ........ " ^ mpl2s (#model_parms a) ^ "\n" ^
120      "  set_parm:\n" ^
121      "    prefactoring:\n" ^ f2s (#prefactoring b) ^
122      "    postfactoring:\n" ^ f2s (#postfactoring b)
123    end;
124
125  fun rp2s name (parm : R.parameters) = name ^ ":\n" ^ raw_rp2s parm;
126
127  fun rlp2s name parm = name ^ ":\n" ^ join "  +\n" (map raw_rp2s parm);
128
129  fun mp2s name (parm : M.parameters) =
130    name ^ ":\n" ^
131    "  ancestor_pruning ..... " ^ b2s (#ancestor_pruning parm) ^ "\n" ^
132    "  ancestor_cutting ..... " ^ b2s (#ancestor_cutting parm) ^ "\n" ^
133    "  state_simplify ....... " ^ b2s (#state_simplify parm) ^ "\n" ^
134    "  cache_cutting ........ " ^ b2s (#cache_cutting parm) ^ "\n" ^
135    "  divide_conquer ....... " ^ b2s (#divide_conquer parm) ^ "\n" ^
136    "  unit_lemmaizing ...... " ^ b2s (#unit_lemmaizing parm) ^ "\n" ^
137    "  sort_literals ........ " ^ i2s (#sort_literals parm) ^ "\n" ^
138    "  sort_rules ........... " ^ b2s (#sort_rules parm) ^ "\n";
139
140  fun p2s (mlibResolution r) = rp2s "resolution" r
141    | p2s (mlibMeson m) = mp2s "meson" m
142    | p2s (Delta d) = mp2s "delta" d;
143
144  fun s2s (s : sos_filter option) =
145    "sos: " ^ (case s of NONE => "natural" | SOME {name, ...} => name) ^ "\n";
146
147  fun c2s c = "cost_fn: " ^ PP.pp_to_string (!LINE_LENGTH) pp_cost_fn c ^ "\n";
148in
149  fun parameters_to_string (parm : parameters) =
150    join "\n" (map (fn (p,s,c) => p2s p ^ s2s s ^ c2s c) parm);
151end;
152
153(* ------------------------------------------------------------------------- *)
154(* The metis combination of solvers.                                         *)
155(* ------------------------------------------------------------------------- *)
156
157local
158  fun mk_prover (mlibResolution p) = ("r", fn n => R.resolution' (n,p))
159    | mk_prover (mlibMeson p) = ("m", fn n => M.meson' (n,p))
160    | mk_prover (Delta p) = ("d", fn n => M.delta' (n,p));
161
162  fun apply NONE slv = slv | apply (SOME s) slv = apply_sos_filter s slv;
163
164  fun mk_provers ((t,s,c),(l,v)) =
165    let
166      val (n,f) = mk_prover t
167      val n = variant n v
168    in
169      ((c, apply s (f n)) :: l, n :: v)
170    end
171in
172  val metis' = combine o rev o fst o foldl mk_provers ([],[]);
173end;
174
175val metis = metis' defaults;
176
177(* ------------------------------------------------------------------------- *)
178(* A user-friendly interface.                                                *)
179(* ------------------------------------------------------------------------- *)
180
181val settings = ref defaults;
182
183val limit : limit ref = ref {time = NONE, infs = NONE};
184
185fun prove goal =
186    let
187      val {thms,hyps} = clauses goal
188      val solv = metis' (!settings)
189    in
190      refute (initialize solv {limit = !limit, thms = thms, hyps = hyps})
191    end;
192
193fun query database =
194  initialize M.prolog
195  {thms = axiomatize database, hyps = [], limit = unlimited};
196
197end
198