philzook58

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()

philzook58

import re

# \s* is whitespace follow by digits or symbol or ( or )
token_pattern = re.compile(r"\s*(?:(\d+)|([A-Za-z\-!=\+\*\_<>]+[A-Za-z0-9\-!=\+\*\_<>]*)|(\()|(\)))")

def tokenize(s):
    for match in token_pattern.finditer(s):
        yield match.groups()

def parse_expression(iterator):

philzook58

CREATE TABLE tc(a INTEGER, b INTEGER, PRIMARY KEY (a,b)); 

INSERT OR IGNORE INTO tc(a,b)
VALUES (1,2),(2,3),(3,4); 

-- repeat this query many times for naive iteration
-- path(x,z) :- path(x,y), path(y,z).
INSERT OR IGNORE INTO tc SELECT DISTINCT tc0.a, tc1.b   -- the head of the rule gives the insert and select fields  
FROM tc as tc0, tc as tc1
WHERE tc0.b = tc1.a; -- The body of the rule gives FROM and WHERE 

philzook58

Computing weakest precondition of Imp programs directly in Z3. Requires reflection of smtlib expressions into expression datatypes and representing the variable store as an array. In principle, smtlib is it's own macro system.

Typically people use python or some other language to generate smtlib. Boogie and Why3 are frameworks that generate smtlib (among other things) from imperative code. We can remove one level of indirection by directly programming in Z3. There are so many other good abstractions that smtlib is just barely able to express in this style.

philzook58

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)

philzook58

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

philzook58

yada yada ayda

/**
     * Returns unionfind parent of Node
     * @param x
     */
    value_type findNode(value_type x) const {
        return sds.findNode(x);
    }

philzook58

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

(executable
(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

(*|

I had a fun time giving a Z3 tutorial at Formal Methods for the Informal Engineer (FMIE) https://fmie2021.github.io/ (videos coming soon hopefully!). I got to be kind of the "fun dad" with the Z3 tutorial https://github.com/philzook58/z3_tutorial , while at times it felt a bit like Cody's Coq tutorial https://github.com/codyroux/broad-coq-tutorial was trying to feed the kids their vegetables. He knew it was going to be like this from the outset and had a fun little analogy of me downhill skiing while he was about to go on a cross country slog.

There are a number of factors to this. 
* I could use Z3's python bindings giving an air of familiarity, whereas everything was incredibly foreign in Coq.
* Z3 can actually be used to declaratively state problems and automatically calculate solutions to them with very little user help, which gives it a lot more "Wow" factor.
* Coq is a tool that requires significantly more background to even comprehend what the hell it is. I still think many aspects of it are tota