add parameter to control congruence terms in slicing

src/math/polysat/polysat_params.pyg

@@ -6,5 +6,6 @@ def_module_params('polysat',
         ('max_decisions', UINT, UINT_MAX, "maximum number of decisions before giving up"),
         ('log', UINT, UINT_MAX, "polysat logging filter (enable logging in iteration N)"),
         ('log_conflicts', BOOL, False, "log conflicts"),
+        ('slicing.congruence', BOOL, False, "bitvector slicing: add virtual congruence terms"),
     )
 )

src/math/polysat/slicing.cpp

@@ -332,6 +332,8 @@ namespace polysat {
     }
 
     void slicing::update_var_congruences() {
+        if (!m_solver.config().m_slicing_congruence)
+            return;
         for (pvar v : m_needs_congruence)
             add_congruence(v);
         m_needs_congruence.reset();

src/math/polysat/solver.cpp

@@ -82,6 +82,7 @@ namespace polysat {
         m_config.m_max_decisions = pp.max_decisions();
         m_config.m_log_iteration = pp.log();
         m_config.m_log_conflicts = pp.log_conflicts();
+        m_config.m_slicing_congruence = pp.slicing_congruence();
 
         // TODO: log filter to enable/disable based on submodules
         if (m_config.m_log_iteration == 0)

src/math/polysat/solver.h

@@ -48,6 +48,7 @@ namespace polysat {
         uint64_t    m_max_decisions = std::numeric_limits<uint64_t>::max();
         unsigned    m_log_iteration = UINT_MAX;
         bool        m_log_conflicts = false;
+        bool        m_slicing_congruence = false;
     };
 
     /**