Exercise solutions for the Tutorial on Solver-Aided Programming

boyer-moore.rkt

#lang rosette

; https://en.wikipedia.org/wiki/Boyer–Moore_majority_vote_algorithm

; Boyer-Moore majority voting algorithm.
(define (boyer-moore xs)
  (define m (car xs))
  (define i 0)
  (for ([x xs])
    (cond [(= i 0)
           (set! m x)
           (set! i 1)]
          [(= m x)
           (set! i (+ i 1))]
          [else
           (set! i (- i 1))]))
  m)

; Check the algorithm for a list of n arbitrary integers.
(define (check n [bw #f])
  (current-bitwidth bw)
  (define-symbolic* xs integer? [n])
  (define-symbolic* m integer?)
  (verify
   #:assume ; there is a majority value ...
   (assert (> (count (curry = m) xs)
              (quotient n 2)))
   #:guarantee ; algorithm works
   (assert (= m (boyer-moore xs)))))

(time (check 10)) 


; Check the algorithm for a list of n arbitrary integers.
(define (check2 n [bw #f])
  (current-bitwidth bw)
  (define-symbolic* xs integer? [n])
  (define-symbolic* m integer?)
  (verify
   (when ; there is a majority value ...
       (> (count (curry = m) xs)
          (quotient n 2))
     (assert (= m (boyer-moore xs)))))) ; algorithm works

(time (check2 10)) 

                        
           

deep.rkt

#lang rosette

(require rosette/lib/match
         (prefix-in s (only-in "shallow.rkt" Not And Or Iff Xor)))

(current-bitwidth #f)

(struct Not (a)   #:transparent)
(struct And (a b) #:transparent)
(struct Or  (a b) #:transparent)
(struct Iff (a b) #:transparent)
(struct Xor (a b) #:transparent)

(define (interpret prog in)
  (define reg (make-vector (+ (car prog) (length (cdr prog))) #f))
  (define (store i v) (vector-set! reg i v))
  (define (load i) (vector-ref reg i))
  (define (last) (sub1 (vector-length reg)))
  (for ([(i idx) (in-indexed in)])
    (store idx i))
  (for ([(inst idx) (in-indexed (cdr prog))])
    (store
     (+ idx (car prog)) 
     (match inst
       [(Not a)   (sNot (load a))]
       [(And a b) (sAnd (load a) (load b))]
       [(Or a b)  (sOr (load a) (load b))]
       [(Xor a b) (sXor (load a) (load b))]
       [(Iff a b) (sIff (load a) (load b))])))
  (load (last)))

  
(define (ver impl spec)
  (define-symbolic* in boolean? [(car impl)])
  (define sol
    (verify (assert (equal? (interpret impl in) (interpret spec in)))))
  (and (sat? sol) (evaluate in sol)))

(define (syn impl spec)
  (define-symbolic* in boolean? [(car impl)])
  (define sol
    (synthesize
     #:forall in
     #:guarantee (assert (equal? (interpret impl in) (interpret spec in)))))
  (and (sat? sol) (evaluate impl sol)))

(define (superopt spec [k 1])
  (and (< k (length (cdr spec)))
       (or (syn (sketch (car spec) k) spec)
           (superopt spec (+ k 1)))))

  
(require rosette/lib/angelic)

(define sketch
  (case-lambda
    [(n k) (sketch n k Not And Or Xor Iff)]
    [(n k . insts)
     (cons
      n
      (for/list ([i k])
        (define inst (apply choose* insts))
        (define left (apply choose* (build-list (+ i n) values)))
        (define right (apply choose* (build-list (+ i n) values)))
        (match inst
          [(== Not) (Not left)]
          [op (if (<= left right) (op left right) (op right left))])))]))
  

(define NXp
  (list 4 (Xor 0 1) (Not 4) (Xor 2 3) (Not 6) (Xor 5 7)))

(define Niffp
  (list 4 (Iff 0 1) (Iff 2 3) (Iff 4 5) (Not 6)))

; sample interactions
(ver Niffp NXp)
(superopt NXp)

shallow.rkt

#lang rosette

(require rosette/lib/synthax)
(provide Not And Or Xor Iff ver syn ??inst)

(current-bitwidth #f)

(define (Not a)   (if a #f #t))
(define (And a b) (if a b #f))
(define (Or a b)  (if a #t b))
(define (Iff a b) (if a b (! b)))
(define (Xor a b) (if a (! b) b))

(define (ver impl spec)
  (define-symbolic* in boolean? [(procedure-arity impl)])
  (define sol
    (verify (assert (equal? (apply impl in) (apply spec in)))))
  (and (sat? sol) (evaluate in sol)))

(define (syn impl spec)
  (define-symbolic* in boolean? [(procedure-arity impl)])
  (define sol
    (synthesize
     #:forall in
     #:guarantee (assert (equal? (apply impl in) (apply spec in)))))
  (and (sat? sol) (generate-forms sol)))

(define-synthax ??inst
  ([[_ arg ...]
    (choose (Not (choose arg ...))
            ((choose And Or Iff Xor)
             (choose arg ...) (choose arg ...)))]))

(define (specp a b c d)
  (odd? (+ (if a 1 0) (if b 1 0) (if c 1 0) (if d 1 0))))

(define (sk-1 a b c d)
  (define r1 (??inst a b c d))
  r1)

(define (sk-2 a b c d)
  (define r1 (??inst a b c d))
  (define r2 (??inst a b c d r1))
  r2)

(define (sk-3 a b c d)
  (define r1 (??inst a b c d))
  (define r2 (??inst a b c d r1))
  (define r3 (??inst a b c d r1 r2))
  r3)

(define (Niffp a b c d)
  (define r1 (Iff a b))
  (define r2 (Iff c d))
  (define r3 (Iff r1 r2))
  (define r4 (Not r3))
  r4)

(define (NXp a b c d)
  (define r1 (Xor a b))
  (define r2 (Not r1))
  (define r3 (Xor c d))
  (define r4 (Not r3))
  (define r5 (Xor r2 r4))
  r5)

(define (AIGp a b c d)
  (define r1 (Not a))
  (define r2 (Not b))
  (define r3 (And r1 r2))
  (define r4 (Not r3))
  (define r5 (And a b))
  (define r6 (Not r5))
  (define r7 (And r4 r6))
  (define r8 (Not r7))
  (define r9 (Not c))
  (define r10 (Not d))
  (define r11 (And r9 r10))
  (define r12 (Not r11))
  (define r13 (And c d))
  (define r14 (Not r13))
  (define r15 (And r12 r14))
  (define r16 (Not r15))
  (define r17 (Not r8))
  (define r18 (Not r16))
  (define r19 (And r17 r18))
  (define r20 (Not r19))
  (define r21 (And r8 r16))
  (define r22 (Not r21))
  (define r23 (And r20 r22))
  (define r24 (Not r23))
  (define r25 (Not r24))
  r25)

; Sample interactions wrapped in a main module
; (see Racket docs) so they don't get evaluated
; when the shallow.rkt module is imported. 
(module* main #f 
  (ver Niffp NXp)
  (ver NXp specp)
  (syn sk-1 AIGp)
  (syn sk-2 AIGp)
  (syn sk-3 AIGp))
  

Solver-Aided-Programming-Tutorial-Solutions.md

This gist contains the exercise solutions for the Tutorial on Solver-Aided Programming presented at CAV 2019.

sudoku.rkt

#lang rosette

(define (choice type)
  (define-symbolic* c type)
  c)

; A puzzle is represented as a list of 81 digits,
; obtained by concatenating the rows of the puzzle,
; from first to last. This procedure takes as input 
; a puzzle and checks that it satisfies the Sudoku rules.
(define (sudoku-check puzzle)    
  (for ([digit puzzle])             ; all digits between 1 and 9
    (assert (and (<= 1 digit) (<= digit 9))))  
  (for ([row (rows puzzle)])        ; all different in a row
    (assert (apply distinct? row)))            
  (for ([column (columns puzzle)])  ; all different in a column
    (assert (apply distinct? column)))        
  (for ([region (regions puzzle)])  ; all different in a 3x3 region
    (assert (apply distinct? region))))

(define (rows puzzle [n 9])   
  (if (null? puzzle) 
      null
      (cons (take puzzle n)
            (rows (drop puzzle n) n))))

(define (columns puzzle [n 9])
  (if (null? puzzle)
      (make-list n null)
      (map cons
           (take puzzle n)
           (columns (drop puzzle n) n))))

(define (regions puzzle)
  (define rows3 (curryr rows 3))
  (define cols3 (curryr columns 3))
  (map flatten
       (append-map
        append
        (cols3
         (append-map
          rows3
          (cols3
           (append-map rows3 (rows puzzle))))))))

(define (char->digit c)
  (- (char->integer c) (char->integer #\0)))
  
(define (string->puzzle p)
  (map char->digit (string->list p)))

(define (show puzzle)
  (pretty-print (rows puzzle)))

  
; Sample solved puzzle.
(define p0 (string->puzzle "693784512487512936125963874932651487568247391741398625319475268856129743274836159"))
; Sample unsolved puzzle where 0 represents unfilled cells.
(define p1 (string->puzzle "000000010400000000020000000000050604008000300001090000300400200050100000000807000"))

(define (puzzle->symbolic puzzle)
  (for/list ([i puzzle])
      (if (= i 0) (choice integer?) i)))

(define (solve-puzzle puzzle)
  (define sp (puzzle->symbolic puzzle))
  (define sol
    (solve (sudoku-check sp)))
  (and (sat? sol)
       (evaluate sp sol)))

(define (valid-puzzle? puzzle)
  (define sp1 (puzzle->symbolic puzzle))
  (define sp2 (puzzle->symbolic puzzle))
  (unsat?
   (solve
    (begin
      (sudoku-check sp1)
      (sudoku-check sp2)
      (assert (not (equal? sp1 sp2)))))))
      
(define (generate-puzzle)
  (for/fold ([p (solve-puzzle (make-list 81 0))])
            ([i (shuffle (build-list 81 values))])
    (let ([pi0 (list-set p i 0)])
      (if (valid-puzzle? pi0) pi0 p))))
    
  
(show p0)
(show p1)
(valid-puzzle? p0) ; #t
(valid-puzzle? p1) ; #t
(valid-puzzle? ; p1 with one more empty cell is not valid ...
 (string->puzzle
  "000000000400000000020000000000050604008000300001090000300400200050100000000807000"))

(show (solve-puzzle p0))
(show (solve-puzzle p1))

(random-seed 20190714)
(time (show (generate-puzzle)))

warmup.rkt

#lang rosette

(define (abs-spec x)
  (if (bvslt x (bv 0 32))
      (bvneg x)
      x))

(define (abs-impl x) 
  (let* ([o1 (bvashr x (bv 31 32))]
         [o2 (bvadd x o1)]
         [o3 (bvsub o2 o1)])
    o3))

(assert (equal? (abs-impl (bv #x00000000 32)) 
                (abs-spec (bv #x00000000 32))))
(assert (equal? (abs-impl (bv #x00000003 32)) 
                (abs-spec (bv #x00000003 32))))
(assert (equal? (abs-impl (bv #x80000000 32)) 
                (abs-spec (bv #x80000000 32))))

(define-symbolic x (bitvector 32))
(define cex
  (verify
   (assert
    (equal? (abs-spec x) (abs-impl x)))))

(define fault (evaluate x cex))
fault

(require rosette/query/debug rosette/lib/render)

(define/debug (abs-impl-2 x) 
  (let* ([o1 (bvashr x (bv 31 32))]
         [o2 (bvadd x o1)]
         [o3 (bvsub o2 o1)])
    o3))


(render
 (debug [(bitvector 32)]
        (assert (equal? (abs-spec fault) (abs-impl-2 fault)))))

(require rosette/lib/synthax)

(define (abs-impl-3 x) 
  (let* ([o1 (bvashr x (bv 31 32))]
         [o2 ((choose bvadd bvand bvor bvxor bvshl bvlshr bvashr) x o1)]
         [o3 ((choose bvsub bvand bvor bvxor bvshl bvlshr bvashr) o2 o1)])
    o3))

(print-forms
 (synthesize
  #:forall x
  #:guarantee (assert (equal? (abs-spec x) (abs-impl-3 x)))))