1(* ========================================================================= *)
2(* CNF PROBLEMS                                                              *)
3(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License            *)
4(* ========================================================================= *)
5
6structure Problem :> Problem =
7struct
8
9open Useful;
10
11(* ------------------------------------------------------------------------- *)
12(* Problems.                                                                 *)
13(* ------------------------------------------------------------------------- *)
14
15type problem =
16     {axioms : Thm.clause list,
17      conjecture : Thm.clause list};
18
19fun toClauses {axioms,conjecture} = axioms @ conjecture;
20
21fun size prob =
22    let
23      fun lits (cl,n) = n + LiteralSet.size cl
24
25      fun syms (cl,n) = n + LiteralSet.symbols cl
26
27      fun typedSyms (cl,n) = n + LiteralSet.typedSymbols cl
28
29      val cls = toClauses prob
30    in
31      {clauses = length cls,
32       literals = List.foldl lits 0 cls,
33       symbols = List.foldl syms 0 cls,
34       typedSymbols = List.foldl typedSyms 0 cls}
35    end;
36
37fun freeVars {axioms,conjecture} =
38    NameSet.union
39      (LiteralSet.freeVarsList axioms)
40      (LiteralSet.freeVarsList conjecture);
41
42local
43  fun clauseToFormula cl =
44      Formula.listMkDisj (LiteralSet.transform Literal.toFormula cl);
45in
46  fun toFormula prob =
47      Formula.listMkConj (List.map clauseToFormula (toClauses prob));
48
49  fun toGoal {axioms,conjecture} =
50      let
51        val clToFm = Formula.generalize o clauseToFormula
52        val clsToFm = Formula.listMkConj o List.map clToFm
53
54        val fm = Formula.False
55        val fm =
56            if List.null conjecture then fm
57            else Formula.Imp (clsToFm conjecture, fm)
58        val fm = Formula.Imp (clsToFm axioms, fm)
59      in
60        fm
61      end;
62end;
63
64fun toString prob = Formula.toString (toFormula prob);
65
66(* ------------------------------------------------------------------------- *)
67(* Categorizing problems.                                                    *)
68(* ------------------------------------------------------------------------- *)
69
70datatype propositional =
71    Propositional
72  | EffectivelyPropositional
73  | NonPropositional;
74
75datatype equality =
76    NonEquality
77  | Equality
78  | PureEquality;
79
80datatype horn =
81    Trivial
82  | Unit
83  | DoubleHorn
84  | Horn
85  | NegativeHorn
86  | NonHorn;
87
88type category =
89     {propositional : propositional,
90      equality : equality,
91      horn : horn};
92
93fun categorize prob =
94    let
95      val cls = toClauses prob
96
97      val rels =
98          let
99            fun f (cl,set) = NameAritySet.union set (LiteralSet.relations cl)
100          in
101            List.foldl f NameAritySet.empty cls
102          end
103
104      val funs =
105          let
106            fun f (cl,set) = NameAritySet.union set (LiteralSet.functions cl)
107          in
108            List.foldl f NameAritySet.empty cls
109          end
110
111      val propositional =
112          if NameAritySet.allNullary rels then Propositional
113          else if NameAritySet.allNullary funs then EffectivelyPropositional
114          else NonPropositional
115
116      val equality =
117          if not (NameAritySet.member Atom.eqRelation rels) then NonEquality
118          else if NameAritySet.size rels = 1 then PureEquality
119          else Equality
120
121      val horn =
122          if List.exists LiteralSet.null cls then Trivial
123          else if List.all (fn cl => LiteralSet.size cl = 1) cls then Unit
124          else
125            let
126              fun pos cl = LiteralSet.count Literal.positive cl <= 1
127              fun neg cl = LiteralSet.count Literal.negative cl <= 1
128            in
129              case (List.all pos cls, List.all neg cls) of
130                (true,true) => DoubleHorn
131              | (true,false) => Horn
132              | (false,true) => NegativeHorn
133              | (false,false) => NonHorn
134            end
135    in
136      {propositional = propositional,
137       equality = equality,
138       horn = horn}
139    end;
140
141fun categoryToString {propositional,equality,horn} =
142    (case propositional of
143       Propositional => "propositional"
144     | EffectivelyPropositional => "effectively propositional"
145     | NonPropositional => "non-propositional") ^
146    ", " ^
147    (case equality of
148       NonEquality => "non-equality"
149     | Equality => "equality"
150     | PureEquality => "pure equality") ^
151    ", " ^
152    (case horn of
153       Trivial => "trivial"
154     | Unit => "unit"
155     | DoubleHorn => "horn (and negative horn)"
156     | Horn => "horn"
157     | NegativeHorn => "negative horn"
158     | NonHorn => "non-horn");
159
160end
161