fix build

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

src/CMakeLists.txt

@@ -56,12 +56,12 @@ add_subdirectory(parsers/util)
 add_subdirectory(math/grobner)
 add_subdirectory(math/euclid)
 add_subdirectory(tactic/core)
-add_subdirectory(sat/tactic)
-add_subdirectory(tactic/arith)
-add_subdirectory(nlsat/tactic)
 add_subdirectory(math/subpaving/tactic)
 add_subdirectory(tactic/aig)
 add_subdirectory(solver)
+add_subdirectory(sat/tactic)
+add_subdirectory(tactic/arith)
+add_subdirectory(nlsat/tactic)
 add_subdirectory(ackermannization)
 add_subdirectory(interp)
 add_subdirectory(cmd_context)

src/sat/ba_solver.h

@@ -242,10 +242,10 @@ namespace sat {
         unsigned_vector   m_pb_undef;
 
         struct ba_sort {
-            ba_solver& s;
             typedef typename sat::literal literal;
             typedef typename sat::literal_vector literal_vector;
 
+            ba_solver& s;
             literal m_true;
             literal_vector m_lits;
             

src/sat/sat_allocator.h

@@ -90,6 +90,8 @@ public:
         }
     }
     size_t get_allocation_size() const { return m_alloc_size; }
+
+    char const* id() const { return m_id; }
 };
 
 inline void * operator new(size_t s, sat_allocator & r) { return r.allocate(s); }

src/sat/sat_solver.cpp

@@ -38,9 +38,9 @@ namespace sat {
         m_config(p),
         m_par(nullptr),
         m_cls_allocator_idx(false),
-        m_par_syncing_clauses(false),
-        m_par_id(0),
         m_cleaner(*this),
+        m_par_id(0),
+        m_par_syncing_clauses(false),
         m_simplifier(*this, p),
         m_scc(*this, p),
         m_asymm_branch(*this, p),
@@ -487,8 +487,6 @@ namespace sat {
         return reinit;
     }
 
-    static unsigned s_count = 0;
-
     void solver::attach_clause(clause & c, bool & reinit) {
         SASSERT(c.size() > 2);
         reinit = false;
@@ -1332,7 +1330,6 @@ namespace sat {
                 next = m_case_split_queue.min_var();
                 auto age = m_stats.m_conflict - m_canceled[next];
                 while (age > 0) {
-                    double decay = pow(0.95, age);
                     m_activity[next] = static_cast<unsigned>(m_activity[next] * pow(0.95, age));
                     m_case_split_queue.activity_changed_eh(next, false);
                     m_canceled[next] = m_stats.m_conflict;

src/sat/tactic/CMakeLists.txt

@@ -6,6 +6,7 @@ z3_add_component(sat_tactic
   COMPONENT_DEPENDENCIES
     sat
     tactic
+    solver
   TACTIC_HEADERS
     sat_tactic.h
 )

src/tactic/core/split_clause_tactic.cpp

@@ -46,11 +46,10 @@ class split_clause_tactic : public tactic {
     }
 
     class split_pc : public proof_converter {
-        ast_manager & m;
         app_ref       m_clause;
         proof_ref     m_clause_pr;
     public:
-        split_pc(ast_manager & m, app * cls, proof * pr):m(m), m_clause(cls, m), m_clause_pr(pr, m) {
+        split_pc(ast_manager & m, app * cls, proof * pr):m_clause(cls, m), m_clause_pr(pr, m) {
         }
 
         ~split_pc() override { }

src/tactic/generic_model_converter.cpp

@@ -188,8 +188,6 @@ void generic_model_converter::get_units(obj_map<expr, bool>& units) {
     th_rewriter rw(m);
     expr_safe_replace rep(m);
     expr_ref tmp(m);
-    bool val = false;
-    expr* f = nullptr;
     for (auto const& kv : units) {
         rep.insert(kv.m_key, kv.m_value ? m.mk_true() : m.mk_false());
     }

src/tactic/sine_filter.cpp

@@ -36,14 +36,14 @@ public:
     sine_tactic(ast_manager& m, params_ref const& p):
         m(m), m_params(p) {}
 
-    virtual tactic * translate(ast_manager & m) {
+    tactic * translate(ast_manager & m) override {
         return alloc(sine_tactic, m, m_params);
     }
 
-    virtual void updt_params(params_ref const & p) {
+    void updt_params(params_ref const & p) override {
     }
 
-    virtual void collect_param_descrs(param_descrs & r) {
+    void collect_param_descrs(param_descrs & r) override {
     }
 
     void operator()(goal_ref const & g, goal_ref_buffer& result) override {
@@ -63,7 +63,7 @@ public:
         SASSERT(g->is_well_sorted());
     }
 
-    virtual void cleanup() {
+    void cleanup() override {
     }
 
 private:

src/tactic/tactical.cpp

@@ -103,7 +103,6 @@ public:
 
     void operator()(goal_ref const & in, goal_ref_buffer& result) override { 
 
-        bool models_enabled = in->models_enabled();
         bool proofs_enabled = in->proofs_enabled();
         bool cores_enabled  = in->unsat_core_enabled();
 
@@ -513,7 +512,6 @@ public:
 
         // enabling proofs is possible, but requires translating subgoals back.
         fail_if_proof_generation("par_and_then", in);
-        bool models_enabled = in->models_enabled();
         bool proofs_enabled = in->proofs_enabled();
         bool cores_enabled  = in->unsat_core_enabled();
 

src/util/util.cpp

@@ -20,6 +20,7 @@ Revision History:
 #ifdef _WINDOWS
 #include <windows.h>
 #endif
+#include <thread>
 #include "util/util.h"
 
 static unsigned g_verbosity_level = 0;
@@ -38,7 +39,11 @@ void set_verbose_stream(std::ostream& str) {
     g_verbose_stream = &str;
 }
 
+#ifdef _WINDOWS
 static int g_thread_id = 0;
+#else
+static std::thread::id g_thread_id = std::this_thread::get_id();
+#endif
 static bool g_is_threaded = false;
 
 bool is_threaded() {
@@ -47,6 +52,8 @@ bool is_threaded() {
     int thid = GetCurrentThreadId();
     g_is_threaded = g_thread_id != thid && g_thread_id != 0;
     g_thread_id = thid;
+#else
+    g_is_threaded = std::this_thread::get_id() != g_thread_id;
 #endif
     return g_is_threaded;
 }