39348
|
1 |
(* ========================================================================= *)
|
|
2 |
(* CNF PROBLEMS *)
|
39349
|
3 |
(* Copyright (c) 2001-2008 Joe Hurd, distributed under the BSD License *)
|
39348
|
4 |
(* ========================================================================= *)
|
|
5 |
|
|
6 |
structure Problem :> Problem =
|
|
7 |
struct
|
|
8 |
|
|
9 |
open Useful;
|
|
10 |
|
|
11 |
(* ------------------------------------------------------------------------- *)
|
|
12 |
(* Problems. *)
|
|
13 |
(* ------------------------------------------------------------------------- *)
|
|
14 |
|
|
15 |
type problem =
|
|
16 |
{axioms : Thm.clause list,
|
|
17 |
conjecture : Thm.clause list};
|
|
18 |
|
|
19 |
fun toClauses {axioms,conjecture} = axioms @ conjecture;
|
|
20 |
|
|
21 |
fun 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 = foldl lits 0 cls,
|
|
33 |
symbols = foldl syms 0 cls,
|
|
34 |
typedSymbols = foldl typedSyms 0 cls}
|
|
35 |
end;
|
|
36 |
|
|
37 |
fun freeVars {axioms,conjecture} =
|
|
38 |
NameSet.union
|
|
39 |
(LiteralSet.freeVarsList axioms)
|
|
40 |
(LiteralSet.freeVarsList conjecture);
|
|
41 |
|
|
42 |
local
|
|
43 |
fun clauseToFormula cl =
|
|
44 |
Formula.listMkDisj (LiteralSet.transform Literal.toFormula cl);
|
|
45 |
in
|
|
46 |
fun toFormula prob =
|
|
47 |
Formula.listMkConj (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 map clToFm
|
|
53 |
|
|
54 |
val fm = Formula.False
|
|
55 |
val fm =
|
|
56 |
if 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;
|
|
62 |
end;
|
|
63 |
|
|
64 |
fun toString prob = Formula.toString (toFormula prob);
|
|
65 |
|
|
66 |
(* ------------------------------------------------------------------------- *)
|
|
67 |
(* Categorizing problems. *)
|
|
68 |
(* ------------------------------------------------------------------------- *)
|
|
69 |
|
|
70 |
datatype propositional =
|
|
71 |
Propositional
|
|
72 |
| EffectivelyPropositional
|
|
73 |
| NonPropositional;
|
|
74 |
|
|
75 |
datatype equality =
|
|
76 |
NonEquality
|
|
77 |
| Equality
|
|
78 |
| PureEquality;
|
|
79 |
|
|
80 |
datatype horn =
|
|
81 |
Trivial
|
|
82 |
| Unit
|
|
83 |
| DoubleHorn
|
|
84 |
| Horn
|
|
85 |
| NegativeHorn
|
|
86 |
| NonHorn;
|
|
87 |
|
|
88 |
type category =
|
|
89 |
{propositional : propositional,
|
|
90 |
equality : equality,
|
|
91 |
horn : horn};
|
|
92 |
|
|
93 |
fun 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 |
|
|
141 |
fun 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 |
|
|
160 |
end
|