equal
deleted
inserted
replaced
65 *) |
65 *) |
66 fun iforall n f = all (map f (0 upto n - 1)) |
66 fun iforall n f = all (map f (0 upto n - 1)) |
67 fun iexists n f = PropLogic.exists (map f (0 upto n - 1)) |
67 fun iexists n f = PropLogic.exists (map f (0 upto n - 1)) |
68 fun iforall2 n m f = all (map_product f (0 upto n - 1) (0 upto m - 1)) |
68 fun iforall2 n m f = all (map_product f (0 upto n - 1) (0 upto m - 1)) |
69 |
69 |
70 fun the_one var n x = all (var x :: map (Not o var) ((0 upto n - 1) \\ [x])) |
70 fun the_one var n x = all (var x :: map (Not o var) (remove (op =) x (0 upto n - 1))) |
71 fun exactly_one n f = iexists n (the_one f n) |
71 fun exactly_one n f = iexists n (the_one f n) |
72 |
72 |
73 (* SAT solving *) |
73 (* SAT solving *) |
74 val solver = Unsynchronized.ref "auto"; |
74 val solver = Unsynchronized.ref "auto"; |
75 fun sat_solver x = |
75 fun sat_solver x = |