From 2ff2e77739c0948ffc083ee7f88b6b1f8f1eac86 Mon Sep 17 00:00:00 2001
From: Daniel Schemmel <daniel.schemmel@comsys.rwth-aachen.de>
Date: Mon, 21 May 2018 03:19:19 +0200
Subject: [PATCH 1/7] Move buffer.h to old_buffer.h and add a shim buffer.h

---
 src/util/buffer.h     | 265 ++---------------------------------------
 src/util/old_buffer.h | 268 ++++++++++++++++++++++++++++++++++++++++++
 2 files changed, 275 insertions(+), 258 deletions(-)
 create mode 100644 src/util/old_buffer.h

diff --git a/src/util/buffer.h b/src/util/buffer.h
index c64e23d8b..7a89ffef3 100644
--- a/src/util/buffer.h
+++ b/src/util/buffer.h
@@ -1,268 +1,17 @@
-/*++
-Copyright (c) 2006 Microsoft Corporation
-
-Module Name:
-
-    buffer.h
-
-Abstract:
-
-    <abstract>
-
-Author:
-
-    Leonardo de Moura (leonardo) 2006-10-16.
-
-Revision History:
-
---*/
 #ifndef BUFFER_H_
 #define BUFFER_H_
 
-#include<string.h>
-#include "util/memory_manager.h"
+#include "old_buffer.h"
 
 template<typename T, bool CallDestructors=true, unsigned INITIAL_SIZE=16>
-class buffer {
-protected:
-    T *      m_buffer;
-    unsigned m_pos;
-    unsigned m_capacity;
-    char     m_initial_buffer[INITIAL_SIZE * sizeof(T)];
-    
-    void free_memory() {
-        if (m_buffer != reinterpret_cast<T*>(m_initial_buffer)) {
-            dealloc_svect(m_buffer);
-        }
-    }
+using buffer = old_buffer<T, CallDestructors, INITIAL_SIZE>;
 
-    void expand() {
-        unsigned new_capacity = m_capacity << 1;
-        T * new_buffer        = reinterpret_cast<T*>(memory::allocate(sizeof(T) * new_capacity));
-        memcpy(new_buffer, m_buffer, m_pos * sizeof(T));
-        free_memory();
-        m_buffer              = new_buffer;
-        m_capacity            = new_capacity;
-    }
-    
-    void destroy_elements() {
-        iterator it = begin();
-        iterator e  = end();
-        for (; it != e; ++it) {
-            it->~T();
-        }
-    }
-
-    void destroy() {
-        if (CallDestructors) {
-            destroy_elements(); 
-        }
-        free_memory();
-    }
-
-public:
-    typedef T data;
-    typedef T * iterator;
-    typedef const T * const_iterator;
-
-    buffer():
-        m_buffer(reinterpret_cast<T *>(m_initial_buffer)),
-        m_pos(0),
-        m_capacity(INITIAL_SIZE) {
-    }
-    
-    buffer(const buffer & source):
-        m_buffer(reinterpret_cast<T *>(m_initial_buffer)),
-        m_pos(0),
-        m_capacity(INITIAL_SIZE) {
-        unsigned sz = source.size();
-        for(unsigned i = 0; i < sz; i++) {
-            push_back(source.m_buffer[i]);
-        }
-    }
-    
-    buffer(unsigned sz, const T & elem):
-        m_buffer(reinterpret_cast<T *>(m_initial_buffer)),
-        m_pos(0),
-        m_capacity(INITIAL_SIZE) {
-        for (unsigned i = 0; i < sz; i++) {
-            push_back(elem);
-        }
-        SASSERT(size() == sz);
-    }
-    
-    ~buffer() {
-        destroy();
-    }
-    
-    void reset() { 
-        if (CallDestructors) {
-            destroy_elements();
-        }
-        m_pos = 0;
-    }
-    
-    void finalize() {
-        destroy();
-        m_buffer   = reinterpret_cast<T *>(m_initial_buffer);
-        m_pos      = 0;
-        m_capacity = INITIAL_SIZE;
-    }
-    
-    unsigned size() const { 
-        return m_pos;
-    }
-    
-    bool empty() const {
-        return m_pos == 0;
-    }
-    
-    iterator begin() { 
-        return m_buffer; 
-    }
-
-    iterator end() { 
-        return m_buffer + size();
-    }
-
-    void set_end(iterator it) {
-        m_pos = static_cast<unsigned>(it - m_buffer);
-        if (CallDestructors) {
-            iterator e  = end();
-            for (; it != e; ++it) {
-                it->~T();
-            }
-        }
-    }
-    
-    const_iterator begin() const { 
-        return m_buffer; 
-    }
-    
-    const_iterator end() const { 
-        return m_buffer + size(); 
-    }
-    
-    void push_back(const T & elem) {
-        if (m_pos >= m_capacity)
-            expand();
-        new (m_buffer + m_pos) T(elem);
-        m_pos++;
-    }
-
-    void push_back(T && elem) {
-        if (m_pos >= m_capacity)
-            expand();
-        new (m_buffer + m_pos) T(std::move(elem));
-        m_pos++;
-    }
-    
-    void pop_back() {
-        if (CallDestructors) {
-            back().~T(); 
-        }
-        m_pos--;
-    }
-
-    const T & back() const { 
-        SASSERT(!empty()); 
-        SASSERT(m_pos > 0);
-        return m_buffer[m_pos - 1]; 
-    }
-
-    T & back() { 
-        SASSERT(!empty()); 
-        SASSERT(m_pos > 0);
-        return m_buffer[m_pos - 1]; 
-    }
-    
-    T * c_ptr() const {
-        return m_buffer;
-    }
-
-    void append(unsigned n, T const * elems) {
-        for (unsigned i = 0; i < n; i++) {
-            push_back(elems[i]);
-        }
-    }
-
-    void append(const buffer& source) {
-        append(source.size(), source.c_ptr());
-    }
-
-    T & operator[](unsigned idx) { 
-        SASSERT(idx < size()); 
-        return m_buffer[idx]; 
-    }
-
-    const T & operator[](unsigned idx) const { 
-        SASSERT(idx < size()); 
-        return m_buffer[idx];
-    }
-
-    T & get(unsigned idx) { 
-        SASSERT(idx < size()); 
-        return m_buffer[idx]; 
-    }
-
-    const T & get(unsigned idx) const { 
-        SASSERT(idx < size()); 
-        return m_buffer[idx];
-    }
-
-    void set(unsigned idx, T const & val) { 
-        SASSERT(idx < size()); 
-        m_buffer[idx] = val;
-    }
-
-    void resize(unsigned nsz, const T & elem=T()) {
-        unsigned sz = size();
-        if (nsz > sz) {
-            for (unsigned i = sz; i < nsz; i++) {
-                push_back(elem);
-            }
-        }
-        else if (nsz < sz) {
-            for (unsigned i = nsz; i < sz; i++) {
-                pop_back();
-            }
-        }
-        SASSERT(size() == nsz);
-    }
-
-    void shrink(unsigned nsz) {
-        unsigned sz = size();
-        SASSERT(nsz <= sz);
-        for (unsigned i = nsz; i < sz; i++)
-            pop_back();
-        SASSERT(size() == nsz);
-    }
-
-    buffer & operator=(buffer const & other) {
-        if (this == &other)
-            return *this;
-        reset();
-        append(other);
-        return *this;
-    }
-};
+// note that the append added in the old_ptr_buffer is actually not an addition over its base class old_buffer,
+// which already has an append function with the same signature and implementation
+template<typename T, unsigned INITIAL_SIZE=16>
+using ptr_buffer = old_ptr_buffer<T, INITIAL_SIZE>;
 
 template<typename T, unsigned INITIAL_SIZE=16>
-class ptr_buffer : public buffer<T *, false, INITIAL_SIZE> {
-public:
-    void append(unsigned n, T * const * elems) {
-        for (unsigned i = 0; i < n; i++) {
-            this->push_back(elems[i]);
-        }
-    }
-};
-
-template<typename T, unsigned INITIAL_SIZE=16>
-class sbuffer : public buffer<T, false, INITIAL_SIZE> {
-public:
-    sbuffer(): buffer<T, false, INITIAL_SIZE>() {}
-    sbuffer(unsigned sz, const T& elem) : buffer<T, false, INITIAL_SIZE>(sz,elem) {}
-};
+using sbuffer = old_sbuffer<T, INITIAL_SIZE>;
 
 #endif /* BUFFER_H_ */
-
diff --git a/src/util/old_buffer.h b/src/util/old_buffer.h
new file mode 100644
index 000000000..5ed1df583
--- /dev/null
+++ b/src/util/old_buffer.h
@@ -0,0 +1,268 @@
+/*++
+Copyright (c) 2006 Microsoft Corporation
+
+Module Name:
+
+    old_buffer.h
+
+Abstract:
+
+    <abstract>
+
+Author:
+
+    Leonardo de Moura (leonardo) 2006-10-16.
+
+Revision History:
+
+--*/
+#ifndef OLD_BUFFER_H_
+#define OLD_BUFFER_H_
+
+#include<string.h>
+#include "util/memory_manager.h"
+
+template<typename T, bool CallDestructors=true, unsigned INITIAL_SIZE=16>
+class old_buffer {
+protected:
+    T *      m_buffer;
+    unsigned m_pos;
+    unsigned m_capacity;
+    char     m_initial_buffer[INITIAL_SIZE * sizeof(T)];
+    
+    void free_memory() {
+        if (m_buffer != reinterpret_cast<T*>(m_initial_buffer)) {
+            dealloc_svect(m_buffer);
+        }
+    }
+
+    void expand() {
+        unsigned new_capacity = m_capacity << 1;
+        T * new_buffer        = reinterpret_cast<T*>(memory::allocate(sizeof(T) * new_capacity));
+        memcpy(new_buffer, m_buffer, m_pos * sizeof(T));
+        free_memory();
+        m_buffer              = new_buffer;
+        m_capacity            = new_capacity;
+    }
+    
+    void destroy_elements() {
+        iterator it = begin();
+        iterator e  = end();
+        for (; it != e; ++it) {
+            it->~T();
+        }
+    }
+
+    void destroy() {
+        if (CallDestructors) {
+            destroy_elements(); 
+        }
+        free_memory();
+    }
+
+public:
+    typedef T data;
+    typedef T * iterator;
+    typedef const T * const_iterator;
+
+    old_buffer():
+        m_buffer(reinterpret_cast<T *>(m_initial_buffer)),
+        m_pos(0),
+        m_capacity(INITIAL_SIZE) {
+    }
+    
+    old_buffer(const old_buffer & source):
+        m_buffer(reinterpret_cast<T *>(m_initial_buffer)),
+        m_pos(0),
+        m_capacity(INITIAL_SIZE) {
+        unsigned sz = source.size();
+        for(unsigned i = 0; i < sz; i++) {
+            push_back(source.m_buffer[i]);
+        }
+    }
+    
+    old_buffer(unsigned sz, const T & elem):
+        m_buffer(reinterpret_cast<T *>(m_initial_buffer)),
+        m_pos(0),
+        m_capacity(INITIAL_SIZE) {
+        for (unsigned i = 0; i < sz; i++) {
+            push_back(elem);
+        }
+        SASSERT(size() == sz);
+    }
+    
+    ~old_buffer() {
+        destroy();
+    }
+    
+    void reset() { 
+        if (CallDestructors) {
+            destroy_elements();
+        }
+        m_pos = 0;
+    }
+    
+    void finalize() {
+        destroy();
+        m_buffer   = reinterpret_cast<T *>(m_initial_buffer);
+        m_pos      = 0;
+        m_capacity = INITIAL_SIZE;
+    }
+    
+    unsigned size() const { 
+        return m_pos;
+    }
+    
+    bool empty() const {
+        return m_pos == 0;
+    }
+    
+    iterator begin() { 
+        return m_buffer; 
+    }
+
+    iterator end() { 
+        return m_buffer + size();
+    }
+
+    void set_end(iterator it) {
+        m_pos = static_cast<unsigned>(it - m_buffer);
+        if (CallDestructors) {
+            iterator e  = end();
+            for (; it != e; ++it) {
+                it->~T();
+            }
+        }
+    }
+    
+    const_iterator begin() const { 
+        return m_buffer; 
+    }
+    
+    const_iterator end() const { 
+        return m_buffer + size(); 
+    }
+    
+    void push_back(const T & elem) {
+        if (m_pos >= m_capacity)
+            expand();
+        new (m_buffer + m_pos) T(elem);
+        m_pos++;
+    }
+
+    void push_back(T && elem) {
+        if (m_pos >= m_capacity)
+            expand();
+        new (m_buffer + m_pos) T(std::move(elem));
+        m_pos++;
+    }
+    
+    void pop_back() {
+        if (CallDestructors) {
+            back().~T(); 
+        }
+        m_pos--;
+    }
+
+    const T & back() const { 
+        SASSERT(!empty()); 
+        SASSERT(m_pos > 0);
+        return m_buffer[m_pos - 1]; 
+    }
+
+    T & back() { 
+        SASSERT(!empty()); 
+        SASSERT(m_pos > 0);
+        return m_buffer[m_pos - 1]; 
+    }
+    
+    T * c_ptr() const {
+        return m_buffer;
+    }
+
+    void append(unsigned n, T const * elems) {
+        for (unsigned i = 0; i < n; i++) {
+            push_back(elems[i]);
+        }
+    }
+
+    void append(const old_buffer& source) {
+        append(source.size(), source.c_ptr());
+    }
+
+    T & operator[](unsigned idx) { 
+        SASSERT(idx < size()); 
+        return m_buffer[idx]; 
+    }
+
+    const T & operator[](unsigned idx) const { 
+        SASSERT(idx < size()); 
+        return m_buffer[idx];
+    }
+
+    T & get(unsigned idx) { 
+        SASSERT(idx < size()); 
+        return m_buffer[idx]; 
+    }
+
+    const T & get(unsigned idx) const { 
+        SASSERT(idx < size()); 
+        return m_buffer[idx];
+    }
+
+    void set(unsigned idx, T const & val) { 
+        SASSERT(idx < size()); 
+        m_buffer[idx] = val;
+    }
+
+    void resize(unsigned nsz, const T & elem=T()) {
+        unsigned sz = size();
+        if (nsz > sz) {
+            for (unsigned i = sz; i < nsz; i++) {
+                push_back(elem);
+            }
+        }
+        else if (nsz < sz) {
+            for (unsigned i = nsz; i < sz; i++) {
+                pop_back();
+            }
+        }
+        SASSERT(size() == nsz);
+    }
+
+    void shrink(unsigned nsz) {
+        unsigned sz = size();
+        SASSERT(nsz <= sz);
+        for (unsigned i = nsz; i < sz; i++)
+            pop_back();
+        SASSERT(size() == nsz);
+    }
+
+    old_buffer & operator=(old_buffer const & other) {
+        if (this == &other)
+            return *this;
+        reset();
+        append(other);
+        return *this;
+    }
+};
+
+template<typename T, unsigned INITIAL_SIZE=16>
+class old_ptr_buffer : public old_buffer<T *, false, INITIAL_SIZE> {
+public:
+    void append(unsigned n, T * const * elems) {
+        for (unsigned i = 0; i < n; i++) {
+            this->push_back(elems[i]);
+        }
+    }
+};
+
+template<typename T, unsigned INITIAL_SIZE=16>
+class old_sbuffer : public old_buffer<T, false, INITIAL_SIZE> {
+public:
+    old_sbuffer(): old_buffer<T, false, INITIAL_SIZE>() {}
+    old_sbuffer(unsigned sz, const T& elem) : old_buffer<T, false, INITIAL_SIZE>(sz,elem) {}
+};
+
+#endif /* OLD_BUFFER_H_ */
+

