try dual phase lookahead

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Z3Prover · Dec 27, 2024 · 0b9ed92 · 0b9ed92
1 parent 1f55ec5
commit 0b9ed92
Show file tree

Hide file tree

Showing 2 changed files with 14 additions and 1 deletion.
diff --git a/src/ast/sls/sls_bv_eval.cpp b/src/ast/sls/sls_bv_eval.cpp
@@ -674,12 +674,21 @@ namespace sls {
             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) {  
         expr* arg = e->get_arg(i);
         if (m.is_value(arg))
             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;
         if (e->get_family_id() == bv.get_family_id() && try_repair_bv(e, i)) {
             commit_eval(e, to_app(arg));

diff --git a/src/ast/sls/sls_bv_eval.h b/src/ast/sls/sls_bv_eval.h
@@ -52,6 +52,8 @@ namespace sls {
         random_gen          m_rand;
         config              m_config;
         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
@@ -147,6 +149,8 @@ namespace sls {
 
         void commit_eval(expr* p, app* e);
 
+        bool is_lookahead_phase();
+
     public:
         bv_eval(sls::bv_terms& terms, sls::context& ctx);