Skip to content

Instantly share code, notes, and snippets.

Avatar

Philip Zucker philzook58

View GitHub Profile
@philzook58
philzook58 / custom_cart.py
Created December 27, 2017 02:04
Edited Cartpole
View custom_cart.py
"""
Classic cart-pole system implemented by Rich Sutton et al.
Copied from http://incompleteideas.net/sutton/book/code/pole.c
permalink: https://perma.cc/C9ZM-652R
Edit reset in order to change initial stae to down low
"""
@philzook58
philzook58 / app.py
Last active August 18, 2019 18:57
test_gist
View app.py
print("Success!")
import pickle
favorite_color = { "lion": "yellow", "kitty": "red" }
import os
os.mkdir("logs")
pickle.dump( favorite_color, open( "./logs/save.p", "wb" ) )
print("it good b")
@philzook58
philzook58 / optimal_relation.hs
Created November 26, 2019 20:34
a sketch of using linear relations for LQR control
View optimal_relation.hs
-- state of an oscillator
data SHOState = X | P deriving (Show, Enum, Bounded, Eq, Ord)
data Control = F deriving (Show, Enum, Bounded, Eq, Ord)
-- Costate newtype wrapper
newtype Co a = Co a deriving (Show, Enum, Bounded, Eq, Ord)
type M = Matrix Double
dynamics :: forall x u. (BEnum x, BEnum u) => Matrix Double -> Matrix Double ->
HLinRel (Either x u) x
@philzook58
philzook58 / SOS Diff Eq.ipynb
Created December 12, 2019 03:53
Sum of squares for differential equations
View SOS Diff Eq.ipynb
Sorry, something went wrong. Reload?
Sorry, we cannot display this file.
Sorry, this file is invalid so it cannot be displayed.
@philzook58
philzook58 / laplace.hs
Created December 22, 2019 18:46
Laplace equation using linear relations in hmatrix
View laplace.hs
type HLinRel2D u d l r = HLinRel (Either u l) (Either d r)
{-
A stencil of 2d resistors for tiling
u
/
\
@philzook58
philzook58 / batcher.py
Last active December 24, 2019 23:32
z3 verify sorting network
View batcher.py
#direct from https://en.wikipedia.org/wiki/Batcher_odd%E2%80%93even_mergesort
def oddeven_merge(lo: int, hi: int, r: int):
step = r * 2
if step < hi - lo:
yield from oddeven_merge(lo, hi, step)
yield from oddeven_merge(lo + r, hi, step)
yield from [(i, i + r) for i in range(lo + r, hi - r, step)]
else:
yield (lo, lo + r)
@philzook58
philzook58 / bab.py
Created December 29, 2019 04:09
simple z3py proofs
View bab.py
def babylonian(x):
res = 1
for i in range(7):
res = (x / res + res) / 2
return res
x, y = Reals("x y")
prove(Implies(And(y**2 == x, y >= 0, 0 <= x, x <= 10), babylonian(x) - y <= 0.01))
@philzook58
philzook58 / euler.py
Last active January 7, 2020 02:54
positive polynomial optimization + taylor model sketch idea
View euler.py
import cvxpy as cvx
import numpy as np
import sos
import sympy as sy
import matplotlib.pyplot as plt
#raised chebyehve
t = sy.symbols("t")
N = 5
# seems like even N becomes infeasible.
@philzook58
philzook58 / combinators.py
Last active January 25, 2020 19:36
z3py relation algebra sketch
View combinators.py
trivial = BoolVal(True)
def top1(x,y): # top is the full relation,
return trivial
def bottom1(x,y):
return BoolVal(False)
def top2(sorty):
def res(x):
y = FreshConst(sorty)
@philzook58
philzook58 / linrel.jl
Last active January 26, 2020 19:34
Sketch of linear relations in julia
View linrel.jl
#A*x = 0
using LinearAlgebra
struct HRep{T}
n :: Int64 #input size
A :: AbstractArray{T}
end
struct VRep{T}
n :: Int64 #input size
A :: AbstractArray{T}
end