From e881c4af3fbf8141604e1cce24fca05e73ae0992 Mon Sep 17 00:00:00 2001 From: Arie Gurfinkel Date: Sat, 7 Sep 2019 16:59:51 +0300 Subject: [PATCH] Support repr_html for jupyter --- src/api/python/z3/z3.py | 15 +++++++++++++++ 1 file changed, 15 insertions(+) diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index f8df8f003..3d77b9ed9 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -296,6 +296,14 @@ class Z3PPObject: def use_pp(self): return True + def _repr_html_(self): + in_html = in_html_mode() + set_html_mode(True) + res = repr(self) + set_html_mode(in_html) + return res + + class AstRef(Z3PPObject): """AST are Direct Acyclic Graphs (DAGs) used to represent sorts, declarations and expressions.""" def __init__(self, ast, ctx=None): @@ -6418,6 +6426,13 @@ class CheckSatResult: else: return "unknown" + def _repr_html_(self): + in_html = in_html_mode() + set_html_mode(True) + res = repr(self) + set_html_mode(in_html) + return res + sat = CheckSatResult(Z3_L_TRUE) unsat = CheckSatResult(Z3_L_FALSE) unknown = CheckSatResult(Z3_L_UNDEF)