author | webertj |
Thu, 31 Aug 2006 02:59:08 +0200 | |
changeset 20442 | 04621ea9440e |
parent 17809 | 195045659c06 |
child 22441 | 7da872d34ace |
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 |
|
20442 | 38 |
(* propositional representation of HOL terms *) |
17809
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
16913
diff
changeset
|
39 |
val prop_formula_of_term : Term.term -> int Termtab.table -> prop_formula * int Termtab.table |
20442 | 40 |
(* HOL term representation of propositional formulae *) |
41 |
val term_of_prop_formula : prop_formula -> Term.term |
|
14452 | 42 |
end; |
43 |
||
44 |
structure PropLogic : PROP_LOGIC = |
|
45 |
struct |
|
46 |
||
47 |
(* ------------------------------------------------------------------------- *) |
|
14753 | 48 |
(* prop_formula: formulas of propositional logic, built from Boolean *) |
14452 | 49 |
(* variables (referred to by index) and True/False using *) |
50 |
(* not/or/and *) |
|
51 |
(* ------------------------------------------------------------------------- *) |
|
52 |
||
53 |
datatype prop_formula = |
|
54 |
True |
|
55 |
| False |
|
56 |
| BoolVar of int (* NOTE: only use indices >= 1 *) |
|
57 |
| Not of prop_formula |
|
58 |
| Or of prop_formula * prop_formula |
|
59 |
| And of prop_formula * prop_formula; |
|
60 |
||
61 |
(* ------------------------------------------------------------------------- *) |
|
62 |
(* The following constructor functions make sure that True and False do not *) |
|
63 |
(* occur within any of the other connectives (i.e. Not, Or, And), and *) |
|
64 |
(* perform double-negation elimination. *) |
|
65 |
(* ------------------------------------------------------------------------- *) |
|
66 |
||
67 |
(* prop_formula -> prop_formula *) |
|
68 |
||
69 |
fun SNot True = False |
|
70 |
| SNot False = True |
|
71 |
| SNot (Not fm) = fm |
|
72 |
| SNot fm = Not fm; |
|
73 |
||
74 |
(* prop_formula * prop_formula -> prop_formula *) |
|
75 |
||
76 |
fun SOr (True, _) = True |
|
77 |
| SOr (_, True) = True |
|
78 |
| SOr (False, fm) = fm |
|
79 |
| SOr (fm, False) = fm |
|
80 |
| SOr (fm1, fm2) = Or (fm1, fm2); |
|
81 |
||
82 |
(* prop_formula * prop_formula -> prop_formula *) |
|
83 |
||
84 |
fun SAnd (True, fm) = fm |
|
85 |
| SAnd (fm, True) = fm |
|
86 |
| SAnd (False, _) = False |
|
87 |
| SAnd (_, False) = False |
|
88 |
| SAnd (fm1, fm2) = And (fm1, fm2); |
|
89 |
||
90 |
(* ------------------------------------------------------------------------- *) |
|
16909
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
91 |
(* 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
|
92 |
(* negation *) |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
93 |
(* ------------------------------------------------------------------------- *) |
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 |
(* prop_formula -> prop_formula *) |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
96 |
|
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
97 |
fun simplify (Not fm) = SNot (simplify fm) |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
98 |
| 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
|
99 |
| 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
|
100 |
| simplify fm = fm; |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
101 |
|
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
102 |
(* ------------------------------------------------------------------------- *) |
14753 | 103 |
(* indices: collects all indices of Boolean variables that occur in a *) |
14452 | 104 |
(* propositional formula 'fm'; no duplicates *) |
105 |
(* ------------------------------------------------------------------------- *) |
|
106 |
||
107 |
(* prop_formula -> int list *) |
|
108 |
||
16909
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
109 |
fun indices True = [] |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
110 |
| indices False = [] |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
111 |
| indices (BoolVar i) = [i] |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
112 |
| indices (Not fm) = indices fm |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
113 |
| 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
|
114 |
| indices (And (fm1, fm2)) = (indices fm1) union_int (indices fm2); |
14452 | 115 |
|
116 |
(* ------------------------------------------------------------------------- *) |
|
117 |
(* maxidx: computes the maximal variable index occuring in a formula of *) |
|
118 |
(* propositional logic 'fm'; 0 if 'fm' contains no variable *) |
|
119 |
(* ------------------------------------------------------------------------- *) |
|
120 |
||
121 |
(* prop_formula -> int *) |
|
122 |
||
16909
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
123 |
fun maxidx True = 0 |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
124 |
| maxidx False = 0 |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
125 |
| maxidx (BoolVar i) = i |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
126 |
| maxidx (Not fm) = maxidx fm |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
127 |
| 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
|
128 |
| 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
|
129 |
|
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
130 |
(* ------------------------------------------------------------------------- *) |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
131 |
(* 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
|
132 |
(* formulas *) |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
133 |
(* ------------------------------------------------------------------------- *) |
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 |
(* prop_formula list -> prop_formula *) |
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 |
fun exists xs = Library.foldl SOr (False, xs); |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
138 |
|
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 |
(* 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
|
141 |
(* ------------------------------------------------------------------------- *) |
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 |
(* prop_formula list -> prop_formula *) |
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 |
fun all xs = Library.foldl SAnd (True, xs); |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
146 |
|
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 |
(* 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
|
149 |
(* ------------------------------------------------------------------------- *) |
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 |
(* prop_formula list * prop_formula list -> prop_formula *) |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
152 |
|
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
153 |
fun dot_product (xs,ys) = exists (map SAnd (xs~~ys)); |
14452 | 154 |
|
155 |
(* ------------------------------------------------------------------------- *) |
|
156 |
(* 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
|
157 |
(* 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
|
158 |
(* Simplification (c.f. 'simplify') is performed as well. *) |
14452 | 159 |
(* ------------------------------------------------------------------------- *) |
160 |
||
161 |
(* prop_formula -> prop_formula *) |
|
162 |
||
163 |
fun |
|
164 |
(* constants *) |
|
16909
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
165 |
nnf True = True |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
166 |
| nnf False = False |
14452 | 167 |
(* variables *) |
16909
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
168 |
| nnf (BoolVar i) = (BoolVar i) |
14452 | 169 |
(* '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
|
170 |
| 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
|
171 |
| nnf (And (fm1, fm2)) = SAnd (nnf fm1, nnf fm2) |
14452 | 172 |
(* 'not' + constant *) |
16909
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
173 |
| nnf (Not True) = False |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
174 |
| nnf (Not False) = True |
14452 | 175 |
(* 'not' + variable *) |
16909
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
176 |
| nnf (Not (BoolVar i)) = Not (BoolVar i) |
14452 | 177 |
(* 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
|
178 |
| 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
|
179 |
| nnf (Not (And (fm1, fm2))) = SOr (nnf (SNot fm1), nnf (SNot fm2)) |
14452 | 180 |
(* double-negation elimination *) |
16909
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
181 |
| nnf (Not (Not fm)) = nnf fm; |
14452 | 182 |
|
183 |
(* ------------------------------------------------------------------------- *) |
|
14681 | 184 |
(* cnf: computes the conjunctive normal form (i.e. a conjunction of *) |
185 |
(* disjunctions) of a formula 'fm' of propositional logic. The result *) |
|
186 |
(* formula may be exponentially longer than 'fm'. *) |
|
14452 | 187 |
(* ------------------------------------------------------------------------- *) |
188 |
||
189 |
(* prop_formula -> prop_formula *) |
|
190 |
||
191 |
fun cnf fm = |
|
192 |
let |
|
193 |
fun |
|
194 |
(* constants *) |
|
14939 | 195 |
cnf_from_nnf True = True |
196 |
| cnf_from_nnf False = False |
|
14452 | 197 |
(* literals *) |
14939 | 198 |
| cnf_from_nnf (BoolVar i) = BoolVar i |
199 |
| cnf_from_nnf (Not fm1) = Not fm1 (* 'fm1' must be a variable since the formula is in NNF *) |
|
14452 | 200 |
(* pushing 'or' inside of 'and' using distributive laws *) |
14939 | 201 |
| cnf_from_nnf (Or (fm1, fm2)) = |
14452 | 202 |
let |
14939 | 203 |
fun cnf_or (And (fm11, fm12), fm2) = |
204 |
And (cnf_or (fm11, fm2), cnf_or (fm12, fm2)) |
|
205 |
| cnf_or (fm1, And (fm21, fm22)) = |
|
206 |
And (cnf_or (fm1, fm21), cnf_or (fm1, fm22)) |
|
207 |
(* neither subformula contains 'and' *) |
|
208 |
| cnf_or (fm1, fm2) = |
|
209 |
Or (fm1, fm2) |
|
14452 | 210 |
in |
14939 | 211 |
cnf_or (cnf_from_nnf fm1, cnf_from_nnf fm2) |
14452 | 212 |
end |
213 |
(* 'and' as outermost connective is left untouched *) |
|
14939 | 214 |
| cnf_from_nnf (And (fm1, fm2)) = And (cnf_from_nnf fm1, cnf_from_nnf fm2) |
14452 | 215 |
in |
216 |
(cnf_from_nnf o nnf) fm |
|
217 |
end; |
|
218 |
||
219 |
(* ------------------------------------------------------------------------- *) |
|
16909
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
220 |
(* auxcnf: computes the definitional conjunctive normal form of a formula *) |
14681 | 221 |
(* 'fm' of propositional logic, introducing auxiliary variables if *) |
222 |
(* necessary to avoid an exponential blowup of the formula. The result *) |
|
223 |
(* formula is satisfiable if and only if 'fm' is satisfiable. *) |
|
16907 | 224 |
(* 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
|
225 |
(* 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
|
226 |
(* 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
|
227 |
(* aux)". *) |
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 |
|
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
230 |
(* ------------------------------------------------------------------------- *) |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
231 |
(* Note: 'auxcnf' tends to use fewer variables and fewer clauses than *) |
16913 | 232 |
(* '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
|
233 |
(* 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
|
234 |
(* 'defcnf' does). It is currently not quite clear to me if one of the *) |
16913 | 235 |
(* algorithms is clearly superior to the other, but I suggest using *) |
236 |
(* 'defcnf' instead. *) |
|
14452 | 237 |
(* ------------------------------------------------------------------------- *) |
238 |
||
239 |
(* prop_formula -> prop_formula *) |
|
240 |
||
16909
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
241 |
fun auxcnf fm = |
14452 | 242 |
let |
16907 | 243 |
(* convert formula to NNF first *) |
244 |
val fm' = nnf fm |
|
14452 | 245 |
(* 'new' specifies the next index that is available to introduce an auxiliary variable *) |
16907 | 246 |
(* int ref *) |
247 |
val new = ref (maxidx fm' + 1) |
|
248 |
(* unit -> int *) |
|
249 |
fun new_idx () = let val idx = !new in new := idx+1; idx end |
|
250 |
(* prop_formula -> prop_formula *) |
|
14452 | 251 |
fun |
252 |
(* constants *) |
|
16909
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
253 |
auxcnf_from_nnf True = True |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
254 |
| auxcnf_from_nnf False = False |
14452 | 255 |
(* literals *) |
16909
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
256 |
| auxcnf_from_nnf (BoolVar i) = BoolVar i |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
257 |
| auxcnf_from_nnf (Not fm1) = Not fm1 (* 'fm1' must be a variable since the formula is in NNF *) |
14939 | 258 |
(* 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
|
259 |
| auxcnf_from_nnf (Or (fm1, fm2)) = |
14452 | 260 |
let |
16909
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
261 |
val fm1' = auxcnf_from_nnf fm1 |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
262 |
val fm2' = auxcnf_from_nnf fm2 |
16907 | 263 |
(* prop_formula * prop_formula -> prop_formula *) |
16909
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
264 |
fun auxcnf_or (And (fm11, fm12), fm2) = |
14964 | 265 |
(case fm2 of |
266 |
(* do not introduce an auxiliary variable for literals *) |
|
267 |
BoolVar _ => |
|
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 |
| Not _ => |
16909
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
270 |
And (auxcnf_or (fm11, fm2), auxcnf_or (fm12, fm2)) |
14964 | 271 |
| _ => |
272 |
let |
|
16907 | 273 |
val aux = BoolVar (new_idx ()) |
14964 | 274 |
in |
16909
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
275 |
And (And (auxcnf_or (fm11, aux), auxcnf_or (fm12, aux)), auxcnf_or (fm2, Not aux)) |
14964 | 276 |
end) |
16909
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
277 |
| auxcnf_or (fm1, And (fm21, fm22)) = |
14964 | 278 |
(case fm1 of |
279 |
(* do not introduce an auxiliary variable for literals *) |
|
280 |
BoolVar _ => |
|
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 |
| Not _ => |
16909
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
283 |
And (auxcnf_or (fm1, fm21), auxcnf_or (fm1, fm22)) |
14964 | 284 |
| _ => |
285 |
let |
|
16907 | 286 |
val aux = BoolVar (new_idx ()) |
14964 | 287 |
in |
16909
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
288 |
And (auxcnf_or (fm1, Not aux), And (auxcnf_or (fm21, aux), auxcnf_or (fm22, aux))) |
14964 | 289 |
end) |
14939 | 290 |
(* neither subformula contains 'and' *) |
16909
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
291 |
| auxcnf_or (fm1, fm2) = |
16907 | 292 |
Or (fm1, fm2) |
14939 | 293 |
in |
16909
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
294 |
auxcnf_or (fm1', fm2') |
14452 | 295 |
end |
296 |
(* 'and' as outermost connective is left untouched *) |
|
16909
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
297 |
| auxcnf_from_nnf (And (fm1, fm2)) = |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
298 |
And (auxcnf_from_nnf fm1, auxcnf_from_nnf fm2) |
14452 | 299 |
in |
16909
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
300 |
auxcnf_from_nnf fm' |
14452 | 301 |
end; |
302 |
||
303 |
(* ------------------------------------------------------------------------- *) |
|
16909
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
304 |
(* 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
|
305 |
(* 'fm' of propositional logic, introducing auxiliary variables to *) |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
306 |
(* 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
|
307 |
(* 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
|
308 |
(* 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
|
309 |
(* on the following equisatisfiabilities (+/- indicates polarity): *) |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
310 |
(* LITERAL+ == LITERAL *) |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
311 |
(* LITERAL- == NOT LITERAL *) |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
312 |
(* (NOT fm1)+ == aux AND (NOT aux OR fm1-) *) |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
313 |
(* (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
|
314 |
(* (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
|
315 |
(* (NOT fm1)- == aux AND (NOT aux OR fm1+) *) |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
316 |
(* (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
|
317 |
(* (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
|
318 |
(* Example: *) |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
319 |
(* 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
|
320 |
(* AND (NOT aux2 OR NOT a OR NOT b) *) |
14452 | 321 |
(* ------------------------------------------------------------------------- *) |
322 |
||
16909
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
323 |
(* prop_formula -> prop_formula *) |
14452 | 324 |
|
16909
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
325 |
fun defcnf fm = |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
326 |
let |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
327 |
(* simplify formula first *) |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
328 |
val fm' = simplify fm |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
329 |
(* '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
|
330 |
(* int ref *) |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
331 |
val new = ref (maxidx fm' + 1) |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
332 |
(* unit -> int *) |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
333 |
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
|
334 |
(* optimization for n-ary disjunction/conjunction *) |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
335 |
(* prop_formula -> prop_formula list *) |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
336 |
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
|
337 |
| disjuncts fm1 = [fm1] |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
338 |
(* prop_formula -> prop_formula list *) |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
339 |
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
|
340 |
| conjuncts fm1 = [fm1] |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
341 |
(* polarity -> formula -> (defining clauses, literal) *) |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
342 |
(* bool -> prop_formula -> prop_formula * prop_formula *) |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
343 |
fun |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
344 |
(* constants *) |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
345 |
defcnf' true True = (True, True) |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
346 |
| 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
|
347 |
| defcnf' true False = (True, False) |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
348 |
| 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
|
349 |
(* literals *) |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
350 |
| defcnf' true (BoolVar i) = (True, BoolVar i) |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
351 |
| defcnf' false (BoolVar i) = (True, Not (BoolVar i)) |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
352 |
| 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
|
353 |
| defcnf' false (Not (BoolVar i)) = (True, BoolVar i) |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
354 |
(* 'not' *) |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
355 |
| defcnf' polarity (Not fm1) = |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
356 |
let |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
357 |
val (def1, aux1) = defcnf' (not polarity) fm1 |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
358 |
val aux = BoolVar (new_idx ()) |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
359 |
val def = Or (Not aux, aux1) |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
360 |
in |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
361 |
(SAnd (def1, def), aux) |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
362 |
end |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
363 |
(* 'or' *) |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
364 |
| defcnf' polarity (Or (fm1, fm2)) = |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
365 |
let |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
366 |
val fms = disjuncts (Or (fm1, fm2)) |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
367 |
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
|
368 |
val aux = BoolVar (new_idx ()) |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
369 |
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
|
370 |
in |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
371 |
(SAnd (all defs, def), aux) |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
372 |
end |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
373 |
(* 'and' *) |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
374 |
| defcnf' polarity (And (fm1, fm2)) = |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
375 |
let |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
376 |
val fms = conjuncts (And (fm1, fm2)) |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
377 |
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
|
378 |
val aux = BoolVar (new_idx ()) |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
379 |
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
|
380 |
in |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
381 |
(SAnd (all defs, def), aux) |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
382 |
end |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
383 |
(* 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
|
384 |
(* prop_formula -> prop_formula * prop_formula *) |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
385 |
fun defcnf_or (Or (fm1, fm2)) = |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
386 |
let |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
387 |
val (def1, aux1) = defcnf_or fm1 |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
388 |
val (def2, aux2) = defcnf_or fm2 |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
389 |
in |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
390 |
(SAnd (def1, def2), Or (aux1, aux2)) |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
391 |
end |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
392 |
| defcnf_or fm = |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
393 |
defcnf' true fm |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
394 |
(* prop_formula -> prop_formula * prop_formula *) |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
395 |
fun defcnf_and (And (fm1, fm2)) = |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
396 |
let |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
397 |
val (def1, aux1) = defcnf_and fm1 |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
398 |
val (def2, aux2) = defcnf_and fm2 |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
399 |
in |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
400 |
(SAnd (def1, def2), And (aux1, aux2)) |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
401 |
end |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
402 |
| defcnf_and (Or (fm1, fm2)) = |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
403 |
let |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
404 |
val (def1, aux1) = defcnf_or fm1 |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
405 |
val (def2, aux2) = defcnf_or fm2 |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
406 |
in |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
407 |
(SAnd (def1, def2), Or (aux1, aux2)) |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
408 |
end |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
409 |
| defcnf_and fm = |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
410 |
defcnf' true fm |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
411 |
in |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
412 |
SAnd (defcnf_and fm') |
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset
|
413 |
end; |
14452 | 414 |
|
415 |
(* ------------------------------------------------------------------------- *) |
|
14753 | 416 |
(* eval: given an assignment 'a' of Boolean values to variable indices, the *) |
14452 | 417 |
(* truth value of a propositional formula 'fm' is computed *) |
418 |
(* ------------------------------------------------------------------------- *) |
|
419 |
||
420 |
(* (int -> bool) -> prop_formula -> bool *) |
|
421 |
||
422 |
fun eval a True = true |
|
423 |
| eval a False = false |
|
424 |
| eval a (BoolVar i) = (a i) |
|
425 |
| eval a (Not fm) = not (eval a fm) |
|
426 |
| eval a (Or (fm1,fm2)) = (eval a fm1) orelse (eval a fm2) |
|
427 |
| eval a (And (fm1,fm2)) = (eval a fm1) andalso (eval a fm2); |
|
428 |
||
17809
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
16913
diff
changeset
|
429 |
(* ------------------------------------------------------------------------- *) |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
16913
diff
changeset
|
430 |
(* 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
|
431 |
(* with subterms replaced by Boolean variables. Also returns a table *) |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
16913
diff
changeset
|
432 |
(* of terms and corresponding variables that extends the table that was *) |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
16913
diff
changeset
|
433 |
(* given as an argument. Usually, you'll just want to use *) |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
16913
diff
changeset
|
434 |
(* 'Termtab.empty' as value for 'table'. *) |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
16913
diff
changeset
|
435 |
(* ------------------------------------------------------------------------- *) |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
16913
diff
changeset
|
436 |
|
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
16913
diff
changeset
|
437 |
(* 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
|
438 |
(* is computed only when it is actually needed. However, when *) |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
16913
diff
changeset
|
439 |
(* '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
|
440 |
(* efficient to pass and return this value as an additional parameter, *) |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
16913
diff
changeset
|
441 |
(* 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
|
442 |
(* table) for each invocation. *) |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
16913
diff
changeset
|
443 |
|
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
16913
diff
changeset
|
444 |
(* Term.term -> int Termtab.table -> prop_formula * int Termtab.table *) |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
16913
diff
changeset
|
445 |
fun prop_formula_of_term t table = |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
16913
diff
changeset
|
446 |
let |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
16913
diff
changeset
|
447 |
val next_idx_is_valid = ref false |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
16913
diff
changeset
|
448 |
val next_idx = ref 0 |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
16913
diff
changeset
|
449 |
fun get_next_idx () = |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
16913
diff
changeset
|
450 |
if !next_idx_is_valid then |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
16913
diff
changeset
|
451 |
inc next_idx |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
16913
diff
changeset
|
452 |
else ( |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
16913
diff
changeset
|
453 |
next_idx := Termtab.fold (curry Int.max o snd) table 0; |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
16913
diff
changeset
|
454 |
next_idx_is_valid := true; |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
16913
diff
changeset
|
455 |
inc next_idx |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
16913
diff
changeset
|
456 |
) |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
16913
diff
changeset
|
457 |
fun aux (Const ("True", _)) table = |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
16913
diff
changeset
|
458 |
(True, table) |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
16913
diff
changeset
|
459 |
| aux (Const ("False", _)) table = |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
16913
diff
changeset
|
460 |
(False, table) |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
16913
diff
changeset
|
461 |
| aux (Const ("Not", _) $ x) table = |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
16913
diff
changeset
|
462 |
apfst Not (aux x table) |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
16913
diff
changeset
|
463 |
| aux (Const ("op |", _) $ x $ y) table = |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
16913
diff
changeset
|
464 |
let |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
16913
diff
changeset
|
465 |
val (fm1, table1) = aux x table |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
16913
diff
changeset
|
466 |
val (fm2, table2) = aux y table1 |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
16913
diff
changeset
|
467 |
in |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
16913
diff
changeset
|
468 |
(Or (fm1, fm2), table2) |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
16913
diff
changeset
|
469 |
end |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
16913
diff
changeset
|
470 |
| aux (Const ("op &", _) $ x $ y) table = |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
16913
diff
changeset
|
471 |
let |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
16913
diff
changeset
|
472 |
val (fm1, table1) = aux x table |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
16913
diff
changeset
|
473 |
val (fm2, table2) = aux y table1 |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
16913
diff
changeset
|
474 |
in |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
16913
diff
changeset
|
475 |
(And (fm1, fm2), table2) |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
16913
diff
changeset
|
476 |
end |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
16913
diff
changeset
|
477 |
| aux x table = |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
16913
diff
changeset
|
478 |
(case Termtab.lookup table x of |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
16913
diff
changeset
|
479 |
SOME i => |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
16913
diff
changeset
|
480 |
(BoolVar i, table) |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
16913
diff
changeset
|
481 |
| NONE => |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
16913
diff
changeset
|
482 |
let |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
16913
diff
changeset
|
483 |
val i = get_next_idx () |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
16913
diff
changeset
|
484 |
in |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
16913
diff
changeset
|
485 |
(BoolVar i, Termtab.update (x, i) table) |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
16913
diff
changeset
|
486 |
end) |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
16913
diff
changeset
|
487 |
in |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
16913
diff
changeset
|
488 |
aux t table |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
16913
diff
changeset
|
489 |
end; |
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
16913
diff
changeset
|
490 |
|
20442 | 491 |
(* ------------------------------------------------------------------------- *) |
492 |
(* term_of_prop_formula: returns a HOL term that corresponds to a *) |
|
493 |
(* propositional formula, with Boolean variables replaced by Free's *) |
|
494 |
(* ------------------------------------------------------------------------- *) |
|
495 |
||
496 |
(* Note: A more generic implementation should take another argument of type *) |
|
497 |
(* Term.term Inttab.table (or so) that specifies HOL terms for some *) |
|
498 |
(* Boolean variables in the formula, similar to 'prop_formula_of_term' *) |
|
499 |
(* (but the other way round). *) |
|
500 |
||
501 |
(* prop_formula -> Term.term *) |
|
502 |
fun term_of_prop_formula True = |
|
503 |
HOLogic.true_const |
|
504 |
| term_of_prop_formula False = |
|
505 |
HOLogic.false_const |
|
506 |
| term_of_prop_formula (BoolVar i) = |
|
507 |
Free ("v" ^ Int.toString i, HOLogic.boolT) |
|
508 |
| term_of_prop_formula (Not fm) = |
|
509 |
HOLogic.mk_not (term_of_prop_formula fm) |
|
510 |
| term_of_prop_formula (Or (fm1, fm2)) = |
|
511 |
HOLogic.mk_disj (term_of_prop_formula fm1, term_of_prop_formula fm2) |
|
512 |
| term_of_prop_formula (And (fm1, fm2)) = |
|
513 |
HOLogic.mk_conj (term_of_prop_formula fm1, term_of_prop_formula fm2); |
|
514 |
||
14452 | 515 |
end; |