From f2d1ed7b07e43e73950f9a766e6ce9ce06b65d03 Mon Sep 17 00:00:00 2001
From: Jakob Rath <git@jakobrath.eu>
Date: Tue, 1 Aug 2023 14:13:59 +0200
Subject: [PATCH] add parameter to control congruence terms in slicing

---
 src/math/polysat/polysat_params.pyg | 1 +
 src/math/polysat/slicing.cpp        | 2 ++
 src/math/polysat/solver.cpp         | 1 +
 src/math/polysat/solver.h           | 1 +
 4 files changed, 5 insertions(+)

diff --git a/src/math/polysat/polysat_params.pyg b/src/math/polysat/polysat_params.pyg
index 9b55e8f10..9d60e3682 100644
--- a/src/math/polysat/polysat_params.pyg
+++ b/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"),
     )
 )
diff --git a/src/math/polysat/slicing.cpp b/src/math/polysat/slicing.cpp
index bd32bfed0..59a19ad67 100644
--- a/src/math/polysat/slicing.cpp
+++ b/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();
diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp
index db79ff5a5..f91565f86 100644
--- a/src/math/polysat/solver.cpp
+++ b/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)
diff --git a/src/math/polysat/solver.h b/src/math/polysat/solver.h
index 818483488..17696f30a 100644
--- a/src/math/polysat/solver.h
+++ b/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;
     };
 
     /**