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

fix #4624 #4633 #4632 #4631

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-08-13 08:36:16 -07:00
parent 84390575e2
commit c41abf2241
4 changed files with 29 additions and 32 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/math/dd/dd_bdd.cpp
View file

@ -318,7 +318,7 @@ namespace dd {
goto go_down;
}
else {
while (current_cost() != best_cost) {
while (current_cost() > best_cost) {
sift_up(--lvl);
}
return;
@ -339,7 +339,7 @@ namespace dd {
goto go_up;
}
else {
while (current_cost() != best_cost) {
while (current_cost() > best_cost) {
sift_up(lvl++);
}
return;

4
src/opt/maxres.cpp
View file

@ -289,10 +289,8 @@ public:
Give preference to cores that have large minimal values.
*/
sort_assumptions(asms);
m_last_index = std::min(m_last_index, asms.size()-1);
m_last_index = 0;
unsigned index = m_last_index>0?m_last_index-1:0;
m_last_index = 0;
unsigned index = 0;
bool first = index > 0;
SASSERT(index < asms.size() || asms.empty());
IF_VERBOSE(10, verbose_stream() << "start hill climb " << index << " asms: " << asms.size() << "\n";);

2
src/sat/sat_config.cpp
View file

@ -99,7 +99,7 @@ namespace sat {
else
m_local_search_mode = local_search_mode::wsat;
m_local_search_dbg_flips = p.local_search_dbg_flips();
m_binspr = p.binspr();
//m_binspr = p.binspr();
m_binspr = false; // prevent adventurous users from trying feature that isn't ready
m_anf_simplify = p.anf();
m_anf_delay = p.anf_delay();

51
src/smt/theory_pb.cpp
View file

@ -1325,37 +1325,37 @@ namespace smt {
bool theory_pb::gc() {
unsigned z = 0, nz = 0;
m_occs.reset();
for (unsigned i = 0; i < m_card_trail.size(); ++i) {
bool_var v = m_card_trail[i];
if (v == null_bool_var) continue;
if (v == null_bool_var)
continue;
card* c = m_var_infos[v].m_card;
if (c) {
c->reset_propagations();
literal lit = c->lit();
if (c->is_aux() && ctx.get_assign_level(lit) > ctx.get_search_level()) {
double activity = ctx.get_activity(v);
if (activity <= 0) {
nz++;
}
else {
z++;
clear_watch(*c);
m_var_infos[v].m_card = nullptr;
dealloc(c);
m_card_trail[i] = null_bool_var;
ctx.remove_watch(v);
// TBD: maybe v was used in a clause for propagation.
m_occs.insert(v);
}
if (!c)
continue;
c->reset_propagations();
literal lit = c->lit();
if (c->is_aux() && ctx.get_assign_level(lit) > ctx.get_search_level()) {
double activity = ctx.get_activity(v);
if (activity <= 0) {
nz++;
}
else {
z++;
clear_watch(*c);
m_var_infos[v].m_card = nullptr;
dealloc(c);
m_card_trail[i] = null_bool_var;
ctx.remove_watch(v);
// TBD: maybe v was used in a clause for propagation.
m_occs.insert(v);
}
}
}
clause_vector const& lemmas = ctx.get_lemmas();
for (unsigned i = 0; i < lemmas.size(); ++i) {
clause* cl = lemmas[i];
#if 0
for (clause* cl : ctx.get_lemmas()) {
if (!cl->deleted()) {
for (literal lit : *cl) {
if (m_occs.contains(lit.var())) {
@ -1365,9 +1365,6 @@ namespace smt {
}
}
//std::cout << "zs: " << z << " nzs: " << nz << " lemmas: " << ctx.get_lemmas().size() << " trail: " << m_card_trail.size() << "\n";
return z*10 >= nz;
m_occs.reset();
for (unsigned i = 0; i < lemmas.size(); ++i) {
clause* cl = lemmas[i];
@ -1377,6 +1374,8 @@ namespace smt {
m_occs.insert(idx);
}
}
#endif
return z*10 >= nz;
}