tuzz

tuzz

(set-option :pp.bv-literals false)
(define-sort I () (_ BitVec 300))

(declare-const a I)
(declare-const b I)
(declare-const c I)
(declare-const d I)
(declare-const e I)
(declare-const f I)
(declare-const g I)

tuzz

# A Sentient program to encode ISBN-10s, ISBN-13s, their check
# digits and how they relate.

# Declare all parts of the ISBN including check digits.
int5 ten0, ten1, ten2, ten3, ten4, ten5, ten6, ten7, ten8;
int5 ten_check_digit, thirteen_check_digit;

# State that all digits must be between 0 and 9 inclusive aside
# from ISBN-10 check digits which can include 10.
invariant ten0 >= 0, ten0 <= 9;

tuzz

# I have a problem at work that I _think_ is the Knapsack Problem but perhaps
# someone here can help me research/find a heuristic solution: we have access
# to the <redacted> and get a finite number of “rules” we can use (e.g. 1000)
# and each rule can only be 1024 characters long and have a maximum of 30
# operators in them (e.g. “foo OR bar OR baz”), we have a list of domains
# (e.g. example.com, example.org) we want to pack domains into rules as
# efficiently as possible in the minimum number of rules.

# Here's an attempt at a Sentient program to solve the decision version of
# this problem, i.e. Can 100 domains fit into 5 rules?

tuzz

# A Sentient program in response to this tweet:
# https://twitter.com/jamestanton/status/874962919963885568
#
# Run it with:
# for i in {1..100}; do ruby search.rb $i > search.snt && sentient -c -o -r -n 0 -m lingeling search.snt; done

n = Integer(ARGV.first)

program = <<-SNT
array#{n}<int5> numbers;

tuzz

# A Sentient[1] program that solves this problem:
#
# Given three and five gallon buckets and a water supply, fill the five gallon
# bucket with four gallons of water. [2]
#
# [1] http://sentient-lang.org/
# [2] http://nchammas.com/writing/how-not-to-die-hard-with-hypothesis
#
# Sentient solves this in a minimum of six steps:
#

tuzz

I've been thinking about pre-computing a database of pangram solutions. Why?

• I think it would be fun
• I like the idea of showing solutions in real-time as you type
• I'm interested in patterns/stats relating to the set

I started thinking about which pangrams I should pre-compute, e.g.

• "This seventy first pangram contains ..."
• "This pangram is dedicated to John Smith and it contains ..."

tuzz

dimacs = JSON.parse(File.read("foo.json"))["dimacs"].split("\n")[1..-1].map { |line| line.split(" ")[0..-2].map { |s| s.start_with?("-") ? "!x#{s[1..-1]}" : "x#{s}" }.join(" || ") }.map { |line| "(#{line})" }.join(" && ")

tuzz

# Five of Santa's reindeer are lost.
#
# Rudolph has found them by the frozen waterfall, and knows the way back to
# Santa's stable.
#
# But Rudolph's nose will only light the way for one or two other reindeer at a
# time, so he cannot travel with more.
#
# And unfortunately, Rudolph doesn't know the quickest route from the stable to
# the waterfall (and he won't learn it either), so he can't make the journey

tuzz

function main () {
  array9<array9<int5>> sudoku;

  sudoku.each(function (row) {
    invariant row.uniq?;

    invariant row.all?(function (n) {
      return n.between?(1, 9);
    });
  });