mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-04 05:19:11 +00:00
Code Activity

addressing max-segment issue for AMD64 + Debug

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2016-08-18 18:01:29 -07:00
parent 14e8126f16
commit 665fccf07a
3 changed files with 42 additions and 16 deletions
Download patch file Download diff file Expand all files Collapse all files

5
src/api/python/z3.py
View file

@ -1547,6 +1547,9 @@ def And(*args):
if isinstance(last_arg, Context): if isinstance(last_arg, Context):
ctx = args[len(args)-1] ctx = args[len(args)-1]
args = args[:len(args)-1] args = args[:len(args)-1]
elif len(args) == 1 and isinstance(args[0], AstVector):
ctx = args[0].ctx
args = [a for a in args[0]]
else: else:
ctx = main_ctx() ctx = main_ctx()
args = _get_args(args) args = _get_args(args)
@ -6773,7 +6776,7 @@ class Optimize(Z3PPObject):
return Z3_optimize_to_string(self.ctx.ref(), self.optimize) return Z3_optimize_to_string(self.ctx.ref(), self.optimize)
def statistics(self): def statistics(self):
"""Return statistics for the last `query()`. """Return statistics for the last check`.
""" """
return Statistics(Z3_optimize_get_statistics(self.ctx.ref(), self.optimize), self.ctx) return Statistics(Z3_optimize_get_statistics(self.ctx.ref(), self.optimize), self.ctx)

41
src/sat/sat_clause.cpp
View file

@ -123,21 +123,28 @@ namespace sat {
clause_allocator::clause_allocator(): clause_allocator::clause_allocator():
m_allocator("clause-allocator") { m_allocator("clause-allocator") {
#ifdef _AMD64_ #if defined(_AMD64_)
m_num_segments = 0; m_num_segments = 0;
m_overflow_valid = false;
#endif #endif
} }
clause * clause_allocator::get_clause(clause_offset cls_off) const { clause * clause_allocator::get_clause(clause_offset cls_off) const {
#ifdef _AMD64_ #if defined(_AMD64_)
clause const* result;
if (m_overflow_valid && m_cls_offset2ptr.find(cls_off, result)) {
return const_cast<clause*>(result);
}
return reinterpret_cast<clause *>(m_segments[cls_off & c_aligment_mask] + (static_cast<size_t>(cls_off) & ~c_aligment_mask)); return reinterpret_cast<clause *>(m_segments[cls_off & c_aligment_mask] + (static_cast<size_t>(cls_off) & ~c_aligment_mask));
#else #else
return reinterpret_cast<clause *>(cls_off); return reinterpret_cast<clause *>(cls_off);
#endif #endif
} }
#ifdef _AMD64_ #if defined(_AMD64_)
unsigned clause_allocator::get_segment(size_t ptr) { unsigned clause_allocator::get_segment(clause const* cls) {
size_t ptr = reinterpret_cast<size_t>(cls);
SASSERT((ptr & c_aligment_mask) == 0); SASSERT((ptr & c_aligment_mask) == 0);
ptr &= ~0xFFFFFFFFull; // Keep only high part ptr &= ~0xFFFFFFFFull; // Keep only high part
unsigned i = 0; unsigned i = 0;
@ -145,18 +152,30 @@ namespace sat {
if (m_segments[i] == ptr) if (m_segments[i] == ptr)
return i; return i;
i = m_num_segments; i = m_num_segments;
SASSERT(m_num_segments < c_max_segments);
if (i + 1 == c_max_segments) {
m_overflow_valid = true;
i += c_max_segments * m_cls_offset2ptr.size();
m_ptr2cls_offset.insert(ptr, i);
m_cls_offset2ptr.insert(i, cls);
}
else {
m_num_segments++; m_num_segments++;
SASSERT(m_num_segments <= c_max_segments);
if (i >= c_max_segments)
throw default_exception("segment out of range");
m_segments[i] = ptr; m_segments[i] = ptr;
}
return i; return i;
} }
#endif #endif
clause_offset clause_allocator::get_offset(clause const * ptr) const { clause_offset clause_allocator::get_offset(clause const * ptr) const {
#ifdef _AMD64_ #if defined(_AMD64_)
return static_cast<unsigned>(reinterpret_cast<size_t>(ptr)) + const_cast<clause_allocator*>(this)->get_segment(reinterpret_cast<size_t>(ptr)); unsigned segment = const_cast<clause_allocator*>(this)->get_segment(ptr);
if (segment >= c_max_segments) {
return m_ptr2cls_offset.find(reinterpret_cast<size_t>(ptr));
}
else {
return static_cast<unsigned>(reinterpret_cast<size_t>(ptr)) + segment;
}
#else #else
return reinterpret_cast<size_t>(ptr); return reinterpret_cast<size_t>(ptr);
#endif #endif
@ -164,7 +183,7 @@ namespace sat {
clause * clause_allocator::mk_clause(unsigned num_lits, literal const * lits, bool learned) { clause * clause_allocator::mk_clause(unsigned num_lits, literal const * lits, bool learned) {
size_t size = clause::get_obj_size(num_lits); size_t size = clause::get_obj_size(num_lits);
#ifdef _AMD64_ #if defined(_AMD64_)
size_t slot = size >> c_cls_alignment; size_t slot = size >> c_cls_alignment;
if ((size & c_aligment_mask) != 0) if ((size & c_aligment_mask) != 0)
slot++; slot++;
@ -181,7 +200,7 @@ namespace sat {
TRACE("sat", tout << "delete: " << cls->id() << " " << cls << " " << *cls << "\n";); TRACE("sat", tout << "delete: " << cls->id() << " " << cls << " " << *cls << "\n";);
m_id_gen.recycle(cls->id()); m_id_gen.recycle(cls->id());
size_t size = clause::get_obj_size(cls->m_capacity); size_t size = clause::get_obj_size(cls->m_capacity);
#ifdef _AMD64_ #if defined(_AMD64_)
size_t slot = size >> c_cls_alignment; size_t slot = size >> c_cls_alignment;
if ((size & c_aligment_mask) != 0) if ((size & c_aligment_mask) != 0)
slot++; slot++;

8
src/sat/sat_clause.h
View file

@ -22,6 +22,7 @@ Revision History:
#include"sat_types.h" #include"sat_types.h"
#include"small_object_allocator.h" #include"small_object_allocator.h"
#include"id_gen.h" #include"id_gen.h"
#include"map.h"
#ifdef _MSC_VER #ifdef _MSC_VER
#pragma warning(disable : 4200) #pragma warning(disable : 4200)
@ -124,13 +125,16 @@ namespace sat {
class clause_allocator { class clause_allocator {
small_object_allocator m_allocator; small_object_allocator m_allocator;
id_gen m_id_gen; id_gen m_id_gen;
#ifdef _AMD64_ #if defined(_AMD64_)
unsigned get_segment(size_t ptr); unsigned get_segment(clause const* cls);
static const unsigned c_cls_alignment = 3; static const unsigned c_cls_alignment = 3;
static const unsigned c_max_segments = 1 << c_cls_alignment; static const unsigned c_max_segments = 1 << c_cls_alignment;
static const size_t c_aligment_mask = (1ull << c_cls_alignment) - 1ull; static const size_t c_aligment_mask = (1ull << c_cls_alignment) - 1ull;
unsigned m_num_segments; unsigned m_num_segments;
size_t m_segments[c_max_segments]; size_t m_segments[c_max_segments];
bool m_overflow_valid;
size_t_map<unsigned> m_ptr2cls_offset;
u_map<clause const*> m_cls_offset2ptr;
#endif #endif
public: public:
clause_allocator(); clause_allocator();