From 5339a2f70f40ca37bc63f211e6aa654b04287149 Mon Sep 17 00:00:00 2001
From: Jakob Rath <git@jakobrath.eu>
Date: Wed, 20 Mar 2024 10:16:40 +0100
Subject: [PATCH] Don't access solver_interface directly

---
 src/sat/smt/polysat/core.cpp   | 4 ++++
 src/sat/smt/polysat/core.h     | 3 ++-
 src/sat/smt/polysat/viable.cpp | 2 +-
 3 files changed, 7 insertions(+), 2 deletions(-)

diff --git a/src/sat/smt/polysat/core.cpp b/src/sat/smt/polysat/core.cpp
index 23cdcc24c..61f52ab59 100644
--- a/src/sat/smt/polysat/core.cpp
+++ b/src/sat/smt/polysat/core.cpp
@@ -504,6 +504,10 @@ namespace polysat {
         s.get_bitvector_sub_slices(v, out);
     }
 
+    void core::get_fixed_subslices(pvar v, fixed_bits_vector& fixed_subslices) {
+        s.get_fixed_sub_slices(v, fixed_subslices);
+    }
+
     pdd core::mk_zero_extend(unsigned sz, pdd const& p) { 
         if (p.is_val()) 
             return value(p.val(), p.manager().power_of_2() + sz);        
diff --git a/src/sat/smt/polysat/core.h b/src/sat/smt/polysat/core.h
index d3290dedc..30e50b534 100644
--- a/src/sat/smt/polysat/core.h
+++ b/src/sat/smt/polysat/core.h
@@ -168,8 +168,9 @@ namespace polysat {
         * Viable 
         */
         void get_bitvector_suffixes(pvar v, offset_slices& out);
-        void get_fixed_bits(pvar v, fixed_bits_vector& fixed_slice);
+        void get_fixed_bits(pvar v, fixed_bits_vector& fixed_slices);
         void get_subslices(pvar v, offset_slices& out);
+        void get_fixed_subslices(pvar v, fixed_bits_vector& fixed_subslices);
         pdd  mk_zero_extend(unsigned sz, pdd const& p);
         pdd  mk_extract(unsigned hi, unsigned lo, pdd const& p);
 
diff --git a/src/sat/smt/polysat/viable.cpp b/src/sat/smt/polysat/viable.cpp
index 026d191f0..25602c149 100644
--- a/src/sat/smt/polysat/viable.cpp
+++ b/src/sat/smt/polysat/viable.cpp
@@ -691,7 +691,7 @@ namespace polysat {
         //       although, the max admissible level of fixed slices depends on the child pvar under consideration, so we may not get the optimal interval anymore?
         //       (pvars on the same slice only differ by level. the fixed value is the same for all. so we can limit by the max level of pvars and then the projection will work for at least one.)
         fixed_bits_vector fixed;
-        c.s.get_fixed_sub_slices(e->var, fixed);   // TODO: move into m_fixed bits?
+        c.get_fixed_subslices(e->var, fixed);
 
         bool has_pvar = any_of(fixed, [](fixed_slice const& f) { return f.child != null_var; });