From 72c7a9cf6af4e40a09b9bba8982970ee31947216 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 22 Jan 2025 10:59:52 -0800
Subject: [PATCH] fix re-entrancy bug between ddfw and theory solvers.

Flips triggered from external sources should not trigger callbacks.
---
 src/ast/sls/sat_ddfw.cpp          | 17 +++++++++++------
 src/ast/sls/sat_ddfw.h            |  9 +++++----
 src/ast/sls/sls_arith_clausal.cpp |  1 +
 src/ast/sls/sls_context.h         |  4 ++--
 4 files changed, 19 insertions(+), 12 deletions(-)

diff --git a/src/ast/sls/sat_ddfw.cpp b/src/ast/sls/sat_ddfw.cpp
index f08e1db37..db9dd0d9f 100644
--- a/src/ast/sls/sat_ddfw.cpp
+++ b/src/ast/sls/sat_ddfw.cpp
@@ -99,8 +99,8 @@ namespace sat {
         m_last_flips = m_flips;
     }
 
-    sat::bool_var ddfw::bool_flip() {
-        flet<bool> _in_bool_flip(m_in_bool_flip, true);
+    sat::bool_var ddfw::external_flip() {
+        flet<bool> _in_external_flip(m_in_external_flip, true);
         double reward = 0;
         bool_var v = pick_var(reward);
         if (apply_flip(v, reward))
@@ -135,7 +135,7 @@ namespace sat {
         bool_var v0 = null_bool_var;
         for (bool_var v : m_unsat_vars) {
             r = reward(v);
-            if (m_in_bool_flip && m_plugin->is_external(v))
+            if (m_in_external_flip && m_plugin->is_external(v))
                 ;
             else if (r > 0.0)    
                 sum_pos += score(r);            
@@ -146,7 +146,7 @@ namespace sat {
             double lim_pos = ((double) m_rand() / (1.0 + m_rand.max_value())) * sum_pos;                
             for (bool_var v : m_unsat_vars) {
                 r = reward(v);
-                if (m_in_bool_flip && m_plugin->is_external(v))
+                if (m_in_external_flip && m_plugin->is_external(v))
                     continue;
                 if (r > 0) {
                     lim_pos -= score(r);
@@ -160,7 +160,7 @@ namespace sat {
             return v0;
         if (m_unsat_vars.empty())
             return null_bool_var;
-        if (m_in_bool_flip)
+        if (m_in_external_flip)
             return false;
         return m_unsat_vars.elem_at(m_rand(m_unsat_vars.size()));
     }
@@ -258,6 +258,11 @@ namespace sat {
         return true;
     }
 
+    void ddfw::external_flip(bool_var v) {
+        flet<bool> _external_flip(m_in_external_flip, true);
+        flip(v);
+    }
+
     void ddfw::flip(bool_var v) {
         ++m_flips;
         m_limit.inc();
@@ -417,7 +422,7 @@ namespace sat {
         for (unsigned i = 0; i < num_vars(); ++i) 
             m_model[i] = to_lbool(value(i));
         save_priorities();
-        if (m_plugin && !m_in_bool_flip)
+        if (m_plugin && !m_in_external_flip)
             m_last_result = m_plugin->on_save_model();   
     }
 
diff --git a/src/ast/sls/sat_ddfw.h b/src/ast/sls/sat_ddfw.h
index 217a0ca0b..7f3f3e555 100644
--- a/src/ast/sls/sat_ddfw.h
+++ b/src/ast/sls/sat_ddfw.h
@@ -214,7 +214,9 @@ namespace sat {
         bool_var_set m_rotate_tabu;
         bool_var_vector m_new_tabu_vars;
 
-        bool m_in_bool_flip = false;
+        void flip(bool_var v);
+        bool m_in_external_flip = false;
+
 
     public:
 
@@ -265,9 +267,8 @@ namespace sat {
 
         void remove_assumptions();
 
-        void flip(bool_var v);
-
-        sat::bool_var bool_flip();
+        void external_flip(sat::bool_var v);
+        sat::bool_var external_flip();
 
         void shift_weights();
 
diff --git a/src/ast/sls/sls_arith_clausal.cpp b/src/ast/sls/sls_arith_clausal.cpp
index 8acdeeb77..ca3f2cf8f 100644
--- a/src/ast/sls/sls_arith_clausal.cpp
+++ b/src/ast/sls/sls_arith_clausal.cpp
@@ -238,6 +238,7 @@ namespace sls {
         m_last_delta = delta;
         if (!a.can_update_num(v, delta))
             return;
+        ctx.rlimit().inc();
         auto score = get_score(v, delta);
         auto& vi = a.m_vars[v];        
         num_t abs_value = abs(vi.value() + delta);
diff --git a/src/ast/sls/sls_context.h b/src/ast/sls/sls_context.h
index 1b69682d9..96958ab0f 100644
--- a/src/ast/sls/sls_context.h
+++ b/src/ast/sls/sls_context.h
@@ -69,7 +69,7 @@ namespace sls {
         virtual sat::clause_info const& get_clause(unsigned idx) const = 0;
         virtual ptr_iterator<unsigned> get_use_list(sat::literal lit) = 0;
         virtual void flip(sat::bool_var v) = 0;
-        virtual sat::bool_var bool_flip() = 0;
+        virtual sat::bool_var external_flip() = 0;
         virtual bool try_rotate(sat::bool_var v, sat::bool_var_set& rotated, unsigned& budget) = 0;
         virtual double reward(sat::bool_var v) = 0;
         virtual double get_weigth(unsigned clause_idx) = 0;
@@ -189,7 +189,7 @@ namespace sls {
         void add_theory_axiom(expr* f) { add_assertion(f, false); }
         void add_clause(sat::literal_vector const& lits);
         void flip(sat::bool_var v) { s.flip(v); }
-        sat::bool_var bool_flip() { return s.bool_flip(); }
+        sat::bool_var bool_flip() { return s.external_flip(); }
         void shift_weights() { s.shift_weights(); }
         bool try_rotate(sat::bool_var v, sat::bool_var_set& rotated, unsigned& budget) { return s.try_rotate(v, rotated, budget); }
         double reward(sat::bool_var v) { return s.reward(v); }