mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

try uneven lookahead skew

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2024-12-27 13:55:22 -08:00
parent 3aacc62229
commit a5bc5ed813
2 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/ast/sls/sls_bv_eval.cpp
View file

@ -679,7 +679,7 @@ namespace sls {
++m_lookahead_steps; ++m_lookahead_steps;
if (m_lookahead_steps < m_lookahead_phase_size) if (m_lookahead_steps < m_lookahead_phase_size)
return true; return true;
if (m_lookahead_steps > 2 * m_lookahead_phase_size) if (m_lookahead_steps > 10 * m_lookahead_phase_size)
m_lookahead_steps = 0; m_lookahead_steps = 0;
return false; return false;
} }

2
src/ast/sls/sls_bv_eval.h
View file

@ -53,7 +53,7 @@ namespace sls {
config m_config; config m_config;
bool_vector m_fixed; bool_vector m_fixed;
unsigned m_lookahead_steps = 0; unsigned m_lookahead_steps = 0;
unsigned m_lookahead_phase_size = 100; unsigned m_lookahead_phase_size = 10;
scoped_ptr_vector<sls::bv_valuation> m_values; // expr-id -> bv valuation scoped_ptr_vector<sls::bv_valuation> m_values; // expr-id -> bv valuation