From 721ea2a8d3eec8819e3f3b2c4b55ed5212c67dcb Mon Sep 17 00:00:00 2001
From: Daniel Schemmel <daniel.schemmel@comsys.rwth-aachen.de>
Date: Sat, 26 May 2018 05:22:39 +0200
Subject: [PATCH 2/7] Move vector.h to old_vector.h and add a shim vector.h To
 do so, one instance of the class keyword needs to be removed.

---
 src/util/lp/dense_matrix.cpp |   2 +-
 src/util/old_vector.h        | 609 ++++++++++++++++++++++++++++++++++
 src/util/vector.h            | 617 +----------------------------------
 3 files changed, 622 insertions(+), 606 deletions(-)
 create mode 100644 src/util/old_vector.h

diff --git a/src/util/lp/dense_matrix.cpp b/src/util/lp/dense_matrix.cpp
index 50f2598c8..4ababc47a 100644
--- a/src/util/lp/dense_matrix.cpp
+++ b/src/util/lp/dense_matrix.cpp
@@ -35,6 +35,6 @@ template lp::dense_matrix<lp::mpq, lp::numeric_pair<lp::mpq> >::dense_matrix(uns
 template lp::dense_matrix<lp::mpq, lp::numeric_pair<lp::mpq> >& lp::dense_matrix<lp::mpq, lp::numeric_pair<lp::mpq> >::operator=(lp::dense_matrix<lp::mpq, lp::numeric_pair<lp::mpq> > const&);
 template lp::dense_matrix<lp::mpq, lp::numeric_pair<lp::mpq> > lp::operator*<lp::mpq, lp::numeric_pair<lp::mpq> >(lp::matrix<lp::mpq, lp::numeric_pair<lp::mpq> >&, lp::matrix<lp::mpq, lp::numeric_pair<lp::mpq> >&);
 template void lp::dense_matrix<lp::mpq, lp::numeric_pair< lp::mpq> >::apply_from_right( vector< lp::mpq> &);
-template void lp::dense_matrix<double,double>::apply_from_right(class vector<double> &);
+template void lp::dense_matrix<double,double>::apply_from_right(vector<double> &);
 template void lp::dense_matrix<lp::mpq, lp::mpq>::apply_from_left(vector<lp::mpq>&);
 #endif
diff --git a/src/util/old_vector.h b/src/util/old_vector.h
new file mode 100644
index 000000000..53450e6cf
--- /dev/null
+++ b/src/util/old_vector.h
@@ -0,0 +1,609 @@
+/*++
+Copyright (c) 2006 Microsoft Corporation
+
+Module Name:
+
+    old_vector.h
+
+Abstract:
+    Dynamic array implementation. 
+    Remarks:
+
+    - Empty arrays consume only sizeof(T *) bytes.
+
+    - There is the option of disabling the destructor invocation for elements stored in the vector.
+    This is useful for vectors of int.
+
+Author:
+
+    Leonardo de Moura (leonardo) 2006-09-11.
+
+Revision History:
+
+--*/
+#ifndef OLD_VECTOR_H_
+#define OLD_VECTOR_H_
+
+#include "util/debug.h"
+#include<algorithm>
+#include<type_traits>
+#include<memory.h>
+#include<functional>
+#include "util/memory_manager.h"
+#include "util/hash.h"
+#include "util/z3_exception.h"
+
+// disable warning for constant 'if' expressions.
+// these are used heavily in templates.
+#ifdef _MSC_VER
+#pragma warning(disable:4127)
+#endif
+
+template<typename T, bool CallDestructors=true, typename SZ = unsigned>
+class old_vector {
+#define SIZE_IDX     -1
+#define CAPACITY_IDX -2
+    T * m_data;
+
+    void destroy_elements() {
+        iterator it = begin();
+        iterator e  = end();
+        for (; it != e; ++it) {
+            it->~T();
+        }
+    }
+
+    void free_memory() { 
+        memory::deallocate(reinterpret_cast<char*>(reinterpret_cast<SZ*>(m_data) - 2));
+    }
+
+    void expand_vector() {
+        if (m_data == nullptr) {
+            SZ capacity = 2;
+            SZ * mem    = reinterpret_cast<SZ*>(memory::allocate(sizeof(T) * capacity + sizeof(SZ) * 2));
+            *mem              = capacity; 
+            mem++;
+            *mem              = 0;        
+            mem++;
+            m_data            = reinterpret_cast<T *>(mem);
+        }
+        else {
+            SASSERT(capacity() > 0);
+            SZ old_capacity = reinterpret_cast<SZ *>(m_data)[CAPACITY_IDX];
+            SZ old_capacity_T = sizeof(T) * old_capacity + sizeof(SZ) * 2;
+            SZ new_capacity = (3 * old_capacity + 1) >> 1;
+            SZ new_capacity_T = sizeof(T) * new_capacity + sizeof(SZ) * 2;
+            if (new_capacity <= old_capacity || new_capacity_T <= old_capacity_T) {
+                throw default_exception("Overflow encountered when expanding old_vector");
+            }
+            SZ *mem, *old_mem = reinterpret_cast<SZ*>(m_data) - 2;
+#if defined(__GNUC__) && !defined(__clang__) && __GNUC__ < 5
+            if (__has_trivial_copy(T)) {
+#else
+            if (std::is_trivially_copyable<T>::value) {
+#endif
+                mem = (SZ*)memory::reallocate(old_mem, new_capacity_T);
+                m_data = reinterpret_cast<T *>(mem + 2);
+            } else {
+                mem = (SZ*)memory::allocate(new_capacity_T);
+                auto old_data = m_data;
+                auto old_size = size();
+                mem[1] = old_size;
+                m_data  = reinterpret_cast<T *>(mem + 2);
+                for (unsigned i = 0; i < old_size; ++i) {
+                    new (&m_data[i]) T(std::move(old_data[i]));
+                    old_data[i].~T();
+                }
+                memory::deallocate(old_mem);
+            }
+            *mem = new_capacity;
+        }
+    }
+
+    void copy_core(old_vector const & source) {
+        SZ size      = source.size();
+        SZ capacity  = source.capacity();
+        SZ * mem     = reinterpret_cast<SZ*>(memory::allocate(sizeof(T) * capacity + sizeof(SZ) * 2));
+        *mem = capacity; 
+        mem++;
+        *mem = size; 
+        mem++;
+        m_data             = reinterpret_cast<T *>(mem);
+        const_iterator it  = source.begin();
+        iterator it2       = begin();
+        SASSERT(it2 == m_data);
+        const_iterator e   = source.end();
+        for (; it != e; ++it, ++it2) {
+            new (it2) T(*it); 
+        }
+    }
+
+    void destroy() {
+        if (m_data) { 
+            if (CallDestructors) {
+                destroy_elements(); 
+            }
+            free_memory(); 
+        } 
+    }
+
+public:
+    typedef T data;
+    typedef T * iterator;
+    typedef const T * const_iterator;
+
+    old_vector():
+        m_data(nullptr) {
+    }
+
+    old_vector(SZ s) {
+        if (s == 0) {
+            m_data = nullptr;
+            return;
+        }
+        SZ * mem = reinterpret_cast<SZ*>(memory::allocate(sizeof(T) * s + sizeof(SZ) * 2));
+        *mem = s; 
+        mem++;
+        *mem = s; 
+        mem++;
+        m_data = reinterpret_cast<T *>(mem);
+        // initialize elements
+        iterator it = begin();
+        iterator e  = end();
+        for (; it != e; ++it) {
+            new (it) T(); 
+        }
+    }
+
+    old_vector(SZ s, T const & elem):
+        m_data(nullptr) {
+        resize(s, elem);
+    }
+
+    old_vector(old_vector const & source):
+        m_data(nullptr) {
+        if (source.m_data) {
+            copy_core(source);
+        }
+        SASSERT(size() == source.size());
+    }
+
+    old_vector(old_vector&& other) : m_data(nullptr) {
+        std::swap(m_data, other.m_data);
+    }
+
+    old_vector(SZ s, T const * data):
+        m_data(nullptr) {
+        for (SZ i = 0; i < s; i++) {
+            push_back(data[i]);
+        }
+    }
+
+ 
+    ~old_vector() { 
+        destroy();
+    } 
+
+    void finalize() {
+        destroy();
+        m_data = nullptr;
+    }
+
+    bool operator==(old_vector const & other) const {
+        if (this == &other) {
+            return true;
+        }
+        if (size() != other.size())
+            return false;
+        for (unsigned i = 0; i < size(); i++) {
+            if ((*this)[i] != other[i])
+                return false;
+        }
+        return true;
+    }
+
+    bool operator!=(old_vector const & other) const {
+        return !(*this == other);
+    }
+
+    
+    old_vector & operator=(old_vector const & source) {
+        if (this == &source) {
+            return *this;
+        }
+        destroy();
+        if (source.m_data) {
+            copy_core(source);
+        }
+        else {
+            m_data = nullptr;
+        }
+        return *this;
+    }
+
+    old_vector & operator=(old_vector && source) {
+        if (this == &source) {
+            return *this;
+        }
+        destroy();
+        m_data = nullptr;
+        std::swap(m_data, source.m_data);
+        return *this;
+    }
+
+    bool containsp(std::function<bool(T)>& predicate) const {
+        for (auto const& t : *this)
+            if (predicate(t)) 
+                return true;
+        return false;
+    }
+
+    /**
+     * retain elements that satisfy predicate. aka 'where'.
+     */
+    old_vector filter_pure(std::function<bool(T)>& predicate) const {
+        old_vector result;
+        for (auto& t : *this)
+            if (predicate(t)) 
+                result.push_back(t);
+        return result;
+    }
+
+    old_vector& filter_update(std::function<bool(T)>& predicate) {
+        unsigned j = 0;
+        for (auto& t : *this)
+            if (predicate(t)) 
+                set(j++, t);
+        shrink(j);
+        return *this;
+    }
+
+    /**
+     * update elements using f, aka 'select'
+     */
+    template <typename S>
+    old_vector<S> map_pure(std::function<S(T)>& f) const {
+        old_vector<S> result;
+        for (auto& t : *this)
+            result.push_back(f(t));
+        return result;
+    }
+
+    old_vector& map_update(std::function<T(T)>& f) {
+        unsigned j = 0;
+        for (auto& t : *this)
+            set(j++, f(t));
+        return *this;
+    }
+
+    void reset() { 
+        if (m_data) {
+            if (CallDestructors) {
+                destroy_elements();
+            }
+            reinterpret_cast<SZ *>(m_data)[SIZE_IDX] = 0;
+        }
+    }
+
+    void clear() { reset(); }
+
+    bool empty() const { 
+        return m_data == nullptr || reinterpret_cast<SZ *>(m_data)[SIZE_IDX] == 0;
+    }
+
+    SZ size() const { 
+        if (m_data == nullptr) {
+            return 0;  
+        }
+        return reinterpret_cast<SZ *>(m_data)[SIZE_IDX]; 
+    }
+
+    SZ capacity() const { 
+        if (m_data == nullptr) {
+            return 0;
+        }
+        return reinterpret_cast<SZ *>(m_data)[CAPACITY_IDX]; 
+    }
+
+    iterator begin() { 
+        return m_data; 
+    }
+
+    iterator end() { 
+        return m_data + size();
+    }
+
+    const_iterator begin() const { 
+        return m_data; 
+    }
+
+    const_iterator end() const { 
+        return m_data + size(); 
+    }
+
+    class reverse_iterator {
+        T* v;
+    public:
+        reverse_iterator(T* v):v(v) {}
+        
+        T operator*() { return *v; }
+        reverse_iterator operator++(int) {
+            reverse_iterator tmp = *this;
+            --v;
+            return tmp;
+        }
+        reverse_iterator& operator++() {
+            --v;
+            return *this;
+        }
+
+        bool operator==(reverse_iterator const& other) const {
+            return other.v == v;
+        }
+        bool operator!=(reverse_iterator const& other) const {
+            return other.v != v;
+        }
+    };
+
+    reverse_iterator rbegin() { return reverse_iterator(end() - 1); }
+    reverse_iterator rend() { return reverse_iterator(begin() - 1); }
+
+    void set_end(iterator it) {
+        if (m_data) {
+            SZ new_sz = static_cast<SZ>(it - m_data);
+            if (CallDestructors) {
+                iterator e = end();
+                for(; it != e; ++it) {
+                    it->~T();
+                }
+            }
+            reinterpret_cast<SZ *>(m_data)[SIZE_IDX] = new_sz;
+        }
+        else {
+            SASSERT(it == 0);
+        }
+    }
+
+    T & operator[](SZ idx) { 
+        SASSERT(idx < size()); 
+        return m_data[idx]; 
+    }
+
+    T const & operator[](SZ idx) const { 
+        SASSERT(idx < size()); 
+        return m_data[idx];
+    }
+
+    T & get(SZ idx) { 
+        SASSERT(idx < size()); 
+        return m_data[idx]; 
+    }
+
+    T const & get(SZ idx) const { 
+        SASSERT(idx < size()); 
+        return m_data[idx];
+    }
+
+    void set(SZ idx, T const & val) { 
+        SASSERT(idx < size()); 
+        m_data[idx] = val;
+    }
+
+    void set(SZ idx, T && val) {
+        SASSERT(idx < size());
+        m_data[idx] = std::move(val);
+    }
+
+    T & back() { 
+        SASSERT(!empty()); 
+        return operator[](size() - 1); 
+    }
+
+    T const & back() const { 
+        SASSERT(!empty()); 
+        return operator[](size() - 1); 
+    }
+
+    void pop_back() { 
+        SASSERT(!empty()); 
+        if (CallDestructors) {
+            back().~T(); 
+        }
+        reinterpret_cast<SZ *>(m_data)[SIZE_IDX]--; 
+    }
+
+    void push_back(T const & elem) {
+        if (m_data == nullptr || reinterpret_cast<SZ *>(m_data)[SIZE_IDX] == reinterpret_cast<SZ *>(m_data)[CAPACITY_IDX]) {
+            expand_vector();
+        }
+        new (m_data + reinterpret_cast<SZ *>(m_data)[SIZE_IDX]) T(elem); 
+        reinterpret_cast<SZ *>(m_data)[SIZE_IDX]++;
+    }
+
+    void push_back(T && elem) {
+        if (m_data == nullptr || reinterpret_cast<SZ *>(m_data)[SIZE_IDX] == reinterpret_cast<SZ *>(m_data)[CAPACITY_IDX]) {
+            expand_vector();
+        }
+        new (m_data + reinterpret_cast<SZ *>(m_data)[SIZE_IDX]) T(std::move(elem));
+        reinterpret_cast<SZ *>(m_data)[SIZE_IDX]++;
+    }
+
+    void insert(T const & elem) {
+        push_back(elem);
+    }
+
+    void erase(iterator pos) {
+        SASSERT(pos >= begin() && pos < end());
+        iterator prev = pos;
+        ++pos;
+        iterator e    = end();
+        for(; pos != e; ++pos, ++prev) {
+            *prev = *pos;
+        }
+        reinterpret_cast<SZ *>(m_data)[SIZE_IDX]--;
+    }
+
+    void erase(T const & elem) {
+        iterator it = std::find(begin(), end(), elem);
+        if (it != end()) {
+            erase(it);
+        }
+    }
+
+    void shrink(SZ s) {
+        if (m_data) {
+            SASSERT(s <= reinterpret_cast<SZ *>(m_data)[SIZE_IDX]);
+            if (CallDestructors) {
+                iterator it = m_data + s;
+                iterator e  = end();
+                for(; it != e; ++it) {
+                    it->~T();
+                }
+            }
+            reinterpret_cast<SZ *>(m_data)[SIZE_IDX] = s;
+        }
+        else {
+            SASSERT(s == 0);
+        }
+    }
+
+    template<typename Args>
+    void resize(SZ s, Args args...) {
+        SZ sz = size();
+        if (s <= sz) { shrink(s); return; }
+        while (s > capacity()) {
+            expand_vector();
+        }
+        SASSERT(m_data != 0);
+        reinterpret_cast<SZ *>(m_data)[SIZE_IDX] = s;
+        iterator it  = m_data + sz;
+        iterator end = m_data + s;
+        for (; it != end; ++it) {
+            new (it) T(std::forward<Args>(args));
+        }
+    }
+
+    void resize(SZ s) {
+        SZ sz = size();
+        if (s <= sz) { shrink(s); return; }
+        while (s > capacity()) {
+            expand_vector();
+        }
+        SASSERT(m_data != 0);
+        reinterpret_cast<SZ *>(m_data)[SIZE_IDX] = s;
+        iterator it  = m_data + sz;
+        iterator end = m_data + s;
+        for (; it != end; ++it) {
+            new (it) T();
+        }
+    }
+
+    void append(old_vector<T, CallDestructors> const & other) {
+        for(SZ i = 0; i < other.size(); ++i) {
+            push_back(other[i]);
+        }
+    }
+
+    void append(SZ sz, T const * data) {
+        for(SZ i = 0; i < sz; ++i) {
+            push_back(data[i]);
+        }
+    }
+
+    T * c_ptr() const {
+        return m_data;
+    }
+
+    void swap(old_vector & other) {
+        std::swap(m_data, other.m_data);
+    }
+
+    void reverse() {
+        SZ sz = size();
+        for (SZ i = 0; i < sz/2; ++i) {
+            std::swap(m_data[i], m_data[sz-i-1]);
+        }
+    }
+
+    void fill(T const & elem) {
+        iterator i = begin();
+        iterator e = end();
+        for (; i != e; ++i) {
+            *i = elem;
+        }
+    }
+
+    void fill(unsigned sz, T const & elem) {
+        resize(sz);
+        fill(elem);
+    }
+
+    bool contains(T const & elem) const {
+        const_iterator it  = begin();
+        const_iterator e = end();
+        for (; it != e; ++it) {
+            if (*it == elem) {
+                return true;
+            }
+        }
+        return false;
+    }
+
+    // set pos idx with elem. If idx >= size, then expand using default.
+    void setx(SZ idx, T const & elem, T const & d) {
+        if (idx >= size()) {
+            resize(idx+1, d);
+        }
+        m_data[idx] = elem;
+    }
+
+    // return element at position idx, if idx >= size, then return default
+    T const & get(SZ idx, T const & d) const {
+        if (idx >= size()) {
+            return d;
+        }
+        return m_data[idx];
+    }
+
+    void reserve(SZ s, T const & d) {
+        if (s > size())
+            resize(s, d);
+    }
+
+    void reserve(SZ s) {
+        if (s > size())
+            resize(s);
+    }
+};
+
+template<typename T>
+class old_ptr_vector : public old_vector<T *, false> {
+public:
+    old_ptr_vector():old_vector<T *, false>() {}
+    old_ptr_vector(unsigned s):old_vector<T *, false>(s) {}
+    old_ptr_vector(unsigned s, T * elem):old_vector<T *, false>(s, elem) {}
+    old_ptr_vector(old_ptr_vector const & source):old_vector<T *, false>(source) {}
+    old_ptr_vector(old_ptr_vector && other) : old_vector<T*, false>(std::move(other)) {}
+    old_ptr_vector(unsigned s, T * const * data):old_vector<T *, false>(s, const_cast<T**>(data)) {}
+    old_ptr_vector & operator=(old_ptr_vector const & source) {
+        old_vector<T *, false>::operator=(source);
+        return *this;
+    }
+};
+
+template<typename T, typename SZ = unsigned>
+class old_svector : public old_vector<T, false, SZ> {
+public:
+    old_svector():old_vector<T, false, SZ>() {}
+    old_svector(SZ s):old_vector<T, false, SZ>(s) {}
+    old_svector(SZ s, T const & elem):old_vector<T, false, SZ>(s, elem) {}
+    old_svector(old_svector const & source):old_vector<T, false, SZ>(source) {}
+    old_svector(old_svector && other) : old_vector<T, false, SZ>(std::move(other)) {}
+    old_svector(SZ s, T const * data):old_vector<T, false, SZ>(s, data) {}
+    old_svector & operator=(old_svector const & source) {
+        old_vector<T, false, SZ>::operator=(source);
+        return *this;
+    }
+};
+
+#endif /* OLD_VECTOR_H_ */
diff --git a/src/util/vector.h b/src/util/vector.h
index acbcd1357..b3625bdfc 100644
--- a/src/util/vector.h
+++ b/src/util/vector.h
@@ -1,616 +1,23 @@
-/*++
-Copyright (c) 2006 Microsoft Corporation
-
-Module Name:
-
-    vector.h
-
-Abstract:
-    Dynamic array implementation. 
-    Remarks:
-
-    - Empty arrays consume only sizeof(T *) bytes.
-
-    - There is the option of disabling the destructor invocation for elements stored in the vector.
-    This is useful for vectors of int.
-
-Author:
-
-    Leonardo de Moura (leonardo) 2006-09-11.
-
-Revision History:
-
---*/
 #ifndef VECTOR_H_
 #define VECTOR_H_
 
-#include "util/debug.h"
-#include<algorithm>
-#include<type_traits>
-#include<memory.h>
-#include<functional>
-#include "util/memory_manager.h"
-#include "util/hash.h"
-#include "util/z3_exception.h"
-
-// disable warning for constant 'if' expressions.
-// these are used heavily in templates.
-#ifdef _MSC_VER
-#pragma warning(disable:4127)
-#endif
+#include "old_vector.h"
+#include "hash.h"
 
 template<typename T, bool CallDestructors=true, typename SZ = unsigned>
-class vector {
-#define SIZE_IDX     -1
-#define CAPACITY_IDX -2
-    T * m_data;
-
-    void destroy_elements() {
-        iterator it = begin();
-        iterator e  = end();
-        for (; it != e; ++it) {
-            it->~T();
-        }
-    }
-
-    void free_memory() { 
-        memory::deallocate(reinterpret_cast<char*>(reinterpret_cast<SZ*>(m_data) - 2));
-    }
-
-    void expand_vector() {
-        if (m_data == nullptr) {
-            SZ capacity = 2;
-            SZ * mem    = reinterpret_cast<SZ*>(memory::allocate(sizeof(T) * capacity + sizeof(SZ) * 2));
-            *mem              = capacity; 
-            mem++;
-            *mem              = 0;        
-            mem++;
-            m_data            = reinterpret_cast<T *>(mem);
-        }
-        else {
-            SASSERT(capacity() > 0);
-            SZ old_capacity = reinterpret_cast<SZ *>(m_data)[CAPACITY_IDX];
-            SZ old_capacity_T = sizeof(T) * old_capacity + sizeof(SZ) * 2;
-            SZ new_capacity = (3 * old_capacity + 1) >> 1;
-            SZ new_capacity_T = sizeof(T) * new_capacity + sizeof(SZ) * 2;
-            if (new_capacity <= old_capacity || new_capacity_T <= old_capacity_T) {
-                throw default_exception("Overflow encountered when expanding vector");
-            }
-            SZ *mem, *old_mem = reinterpret_cast<SZ*>(m_data) - 2;
-#if defined(__GNUC__) && !defined(__clang__) && __GNUC__ < 5
-            if (__has_trivial_copy(T)) {
-#else
-            if (std::is_trivially_copyable<T>::value) {
-#endif
-                mem = (SZ*)memory::reallocate(old_mem, new_capacity_T);
-                m_data = reinterpret_cast<T *>(mem + 2);
-            } else {
-                mem = (SZ*)memory::allocate(new_capacity_T);
-                auto old_data = m_data;
-                auto old_size = size();
-                mem[1] = old_size;
-                m_data  = reinterpret_cast<T *>(mem + 2);
-                for (unsigned i = 0; i < old_size; ++i) {
-                    new (&m_data[i]) T(std::move(old_data[i]));
-                    old_data[i].~T();
-                }
-                memory::deallocate(old_mem);
-            }
-            *mem = new_capacity;
-        }
-    }
-
-    void copy_core(vector const & source) {
-        SZ size      = source.size();
-        SZ capacity  = source.capacity();
-        SZ * mem     = reinterpret_cast<SZ*>(memory::allocate(sizeof(T) * capacity + sizeof(SZ) * 2));
-        *mem = capacity; 
-        mem++;
-        *mem = size; 
-        mem++;
-        m_data             = reinterpret_cast<T *>(mem);
-        const_iterator it  = source.begin();
-        iterator it2       = begin();
-        SASSERT(it2 == m_data);
-        const_iterator e   = source.end();
-        for (; it != e; ++it, ++it2) {
-            new (it2) T(*it); 
-        }
-    }
-
-    void destroy() {
-        if (m_data) { 
-            if (CallDestructors) {
-                destroy_elements(); 
-            }
-            free_memory(); 
-        } 
-    }
-
-public:
-    typedef T data;
-    typedef T * iterator;
-    typedef const T * const_iterator;
-
-    vector():
-        m_data(nullptr) {
-    }
-
-    vector(SZ s) {
-        if (s == 0) {
-            m_data = nullptr;
-            return;
-        }
-        SZ * mem = reinterpret_cast<SZ*>(memory::allocate(sizeof(T) * s + sizeof(SZ) * 2));
-        *mem = s; 
-        mem++;
-        *mem = s; 
-        mem++;
-        m_data = reinterpret_cast<T *>(mem);
-        // initialize elements
-        iterator it = begin();
-        iterator e  = end();
-        for (; it != e; ++it) {
-            new (it) T(); 
-        }
-    }
-
-    vector(SZ s, T const & elem):
-        m_data(nullptr) {
-        resize(s, elem);
-    }
-
-    vector(vector const & source):
-        m_data(nullptr) {
-        if (source.m_data) {
-            copy_core(source);
-        }
-        SASSERT(size() == source.size());
-    }
-
-    vector(vector&& other) : m_data(nullptr) {
-        std::swap(m_data, other.m_data);
-    }
-
-    vector(SZ s, T const * data):
-        m_data(nullptr) {
-        for (SZ i = 0; i < s; i++) {
-            push_back(data[i]);
-        }
-    }
-
- 
-    ~vector() { 
-        destroy();
-    } 
-
-    void finalize() {
-        destroy();
-        m_data = nullptr;
-    }
-
-    bool operator==(vector const & other) const {
-        if (this == &other) {
-            return true;
-        }
-        if (size() != other.size())
-            return false;
-        for (unsigned i = 0; i < size(); i++) {
-            if ((*this)[i] != other[i])
-                return false;
-        }
-        return true;
-    }
-
-    bool operator!=(vector const & other) const {
-        return !(*this == other);
-    }
-
-    
-    vector & operator=(vector const & source) {
-        if (this == &source) {
-            return *this;
-        }
-        destroy();
-        if (source.m_data) {
-            copy_core(source);
-        }
-        else {
-            m_data = nullptr;
-        }
-        return *this;
-    }
-
-    vector & operator=(vector && source) {
-        if (this == &source) {
-            return *this;
-        }
-        destroy();
-        m_data = nullptr;
-        std::swap(m_data, source.m_data);
-        return *this;
-    }
-
-    bool containsp(std::function<bool(T)>& predicate) const {
-        for (auto const& t : *this)
-            if (predicate(t)) 
-                return true;
-        return false;
-    }
-
-    /**
-     * retain elements that satisfy predicate. aka 'where'.
-     */
-    vector filter_pure(std::function<bool(T)>& predicate) const {
-        vector result;
-        for (auto& t : *this)
-            if (predicate(t)) 
-                result.push_back(t);
-        return result;
-    }
-
-    vector& filter_update(std::function<bool(T)>& predicate) {
-        unsigned j = 0;
-        for (auto& t : *this)
-            if (predicate(t)) 
-                set(j++, t);
-        shrink(j);
-        return *this;
-    }
-
-    /**
-     * update elements using f, aka 'select'
-     */
-    template <typename S>
-    vector<S> map_pure(std::function<S(T)>& f) const {
-        vector<S> result;
-        for (auto& t : *this)
-            result.push_back(f(t));
-        return result;
-    }
-
-    vector& map_update(std::function<T(T)>& f) {
-        unsigned j = 0;
-        for (auto& t : *this)
-            set(j++, f(t));
-        return *this;
-    }
-
-    void reset() { 
-        if (m_data) {
-            if (CallDestructors) {
-                destroy_elements();
-            }
-            reinterpret_cast<SZ *>(m_data)[SIZE_IDX] = 0;
-        }
-    }
-
-    void clear() { reset(); }
-
-    bool empty() const { 
-        return m_data == nullptr || reinterpret_cast<SZ *>(m_data)[SIZE_IDX] == 0;
-    }
-
-    SZ size() const { 
-        if (m_data == nullptr) {
-            return 0;  
-        }
-        return reinterpret_cast<SZ *>(m_data)[SIZE_IDX]; 
-    }
-
-    SZ capacity() const { 
-        if (m_data == nullptr) {
-            return 0;
-        }
-        return reinterpret_cast<SZ *>(m_data)[CAPACITY_IDX]; 
-    }
-
-    iterator begin() { 
-        return m_data; 
-    }
-
-    iterator end() { 
-        return m_data + size();
-    }
-
-    const_iterator begin() const { 
-        return m_data; 
-    }
-
-    const_iterator end() const { 
-        return m_data + size(); 
-    }
-
-    class reverse_iterator {
-        T* v;
-    public:
-        reverse_iterator(T* v):v(v) {}
-        
-        T operator*() { return *v; }
-        reverse_iterator operator++(int) {
-            reverse_iterator tmp = *this;
-            --v;
-            return tmp;
-        }
-        reverse_iterator& operator++() {
-            --v;
-            return *this;
-        }
-
-        bool operator==(reverse_iterator const& other) const {
-            return other.v == v;
-        }
-        bool operator!=(reverse_iterator const& other) const {
-            return other.v != v;
-        }
-    };
-
-    reverse_iterator rbegin() { return reverse_iterator(end() - 1); }
-    reverse_iterator rend() { return reverse_iterator(begin() - 1); }
-
-    void set_end(iterator it) {
-        if (m_data) {
-            SZ new_sz = static_cast<SZ>(it - m_data);
-            if (CallDestructors) {
-                iterator e = end();
-                for(; it != e; ++it) {
-                    it->~T();
-                }
-            }
-            reinterpret_cast<SZ *>(m_data)[SIZE_IDX] = new_sz;
-        }
-        else {
-            SASSERT(it == 0);
-        }
-    }
-
-    T & operator[](SZ idx) { 
-        SASSERT(idx < size()); 
-        return m_data[idx]; 
-    }
-
-    T const & operator[](SZ idx) const { 
-        SASSERT(idx < size()); 
-        return m_data[idx];
-    }
-
-    T & get(SZ idx) { 
-        SASSERT(idx < size()); 
-        return m_data[idx]; 
-    }
-
-    T const & get(SZ idx) const { 
-        SASSERT(idx < size()); 
-        return m_data[idx];
-    }
-
-    void set(SZ idx, T const & val) { 
-        SASSERT(idx < size()); 
-        m_data[idx] = val;
-    }
-
-    void set(SZ idx, T && val) {
-        SASSERT(idx < size());
-        m_data[idx] = std::move(val);
-    }
-
-    T & back() { 
-        SASSERT(!empty()); 
-        return operator[](size() - 1); 
-    }
-
-    T const & back() const { 
-        SASSERT(!empty()); 
-        return operator[](size() - 1); 
-    }
-
-    void pop_back() { 
-        SASSERT(!empty()); 
-        if (CallDestructors) {
-            back().~T(); 
-        }
-        reinterpret_cast<SZ *>(m_data)[SIZE_IDX]--; 
-    }
-
-    void push_back(T const & elem) {
-        if (m_data == nullptr || reinterpret_cast<SZ *>(m_data)[SIZE_IDX] == reinterpret_cast<SZ *>(m_data)[CAPACITY_IDX]) {
-            expand_vector();
-        }
-        new (m_data + reinterpret_cast<SZ *>(m_data)[SIZE_IDX]) T(elem); 
-        reinterpret_cast<SZ *>(m_data)[SIZE_IDX]++;
-    }
-
-    void push_back(T && elem) {
-        if (m_data == nullptr || reinterpret_cast<SZ *>(m_data)[SIZE_IDX] == reinterpret_cast<SZ *>(m_data)[CAPACITY_IDX]) {
-            expand_vector();
-        }
-        new (m_data + reinterpret_cast<SZ *>(m_data)[SIZE_IDX]) T(std::move(elem));
-        reinterpret_cast<SZ *>(m_data)[SIZE_IDX]++;
-    }
-
-    void insert(T const & elem) {
-        push_back(elem);
-    }
-
-    void erase(iterator pos) {
-        SASSERT(pos >= begin() && pos < end());
-        iterator prev = pos;
-        ++pos;
-        iterator e    = end();
-        for(; pos != e; ++pos, ++prev) {
-            *prev = *pos;
-        }
-        reinterpret_cast<SZ *>(m_data)[SIZE_IDX]--;
-    }
-
-    void erase(T const & elem) {
-        iterator it = std::find(begin(), end(), elem);
-        if (it != end()) {
-            erase(it);
-        }
-    }
-
-    void shrink(SZ s) {
-        if (m_data) {
-            SASSERT(s <= reinterpret_cast<SZ *>(m_data)[SIZE_IDX]);
-            if (CallDestructors) {
-                iterator it = m_data + s;
-                iterator e  = end();
-                for(; it != e; ++it) {
-                    it->~T();
-                }
-            }
-            reinterpret_cast<SZ *>(m_data)[SIZE_IDX] = s;
-        }
-        else {
-            SASSERT(s == 0);
-        }
-    }
-
-    template<typename Args>
-    void resize(SZ s, Args args...) {
-        SZ sz = size();
-        if (s <= sz) { shrink(s); return; }
-        while (s > capacity()) {
-            expand_vector();
-        }
-        SASSERT(m_data != 0);
-        reinterpret_cast<SZ *>(m_data)[SIZE_IDX] = s;
-        iterator it  = m_data + sz;
-        iterator end = m_data + s;
-        for (; it != end; ++it) {
-            new (it) T(std::forward<Args>(args));
-        }
-    }
-
-    void resize(SZ s) {
-        SZ sz = size();
-        if (s <= sz) { shrink(s); return; }
-        while (s > capacity()) {
-            expand_vector();
-        }
-        SASSERT(m_data != 0);
-        reinterpret_cast<SZ *>(m_data)[SIZE_IDX] = s;
-        iterator it  = m_data + sz;
-        iterator end = m_data + s;
-        for (; it != end; ++it) {
-            new (it) T();
-        }
-    }
-
-    void append(vector<T, CallDestructors> const & other) {
-        for(SZ i = 0; i < other.size(); ++i) {
-            push_back(other[i]);
-        }
-    }
-
-    void append(SZ sz, T const * data) {
-        for(SZ i = 0; i < sz; ++i) {
-            push_back(data[i]);
-        }
-    }
-
-    T * c_ptr() const {
-        return m_data;
-    }
-
-    void swap(vector & other) {
-        std::swap(m_data, other.m_data);
-    }
-
-    void reverse() {
-        SZ sz = size();
-        for (SZ i = 0; i < sz/2; ++i) {
-            std::swap(m_data[i], m_data[sz-i-1]);
-        }
-    }
-
-    void fill(T const & elem) {
-        iterator i = begin();
-        iterator e = end();
-        for (; i != e; ++i) {
-            *i = elem;
-        }
-    }
-
-    void fill(unsigned sz, T const & elem) {
-        resize(sz);
-        fill(elem);
-    }
-
-    bool contains(T const & elem) const {
-        const_iterator it  = begin();
-        const_iterator e = end();
-        for (; it != e; ++it) {
-            if (*it == elem) {
-                return true;
-            }
-        }
-        return false;
-    }
-
-    // set pos idx with elem. If idx >= size, then expand using default.
-    void setx(SZ idx, T const & elem, T const & d) {
-        if (idx >= size()) {
-            resize(idx+1, d);
-        }
-        m_data[idx] = elem;
-    }
-
-    // return element at position idx, if idx >= size, then return default
-    T const & get(SZ idx, T const & d) const {
-        if (idx >= size()) {
-            return d;
-        }
-        return m_data[idx];
-    }
-
-    void reserve(SZ s, T const & d) {
-        if (s > size())
-            resize(s, d);
-    }
-
-    void reserve(SZ s) {
-        if (s > size())
-            resize(s);
-    }
-};
-
-template<typename T>
-class ptr_vector : public vector<T *, false> {
-public:
-    ptr_vector():vector<T *, false>() {}
-    ptr_vector(unsigned s):vector<T *, false>(s) {}
-    ptr_vector(unsigned s, T * elem):vector<T *, false>(s, elem) {}
-    ptr_vector(ptr_vector const & source):vector<T *, false>(source) {}
-    ptr_vector(ptr_vector && other) : vector<T*, false>(std::move(other)) {}
-    ptr_vector(unsigned s, T * const * data):vector<T *, false>(s, const_cast<T**>(data)) {}
-    ptr_vector & operator=(ptr_vector const & source) {
-        vector<T *, false>::operator=(source);
-        return *this;
-    }
-};
+using vector = old_vector<T, CallDestructors, SZ>;
 
 template<typename T, typename SZ = unsigned>
-class svector : public vector<T, false, SZ> {
-public:
-    svector():vector<T, false, SZ>() {}
-    svector(SZ s):vector<T, false, SZ>(s) {}
-    svector(SZ s, T const & elem):vector<T, false, SZ>(s, elem) {}
-    svector(svector const & source):vector<T, false, SZ>(source) {}
-    svector(svector && other) : vector<T, false, SZ>(std::move(other)) {}
-    svector(SZ s, T const * data):vector<T, false, SZ>(s, data) {}
-    svector & operator=(svector const & source) {
-        vector<T, false, SZ>::operator=(source);
-        return *this;
-    }
-};
+using svector = old_svector<T, SZ>;
 
-typedef svector<int> int_vector;
-typedef svector<unsigned> unsigned_vector;
-typedef svector<char> char_vector;
-typedef svector<signed char> signed_char_vector;
-typedef svector<double> double_vector;
+template<typename T>
+using ptr_vector = old_ptr_vector<T>;
+
+using int_vector         = old_svector<int>;
+using unsigned_vector    = old_svector<unsigned>;
+using char_vector        = old_svector<char>;
+using signed_char_vector = old_svector<signed char>;
+using double_vector      = old_svector<double>;
 
 inline std::ostream& operator<<(std::ostream& out, unsigned_vector const& v) {
     for (unsigned u : v) out << u << " ";

From 4c799c144a2f7554b449dc3a0ad6432e4a348c3f Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Fri, 22 Feb 2019 11:14:20 +0100
Subject: [PATCH 3/7] fix gc to not remove ternary clauses that are on
 assignment trail. This addresses issue with drat proofs that don't pass
 drat-trim due to deletion during gc, but use in conflicts

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/sat/sat_clause.cpp        |   2 +-
 src/sat/sat_drat.cpp          | 113 +++++++++++++++++++++++++---------
 src/sat/sat_drat.h            |   4 ++
 src/sat/sat_elim_eqs.cpp      |   2 +-
 src/sat/sat_probing.cpp       |   3 +
 src/sat/sat_simplifier.cpp    |  24 ++++----
 src/sat/sat_simplifier.h      |   2 +-
 src/sat/sat_solver.cpp        |  88 ++++++++++++++++++++++----
 src/sat/sat_solver.h          |  23 +++----
 src/sat/sat_watched.cpp       |  10 ++-
 src/sat/tactic/sat_tactic.cpp |   1 +
 11 files changed, 201 insertions(+), 71 deletions(-)

diff --git a/src/sat/sat_clause.cpp b/src/sat/sat_clause.cpp
index d27820e71..03ae55092 100644
--- a/src/sat/sat_clause.cpp
+++ b/src/sat/sat_clause.cpp
@@ -38,7 +38,6 @@ namespace sat {
         memcpy(m_lits, lits, sizeof(literal) * sz);
         mark_strengthened();
         SASSERT(check_approx());
-        SASSERT(sz > 1);
     }
 
     var_approx_set clause::approx(unsigned num, literal const * lits) {
@@ -83,6 +82,7 @@ namespace sat {
         i++;
         for (; i < m_size; i++)
             m_lits[i-1] = m_lits[i];
+        m_lits[m_size-1] = l;
         m_size--;
         mark_strengthened();
     }
diff --git a/src/sat/sat_drat.cpp b/src/sat/sat_drat.cpp
index ac05b50f1..de65aca92 100644
--- a/src/sat/sat_drat.cpp
+++ b/src/sat/sat_drat.cpp
@@ -49,10 +49,13 @@ namespace sat {
         dealloc(m_bout);
         for (unsigned i = 0; i < m_proof.size(); ++i) {
             clause* c = m_proof[i];
-            if (c && (c->size() == 2 || m_status[i] == status::deleted || m_status[i] == status::external)) {
-                s.dealloc_clause(c);
+            if (c) {
+                m_alloc.del_clause(c);
             }
         }
+        m_proof.reset();
+        m_out = nullptr;
+        m_bout = nullptr;
     }
 
     void drat::updt_config() {
@@ -75,7 +78,7 @@ namespace sat {
         if (st == status::asserted || st == status::external) {
             return;
         }
-
+        
         char buffer[10000];
         char digits[20];     // enough for storing unsigned
         char* lastd = digits + sizeof(digits);
@@ -166,6 +169,9 @@ namespace sat {
     }
 
     void drat::append(literal l, status st) {
+        TRACE("sat_drat", tout << st << " " << l << "\n";);
+
+        declare(l);
         IF_VERBOSE(20, trace(verbose_stream(), 1, &l, st););
         if (st == status::learned) {
             verify(1, &l);
@@ -177,13 +183,15 @@ namespace sat {
             assign_propagate(l);
         }
 
-        clause* c = s.alloc_clause(1, &l, st == status::learned);
-        m_proof.push_back(c);
-        m_status.push_back(st);
+        m_units.push_back(l);
     }
 
     void drat::append(literal l1, literal l2, status st) {
+        TRACE("sat_drat", tout << st << " " << l1 << " " << l2 << "\n";);
+        declare(l1); 
+        declare(l2);
         literal lits[2] = { l1, l2 };
+        
         IF_VERBOSE(20, trace(verbose_stream(), 2, lits, st););
         if (st == status::deleted) {
             // noop
@@ -193,7 +201,7 @@ namespace sat {
             if (st == status::learned) {
                 verify(2, lits);
             }
-            clause* c = s.alloc_clause(2, lits, st == status::learned);
+            clause* c = m_alloc.mk_clause(2, lits, st == status::learned);
             m_proof.push_back(c);
             m_status.push_back(st);
             if (!m_check_unsat) return;
@@ -214,14 +222,37 @@ namespace sat {
         }
     }
 
+#if 0
+    // debugging code
+    bool drat::is_clause(clause& c, literal l1, literal l2, literal l3, drat::status st1, drat::status st2) {
+        //if (st1 != st2) return false;
+        if (c.size() != 3) return false;
+        if (l1 == c[0]) {
+            if (l2 == c[1] && l3 == c[2]) return true;
+            if (l2 == c[2] && l3 == c[1]) return true;
+        }
+        if (l2 == c[0]) {
+            if (l1 == c[1] && l3 == c[2]) return true;
+            if (l1 == c[2] && l3 == c[1]) return true;
+        }
+        if (l3 == c[0]) {
+            if (l1 == c[1] && l2 == c[2]) return true;
+            if (l1 == c[2] && l2 == c[1]) return true;
+        }
+        return false;
+    }
+#endif
+
     void drat::append(clause& c, status st) {
+        TRACE("sat_drat", tout << st << " " << c << "\n";);
+        for (literal lit : c) declare(lit);
         unsigned n = c.size();
         IF_VERBOSE(20, trace(verbose_stream(), n, c.begin(), st););
 
         if (st == status::learned) {
             verify(c);
         }
-
+           
         m_status.push_back(st);
         m_proof.push_back(&c); 
         if (st == status::deleted) {
@@ -274,6 +305,7 @@ namespace sat {
     }
 
     void drat::declare(literal l) {
+        if (!m_check) return;
         unsigned n = static_cast<unsigned>(l.var());
         while (m_assignment.size() <= n) {
             m_assignment.push_back(l_undef);
@@ -379,7 +411,7 @@ namespace sat {
                     case l_undef: num_undef++; break;
                     }
                 }
-                CTRACE("sat", num_true == 0 && num_undef == 1, display(tout););
+                CTRACE("sat_drat", num_true == 0 && num_undef == 1, display(tout););
                 SASSERT(num_true != 0 || num_undef != 1);
             }
         }
@@ -423,7 +455,7 @@ namespace sat {
             exit(0);
             UNREACHABLE();
             //display(std::cout);
-            TRACE("sat", 
+            TRACE("sat_drat", 
                   tout << literal_vector(n, c) << "\n";
                   display(tout); 
                   s.display(tout););
@@ -431,16 +463,41 @@ namespace sat {
         }
     }
 
+    bool drat::contains(literal c, justification const& j) {
+        if (!m_check_sat) {
+            return true;
+        }
+        switch (j.get_kind()) {
+        case justification::NONE:
+            return m_units.contains(c);
+        case justification::BINARY:
+            return contains(c, j.get_literal());
+        case justification::TERNARY:
+            return contains(c, j.get_literal1(), j.get_literal2());
+        case justification::CLAUSE: 
+            return contains(s.get_clause(j));
+        default:
+            return true;
+        }
+    }
+
     bool drat::contains(unsigned n, literal const* lits) {
         if (!m_check) return true;
+        unsigned num_add = 0;
+        unsigned num_del = 0;
         for (unsigned i = m_proof.size(); i-- > 0; ) {
             clause& c = *m_proof[i];
             status st = m_status[i];
             if (match(n, lits, c)) {
-                return st != status::deleted;
+                if (st == status::deleted) {
+                    num_del++;
+                } 
+                else {
+                    num_add++;
+                }
             }
         }
-        return false;
+        return num_add > num_del;
     }
 
     bool drat::match(unsigned n, literal const* lits, clause const& c) const {
@@ -454,7 +511,9 @@ namespace sat {
                         break;
                     }
                 }
-                if (!found) return false;
+                if (!found) {
+                    return false;
+                }
             }
             return true;
         }
@@ -512,7 +571,7 @@ namespace sat {
     void drat::assign(literal l) {
         lbool new_value = l.sign() ? l_false : l_true;
         lbool old_value = value(l);
-//        TRACE("sat", tout << "assign " << l << " := " << new_value << " from " << old_value << "\n";);
+//        TRACE("sat_drat", tout << "assign " << l << " := " << new_value << " from " << old_value << "\n";);
         switch (old_value) {
         case l_false:
             m_inconsistent = true;
@@ -544,7 +603,7 @@ namespace sat {
             watched_clause& wc = m_watched_clauses[idx];
             clause& c = *wc.m_clause;
 
-            //TRACE("sat", tout << "Propagate " << l << " " << c << " watch: " << wc.m_l1 << " " << wc.m_l2 << "\n";);
+            //TRACE("sat_drat", tout << "Propagate " << l << " " << c << " watch: " << wc.m_l1 << " " << wc.m_l2 << "\n";);
             if (wc.m_l1 == ~l) {
                 std::swap(wc.m_l1, wc.m_l2);
             }
@@ -596,17 +655,12 @@ namespace sat {
         }
     }
     void drat::add(literal l, bool learned) {
-        TRACE("sat", tout << "add: " << l << " " << (learned?"l":"t") << "\n";);
-        declare(l);
         status st = get_status(learned);
         if (m_out) dump(1, &l, st);
         if (m_bout) bdump(1, &l, st);
         if (m_check) append(l, st);
     }
     void drat::add(literal l1, literal l2, bool learned) {
-        TRACE("sat", tout << "add: " << l1 << " " << l2 << " " << (learned?"l":"t") << "\n";);
-        declare(l1);
-        declare(l2);
         literal ls[2] = {l1, l2};
         status st = get_status(learned);
         if (m_out) dump(2, ls, st);
@@ -614,12 +668,13 @@ namespace sat {
         if (m_check) append(l1, l2, st);
     }
     void drat::add(clause& c, bool learned) {
-        TRACE("sat", tout << "add: " << c << "\n";);
-        for (unsigned i = 0; i < c.size(); ++i) declare(c[i]);
         status st = get_status(learned);
         if (m_out) dump(c.size(), c.begin(), st);
         if (m_bout) bdump(c.size(), c.begin(), st);
-        if (m_check_unsat) append(c, get_status(learned));
+        if (m_check) {
+            clause* cl = m_alloc.mk_clause(c.size(), c.begin(), learned);
+            append(*cl, get_status(learned));
+        }
     }
     void drat::add(literal_vector const& lits, svector<premise> const& premises) {
         if (m_check) {
@@ -627,7 +682,7 @@ namespace sat {
             case 0: add(); break;
             case 1: append(lits[0], status::external); break;
             default: {
-                clause* c = s.alloc_clause(lits.size(), lits.c_ptr(), true);
+                clause* c = m_alloc.mk_clause(lits.size(), lits.c_ptr(), true);
                 append(*c, status::external);
                 break;
             }
@@ -635,16 +690,16 @@ namespace sat {
         }                        
     }
     void drat::add(literal_vector const& c) {
-        for (unsigned i = 0; i < c.size(); ++i) declare(c[i]);
         if (m_out) dump(c.size(), c.begin(), status::learned);
         if (m_bout) bdump(c.size(), c.begin(), status::learned);
         if (m_check) {
+            for (literal lit : c) declare(lit);
             switch (c.size()) {
             case 0: add(); break;
             case 1: append(c[0], status::learned); break;
             default: {
                 verify(c.size(), c.begin());
-                clause* cl = s.alloc_clause(c.size(), c.c_ptr(), true);
+                clause* cl = m_alloc.mk_clause(c.size(), c.c_ptr(), true);
                 append(*cl, status::external);                
                 break;
             }
@@ -657,8 +712,10 @@ namespace sat {
         if (m_bout) bdump(1, &l, status::deleted);
         if (m_check_unsat) append(l, status::deleted);
     }
+
     void drat::del(literal l1, literal l2) {
         literal ls[2] = {l1, l2};
+        SASSERT(!(l1 == literal(13923, false) && l2 == literal(14020, true)));
         if (m_out) dump(2, ls, status::deleted);
         if (m_bout) bdump(2, ls, status::deleted);
         if (m_check) append(l1, l2, status::deleted);
@@ -677,11 +734,11 @@ namespace sat {
         }
 #endif
 
-        TRACE("sat", tout << "del: " << c << "\n";);
+        //SASSERT(!(c.size() == 2 && c[0] == literal(13923, false) && c[1] == literal(14020, true)));
         if (m_out) dump(c.size(), c.begin(), status::deleted);
         if (m_bout) bdump(c.size(), c.begin(), status::deleted);
         if (m_check) {
-            clause* c1 = s.alloc_clause(c.size(), c.begin(), c.is_learned()); 
+            clause* c1 = m_alloc.mk_clause(c.size(), c.begin(), c.is_learned()); 
             append(*c1, status::deleted);
         }
     }
diff --git a/src/sat/sat_drat.h b/src/sat/sat_drat.h
index 35e5a0655..7224da063 100644
--- a/src/sat/sat_drat.h
+++ b/src/sat/sat_drat.h
@@ -45,6 +45,7 @@ namespace sat {
         svector<watched_clause>   m_watched_clauses;
         typedef svector<unsigned> watch;
         solver& s;
+        clause_allocator        m_alloc;
         std::ostream*           m_out;
         std::ostream*           m_bout;
         ptr_vector<clause>      m_proof;
@@ -61,6 +62,8 @@ namespace sat {
         void append(literal l1, literal l2, status st);
         void append(clause& c, status st);
 
+        bool is_clause(clause& c, literal l1, literal l2, literal l3, status st1, status st2);
+
         friend std::ostream& operator<<(std::ostream & out, status st);
         status get_status(bool learned) const;
 
@@ -104,6 +107,7 @@ namespace sat {
         bool contains(unsigned n, literal const* c);
         bool contains(literal l1, literal l2) { literal lits[2] = {l1, l2}; return contains(2, lits); }
         bool contains(literal l1, literal l2, literal l3) { literal lits[3] = {l1, l2, l3}; return contains(3, lits); }
+        bool contains(literal c, justification const& j);
 
         void check_model(model const& m);
     };
diff --git a/src/sat/sat_elim_eqs.cpp b/src/sat/sat_elim_eqs.cpp
index bc69c1f5d..7e19bf520 100644
--- a/src/sat/sat_elim_eqs.cpp
+++ b/src/sat/sat_elim_eqs.cpp
@@ -207,7 +207,7 @@ namespace sat {
                     c.update_approx();
                 }
                 if (m_solver.m_config.m_drat) {
-                    m_solver.m_drat.add(c, true); 
+                    m_solver.m_drat.add(c, true);
                     drat_delete_clause();
                 }
 
diff --git a/src/sat/sat_probing.cpp b/src/sat/sat_probing.cpp
index 5689112d4..e12e78560 100644
--- a/src/sat/sat_probing.cpp
+++ b/src/sat/sat_probing.cpp
@@ -52,6 +52,9 @@ namespace sat {
         unsigned tr_sz = s.m_trail.size();
         for (unsigned i = old_tr_sz; i < tr_sz; i++) {
             entry.m_lits.push_back(s.m_trail[i]);
+            if (s.m_config.m_drat) {
+                s.m_drat.add(~l, s.m_trail[i], true);
+            }
         }
     }
 
diff --git a/src/sat/sat_simplifier.cpp b/src/sat/sat_simplifier.cpp
index 58dab0ff5..86094d7a3 100644
--- a/src/sat/sat_simplifier.cpp
+++ b/src/sat/sat_simplifier.cpp
@@ -124,9 +124,9 @@ namespace sat {
         }
     }
 
-    inline void simplifier::remove_clause(clause & c) {
+    inline void simplifier::remove_clause(clause & c, bool is_unique) {
         if (!c.was_removed()) {
-            if (s.m_config.m_drat) {
+            if (s.m_config.m_drat && is_unique) {
                 s.m_drat.del(c);
             }
             for (literal l : c) {
@@ -477,7 +477,7 @@ namespace sat {
                     s.set_learned(c1, false);
                 }
                 TRACE("subsumption", tout << c1 << " subsumed " << c2 << "\n";);
-                remove_clause(c2);
+                remove_clause(c2, false);
                 m_num_subsumed++;
             }
             else if (!c2.was_removed()) {
@@ -577,7 +577,7 @@ namespace sat {
             if (c1.is_learned() && !c2.is_learned())
                 s.set_learned(c1, false);
             TRACE("subsumption", tout << c1 << " subsumed " << c2 << "\n";);
-            remove_clause(c2);
+            remove_clause(c2, false);
             m_num_subsumed++;
         }
     }
@@ -662,7 +662,7 @@ namespace sat {
             for (auto it = cs.mk_iterator(); !it.at_end(); ) {
                 clause & c = it.curr();
                 it.next();
-                remove_clause(c);
+                remove_clause(c, true);
             }
             cs.reset();            
         }
@@ -674,10 +674,12 @@ namespace sat {
         m_num_elim_lits++;
         insert_elim_todo(l.var());
         if (s.m_config.m_drat && c.contains(l)) {
-            m_dummy.set(c.size(), c.begin(), c.is_learned());
+            unsigned sz = c.size();
             c.elim(l);
             s.m_drat.add(c, true); 
-            s.m_drat.del(*m_dummy.get());
+            c.restore(sz);
+            s.m_drat.del(c);
+            c.shrink(sz-1);
         }
         else {
             c.elim(l);
@@ -690,7 +692,7 @@ namespace sat {
         if (cleanup_clause(c)) {
             // clause was satisfied
             TRACE("elim_lit", tout << "clause was satisfied\n";);
-            remove_clause(c);
+            remove_clause(c, true);
             return;
         }
         unsigned sz = c.size();
@@ -710,7 +712,7 @@ namespace sat {
             c.restore(sz0);
             s.mk_bin_clause(c[0], c[1], c.is_learned());
             m_sub_bin_todo.push_back(bin_clause(c[0], c[1], c.is_learned()));            
-            remove_clause(c);
+            remove_clause(c, sz0 != sz);
             break;
         default:
             if (s.m_config.m_drat && sz0 != sz) {
@@ -888,7 +890,7 @@ namespace sat {
             if (s.m_trail.size() > m_last_sub_trail_sz) {
                 unsigned sz0 = c.size();
                 if (cleanup_clause(c)) {
-                    remove_clause(c);
+                    remove_clause(c, true);
                     continue;
                 }
                 unsigned sz = c.size();
@@ -906,7 +908,7 @@ namespace sat {
                     s.mk_bin_clause(c[0], c[1], c.is_learned());
                     m_sub_bin_todo.push_back(bin_clause(c[0], c[1], c.is_learned()));
                     c.restore(sz0);
-                    remove_clause(c);
+                    remove_clause(c, sz != sz0);
                     continue;
                 default:
                     if (s.m_config.m_drat && sz != sz0) {
diff --git a/src/sat/sat_simplifier.h b/src/sat/sat_simplifier.h
index 2aa2b4252..895ebdcb5 100644
--- a/src/sat/sat_simplifier.h
+++ b/src/sat/sat_simplifier.h
@@ -133,7 +133,7 @@ namespace sat {
 
         void register_clauses(clause_vector & cs);
 
-        void remove_clause(clause & c);
+        void remove_clause(clause & c, bool is_unique);
         void set_learned(clause & c);
         void set_learned(literal l1, literal l2);
 
diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp
index 3deb6fc17..4a0397cee 100644
--- a/src/sat/sat_solver.cpp
+++ b/src/sat/sat_solver.cpp
@@ -33,19 +33,22 @@ Revision History:
 
 namespace sat {
 
+    static unsigned s_lemma_count = 0;
+    static bool     s_verify_contains = false;
+
     solver::solver(params_ref const & p, reslimit& l):
         solver_core(l),
         m_checkpoint_enabled(true),
         m_config(p),
         m_par(nullptr),
         m_cls_allocator_idx(false),
+        m_drat(*this),
         m_cleaner(*this),
         m_simplifier(*this, p),
         m_scc(*this, p),
         m_asymm_branch(*this, p),
         m_probing(*this, p),
         m_mus(*this),
-        m_drat(*this),
         m_inconsistent(false),
         m_searching(false),
         m_num_frozen(0),
@@ -382,6 +385,9 @@ namespace sat {
             if (!learned && !at_search_lvl()) 
                 m_clauses_to_reinit.push_back(clause_wrapper(l1, l2));
         }
+        if (l1 == literal(29327, false) && l2 == literal(29328, false)) {
+            std::cout << s_lemma_count << "\n";            
+        }
         m_stats.m_mk_bin_clause++;
         get_wlist(~l1).push_back(watched(l2, learned));
         get_wlist(~l2).push_back(watched(l1, learned));
@@ -413,8 +419,6 @@ namespace sat {
         clause * r = alloc_clause(3, lits, learned);
         bool reinit = attach_ter_clause(*r);
         if (reinit && !learned) push_reinit_stack(*r);
-        if (m_config.m_drat) m_drat.add(*r, learned);
-
         if (learned)
             m_learned.push_back(r);
         else
@@ -424,6 +428,9 @@ namespace sat {
 
     bool solver::attach_ter_clause(clause & c) {
         bool reinit = false;
+        if (m_config.m_drat) m_drat.add(c, c.is_learned());
+        TRACE("sat", tout << c << "\n";);
+        SASSERT(!c.was_removed());
         m_watches[(~c[0]).index()].push_back(watched(c[1], c[2]));
         m_watches[(~c[1]).index()].push_back(watched(c[0], c[2]));
         m_watches[(~c[2]).index()].push_back(watched(c[0], c[1]));
@@ -459,8 +466,9 @@ namespace sat {
         else {
             m_clauses.push_back(r);
         }
-        if (m_config.m_drat) 
+        if (m_config.m_drat) {
             m_drat.add(*r, learned);
+        }
         return r;
     }
 
@@ -2163,6 +2171,36 @@ namespace sat {
         IF_VERBOSE(SAT_VB_LVL, verbose_stream() << "(sat-gc :strategy " << st_name << " :deleted " << (sz - new_sz) << ")\n";);
     }
 
+    bool solver::can_delete3(literal l1, literal l2, literal l3) const {                                                           
+        if (value(l1) == l_true && 
+            value(l2) == l_false && 
+            value(l3) == l_false) {
+            justification const& j = m_justification[l1.var()];
+            if (j.is_ternary_clause()) {
+                watched w1(l2, l3);
+                watched w2(j.get_literal1(), j.get_literal2());
+                return w1 != w2;
+            }
+        }
+        return true;
+    }
+
+    bool solver::can_delete(clause const & c) const {
+        if (c.on_reinit_stack())
+            return false;
+        if (c.size() == 3) {
+            return
+                can_delete3(c[0],c[1],c[2]) &&
+                can_delete3(c[1],c[0],c[2]) &&
+                can_delete3(c[2],c[0],c[1]);
+        }
+        literal l0 = c[0];
+        if (value(l0) != l_true)
+            return true;
+        justification const & jst = m_justification[l0.var()];
+        return !jst.is_clause() || cls_allocator().get_clause(jst.get_clause_offset()) != &c;
+    }
+
     /**
        \brief Use gc based on dynamic psm. Clauses are initially frozen.
     */
@@ -2381,6 +2419,21 @@ namespace sat {
             }
         }
 
+        s_lemma_count++;
+
+        if (s_lemma_count == 51802) {
+            disable_trace("sat");
+            disable_trace("sat_conflict");
+            s_verify_contains = false;
+        }
+
+
+        if (s_lemma_count == 51801) {
+            enable_trace("sat");
+            enable_trace("sat_conflict");
+            s_verify_contains = true;
+        }
+
         m_lemma.reset();
 
         unsigned idx = skip_literals_above_conflict_level();
@@ -2401,6 +2454,9 @@ namespace sat {
         do {
             TRACE("sat_conflict_detail", tout << "processing consequent: " << consequent << "\n";
                   tout << "num_marks: " << num_marks << ", js: " << js << "\n";);
+
+            // VERIFY(!s_verify_contains || !m_config.m_drat || m_drat.contains(consequent, js));
+
             switch (js.get_kind()) {
             case justification::NONE:
                 break;
@@ -2455,6 +2511,8 @@ namespace sat {
             idx--;
             num_marks--;
             reset_mark(c_var);
+
+            TRACE("sat", display_justification(tout << consequent << " ", js) << "\n";);            
         }
         while (num_marks > 0);
 
@@ -2467,12 +2525,13 @@ namespace sat {
         TRACE("sat_lemma", tout << "new lemma size: " << m_lemma.size() << "\n" << m_lemma << "\n";);
 
         unsigned new_scope_lvl       = 0;
+        bool sub_min = false, res_min = false;
         if (!m_lemma.empty()) {
             if (m_config.m_minimize_lemmas) {
-                minimize_lemma();
+                res_min = minimize_lemma();
                 reset_lemma_var_marks();
                 if (m_config.m_dyn_sub_res)
-                    dyn_sub_res();
+                    sub_min = dyn_sub_res();
                 TRACE("sat_lemma", tout << "new lemma (after minimization) size: " << m_lemma.size() << "\n" << m_lemma << "\n";);
             }
             else
@@ -2492,12 +2551,12 @@ namespace sat {
         m_slow_glue_avg.update(glue);
         pop_reinit(m_scope_lvl - new_scope_lvl);
         TRACE("sat_conflict_detail", tout << glue << " " << new_scope_lvl << "\n";);
-        // unsound: m_asymm_branch.minimize(m_scc, m_lemma);
         clause * lemma = mk_clause_core(m_lemma.size(), m_lemma.c_ptr(), true);
         if (lemma) {
             lemma->set_glue(glue);
             if (m_par) m_par->share_clause(*this, *lemma);
         }
+
         TRACE("sat_conflict_detail", tout << new_scope_lvl << "\n";);
         decay_activity();
         updt_phase_counters();
@@ -2844,7 +2903,7 @@ namespace sat {
             if (m_lvl_set.may_contain(var_lvl)) {
                 mark(var);
                 m_unmark.push_back(var);
-                m_lemma_min_stack.push_back(var);
+                m_lemma_min_stack.push_back(antecedent);
             }
             else {
                 return false;
@@ -2862,11 +2921,12 @@ namespace sat {
     */
     bool solver::implied_by_marked(literal lit) {
         m_lemma_min_stack.reset();  // avoid recursive function
-        m_lemma_min_stack.push_back(lit.var());
+        m_lemma_min_stack.push_back(lit);
         unsigned old_size = m_unmark.size();
 
         while (!m_lemma_min_stack.empty()) {
-            bool_var var       = m_lemma_min_stack.back();
+            lit = m_lemma_min_stack.back();
+            bool_var var = lit.var();
             m_lemma_min_stack.pop_back();
             justification const& js   = m_justification[var];
             switch(js.get_kind()) {
@@ -2928,6 +2988,8 @@ namespace sat {
                 UNREACHABLE();
                 break;
             }
+            TRACE("sat_conflict", 
+                  display_justification(tout << var << " ",js) << "\n";);
         }
         return true;
     }
@@ -2958,7 +3020,7 @@ namespace sat {
        literals that are implied by other literals in m_lemma and/or literals
        assigned at level 0.
     */
-    void solver::minimize_lemma() {
+    bool solver::minimize_lemma() {
         SASSERT(!m_lemma.empty());
         SASSERT(m_unmark.empty());
         updt_lemma_lvl_set();
@@ -2982,6 +3044,7 @@ namespace sat {
         reset_unmark(0);
         m_lemma.shrink(j);
         m_stats.m_minimized_lits += sz - j;
+        return j < sz;
     }
 
     /**
@@ -3055,7 +3118,7 @@ namespace sat {
        \brief Apply dynamic subsumption resolution to new lemma.
        Only binary and ternary clauses are used.
     */
-    void solver::dyn_sub_res() {
+    bool solver::dyn_sub_res() {
         unsigned sz = m_lemma.size();
         for (unsigned i = 0; i < sz; i++) {
             mark_lit(m_lemma[i]);
@@ -3168,6 +3231,7 @@ namespace sat {
 
         SASSERT(j >= 1);
         m_lemma.shrink(j);
+        return j < sz;
     }
 
 
diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h
index c000ccb79..47e226cc4 100644
--- a/src/sat/sat_solver.h
+++ b/src/sat/sat_solver.h
@@ -85,9 +85,10 @@ namespace sat {
         stats                   m_stats;
         scoped_ptr<extension>   m_ext;
         parallel*               m_par;
-        random_gen              m_rand;
+        drat                    m_drat;          // DRAT for generating proofs
         clause_allocator        m_cls_allocator[2];
         bool                    m_cls_allocator_idx;
+        random_gen              m_rand;
         cleaner                 m_cleaner;
         model                   m_model;        
         model_converter         m_mc;
@@ -97,7 +98,6 @@ namespace sat {
         asymm_branch            m_asymm_branch;
         probing                 m_probing;
         mus                     m_mus;           // MUS for minimal core extraction
-        drat                    m_drat;          // DRAT for generating proofs
         bool                    m_inconsistent;
         bool                    m_searching;
         // A conflict is usually a single justification. That is, a justification
@@ -461,17 +461,8 @@ namespace sat {
         void gc_dyn_psm();
         bool activate_frozen_clause(clause & c);
         unsigned psm(clause const & c) const;
-        bool can_delete(clause const & c) const {
-            if (c.on_reinit_stack())
-                return false;
-            if (c.size() == 3)
-                return true; // not needed to justify anything.
-            literal l0 = c[0];
-            if (value(l0) != l_true)
-                return true;
-            justification const & jst = m_justification[l0.var()];
-            return !jst.is_clause() || cls_allocator().get_clause(jst.get_clause_offset()) != &c;
-        }
+        bool can_delete(clause const & c) const;
+        bool can_delete3(literal l1, literal l2, literal l3) const;
 
         clause& get_clause(watch_list::iterator it) const {
             SASSERT(it->get_kind() == watched::CLAUSE);
@@ -522,14 +513,14 @@ namespace sat {
         typedef approx_set_tpl<unsigned, u2u, unsigned> level_approx_set;
         bool_var_vector   m_unmark;
         level_approx_set  m_lvl_set;
-        bool_var_vector   m_lemma_min_stack;
+        literal_vector    m_lemma_min_stack;
         bool process_antecedent_for_minimization(literal antecedent);
         bool implied_by_marked(literal lit);
         void reset_unmark(unsigned old_size);
         void updt_lemma_lvl_set();
-        void minimize_lemma();
         void reset_lemma_var_marks();
-        void dyn_sub_res();
+        bool minimize_lemma();
+        bool dyn_sub_res();
 
         // -----------------------
         //
diff --git a/src/sat/sat_watched.cpp b/src/sat/sat_watched.cpp
index 966bd8325..8811a4e74 100644
--- a/src/sat/sat_watched.cpp
+++ b/src/sat/sat_watched.cpp
@@ -86,7 +86,15 @@ namespace sat {
             }    
         }
         wlist.set_end(it2);
-        //VERIFY(found);
+#if 0
+        VERIFY(found);
+        for (watched const& w2 : wlist) {
+            if (w2 == w) {
+                std::cout << l1 << " " << l2 << "\n";
+            }
+            //VERIFY(w2 != w);
+        }
+#endif
     }
 
     void conflict_cleanup(watch_list::iterator it, watch_list::iterator it2, watch_list& wlist) {
diff --git a/src/sat/tactic/sat_tactic.cpp b/src/sat/tactic/sat_tactic.cpp
index 2739932e6..b2137795b 100644
--- a/src/sat/tactic/sat_tactic.cpp
+++ b/src/sat/tactic/sat_tactic.cpp
@@ -200,6 +200,7 @@ public:
             throw tactic_exception(ex.msg());
         }
         catch (z3_exception& ex) {
+            (void)ex;
             TRACE("sat", tout << ex.msg() << "\n";);            
             throw;
         }

From 699834261e6e8f70d3928409f6a7fde22f34d2ee Mon Sep 17 00:00:00 2001
From: "Christoph M. Wintersteiger" <cwinter@microsoft.com>
Date: Fri, 22 Feb 2019 12:55:01 +0000
Subject: [PATCH 4/7] Fix translation of FPA numerals in ast_smt_pp. Fixes
 #2145.

---
 src/ast/ast_smt_pp.cpp | 30 ++++++++++++++----------------
 1 file changed, 14 insertions(+), 16 deletions(-)

diff --git a/src/ast/ast_smt_pp.cpp b/src/ast/ast_smt_pp.cpp
index 2490e0314..ea220f7e7 100644
--- a/src/ast/ast_smt_pp.cpp
+++ b/src/ast/ast_smt_pp.cpp
@@ -24,6 +24,7 @@ Revision History:
 #include "util/vector.h"
 #include "util/smt2_util.h"
 #include "ast/ast_smt_pp.h"
+#include "ast/ast_smt2_pp.h"
 #include "ast/arith_decl_plugin.h"
 #include "ast/bv_decl_plugin.h"
 #include "ast/array_decl_plugin.h"
@@ -223,7 +224,7 @@ class smt_printer {
             }
         }
         else if (m_manager.is_ite(d)) {
-            m_out << "ite";            
+            m_out << "ite";
         }
         else if (m_manager.is_implies(d)) {
             m_out << "=>";
@@ -266,7 +267,7 @@ class smt_printer {
         else {
             m_out << "(_ " << sym << " ";
         }
-        
+
         for (unsigned i = 0; i < num_params; ++i) {
             parameter const& p = params[i];
             if (p.is_ast()) {
@@ -320,7 +321,7 @@ class smt_printer {
             if (num_sorts > 0) {
                 m_out << "(";
             }
-            m_out << m_renaming.get_symbol(s->get_name(), false);            
+            m_out << m_renaming.get_symbol(s->get_name(), false);
             if (num_sorts > 0) {
                 for (unsigned i = 0; i < num_sorts; ++i) {
                     m_out << " ";
@@ -388,10 +389,7 @@ class smt_printer {
             m_out << "(_ bv" << val << " " << bv_size << ")";
         }
         else if (m_futil.is_numeral(n, float_val)) {
-            m_out << "((_ to_fp " <<
-                float_val.get().get_ebits() << " " <<
-                float_val.get().get_sbits() << ") RTZ " <<
-                m_futil.fm().to_string(float_val).c_str() << ")";
+            m_out << mk_ismt2_pp(n, m_manager);
         }
         else if (m_bvutil.is_bit2bool(n)) {
             unsigned bit = n->get_decl()->get_parameter(0).get_int();
@@ -402,7 +400,7 @@ class smt_printer {
         else if (m_manager.is_label(n, pos, names) && !names.empty()) {
             m_out << "(! ";
             pp_marked_expr(n->get_arg(0));
-            m_out << (pos?":lblpos":":lblneg") << " " << m_renaming.get_symbol(names[0], false) << ")";            
+            m_out << (pos?":lblpos":":lblneg") << " " << m_renaming.get_symbol(names[0], false) << ")";
         }
         else if (m_manager.is_label_lit(n, names) && !names.empty()) {
             m_out << "(! true :lblpos " << m_renaming.get_symbol(names[0], false) << ")";
@@ -435,7 +433,7 @@ class smt_printer {
             pp_arg(curr, n);
             m_out << ")";
 
-        } 
+        }
         else if (m_manager.is_distinct(decl)) {
             ptr_vector<expr> args(num_args, n->get_args());
             unsigned         idx = 0;
@@ -613,7 +611,7 @@ class smt_printer {
         pp_id(n);
         m_out << " ";
         pp_expr(n);
-        m_out << ")";        
+        m_out << ")";
         m_out << ")";
         newline();
     }
@@ -781,7 +779,7 @@ public:
         datatype_util util(m_manager);
         SASSERT(util.is_datatype(s));
 
-        sort_ref_vector ps(m_manager);        
+        sort_ref_vector ps(m_manager);
         ptr_vector<datatype::def> defs;
         util.get_defs(s, defs);
 
@@ -790,7 +788,7 @@ public:
             if (mark.is_marked(sr)) return; // already processed
             mark.mark(sr, true);
         }
-                
+
         m_out << "(declare-datatypes (";
         bool first_def = true;
         for (datatype::def* d : defs) {
@@ -800,7 +798,7 @@ public:
         m_out << ") (";
         bool first_sort = true;
         for (datatype::def* d : defs) {
-            if (!first_sort) m_out << "\n   "; else first_sort = false; 
+            if (!first_sort) m_out << "\n   "; else first_sort = false;
             if (!d->params().empty()) {
                 m_out << "(par (";
                 bool first_param = true;
@@ -814,7 +812,7 @@ public:
             bool first_constr = true;
             for (datatype::constructor* f : *d) {
                 if (!first_constr) m_out << " "; else first_constr = false;
-                m_out << "(";                
+                m_out << "(";
                 m_out << m_renaming.get_symbol(f->name(), false);
                 for (datatype::accessor* a : *f) {
                     m_out << " (" << m_renaming.get_symbol(a->name(), false) << " ";
@@ -828,7 +826,7 @@ public:
             }
             m_out << ")";
         }
-        m_out << "))";     
+        m_out << "))";
         newline();
     }
 
@@ -864,7 +862,7 @@ public:
         }
         m_out << ") ";
         visit_sort(d->get_range());
-        m_out << ")";       
+        m_out << ")";
     }
 
     void visit_pred(func_decl* d) {

From 73060ecaec864ad09ba6a5c916607bb6c5ca78da Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Fri, 22 Feb 2019 13:57:09 +0100
Subject: [PATCH 5/7] remove debug code

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/sat/sat_solver.cpp | 21 ---------------------
 1 file changed, 21 deletions(-)

diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp
index 3669f801e..c6b04cfd8 100644
--- a/src/sat/sat_solver.cpp
+++ b/src/sat/sat_solver.cpp
@@ -36,8 +36,6 @@ Revision History:
 
 namespace sat {
 
-    static unsigned s_lemma_count = 0;
-    static bool     s_verify_contains = false;
 
     solver::solver(params_ref const & p, reslimit& l):
         solver_core(l),
@@ -388,9 +386,6 @@ namespace sat {
             if (!learned && !at_search_lvl()) 
                 m_clauses_to_reinit.push_back(clause_wrapper(l1, l2));
         }
-        if (l1 == literal(29327, false) && l2 == literal(29328, false)) {
-            std::cout << s_lemma_count << "\n";            
-        }
         m_stats.m_mk_bin_clause++;
         get_wlist(~l1).push_back(watched(l2, learned));
         get_wlist(~l2).push_back(watched(l1, learned));
@@ -2422,20 +2417,6 @@ namespace sat {
             }
         }
 
-        s_lemma_count++;
-
-        if (s_lemma_count == 51802) {
-            disable_trace("sat");
-            disable_trace("sat_conflict");
-            s_verify_contains = false;
-        }
-
-
-        if (s_lemma_count == 51801) {
-            enable_trace("sat");
-            enable_trace("sat_conflict");
-            s_verify_contains = true;
-        }
 
         m_lemma.reset();
 
@@ -2458,8 +2439,6 @@ namespace sat {
             TRACE("sat_conflict_detail", tout << "processing consequent: " << consequent << "\n";
                   tout << "num_marks: " << num_marks << ", js: " << js << "\n";);
 
-            // VERIFY(!s_verify_contains || !m_config.m_drat || m_drat.contains(consequent, js));
-
             switch (js.get_kind()) {
             case justification::NONE:
                 break;

From c0d20f8ea8a39b51b8651481a79e49157bb86548 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sat, 23 Feb 2019 10:59:10 +0100
Subject: [PATCH 6/7] add cr

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/util/buffer.h     | 13 +++++++++++++
 src/util/old_buffer.h |  2 ++
 src/util/old_vector.h |  2 ++
 src/util/vector.h     | 13 +++++++++++++
 4 files changed, 30 insertions(+)

diff --git a/src/util/buffer.h b/src/util/buffer.h
index 7a89ffef3..0d32245d3 100644
--- a/src/util/buffer.h
+++ b/src/util/buffer.h
@@ -1,3 +1,16 @@
+/*++
+Copyright (c) 2019 Microsoft Corporation
+
+Module Name:
+
+    buffer.h
+
+Author:
+
+    Daniel Schemmel 2019-2-23
+
+--*/
+
 #ifndef BUFFER_H_
 #define BUFFER_H_
 
diff --git a/src/util/old_buffer.h b/src/util/old_buffer.h
index 5ed1df583..88800b05a 100644
--- a/src/util/old_buffer.h
+++ b/src/util/old_buffer.h
@@ -15,6 +15,8 @@ Author:
 
 Revision History:
 
+   2019-2-23 Renamed to old_buffer from buffer to provide new implementation
+
 --*/
 #ifndef OLD_BUFFER_H_
 #define OLD_BUFFER_H_
diff --git a/src/util/old_vector.h b/src/util/old_vector.h
index 53450e6cf..47dc88aab 100644
--- a/src/util/old_vector.h
+++ b/src/util/old_vector.h
@@ -20,6 +20,8 @@ Author:
 
 Revision History:
 
+   2019-2-23 Renamed from vector to old_vector to provide new implementation
+
 --*/
 #ifndef OLD_VECTOR_H_
 #define OLD_VECTOR_H_
diff --git a/src/util/vector.h b/src/util/vector.h
index b3625bdfc..9e2e35acc 100644
--- a/src/util/vector.h
+++ b/src/util/vector.h
@@ -1,3 +1,16 @@
+/*++
+Copyright (c) 2019 Microsoft Corporation
+
+Module Name:
+
+    vector.h
+
+Author:
+
+    Daniel Schemmel 2019-2-23
+
+--*/
+
 #ifndef VECTOR_H_
 #define VECTOR_H_
 

From 773c61369480b6f031eb8fa98a7eb24bd52c7070 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sat, 23 Feb 2019 11:10:01 +0100
Subject: [PATCH 7/7] fix #2149

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/ast/rewriter/array_rewriter.cpp | 8 +++++++-
 1 file changed, 7 insertions(+), 1 deletion(-)

diff --git a/src/ast/rewriter/array_rewriter.cpp b/src/ast/rewriter/array_rewriter.cpp
index 83749c82d..56e094dab 100644
--- a/src/ast/rewriter/array_rewriter.cpp
+++ b/src/ast/rewriter/array_rewriter.cpp
@@ -375,7 +375,13 @@ br_status array_rewriter::mk_set_intersect(unsigned num_args, expr * const * arg
 
 
 br_status array_rewriter::mk_set_complement(expr * arg, expr_ref & result) {
-    return mk_map_core(m().mk_not_decl(), 1, &arg, result);
+    func_decl* fnot = m().mk_not_decl();
+    br_status st = mk_map_core(fnot, 1, &arg, result);
+    if (BR_FAILED == st) {
+        result = m_util.mk_map(fnot, 1, &arg);
+        st = BR_DONE;
+    }
+    return st;
 }
 
 br_status array_rewriter::mk_set_difference(expr * arg1, expr * arg2, expr_ref & result) {