From afa7162ab18f43d27c919067ff7cc7d7e6c71fd7 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 12 Apr 2022 10:35:23 +0200
Subject: [PATCH] add parameter class for polysat

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/math/polysat/CMakeLists.txt     |  2 ++
 src/math/polysat/polysat_params.pyg |  6 ++++++
 src/math/polysat/solver.cpp         | 13 ++++++++-----
 src/math/polysat/solver.h           | 12 +++++++++---
 4 files changed, 25 insertions(+), 8 deletions(-)
 create mode 100644 src/math/polysat/polysat_params.pyg

diff --git a/src/math/polysat/CMakeLists.txt b/src/math/polysat/CMakeLists.txt
index d387a1a5c..b5a36967a 100644
--- a/src/math/polysat/CMakeLists.txt
+++ b/src/math/polysat/CMakeLists.txt
@@ -28,4 +28,6 @@ z3_add_component(polysat
     simplex
     interval
     bigfix
+ PYG_FILES
+    polysat_params.pyg
 )
diff --git a/src/math/polysat/polysat_params.pyg b/src/math/polysat/polysat_params.pyg
new file mode 100644
index 000000000..8cd824a3a
--- /dev/null
+++ b/src/math/polysat/polysat_params.pyg
@@ -0,0 +1,6 @@
+def_module_params('polysat', 
+                  description='polysat solver',
+                  export=True,
+                  params=(('log_conflicts', BOOL, True, "log conflicts"),
+                          ))         
+                
diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp
index 868a57526..b2b8e3591 100644
--- a/src/math/polysat/solver.cpp
+++ b/src/math/polysat/solver.cpp
@@ -20,6 +20,7 @@ Author:
 #include "math/polysat/explain.h"
 #include "math/polysat/log.h"
 #include "math/polysat/variable_elimination.h"
+#include "math/polysat/polysat_params.hpp"
 
 // For development; to be removed once the linear solver works well enough
 #define ENABLE_LINEAR_SOLVER 0
@@ -48,16 +49,18 @@ namespace polysat {
     }
 
     void solver::updt_params(params_ref const& p) {
+        polysat_params pp(p);
         m_params.append(p);
-        m_max_conflicts = m_params.get_uint("max_conflicts", UINT_MAX);
-        m_max_decisions = m_params.get_uint("max_decisions", UINT_MAX);
+        m_config.m_max_conflicts = m_params.get_uint("max_conflicts", UINT_MAX);
+        m_config.m_max_decisions = m_params.get_uint("max_decisions", UINT_MAX);
+        m_config.m_log_conflicts = pp.log_conflicts();
     }
 
     bool solver::should_search() {
         return 
             m_lim.inc() && 
-            (m_stats.m_num_conflicts < m_max_conflicts) &&
-            (m_stats.m_num_decisions < m_max_decisions);
+            (m_stats.m_num_conflicts < get_config().m_max_conflicts) &&
+            (m_stats.m_num_decisions < get_config().m_max_decisions);
     }
    
     lbool solver::check_sat() {         
@@ -86,7 +89,7 @@ namespace polysat {
     lbool solver::unit_propagate() {
         return l_undef;
         // disabled to allow debugging unsoundness for watched literals
-        flet<uint64_t> _max_d(m_max_conflicts, m_stats.m_num_conflicts + 2);
+        flet<uint64_t> _max_d(m_config.m_max_conflicts, m_stats.m_num_conflicts + 2);
         return check_sat();
     }
 
diff --git a/src/math/polysat/solver.h b/src/math/polysat/solver.h
index 2daf0e15d..8093b4fbf 100644
--- a/src/math/polysat/solver.h
+++ b/src/math/polysat/solver.h
@@ -39,6 +39,12 @@ Author:
 
 namespace polysat {
 
+    struct config {
+        uint64_t                 m_max_conflicts = std::numeric_limits<uint64_t>::max();
+        uint64_t                 m_max_decisions = std::numeric_limits<uint64_t>::max();
+        bool                     m_log_conflicts = false;
+    };
+
     class solver {
 
         struct stats {
@@ -94,9 +100,7 @@ namespace polysat {
         var_queue                m_free_pvars;  // free poly vars
         stats                    m_stats;
 
-        uint64_t                 m_max_conflicts = std::numeric_limits<uint64_t>::max();
-        uint64_t                 m_max_decisions = std::numeric_limits<uint64_t>::max();
-
+        config                   m_config;
         // Per constraint state
         constraint_manager       m_constraints;
 
@@ -402,6 +406,8 @@ namespace polysat {
 
         void updt_params(params_ref const& p);
 
+        config const& get_config() const { return m_config; }
+
     };  // class solver
 
     class assignments_pp {