mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 04:03:39 +00:00
Code Activity

try dual phase lookahead

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2024-12-27 13:34:48 -08:00
parent 1f55ec5cef
commit 0b9ed925d6
2 changed files with 14 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -674,12 +674,21 @@ namespace sls {
return false; return false;
} }
} }
bool bv_eval::is_lookahead_phase() {
++m_lookahead_steps;
if (m_lookahead_steps < m_lookahead_phase_size)
return true;
if (m_lookahead_steps > 2 * m_lookahead_phase_size)
m_lookahead_steps = 0;
return false;
}
bool bv_eval::repair_down(app* e, unsigned i) { bool bv_eval::repair_down(app* e, unsigned i) {
expr* arg = e->get_arg(i); expr* arg = e->get_arg(i);
if (m.is_value(arg)) if (m.is_value(arg))
return false; return false;
if (false && m.is_bool(e) && ctx.rand(10) == 0 && m_lookahead.try_repair_down(e)) if (m.is_bool(e) && is_lookahead_phase() && m_lookahead.try_repair_down(e))
return true; return true;
if (e->get_family_id() == bv.get_family_id() && try_repair_bv(e, i)) { if (e->get_family_id() == bv.get_family_id() && try_repair_bv(e, i)) {
commit_eval(e, to_app(arg)); commit_eval(e, to_app(arg));

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

@ -52,6 +52,8 @@ namespace sls {
random_gen m_rand; random_gen m_rand;
config m_config; config m_config;
bool_vector m_fixed; bool_vector m_fixed;
unsigned m_lookahead_steps = 0;
unsigned m_lookahead_phase_size = 100;
scoped_ptr_vector<sls::bv_valuation> m_values; // expr-id -> bv valuation scoped_ptr_vector<sls::bv_valuation> m_values; // expr-id -> bv valuation
@ -147,6 +149,8 @@ namespace sls {
void commit_eval(expr* p, app* e); void commit_eval(expr* p, app* e);
bool is_lookahead_phase();
public: public:
bv_eval(sls::bv_terms& terms, sls::context& ctx); bv_eval(sls::bv_terms& terms, sls::context& ctx);