mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-27 00:18:45 +00:00
Code Activity

remove stale API #7648

Browse source
This commit is contained in:
Nikolaj Bjorner 2025-05-15 10:55:47 -07:00
parent 0b26f7e0ee
commit 7ebe7c46b9
1 changed files with 0 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -7394,11 +7394,6 @@ class Solver(Z3PPObject):
b = _py2expr(b, self.ctx) b = _py2expr(b, self.ctx)
return _to_expr_ref(Z3_solver_congruence_explain(self.ctx.ref(), self.solver, a.ast, b.ast), self.ctx) return _to_expr_ref(Z3_solver_congruence_explain(self.ctx.ref(), self.solver, a.ast, b.ast), self.ctx)
def solve_for1(self, t):
"""Retrieve a solution for t relative to linear equations maintained in the current state.
The function primarily works for SimpleSolver and when there is a solution using linear arithmetic."""
t = _py2expr(t, self.ctx)
return _to_expr_ref(Z3_solver_solve_for1(self.ctx.ref(), self.solver, t.ast), self.ctx)
def solve_for(self, ts): def solve_for(self, ts):
"""Retrieve a solution for t relative to linear equations maintained in the current state.""" """Retrieve a solution for t relative to linear equations maintained in the current state."""