add placeholder for simplification

src/math/polysat/CMakeLists.txt

@@ -13,6 +13,7 @@ z3_add_component(polysat
     mul_ovfl_constraint.cpp
     saturation.cpp
     search_state.cpp
+    simplify.cpp
     solver.cpp
     ule_constraint.cpp
     viable.cpp

src/math/polysat/explain.cpp

@@ -149,8 +149,8 @@ namespace polysat {
             LOG("try-reduce: " << c << " " << c.is_currently_false(s));
             if (!c->is_ule())
                 continue;
-            auto lhs = c->to_ule().lhs();
-            auto rhs = c->to_ule().rhs();
+            auto const& lhs = c->to_ule().lhs();
+            auto const& rhs = c->to_ule().rhs();
             auto a = lhs.reduce(v, p);
             auto b = rhs.reduce(v, p);
             LOG("try-reduce: " << c << " " << a << " " << b << " vs " << lhs << " " << rhs);

src/math/polysat/simplify.cpp

@@ -0,0 +1,54 @@
+/*++
+Copyright (c) 2021 Microsoft Corporation
+
+Module Name:
+
+    Simplification
+
+Author:
+
+    Jakob Rath, Nikolaj Bjorner (nbjorner) 2021-12-12
+
+Notes:
+
+This is a place holder for simplification.
+
+- Replace literals of the form p < 1 (which is ~(p >= 1)) by p <= 0
+
+- Rewrite clauses using factoring and normalization rules
+
+  - p*q <= 0 or C
+    -> p <= 0 or C, q <= 0 or C
+
+  - ovfl(1, x) or C 
+    -> C
+
+- Drop redundant literals from lemmas.
+
+- Generalize lemmas by replacing equalities or destructive resolution.
+
+  - x = k => C[x]
+    - C[k]
+
+  - x = k & y = k' => ax + by <= c
+    - lo <= x <= k & lo' <= y <= k' => ax + by <= c
+
+  
+--*/
+#pragma once
+#include "math/polysat/solver.h"
+#include "math/polysat/simplify.h"
+
+namespace polysat {
+
+    simplify::simplify(solver& s):
+        s(s)
+    {}
+
+    bool simplify::should_apply() const { 
+        return false; 
+    }
+
+    void simplify::operator()() {}
+
+}

src/math/polysat/simplify.h

@@ -0,0 +1,31 @@
+/*++
+Copyright (c) 2021 Microsoft Corporation
+
+Module Name:
+
+    Simplification
+
+Author:
+
+    Jakob Rath, Nikolaj Bjorner (nbjorner) 2021-12-12
+
+--*/
+#pragma once
+#include "math/polysat/constraint.h"
+
+namespace polysat {
+
+    class solver;
+
+    class simplify {
+        solver& s;
+
+    public:
+        simplify(solver& s);
+
+        bool should_apply() const;
+
+        void operator()();
+    };
+
+}

src/math/polysat/solver.cpp

@@ -34,6 +34,7 @@ namespace polysat {
         m_viable(*this),
         m_linear_solver(*this),
         m_conflict(*this),
+        m_simplify(*this),
         m_forbidden_intervals(*this),
         m_bvars(),
         m_free_pvars(m_activity),
@@ -73,7 +74,7 @@ namespace polysat {
             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 (should_simplify()) simplify();
+            else if (m_simplify.should_apply()) m_simplify();
             else if (should_restart()) restart();
             else decide();
         }
@@ -251,17 +252,6 @@ namespace polysat {
 #endif
     }
 
-    /*
-    * This is a place holder for in-processing simplification
-    */
-    bool solver::should_simplify() {
-        return false;
-    }
-
-    void solver::simplify() {
-
-    }
-
     /*
     * Basic restart functionality.
     * restarts make more sense when the order of variable 

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.h"
 #include "math/polysat/explain.h"
 #include "math/polysat/ule_constraint.h"
 #include "math/polysat/justification.h"
@@ -59,6 +60,7 @@ namespace polysat {
         friend class clause_builder;
         friend class conflict;
         friend class conflict_explainer;
+        friend class simplify;
         friend class explainer;
         friend class inference_engine;
         friend class forbidden_intervals;
@@ -78,7 +80,8 @@ namespace polysat {
         scoped_ptr_vector<dd::pdd_manager> m_pdd;
         viable                   m_viable;   // viable sets per variable
         linear_solver            m_linear_solver;
-        conflict                 m_conflict;        
+        conflict                 m_conflict; 
+        simplify                 m_simplify;
         forbidden_intervals      m_forbidden_intervals;
         bool_var_manager         m_bvars;       // Map boolean variables to constraints
         var_queue                m_free_pvars;  // free poly vars
@@ -201,9 +204,6 @@ namespace polysat {
         void backjump(unsigned new_level);
         void add_lemma(clause& lemma);
 
-        bool should_simplify();
-        void simplify();
-
         unsigned m_conflicts_at_restart = 0;
         unsigned m_restart_threshold = 100;
         unsigned m_restart_init = 100;

src/test/polysat.cpp

@@ -1078,7 +1078,7 @@ namespace polysat {
                 std::cout << "SKIP: " << mk_pp(fm, m) << "\n";            
             }
         }
-        for (auto [k,v] : expr2pdd)
+        for (auto const& [k,v] : expr2pdd)
             dealloc(v);
     }
 }
@@ -1193,7 +1193,7 @@ void tst_polysat_argv(char** argv, int argc, int& i) {
     ast_manager& m = ctx.m();
     ctx.set_ignore_check(true);
     VERIFY(parse_smt2_commands(ctx, is));
-    auto fmls = ctx.assertions();
+    ptr_vector<expr> fmls = ctx.assertions();
     polysat::scoped_solver s("polysat");
     g_solver = &s;
     polysat::internalize(m, s, fmls);