Skip to content

Instantly share code, notes, and snippets.


Philip Zucker philzook58

View GitHub Profile
philzook58 /
Created Apr 10, 2022
Z3 on uninterpreted commutative
from z3 import *
Num = DeclareSort("Num")
add = Function("add", Num, Num, Num)
num = Function("num", IntSort(), Num)
from functools import reduce
import random
print(reduce(add, [num(n) for n in range(10)]))
x,y,z = Consts("x y z", Num)

Scoped union find

Max has put forward that we need different union finds floating around indexed in some way

A more complex union find structure seems like it could be useful. We might want a fully non destructive union find. Another option is a "scoped union find". Scopes form a forest. Deeper scopes get the subsequent unions of their ancestor scopes, but not vice versa. Scopes form a partially ordered set.

Options of multiple related union finds:

  1. The fillaitre conchon persistent union find has an angle where you really only have one union find active at a time.
  2. Using functional maps to implement union find rather than imperative arrays or refs. You don't get path compression? How important is that really? ln(n) vs inverse_ack(n) both feel close to constant.
  3. just copy entire union find every time you need a new one. Updates to higher union finds don't immediately propagate to lower ones for good or bad

Compile the library. I got the various build arguments from souffle-compile. You can also run this in interpreter mode.

../../souffle/build/src/souffle add2.dl -lunionfind -o out -j4
time ./out -j4
philzook58 / EquivalenceRelation.h
Last active Mar 4, 2022
souffle findNode functor
View EquivalenceRelation.h
yada yada ayda
* Returns unionfind parent of Node
* @param x
value_type findNode(value_type x) const {
return sds.findNode(x);
philzook58 / dune
Last active Jan 6, 2022
primus lisp programmatic loading in bap
View dune
(name main)
;(modes byte js)
(flags -linkall -g)
; with dune build main.bc.js --release
; gets us to the Sys flushed error.
(js_of_ocaml (flags --toplevel --dynlink +toplevel.js +dynlink.js --disable inline --pretty --source-map-inline
--file /home/philip/.opam/bapjs/lib/bap/bil.plugin
--file /home/philip/.opam/bapjs/lib/bap/primus_lisp.plugin
--file /home/philip/Documents/ocaml/bapjs2/staticload/test.lisp
philzook58 /
Last active Jan 1, 2022
js_of_ocaml custom directory
dune build main.bc.js --release
node _build/default/main.bc.js


$node _build/default/main.bc.js
 {r += exn[1][1];
philzook58 /
Last active Dec 31, 2021
Bap Stack overflow error in js_of_ocaml

Build with dune build main.bc.js --release Demonstrates stack overflow on dynlinking the bap_c library.

Troubleshooting is difficult. Unfortunately the overflow error is being caught and translated in a way that obscures the original cause. To find what I believe is an accurate stack trace do the following: Go into _build/default/main.bc.js. Add Error.stackTraceLimit = Infinity; to the top. Grep for RangeError. Add in console.log(e.stack); into the exception handler like so

     {if(e instanceof Array)return e;
philzook58 /
Created Nov 5, 2021
Attempting to js_of_ocaml bap
ocamlfind ocamlc -package bap -package core_kernel -linkpkg -linkall
js_of_ocaml +dynlink.js +toplevel.js +zarith_stubs_js/runtime.js +zarith_stubs_js/biginteger.js \
+base/base_internalhash_types/runtime.js +base/runtime.js +time_now/runtime.js +bin_prot/runtime.js \
+ppx_expect/collector/runtime.js +base_bigstring/runtime.js +core_kernel/strftime.js +core_kernel/runtime.js \
+bigstringaf/runtime.js --linkall --extern-fs --toplevel a.out
open Core_kernel
open Bap.Std
View exmaple.c
#include <stdlib.h>
#include <stdio.h>
#include <string.h>
#include <time.h>
#define FLAG_BUFFER 128
#define MAX_SYM_LEN 4
typedef struct Stonks {
int shares;
philzook58 /
Created May 22, 2021
A Kanren abusing Z3 to full extent
import operator
from z3 import *
def lift(z3assert):
def res(s):
if s.is_good():