1(* ========================================================================= *)
2(* THE RESOLUTION PROOF PROCEDURE                                            *)
3(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License            *)
4(* ========================================================================= *)
5
6structure Resolution :> Resolution =
7struct
8
9open Useful;
10
11(* ------------------------------------------------------------------------- *)
12(* A type of resolution proof procedures.                                    *)
13(* ------------------------------------------------------------------------- *)
14
15type parameters =
16     {active : Active.parameters,
17      waiting : Waiting.parameters};
18
19datatype resolution =
20    Resolution of
21      {parameters : parameters,
22       active : Active.active,
23       waiting : Waiting.waiting};
24
25(* ------------------------------------------------------------------------- *)
26(* Basic operations.                                                         *)
27(* ------------------------------------------------------------------------- *)
28
29val default : parameters =
30    {active = Active.default,
31     waiting = Waiting.default};
32
33fun new parameters ths =
34    let
35      val {active = activeParm, waiting = waitingParm} = parameters
36
37      val (active,cls) = Active.new activeParm ths  (* cls = factored ths *)
38
39      val waiting = Waiting.new waitingParm cls
40    in
41      Resolution {parameters = parameters, active = active, waiting = waiting}
42    end
43(*MetisDebug
44    handle e =>
45      let
46        val () = Print.trace Print.ppException "Resolution.new: exception" e
47      in
48        raise e
49      end;
50*)
51
52fun active (Resolution {active = a, ...}) = a;
53
54fun waiting (Resolution {waiting = w, ...}) = w;
55
56val pp =
57    Print.ppMap
58      (fn Resolution {active,waiting,...} =>
59          "Resolution(" ^ Int.toString (Active.size active) ^
60          "<-" ^ Int.toString (Waiting.size waiting) ^ ")")
61      Print.ppString;
62
63(* ------------------------------------------------------------------------- *)
64(* The main proof loop.                                                      *)
65(* ------------------------------------------------------------------------- *)
66
67datatype decision =
68    Contradiction of Thm.thm
69  | Satisfiable of Thm.thm list;
70
71datatype state =
72    Decided of decision
73  | Undecided of resolution;
74
75fun iterate res =
76    let
77      val Resolution {parameters,active,waiting} = res
78
79(*MetisTrace2
80      val () = Print.trace Active.pp "Resolution.iterate: active" active
81      val () = Print.trace Waiting.pp "Resolution.iterate: waiting" waiting
82*)
83    in
84      case Waiting.remove waiting of
85        NONE =>
86        let
87          val sat = Satisfiable (List.map Clause.thm (Active.saturation active))
88        in
89          Decided sat
90        end
91      | SOME ((d,cl),waiting) =>
92        if Clause.isContradiction cl then
93          Decided (Contradiction (Clause.thm cl))
94        else
95          let
96(*MetisTrace1
97            val () = Print.trace Clause.pp "Resolution.iterate: cl" cl
98*)
99            val (active,cls) = Active.add active cl
100
101            val waiting = Waiting.add waiting (d,cls)
102
103            val res =
104                Resolution
105                  {parameters = parameters,
106                   active = active,
107                   waiting = waiting}
108          in
109            Undecided res
110          end
111    end;
112
113fun loop res =
114    case iterate res of
115      Decided dec => dec
116    | Undecided res => loop res;
117
118end
119