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 after first backtrack

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-11-08 22:14:59 -08:00
parent 75b8d10f48
commit bc8681a0ea
2 changed files with 4 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -5988,6 +5988,7 @@ class Solver(Z3PPObject):
def __init__(self, solver=None, ctx=None): def __init__(self, solver=None, ctx=None):
assert solver is None or ctx is not None assert solver is None or ctx is not None
self.ctx = _get_ctx(ctx) self.ctx = _get_ctx(ctx)
self.backtrack_level = 4000000000
self.solver = None self.solver = None
if solver is None: if solver is None:
self.solver = Z3_mk_solver(self.ctx.ref()) self.solver = Z3_mk_solver(self.ctx.ref())
@ -6283,11 +6284,10 @@ class Solver(Z3PPObject):
consequences = [ consequences[i] for i in range(sz) ] consequences = [ consequences[i] for i in range(sz) ]
return CheckSatResult(r), consequences return CheckSatResult(r), consequences
def cube(self, level_ref): def cube(self):
"""Get set of cubes""" """Get set of cubes"""
while True: while True:
backtrack_level = level_ref.backtrack_level r = _to_expr_ref(Z3_solver_cube(self.ctx.ref(), self.solver, self.backtrack_level), self.ctx)
r = _to_expr_ref(Z3_solver_cube(self.ctx.ref(), self.solver, backtrack_level), self.ctx)
if (is_false(r)): if (is_false(r)):
return return
if (is_true(r)): if (is_true(r)):

2
src/sat/sat_lookahead.cpp
View file

@ -2012,8 +2012,8 @@ namespace sat {
set_conflict(); set_conflict();
backtrack(m_cube_state.m_cube, m_cube_state.m_is_decision); backtrack(m_cube_state.m_cube, m_cube_state.m_is_decision);
} }
backtrack_level = UINT_MAX;
} }
backtrack_level = UINT_MAX;
depth = m_cube_state.m_cube.size(); depth = m_cube_state.m_cube.size();
if ((m_config.m_cube_cutoff != 0 && depth == m_config.m_cube_cutoff) || if ((m_config.m_cube_cutoff != 0 && depth == m_config.m_cube_cutoff) ||
(m_config.m_cube_cutoff == 0 && m_freevars.size() < m_cube_state.m_freevars_threshold)) { (m_config.m_cube_cutoff == 0 && m_freevars.size() < m_cube_state.m_freevars_threshold)) {