From 37b94f1f909e35b7eaf3dcba0d1430ea7ad691e5 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 11 Nov 2017 17:22:33 -0800 Subject: [PATCH] fixes Signed-off-by: Nikolaj Bjorner --- src/api/c++/z3++.h | 40 +++++++++++++++++++++++-------------- src/sat/sat_clause.cpp | 45 ++---------------------------------------- src/sat/sat_clause.h | 9 --------- 3 files changed, 27 insertions(+), 67 deletions(-) diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index 52671a073..417a86458 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -826,7 +826,6 @@ namespace z3 { */ friend expr operator!(expr const & a); - /** \brief Return an expression representing a and b. @@ -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; } diff --git a/src/sat/sat_clause.cpp b/src/sat/sat_clause.cpp index 9bfd1d38d..90d542a14 100644 --- a/src/sat/sat_clause.cpp +++ b/src/sat/sat_clause.cpp @@ -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(m_last_seg_id2cls[id]); - } - return reinterpret_cast(m_segments[cls_off & c_alignment_mask] + (static_cast(cls_off) & ~c_alignment_mask)); -#else - VERIFY(cls_off == reinterpret_cast(reinterpret_cast(cls_off))); + SASSERT(cls_off == reinterpret_cast(reinterpret_cast(cls_off))); return reinterpret_cast(cls_off); -#endif } clause_offset clause_allocator::get_offset(clause const * cls) const { -#if 0 -// defined(_AMD64_) - size_t ptr = reinterpret_cast(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(reinterpret_cast(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(reinterpret_cast(cls)) + i; - } -#else - VERIFY(cls == reinterpret_cast(reinterpret_cast(cls))); + SASSERT(cls == reinterpret_cast(reinterpret_cast(cls))); return reinterpret_cast(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(); diff --git a/src/sat/sat_clause.h b/src/sat/sat_clause.h index 08fff7adb..76f1a9ad3 100644 --- a/src/sat/sat_clause.h +++ b/src/sat/sat_clause.h @@ -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 m_aux_segments; - mutable ptr_vector m_last_seg_id2cls; -#endif public: clause_allocator(); clause * get_clause(clause_offset cls_off) const;