adding ema

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

src/sat/sat_solver.cpp

@@ -1415,7 +1415,7 @@ namespace sat {
             return l_false;
         if (m_conflicts_since_init > m_config.m_max_conflicts) 
             return l_undef;
-        if (m_conflicts_since_restart > m_restart_threshold) 
+        if (should_restart()) 
             return l_undef;
         if (at_base_lvl()) {
             cleanup(); // cleaner may propagate frozen clauses
@@ -1828,6 +1828,10 @@ namespace sat {
         return ok;
     }
 
+    bool solver::should_restart() const {
+        return m_conflicts_since_restart > m_restart_threshold;
+    }
+
     void solver::restart(bool to_base) {
         m_stats.m_restart++;
         m_restarts++;

src/sat/sat_solver.h

@@ -416,6 +416,7 @@ namespace sat {
         void mk_model();
         bool check_model(model const & m) const;
         void restart(bool to_base);
+        bool should_restart() const;
         void sort_watch_lits();
         void exchange_par();
         lbool check_par(unsigned num_lits, literal const* lits);

src/test/sat_local_search.cpp

@@ -17,12 +17,11 @@ static bool build_instance(char const * filename, sat::solver& s, sat::local_sea
         return false;
     }
     infile.getline(line, 16383);
-    int num_vars, num_constraints;
 #ifdef _WINDOWS
+    int num_vars = 0, num_constraints = 0;
     sscanf_s(line, "%d %d", &num_vars, &num_constraints);
 #else
     return false;
-#endif
     //std::cout << "number of variables: " << num_vars << '\n';
     //std::cout << "number of constraints: " << num_constraints << '\n';
 
@@ -70,6 +69,7 @@ static bool build_instance(char const * filename, sat::solver& s, sat::local_sea
 
     infile.close();
     return true;
+#endif
 }
 
 void tst_sat_local_search(char ** argv, int argc, int& i) {

src/util/ema.h

@@ -0,0 +1,44 @@
+/*++
+Copyright (c) 2018 Microsoft Corporation
+
+Module Name:
+
+    ema.h
+
+Abstract:
+
+    Exponential moving average in the style of CaDiCal.
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2018-05-03
+
+Revision History:
+
+--*/
+#ifndef EMA_H_
+#define EMA_H_
+
+class ema {
+    double m_alpha, m_beta, m_value;
+    unsigned m_period, m_wait;
+
+ public:
+    ema() { memset(this, 0, sizeof(*this)); }
+
+    ema(double alpha): 
+        m_alpha(alpha), m_beta(1), m_value(0), 
+        m_period(0), m_wait(0) {}
+
+    double operator() const { return m_value; }
+
+    void update(double x) {
+        m_value += m_beta * (x - m_value);
+        if (m_beta <= m_alpha || m_wait--) return;
+        m_wait = m_period = 2*(m_period + 1) - 1;
+        m_beta *= 0.5;
+        if (m_beta < m_alpha) m_beta = m_alpha;        
+    }
+};
+
+#endif

src/util/sorting_network.h

@@ -371,6 +371,9 @@ Notes:
                 break;
             case ordered_at_most_1:
                 return mk_ordered_exactly_1(full, n, xs);
+            default:
+                UNREACHABLE();
+                return mk_ordered_exactly_1(full, n, xs);                
             }
 
             if (full) {