From dc95f6d0186eaafd5dd6f53a6fbec33ea8694769 Mon Sep 17 00:00:00 2001
From: a <a@a.a>
Date: Thu, 9 May 2024 21:28:02 +0200
Subject: [PATCH] fix benchmarks

---
 examples/prove.jl | 35 +++++++++++++++++++++++++++++++++++
 1 file changed, 35 insertions(+)
 create mode 100644 examples/prove.jl

diff --git a/examples/prove.jl b/examples/prove.jl
new file mode 100644
index 00000000..df9a5859
--- /dev/null
+++ b/examples/prove.jl
@@ -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
+