From 530212df79a3466afd8951751f2b1c5867b360f0 Mon Sep 17 00:00:00 2001 From: Yoni Zohar Date: Thu, 6 Jun 2024 09:48:41 +0300 Subject: [PATCH 1/2] nullary and unary ands and ors --- cvc5_pythonic_api/cvc5_pythonic.py | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) diff --git a/cvc5_pythonic_api/cvc5_pythonic.py b/cvc5_pythonic_api/cvc5_pythonic.py index bae370f..d9b1822 100644 --- a/cvc5_pythonic_api/cvc5_pythonic.py +++ b/cvc5_pythonic_api/cvc5_pythonic.py @@ -1716,7 +1716,15 @@ def And(*args): >>> P = BoolVector('p', 5) >>> And(P) And(p__0, p__1, p__2, p__3, p__4) + >>> And() + True + >>> And(p) + p """ + if len(args) == 0: + return True + if len(args) == 1: + return args[0] return _nary_kind_builder(Kind.AND, *args) @@ -1731,7 +1739,15 @@ def Or(*args): >>> P = BoolVector('p', 5) >>> Or(P) Or(p__0, p__1, p__2, p__3, p__4) + >>> Or() + False + >>> Or(p) + p """ + if len(args) == 0: + return False + if len(args) == 1: + return args[0] return _nary_kind_builder(Kind.OR, *args) From e97fb03d31dc07f8791d0e297b52f508c335c450 Mon Sep 17 00:00:00 2001 From: Yoni Zohar Date: Thu, 6 Jun 2024 10:13:25 +0300 Subject: [PATCH 2/2] fix --- cvc5_pythonic_api/cvc5_pythonic.py | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/cvc5_pythonic_api/cvc5_pythonic.py b/cvc5_pythonic_api/cvc5_pythonic.py index d9b1822..a708ffa 100644 --- a/cvc5_pythonic_api/cvc5_pythonic.py +++ b/cvc5_pythonic_api/cvc5_pythonic.py @@ -1723,7 +1723,7 @@ def And(*args): """ if len(args) == 0: return True - if len(args) == 1: + if len(args) == 1 and type(args[0]) is not list: return args[0] return _nary_kind_builder(Kind.AND, *args) @@ -1746,7 +1746,7 @@ def Or(*args): """ if len(args) == 0: return False - if len(args) == 1: + if len(args) == 1 and type(args[0]) is not list: return args[0] return _nary_kind_builder(Kind.OR, *args)