From 40f794c5b4247c21cf77145d988f73e226209470 Mon Sep 17 00:00:00 2001
From: Jakob Rath <git@jakobrath.eu>
Date: Thu, 15 Jun 2023 11:53:06 +0200
Subject: [PATCH] test stub

---
 src/math/polysat/solver.cpp |  5 ++++-
 src/math/polysat/solver.h   |  1 +
 src/test/slicing.cpp        | 20 ++++++++++++++++++++
 3 files changed, 25 insertions(+), 1 deletion(-)

diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp
index 42c6a843a..1e14a7b8f 100644
--- a/src/math/polysat/solver.cpp
+++ b/src/math/polysat/solver.cpp
@@ -42,7 +42,7 @@ namespace polysat {
         m_free_pvars(m_activity),
         m_constraints(*this),
         m_names(*this),
-        m_slicing(*this),
+        // m_slicing(*this),
         m_search(*this) {
     }
 
@@ -148,6 +148,7 @@ namespace polysat {
         m_trail.push_back(trail_instr_t::add_var_i);
         m_free_pvars.mk_var_eh(v);
         m_names.push_var(var(v));  // needs m_vars
+        m_slicing.add_var(sz);
         return v;
     }
 
@@ -612,6 +613,7 @@ namespace polysat {
     void solver::push_level() {
         ++m_level;
         m_reinit_heads.push_back(m_clauses_to_reinit.size());
+        m_slicing.push_scope();
         m_trail.push_back(trail_instr_t::inc_level_i);
     }
 
@@ -621,6 +623,7 @@ namespace polysat {
         SASSERT(m_level >= num_levels);
         unsigned const target_level = m_level - num_levels;
         LOG("Pop " << num_levels << " levels (lvl " << m_level << " -> " << target_level << ")");
+        m_slicing.pop_scope(num_levels);
         while (num_levels > 0) {
             switch (m_trail.back()) {
             case trail_instr_t::qhead_i: {
diff --git a/src/math/polysat/solver.h b/src/math/polysat/solver.h
index d46c87261..ddade9d2f 100644
--- a/src/math/polysat/solver.h
+++ b/src/math/polysat/solver.h
@@ -141,6 +141,7 @@ namespace polysat {
         friend class constraint_manager;
         friend class name_manager;
         friend class scoped_solverv;
+        friend class scoped_solver_slicing;
         friend class test_polysat;
         friend class test_fi;
         friend struct inf_resolve_evaluated;
diff --git a/src/test/slicing.cpp b/src/test/slicing.cpp
index b87b58651..20efb89dc 100644
--- a/src/test/slicing.cpp
+++ b/src/test/slicing.cpp
@@ -1,8 +1,27 @@
 #include "math/polysat/slicing.h"
+#include "math/polysat/solver.h"
 
 namespace polysat {
 
+    struct solver_scope_slicing {
+        reslimit lim;
+    };
+
+    class scoped_solver_slicing : public solver_scope_slicing, public solver {
+    public:
+        scoped_solver_slicing(): solver(lim) {}
+        slicing& sl() { return m_slicing; }
+    };
+
     class test_slicing {
+    public:
+
+        static void test1() {
+            std::cout << __func__ << "\n";
+            scoped_solver_slicing s;
+            slicing& sl = s.sl();
+            pvar x = s.add_var(8);
+        }
 
     };
 
@@ -11,5 +30,6 @@ namespace polysat {
 
 void tst_slicing() {
     using namespace polysat;
+    test_slicing::test1();
     std::cout << "ok\n";
 }