From 37c9534d0477dd9b2d9d2c7c687f3a5b181b6307 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 9 Sep 2025 18:57:35 -0700
Subject: [PATCH] try per thread tree

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/smt/smt_parallel2.cpp | 50 +++++++++++++++++++++++++++++++++++++--
 src/smt/smt_parallel2.h   |  7 ++++++
 2 files changed, 55 insertions(+), 2 deletions(-)

diff --git a/src/smt/smt_parallel2.cpp b/src/smt/smt_parallel2.cpp
index 209988785..234ed7b6c 100644
--- a/src/smt/smt_parallel2.cpp
+++ b/src/smt/smt_parallel2.cpp
@@ -73,10 +73,15 @@ namespace smt {
         while (true) { 
             collect_shared_clauses(m_g2l);
 
+#if 0
             if (!b.get_cube(m_g2l, id, cube, node)) {
                 LOG_WORKER(1, " no more cubes\n");
                 return;
             }
+#else
+            if (!get_cube(cube, node))
+                return;
+#endif
 
         check_cube_start:
             LOG_WORKER(1, " CUBE SIZE IN MAIN LOOP: " << cube.size() << "\n");
@@ -97,7 +102,11 @@ namespace smt {
                     auto atom = get_split_atom();
                     if (!atom)
                         goto check_cube_start;
+#if 0
                     b.split(m_l2g, id, node, atom);
+#else
+                    split(node, atom);
+#endif
                     break;
                 }
                 case l_true: {
@@ -125,8 +134,12 @@ namespace smt {
                         if (asms.contains(e))
                             b.report_assumption_used(m_l2g, e); // report assumptions used in unsat core, so they can be used in final core
 
-                    LOG_WORKER(1, " found unsat cube\n");                    
+                    LOG_WORKER(1, " found unsat cube\n");    
+#if 0
                     b.backtrack(m_l2g, unsat_core, node);
+#else
+                    backtrack(unsat_core, node);
+#endif
                     break;
                 }
             }    
@@ -135,10 +148,43 @@ namespace smt {
         }
     }
 
+    bool parallel2::worker::get_cube(expr_ref_vector& cube, node*& n) {
+        node* t = m_search_tree.activate_node(n);
+        cube.reset();
+        if (!t) {
+            b.set_unsat(m_l2g, cube);
+            return false;
+        }
+        n = t;
+        while (t) {
+            if (cube_config::literal_is_null(t->get_literal()))
+                break;
+            cube.push_back(t->get_literal());
+            t = t->parent();
+        }
+        return true;
+    }
+
+    void parallel2::worker::backtrack(expr_ref_vector const& core, node* n) {
+        vector<expr_ref> core_copy;
+        for (auto c : core)
+            core_copy.push_back(expr_ref(c, m));
+        m_search_tree.backtrack(n, core_copy);
+        //LOG_WORKER(1, m_search_tree.display(verbose_stream() << bounded_pp_exprs(core) << "\n"););
+    }
+
+    void parallel2::worker::split(node* n, expr* atom) {
+        expr_ref lit(atom, m), nlit(m);
+        nlit = mk_not(m, lit);
+        IF_VERBOSE(1, verbose_stream() << "Batch manager splitting on literal: " << mk_bounded_pp(lit, m, 3) << "\n");
+        m_search_tree.split(n, lit, nlit);
+    }
+
     parallel2::worker::worker(unsigned id, parallel2& p, expr_ref_vector const& _asms): 
         id(id), p(p), b(p.m_batch_manager), m_smt_params(p.ctx.get_fparams()), asms(m),
         m_g2l(p.ctx.m, m),
-        m_l2g(m, p.ctx.m) {
+        m_l2g(m, p.ctx.m),
+        m_search_tree(expr_ref(m)) {
         for (auto e : _asms) 
             asms.push_back(m_g2l(e));
         LOG_WORKER(1, " created with " << asms.size() << " assumptions\n");        
diff --git a/src/smt/smt_parallel2.h b/src/smt/smt_parallel2.h
index b1983d192..345a398fa 100644
--- a/src/smt/smt_parallel2.h
+++ b/src/smt/smt_parallel2.h
@@ -64,6 +64,7 @@ namespace smt {
                 unsigned m_num_cubes = 0;
             };
 
+
             ast_manager& m;
             parallel2& p;
             std::mutex mux;
@@ -135,6 +136,8 @@ namespace smt {
                 bool m_cubetree = false;
             };
 
+            using node = search_tree::node<cube_config>;
+
             unsigned id; // unique identifier for the worker
             parallel2& p;
             batch_manager& b;
@@ -145,6 +148,7 @@ namespace smt {
             random_gen m_rand;
             scoped_ptr<context> ctx;
             ast_translation m_g2l, m_l2g;
+            search_tree::tree<cube_config> m_search_tree;
 
             unsigned m_num_shared_units = 0;
             unsigned m_num_initial_atoms = 0;
@@ -159,6 +163,9 @@ namespace smt {
                 m_config.m_threads_max_conflicts = (unsigned)(m_config.m_max_conflict_mul * m_config.m_threads_max_conflicts);
             } // allow for backoff scheme of conflicts within the thread for cube timeouts.
 
+            bool get_cube(expr_ref_vector& cube, node*& n);
+            void backtrack(expr_ref_vector const& core, node* n);
+            void split(node* n, expr* atom);
 
         public:
             worker(unsigned id, parallel2& p, expr_ref_vector const& _asms);