From 5e8b01760346f07d3d4ce092f97c9fc6197db639 Mon Sep 17 00:00:00 2001
From: Haniel Barbosa <hanielbbarbosa@gmail.com>
Date: Mon, 24 Jun 2024 15:52:40 +0200
Subject: [PATCH 1/4] print support for SEXPR

---
 cvc5_pythonic_api/cvc5_pythonic_printer.py | 13 +++++++++++++
 1 file changed, 13 insertions(+)

diff --git a/cvc5_pythonic_api/cvc5_pythonic_printer.py b/cvc5_pythonic_api/cvc5_pythonic_printer.py
index a8429d7..4cd113e 100644
--- a/cvc5_pythonic_api/cvc5_pythonic_printer.py
+++ b/cvc5_pythonic_api/cvc5_pythonic_printer.py
@@ -1080,6 +1080,17 @@ def pp_select(self, a, d, xs):
                 arg1_pp, indent(2, compose(to_format("["), arg2_pp, to_format("]")))
             )
 
+    def pp_sexpr(self, a, d, xs):
+        r = []
+        sz = 0
+        for child in a.children():
+            r.append(self.pp_expr(child, d + 1, xs))
+            sz = sz + 1
+            if sz > self.max_args:
+                r.append(self.pp_ellipses())
+                break
+        return seq3(r)
+
     def pp_unary_param(self, a, d, xs, param_on_right):
         p = a.ast.getOp()[0].toPythonObj()
         arg = self.pp_expr(a.arg(0), d + 1, xs)
@@ -1194,6 +1205,8 @@ def pp_app(self, a, d, xs):
                 return self.pp_uf_apply(a, d, xs)
             elif k in [Kind.APPLY_CONSTRUCTOR, Kind.APPLY_SELECTOR, Kind.APPLY_TESTER]:
                 return self.pp_dt_apply(a, d, xs)
+            elif k == Kind.SEXPR:
+                return self.pp_sexpr(a, d, xs)
             else:
                 return self.pp_prefix(a, d, xs)
 

From 4d4487b809ca30d4f6a708a7a7c0cfc944039b23 Mon Sep 17 00:00:00 2001
From: Haniel Barbosa <hanielbbarbosa@gmail.com>
Date: Mon, 24 Jun 2024 22:33:35 +0200
Subject: [PATCH 2/4] address review

---
 cvc5_pythonic_api/cvc5_pythonic.py         | 9 +++++++++
 cvc5_pythonic_api/cvc5_pythonic_printer.py | 2 +-
 test/pgm_outputs/example_sexpr.py.out      | 1 +
 test/pgms/example_sexpr.py                 | 5 +++++
 4 files changed, 16 insertions(+), 1 deletion(-)
 create mode 100644 test/pgm_outputs/example_sexpr.py.out
 create mode 100644 test/pgms/example_sexpr.py

diff --git a/cvc5_pythonic_api/cvc5_pythonic.py b/cvc5_pythonic_api/cvc5_pythonic.py
index bae370f..0b2356e 100644
--- a/cvc5_pythonic_api/cvc5_pythonic.py
+++ b/cvc5_pythonic_api/cvc5_pythonic.py
@@ -1312,6 +1312,15 @@ def FreshConst(sort, prefix="c"):
     return Const(name, sort)
 
 
+def Sexpr(*args):
+    """Create an SEXPR term.
+
+    >>> p, q, r = Bools('p q r')
+    >>> Sexpr(p, q, r)
+    (p q r)
+    """
+    return _nary_kind_builder(Kind.SEXPR, *args)
+
 #########################################
 #
 # Booleans
diff --git a/cvc5_pythonic_api/cvc5_pythonic_printer.py b/cvc5_pythonic_api/cvc5_pythonic_printer.py
index 4cd113e..ff5db65 100644
--- a/cvc5_pythonic_api/cvc5_pythonic_printer.py
+++ b/cvc5_pythonic_api/cvc5_pythonic_printer.py
@@ -1089,7 +1089,7 @@ def pp_sexpr(self, a, d, xs):
             if sz > self.max_args:
                 r.append(self.pp_ellipses())
                 break
