Print support for SEXPR (#97)

Author: HanielB

cvc5_pythonic_api/cvc5_pythonic.py

@@ -1312,6 +1312,16 @@ 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

cvc5_pythonic_api/cvc5_pythonic_printer.py

@@ -1080,6 +1080,21 @@ 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 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()
         arg = self.pp_expr(a.arg(0), d + 1, xs)
@@ -1194,6 +1209,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)
 

test/pgm_outputs/example_sexpr.py.out

@@ -0,0 +1 @@
+(x y z)

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))