mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-14 21:08:46 +00:00
Code Activity

Merge pull request #12 from TheRealNebus/opt

Browse source 
Opt
This commit is contained in:
Nikolaj Bjorner 2017-12-15 14:12:02 -08:00 committed by GitHub
parent b3e5fade32 a52fd4c6f2
commit 5adfae0fa8
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
4 changed files with 12 additions and 9 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/ast/ast_translation.cpp
View file

@ -77,8 +77,8 @@ void ast_translation::push_frame(ast * n) {
} }
bool ast_translation::visit(ast * n) { bool ast_translation::visit(ast * n) {
ast * r;
if (n->get_ref_count() > 1) { if (n->get_ref_count() > 1) {
ast * r;
if (m_cache.find(n, r)) { if (m_cache.find(n, r)) {
m_result_stack.push_back(r); m_result_stack.push_back(r);
++m_hit_count; ++m_hit_count;

2
src/sat/sat_elim_eqs.cpp
View file

@ -181,7 +181,7 @@ namespace sat {
for (bool_var v : to_elim) { for (bool_var v : to_elim) {
literal l(v, false); literal l(v, false);
literal r = roots[v]; literal r = roots[v];
SASSERT(v != r.var()); SASSERT(v != r.var());
bool root_ok = !m_solver.is_external(v) || m_solver.set_root(l, r); bool root_ok = !m_solver.is_external(v) || m_solver.set_root(l, r);
if (m_solver.is_external(v) && (m_solver.is_incremental() || !root_ok)) { if (m_solver.is_external(v) && (m_solver.is_incremental() || !root_ok)) {
// cannot really eliminate v, since we have to notify extension of future assignments // cannot really eliminate v, since we have to notify extension of future assignments

16
src/sat/sat_lookahead.cpp
View file

@ -1477,7 +1477,7 @@ namespace sat {
} }
} }
if (m_search_mode == lookahead_mode::lookahead1) { if (m_search_mode == lookahead_mode::lookahead1) {
SASSERT(nonfixed >= 2); //SASSERT(nonfixed >= 2);
switch (m_config.m_reward_type) { switch (m_config.m_reward_type) {
case heule_schur_reward: { case heule_schur_reward: {
double to_add = 0; double to_add = 0;
@ -1493,7 +1493,7 @@ namespace sat {
m_lookahead_reward += pow(0.5, nonfixed); m_lookahead_reward += pow(0.5, nonfixed);
break; break;
case march_cu_reward: case march_cu_reward:
m_lookahead_reward += 3.3 * pow(0.5, nonfixed - 2); m_lookahead_reward += nonfixed >= 2 ? 3.3 * pow(0.5, nonfixed - 2) : 0.0;
break; break;
case ternary_reward: case ternary_reward:
UNREACHABLE(); UNREACHABLE();
@ -1703,7 +1703,8 @@ namespace sat {
num_units += do_double(lit, dl_lvl); num_units += do_double(lit, dl_lvl);
if (dl_lvl > level) { if (dl_lvl > level) {
base = dl_lvl; base = dl_lvl;
SASSERT(get_level(m_trail.back()) == base + m_lookahead[i].m_offset); //SASSERT(get_level(m_trail.back()) == base + m_lookahead[i].m_offset);
SASSERT(get_level(m_trail.back()) == base);
} }
unsat = inconsistent(); unsat = inconsistent();
pop_lookahead1(lit, num_units); pop_lookahead1(lit, num_units);
@ -1822,11 +1823,11 @@ namespace sat {
unsigned lookahead::double_look(literal l, unsigned& base) { unsigned lookahead::double_look(literal l, unsigned& base) {
SASSERT(!inconsistent()); SASSERT(!inconsistent());
SASSERT(dl_no_overflow(base)); SASSERT(dl_no_overflow(base));
SASSERT(is_fixed_at(l, base));
base += m_lookahead.size(); base += m_lookahead.size();
unsigned dl_truth = base + m_lookahead.size() * m_config.m_dl_max_iterations; unsigned dl_truth = base + m_lookahead.size() * m_config.m_dl_max_iterations;
scoped_level _sl(*this, dl_truth); scoped_level _sl(*this, dl_truth);
SASSERT(get_level(m_trail.back()) == dl_truth); //SASSERT(get_level(m_trail.back()) == dl_truth);
SASSERT(is_fixed(l));
IF_VERBOSE(2, verbose_stream() << "(sat-lookahead :double " << l << " :depth " << m_trail_lim.size() << ")\n";); IF_VERBOSE(2, verbose_stream() << "(sat-lookahead :double " << l << " :depth " << m_trail_lim.size() << ")\n";);
lookahead_backtrack(); lookahead_backtrack();
assign(l); assign(l);
@ -2078,7 +2079,8 @@ namespace sat {
inc_istamp(); inc_istamp();
if (inconsistent()) { if (inconsistent()) {
TRACE("sat", tout << "inconsistent: " << m_cube_state.m_cube << "\n";); TRACE("sat", tout << "inconsistent: " << m_cube_state.m_cube << "\n";);
m_cube_state.m_freevars_threshold = m_freevars.size(); m_cube_state.m_freevars_threshold = m_freevars.size();
m_cube_state.m_psat_threshold = m_config.m_cube_cutoff == adaptive_psat_cutoff ? psat_heur() : DBL_MAX; // MN. only compute PSAT if enabled
m_cube_state.inc_conflict(); m_cube_state.inc_conflict();
if (!backtrack(m_cube_state.m_cube, m_cube_state.m_is_decision)) return l_false; if (!backtrack(m_cube_state.m_cube, m_cube_state.m_is_decision)) return l_false;
continue; continue;
@ -2100,7 +2102,7 @@ namespace sat {
(m_config.m_cube_cutoff == adaptive_psat_cutoff && psat_heur() >= m_cube_state.m_psat_threshold)) { (m_config.m_cube_cutoff == adaptive_psat_cutoff && psat_heur() >= m_cube_state.m_psat_threshold)) {
double dec = (1.0 - pow(m_config.m_cube_fraction, depth)); double dec = (1.0 - pow(m_config.m_cube_fraction, depth));
m_cube_state.m_freevars_threshold *= dec; m_cube_state.m_freevars_threshold *= dec;
m_cube_state.m_psat_threshold *= dec; m_cube_state.m_psat_threshold *= 2.0 - dec;
set_conflict(); set_conflict();
m_cube_state.inc_cutoff(); m_cube_state.inc_cutoff();
#if 0 #if 0

1
src/sat/sat_solver.cpp
View file

@ -60,6 +60,7 @@ namespace sat {
m_next_simplify = 0; m_next_simplify = 0;
m_num_checkpoints = 0; m_num_checkpoints = 0;
m_simplifications = 0; m_simplifications = 0;
m_ext = 0;
m_cuber = nullptr; m_cuber = nullptr;
m_mc.set_solver(this); m_mc.set_solver(this);
} }