Skip to content

Instantly share code, notes, and snippets.

Created April 10, 2022 02:14
What would you like to do?
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)
axioms = [
ForAll([x,y], add(x,y) == add(y,x)),
ForAll([x,y,z], add(add(x,y),z) == add(x,add(y,z)))
import timeit
for N in range(5,17):
s = Solver()
e1 = reduce(add, [num(n) for n in range(N)])
perm = list(range(N))
e2 = reduce(add, [num(n) for n in perm])
s.add(e1 != e2)
print(N, timeit.timeit(lambda: s.check(), number = 1))
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment