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