(define (pos B)
(if (symbol? B)
(if (eq? B 'T) '(()) '())
(case (car B)
((V) `((( ,(cadr B) . #t ))))
((Not) (neg (cadr B)))
((And) (prune (mk-and (pos (cadr B)) (pos (caddr B)))))
((Or) (prune (mk-or (pos (cadr B)) (pos (caddr B)))))
((Imp) (prune (mk-or (neg (cadr B)) (pos (caddr B)))))
((Eqv) (pos `(Or (And ,(cadr B) ,(caddr B))
(And (Not ,(cadr B)) (Not ,(caddr B))))))
(else (error "bad Boolean expression")))))
(define (neg B)
(if (symbol? B)
(if (eq? B 'T) '() '(()))
(case (car B)
((V) `((( ,(cadr B) . #f))))
((Not) (pos (cadr B)))
((And) (prune (mk-or (neg (cadr B)) (neg (caddr B)))))
((Or) (prune (mk-and (neg (cadr B)) (neg (caddr B)))))
((Imp) (prune (mk-and (pos (cadr B)) (neg (caddr B)))))
((Eqv) (neg `(Or (And ,(cadr B) ,(caddr B))
(And (Not ,(cadr B)) (Not ,(caddr B))))))
(else (error "bad Boolean expression")))))
(define (filter P L)
(if (pair? L)
(let ((R (filter P (cdr L))))
(if (P (car L)) (cons (car L) R) R))
'()))
(define (any P L)
(and (pair? L) (or (P (car L)) (any P (cdr L)))))
(define (prune D)
(filter (lambda (C) (not (any (lambda (C1) (subsumes C1 C)) D))) D))
(define (subsumes A B) ; A, B are clauses, lists of (int.bool) pairs
(if (pair? A)
(and (pair? B)
(cond
((< (caar A) (caar B))
#f)
((> (caar A) (caar B))
(subsumes A (cdr B)))
((eq? (cdar A) (cdar B))
(subsumes (cdr A) (cdr B)))
(else
#f)))
(pair? B)))
(define (mk-or A B)
(if (and (pair? A) (pair? B))
(case (c-compare (car A) (car B))
((<) (cons (car A) (mk-or (cdr A) B)))
((>) (cons (car B) (mk-or A (cdr B))))
(else (cons (car A) (mk-or (cdr A) (cdr B)))))
(if (pair? A) A B)))
(define (c-compare A B)
(if (pair? A)
(if (pair? B)
(cond
((< (caar A) (caar B)) '<)
((> (caar A) (caar B)) '>)
((and (not (cdar A)) (cdar B)) '<)
((and (cdar A) (not (cdar B))) '>)
(else (c-compare (cdr A) (cdr B))))
'>)
(if (pair? B) '< '=)))
(define (do-list L F) (for-each F L))
(define (mk-and D1 D2)
(let ((R '()))
(do-list D1 (lambda (C1)
(do-list D2 (lambda (C2)
(let ((C (c-merge C1 C2)))
(if (not (eq? C 'fail))
(set! R (cons C R))))))))
R))
(define (c-merge A B)
(if (pair? A)
(if (pair? B)
(cond
((< (caar A) (caar B))
(let ((X (c-merge (cdr A) B)))
(if (eq? X 'fail) X (cons (car A) X))))
((> (caar A) (caar B))
(let ((X (c-merge A (cdr B))))
(if (eq? X 'fail) X (cons (car B) X))))
((eq? (cdar A) (cdar B))
(let ((X (c-merge (cdr A) (cdr B))))
(if (eq? X 'fail) X (cons (car B) X))))
(else
'fail))
A)
B))
(define (write-lit X)
(if (not (cdr X)) (write-char #\~))
(display (car X)))
(define (write-con X)
(write-char #\{)
(if (pair? X)
(begin
(write-lit (car X))
(do ((X (cdr X) (cdr X)))
((null? X))
(write-char #\,)
(write-lit (car X)))))
(write-char #\}))
(define (write-dis X)
(write-char #\{)
(if (pair? X)
(begin
(write-con (car X))
(do ((X (cdr X) (cdr X)))
((null? X))
(write-char #\,)
(write-con (car X)))))
(write-char #\}))
(define (t N)
(write-dis (pos (test-case N)))
(newline))
(define (test-case N)
(case N
((1) '(V 1))
((2) '(Or (V 1) (V 1)))
((3) '(Eqv (Imp (V 1) (V 2)) (Or (Not (V 1)) (V 2))))
((4) '(Eqv (And (V 1) (V 1)) (V 1)))
((5) '(And (And (And (Eqv (V 13) (Or (And F (V 1)) (Or (And F (V
5)) (And (V 1) (V 5))))) (Eqv (V 9) (Eqv (Eqv F (Not (V
1))) (Not (V 5))))) (And (And (Eqv (V 14) (Or (And (V 13)
(V 2)) (Or (And (V 13) (V 6)) (And (V 2) (V 6)))))
(Eqv (V 10) (Eqv (Eqv (V 13) (Not (V 2))) (Not (V 6)))))
(And (And (Eqv (V 15) (Or (And (V 14) (V 3)) (Or (And (V
14) (V 7)) (And (V 3) (V 7))))) (Eqv (V 11) (Eqv (Eqv
(V 14) (Not (V 3))) (Not (V 7))))) (And (Eqv (V 16) (Or
(And (V 15) (V 4)) (Or (And (V 15) (V 8)) (And (V 4)
(V 8))))) (Eqv (V 12) (Eqv (Eqv (V 15) (Not (V 4))) (Not
(V 8)))))))) (And (And (And (Eqv (V 17) (Or (And (Not F)
(And (V 1) (V 5))) (And F (Or (V 1) (V 5))))) (Eqv (V
9) (Or (And F (And (V 1) (V 5))) (Or (And F (And (Not (V
1)) (Not (V 5)))) (Or (And (Not F) (And (V 1) (Not (V
5)))) (And (Not F) (And (Not (V 1)) (V 5)))))))) (And (And
(Eqv (V 18) (Or (And (Not (V 17)) (And (V 2) (V 6)))
(And (V 17) (Or (V 2) (V 6))))) (Eqv (V 10) (Or (And
(V 17) (And (V 2) (V 6))) (Or (And (V 17) (And (Not (V
2)) (Not (V 6)))) (Or (And (Not (V 17)) (And (V 2) (Not
(V 6)))) (And (Not (V 17)) (And (Not (V 2)) (V 6))))))))
(And (And (Eqv (V 19) (Or (And (Not (V 18)) (And (V 3)
(V 7))) (And (V 18) (Or (V 3) (V 7))))) (Eqv (V 11)
(Or (And (V 18) (And (V 3) (V 7))) (Or (And (V 18) (And
(Not (V 3)) (Not (V 7)))) (Or (And (Not (V 18)) (And (V
3) (Not (V 7)))) (And (Not (V 18)) (And (Not (V 3)) (V
7)))))))) (And (Eqv (V 20) (Or (And (Not (V 19)) (And (V
4) (V 8))) (And (V 19) (Or (V 4) (V 8))))) (Eqv (V 12)
(Or (And (V 19) (And (V 4) (V 8))) (Or (And (V 19) (And
(Not (V 4)) (Not (V 8)))) (Or (And (Not (V 19)) (And (V
4) (Not (V 8)))) (And (Not (V 19)) (And (Not (V 4)) (V
8))))))))))) (Eqv (V 16) (V 20)))))
((6) '(And (And (And (Eqv (V 13) (Or (And F T) (Or (And F (V 5))
(And T (V 5))))) (Eqv (V 9) (Eqv (Eqv F (Not T)) (Not (V
5))))) (And (And (Eqv (V 14) (Or (And (V 13) F) (Or (And
(V 13) (V 6)) (And F (V 6))))) (Eqv (V 10) (Eqv (Eqv
(V 13) (Not F)) (Not (V 6))))) (And (And (Eqv (V 15) (Or
(And (V 14) F) (Or (And (V 14) (V 7)) (And F (V 7)))))
(Eqv (V 11) (Eqv (Eqv (V 14) (Not F)) (Not (V 7))))) (And
(Eqv (V 16) (Or (And (V 15) T) (Or (And (V 15) (V 8))
(And T (V 8))))) (Eqv (V 12) (Eqv (Eqv (V 15) (Not T))
(Not (V 8)))))))) (And (And (And (Eqv (V 17) (Or (And (Not
F) (And T (V 5))) (And F (Or T (V 5))))) (Eqv (V 9) (Or
(And F (And T (V 5))) (Or (And F (And (Not T) (Not (V 5))))
(Or (And (Not F) (And T (Not (V 5)))) (And (Not F) (And (Not
T) (V 5)))))))) (And (And (Eqv (V 18) (Or (And (Not (V
17)) (And F (V 6))) (And (V 17) (Or F (V 6))))) (Eqv (V
10) (Or (And (V 17) (And F (V 6))) (Or (And (V 17) (And
(Not F) (Not (V 6)))) (Or (And (Not (V 17)) (And F (Not (V
6)))) (And (Not (V 17)) (And (Not F) (V 6)))))))) (And (And
(Eqv (V 19) (Or (And (Not (V 18)) (And F (V 7))) (And (V
18) (Or F (V 7))))) (Eqv (V 11) (Or (And (V 18) (And F
(V 7))) (Or (And (V 18) (And (Not F) (Not (V 7)))) (Or
(And (Not (V 18)) (And F (Not (V 7)))) (And (Not (V 18))
(And (Not F) (V 7)))))))) (And (Eqv (V 20) (Or (And (Not
(V 19)) (And T (V 8))) (And (V 19) (Or T (V 8))))) (Eqv
(V 12) (Or (And (V 19) (And T (V 8))) (Or (And (V 19)
(And (Not T) (Not (V 8)))) (Or (And (Not (V 19)) (And T (Not
(V 8)))) (And (Not (V 19)) (And (Not T) (V 8)))))))))))
(Eqv (V 16) (V 20)))))
((7) '(Eqv (Not (Or (V 1) (Or (V 2) (V 3))))
(And (Not (V 1)) (And (Not (V 2)) (Not (V 3)) ))))
((8) '(Eqv (Not (And (V 1) (And (V 2) (And (V 3) (And (V 4)
(And (V 5) (And (V 6) (And (V 7) (And (V 8) (And (V 9)
(And (V 10) (And (V 11) (And (V 12) (And (V 13) (And
(V 14) (And (V 15) (V 16))))))))))))))))) (Or (Not (V
1)) (Or (Not (V 2)) (Or (Not (V 3)) (Or (Not (V 4)) (Or
(Not (V 5)) (Or (Not (V 6)) (Or (Not (V 7)) (Or (Not (V
8)) (Or (Not (V 9)) (Or (Not (V 10)) (Or (Not (V 11)) (Or
(Not (V 12)) (Or (Not (V 13)) (Or (Not (V 14)) (Or (Not
(V 15)) (Not (V 16)))))))))))))))))))
((9) '(Eqv (Not (Or (V 1) (Or (V 2) (Or (V 3) (Or (V 4) (Or
(V 5) (Or (V 6) (Or (V 7) (Or (V 8) (Or (V 9) (Or (V
10) (Or (V 11) (Or (V 12) (Or (V 13) (Or (V 14) (Or (V
15) (V 16))))))))))))))))) (And (Not (V 1)) (And (Not (V
2)) (And (Not (V 3)) (And (Not (V 4)) (And (Not (V 5))
(And (Not (V 6)) (And (Not (V 7)) (And (Not (V 8)) (And
(Not (V 9)) (And (Not (V 10)) (And (Not (V 11)) (And (Not
(V 12)) (And (Not (V 13)) (And (Not (V 14)) (And (Not (V
15)) (Not (V 16)))))))))))))))))))
;; Test cases 10 to 21 were provided by Jonathan Pengelly
((10) '(And (V 1) (Not (V 1))))
((11) '(Or (And (V 1) (Not (V 2))) (And (Not (V 1)) (V 2))))
((12) '(And (And (V 1) (Imp (V 1) (V 2))) (Not (V 2))))
((13) '(And (And (Not (V 2)) (Imp (V 1) (V 2))) (V 1)))
((14) '(Eqv (V 1) (Not (Not (V 1)))))
((15) '(Eqv (And (And (V 1) (V 2)) (V 3))
(And (V 1) (And (V 2) (V 3)))))
((16) '(Eqv (Not (Or (V 1) (V 2))) (And (Not (V 1)) (Not (V 2)))))
((17) '(Imp (Imp (V 1) (V 3)) (Imp (Imp (V 2) (V 4))
(Imp (Or (V 1) (V 2)) (V 3)))))
((18) '(And (And (And (Or (Or (V 1) (V 2)) (Not (V 3)))
(Or (Or (V 1) (V 2)) (V 3))) (Or (V 1) (Not (V 2))))
(Not (V 1))))
((19) '(Imp (V 1) (Imp (V 2) (V 1))))
((20) 'T)
((21) 'F)
(else (error "no such test case"))))