From 53f276d225ca795e07265d611429b75eb8cd5112 Mon Sep 17 00:00:00 2001
From: Jakob Rath <git@jakobrath.eu>
Date: Mon, 22 Aug 2022 12:44:56 +0200
Subject: [PATCH] apply

---
 src/math/polysat/simplify_clause.cpp | 5 +++++
 src/math/polysat/simplify_clause.h   | 2 ++
 src/math/polysat/solver.cpp          | 4 +++-
 src/math/polysat/solver.h            | 3 +++
 4 files changed, 13 insertions(+), 1 deletion(-)

diff --git a/src/math/polysat/simplify_clause.cpp b/src/math/polysat/simplify_clause.cpp
index 60c2b0614..b8de97dae 100644
--- a/src/math/polysat/simplify_clause.cpp
+++ b/src/math/polysat/simplify_clause.cpp
@@ -21,4 +21,9 @@ namespace polysat {
         s(s)
     {}
 
+    bool simplify_clause::apply(clause& cl)
+    {
+        (void)s;
+        return false;
+    }
 }
diff --git a/src/math/polysat/simplify_clause.h b/src/math/polysat/simplify_clause.h
index 599b24b94..4b60399a2 100644
--- a/src/math/polysat/simplify_clause.h
+++ b/src/math/polysat/simplify_clause.h
@@ -22,6 +22,8 @@ namespace polysat {
 
     public:
         simplify_clause(solver& s);
+
+        bool apply(clause& cl);
     };
 
 }
diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp
index 632242b71..25c62e78e 100644
--- a/src/math/polysat/solver.cpp
+++ b/src/math/polysat/solver.cpp
@@ -12,7 +12,7 @@ Abstract:
 Author:
 
     Nikolaj Bjorner (nbjorner) 2021-03-19
-    Jakob Rath 2021-04-6
+    Jakob Rath 2021-04-06
 
 --*/
 
@@ -33,6 +33,7 @@ namespace polysat {
         m_viable_fallback(*this),
         m_linear_solver(*this),
         m_conflict(*this),
+        m_simplify_clause(*this),
         m_simplify(*this),
         m_restart(*this),
         m_bvars(),
@@ -825,6 +826,7 @@ namespace polysat {
     void solver::learn_lemma(clause& lemma) {
         LOG("Learning: "<< lemma);
         SASSERT(!lemma.empty());
+        m_simplify_clause.apply(lemma);
         add_clause(lemma);
         // TODO: add pwatch?
     }
diff --git a/src/math/polysat/solver.h b/src/math/polysat/solver.h
index 418f08080..98bda894f 100644
--- a/src/math/polysat/solver.h
+++ b/src/math/polysat/solver.h
@@ -24,6 +24,7 @@ Author:
 #include "math/polysat/conflict.h"
 #include "math/polysat/constraint.h"
 #include "math/polysat/clause_builder.h"
+#include "math/polysat/simplify_clause.h"
 #include "math/polysat/simplify.h"
 #include "math/polysat/restart.h"
 #include "math/polysat/explain.h"
@@ -69,6 +70,7 @@ namespace polysat {
         friend class clause_builder;
         friend class conflict;
         friend class conflict_explainer;
+        friend class simplify_clause;
         friend class simplify;
         friend class restart;
         friend class explainer;
@@ -99,6 +101,7 @@ namespace polysat {
         viable_fallback          m_viable_fallback;   // fallback for viable, using bitblasting over univariate constraints
         linear_solver            m_linear_solver;
         conflict                 m_conflict; 
+        simplify_clause          m_simplify_clause;
         simplify                 m_simplify;
         restart                  m_restart;
         bool_var_manager         m_bvars;       // Map boolean variables to constraints