mirror of
https://github.com/Z3Prover/z3
synced 2025-04-06 09:34:08 +00:00
Support repr_html for jupyter
This commit is contained in:
parent
228d68f165
commit
e881c4af3f
|
@ -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)
|
||||
|
|
Loading…
Reference in a new issue