mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-27 00:18:45 +00:00
Code Activity

also deal with initializing boolean variables in smt context

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-02-15 17:58:26 -08:00
parent 39f73fa595
commit f84de9400e
3 changed files with 13 additions and 14 deletions
Download patch file Download diff file Expand all files Collapse all files

18
src/sat/sat_unit_walk.cpp
View file

@ -99,6 +99,7 @@ namespace sat {
while (s.rlimit().inc() && st == l_undef) { while (s.rlimit().inc() && st == l_undef) {
if (inconsistent() && !m_decisions.empty()) do_pop(); if (inconsistent() && !m_decisions.empty()) do_pop();
else if (inconsistent()) st = l_false; else if (inconsistent()) st = l_false;
else if (should_restart()) restart();
else if (should_backjump()) st = do_backjump(); else if (should_backjump()) st = do_backjump();
else st = decide(); else st = decide();
} }
@ -276,9 +277,6 @@ namespace sat {
init_runs(); init_runs();
init_phase(); init_phase();
} }
if (false && should_restart()) {
restart();
}
} }
bool unit_walk::should_restart() { bool unit_walk::should_restart() {
@ -287,9 +285,7 @@ namespace sat {
++m_luby_index; ++m_luby_index;
return true; return true;
} }
else { return false;
return false;
}
} }
void unit_walk::restart() { void unit_walk::restart() {
@ -328,9 +324,9 @@ namespace sat {
} }
void unit_walk::propagate() { void unit_walk::propagate() {
while (m_qhead < m_trail.size() && !inconsistent()) while (m_qhead < m_trail.size() && !inconsistent()) {
propagate(choose_literal()); propagate(m_trail[m_qhead++]);
// IF_VERBOSE(1, verbose_stream() << m_trail.size() << " " << inconsistent() << "\n";); }
} }
std::ostream& unit_walk::display(std::ostream& out) const { std::ostream& unit_walk::display(std::ostream& out) const {
@ -495,10 +491,6 @@ namespace sat {
<< ")\n";); << ")\n";);
} }
literal unit_walk::choose_literal() {
return m_trail[m_qhead++];
}
void unit_walk::set_conflict(literal l1, literal l2) { void unit_walk::set_conflict(literal l1, literal l2) {
set_conflict(); set_conflict();
} }

1
src/sat/sat_unit_walk.h
View file

@ -91,7 +91,6 @@ namespace sat {
void flip_phase(literal l); void flip_phase(literal l);
void propagate(); void propagate();
void propagate(literal lit); void propagate(literal lit);
literal choose_literal();
void set_conflict(literal l1, literal l2); void set_conflict(literal l1, literal l2);
void set_conflict(literal l1, literal l2, literal l3); void set_conflict(literal l1, literal l2, literal l3);
void set_conflict(clause const& c); void set_conflict(clause const& c);

8
src/smt/smt_kernel.cpp
View file

@ -156,6 +156,14 @@ namespace smt {
} }
void set_activity(expr* lit, double act) { void set_activity(expr* lit, double act) {
SASSERT(m().is_bool(lit));
m().is_not(lit, lit);
if (!m_kernel.b_internalized(lit)) {
m_kernel.internalize(lit, false);
}
if (!m_kernel.b_internalized(lit)) {
return;
}
auto v = m_kernel.get_bool_var(lit); auto v = m_kernel.get_bool_var(lit);
double old_act = m_kernel.get_activity(v); double old_act = m_kernel.get_activity(v);
m_kernel.set_activity(v, act); m_kernel.set_activity(v, act);