author | webertj |
Sun, 09 Oct 2005 17:06:03 +0200 | |
changeset 17809 | 195045659c06 |
parent 16913 | 1d8a8d010e69 |
child 20442 | 04621ea9440e |
permissions | -rw-r--r-- |
14452 | 1 |
(* Title: HOL/Tools/prop_logic.ML |
2 |
ID: $Id$ |
|
3 |
Author: Tjark Weber |
|
16907 | 4 |
Copyright 2004-2005 |
14452 | 5 |
|
6 |
Formulas of propositional logic. |
|
7 |
*) |
|
8 |
||
9 |
signature PROP_LOGIC = |
|
10 |
sig |
|
11 |
datatype prop_formula = |
|
12 |
True |
|
13 |
| False |
|
14 |
| BoolVar of int (* NOTE: only use indices >= 1 *) |
|
15 |
| Not of prop_formula |
|
16 |
| Or of prop_formula * prop_formula |
|
17 |
| And of prop_formula * prop_formula |
|
18 |
||
16909
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
19 |
val SNot : prop_formula -> prop_formula |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
20 |
val SOr : prop_formula * prop_formula -> prop_formula |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
21 |
val SAnd : prop_formula * prop_formula -> prop_formula |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
22 |
val simplify : prop_formula -> prop_formula (* eliminates True/False and double-negation *) |
14452 | 23 |
|
14681 | 24 |
val indices : prop_formula -> int list (* set of all variable indices *) |
15301 | 25 |
val maxidx : prop_formula -> int (* maximal variable index *) |
14452 | 26 |
|
27 |
val exists : prop_formula list -> prop_formula (* finite disjunction *) |
|
28 |
val all : prop_formula list -> prop_formula (* finite conjunction *) |
|
29 |
val dot_product : prop_formula list * prop_formula list -> prop_formula |
|
30 |
||
16909
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
31 |
val nnf : prop_formula -> prop_formula (* negation normal form *) |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
32 |
val cnf : prop_formula -> prop_formula (* conjunctive normal form *) |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
33 |
val auxcnf : prop_formula -> prop_formula (* cnf with auxiliary variables *) |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
34 |
val defcnf : prop_formula -> prop_formula (* definitional cnf *) |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
35 |
|
14452 | 36 |
val eval : (int -> bool) -> prop_formula -> bool (* semantics *) |
17809
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
16913
diff
changeset
|
37 |
|
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
16913
diff
changeset
|
38 |
val prop_formula_of_term : Term.term -> int Termtab.table -> prop_formula * int Termtab.table |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
16913
diff
changeset
|
39 |
(* propositional representation of HOL terms *) |
14452 | 40 |
end; |
41 |
||
42 |
structure PropLogic : PROP_LOGIC = |
|
43 |
struct |
|
44 |
||
45 |
(* ------------------------------------------------------------------------- *) |
|
14753 | 46 |
(* prop_formula: formulas of propositional logic, built from Boolean *) |
14452 | 47 |
(* variables (referred to by index) and True/False using *) |
48 |
(* not/or/and *) |
|
49 |
(* ------------------------------------------------------------------------- *) |
|
50 |
||
51 |
datatype prop_formula = |
|
52 |
True |
|
53 |
| False |
|
54 |
| BoolVar of int (* NOTE: only use indices >= 1 *) |
|
55 |
| Not of prop_formula |
|
56 |
| Or of prop_formula * prop_formula |
|
57 |
| And of prop_formula * prop_formula; |
|
58 |
||
59 |
(* ------------------------------------------------------------------------- *) |
|
60 |
(* The following constructor functions make sure that True and False do not *) |
|
61 |
(* occur within any of the other connectives (i.e. Not, Or, And), and *) |
|
62 |
(* perform double-negation elimination. *) |
|
63 |
(* ------------------------------------------------------------------------- *) |
|
64 |
||
65 |
(* prop_formula -> prop_formula *) |
|
66 |
||
67 |
fun SNot True = False |
|
68 |
| SNot False = True |
|
69 |
| SNot (Not fm) = fm |
|
70 |
| SNot fm = Not fm; |
|
71 |
||
72 |
(* prop_formula * prop_formula -> prop_formula *) |
|
73 |
||
74 |
fun SOr (True, _) = True |
|
75 |
| SOr (_, True) = True |
|
76 |
| SOr (False, fm) = fm |
|
77 |
| SOr (fm, False) = fm |
|
78 |
| SOr (fm1, fm2) = Or (fm1, fm2); |
|
79 |
||
80 |
(* prop_formula * prop_formula -> prop_formula *) |
|
81 |
||
82 |
fun SAnd (True, fm) = fm |
|
83 |
| SAnd (fm, True) = fm |
|
84 |
| SAnd (False, _) = False |
|
85 |
| SAnd (_, False) = False |
|
86 |
| SAnd (fm1, fm2) = And (fm1, fm2); |
|
87 |
||
88 |
(* ------------------------------------------------------------------------- *) |
|
16909
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
89 |
(* simplify: eliminates True/False below other connectives, and double- *) |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
90 |
(* negation *) |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
91 |
(* ------------------------------------------------------------------------- *) |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
92 |
|
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
93 |
(* prop_formula -> prop_formula *) |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
94 |
|
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
95 |
fun simplify (Not fm) = SNot (simplify fm) |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
96 |
| simplify (Or (fm1, fm2)) = SOr (simplify fm1, simplify fm2) |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
97 |
| simplify (And (fm1, fm2)) = SAnd (simplify fm1, simplify fm2) |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
98 |
| simplify fm = fm; |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
99 |
|
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
100 |
(* ------------------------------------------------------------------------- *) |
14753 | 101 |
(* indices: collects all indices of Boolean variables that occur in a *) |
14452 | 102 |
(* propositional formula 'fm'; no duplicates *) |
103 |
(* ------------------------------------------------------------------------- *) |
|
104 |
||
105 |
(* prop_formula -> int list *) |
|
106 |
||
16909
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
107 |
fun indices True = [] |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
108 |
| indices False = [] |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
109 |
| indices (BoolVar i) = [i] |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
110 |
| indices (Not fm) = indices fm |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
111 |
| indices (Or (fm1, fm2)) = (indices fm1) union_int (indices fm2) |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
112 |
| indices (And (fm1, fm2)) = (indices fm1) union_int (indices fm2); |
14452 | 113 |
|
114 |
(* ------------------------------------------------------------------------- *) |
|
115 |
(* maxidx: computes the maximal variable index occuring in a formula of *) |
|
116 |
(* propositional logic 'fm'; 0 if 'fm' contains no variable *) |
|
117 |
(* ------------------------------------------------------------------------- *) |
|
118 |
||
119 |
(* prop_formula -> int *) |
|
120 |
||
16909
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
121 |
fun maxidx True = 0 |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
122 |
| maxidx False = 0 |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
123 |
| maxidx (BoolVar i) = i |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
124 |
| maxidx (Not fm) = maxidx fm |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
125 |
| maxidx (Or (fm1, fm2)) = Int.max (maxidx fm1, maxidx fm2) |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
126 |
| maxidx (And (fm1, fm2)) = Int.max (maxidx fm1, maxidx fm2); |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
127 |
|
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
128 |
(* ------------------------------------------------------------------------- *) |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
129 |
(* exists: computes the disjunction over a list 'xs' of propositional *) |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
130 |
(* formulas *) |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
131 |
(* ------------------------------------------------------------------------- *) |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
132 |
|
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
133 |
(* prop_formula list -> prop_formula *) |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
134 |
|
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
135 |
fun exists xs = Library.foldl SOr (False, xs); |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
136 |
|
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
137 |
(* ------------------------------------------------------------------------- *) |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
138 |
(* all: computes the conjunction over a list 'xs' of propositional formulas *) |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
139 |
(* ------------------------------------------------------------------------- *) |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
140 |
|
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
141 |
(* prop_formula list -> prop_formula *) |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
142 |
|
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
143 |
fun all xs = Library.foldl SAnd (True, xs); |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
144 |
|
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
145 |
(* ------------------------------------------------------------------------- *) |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
146 |
(* dot_product: ([x1,...,xn], [y1,...,yn]) -> x1*y1+...+xn*yn *) |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
147 |
(* ------------------------------------------------------------------------- *) |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
148 |
|
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
149 |
(* prop_formula list * prop_formula list -> prop_formula *) |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
150 |
|
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
151 |
fun dot_product (xs,ys) = exists (map SAnd (xs~~ys)); |
14452 | 152 |
|
153 |
(* ------------------------------------------------------------------------- *) |
|
154 |
(* nnf: computes the negation normal form of a formula 'fm' of propositional *) |
|
16909
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
155 |
(* logic (i.e. only variables may be negated, but not subformulas). *) |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
156 |
(* Simplification (c.f. 'simplify') is performed as well. *) |
14452 | 157 |
(* ------------------------------------------------------------------------- *) |
158 |
||
159 |
(* prop_formula -> prop_formula *) |
|
160 |
||
161 |
fun |
|
162 |
(* constants *) |
|
16909
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
163 |
nnf True = True |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
164 |
| nnf False = False |
14452 | 165 |
(* variables *) |
16909
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
166 |
| nnf (BoolVar i) = (BoolVar i) |
14452 | 167 |
(* 'or' and 'and' as outermost connectives are left untouched *) |
16909
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
168 |
| nnf (Or (fm1, fm2)) = SOr (nnf fm1, nnf fm2) |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
169 |
| nnf (And (fm1, fm2)) = SAnd (nnf fm1, nnf fm2) |
14452 | 170 |
(* 'not' + constant *) |
16909
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
171 |
| nnf (Not True) = False |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
172 |
| nnf (Not False) = True |
14452 | 173 |
(* 'not' + variable *) |
16909
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
174 |
| nnf (Not (BoolVar i)) = Not (BoolVar i) |
14452 | 175 |
(* pushing 'not' inside of 'or'/'and' using de Morgan's laws *) |
16909
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
176 |
| nnf (Not (Or (fm1, fm2))) = SAnd (nnf (SNot fm1), nnf (SNot fm2)) |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
177 |
| nnf (Not (And (fm1, fm2))) = SOr (nnf (SNot fm1), nnf (SNot fm2)) |
14452 | 178 |
(* double-negation elimination *) |
16909
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
179 |
| nnf (Not (Not fm)) = nnf fm; |
14452 | 180 |
|
181 |
(* ------------------------------------------------------------------------- *) |
|
14681 | 182 |
(* cnf: computes the conjunctive normal form (i.e. a conjunction of *) |
183 |
(* disjunctions) of a formula 'fm' of propositional logic. The result *) |
|
184 |
(* formula may be exponentially longer than 'fm'. *) |
|
14452 | 185 |
(* ------------------------------------------------------------------------- *) |
186 |
||
187 |
(* prop_formula -> prop_formula *) |
|
188 |
||
189 |
fun cnf fm = |
|
190 |
let |
|
191 |
fun |
|
192 |
(* constants *) |
|
14939 | 193 |
cnf_from_nnf True = True |
194 |
| cnf_from_nnf False = False |
|
14452 | 195 |
(* literals *) |
14939 | 196 |
| cnf_from_nnf (BoolVar i) = BoolVar i |
197 |
| cnf_from_nnf (Not fm1) = Not fm1 (* 'fm1' must be a variable since the formula is in NNF *) |
|
14452 | 198 |
(* pushing 'or' inside of 'and' using distributive laws *) |
14939 | 199 |
| cnf_from_nnf (Or (fm1, fm2)) = |
14452 | 200 |
let |
14939 | 201 |
fun cnf_or (And (fm11, fm12), fm2) = |
202 |
And (cnf_or (fm11, fm2), cnf_or (fm12, fm2)) |
|
203 |
| cnf_or (fm1, And (fm21, fm22)) = |
|
204 |
And (cnf_or (fm1, fm21), cnf_or (fm1, fm22)) |
|
205 |
(* neither subformula contains 'and' *) |
|
206 |
| cnf_or (fm1, fm2) = |
|
207 |
Or (fm1, fm2) |
|
14452 | 208 |
in |
14939 | 209 |
cnf_or (cnf_from_nnf fm1, cnf_from_nnf fm2) |
14452 | 210 |
end |
211 |
(* 'and' as outermost connective is left untouched *) |
|
14939 | 212 |
| cnf_from_nnf (And (fm1, fm2)) = And (cnf_from_nnf fm1, cnf_from_nnf fm2) |
14452 | 213 |
in |
214 |
(cnf_from_nnf o nnf) fm |
|
215 |
end; |
|
216 |
||
217 |
(* ------------------------------------------------------------------------- *) |
|
16909
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
218 |
(* auxcnf: computes the definitional conjunctive normal form of a formula *) |
14681 | 219 |
(* 'fm' of propositional logic, introducing auxiliary variables if *) |
220 |
(* necessary to avoid an exponential blowup of the formula. The result *) |
|
221 |
(* formula is satisfiable if and only if 'fm' is satisfiable. *) |
|
16907 | 222 |
(* Auxiliary variables are introduced as switches for OR-nodes, based *) |
16909
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
223 |
(* on the observation that e.g. "fm1 OR (fm21 AND fm22)" is *) |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
224 |
(* equisatisfiable with "(fm1 OR ~aux) AND (fm21 OR aux) AND (fm22 OR *) |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
225 |
(* aux)". *) |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
226 |
(* ------------------------------------------------------------------------- *) |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
227 |
|
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
228 |
(* ------------------------------------------------------------------------- *) |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
229 |
(* Note: 'auxcnf' tends to use fewer variables and fewer clauses than *) |
16913 | 230 |
(* 'defcnf' below, but sometimes generates much larger SAT problems *) |
16909
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
231 |
(* overall (hence it must sometimes generate longer clauses than *) |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
232 |
(* 'defcnf' does). It is currently not quite clear to me if one of the *) |
16913 | 233 |
(* algorithms is clearly superior to the other, but I suggest using *) |
234 |
(* 'defcnf' instead. *) |
|
14452 | 235 |
(* ------------------------------------------------------------------------- *) |
236 |
||
237 |
(* prop_formula -> prop_formula *) |
|
238 |
||
16909
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
239 |
fun auxcnf fm = |
14452 | 240 |
let |
16907 | 241 |
(* convert formula to NNF first *) |
242 |
val fm' = nnf fm |
|
14452 | 243 |
(* 'new' specifies the next index that is available to introduce an auxiliary variable *) |
16907 | 244 |
(* int ref *) |
245 |
val new = ref (maxidx fm' + 1) |
|
246 |
(* unit -> int *) |
|
247 |
fun new_idx () = let val idx = !new in new := idx+1; idx end |
|
248 |
(* prop_formula -> prop_formula *) |
|
14452 | 249 |
fun |
250 |
(* constants *) |
|
16909
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
251 |
auxcnf_from_nnf True = True |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
252 |
| auxcnf_from_nnf False = False |
14452 | 253 |
(* literals *) |
16909
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
254 |
| auxcnf_from_nnf (BoolVar i) = BoolVar i |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
255 |
| auxcnf_from_nnf (Not fm1) = Not fm1 (* 'fm1' must be a variable since the formula is in NNF *) |
14939 | 256 |
(* pushing 'or' inside of 'and' using auxiliary variables *) |
16909
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
257 |
| auxcnf_from_nnf (Or (fm1, fm2)) = |
14452 | 258 |
let |
16909
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
259 |
val fm1' = auxcnf_from_nnf fm1 |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
260 |
val fm2' = auxcnf_from_nnf fm2 |
16907 | 261 |
(* prop_formula * prop_formula -> prop_formula *) |
16909
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
262 |
fun auxcnf_or (And (fm11, fm12), fm2) = |
14964 | 263 |
(case fm2 of |
264 |
(* do not introduce an auxiliary variable for literals *) |
|
265 |
BoolVar _ => |
|
16909
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
266 |
And (auxcnf_or (fm11, fm2), auxcnf_or (fm12, fm2)) |
14964 | 267 |
| Not _ => |
16909
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
268 |
And (auxcnf_or (fm11, fm2), auxcnf_or (fm12, fm2)) |
14964 | 269 |
| _ => |
270 |
let |
|
16907 | 271 |
val aux = BoolVar (new_idx ()) |
14964 | 272 |
in |
16909
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
273 |
And (And (auxcnf_or (fm11, aux), auxcnf_or (fm12, aux)), auxcnf_or (fm2, Not aux)) |
14964 | 274 |
end) |
16909
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
275 |
| auxcnf_or (fm1, And (fm21, fm22)) = |
14964 | 276 |
(case fm1 of |
277 |
(* do not introduce an auxiliary variable for literals *) |
|
278 |
BoolVar _ => |
|
16909
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
279 |
And (auxcnf_or (fm1, fm21), auxcnf_or (fm1, fm22)) |
14964 | 280 |
| Not _ => |
16909
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
281 |
And (auxcnf_or (fm1, fm21), auxcnf_or (fm1, fm22)) |
14964 | 282 |
| _ => |
283 |
let |
|
16907 | 284 |
val aux = BoolVar (new_idx ()) |
14964 | 285 |
in |
16909
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
286 |
And (auxcnf_or (fm1, Not aux), And (auxcnf_or (fm21, aux), auxcnf_or (fm22, aux))) |
14964 | 287 |
end) |
14939 | 288 |
(* neither subformula contains 'and' *) |
16909
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
289 |
| auxcnf_or (fm1, fm2) = |
16907 | 290 |
Or (fm1, fm2) |
14939 | 291 |
in |
16909
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
292 |
auxcnf_or (fm1', fm2') |
14452 | 293 |
end |
294 |
(* 'and' as outermost connective is left untouched *) |
|
16909
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
295 |
| auxcnf_from_nnf (And (fm1, fm2)) = |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
296 |
And (auxcnf_from_nnf fm1, auxcnf_from_nnf fm2) |
14452 | 297 |
in |
16909
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
298 |
auxcnf_from_nnf fm' |
14452 | 299 |
end; |
300 |
||
301 |
(* ------------------------------------------------------------------------- *) |
|
16909
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
302 |
(* defcnf: computes the definitional conjunctive normal form of a formula *) |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
303 |
(* 'fm' of propositional logic, introducing auxiliary variables to *) |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
304 |
(* avoid an exponential blowup of the formula. The result formula is *) |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
305 |
(* satisfiable if and only if 'fm' is satisfiable. Auxiliary variables *) |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
306 |
(* are introduced as abbreviations for AND-, OR-, and NOT-nodes, based *) |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
307 |
(* on the following equisatisfiabilities (+/- indicates polarity): *) |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
308 |
(* LITERAL+ == LITERAL *) |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
309 |
(* LITERAL- == NOT LITERAL *) |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
310 |
(* (NOT fm1)+ == aux AND (NOT aux OR fm1-) *) |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
311 |
(* (fm1 OR fm2)+ == aux AND (NOT aux OR fm1+ OR fm2+) *) |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
312 |
(* (fm1 AND fm2)+ == aux AND (NOT aux OR fm1+) AND (NOT aux OR fm2+) *) |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
313 |
(* (NOT fm1)- == aux AND (NOT aux OR fm1+) *) |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
314 |
(* (fm1 OR fm2)- == aux AND (NOT aux OR fm1-) AND (NOT aux OR fm2-) *) |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
315 |
(* (fm1 AND fm2)- == aux AND (NOT aux OR fm1- OR fm2-) *) |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
316 |
(* Example: *) |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
317 |
(* NOT (a AND b) == aux1 AND (NOT aux1 OR aux2) *) |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
318 |
(* AND (NOT aux2 OR NOT a OR NOT b) *) |
14452 | 319 |
(* ------------------------------------------------------------------------- *) |
320 |
||
16909
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
321 |
(* prop_formula -> prop_formula *) |
14452 | 322 |
|
16909
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
323 |
fun defcnf fm = |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
324 |
let |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
325 |
(* simplify formula first *) |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
326 |
val fm' = simplify fm |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
327 |
(* 'new' specifies the next index that is available to introduce an auxiliary variable *) |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
328 |
(* int ref *) |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
329 |
val new = ref (maxidx fm' + 1) |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
330 |
(* unit -> int *) |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
331 |
fun new_idx () = let val idx = !new in new := idx+1; idx end |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
332 |
(* optimization for n-ary disjunction/conjunction *) |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
333 |
(* prop_formula -> prop_formula list *) |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
334 |
fun disjuncts (Or (fm1, fm2)) = (disjuncts fm1) @ (disjuncts fm2) |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
335 |
| disjuncts fm1 = [fm1] |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
336 |
(* prop_formula -> prop_formula list *) |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
337 |
fun conjuncts (And (fm1, fm2)) = (conjuncts fm1) @ (conjuncts fm2) |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
338 |
| conjuncts fm1 = [fm1] |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
339 |
(* polarity -> formula -> (defining clauses, literal) *) |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
340 |
(* bool -> prop_formula -> prop_formula * prop_formula *) |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
341 |
fun |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
342 |
(* constants *) |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
343 |
defcnf' true True = (True, True) |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
344 |
| defcnf' false True = (*(True, False)*) error "formula is not simplified, True occurs with negative polarity" |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
345 |
| defcnf' true False = (True, False) |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
346 |
| defcnf' false False = (*(True, True)*) error "formula is not simplified, False occurs with negative polarity" |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
347 |
(* literals *) |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
348 |
| defcnf' true (BoolVar i) = (True, BoolVar i) |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
349 |
| defcnf' false (BoolVar i) = (True, Not (BoolVar i)) |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
350 |
| defcnf' true (Not (BoolVar i)) = (True, Not (BoolVar i)) |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
351 |
| defcnf' false (Not (BoolVar i)) = (True, BoolVar i) |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
352 |
(* 'not' *) |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
353 |
| defcnf' polarity (Not fm1) = |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
354 |
let |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
355 |
val (def1, aux1) = defcnf' (not polarity) fm1 |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
356 |
val aux = BoolVar (new_idx ()) |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
357 |
val def = Or (Not aux, aux1) |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
358 |
in |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
359 |
(SAnd (def1, def), aux) |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
360 |
end |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
361 |
(* 'or' *) |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
362 |
| defcnf' polarity (Or (fm1, fm2)) = |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
363 |
let |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
364 |
val fms = disjuncts (Or (fm1, fm2)) |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
365 |
val (defs, auxs) = split_list (map (defcnf' polarity) fms) |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
366 |
val aux = BoolVar (new_idx ()) |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
367 |
val def = if polarity then Or (Not aux, exists auxs) else all (map (fn a => Or (Not aux, a)) auxs) |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
368 |
in |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
369 |
(SAnd (all defs, def), aux) |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
370 |
end |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
371 |
(* 'and' *) |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
372 |
| defcnf' polarity (And (fm1, fm2)) = |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
373 |
let |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
374 |
val fms = conjuncts (And (fm1, fm2)) |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
375 |
val (defs, auxs) = split_list (map (defcnf' polarity) fms) |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
376 |
val aux = BoolVar (new_idx ()) |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
377 |
val def = if not polarity then Or (Not aux, exists auxs) else all (map (fn a => Or (Not aux, a)) auxs) |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
378 |
in |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
379 |
(SAnd (all defs, def), aux) |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
380 |
end |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
381 |
(* optimization: do not introduce auxiliary variables for parts of the formula that are in CNF already *) |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
382 |
(* prop_formula -> prop_formula * prop_formula *) |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
383 |
fun defcnf_or (Or (fm1, fm2)) = |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
384 |
let |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
385 |
val (def1, aux1) = defcnf_or fm1 |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
386 |
val (def2, aux2) = defcnf_or fm2 |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
387 |
in |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
388 |
(SAnd (def1, def2), Or (aux1, aux2)) |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
389 |
end |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
390 |
| defcnf_or fm = |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
391 |
defcnf' true fm |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
392 |
(* prop_formula -> prop_formula * prop_formula *) |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
393 |
fun defcnf_and (And (fm1, fm2)) = |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
394 |
let |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
395 |
val (def1, aux1) = defcnf_and fm1 |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
396 |
val (def2, aux2) = defcnf_and fm2 |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
397 |
in |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
398 |
(SAnd (def1, def2), And (aux1, aux2)) |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
399 |
end |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
400 |
| defcnf_and (Or (fm1, fm2)) = |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
401 |
let |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
402 |
val (def1, aux1) = defcnf_or fm1 |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
403 |
val (def2, aux2) = defcnf_or fm2 |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
404 |
in |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
405 |
(SAnd (def1, def2), Or (aux1, aux2)) |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
406 |
end |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
407 |
| defcnf_and fm = |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
408 |
defcnf' true fm |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
409 |
in |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
410 |
SAnd (defcnf_and fm') |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
411 |
end; |
14452 | 412 |
|
413 |
(* ------------------------------------------------------------------------- *) |
|
14753 | 414 |
(* eval: given an assignment 'a' of Boolean values to variable indices, the *) |
14452 | 415 |
(* truth value of a propositional formula 'fm' is computed *) |
416 |
(* ------------------------------------------------------------------------- *) |
|
417 |
||
418 |
(* (int -> bool) -> prop_formula -> bool *) |
|
419 |
||
420 |
fun eval a True = true |
|
421 |
| eval a False = false |
|
422 |
| eval a (BoolVar i) = (a i) |
|
423 |
| eval a (Not fm) = not (eval a fm) |
|
424 |
| eval a (Or (fm1,fm2)) = (eval a fm1) orelse (eval a fm2) |
|
425 |
| eval a (And (fm1,fm2)) = (eval a fm1) andalso (eval a fm2); |
|
426 |
||
17809
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
16913
diff
changeset
|
427 |
(* ------------------------------------------------------------------------- *) |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
16913
diff
changeset
|
428 |
(* prop_formula_of_term: returns the propositional structure of a HOL term, *) |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
16913
diff
changeset
|
429 |
(* with subterms replaced by Boolean variables. Also returns a table *) |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
16913
diff
changeset
|
430 |
(* of terms and corresponding variables that extends the table that was *) |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
16913
diff
changeset
|
431 |
(* given as an argument. Usually, you'll just want to use *) |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
16913
diff
changeset
|
432 |
(* 'Termtab.empty' as value for 'table'. *) |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
16913
diff
changeset
|
433 |
(* ------------------------------------------------------------------------- *) |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
16913
diff
changeset
|
434 |
|
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
16913
diff
changeset
|
435 |
(* Note: The implementation is somewhat optimized; the next index to be used *) |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
16913
diff
changeset
|
436 |
(* is computed only when it is actually needed. However, when *) |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
16913
diff
changeset
|
437 |
(* 'prop_formula_of_term' is invoked many times, it might be more *) |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
16913
diff
changeset
|
438 |
(* efficient to pass and return this value as an additional parameter, *) |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
16913
diff
changeset
|
439 |
(* so that it does not have to be recomputed (by folding over the *) |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
16913
diff
changeset
|
440 |
(* table) for each invocation. *) |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
16913
diff
changeset
|
441 |
|
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
16913
diff
changeset
|
442 |
(* Term.term -> int Termtab.table -> prop_formula * int Termtab.table *) |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
16913
diff
changeset
|
443 |
fun prop_formula_of_term t table = |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
16913
diff
changeset
|
444 |
let |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
16913
diff
changeset
|
445 |
val next_idx_is_valid = ref false |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
16913
diff
changeset
|
446 |
val next_idx = ref 0 |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
16913
diff
changeset
|
447 |
fun get_next_idx () = |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
16913
diff
changeset
|
448 |
if !next_idx_is_valid then |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
16913
diff
changeset
|
449 |
inc next_idx |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
16913
diff
changeset
|
450 |
else ( |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
16913
diff
changeset
|
451 |
next_idx := Termtab.fold (curry Int.max o snd) table 0; |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
16913
diff
changeset
|
452 |
next_idx_is_valid := true; |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
16913
diff
changeset
|
453 |
inc next_idx |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
16913
diff
changeset
|
454 |
) |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
16913
diff
changeset
|
455 |
fun aux (Const ("True", _)) table = |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
16913
diff
changeset
|
456 |
(True, table) |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
16913
diff
changeset
|
457 |
| aux (Const ("False", _)) table = |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
16913
diff
changeset
|
458 |
(False, table) |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
16913
diff
changeset
|
459 |
| aux (Const ("Not", _) $ x) table = |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
16913
diff
changeset
|
460 |
apfst Not (aux x table) |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
16913
diff
changeset
|
461 |
| aux (Const ("op |", _) $ x $ y) table = |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
16913
diff
changeset
|
462 |
let |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
16913
diff
changeset
|
463 |
val (fm1, table1) = aux x table |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
16913
diff
changeset
|
464 |
val (fm2, table2) = aux y table1 |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
16913
diff
changeset
|
465 |
in |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
16913
diff
changeset
|
466 |
(Or (fm1, fm2), table2) |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
16913
diff
changeset
|
467 |
end |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
16913
diff
changeset
|
468 |
| aux (Const ("op &", _) $ x $ y) table = |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
16913
diff
changeset
|
469 |
let |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
16913
diff
changeset
|
470 |
val (fm1, table1) = aux x table |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
16913
diff
changeset
|
471 |
val (fm2, table2) = aux y table1 |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
16913
diff
changeset
|
472 |
in |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
16913
diff
changeset
|
473 |
(And (fm1, fm2), table2) |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
16913
diff
changeset
|
474 |
end |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
16913
diff
changeset
|
475 |
| aux x table = |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
16913
diff
changeset
|
476 |
(case Termtab.lookup table x of |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
16913
diff
changeset
|
477 |
SOME i => |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
16913
diff
changeset
|
478 |
(BoolVar i, table) |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
16913
diff
changeset
|
479 |
| NONE => |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
16913
diff
changeset
|
480 |
let |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
16913
diff
changeset
|
481 |
val i = get_next_idx () |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
16913
diff
changeset
|
482 |
in |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
16913
diff
changeset
|
483 |
(BoolVar i, Termtab.update (x, i) table) |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
16913
diff
changeset
|
484 |
end) |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
16913
diff
changeset
|
485 |
in |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
16913
diff
changeset
|
486 |
aux t table |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
16913
diff
changeset
|
487 |
end; |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
16913
diff
changeset
|
488 |
|
14452 | 489 |
end; |