From bf1a7914cdf520b09420af51e8a6c4f3d861d96a Mon Sep 17 00:00:00 2001
From: Jakob Rath <git@jakobrath.eu>
Date: Mon, 22 Aug 2022 12:36:05 +0200
Subject: [PATCH] Add clause simplification stub

---
 src/math/polysat/CMakeLists.txt      |  3 ++-
 src/math/polysat/simplify_clause.cpp | 24 ++++++++++++++++++++++++
 src/math/polysat/simplify_clause.h   | 27 +++++++++++++++++++++++++++
 3 files changed, 53 insertions(+), 1 deletion(-)
 create mode 100644 src/math/polysat/simplify_clause.cpp
 create mode 100644 src/math/polysat/simplify_clause.h

diff --git a/src/math/polysat/CMakeLists.txt b/src/math/polysat/CMakeLists.txt
index c18ca7189..6bc17c650 100644
--- a/src/math/polysat/CMakeLists.txt
+++ b/src/math/polysat/CMakeLists.txt
@@ -16,6 +16,7 @@ z3_add_component(polysat
     saturation.cpp
     search_state.cpp
     simplify.cpp
+    simplify_clause.cpp
     smul_fl_constraint.cpp
     solver.cpp
     ule_constraint.cpp
@@ -28,6 +29,6 @@ z3_add_component(polysat
     simplex
     interval
     bigfix
- PYG_FILES
+  PYG_FILES
     polysat_params.pyg
 )
diff --git a/src/math/polysat/simplify_clause.cpp b/src/math/polysat/simplify_clause.cpp
new file mode 100644
index 000000000..60c2b0614
--- /dev/null
+++ b/src/math/polysat/simplify_clause.cpp
@@ -0,0 +1,24 @@
+/*++
+Copyright (c) 2022 Microsoft Corporation
+
+Module Name:
+
+    Clause Simplification
+
+Author:
+
+    Jakob Rath, Nikolaj Bjorner (nbjorner) 2022-08-22
+
+Notes:
+
+--*/
+#include "math/polysat/solver.h"
+#include "math/polysat/simplify_clause.h"
+
+namespace polysat {
+
+    simplify_clause::simplify_clause(solver& s):
+        s(s)
+    {}
+
+}
diff --git a/src/math/polysat/simplify_clause.h b/src/math/polysat/simplify_clause.h
new file mode 100644
index 000000000..599b24b94
--- /dev/null
+++ b/src/math/polysat/simplify_clause.h
@@ -0,0 +1,27 @@
+/*++
+Copyright (c) 2022 Microsoft Corporation
+
+Module Name:
+
+    Clause Simplification
+
+Author:
+
+    Jakob Rath, Nikolaj Bjorner (nbjorner) 2022-08-22
+
+--*/
+#pragma once
+#include "math/polysat/constraint.h"
+
+namespace polysat {
+
+    class solver;
+
+    class simplify_clause {
+        solver& s;
+
+    public:
+        simplify_clause(solver& s);
+    };
+
+}