mirror of
https://github.com/Z3Prover/z3
synced 2025-04-20 23:56:37 +00:00
64 bit clause offset fix
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
a55416351f
commit
bc54197fb3
|
@ -198,28 +198,29 @@ ATOMIC_CMD(get_proof_cmd, "get-proof", "retrieve proof", {
|
|||
}
|
||||
});
|
||||
|
||||
#define PRINT_CORE() \
|
||||
ptr_vector<expr> core; \
|
||||
ctx.get_check_sat_result()->get_unsat_core(core); \
|
||||
ctx.regular_stream() << "("; \
|
||||
ptr_vector<expr>::const_iterator it = core.begin(); \
|
||||
ptr_vector<expr>::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<expr> core;
|
||||
ctx.get_check_sat_result()->get_unsat_core(core);
|
||||
ctx.regular_stream() << "(";
|
||||
ptr_vector<expr>::const_iterator it = core.begin();
|
||||
ptr_vector<expr>::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);
|
||||
});
|
||||
|
||||
|
||||
|
|
|
@ -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<clause*>(result);
|
||||
return const_cast<clause*>(m_last_seg_id2cls[id]);
|
||||
}
|
||||
#endif
|
||||
return reinterpret_cast<clause *>(m_segments[cls_off & c_alignment_mask] + (static_cast<size_t>(cls_off) & ~c_alignment_mask));
|
||||
#else
|
||||
return reinterpret_cast<clause *>(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<size_t>(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<clause_offset>(reinterpret_cast<size_t>(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<clause_offset>(reinterpret_cast<size_t>(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<clause_allocator*>(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<unsigned>(reinterpret_cast<size_t>(cls)) + segment;
|
||||
#else
|
||||
return reinterpret_cast<size_t>(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();
|
||||
|
|
|
@ -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<clause const*> m_last_seg_id2cls;
|
||||
#endif
|
||||
mutable unsigned m_num_segments;
|
||||
mutable size_t m_segments[c_last_segment];
|
||||
mutable svector<size_t> m_aux_segments;
|
||||
mutable ptr_vector<clause const> m_last_seg_id2cls;
|
||||
#endif
|
||||
public:
|
||||
clause_allocator();
|
||||
|
|
Loading…
Reference in a new issue