mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-13 20:38:43 +00:00
Code Activity

add statistics to cubing

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-12-01 10:13:54 -08:00
parent e0d28c67cd
commit c8e655830f
3 changed files with 20 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
src/sat/sat_lookahead.cpp
View file

@ -2013,6 +2013,11 @@ namespace sat {
return true;
}
void lookahead::update_cube_statistics(statistics& st) {
st.update("lh cube cutoffs", m_cube_state.m_cutoffs);
st.update("lh cube conflicts", m_cube_state.m_conflicts);
}
lbool lookahead::cube(bool_var_vector const& vars, literal_vector& lits, unsigned backtrack_level) {
scoped_ext _scoped_ext(*this);
lits.reset();
@ -2031,6 +2036,7 @@ namespace sat {
unsigned depth = 0;
unsigned init_trail = m_trail.size();
m_cube_state.reset_stats();
if (!is_first) {
goto pick_up_work;
}
@ -2041,8 +2047,9 @@ namespace sat {
inc_istamp();
if (inconsistent()) {
TRACE("sat", tout << "inconsistent: " << m_cube_state.m_cube << "\n";);
m_cube_state.m_freevars_threshold = m_freevars.size();
if (!backtrack(m_cube_state.m_cube, m_cube_state.m_is_decision)) return l_false;
m_cube_state.m_freevars_threshold = m_freevars.size();
m_cube_state.inc_conflict();
if (!backtrack(m_cube_state.m_cube, m_cube_state.m_is_decision)) return l_false;
continue;
}
pick_up_work:
@ -2059,6 +2066,7 @@ namespace sat {
(m_config.m_cube_cutoff == 0 && m_freevars.size() < m_cube_state.m_freevars_threshold)) {
m_cube_state.m_freevars_threshold *= (1.0 - pow(m_config.m_cube_fraction, depth));
set_conflict();
m_cube_state.inc_cutoff();
#if 0
// return cube of all literals, not just the ones in the main cube
lits.append(m_trail.size() - init_trail, m_trail.c_ptr() + init_trail);

10
src/sat/sat_lookahead.h
View file

@ -167,13 +167,19 @@ namespace sat {
svector<bool> m_is_decision;
literal_vector m_cube;
double m_freevars_threshold;
unsigned m_conflicts;
unsigned m_cutoffs;
cube_state() { reset(); }
void reset() {
m_first = true;
m_is_decision.reset();
m_cube.reset();
m_freevars_threshold = 0;
m_freevars_threshold = 0;
reset_stats();
}
void reset_stats() { m_conflicts = 0; m_cutoffs = 0; }
void inc_conflict() { ++m_conflicts; }
void inc_cutoff() { ++m_cutoffs; }
};
config m_config;
@ -572,6 +578,8 @@ namespace sat {
lbool cube(bool_var_vector const& vars, literal_vector& lits, unsigned backtrack_level);
void update_cube_statistics(statistics& st);
literal select_lookahead(literal_vector const& assumptions, bool_var_vector const& vars);
/**
\brief simplify set of clauses by extracting units from a lookahead at base level.

1
src/sat/sat_solver.cpp
View file

@ -859,6 +859,7 @@ namespace sat {
m_cuber = alloc(lookahead, *this);
}
lbool result = m_cuber->cube(vars, lits, backtrack_level);
m_cuber->update_cube_statistics(m_aux_stats);
if (result == l_false) {
dealloc(m_cuber);
m_cuber = nullptr;