nonograms
diff --git a/sentient/gchq.json b/sentient/gchq.json
new file mode 100644
index 0000000..ed95b13
--- /dev/null
+++ b/sentient/gchq.json
@@ -0,0 +1,81 @@
+{
+ "rowNumbers": [
+ [7, 3, 1, 1, 7],
+ [1, 1, 2, 2, 1, 1],
+ [1, 3, 1, 3, 1, 1, 3, 1],
+ [1, 3, 1, 1, 6, 1, 3, 1],
+ [1, 3, 1, 5, 2, 1, 3, 1],
+ [1, 1, 2, 1, 1],
+ [7, 1, 1, 1, 1, 1, 7],
+ [3, 3],
+ [1, 2, 3, 1, 1, 3, 1, 1, 2],
+ [1, 1, 3, 2, 1, 1],
+ [4, 1, 4, 2, 1, 2],
+ [1, 1, 1, 1, 1, 4, 1, 3],
+ [2, 1, 1, 1, 2, 5],
+ [3, 2, 2, 6, 3, 1],
+ [1, 9, 1, 1, 2, 1],
+ [2, 1, 2, 2, 3, 1],
+ [3, 1, 1, 1, 1, 5, 1],
+ [1, 2, 2, 5],
+ [7, 1, 2, 1, 1, 1, 3],
+ [1, 1, 2, 1, 2, 2, 1],
+ [1, 3, 1, 4, 5, 1],
+ [1, 3, 1, 3, 10, 2],
+ [1, 3, 1, 1, 6, 6],
+ [1, 1, 2, 1, 1, 2],
+ [7, 2, 1, 2, 5]
+ ],
+ "columnNumbers": [
+ [7, 2, 1, 1, 7],
+ [1, 1, 2, 2, 1, 1],
+ [1, 3, 1, 3, 1, 3, 1, 3, 1],
+ [1, 3, 1, 1, 5, 1, 3, 1],
+ [1, 3, 1, 1, 4, 1, 3, 1],
+ [1, 1, 1, 2, 1, 1],
+ [7, 1, 1, 1, 1, 1, 7],
+ [1, 1, 3],
+ [2, 1, 2, 1, 8, 2, 1],
+ [2, 2, 1, 2, 1, 1, 1, 2],
+ [1, 7, 3, 2, 1],
+ [1, 2, 3, 1, 1, 1, 1, 1],
+ [4, 1, 1, 2, 6],
+ [3, 3, 1, 1, 1, 3, 1],
+ [1, 2, 5, 2, 2],
+ [2, 2, 1, 1, 1, 1, 1, 2, 1],
+ [1, 3, 3, 2, 1, 8, 1],
+ [6, 2, 1],
+ [7, 1, 4, 1, 1, 3],
+ [1, 1, 1, 1, 4],
+ [1, 3, 1, 3, 7, 1],
+ [1, 3, 1, 1, 1, 2, 1, 1, 4],
+ [1, 3, 1, 4, 3, 3],
+ [1, 1, 2, 2, 2, 6, 1],
+ [7, 1, 3, 2, 1, 1]
+ ],
+ "grid": {
+ "3": {
+ "3": true, "4": true,
+ "12": true, "13": true,
+ "21": true
+ },
+ "8": {
+ "6": true, "7": true,
+ "10": true,
+ "14": true, "15": true,
+ "18": true
+ },
+ "16": {
+ "6": true,
+ "11": true,
+ "16": true,
+ "20": true
+ },
+ "21": {
+ "3": true, "4": true,
+ "9": true, "10": true,
+ "15": true,
+ "20": true, "21": true
+ }
+ }
+}
diff --git a/sentient/nonogram.json b/sentient/nonogram.json
new file mode 100644
index 0000000..e69de29
diff --git a/sentient/nonogram.snt b/sentient/nonogram.snt
new file mode 100644
index 0000000..0a09a8b
--- /dev/null
+++ b/sentient/nonogram.snt
@@ -0,0 +1,49 @@
+function main () {
+ array25<array25<bool>> grid;
+ array25<array13<int6>> rowNumbers, columnNumbers;
+
+ rowNumbers = removeZeros(rowNumbers);
+ columnNumbers = removeZeros(columnNumbers);
+
+ grid.validate!(rowNumbers);
+ grid.transpose.validate!(columnNumbers);
+
+ expose grid, rowNumbers, columnNumbers;
+};
+
+function removeZeros (numbersArray) {
+ return numbersArray.map(function (numbers) {
+ return numbers.reject(*zero?);
+ });
+};
+
+function validate! (grid, rowNumbers) {
+ rowNumbers.each(function^ (numbers, rowIndex) {
+ cells = grid[rowIndex];
+
+ previous = false;
+ count = 0;
+ index = -1;
+
+ cells.each(function^ (cell) {
+ edge = cell != previous;
+ endOfRun = edge && !cell;
+
+ tickOffNumberIf(endOfRun);
+
+ count = edge ? 1 : count + 1;
+ previous = cell;
+ });
+
+ tickOffNumberIf(previous);
+ invariant index == numbers.length - 1;
+ });
+};
+
+function^ tickOffNumberIf (condition) {
+ index += condition ? 1 : 0;
+ number, inBounds = numbers.get(index);
+ invariant condition ? number == count : true;
+};
+
+main();
\ No newline at end of file
diff --git a/z3/Gemfile b/z3/Gemfile
new file mode 100644
index 0000000..6306eb5
--- /dev/null
+++ b/z3/Gemfile
@@ -0,0 +1,7 @@
+# frozen_string_literal: true
+
+source "https://rubygems.org"
+
+git_source(:github) {|repo_name| "https://github.com/#{repo_name}" }
+
+gem "z3"
diff --git a/z3/Gemfile.lock b/z3/Gemfile.lock
new file mode 100644
index 0000000..284ef12
--- /dev/null
+++ b/z3/Gemfile.lock
@@ -0,0 +1,15 @@
+GEM
+ remote: https://rubygems.org/
+ specs:
+ ffi (1.15.0)
+ z3 (0.0.20181229)
+ ffi (~> 1.9)
+
+PLATFORMS
+ x86_64-darwin-17
+
+DEPENDENCIES
+ z3
+
+BUNDLED WITH
+ 2.2.16
diff --git a/z3/hello.py b/z3/hello.py
new file mode 100644
index 0000000..f1edaf4
--- /dev/null
+++ b/z3/hello.py
@@ -0,0 +1,5 @@
+from z3 import *
+
+x = Int('x')
+y = Int('y')
+solve(x > 2, y < 10, x + 2*y == 7)
diff --git a/z3/red-vs-blue.py b/z3/red-vs-blue.py
new file mode 100644
index 0000000..c0d5e4c
--- /dev/null
+++ b/z3/red-vs-blue.py
@@ -0,0 +1,155 @@
+from itertools import *
+from z3 import *
+
+row_rules = [
+ [17, 4],
+ [17, 1, 3],
+ [14, 2, 3],
+ [12, 1, 3],
+ [9, 2, 2, 1],
+
+ [2, 7, 1, 4],
+ [4, 4, 3, 1, 1],
+ [1, 3, 2, 1, 3, 1, 1],
+ [3, 2, 3, 2],
+ [3, 1, 2, 3, 1],
+
+ [2, 5, 2, 1, 3, 1],
+ [1, 8, 1, 2, 3],
+ [1, 11, 1, 1],
+ [2, 1, 2, 6, 4, 2],
+ [1, 1, 4, 3, 1],
+
+ [2, 2, 1, 3, 2],
+ [1, 2, 3, 1],
+ [1, 2, 1, 3],
+ [4, 2, 1],
+ [3, 1, 2],
+
+ [3, 2, 1],
+ [3, 1, 1, 2],
+ [3, 2, 1],
+ [3, 2, 2],
+ [3, 2, 1],
+
+ [4, 3, 2],
+ [2, 3, 3, 1],
+ [3, 4, 4],
+ [6, 1, 1],
+ [4],
+]
+
+col_rules = [
+ [3, 2, 2, 1, 1, 11],
+ [3, 3, 2, 1, 2, 11],
+ [3, 4, 2, 3, 6, 2],
+ [3, 4, 3, 6, 1],
+ [3, 7, 1, 6],
+
+ [3, 4, 4, 7],
+ [3, 2, 6, 6],
+ [3, 8, 3, 1],
+ [3, 8, 2, 1],
+ [3, 8, 2, 2],
+
+ [3, 6, 1, 1],
+ [3, 3, 2, 6],
+ [3, 1, 4, 5],
+ [3, 4, 2, 5],
+ [6, 7, 1, 4],
+
+ [6, 9, 2, 4],
+ [6, 1, 9, 1, 3],
+ [6, 4, 9, 2, 3],
+ [4, 6, 9, 1, 2],
+ [2, 1, 3, 9, 2, 2],
+
+ [4, 1, 2, 11, 1],
+ [6, 5, 9, 2],
+ [7, 6, 6, 4],
+ [6, 6, 4, 6],
+ [1, 7, 6, 1, 8],
+
+ [1, 1, 3, 6, 10],
+ [2, 1, 1, 4, 12],
+ [2, 1, 2, 1, 1, 14],
+ [3, 1, 3, 16],
+ [3, 4, 18],
+]
+
+def pairwise(iterable):
+ "s -> (s0,s1), (s1,s2), (s2, s3), ..."
+ a, b = tee(iterable)
+ next(b, None)
+ return zip(a, b)
+
+def cell(x, y):
+ return Bool(f"cell-{x},{y}")
+
+def row(y):
+ return [cell(x, y) for x in range(0, len(col_rules))]
+
+def col(x):
+ return [cell(x, y) for y in range(0, len(row_rules))]
+
+s = Solver()
+
+for x, col_rule in enumerate(col_rules):
+ stripe_name = f"col-{x}"
+ stripe_constraints = col_rule
+ stripe = col(x)
+ group_count = len(stripe_constraints)
+ group_start = [Int(f"{stripe_name}-{i}-start") for i in range(0, group_count)]
+ group_end = [Int(f"{stripe_name}-{i}-end") for i in range(0, group_count)]
+
+ # # Start and end of each group
+ for i in range(0, group_count):
+ s.add(group_start[i] >= 0, group_start[i] < len(stripe))
+ s.add(group_end[i] >= 0, group_end[i] < len(stripe))
+ s.add(group_end[i] - group_start[i] == stripe_constraints[i] - 1)
+
+ # Gap between each group and following group
+ for i, j in pairwise(range(0, group_count)):
+ s.add(group_start[j] >= group_end[i] + 2)
+
+ # Cells
+ for k in range(0, len(stripe)):
+ cell_in_specific_group = [
+ And(k >= group_start[i], k <= group_end[i])
+ for i in range(0, group_count)
+ ]
+ s.add(stripe[k] == Or(*cell_in_specific_group))
+
+for y, row_rule in enumerate(row_rules):
+ stripe_name = f"row-{y}"
+ stripe_constraints = row_rule
+ stripe = row(y)
+ group_count = len(stripe_constraints)
+ group_start = [Int(f"{stripe_name}-{i}-start") for i in range(0, group_count)]
+ group_end = [Int(f"{stripe_name}-{i}-end") for i in range(0, group_count)]
+
+ # # Start and end of each group
+ for i in range(0, group_count):
+ s.add(group_start[i] >= 0, group_start[i] < len(stripe))
+ s.add(group_end[i] >= 0, group_end[i] < len(stripe))
+ s.add(group_end[i] - group_start[i] == stripe_constraints[i] - 1)
+
+ # Gap between each group and following group
+ for i, j in pairwise(range(0, group_count)):
+ s.add(group_start[j] >= group_end[i] + 2)
+
+ # Cells
+ for k in range(0, len(stripe)):
+ cell_in_specific_group = [
+ And(k >= group_start[i], k <= group_end[i])
+ for i in range(0, group_count)
+ ]
+ s.add(stripe[k] == Not(Or(*cell_in_specific_group)))
+
+s.check()
+m = s.model()
+
+for y in range(0, len(row_rules)):
+ row = "".join(["█" if m[cell(x,y)] else " " for x in range(0, len(col_rules))])
+ print(row)
+
diff --git a/z3/red-vs-blue.rb b/z3/red-vs-blue.rb
new file mode 100644
index 0000000..399def2
--- /dev/null
+++ b/z3/red-vs-blue.rb
@@ -0,0 +1,120 @@
+require "z3"
+
+class NonogramSolver
+ def initialize
+ @row_constraints = [
+ [3],
+ [5],
+ [3,1],
+ [2,1],
+ [3,3,4],
+ [2,2,7],
+ [6,1,1],
+ [4,2,2],
+ [1,1],
+ [3,1],
+ [6],
+ [2,7],
+ [6,3,1],
+ [1,2,2,1,1],
+ [4,1,1,3],
+ [4,2,2],
+ [3,3,1],
+ [3,3],
+ [3],
+ [2,1],
+ ]
+ @column_constraints = [
+ [2],
+ [1,2],
+ [2,3],
+ [2,3],
+ [3,1,1],
+ [2,1,1],
+ [1,1,1,2,2],
+ [1,1,3,1,3],
+ [2,6,4],
+ [3,3,9,1],
+ [5,3,2],
+ [3,1,2,2],
+ [2,1,7],
+ [3,3,2],
+ [2,4],
+ [2,1,2],
+ [2,2,1],
+ [2,2],
+ [1],
+ [1],
+ ]
+ @row_count = @row_constraints.size
+ @column_count = @column_constraints.size
+ @solver = Z3::Solver.new
+ end
+
+ def cell(x,y)
+ Z3.Bool("cell#{x},#{y}")
+ end
+
+ def row(y)
+ (0...@column_count).map{|x| cell(x,y) }
+ end
+
+ def column(x)
+ (0...@row_count).map{|y| cell(x,y) }
+ end
+
+ def setup_grid_constraints!
+ (0...@column_count).each do |x|
+ setup_stripe_constraints! "column-#{x}", @column_constraints[x], column(x)
+ end
+
+ (0...@row_count).each do |y|
+ setup_stripe_constraints! "row-#{y}", @row_constraints[y], row(y)
+ end
+ end
+
+ def setup_stripe_constraints!(stripe_name, stripe_constraints, stripe)
+ group_count = stripe_constraints.size
+ group_start = (0...group_count).map{|i| Z3.Int("#{stripe_name}-#{i}-start")}
+ group_end = (0...group_count).map{|i| Z3.Int("#{stripe_name}-#{i}-end")}
+
+ # Start and end of each group
+ (0...group_count).each do |i|
+ @solver.assert (group_start[i] >= 0) & (group_start[i] < stripe.size)
+ @solver.assert (group_end[i] >= 0) & (group_end[i] < stripe.size)
+ @solver.assert group_end[i] - group_start[i] == stripe_constraints[i] - 1
+ end
+ # Gap between each group and following group
+ (0...group_count).each_cons(2) do |i,j|
+ @solver.assert group_start[j] >= group_end[i] + 2
+ end
+ # Cells
+ (0...stripe.size).each do |k|
+ cell_in_specific_group = (0...group_count).map{|i|
+ (k >= group_start[i]) & (k <= group_end[i])
+ }
+ @solver.assert stripe[k] == Z3.Or(*cell_in_specific_group)
+ end
+ end
+
+ def solve!
+ setup_grid_constraints!
+ if @solver.satisfiable?
+ model = @solver.model
+ (0...@row_count).each do |y|
+ (0...@column_count).each do |x|
+ value = model[cell(x,y)].to_s
+ print value == "true" ? "\u25FC" : "\u25FB"
+ end
+ print "\n"
+ end
+ else
+ puts "Nonogram has no solution"
+ end
+ end
+end
+
+if __FILE__ == $0
+ nonogram = NonogramSolver.new
+ nonogram.solve!
+end
diff --git a/z3/shell.nix b/z3/shell.nix
new file mode 100644
index 0000000..c1aa3fe
--- /dev/null
+++ b/z3/shell.nix
@@ -0,0 +1,15 @@
+{ pkgs ? import <nixpkgs> {} }:
+let
+ my-python = pkgs.python3.buildEnv.override {
+ extraLibs = [ pkgs.python3Packages.z3 ];
+ };
+in
+
+pkgs.mkShell {
+ nativeBuildInputs = [
+ pkgs.go
+ my-python
+ pkgs.ruby
+ pkgs.z3
+ ];
+}