Skip to content

Instantly share code, notes, and snippets.


Philip Zucker philzook58

View GitHub Profile
philzook58 /
Created December 27, 2017 02:04
Edited Cartpole
Classic cart-pole system implemented by Rich Sutton et al.
Copied from
Edit reset in order to change initial stae to down low
philzook58 /
Last active August 18, 2019 18:57
import pickle
favorite_color = { "lion": "yellow", "kitty": "red" }
import os
pickle.dump( favorite_color, open( "./logs/save.p", "wb" ) )
print("it good b")
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 / 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 / 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
philzook58 /
Last active December 24, 2019 23:32
z3 verify sorting network
#direct from
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)]
yield (lo, lo + r)
philzook58 /
Created December 29, 2019 04:09
simple z3py proofs
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 /
Created December 29, 2019 23:59
Verifying a neural network with z3
import sympy as sy
import matplotlib.pyplot as plt
import numpy as np
x = sy.symbols('x')
cheb = sy.lambdify(x, sy.chebyshevt(4,x))
xs = np.linspace(-1,1,1000)
ys = cheb(xs)
plt.plot(xs, ys)
philzook58 /
Last active January 7, 2020 02:54
positive polynomial optimization + taylor model sketch idea
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 /
Last active January 25, 2020 19:36
z3py relation algebra sketch
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)