Skip to content

Instantly share code, notes, and snippets.

View mgritter's full-sized avatar

Mark Gritter mgritter

53 followers · 19 following
View GitHub Profile
@mgritter
mgritter / Repro.hs
Created December 21, 2022 18:56
LH file that causes Z3 to take forever
module Repro (part1) where
import qualified Data.Map as Map
import Data.List.Split
import Data.Either
import Data.Maybe
import Control.Monad.ST
import Data.STRef
{-@
@mgritter
mgritter / nonintersecting_lattice_paths.py
Created November 20, 2022 07:41
Counting pairs of non-edge-intersecting lattice paths.
def init_4d(n):
return [[[[0 for i in range(n)]
for j in range(n)]
for k in range(n)]
for l in range(n)]
def recurrence(c,x1,y1,x2,y2):
total = 0
# These two cases are always valid; even if the two paths have met at
# (x1,y1), then in these cases the previous step cannot be the same, so
@mgritter
mgritter / ant_paths.py
Created November 5, 2022 06:05
Counting pairs of nonintersecting or semi-intersection lattice paths
import cairo
import math
import itertools
def base_position( i, j ):
return (i * 60 + 10, j * 50 + 10)
def drawGrid( ctx, i, j ):
ctx.set_line_width( 1 )
ctx.set_source_rgba( 0.0, 0.0, 0.0, 1.0 )
@mgritter
mgritter / Factorial.fst
Last active November 10, 2021 18:01
An F* program for computing factorial sums
module Factorial
open FStar.Mul // Give us * for multiplication instead of pairs
open FStar.IO
open FStar.Printf
let rec factorial (n:nat) : nat =
if n = 0 then 1
else n * factorial (n-1)
@mgritter
mgritter / henneberg.json
Last active July 25, 2021 01:50
Soffit grammar for Henneberg sequences generating minimal generically rigid graphs
{
"version": "0.1",
"start": "A--B",
"A; B": "B--N--A",
"A--B; C": "A--D; B--D; C--D"
}
@mgritter
mgritter / akita_capture_daemonset.yaml
Created July 13, 2021 17:58
Akita CLI Daemonset for production use
apiVersion: extensions/v1beta1
kind: DaemonSet
metadata:
name: akita-capture
namespace: superstar
spec:
selector:
matchLabels:
name: akita-capture
template:
@mgritter
mgritter / grid_coloring_z3.py
Created July 5, 2021 17:37
Grid problem solver with Z3
from z3 import *
import itertools
# A color type
num_colors = 8
Color, color_consts = EnumSort( 'Color',
[ f"{c}" for c in range(num_colors) ] )
# Edges
# --0,0-- --0,1-- --0,2-- horizontal
@mgritter
mgritter / soffit.json
Last active May 20, 2021 14:05
WIP -- Soffit grammar for building ontologies, based on http://www.inf.ufes.br/~gguizzardi/Building_Correct_Taxonomies_with_a_Well_Founded_Graph_Grammar.pdf
{
"version": "0.1",
"start": "K[kind]; K->N [name]; N",
"K[kind];": [
"K[kind]; K2[kind]; K2->N2 [name]; ",
"K[kind]; K2[category]; K2->N2 [name]; K2->K2[depth 0]",
"K[kind]; K2[category]; K2->N2 [name]; K2->K2[depth 1]",
"K[kind]; K2[category]; K2->N2 [name]; K2->K2[depth 2]",
"K[kind]; K2[mixin]; K2->N2 [name]; K2->K2[depth 0]",
"K[kind]; K2[mixin]; K2->N2 [name]; K2->K2[depth 1]",
@mgritter
mgritter / primes_mod_6.cpp
Last active May 9, 2021 04:20
Use primesieve to find the primes where the Chebyshev bias mod 6 is zero
#include <primesieve.hpp>
#include <iostream>
// Compile with: g++ -Wall -O3 -o primes_mod_6 primes_mod_6.cpp -lprimesieve
int main( int argc, char *argv[] ) {
primesieve::iterator it;
uint64_t prime = it.next_prime();
uint64_t count_mod_1 = 0;
uint64_t count_mod_5 = 0;
@mgritter
mgritter / euler_circuit.json
Created May 8, 2021 18:43
Soffit rule to generate Euler Circuits
{
"version": "0.1",
"start": "X[node]; Y[node]; Z[node]; XY[edge]; XY->X; XY->Y; YZ[edge]; YZ->Y; YZ->Z; ZX[edge]; ZX->X; ZX->Z; XY->YZ->ZX->XY [cycle]",
"Z[node]; PZ[edge]; PZ->Z; ZS[edge]; ZS->Z; PZ->ZS[cycle]":
"Z[node]; PZ[edge]; PZ->Z; ZS[edge]; ZS->Z; A[node]; ZA[edge]; ZA->Z; ZA->A; PZ->ZA [cycle]; B[node]; AB[edge]; AB->A; AB->B; ZA->AB [cycle]; BZ[edge]; BZ->B; BZ->Z; AB->BZ [cycle]; BZ->ZS[cycle]",
"A[node]; PA[edge]; PA->A; AS[edge]; AS->A; PA->AS[cycle]; B[node]; C[node];" :
"A[node]; PA[edge]; PA->A; AS[edge]; AS->A; B[node]; AB[edge]; AB->A; AB->B; PA->AB [cycle]; C[node]; BC[edge]; BC->B; BC->C; AB->BC [cycle]; CA[edge]; CA->C; CA->A; BC->CA [cycle]; CA->AS [cycle];"
}