mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

reset backtrack level at each cube

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-11-09 10:04:32 -08:00
parent ee3ed3a27a
commit cb7e53aae4
2 changed files with 6 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/api/dotnet/Solver.cs
View file

@ -364,9 +364,10 @@ namespace Microsoft.Z3
/// </summary> /// </summary>
public IEnumerable<BoolExpr> Cube() public IEnumerable<BoolExpr> Cube()
{ {
int rounds = 0;
while (true) { while (true) {
BoolExpr r = (BoolExpr)Expr.Create(Context, Native.Z3_solver_cube(Context.nCtx, NativeObject, BacktrackLevel)); var lvl = BacktrackLevel;
BacktrackLevel = uint.MaxValue;
BoolExpr r = (BoolExpr)Expr.Create(Context, Native.Z3_solver_cube(Context.nCtx, NativeObject, lvl));
if (r.IsFalse) { if (r.IsFalse) {
break; break;
} }
@ -374,7 +375,6 @@ namespace Microsoft.Z3
yield return r; yield return r;
break; break;
} }
++rounds;
yield return r; yield return r;
} }
} }

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

@ -6287,7 +6287,9 @@ class Solver(Z3PPObject):
def cube(self): def cube(self):
"""Get set of cubes""" """Get set of cubes"""
while True: while True:
r = _to_expr_ref(Z3_solver_cube(self.ctx.ref(), self.solver, self.backtrack_level), self.ctx) lvl = self.backtrack_level
self.backtrack_level = 4000000000
r = _to_expr_ref(Z3_solver_cube(self.ctx.ref(), self.solver, lvl), self.ctx)
if (is_false(r)): if (is_false(r)):
return return
if (is_true(r)): if (is_true(r)):