From e4d24fd2c35e2310318a4234a6b0c6bd2e51841c Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 1 May 2018 09:39:19 -0700 Subject: [PATCH] fix build Signed-off-by: Nikolaj Bjorner --- src/CMakeLists.txt | 6 +++--- src/sat/ba_solver.h | 2 +- src/sat/sat_allocator.h | 2 ++ src/sat/sat_solver.cpp | 7 ++----- src/sat/tactic/CMakeLists.txt | 1 + src/tactic/core/split_clause_tactic.cpp | 3 +-- src/tactic/generic_model_converter.cpp | 2 -- src/tactic/sine_filter.cpp | 8 ++++---- src/tactic/tactical.cpp | 2 -- src/util/util.cpp | 7 +++++++ 10 files changed, 21 insertions(+), 19 deletions(-) diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 5ed95b827..d8a773747 100644 --- a/src/CMakeLists.txt +++ b/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) diff --git a/src/sat/ba_solver.h b/src/sat/ba_solver.h index 303329594..14482eabb 100644 --- a/src/sat/ba_solver.h +++ b/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; diff --git a/src/sat/sat_allocator.h b/src/sat/sat_allocator.h index b4e9f82e6..06585ebed 100644 --- a/src/sat/sat_allocator.h +++ b/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); } diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index 1f3995d49..5b6fb628a 100644 --- a/src/sat/sat_solver.cpp +++ b/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(m_activity[next] * pow(0.95, age)); m_case_split_queue.activity_changed_eh(next, false); m_canceled[next] = m_stats.m_conflict; diff --git a/src/sat/tactic/CMakeLists.txt b/src/sat/tactic/CMakeLists.txt index fed6a89c8..dbbfbe753 100644 --- a/src/sat/tactic/CMakeLists.txt +++ b/src/sat/tactic/CMakeLists.txt @@ -6,6 +6,7 @@ z3_add_component(sat_tactic COMPONENT_DEPENDENCIES sat tactic + solver TACTIC_HEADERS sat_tactic.h ) diff --git a/src/tactic/core/split_clause_tactic.cpp b/src/tactic/core/split_clause_tactic.cpp index e8b3bcff0..138bc91ec 100644 --- a/src/tactic/core/split_clause_tactic.cpp +++ b/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 { } diff --git a/src/tactic/generic_model_converter.cpp b/src/tactic/generic_model_converter.cpp index ddc396597..9e2a7b9b2 100644 --- a/src/tactic/generic_model_converter.cpp +++ b/src/tactic/generic_model_converter.cpp @@ -188,8 +188,6 @@ void generic_model_converter::get_units(obj_map& 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()); } diff --git a/src/tactic/sine_filter.cpp b/src/tactic/sine_filter.cpp index c5242e237..0ac726986 100644 --- a/src/tactic/sine_filter.cpp +++ b/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: diff --git a/src/tactic/tactical.cpp b/src/tactic/tactical.cpp index 0b54037da..bb04a2be7 100644 --- a/src/tactic/tactical.cpp +++ b/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(); diff --git a/src/util/util.cpp b/src/util/util.cpp index 913191e87..59d6d752c 100644 --- a/src/util/util.cpp +++ b/src/util/util.cpp @@ -20,6 +20,7 @@ Revision History: #ifdef _WINDOWS #include #endif +#include #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; }