diff --git a/src/cmd_context/basic_cmds.cpp b/src/cmd_context/basic_cmds.cpp index 6d6217b50..f46e0d8ff 100644 --- a/src/cmd_context/basic_cmds.cpp +++ b/src/cmd_context/basic_cmds.cpp @@ -198,28 +198,29 @@ ATOMIC_CMD(get_proof_cmd, "get-proof", "retrieve proof", { } }); -#define PRINT_CORE() \ - ptr_vector core; \ - ctx.get_check_sat_result()->get_unsat_core(core); \ - ctx.regular_stream() << "("; \ - ptr_vector::const_iterator it = core.begin(); \ - ptr_vector::const_iterator end = core.end(); \ - for (bool first = true; it != end; ++it) { \ - if (first) \ - first = false; \ - else \ - ctx.regular_stream() << " "; \ - ctx.regular_stream() << mk_ismt2_pp(*it, ctx.m()); \ - } \ - ctx.regular_stream() << ")" << std::endl; \ +static void print_core(cmd_context& ctx) { + ptr_vector core; + ctx.get_check_sat_result()->get_unsat_core(core); + ctx.regular_stream() << "("; + ptr_vector::const_iterator it = core.begin(); + ptr_vector::const_iterator end = core.end(); + for (bool first = true; it != end; ++it) { + if (first) + first = false; + else + ctx.regular_stream() << " "; + ctx.regular_stream() << mk_ismt2_pp(*it, ctx.m()); + } + ctx.regular_stream() << ")" << std::endl; +} -ATOMIC_CMD(get_unsat_core_cmd, "get-unsat-core", "retrieve unsat core", { +TOMIC_CMD(get_unsat_core_cmd, "get-unsat-core", "retrieve unsat core", { if (!ctx.produce_unsat_cores()) throw cmd_exception("unsat core construction is not enabled, use command (set-option :produce-unsat-cores true)"); if (!ctx.has_manager() || ctx.cs_state() != cmd_context::css_unsat) throw cmd_exception("unsat core is not available"); - PRINT_CORE(); + print_core(ctx); }); ATOMIC_CMD(get_unsat_assumptions_cmd, "get-unsat-assumptions", "retrieve subset of assumptions sufficient for unsatisfiability", { @@ -228,7 +229,7 @@ ATOMIC_CMD(get_unsat_assumptions_cmd, "get-unsat-assumptions", "retrieve subset if (!ctx.has_manager() || ctx.cs_state() != cmd_context::css_unsat) { throw cmd_exception("unsat assumptions is not available"); } - PRINT_CORE(); + print_core(ctx); }); diff --git a/src/sat/sat_clause.cpp b/src/sat/sat_clause.cpp index 68af09ec7..27c566b69 100644 --- a/src/sat/sat_clause.cpp +++ b/src/sat/sat_clause.cpp @@ -130,23 +130,19 @@ namespace sat { clause * clause_allocator::get_clause(clause_offset cls_off) const { #if defined(_AMD64_) -#if defined (Z3DEBUG) - clause const* result; if (((cls_off & c_alignment_mask) == c_last_segment)) { unsigned id = cls_off >> c_cls_alignment; - bool check = m_last_seg_id2cls.find(id, result); - SASSERT(check); - return const_cast(result); + return const_cast(m_last_seg_id2cls[id]); } -#endif return reinterpret_cast(m_segments[cls_off & c_alignment_mask] + (static_cast(cls_off) & ~c_alignment_mask)); #else return reinterpret_cast(cls_off); #endif } + + clause_offset clause_allocator::get_offset(clause const * cls) const { #if defined(_AMD64_) - unsigned clause_allocator::get_segment(clause const* cls) { size_t ptr = reinterpret_cast(cls); SASSERT((ptr & c_alignment_mask) == 0); @@ -154,41 +150,18 @@ namespace sat { unsigned i = 0; for (i = 0; i < m_num_segments; ++i) if (m_segments[i] == ptr) - return i; - i = m_num_segments; + return static_cast(reinterpret_cast(cls)) + i; + SASSERT(i == m_num_segments); SASSERT(i <= c_last_segment); -#if defined(Z3DEBUG) if (i == c_last_segment) { - if (!m_last_seg_id2cls.contains(cls->id())) - m_last_seg_id2cls.insert(cls->id(), cls); + m_last_seg_id2cls.setx(cls->id(), cls, 0); + return (cls->id() << c_cls_alignment) | c_last_segment; } else { ++m_num_segments; m_segments[i] = ptr; + return static_cast(reinterpret_cast(cls)) + i; } -#else - if (i == c_last_segment) { - throw default_exception("segment out of range"); - } - m_segments[i] = ptr; - ++m_num_segments; -#endif - - return i; - } -#endif - - clause_offset clause_allocator::get_offset(clause const * cls) const { -#if defined(_AMD64_) - unsigned segment = const_cast(this)->get_segment(cls); -#if defined(Z3DEBUG) - SASSERT(segment <= c_last_segment); - if (segment == c_last_segment) { - SASSERT(m_last_seg_id2cls.contains(cls->id())); - return (cls->id() << c_cls_alignment) | c_last_segment; - } -#endif - return static_cast(reinterpret_cast(cls)) + segment; #else return reinterpret_cast(cls); #endif @@ -207,9 +180,6 @@ namespace sat { TRACE("sat_clause", tout << "delete: " << cls->id() << " " << *cls << "\n";); m_id_gen.recycle(cls->id()); #if defined(_AMD64_) -#if defined(Z3DEBUG) - m_last_seg_id2cls.remove(cls->id()); -#endif #endif size_t size = clause::get_obj_size(cls->m_capacity); cls->~clause(); diff --git a/src/sat/sat_clause.h b/src/sat/sat_clause.h index 11824b247..beaa97862 100644 --- a/src/sat/sat_clause.h +++ b/src/sat/sat_clause.h @@ -132,15 +132,13 @@ namespace sat { small_object_allocator m_allocator; id_gen m_id_gen; #if defined(_AMD64_) - unsigned get_segment(clause const* cls); static const unsigned c_cls_alignment = 3; static const unsigned c_last_segment = (1ull << c_cls_alignment) - 1ull; static const size_t c_alignment_mask = (1ull << c_cls_alignment) - 1ull; - unsigned m_num_segments; - size_t m_segments[c_last_segment]; -#if defined(Z3DEBUG) - u_map m_last_seg_id2cls; -#endif + mutable unsigned m_num_segments; + mutable size_t m_segments[c_last_segment]; + mutable svector m_aux_segments; + mutable ptr_vector m_last_seg_id2cls; #endif public: clause_allocator();