Instantly share code, notes, and snippets.

Philip Zucker philzook58

Created December 27, 2017 02:04
Edited Cartpole
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters. Learn more about bidirectional Unicode characters
 """ 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 """
Last active August 18, 2019 18:57
test_gist
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters. Learn more about bidirectional Unicode characters
 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")
Created November 26, 2019 20:34
a sketch of using linear relations for LQR control
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters. Learn more about bidirectional Unicode characters
 -- 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
Created December 12, 2019 03:53
Sum of squares for differential equations
Sorry, we cannot display this file.
Sorry, this file is invalid so it cannot be displayed.
Created December 22, 2019 18:46
Laplace equation using linear relations in hmatrix
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters. Learn more about bidirectional Unicode characters
 type HLinRel2D u d l r = HLinRel (Either u l) (Either d r) {- A stencil of 2d resistors for tiling u / \
Last active December 24, 2019 23:32
z3 verify sorting network
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters. Learn more about bidirectional Unicode characters
 #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)
Created December 29, 2019 04:09
simple z3py proofs
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters. Learn more about bidirectional Unicode characters
 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))
Created December 29, 2019 23:59
Verifying a neural network with z3
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters. Learn more about bidirectional Unicode characters
 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) plt.show()
Last active January 7, 2020 02:54
positive polynomial optimization + taylor model sketch idea
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters. Learn more about bidirectional Unicode characters
 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.
Last active January 25, 2020 19:36
z3py relation algebra sketch
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters. Learn more about bidirectional Unicode characters
 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)