mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-13 12:28:44 +00:00
Code Activity

fixes

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-11-11 17:22:33 -08:00
parent 6f273e7b8f
commit 37b94f1f90
3 changed files with 27 additions and 67 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

40
src/api/c++/z3++.h
View file

@ -826,7 +826,6 @@ namespace z3 {
*/
friend expr operator!(expr const & a);
/**
\brief Return an expression representing <tt>a and b</tt>.
@ -883,6 +882,16 @@ namespace z3 {
friend expr ite(expr const & c, expr const & t, expr const & e);
bool is_true() const { return is_app() && Z3_OP_TRUE == decl().decl_kind(); }
bool is_false() const { return is_app() && Z3_OP_FALSE == decl().decl_kind(); }
bool is_not() const { return is_app() && Z3_OP_NOT == decl().decl_kind(); }
bool is_and() const { return is_app() && Z3_OP_AND == decl().decl_kind(); }
bool is_or() const { return is_app() && Z3_OP_OR == decl().decl_kind(); }
bool is_xor() const { return is_app() && Z3_OP_XOR == decl().decl_kind(); }
bool is_implies() const { return is_app() && Z3_OP_IMPLIES == decl().decl_kind(); }
bool is_eq() const { return is_app() && Z3_OP_EQ == decl().decl_kind(); }
bool is_ite() const { return is_app() && Z3_OP_ITE == decl().decl_kind(); }
friend expr distinct(expr_vector const& args);
friend expr concat(expr const& a, expr const& b);
friend expr concat(expr_vector const& args);
@ -1997,31 +2006,27 @@ namespace z3 {
unsigned& m_cutoff;
expr_vector m_cube;
bool m_end;
bool m_empty;
bool is_false() const { return m_cube.size() == 1 && Z3_OP_FALSE == m_cube[0].decl().decl_kind(); }
void check_end() {
if (is_false()) {
void inc() {
assert(!m_end && !m_empty);
m_cube = m_solver.cube(m_cutoff);
m_cutoff = 0xFFFFFFFF;
if (m_cube.size() == 1 && m_cube[0].is_false()) {
m_cube = z3::expr_vector(m_solver.ctx());
m_end = true;
}
else if (m_cube.empty()) {
m_end = true;
m_empty = true;
}
}
void inc() {
assert(!m_end);
m_cube = m_solver.cube(m_cutoff);
m_cutoff = 0xFFFFFFFF;
check_end();
}
public:
cube_iterator(solver& s, unsigned& cutoff, bool end):
m_solver(s),
m_cutoff(cutoff),
m_cube(s.ctx()),
m_end(end) {
m_end(end),
m_empty(false) {
if (!m_end) {
inc();
}
@ -2029,7 +2034,12 @@ namespace z3 {
cube_iterator& operator++() {
assert(!m_end);
inc();
if (m_empty) {
m_end = true;
}
else {
inc();
}
return *this;
}
cube_iterator operator++(int) { assert(false); return *this; }

45
src/sat/sat_clause.cpp
View file

@ -123,52 +123,17 @@ namespace sat {
clause_allocator::clause_allocator():
m_allocator("clause-allocator") {
#if defined(_AMD64_)
m_num_segments = 0;
#endif
}
clause * clause_allocator::get_clause(clause_offset cls_off) const {
#if 0
// defined(_AMD64_)
if (((cls_off & c_alignment_mask) == c_last_segment)) {
unsigned id = cls_off >> c_cls_alignment;
return const_cast<clause*>(m_last_seg_id2cls[id]);
}
return reinterpret_cast<clause *>(m_segments[cls_off & c_alignment_mask] + (static_cast<size_t>(cls_off) & ~c_alignment_mask));
#else
VERIFY(cls_off == reinterpret_cast<clause_offset>(reinterpret_cast<clause*>(cls_off)));
SASSERT(cls_off == reinterpret_cast<clause_offset>(reinterpret_cast<clause*>(cls_off)));
return reinterpret_cast<clause *>(cls_off);
#endif
}
clause_offset clause_allocator::get_offset(clause const * cls) const {
#if 0
// defined(_AMD64_)
size_t ptr = reinterpret_cast<size_t>(cls);
SASSERT((ptr & c_alignment_mask) == 0);
ptr &= 0xFFFFFFFF00000000ull; // Keep only high part
unsigned i = 0;
for (i = 0; i < m_num_segments; ++i)
if (m_segments[i] == ptr)
return static_cast<clause_offset>(reinterpret_cast<size_t>(cls)) + i;
SASSERT(i == m_num_segments);
SASSERT(i <= c_last_segment);
if (i == c_last_segment) {
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
VERIFY(cls == reinterpret_cast<clause *>(reinterpret_cast<size_t>(cls)));
SASSERT(cls == reinterpret_cast<clause *>(reinterpret_cast<size_t>(cls)));
return reinterpret_cast<size_t>(cls);
#endif
}
clause * clause_allocator::mk_clause(unsigned num_lits, literal const * lits, bool learned) {
@ -182,12 +147,6 @@ namespace sat {
void clause_allocator::del_clause(clause * cls) {
TRACE("sat_clause", tout << "delete: " << cls->id() << " " << *cls << "\n";);
if (cls->id() == 62805 && cls->capacity() == 29) {
std::cout << "delete 62805\n";
for (literal l : *cls) {
std::cout << l << "\n";
}
}
m_id_gen.recycle(cls->id());
size_t size = clause::get_obj_size(cls->m_capacity);
cls->~clause();

9
src/sat/sat_clause.h
View file

@ -139,15 +139,6 @@ namespace sat {
class clause_allocator {
small_object_allocator m_allocator;
id_gen m_id_gen;
#if defined(_AMD64_)
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;
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();
clause * get_clause(clause_offset cls_off) const;