Add clause simplification stub

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
 )

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)
+    {}
+
+}

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);
+    };
+
+}