From 99861ffc3296637e60cda392903b7f4277c9d196 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 7 May 2015 21:32:02 -0700 Subject: [PATCH] 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: