equal
deleted
inserted
replaced
109 |
109 |
110 fun indices True = [] |
110 fun indices True = [] |
111 | indices False = [] |
111 | indices False = [] |
112 | indices (BoolVar i) = [i] |
112 | indices (BoolVar i) = [i] |
113 | indices (Not fm) = indices fm |
113 | indices (Not fm) = indices fm |
114 | indices (Or (fm1, fm2)) = (indices fm1) union_int (indices fm2) |
114 | indices (Or (fm1, fm2)) = union (op =) (indices fm1, indices fm2) |
115 | indices (And (fm1, fm2)) = (indices fm1) union_int (indices fm2); |
115 | indices (And (fm1, fm2)) = union (op =) (indices fm1, indices fm2); |
116 |
116 |
117 (* ------------------------------------------------------------------------- *) |
117 (* ------------------------------------------------------------------------- *) |
118 (* maxidx: computes the maximal variable index occuring in a formula of *) |
118 (* maxidx: computes the maximal variable index occuring in a formula of *) |
119 (* propositional logic 'fm'; 0 if 'fm' contains no variable *) |
119 (* propositional logic 'fm'; 0 if 'fm' contains no variable *) |
120 (* ------------------------------------------------------------------------- *) |
120 (* ------------------------------------------------------------------------- *) |