Emina Torlak

Lab 1: Getting Started with Solver-Aided Programming

The following exercises explore the concepts covered in Part 1 of the tutorial on solver-aided programming presented at CAV 2019.

Warmup (solution)

Suppose that you are an app developer for a super low-power chip that achieves peak energy efficiency on programs with few or no branches. To build apps faster, you hire Ben Bitdiddle to create a library of efficient primitives for this chip, starting with a branch-free function that computes the absolute value of a 32-bit bitvector. Here is a reference implementation (specification) for this function in Rosette, using the built-in bitvector datatype:

#lang rosette

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

Ben comes up with the following implementation that works on his test suite:

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

; zero, positive, negative ...
> (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))))

Help review Ben’s code by answering the following questions. If a question requires you to modify his implementation in any way, do so on a fresh copy with a new name such as abs-impl-N where N is the question number.

Solving Sudoku (solution)

Rosette’s solve query implements a form of angelic execution. This idea dates back to a 1966 paper by Floyd who proposed it as an elegant way to hide the details of backtracking search behind a language construct he called choice.

Conceptually, the choice function non-determinstically chooses a value to return so that all subsequent assertions are satisfied.

For example, choice would pick the values #f and #t to execute the following program angelically:

#lang rosette

(define (choice type) ...) ; <-- implement choice

(define (more-or-less-1 x)
  (if (choice boolean?)
      (+ x 1)
      (- x 1)))

(solve (assert (= 0 (more-or-less-1 1)))) ; #f
(solve (assert (= 2 (more-or-less-1 1)))) ; #t

Complete the above implementation of the choice function.

Now, consider the implementation of a checker for Sudoku solutions shown below: given a 9x9 Sudoku solution expressed a list of 81 integers, the check-sudoku procedure succeeds if and only if the solution satisfies the rules of Sudoku.

; 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)))

(define (solve-puzzle puzzle) ...)
(define (valid-puzzle? puzzle) ...)
(define (generate-puzzle) ...)

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

> (show p0)
'((6 9 3 7 8 4 5 1 2)
  (4 8 7 5 1 2 9 3 6)
  (1 2 5 9 6 3 8 7 4)
  (9 3 2 6 5 1 4 8 7)
  (5 6 8 2 4 7 3 9 1)
  (7 4 1 3 9 8 6 2 5)
  (3 1 9 4 7 5 2 6 8)
  (8 5 6 1 2 9 7 4 3)
  (2 7 4 8 3 6 1 5 9))
> (sudoku-check p0)
> (show p1)
'((0 0 0 0 0 0 0 1 0)
  (4 0 0 0 0 0 0 0 0)
  (0 2 0 0 0 0 0 0 0)
  (0 0 0 0 5 0 6 0 4)
  (0 0 8 0 0 0 3 0 0)
  (0 0 1 0 9 0 0 0 0)
  (3 0 0 4 0 0 2 0 0)
  (0 5 0 1 0 0 0 0 0)
  (0 0 0 8 0 7 0 0 0))
> (sudoku-check p1)
assert: failed

Verifying a majority voting algorithm (solution)

The Boyer–Moore majority vote algorithm is a beautiful and tricky procedure for finding a majority element in a list, using linear time and constant space.

Complete the following Rosette implementation of Boyer-Moore and verify its correctness for any list of N arbitrary integers.

#lang rosette

(define (boyer-moore xs)
  (define m ...)
  (define i ...)
  (for ([x xs])
    (cond [...]
          [...]
          [else ...]))
  m)

(define (check n [bw #f])
  (current-bitwidth bw)
  (define-symbolic* xs integer? [n])
  ...)

(time (check 10))