;;; Boolean expression =
;;; T | F | (V n) | (NOT x) | (AND x y) | (OR x y) | (IMP x y) | (EQV x y)
;;; where n is a natural number and x, y are boolean expressions.
;;; Ordered Binary Decision Diagram =
;;; #t | #f | (n a b)
;;; where n is a natural number and a, b are ordered binary decision
;;; diagrams containing no number less than or equal to n.
(define (robdd B)
(if (symbol? B)
(eq? B 'T)
(case (car B)
((V) (list (cadr B) #t #f))
((NOT) (opposite (robdd (cadr B))))
((AND) (and-merge (robdd (cadr B)) (robdd (caddr B))))
((OR) (or-merge (robdd (cadr B)) (robdd (caddr B))))
((IMP) (imp-merge (robdd (cadr B)) (robdd (caddr B))))
((EQV) (eqv-merge (robdd (cadr B)) (robdd (caddr B))))
(else (error "bad boolean expression")))))
(define (opposite R)
(if (boolean? R)
(not R)
(list (car R) (opposite (cadr R)) (opposite (caddr R)))))
(define (mk-if N A B)
(if (equal? A B) A (list N A B)))
(define (and-merge X Y)
(cond
((eq? X #f) #f)
((eq? Y #f) #f)
((eq? X #t) Y)
((eq? Y #t) X)
((equal? X Y) X)
((< (car X) (car Y))
(mk-if (car X) (and-merge (cadr X) Y) (and-merge (caddr X) Y)))
((> (car X) (car Y))
(mk-if (car Y) (and-merge X (cadr Y)) (and-merge X (caddr Y))))
(else
(mk-if (car X) (and-merge (cadr X) (cadr Y))
(and-merge (caddr X) (caddr Y))))))
(define (or-merge X Y)
(cond
((eq? X #f) Y)
((eq? Y #f) X)
((eq? X #t) #t)
((eq? Y #t) #t)
((equal? X Y) X)
((< (car X) (car Y))
(mk-if (car X) (or-merge (cadr X) Y) (or-merge (caddr X) Y)))
((> (car X) (car Y))
(mk-if (car Y) (or-merge X (cadr Y)) (or-merge X (caddr Y))))
(else
(mk-if (car X) (or-merge (cadr X) (cadr Y))
(or-merge (caddr X) (caddr Y))))))
(define (imp-merge X Y)
(cond
((eq? X #f) #t)
((eq? Y #f) (opposite X))
((eq? X #t) Y)
((eq? Y #t) #t)
((equal? X Y) #t)
((< (car X) (car Y))
(mk-if (car X) (imp-merge (cadr X) Y) (imp-merge (caddr X) Y)))
((> (car X) (car Y))
(mk-if (car Y) (imp-merge X (cadr Y)) (imp-merge X (caddr Y))))
(else
(mk-if (car X) (imp-merge (cadr X) (cadr Y))
(imp-merge (caddr X) (caddr Y))))))
(define (eqv-merge X Y)
(cond
((eq? X #f) (opposite Y))
((eq? Y #f) (opposite X))
((eq? X #t) Y)
((eq? Y #t) X)
((equal? X Y) #t)
((< (car X) (car Y))
(mk-if (car X) (eqv-merge (cadr X) Y) (eqv-merge (caddr X) Y)))
((> (car X) (car Y))
(mk-if (car Y) (eqv-merge X (cadr Y)) (eqv-merge X (caddr Y))))
(else
(mk-if (car X) (eqv-merge (cadr X) (cadr Y))
(eqv-merge (caddr X) (caddr Y))))))
(define (first-model B)
(let ((R (robdd B)))
(call-with-current-continuation (lambda (K)
(let loop ((R R) (M '()))
(if (pair? R)
(begin (loop (cadr R) (cons (cons (car R) #t) M))
(loop (caddr R) (cons (cons (car R) #f) M)))
(if R (K (reverse M)))))
'none))))
(define (first-counter-model B)
(let ((R (robdd B)))
(call-with-current-continuation (lambda (K)
(let loop ((R R) (M '()))
(if (pair? R)
(begin (loop (cadr R) (cons (cons (car R) #t) M))
(loop (caddr R) (cons (cons (car R) #f) M)))
(if (not R) (K (reverse M)))))
'none))))
(define (mm N) (first-model (test-case N)))
(define (cm N) (first-counter-model (test-case N)))
(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"))))