From 99861ffc3296637e60cda392903b7f4277c9d196 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 7 May 2015 21:32:02 -0700 Subject: [PATCH 1/4] allow coercion from Boolean to Integers and reals Signed-off-by: Nikolaj Bjorner --- src/api/python/z3.py | 13 +++++++++++++ 1 file changed, 13 insertions(+) diff --git a/src/api/python/z3.py b/src/api/python/z3.py index ce1cc2103..92640b2d9 100644 --- a/src/api/python/z3.py +++ b/src/api/python/z3.py @@ -1228,6 +1228,15 @@ class BoolSortRef(SortRef): _z3_assert(self.eq(val.sort()), "Value cannot be converted into a Z3 Boolean value") return val + def subsort(self, other): + return isinstance(other, ArithSortRef) + + def is_int(self): + return True + + def is_bool(self): + return True + class BoolRef(ExprRef): """All Boolean expressions are instances of this class.""" def sort(self): @@ -1900,6 +1909,10 @@ class ArithSortRef(SortRef): return val if val_s.is_int() and self.is_real(): return ToReal(val) + if val_s.is_bool() and self.is_int(): + return If(val, 1, 0) + if val_s.is_bool() and self.is_real(): + return ToReal(If(val, 1, 0)) if __debug__: _z3_assert(False, "Z3 Integer/Real expression expected" ) else: From 45eda4bee78c3e95cbdfbc71e8aa27b967639ab9 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 7 May 2015 21:33:36 -0700 Subject: [PATCH 2/4] allow coercion from Boolean to Int/Real, fixes #78 Signed-off-by: Nikolaj Bjorner --- src/api/python/z3.py | 1 + 1 file changed, 1 insertion(+) diff --git a/src/api/python/z3.py b/src/api/python/z3.py index 92640b2d9..7cda4bf83 100644 --- a/src/api/python/z3.py +++ b/src/api/python/z3.py @@ -1237,6 +1237,7 @@ class BoolSortRef(SortRef): def is_bool(self): return True + class BoolRef(ExprRef): """All Boolean expressions are instances of this class.""" def sort(self): From ad39811dc0a9ebd11b62b59693142a5c9518d6f9 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 7 May 2015 21:36:37 -0700 Subject: [PATCH 3/4] allow coercion from Boolean to Int/Real, fixes #78 Signed-off-by: Nikolaj Bjorner --- src/api/python/z3.py | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/src/api/python/z3.py b/src/api/python/z3.py index 7cda4bf83..c1bdf2713 100644 --- a/src/api/python/z3.py +++ b/src/api/python/z3.py @@ -1229,13 +1229,13 @@ class BoolSortRef(SortRef): return val def subsort(self, other): - return isinstance(other, ArithSortRef) + return isinstance(other, ArithSortRef) def is_int(self): - return True + return True def is_bool(self): - return True + return True class BoolRef(ExprRef): @@ -1910,10 +1910,10 @@ class ArithSortRef(SortRef): return val if val_s.is_int() and self.is_real(): return ToReal(val) - if val_s.is_bool() and self.is_int(): - return If(val, 1, 0) - if val_s.is_bool() and self.is_real(): - return ToReal(If(val, 1, 0)) + if val_s.is_bool() and self.is_int(): + return If(val, 1, 0) + if val_s.is_bool() and self.is_real(): + return ToReal(If(val, 1, 0)) if __debug__: _z3_assert(False, "Z3 Integer/Real expression expected" ) else: From 901d8a9f5b8d623982fd90caa3a0ff65026c4192 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 8 May 2015 00:38:26 -0700 Subject: [PATCH 4/4] change exception test to take into account new coercion operation Signed-off-by: Nikolaj Bjorner --- src/api/python/z3.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/api/python/z3.py b/src/api/python/z3.py index c1bdf2713..b46f5a9ef 100644 --- a/src/api/python/z3.py +++ b/src/api/python/z3.py @@ -32,7 +32,7 @@ sat Z3 exceptions: >>> try: -... x = Int('x') +... x = BitVec('x', 32) ... y = Bool('y') ... # the expression x + y is type incorrect ... n = x + y