mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-02-16 22:01:44 +00:00
Code Activity

Document example for Solver.sexpr()

Browse source
This commit is contained in:
Daniel Tang 2026-02-14 21:51:21 -05:00
parent e2486eff77
commit 114a325cd4
No known key found for this signature in database
GPG key ID: E1523803636E3951
1 changed files with 5 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/api/python/z3/z3.py
View file

@ -7657,7 +7657,11 @@ class Solver(Z3PPObject):
>>> s = Solver()
>>> s.add(x > 0)
>>> s.add(x < 2)
>>> r = s.sexpr()
>>> print(s.sexpr())
(declare-fun x () Int)
(assert (> x 0))
(assert (< x 2))
"""
return Z3_solver_to_string(self.ctx.ref(), self.solver)