philnguyen

#lang typed/racket

(require z3/ffi
         z3/smt)

;; Example of how to use Z3-Model in current Racket Z3 library.
;; The common pattern in extracting data with the low-level Z3 library is
;; - querying how many things are there
;; - getting the ith "key" and "value"
;; Some functions used in the following example:

philnguyen

(ℬ (tree) … ((tree ↦ tree_₂)))
↦

;;;;; ok cases

;; `tree` is either a number, in which case `vertices` returns 1
;; or `tree` is a pair, in which case `vertices`returns an exact positive integer
;; Looking up path-condition tails `γ₁` and `γ₂` recursively tell facts
;; about `(car tree)` and `(cdr tree)`

philnguyen

#lang racket

#|
let app = 5;;
let app = 2;;
let z = 3;;
let z = 2;;
let app = 3 in app + z;;
app * z
|#

philnguyen

#lang racket

(let* ([try (λ (f) (or (f #f) (f #t)))]
       [p (λ (x₁ x₂ x₃ x₄ x₅ x₆ x₇ x₈ x₉ x₁₀)
              (and x₁ x₂ x₃ x₄ x₅ x₆ x₇ x₈ x₉ x₁₀))]
       [solve
        (λ (q)
          (try (λ (n₁)
                 (try (λ (n₂)
                        (try (λ (n₃)

philnguyen

mkdir -p out
cp 01-intro.tex out/01-intro.tex
sed -f latex-unicode-pre.sed      -i.bak out/01-intro.tex
sed -f latex-unicode-escape.sed   -i.bak out/01-intro.tex
sed -f latex-unicode.sed          -i.bak out/01-intro.tex
sed -f latex-unicode-unescape.sed -i.bak out/01-intro.tex
sed -f latex-unicode-post.sed     -i.bak out/01-intro.tex
mkdir -p out
cp 14-conclusions.tex out/14-conclusions.tex
sed -f latex-unicode-pre.sed      -i.bak out/14-conclusions.tex

philnguyen

import pyvw
from nltk.corpus import wordnet as wn

valid_labels = {'n.act': 0,
'n.animal': 1,
'n.artifact': 2,
'n.attribute': 3,
'n.body': 4,
'n.cognition': 5,
'n.communication': 6,

philnguyen

import sys
import random

# Given file name, make an iterator returning random line batches, each of which is also randomized
def iterRandomLines(filename):
    batches = readBatches(filename)
    random.shuffle(batches)
    for lines in batches:
        random.shuffle(lines) #FIXME: we don't want to randomize lines within each batch
        for line in lines:

philnguyen

import leon.lang._
import leon.lang.synthesis._
import leon.annotation._

object Test {
  
  /** Compute n's reciprocal, requiring n != 0 */
  def recip (n: Int): Int = {
    require (n != 0)
    1 / n

philnguyen

import leon.lang._
import leon.lang.synthesis._
import leon.annotation._

object BraunTree {
  sealed abstract class Tree
  case object Leaf extends Tree
  case class Node(l: Tree, n: Int, r: Tree) extends Tree
  
  def size(t: Tree): Int = t match {

philnguyen

import scala.language.experimental.macros
import scala.reflect.macros.blackbox.Context
import scala.annotation.StaticAnnotation
import scala.annotation.compileTimeOnly

/**
This annotation turns a simple class declaration into a type-safe and unboxed Enum.
It does not attempt to be compatible with Java, because I have no respect for Java.
There is an example usage at the end of the file.
*/