fix #3878

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

src/math/lp/nla_common.cpp

@@ -194,4 +194,4 @@ template <typename T> void common::create_sum_from_row(const T& row,
 
 
 }
-template void nla::common::create_sum_from_row<old_vector<lp::row_cell<rational>, true, unsigned int> >(old_vector<lp::row_cell<rational>, true, unsigned int> const&, nla::nex_creator&, nla::nex_creator::sum_factory&, u_dependency*&);  
+template void nla::common::create_sum_from_row<vector<lp::row_cell<rational>, true, unsigned int> >(vector<lp::row_cell<rational>, true, unsigned int> const&, nla::nex_creator&, nla::nex_creator::sum_factory&, u_dependency*&);  

src/smt/theory_seq.cpp

@@ -1640,6 +1640,7 @@ bool theory_seq::enforce_length(expr_ref_vector const& es, vector<rational> & le
             len.push_back(rational(s.length()));
         }
         else if (get_length(e, val)) {
+			SASSERT(!val.is_neg());
             len.push_back(val);
         }
         else {
@@ -3916,6 +3917,8 @@ void theory_seq::add_itos_axiom(expr* e) {
     // itos(n) = "" or n >= 0
     add_axiom(~eq1, ~ge0);
     add_axiom(eq1, ge0);
+
+    add_axiom(mk_literal(m_autil.mk_ge(mk_len(e), m_autil.mk_int(0))));    
 
     // n >= 0 => stoi(itos(n)) = n
     app_ref stoi(m_util.str.mk_stoi(e), m);
@@ -5240,8 +5243,8 @@ void theory_seq::add_itos_length_axiom(expr* len) {
         num_char2 = len2.get_unsigned();
     }
     unsigned num_char = std::max(num_char1, num_char2);
-
 
+    add_axiom(mk_literal(m_autil.mk_ge(len, m_autil.mk_int(0))));    
     literal len_le(mk_literal(m_autil.mk_le(len, m_autil.mk_int(num_char))));
     literal len_ge(mk_literal(m_autil.mk_ge(len, m_autil.mk_int(num_char))));
     literal n_ge_0(mk_literal(m_autil.mk_ge(n, m_autil.mk_int(0))));
@@ -5519,7 +5522,7 @@ bool theory_seq::get_length(expr* e, rational& val) {
         }
         else {            
             len = mk_len(c);
-            if (m_arith_value.get_value(len, val1)) {
+            if (m_arith_value.get_value(len, val1) && !val1.is_neg()) {
                 val += val1;
             }
             else {

src/util/buffer.h

@@ -1,30 +1,274 @@
+
 /*++
-Copyright (c) 2019 Microsoft Corporation
+Copyright (c) 2006 Microsoft Corporation
 
 Module Name:
 
     buffer.h
 
+Abstract:
+
+    <abstract>
+
 Author:
 
-    Daniel Schemmel 2019-2-23
+    Leonardo de Moura (leonardo) 2006-10-16.
 
---*/
+Revision History:
 
+
+--*/
 #ifndef BUFFER_H_
 #define BUFFER_H_
 
-#include "old_buffer.h"
+#include<string.h>
+#include "util/memory_manager.h"
 
 template<typename T, bool CallDestructors=true, unsigned INITIAL_SIZE=16>
-using buffer = old_buffer<T, CallDestructors, INITIAL_SIZE>;
+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);
+        }
+    }
+
+    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]; 
+    }
 
-// note that the append added in the old_ptr_buffer is actually not an addition over its base class old_buffer,
+    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 is actually not an addition over its base class 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>;
+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>
-using sbuffer = old_sbuffer<T, INITIAL_SIZE>;
+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) {}
+};
+
+
 
 #endif /* BUFFER_H_ */