From 814d7f4d0a383cffa59e3ddd64b2c9926fcf78f2 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 1 Jan 2025 16:01:58 -0800
Subject: [PATCH] block flips to units

---
 src/ast/sls/sls_bv_lookahead.cpp | 14 ++++++++++++--
 src/ast/sls/sls_context.cpp      |  2 +-
 src/ast/sls/sls_context.h        |  3 ++-
 3 files changed, 15 insertions(+), 4 deletions(-)

diff --git a/src/ast/sls/sls_bv_lookahead.cpp b/src/ast/sls/sls_bv_lookahead.cpp
index c19a0894a..0e63fc727 100644
--- a/src/ast/sls/sls_bv_lookahead.cpp
+++ b/src/ast/sls/sls_bv_lookahead.cpp
@@ -106,8 +106,11 @@ namespace sls {
             return false;
         expr* e = vars[ctx.rand(vars.size())];
         if (m.is_bool(e)) {
+            auto v = ctx.atom2bool_var(e);
+            if (ctx.is_unit(v))
+                return false    ;
             TRACE("bv", tout << "random flip " << mk_bounded_pp(e, m) << "\n";);
-            ctx.flip(ctx.atom2bool_var(e));
+            ctx.flip(v);
             return true;
         }
         SASSERT(bv.is_bv(e));
@@ -126,7 +129,10 @@ namespace sls {
         expr* e = vars[ctx.rand(vars.size())];
         if (m.is_bool(e)) {
             TRACE("bv", tout << "random move flip " << mk_bounded_pp(e, m) << "\n";);
-            ctx.flip(ctx.atom2bool_var(e));
+            auto v = ctx.atom2bool_var(e);
+            if (ctx.is_unit(v))
+                return false;
+            ctx.flip(v);
             return true;
         }
         SASSERT(bv.is_bv(e));
@@ -370,6 +376,8 @@ namespace sls {
     }
 
     double bv_lookahead::lookahead_flip(sat::bool_var v) {
+        if (ctx.is_unit(v))
+            return -100;
         auto a = ctx.atom(v);
         return lookahead_update(a, m_v_updated);
     }
@@ -541,6 +549,8 @@ namespace sls {
                     auto v = ctx.atom2bool_var(e);
                     auto v1 = m_ev.bval1(to_app(e));
                     if (v != sat::null_bool_var) {
+                        if (ctx.is_unit(v))
+                            continue;
                         if (ctx.is_true(v) == v1)
                             continue;
                         TRACE("bv", tout << "update flip " << mk_bounded_pp(e, m) << "\n";);
diff --git a/src/ast/sls/sls_context.cpp b/src/ast/sls/sls_context.cpp
index 74b2eccb8..f67f056b6 100644
--- a/src/ast/sls/sls_context.cpp
+++ b/src/ast/sls/sls_context.cpp
@@ -505,7 +505,7 @@ namespace sls {
             if (clause.m_clause.size() == 1) 
                 m_unit_literals.push_back(clause.m_clause[0]);
         for (sat::literal lit : m_unit_literals)
-            m_unit_indices.insert(lit.index());
+            m_unit_indices.insert(lit.var());
             
         IF_VERBOSE(3, verbose_stream() << "UNITS " << m_unit_literals << "\n");
         for (unsigned i = 0; i < m_atoms.size(); ++i)
diff --git a/src/ast/sls/sls_context.h b/src/ast/sls/sls_context.h
index 5ff1fd052..3eca47726 100644
--- a/src/ast/sls/sls_context.h
+++ b/src/ast/sls/sls_context.h
@@ -181,7 +181,8 @@ namespace sls {
         unsigned rand(unsigned n) { return m_rand(n); }
         sat::literal_vector const& root_literals() const { return m_root_literals; }
         sat::literal_vector const& unit_literals() const { return m_unit_literals; }
-        bool is_unit(sat::literal lit) const { return m_unit_indices.contains(lit.index()); }
+        bool is_unit(sat::literal lit) const { return is_unit(lit.var()); }
+        bool is_unit(sat::bool_var v) const { return m_unit_indices.contains(v); }
         void reinit_relevant();
         void force_restart() { s.force_restart(); }
         bool include_func_interp(func_decl* f) const { return any_of(m_plugins, [&](plugin* p) { return p && p->include_func_interp(f); }); }