mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-04 05:19:11 +00:00
Code Activity

local updates

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-02-01 18:04:08 -08:00
commit c21b860d4e
2 changed files with 48 additions and 34 deletions
Download patch file Download diff file Expand all files Collapse all files

76
src/sat/sat_solver.cpp
View file

@ -48,6 +48,7 @@ namespace sat {
m_case_split_queue(m_activity),
m_qhead(0),
m_scope_lvl(0),
m_search_lvl(0),
m_params(p) {
updt_params(p);
m_conflicts_since_gc = 0;
@ -93,7 +94,7 @@ namespace sat {
m_ext = src.get_extension()->copy(this);
}
{
unsigned sz = scope_lvl() == 0 ? src.m_trail.size() : src.m_scopes[0].m_trail_lim;
unsigned sz = src.init_trail_size();
for (unsigned i = 0; i < sz; ++i) {
assign(src.m_trail[i], justification());
}
@ -134,6 +135,8 @@ namespace sat {
m_user_scope_literals.reset();
m_user_scope_literals.append(src.m_user_scope_literals);
std::cout << "copy: " << init_trail_size() << " " << src.init_trail_size() << "\n";
}
// -----------------------
@ -232,9 +235,9 @@ namespace sat {
void solver::mk_bin_clause(literal l1, literal l2, bool learned) {
if (propagate_bin_clause(l1, l2)) {
if (scope_lvl() == 0)
if (at_base_lvl())
return;
if (!learned)
if (!learned && !at_search_lvl())
m_clauses_to_reinit.push_back(clause_wrapper(l1, l2));
}
m_stats.m_mk_bin_clause++;
@ -281,7 +284,7 @@ namespace sat {
m_watches[(~c[0]).index()].push_back(watched(c[1], c[2]));
m_watches[(~c[1]).index()].push_back(watched(c[0], c[2]));
m_watches[(~c[2]).index()].push_back(watched(c[0], c[1]));
if (scope_lvl() > 0) {
if (!at_base_lvl()) {
if (value(c[1]) == l_false && value(c[2]) == l_false) {
m_stats.m_ter_propagate++;
assign(c[0], justification(c[1], c[2]));
@ -317,7 +320,7 @@ namespace sat {
bool solver::attach_nary_clause(clause & c) {
bool reinit = false;
clause_offset cls_off = m_cls_allocator.get_offset(&c);
if (scope_lvl() > 0) {
if (!at_base_lvl()) {
if (c.is_learned()) {
unsigned w2_idx = select_learned_watch_lit(c);
std::swap(c[1], c[w2_idx]);
@ -467,7 +470,7 @@ namespace sat {
}
bool solver::simplify_clause(unsigned & num_lits, literal * lits) const {
if (scope_lvl() == 0)
if (at_base_lvl())
return simplify_clause_core<true>(num_lits, lits);
else
return simplify_clause_core<false>(num_lits, lits);
@ -514,7 +517,7 @@ namespace sat {
void solver::assign_core(literal l, justification j) {
SASSERT(value(l) == l_undef);
TRACE("sat_assign_core", tout << l << "\n";);
if (scope_lvl() == 0)
if (at_base_lvl())
j = justification(); // erase justification for level 0
m_assignment[l.index()] = l_true;
m_assignment[(~l).index()] = l_false;
@ -733,7 +736,7 @@ namespace sat {
lbool solver::check(unsigned num_lits, literal const* lits) {
pop_to_base_level();
IF_VERBOSE(2, verbose_stream() << "(sat.sat-solver)\n";);
SASSERT(scope_lvl() == 0);
SASSERT(at_base_lvl());
if (m_config.m_num_parallel > 1 && !m_par) {
return check_par(num_lits, lits);
}
@ -785,7 +788,6 @@ namespace sat {
restart();
simplify_problem();
exchange_par();
if (check_inconsistent()) return l_false;
gc();
@ -900,10 +902,11 @@ namespace sat {
\brief import lemmas/units from parallel sat solvers.
*/
void solver::exchange_par() {
if (m_par && scope_lvl() == 0) {
unsigned sz = scope_lvl() == 0 ? m_trail.size() : m_scopes[0].m_trail_lim;
if (m_par) {
SASSERT(scope_lvl() == search_lvl());
// TBD: import also dependencies of assumptions.
unsigned sz = init_trail_size();
unsigned num_in = 0, num_out = 0;
SASSERT(scope_lvl() == 0); // parallel with assumptions is TBD
literal_vector in, out;
for (unsigned i = m_par_limit_out; i < sz; ++i) {
literal lit = m_trail[i];
@ -1026,7 +1029,7 @@ namespace sat {
return l_undef;
if (m_conflicts_since_restart > m_restart_threshold)
return l_undef;
if (scope_lvl() == 0) {
if (at_base_lvl()) {
cleanup(); // cleaner may propagate frozen clauses
if (inconsistent()) {
TRACE("sat", tout << "conflict at level 0\n";);
@ -1074,6 +1077,7 @@ namespace sat {
return;
}
SASSERT(at_base_lvl());
reset_assumptions();
push();
@ -1103,6 +1107,8 @@ namespace sat {
add_assumption(lit);
assign(lit, justification());
}
m_search_lvl = scope_lvl();
SASSERT(m_search_lvl == 1);
}
@ -1146,7 +1152,10 @@ namespace sat {
}
void solver::reinit_assumptions() {
if (tracking_assumptions() && scope_lvl() == 0) {
if (at_search_lvl()) {
std::cout << " " << init_trail_size() << " " << m_trail.size() << "\n";
}
if (tracking_assumptions() && at_base_lvl()) {
TRACE("sat", tout << m_assumptions << "\n";);
push();
for (unsigned i = 0; !inconsistent() && i < m_user_scope_literals.size(); ++i) {
@ -1183,6 +1192,7 @@ namespace sat {
m_gc_threshold = m_config.m_gc_initial;
m_restarts = 0;
m_min_d_tk = 1.0;
m_search_lvl = 0;
m_stopwatch.reset();
m_stopwatch.start();
m_core.reset();
@ -1201,13 +1211,11 @@ namespace sat {
}
IF_VERBOSE(2, verbose_stream() << "(sat.simplify)\n";);
// Disable simplification during MUS computation.
// if (m_mus.is_active()) return;
TRACE("sat", tout << "simplify\n";);
pop(scope_lvl());
SASSERT(scope_lvl() == 0);
SASSERT(at_base_lvl());
m_cleaner();
CASSERT("sat_simplify_bug", check_invariant());
@ -1362,7 +1370,7 @@ namespace sat {
<< " :restarts " << m_stats.m_restart << mk_stat(*this)
<< " :time " << std::fixed << std::setprecision(2) << m_stopwatch.get_current_seconds() << ")\n";);
IF_VERBOSE(30, display_status(verbose_stream()););
pop_reinit(scope_lvl());
pop_reinit(scope_lvl() - search_lvl());
m_conflicts_since_restart = 0;
switch (m_config.m_restart) {
case RS_GEOMETRIC:
@ -1403,7 +1411,7 @@ namespace sat {
gc_psm_glue();
break;
case GC_DYN_PSM:
if (m_scope_lvl != 0)
if (!at_base_lvl())
return;
gc_dyn_psm();
break;
@ -1529,7 +1537,7 @@ namespace sat {
TRACE("sat", tout << "gc\n";);
// To do gc at scope_lvl() > 0, I will need to use the reinitialization stack, or live with the fact
// that I may miss some propagations for reactivated clauses.
SASSERT(scope_lvl() == 0);
SASSERT(at_base_lvl());
// compute
// d_tk
unsigned h = 0;
@ -1620,7 +1628,7 @@ namespace sat {
// return true if should keep the clause, and false if we should delete it.
bool solver::activate_frozen_clause(clause & c) {
TRACE("sat_gc", tout << "reactivating:\n" << c << "\n";);
SASSERT(scope_lvl() == 0);
SASSERT(at_base_lvl());
// do some cleanup
unsigned sz = c.size();
unsigned j = 0;
@ -2099,7 +2107,7 @@ namespace sat {
if (!m_ext)
return scope_lvl();
if (scope_lvl() == 0)
if (at_base_lvl())
return 0;
unsigned r = 0;
@ -2557,6 +2565,7 @@ namespace sat {
void solver::pop_reinit(unsigned num_scopes) {
pop(num_scopes);
exchange_par();
reinit_assumptions();
}
@ -2601,7 +2610,7 @@ namespace sat {
bool reinit = false;
if (cw.is_binary()) {
if (propagate_bin_clause(cw[0], cw[1])) {
if (scope_lvl() > 0) {
if (!at_base_lvl()) {
m_clauses_to_reinit[j] = cw;
j++;
}
@ -2611,7 +2620,7 @@ namespace sat {
clause & c = *(cw.get_clause());
dettach_clause(c);
attach_clause(c, reinit);
if (scope_lvl() > 0 && reinit) {
if (!at_base_lvl() && reinit) {
// clause propagated literal, must keep it in the reinit stack.
m_clauses_to_reinit[j] = cw;
j++;
@ -2877,7 +2886,7 @@ namespace sat {
}
void solver::display_units(std::ostream & out) const {
unsigned end = scope_lvl() == 0 ? m_trail.size() : m_scopes[0].m_trail_lim;
unsigned end = init_trail_size();
for (unsigned i = 0; i < end; i++) {
out << m_trail[i] << " ";
}
@ -3084,14 +3093,14 @@ namespace sat {
//
// -----------------------
void solver::cleanup() {
if (scope_lvl() > 0 || inconsistent())
if (!at_base_lvl() || inconsistent())
return;
if (m_cleaner() && m_ext)
m_ext->clauses_modifed();
}
void solver::simplify(bool learned) {
if (scope_lvl() > 0 || inconsistent())
if (!at_base_lvl() || inconsistent())
return;
m_simplifier(learned);
m_simplifier.finalize();
@ -3100,7 +3109,7 @@ namespace sat {
}
unsigned solver::scc_bin() {
if (scope_lvl() > 0 || inconsistent())
if (!at_base_lvl() || inconsistent())
return 0;
unsigned r = m_scc();
if (r > 0 && m_ext)
@ -3289,13 +3298,14 @@ namespace sat {
}
propagate(false);
if (check_inconsistent()) return l_false;
SASSERT(search_lvl() == 1);
unsigned num_units = 0, num_iterations = 0;
extract_fixed_consequences(num_units, assumptions, unfixed_vars, conseq);
update_unfixed_literals(unfixed_lits, unfixed_vars);
while (!unfixed_lits.empty()) {
if (scope_lvl() > 1) {
pop(scope_lvl() - 1);
if (scope_lvl() > search_lvl()) {
pop(scope_lvl() - search_lvl());
}
++num_iterations;
checkpoint();
@ -3320,12 +3330,12 @@ namespace sat {
propagate(false);
++num_resolves;
}
if (scope_lvl() == 1) {
if (scope_lvl() == search_lvl()) {
break;
}
}
if (is_sat == l_true) {
if (scope_lvl() == 1 && num_resolves > 0) {
if (scope_lvl() == search_lvl() && num_resolves > 0) {
is_sat = l_undef;
}
else {
@ -3488,7 +3498,7 @@ namespace sat {
}
void solver::asymmetric_branching() {
if (scope_lvl() > 0 || inconsistent())
if (!at_base_lvl() || inconsistent())
return;
m_asymm_branch();
if (m_ext)

6
src/sat/sat_solver.h
View file

@ -115,6 +115,7 @@ namespace sat {
var_queue m_case_split_queue;
unsigned m_qhead;
unsigned m_scope_lvl;
unsigned m_search_lvl;
literal_vector m_trail;
clause_wrapper_vector m_clauses_to_reinit;
struct scope {
@ -220,11 +221,14 @@ namespace sat {
bool is_external(bool_var v) const { return m_external[v] != 0; }
bool was_eliminated(bool_var v) const { return m_eliminated[v] != 0; }
unsigned scope_lvl() const { return m_scope_lvl; }
bool at_search_lvl() const { return m_scope_lvl == 0; }
unsigned search_lvl() const { return m_search_lvl; }
bool at_search_lvl() const { return m_scope_lvl == m_search_lvl; }
bool at_base_lvl() const { return m_scope_lvl == 0; }
lbool value(literal l) const { return static_cast<lbool>(m_assignment[l.index()]); }
lbool value(bool_var v) const { return static_cast<lbool>(m_assignment[literal(v, false).index()]); }
unsigned lvl(bool_var v) const { return m_level[v]; }
unsigned lvl(literal l) const { return m_level[l.var()]; }
unsigned init_trail_size() const { return at_base_lvl() ? m_trail.size() : m_scopes[0].m_trail_lim; }
void assign(literal l, justification j) {
TRACE("sat_assign", tout << l << " previous value: " << value(l) << "\n";);
switch (value(l)) {