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

fix #3148

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-03-05 10:35:24 +01:00
parent ca4a78f2ab
commit 8b0d540cca
3 changed files with 21 additions and 13 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/ast/rewriter/bv_rewriter.cpp
View file

@ -273,13 +273,13 @@ bool bv_rewriter::are_eq_upto_num(expr * _a, expr * _b,
}
}
if (!aadd && badd) {
if (to_app(_a)->get_num_args() != 2 || !has_num_a || to_app(_a)->get_arg(0) != _b)
if (!is_app(_a) || to_app(_a)->get_num_args() != 2 || !has_num_a || to_app(_a)->get_arg(0) != _b)
return false;
common = _b;
return true;
}
if (aadd && !badd) {
if (to_app(_b)->get_num_args() != 2 || !has_num_b || to_app(_b)->get_arg(0) != _a)
if (!is_app(_b) || to_app(_b)->get_num_args() != 2 || !has_num_b || to_app(_b)->get_arg(0) != _a)
return false;
common = _a;
return true;

26
src/sat/sat_unit_walk.cpp
View file

@ -97,12 +97,15 @@ namespace sat {
};
lbool unit_walk::operator()() {
m_inconsistent = false;
scoped_set_unit_walk _scoped_set(this, s);
init_runs();
if (init_runs())
return l_true;
init_propagation();
init_phase();
lbool st = l_undef;
while (s.rlimit().inc() && st == l_undef) {
std::cout << "walk " << st << "\n";
if (inconsistent() && !m_decisions.empty()) do_pop();
else if (inconsistent()) st = l_false;
else if (should_restart()) restart();
@ -141,12 +144,15 @@ namespace sat {
lbool unit_walk::do_backjump() {
unsigned backjump_level = m_decisions.size(); // - (m_decisions.size()/20);
switch (update_priority(backjump_level)) {
lbool st = update_priority(backjump_level);
std::cout << "update " << st << "\n";
switch (st) {
case l_true: return l_true;
case l_false: break; // TBD
default: break;
}
refresh_solver();
if (refresh_solver())
return l_true;
return l_undef;
}
@ -175,7 +181,7 @@ namespace sat {
m_inconsistent = false;
}
void unit_walk::init_runs() {
bool unit_walk::init_runs() {
m_luby_index = 0;
m_restart_threshold = 1000;
m_max_trail = 0;
@ -190,7 +196,7 @@ namespace sat {
}
m_ls.import(s, true);
m_rand.set_seed(s.rand()());
update_priority(0);
return l_true == update_priority(0);
}
lbool unit_walk::do_local_search(unsigned num_rounds) {
@ -212,7 +218,7 @@ namespace sat {
while (m_decisions.size() > level) {
pop_decision();
}
IF_VERBOSE(1, verbose_stream() << "(sat.unit-walk :update-priority " << m_decisions.size() << "\n");
IF_VERBOSE(1, verbose_stream() << "(sat.unit-walk :update-priority " << m_decisions.size() << ")\n");
unsigned num_rounds = 50;
log_status();
@ -221,7 +227,7 @@ namespace sat {
switch (is_sat) {
case l_true:
for (unsigned v = 0; v < s.num_vars(); ++v) {
s.m_assignment[v] = m_ls.get_best_phase(v) ? l_true : l_false;
s.m_assignment[v] = m_ls.get_model()[v];
}
return l_true;
case l_false:
@ -265,15 +271,17 @@ namespace sat {
}
}
void unit_walk::refresh_solver() {
bool unit_walk::refresh_solver() {
m_max_conflicts += m_conflict_offset ;
m_conflict_offset += 10000;
if (s.m_par && s.m_par->copy_solver(s)) {
IF_VERBOSE(1, verbose_stream() << "(sat.unit-walk fresh copy)\n";);
if (s.get_extension()) s.get_extension()->set_unit_walk(this);
init_runs();
if (init_runs())
return true;
init_phase();
}
return false;
}
bool unit_walk::should_restart() {

4
src/sat/sat_unit_walk.h
View file

@ -82,12 +82,12 @@ namespace sat {
void restart();
void pop();
void pop_decision();
void init_runs();
bool init_runs();
lbool update_priority(unsigned level);
void update_pqueue();
void init_phase();
void init_propagation();
void refresh_solver();
bool refresh_solver();
void update_max_trail();
void flip_phase(literal l);
void propagate();