From 0e45777104e6da51ca717d1950bd8cbb72657857 Mon Sep 17 00:00:00 2001 From: Jack Feser Date: Tue, 11 Jul 2017 14:41:54 -0400 Subject: [PATCH] add get_num_scopes to python solver api --- src/api/python/z3/z3.py | 18 ++++++++++++++++++ 1 file changed, 18 insertions(+) diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index 9a1ebccf6..a16c1b92b 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -6054,6 +6054,24 @@ class Solver(Z3PPObject): """ Z3_solver_pop(self.ctx.ref(), self.solver, num) + def num_scopes(self): + """Return the current number of backtracking points. + + >>> s = Solver() + >>> s.num_scopes() + 0L + >>> s.push() + >>> s.num_scopes() + 1L + >>> s.push() + >>> s.num_scopes() + 2L + >>> s.pop() + >>> s.num_scopes() + 1L + """ + return Z3_solver_get_num_scopes(self.ctx.ref(), self.solver) + def reset(self): """Remove all asserted constraints and backtracking points created using `push()`.