diff --git a/cvc5_pythonic_api/cvc5_pythonic.py b/cvc5_pythonic_api/cvc5_pythonic.py index bae370f..163eb1e 100644 --- a/cvc5_pythonic_api/cvc5_pythonic.py +++ b/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 diff --git a/cvc5_pythonic_api/cvc5_pythonic_printer.py b/cvc5_pythonic_api/cvc5_pythonic_printer.py index a8429d7..d198c36 100644 --- a/cvc5_pythonic_api/cvc5_pythonic_printer.py +++ b/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) diff --git a/test/pgm_outputs/example_sexpr.py.out b/test/pgm_outputs/example_sexpr.py.out new file mode 100644 index 0000000..9c99543 --- /dev/null +++ b/test/pgm_outputs/example_sexpr.py.out @@ -0,0 +1 @@ +(x y z) 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))