nand.rkt

#lang rosette/safe

(require rosette/lib/angelic rosette/lib/match)

; Circuit building block: NAND gates only
(struct nand (x y) #:transparent)
(define (interpret p)
  (match p
    [(nand x y) (not (and (interpret x) (interpret y)))]
    [_ p]))

; Sketch of basic circuit node
(define (??node x y) (choose* x y (nand x y)))

; Sketch of circuit of given recursive depth and two inputs
(define (??circuit x y depth)
  (if (= depth 0)
      (??node x y)
      (??node (??circuit x y (- depth 1)) (??circuit x y (- depth 1)))))

; Synthesize a circuit of NANDs that matches `f`
(define (find-nands f)
  (define-symbolic a b boolean?)
  (define sketch (??circuit a b 3))
  (define sol (synthesize
               #:forall (list a b)
               #:guarantee (assert (eq? (interpret sketch) (f a b)))))
  (evaluate sketch sol))

; Now find equivalent circuits for basic logic gates
(printf "AND:  ")
(find-nands &&)

(printf "OR:   ")
(find-nands ||)

(printf "NOR:  ")
(define (nor x y) (! (|| x y)))
(find-nands nor)

(printf "NOT A:")
(define (xnot x y) (! x))
(find-nands xnot)

(printf "XOR:  ")
(find-nands xor)

(printf "XNOR: ")
(define (xnor x y) (! (xor x y)))
(find-nands xnor)

output.txt

Welcome to DrRacket, version 7.5 [3m].
Language: rosette/safe, with debugging; memory limit: 256 MB.
AND:  (nand (nand a b) (nand a b))
OR:   (nand (nand a a) (nand (nand a b) b))
NOR:  (nand (nand (nand a (nand a b)) (nand b b)) (nand a (nand a a)))
NOT A:(nand (nand (nand a b) b) a)
XOR:  (nand (nand a (nand a b)) (nand (nand a b) b))
XNOR: (nand (nand (nand (nand a b) b) b) (nand (nand (nand a b) b) (nand a (nand a b))))