From 2997684fdd7f5e15d7273ff6d3cf9b9c3ed60e42 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Henrik=20B=C3=B6ving?= <hargonix@gmail.com>
Date: Wed, 6 Nov 2024 10:13:05 +0100
Subject: [PATCH] test: basic regression tests for the sexp parser

---
 Test/Sexp.lean | 33 +++++++++++++++++++++++++++++++++
 1 file changed, 33 insertions(+)
 create mode 100644 Test/Sexp.lean

diff --git a/Test/Sexp.lean b/Test/Sexp.lean
new file mode 100644
index 0000000..48b9061
--- /dev/null
+++ b/Test/Sexp.lean
@@ -0,0 +1,33 @@
+/-
+Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Henrik Böving
+-/
+import Leanwuzla
+import Leanwuzla.Sexp
+
+open Std.Tactic.BVDecide
+
+def expr1 : BVLogicalExpr := .const true
+
+/-- info: true -/
+#guard_msgs in
+#eval Sexp.Parser.manySexps! |>.run (Lean.Elab.Tactic.BVDecide.Frontend.toSMT expr1 {}) |>.isOk
+
+def expr2 : BVLogicalExpr := .not (.const true)
+
+/-- info: true -/
+#guard_msgs in
+#eval Sexp.Parser.manySexps! |>.run (Lean.Elab.Tactic.BVDecide.Frontend.toSMT expr2 {}) |>.isOk
+
+def expr3 : BVLogicalExpr := .gate .and (.const true) (.const false)
+
+/-- info: true -/
+#guard_msgs in
+#eval Sexp.Parser.manySexps! |>.run (Lean.Elab.Tactic.BVDecide.Frontend.toSMT expr3 {}) |>.isOk
+
+def expr4 : BVLogicalExpr := .literal (.bin (.const 10#32) .eq (.const 11#32))
+
+/-- info: true -/
+#guard_msgs in
+#eval Sexp.Parser.manySexps! |>.run (Lean.Elab.Tactic.BVDecide.Frontend.toSMT expr4 {}) |>.isOk