mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 09:35:32 +00:00
Code Activity

add backtrack level to cuber interface

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-11-08 21:44:21 -08:00
parent 0a9946578b
commit 75b8d10f48
22 changed files with 53 additions and 40 deletions
Download patch file Download diff file Expand all files Collapse all files

10
src/sat/ba_solver.cpp
View file

@ -349,7 +349,7 @@ namespace sat {
}
bool nullify = p.lit() != null_literal && value(p.lit()) == l_true;
if (nullify) {
IF_VERBOSE(10, display(verbose_stream() << "nullify tracking literal\n", p, true););
IF_VERBOSE(100, display(verbose_stream() << "nullify tracking literal\n", p, true););
SASSERT(lvl(p.lit()) == 0);
nullify_tracking_literal(p);
init_watch(p, true);
@ -374,7 +374,7 @@ namespace sat {
if (p.k() == 1 && p.lit() == null_literal) {
literal_vector lits(p.literals());
s().mk_clause(lits.size(), lits.c_ptr(), p.learned());
IF_VERBOSE(10, display(verbose_stream() << "add clause: " << lits << "\n", p, true););
IF_VERBOSE(100, display(verbose_stream() << "add clause: " << lits << "\n", p, true););
remove_constraint(p, "implies clause");
}
else if (true_val == 0 && num_false == 0) {
@ -384,14 +384,14 @@ namespace sat {
}
else if (true_val >= p.k()) {
if (p.lit() != null_literal) {
IF_VERBOSE(10, display(verbose_stream() << "assign true literal ", p, true););
IF_VERBOSE(100, display(verbose_stream() << "assign true literal ", p, true););
s().assign(p.lit(), justification());
}
remove_constraint(p, "is true");
}
else if (slack + true_val < p.k()) {
if (p.lit() != null_literal) {
IF_VERBOSE(10, display(verbose_stream() << "assign false literal ", p, true););
IF_VERBOSE(100, display(verbose_stream() << "assign false literal ", p, true););
s().assign(~p.lit(), justification());
}
else {
@ -2877,7 +2877,7 @@ namespace sat {
bool ba_solver::elim_pure(literal lit) {
if (value(lit) == l_undef && !m_cnstr_use_list[lit.index()].empty() &&
use_count(~lit) == 0 && get_num_unblocked_bin(~lit) == 0) {
IF_VERBOSE(10, verbose_stream() << "pure literal: " << lit << "\n";);
IF_VERBOSE(100, verbose_stream() << "pure literal: " << lit << "\n";);
s().assign(lit, justification());
return true;
}

12
src/sat/sat_lookahead.cpp
View file

@ -1964,7 +1964,7 @@ namespace sat {
bool_var_vector vars;
for (bool_var v : m_freevars) vars.push_back(v);
while (true) {
lbool result = cube(vars, lits);
lbool result = cube(vars, lits, UINT_MAX);
if (lits.empty() || result != l_undef) {
return l_undef;
}
@ -1973,7 +1973,7 @@ namespace sat {
return l_undef;
}
lbool lookahead::cube(bool_var_vector const& vars, literal_vector& lits) {
lbool lookahead::cube(bool_var_vector const& vars, literal_vector& lits, unsigned backtrack_level) {
scoped_ext _scoped_ext(*this);
lits.reset();
m_select_lookahead_vars.reset();
@ -2006,6 +2006,14 @@ namespace sat {
continue;
}
pick_up_work:
if (m_cube_state.m_cube.size() >= backtrack_level) {
IF_VERBOSE(10, verbose_stream() << "(sat-cube :cube: " << m_cube_state.m_cube.size() << " :backtrack_level " << backtrack_level << ")\n";);
while (m_cube_state.m_cube.size() >= backtrack_level) {
set_conflict();
backtrack(m_cube_state.m_cube, m_cube_state.m_is_decision);
}
backtrack_level = UINT_MAX;
}
depth = m_cube_state.m_cube.size();
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)) {

2
src/sat/sat_lookahead.h
View file

@ -567,7 +567,7 @@ namespace sat {
lbool cube();
lbool cube(bool_var_vector const& vars, literal_vector& lits);
lbool cube(bool_var_vector const& vars, literal_vector& lits, unsigned backtrack_level);
literal select_lookahead(literal_vector const& assumptions, bool_var_vector const& vars);
/**

4
src/sat/sat_solver.cpp
View file

@ -837,11 +837,11 @@ namespace sat {
return lh.select_lookahead(assumptions, vars);
}
lbool solver::cube(bool_var_vector const& vars, literal_vector& lits) {
lbool solver::cube(bool_var_vector const& vars, literal_vector& lits, unsigned backtrack_level) {
if (!m_cuber) {
m_cuber = alloc(lookahead, *this);
}
lbool result = m_cuber->cube(vars, lits);
lbool result = m_cuber->cube(vars, lits, backtrack_level);
if (result == l_false) {
dealloc(m_cuber);
m_cuber = nullptr;

2
src/sat/sat_solver.h
View file

@ -352,7 +352,7 @@ namespace sat {
bool check_clauses(model const& m) const;
literal select_lookahead(literal_vector const& assumptions, bool_var_vector const& vars);
lbool cube(bool_var_vector const& vars, literal_vector& lits);
lbool cube(bool_var_vector const& vars, literal_vector& lits, unsigned backtrack_level);
protected:
unsigned m_conflicts_since_init;

4
src/sat/sat_solver/inc_sat_solver.cpp
View file

@ -301,7 +301,7 @@ public:
return 0;
}
virtual expr_ref cube() {
virtual expr_ref cube(unsigned backtrack_level) {
if (!m_internalized) {
dep2asm_t dep2asm;
m_model = 0;
@ -315,7 +315,7 @@ public:
vars.push_back(kv.m_value);
}
sat::literal_vector lits;
lbool result = m_solver.cube(vars, lits);
lbool result = m_solver.cube(vars, lits, backtrack_level);
if (result == l_false || lits.empty()) {
return expr_ref(m.mk_false(), m);
}