From 665fccf07aaedc94b1240b63b7dffcf95dc682ad Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 18 Aug 2016 18:01:29 -0700
Subject: [PATCH] addressing max-segment issue for AMD64 + Debug

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/api/python/z3.py   |  5 ++++-
 src/sat/sat_clause.cpp | 45 ++++++++++++++++++++++++++++++------------
 src/sat/sat_clause.h   |  8 ++++++--
 3 files changed, 42 insertions(+), 16 deletions(-)

diff --git a/src/api/python/z3.py b/src/api/python/z3.py
index 6c4ac13a4..23704f44f 100644
--- a/src/api/python/z3.py
+++ b/src/api/python/z3.py
@@ -1547,6 +1547,9 @@ def And(*args):
     if isinstance(last_arg, Context):
         ctx = 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:
         ctx = main_ctx()
     args = _get_args(args)
@@ -6773,7 +6776,7 @@ class Optimize(Z3PPObject):
         return Z3_optimize_to_string(self.ctx.ref(), self.optimize)
 
     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)
 
diff --git a/src/sat/sat_clause.cpp b/src/sat/sat_clause.cpp
index eabc4fdb1..70965ff9b 100644
--- a/src/sat/sat_clause.cpp
+++ b/src/sat/sat_clause.cpp
@@ -123,21 +123,28 @@ namespace sat {
 
     clause_allocator::clause_allocator():
         m_allocator("clause-allocator") {
-#ifdef _AMD64_
+#if defined(_AMD64_) 
         m_num_segments = 0;
+        m_overflow_valid = false;
 #endif
     }
 
     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));
 #else
         return reinterpret_cast<clause *>(cls_off);
 #endif
     }
 
-#ifdef _AMD64_
-    unsigned clause_allocator::get_segment(size_t ptr) {
+#if defined(_AMD64_) 
+    unsigned clause_allocator::get_segment(clause const* cls) {
+        size_t ptr = reinterpret_cast<size_t>(cls);
+
         SASSERT((ptr & c_aligment_mask) == 0);
         ptr &= ~0xFFFFFFFFull; // Keep only high part
         unsigned i = 0;
@@ -145,18 +152,30 @@ namespace sat {
             if (m_segments[i] == ptr)
                 return i;
         i = 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;
+        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_segments[i] = ptr;
+        }
         return i;
     }
 #endif
 
     clause_offset clause_allocator::get_offset(clause const * ptr) const {
-#ifdef _AMD64_
-        return static_cast<unsigned>(reinterpret_cast<size_t>(ptr)) + const_cast<clause_allocator*>(this)->get_segment(reinterpret_cast<size_t>(ptr));
+#if defined(_AMD64_) 
+        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
         return reinterpret_cast<size_t>(ptr);
 #endif
@@ -164,7 +183,7 @@ namespace sat {
     
     clause * clause_allocator::mk_clause(unsigned num_lits, literal const * lits, bool learned) {
         size_t size = clause::get_obj_size(num_lits);
-#ifdef _AMD64_
+#if defined(_AMD64_) 
         size_t slot = size >> c_cls_alignment;
         if ((size & c_aligment_mask) != 0)
             slot++;
@@ -181,7 +200,7 @@ namespace sat {
         TRACE("sat", tout << "delete: " << cls->id() << " " << cls << " " << *cls << "\n";);
         m_id_gen.recycle(cls->id());
         size_t size = clause::get_obj_size(cls->m_capacity);
-#ifdef _AMD64_
+#if defined(_AMD64_) 
         size_t slot = size >> c_cls_alignment;
         if ((size & c_aligment_mask) != 0)
             slot++;
diff --git a/src/sat/sat_clause.h b/src/sat/sat_clause.h
index 6a183c3df..f78f6b960 100644
--- a/src/sat/sat_clause.h
+++ b/src/sat/sat_clause.h
@@ -22,6 +22,7 @@ Revision History:
 #include"sat_types.h"
 #include"small_object_allocator.h"
 #include"id_gen.h"
+#include"map.h"
 
 #ifdef _MSC_VER
 #pragma warning(disable : 4200)
@@ -124,13 +125,16 @@ namespace sat {
     class clause_allocator {
         small_object_allocator m_allocator;
         id_gen                 m_id_gen;
-#ifdef _AMD64_
-        unsigned get_segment(size_t ptr);
+#if defined(_AMD64_) 
+        unsigned get_segment(clause const* cls);
         static const unsigned  c_cls_alignment = 3; 
         static const unsigned  c_max_segments  = 1 << c_cls_alignment;
         static const size_t    c_aligment_mask = (1ull << c_cls_alignment) - 1ull;
         unsigned               m_num_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
     public:
         clause_allocator();