Lab 1: Getting Started with SolverAided Programming
The following exercises explore the concepts covered in Part 1 of the tutorial on solveraided programming presented at CAV 2019.
Warmup (solution)
Suppose that you are an app developer for a super lowpower 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 branchfree function that computes the absolute value of a 32bit bitvector. Here is a reference implementation (specification) for this function in Rosette, using the builtin bitvector datatype:
#lang rosette
(define (absspec x)
(if (bvslt x (bv 0 32))
(bvneg x)
x))
Ben comes up with the following implementation that works on his test suite:
(define (absimpl x)
(let* ([o1 (bvashr x (bv 31 32))]
[o2 (bvadd x o1)]
[o3 (bvsub o2 o1)])
o3))
; zero, positive, negative ...
> (assert (equal? (absimpl (bv #x00000000 32))
(absspec (bv #x00000000 32))))
> (assert (equal? (absimpl (bv #x00000003 32))
(absspec (bv #x00000003 32))))
> (assert (equal? (absimpl (bv #x80000000 32))
(absspec (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 absimplN
where N
is the question number.

Does Ben’s implementation work on all 32bit inputs? Use the
verify
query to check. 
The verifier will reveal that Ben’s implementation is buggy. Use
debug
to localize the fault found by the verifier (and remember to save your work to a file before invokingdebug
). 
Use
synthesize
to fix Ben’s implementation as suggested by the debugger. You can assume that if Ben has made an error, it is always of the same kind: using an arithmetic operator (such as addition or subtraction) instead of a bitwise operator that takes the same arguments. It is easiest to sketch this knowledge using the choose construct.
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 nondeterminstically 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 (moreorless1 x)
(if (choice boolean?)
(+ x 1)
( x 1)))
(solve (assert (= 0 (moreorless1 1)))) ; #f
(solve (assert (= 2 (moreorless1 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 checksudoku
procedure succeeds if and only if the solution satisfies the rules of Sudoku.

Use your
choice
function, together with thesolve
query, to turn the Sudoku checker into a puzzle solver, and solve the puzzlesp1
p4
. Yoursudokusolve
procedure should take as input a puzzle and produce a solution, if one exists, or return#f
otherwise. 
Write a procedure
validpuzzle?
that takes as input a puzzle and outputs#t
if the puzzle has exactly one solution. 
How would you use
validpuzzle?
to generate minimal Sudoku puzzles, which are valid (have a unique solution) but become invalid (have multiple solutions) if any of their filled cells are erased? Implement your idea if you have time.
; 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 (sudokucheck 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)
(makelist 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
(appendmap
append
(cols3
(appendmap
rows3
(cols3
(appendmap 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)
(prettyprint (rows puzzle)))
(define (solvepuzzle puzzle) ...)
(define (validpuzzle? puzzle) ...)
(define (generatepuzzle) ...)
; 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))
> (sudokucheck 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))
> (sudokucheck 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 BoyerMoore and verify its correctness for any list of N arbitrary integers.
#lang rosette
(define (boyermoore xs)
(define m ...)
(define i ...)
(for ([x xs])
(cond [...]
[...]
[else ...]))
m)
(define (check n [bw #f])
(currentbitwidth bw)
(definesymbolic* xs integer? [n])
...)
(time (check 10))