From 586ffdf40261b16ec2f4a4e62d2cbfa16bd6e644 Mon Sep 17 00:00:00 2001
From: Jakob Rath <git@jakobrath.eu>
Date: Mon, 7 Nov 2022 14:04:28 +0100
Subject: [PATCH] Remove unnecessary argument

---
 src/math/polysat/conflict.cpp           |  2 +-
 src/math/polysat/constraint_manager.cpp | 20 ++++++++++----------
 src/math/polysat/constraint_manager.h   | 12 ++++++------
 src/math/polysat/solver.cpp             |  4 ++--
 4 files changed, 19 insertions(+), 19 deletions(-)

diff --git a/src/math/polysat/conflict.cpp b/src/math/polysat/conflict.cpp
index 949474ac7..7bcc34d8a 100644
--- a/src/math/polysat/conflict.cpp
+++ b/src/math/polysat/conflict.cpp
@@ -600,7 +600,7 @@ namespace polysat {
                 if (needs_side_lemma(lit2))
                     todo.push_back(lit2);
             // Store and bool-propagate the lemma
-            s.m_constraints.store(lemma, s, false);
+            s.m_constraints.store(lemma, false);
             SASSERT(s.m_bvars.value(lit) != l_undef);
         }
         m_lemmas.reset();
diff --git a/src/math/polysat/constraint_manager.cpp b/src/math/polysat/constraint_manager.cpp
index 53695495d..078d92aaf 100644
--- a/src/math/polysat/constraint_manager.cpp
+++ b/src/math/polysat/constraint_manager.cpp
@@ -68,15 +68,15 @@ namespace polysat {
     }
 
 
-    void constraint_manager::register_clause(clause* cl, solver& s) {
+    void constraint_manager::register_clause(clause* cl) {
         while (m_clauses.size() <= s.base_level())
             m_clauses.push_back({});
         m_clauses[s.base_level()].push_back(cl);
     }
 
-    void constraint_manager::store(clause* cl, solver& s, bool value_propagate) {
-        register_clause(cl, s);
-        watch(*cl, s, value_propagate);
+    void constraint_manager::store(clause* cl, bool value_propagate) {
+        register_clause(cl);
+        watch(*cl, value_propagate);
     }
 
     // Release constraints at the given level and above.
@@ -94,7 +94,7 @@ namespace polysat {
     // if clause is unsat then assign arbitrary
     // solver handles unsat clauses by creating a conflict.
     // solver also can propagate, but need to check that it does indeed.
-    void constraint_manager::watch(clause& cl, solver& s, bool value_propagate) {
+    void constraint_manager::watch(clause& cl, bool value_propagate) {
         if (cl.empty())
             return;
 
@@ -168,18 +168,18 @@ namespace polysat {
         }
     }
 
-    void constraint_manager::gc(solver& s) {
+    void constraint_manager::gc() {
         LOG_H1("gc");
-        gc_clauses(s);
-        gc_constraints(s);
+        gc_clauses();
+        gc_constraints();
     }
 
-    void constraint_manager::gc_clauses(solver& s) {
+    void constraint_manager::gc_clauses() {
         LOG_H3("gc_clauses");
         // place to gc redundant clauses
     }
 
-    void constraint_manager::gc_constraints(solver& s) {
+    void constraint_manager::gc_constraints() {
         LOG_H3("gc_constraints");
         uint_set used_vars;
         for (auto const& cls : m_clauses)
diff --git a/src/math/polysat/constraint_manager.h b/src/math/polysat/constraint_manager.h
index 590a9d4ac..edc8849e6 100644
--- a/src/math/polysat/constraint_manager.h
+++ b/src/math/polysat/constraint_manager.h
@@ -63,13 +63,13 @@ namespace polysat {
 
         constraint* dedup(constraint* c);
 
-        void gc_constraints(solver& s);
-        void gc_clauses(solver& s);
+        void gc_constraints();
+        void gc_clauses();
 
-        void watch(clause& cl, solver& s, bool value_propagate);
+        void watch(clause& cl, bool value_propagate);
         void unwatch(clause& cl);
 
-        void register_clause(clause* cl, solver& s);
+        void register_clause(clause* cl);
 
         void ensure_bvar(constraint* c);
         void erase_bvar(constraint* c);
@@ -78,13 +78,13 @@ namespace polysat {
         constraint_manager(solver& s);
         ~constraint_manager();
 
-        void store(clause* cl, solver& s, bool value_propagate);
+        void store(clause* cl, bool value_propagate);
 
         /// Release clauses at the given level and above.
         void release_level(unsigned lvl);
 
         /// Garbage-collect temporary constraints (i.e., those that do not have a boolean variable).
-        void gc(solver& s);
+        void gc();
         bool should_gc();
 
         constraint* lookup(sat::bool_var var) const;
diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp
index 6d0d068fa..c211d5c01 100644
--- a/src/math/polysat/solver.cpp
+++ b/src/math/polysat/solver.cpp
@@ -73,7 +73,7 @@ namespace polysat {
             else if (is_conflict()) resolve_conflict();
             else if (can_propagate()) propagate();
             else if (!can_decide()) { LOG_H2("SAT"); SASSERT(verify_sat()); return l_true; }
-            else if (m_constraints.should_gc()) m_constraints.gc(*this);
+            else if (m_constraints.should_gc()) m_constraints.gc();
             else if (m_simplify.should_apply()) m_simplify();
             else if (m_restart.should_apply()) m_restart();
             else decide();
@@ -1006,7 +1006,7 @@ namespace polysat {
             }
         }
         SASSERT(!clause.empty());
-        m_constraints.store(&clause, *this, true);
+        m_constraints.store(&clause, true);
 
         if (!clause.is_redundant()) {
             // for (at least) non-redundant clauses, we also need to watch the constraints