-        return seq3(r)
+        return group(indent(len("("), compose(to_format("("), seq(r, " ", False), to_format(")"))))
 
     def pp_unary_param(self, a, d, xs, param_on_right):
         p = a.ast.getOp()[0].toPythonObj()
diff --git a/test/pgm_outputs/example_sexpr.py.out b/test/pgm_outputs/example_sexpr.py.out
new file mode 100644
index 0000000..8bf6886
--- /dev/null
+++ b/test/pgm_outputs/example_sexpr.py.out
@@ -0,0 +1 @@
+(x y z)
\ No newline at end of file
diff --git a/test/pgms/example_sexpr.py b/test/pgms/example_sexpr.py
new file mode 100644
index 0000000..9fc816c
--- /dev/null
+++ b/test/pgms/example_sexpr.py
@@ -0,0 +1,5 @@
+from cvc5_pythonic_api import *
+x = Int("x")
+y = Int("y")
+z = Int("z")
+print(Sexpr(x, y, z))

From a853a8e637f10696ca3adfc376d947e79ad21132 Mon Sep 17 00:00:00 2001
From: Haniel Barbosa <hanielbbarbosa@gmail.com>
Date: Mon, 24 Jun 2024 22:35:03 +0200
Subject: [PATCH 3/4] format

---
 cvc5_pythonic_api/cvc5_pythonic.py         | 1 +
 cvc5_pythonic_api/cvc5_pythonic_printer.py | 6 +++++-
 2 files changed, 6 insertions(+), 1 deletion(-)

diff --git a/cvc5_pythonic_api/cvc5_pythonic.py b/cvc5_pythonic_api/cvc5_pythonic.py
index 0b2356e..163eb1e 100644
--- a/cvc5_pythonic_api/cvc5_pythonic.py
+++ b/cvc5_pythonic_api/cvc5_pythonic.py
@@ -1321,6 +1321,7 @@ def Sexpr(*args):
     """
     return _nary_kind_builder(Kind.SEXPR, *args)
 
+
 #########################################
 #
 # Booleans
diff --git a/cvc5_pythonic_api/cvc5_pythonic_printer.py b/cvc5_pythonic_api/cvc5_pythonic_printer.py
index ff5db65..d198c36 100644
--- a/cvc5_pythonic_api/cvc5_pythonic_printer.py
+++ b/cvc5_pythonic_api/cvc5_pythonic_printer.py
@@ -1089,7 +1089,11 @@ def pp_sexpr(self, a, d, xs):
             if sz > self.max_args:
                 r.append(self.pp_ellipses())
                 break
-        return group(indent(len("("), compose(to_format("("), seq(r, " ", False), to_format(")"))))
+        return group(
+            indent(
+                len("("), compose(to_format("("), seq(r, " ", False), to_format(")"))
+            )
+        )
 
     def pp_unary_param(self, a, d, xs, param_on_right):
         p = a.ast.getOp()[0].toPythonObj()

From 1fc8dc44f2201796dff67cbc580854910375a009 Mon Sep 17 00:00:00 2001
From: Haniel Barbosa <hanielbbarbosa@gmail.com>
Date: Mon, 24 Jun 2024 22:51:12 +0200
Subject: [PATCH 4/4] fix

---
 test/pgm_outputs/example_sexpr.py.out | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/test/pgm_outputs/example_sexpr.py.out b/test/pgm_outputs/example_sexpr.py.out
index 8bf6886..9c99543 100644
--- a/test/pgm_outputs/example_sexpr.py.out
+++ b/test/pgm_outputs/example_sexpr.py.out
@@ -1 +1 @@
-(x y z)
\ No newline at end of file
+(x y z)