1(* ========================================================================= *) 2(* PACKAGING UP SOLVERS TO ALLOW THEM TO COOPERATE UNIFORMLY *) 3(* Copyright (c) 2002-2004 Joe Hurd. *) 4(* ========================================================================= *) 5 6signature mlibSolver = 7sig 8 9type 'a pp = 'a mlibUseful.pp 10type 'a stream = 'a mlibStream.stream 11type formula = mlibTerm.formula 12type thm = mlibThm.thm 13type limit = mlibMeter.limit 14type meter = mlibMeter.meter 15type meter_reading = mlibMeter.meter_reading 16type units = mlibUnits.units 17 18(* The type of a generic solver *) 19 20type solver = formula list -> thm list option stream 21 22val contradiction_solver : thm -> solver 23 24(* Filters to cut off searching or drop subsumed solutions *) 25 26val solved_filter : solver -> solver 27val subsumed_filter : solver -> solver 28 29(* User-friendly interface to generic solvers *) 30 31val solve : solver -> int -> formula list -> thm list list 32val find : solver -> formula list -> thm list option 33val refute : solver -> thm option 34 35(* mlibSolver nodes must construct themselves from the following form. *) 36 37type form = 38 {slice : meter ref, (* A meter to stop after each slice *) 39 units : units ref, (* mlibSolvers share a unit cache *) 40 thms : thm list, (* Context, assumed consistent *) 41 hyps : thm list} (* Hypothesis, or set of support *) 42 43(* mlibSolver nodes also incorporate a name. *) 44 45type node_data = {name : string, solver_con : form -> solver} 46type solver_node 47 48val mk_solver_node : node_data -> solver_node 49val pp_solver_node : solver_node pp 50 51(* At each step we schedule a slice to the least cost solver node. *) 52 53val SLICE : real ref 54 55datatype cost_fn = 56 Time of real (* Time used divided by a coefficient *) 57| Infs of real (* Inferences divided by a coefficient *) 58val pp_cost_fn : cost_fn pp 59 60(* This allows us to hierarchically arrange solver nodes. *) 61 62val combine : (cost_fn * solver_node) list -> solver_node 63 64(* Overriding the 'natural' set of support from the problem. *) 65 66type sos_filter = {name : string, filter : thm -> bool} 67val apply_sos_filter : sos_filter -> solver_node -> solver_node 68val only_if_everything : sos_filter -> sos_filter 69 70val everything : sos_filter 71val one_negative : sos_filter 72val one_positive : sos_filter 73val all_negative : sos_filter 74val all_positive : sos_filter 75 76(* Initializing a solver node makes it ready for action. *) 77 78type init_data = {limit : limit, thms : thm list, hyps : thm list} 79 80val initialize : solver_node -> init_data -> solver 81 82end 83