Skip to content

Commit

Permalink
fix benchmarks
Browse files Browse the repository at this point in the history
  • Loading branch information
a committed May 9, 2024
1 parent aa38d76 commit dc95f6d
Showing 1 changed file with 35 additions and 0 deletions.
35 changes: 35 additions & 0 deletions examples/prove.jl
Original file line number Diff line number Diff line change
@@ -0,0 +1,35 @@
# TODO: should this go in MT itself?
# Sketch function for basic iterative saturation and extraction
function prove(
t,
ex,
steps = 1,
timeout = 10,
params = SaturationParams(
timeout = timeout,
scheduler = Schedulers.BackoffScheduler,
schedulerparams = (6000, 5),
timer = false,
),
)
hist = UInt64[]
push!(hist, hash(ex))
for i in 1:steps
g = EGraph(ex)

ids = [addexpr!(g, true), g.root]

params.goal = (g::EGraph) -> in_same_class(g, ids...)
saturate!(g, t, params)
ex = extract!(g, astsize)
if !TermInterface.isexpr(ex)
return ex
end
if hash(ex) hist
return ex
end
push!(hist, hash(ex))
end
return ex
end

0 comments on commit dc95f6d

Please sign in to comment.