mirror of
https://github.com/Z3Prover/z3
synced 2026-02-16 22:01:44 +00:00
remove brittle pydoc example
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
249b59f42c
commit
e87cf5ad2b
1 changed files with 0 additions and 11 deletions
|
|
@ -7662,17 +7662,6 @@ class Solver(Z3PPObject):
|
|||
|
||||
def sexpr(self):
|
||||
"""Return a formatted string (in Lisp-like format) with all added constraints.
|
||||
We say the string is in s-expression format.
|
||||
|
||||
>>> x = Int('x')
|
||||
>>> s = Solver()
|
||||
>>> s.add(x > 0)
|
||||
>>> s.add(x < 2)
|
||||
>>> print(s.sexpr())
|
||||
(declare-fun x () Int)
|
||||
(assert (> x 0))
|
||||
(assert (< x 2))
|
||||
|
||||
"""
|
||||
return Z3_solver_to_string(self.ctx.ref(), self.solver)
|
||||
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue