set partition

[yuanle]

This question is useful.

My code for this problem in acl2:
; all-partitions.acl2
; () --> ()
; (1) --> ((1))
; (1 2) --> insert 1 to all-partitions of (2)
; to 0th pos: ((1)(2))
; to 1st pos: ((1 2))
; (1 2 3) --> insert 1 to all-partitions of (2 3)
; all-partions of (2 3) are: ((2)(3)) ((2 3))
; insert 1 to ((2)(3)):
; to 0th pos: ((1)(2)(3))
; to 1th pos: ((1 2)(3))
; to 2nd pos: ((2)(1 3))
; insert 1 to ((2 3)):
; to 0th pos: ((1)(2 3))
; to 1th pos: ((1 2 3))
; in total: ((1)(2)(3))
; ((1 2)(3))
; ((2)(1 3))
; ((1)(2 3))
; ((1 2 3))

(defun insert-to-list (e l)
"insert e to every element of l"
(if (endp l)
nil
(cons (cons e (car l))
(insert-to-list e (cdr l)))))

;;test case
;(insert-to-list 1 '((1) (2) (3) (4)))
;(insert-to-list '(1) '(((1) (2)) ((3) (4))))

(defun partition-insert-one-list-every-pos (e l)
"insert e to every possible pos of l"
(if (endp l)
nil
(append (list (cons (cons e (car l))
(cdr l)))
(insert-to-list (car l)
(partition-insert-one-list-every-pos e (cdr l))))))

;;test case
;(partition-insert-one-list-every-pos 1 '((4)))
;'((1 4)) insert-to-list (4) nil -> nil
;(partition-insert-one-list-every-pos 1 '((2)(3)(4)))
;'(((1 2)(3)(4)) ((2) (1 3)(4)) ((2)(3)(1 4)))

(defun partition-insert-one-list (e l)
"add (list e) to l or insert e to every possible pos of l"
(cons (cons (list e) l)
(partition-insert-one-list-every-pos e l)))

;;test case
;(partition-insert-one-list 1 '((2)(3)(4)))
;'(((1)(2)(3)(4)) ((1 2)(3)(4)) ((2) (1 3)(4)) ((2)(3)(1 4)))
;(partition-insert-one-list 1 '(2))
;nil

(defun partition-insert (e l)
"insert e to every possible pos of every element of l"
(if (endp l)
nil
(append (partition-insert-one-list e (car l))
(partition-insert e (cdr l)))))

;;test case
;(partition-insert 1 '(((2)(3)) ((2 3))))
;'(((1)(2)(3)) ((1 2)(3)) ((2)(1 3)) ((1)(2 3)) ((1 2 3)))
;(partition-insert 1 '(((2))))
;'(((1) (2)) ((1 2)))

(defun get-all-partitions (l)
"return all partitions of set l"
(if (endp l)
nil
(let ((e (car l))
(rest (cdr l)))
(if (endp rest)
(list (list (list e)))
(partition-insert e (get-all-partitions rest))))))

;test case
;(get-all-partitions '(1 2 3))
;'(((1)(2)(3))
; ((1 2)(3))
; ((2)(1 3))
; ((1)(2 3))
; ((1 2 3)))
;(get-all-partitions '(1))
;'(((1)))
;(get-all-partitions '(1 2))
;'(((1)(2)) ((1 2)))

Is there a unit test framework for acl2?

[David Rager]

> Is there a unit test framework for acl2?

The closest thing I can think of is the book system, combined with the
use of assert$.

Example usage of assert$:

(assert$ t "of course t is non-nil!")

Book example:

http://www.cs.utexas.edu/users/moore/acl2/v3-5/BOOK-EXAMPLE.html

Index into general book documentation:

http://www.cs.utexas.edu/users/moore/acl2/v3-5/BOOKS.html

[jay ordway]

ACL2 FOREVER!