philzook58

def modelValue (ce : CounterExample) (x : Expr) : MetaM Expr := do
  for (lhs, v) in ce.equations do
    if ← isDefEq lhs x then return toExpr v.bv
    match_expr lhs with
    | BitVec.ofBool y =>
        if ← isDefEq y x then return toExpr (v.bv == 1)
    | _ =>
        match lhs with
        | .app (.const (.str typeName suffix) levels) y =>
            if suffix == Normalize.enumToBitVecSuffix && (← isDefEq y x) then

philzook58

import kdrag as kd
import kdrag.smt as smt
import kdrag.theories.logic.zf as zf

Set = zf.ZFSet

A, B, R, x, y, z = smt.Consts("A B R x y z", Set)
a, b, c, p = kd.FreshVars("a b c p", Set)

elem = zf.elem

philzook58

import kdrag as kd
import kdrag.smt as smt
import kdrag.theories.logic.zf as zf

Set = zf.ZFSet

A, B, R, x, y, z = smt.Consts("A B R x y z", Set)
a, b, c, p = kd.FreshVars("a b c p", Set)

elem = zf.elem

philzook58

from dataclasses import dataclass, field


@dataclass(frozen=True)
class Slot:
    name: int

    def __repr__(self):
        return f"${self.name}"

philzook58

from kdrag.parsers.sexp import parse
import operator
import functools
import numpy as np
parse("(+ 1 2 3 4)")

def expr(env, sexp):
    match sexp:
        case int() | float():
            return sexp

philzook58

l = kd.Lemma(smt.ForAll([x,y], add(x, y) == add(y, x)))
x1,y1 = l.intros()
l.induct(x1)
l.auto(by=[add.defn, add_Z_r])
z1 = l.fixes()
l.auto(by=[add.defn, add_s_r])
add_comm = l.qed()

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)