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