add TPTP example

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

examples/tptp/README

@@ -0,0 +1,18 @@
+TPTP front-end and utilities as a sample using the C++ bindings.
+To build the example execute
+   make examples
+in the build directory.
+
+This command will create the executable tptp.
+On Windows, you can just execute it.
+On OSX and Linux, you must install z3 first using 
+   sudo make install
+OR update LD_LIBRARY_PATH (Linux) or DYLD_LIBRARY_PATH (OSX) 
+   with the build directory. You need that to be able to 
+   find the Z3 shared library.
+
+The sample illustrates using Z3 from the TPTP language.
+The TPTP language is documented on http://tptp.org
+It also exposes utilities for converting between SMT-LIB 
+and TPTP format.
+

examples/tptp/tptp5.h

@@ -0,0 +1,38 @@
+#ifndef TPTP5_H_
+#define TPTP5_H_
+
+
+class TreeNode;
+
+#if 0
+class named_formulas {
+    expr_ref_vector m_fmls;
+    svector<symbol> m_names;
+    bool m_has_conjecture;
+    unsigned m_conjecture_index;
+public:
+    named_formulas(ast_manager& m) : 
+        m_fmls(m), 
+        m_has_conjecture(false),
+        m_conjecture_index(0)
+        {}
+    void push_back(expr* fml, char const* name) {
+        m_fmls.push_back(fml);
+        m_names.push_back(symbol(name));
+    }
+    unsigned size() const { return m_fmls.size(); }
+    expr*const* c_ptr() const { return m_fmls.c_ptr(); }
+    expr* operator[](unsigned i) { return m_fmls[i].get(); }
+    symbol const& name(unsigned i) { return m_names[i]; }
+    void set_has_conjecture() { 
+        m_has_conjecture = true;
+        m_conjecture_index = m_fmls.size();
+    }
+    bool has_conjecture() const { return m_has_conjecture; }
+    unsigned conjecture_index() const { return m_conjecture_index; }
+};
+
+bool tptp5_parse(ast_manager& m, char const* filename, named_formulas& fmls);
+#endif
+
+#endif

examples/tptp/tptp5.tab.h

@@ -0,0 +1,138 @@
+/* A Bison parser, made by GNU Bison 2.4.2.  */
+
+/* Skeleton interface for Bison's Yacc-like parsers in C
+   
+      Copyright (C) 1984, 1989-1990, 2000-2006, 2009-2010 Free Software
+   Foundation, Inc.
+   
+   This program is free software: you can redistribute it and/or modify
+   it under the terms of the GNU General Public License as published by
+   the Free Software Foundation, either version 3 of the License, or
+   (at your option) any later version.
+   
+   This program is distributed in the hope that it will be useful,
+   but WITHOUT ANY WARRANTY; without even the implied warranty of
+   MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+   GNU General Public License for more details.
+   
+   You should have received a copy of the GNU General Public License
+   along with this program.  If not, see <http://www.gnu.org/licenses/>.  */
+
+/* As a special exception, you may create a larger work that contains
+   part or all of the Bison parser skeleton and distribute that work
+   under terms of your choice, so long as that work isn't itself a
+   parser generator using the skeleton or a modified version thereof
+   as a parser skeleton.  Alternatively, if you modify or redistribute
+   the parser skeleton itself, you may (at your option) remove this
+   special exception, which will cause the skeleton and the resulting
+   Bison output files to be licensed under the GNU General Public
+   License without this special exception.
+   
+   This special exception was added by the Free Software Foundation in
+   version 2.2 of Bison.  */
+
+
+/* Tokens.  */
+#ifndef YYTOKENTYPE
+# define YYTOKENTYPE
+   /* Put the tokens into the symbol table, so that GDB and other debuggers
+      know about them.  */
+   enum yytokentype {
+     AMPERSAND = 258,
+     AT_SIGN = 259,
+     AT_SIGN_MINUS = 260,
+     AT_SIGN_PLUS = 261,
+     CARET = 262,
+     COLON = 263,
+     COLON_EQUALS = 264,
+     COMMA = 265,
+     EQUALS = 266,
+     EQUALS_GREATER = 267,
+     EXCLAMATION = 268,
+     EXCLAMATION_EQUALS = 269,
+     EXCLAMATION_EXCLAMATION = 270,
+     EXCLAMATION_GREATER = 271,
+     LBRKT = 272,
+     LESS_EQUALS = 273,
+     LESS_EQUALS_GREATER = 274,
+     LESS_TILDE_GREATER = 275,
+     LPAREN = 276,
+     MINUS = 277,
+     MINUS_MINUS_GREATER = 278,
+     PERIOD = 279,
+     QUESTION = 280,
+     QUESTION_QUESTION = 281,
+     QUESTION_STAR = 282,
+     RBRKT = 283,
+     RPAREN = 284,
+     STAR = 285,
+     TILDE = 286,
+     TILDE_AMPERSAND = 287,
+     TILDE_VLINE = 288,
+     VLINE = 289,
+     _DLR_cnf = 290,
+     _DLR_fof = 291,
+     _DLR_fot = 292,
+     _DLR_itef = 293,
+     _DLR_itetf = 294,
+     _DLR_itett = 295,
+     _DLR_tff = 296,
+     _DLR_thf = 297,
+     _LIT_cnf = 298,
+     _LIT_fof = 299,
+     _LIT_include = 300,
+     _LIT_tff = 301,
+     _LIT_thf = 302,
+     arrow = 303,
+     comment = 304,
+     comment_line = 305,
+     decimal = 306,
+     decimal_exponent = 307,
+     decimal_fraction = 308,
+     distinct_object = 309,
+     dollar_dollar_word = 310,
+     dollar_word = 311,
+     dot_decimal = 312,
+     integer = 313,
+     less_sign = 314,
+     lower_word = 315,
+     plus = 316,
+     positive_decimal = 317,
+     rational = 318,
+     real = 319,
+     signed_integer = 320,
+     signed_rational = 321,
+     signed_real = 322,
+     single_quoted = 323,
+     star = 324,
+     unrecognized = 325,
+     unsigned_integer = 326,
+     unsigned_rational = 327,
+     unsigned_real = 328,
+     upper_word = 329,
+     vline = 330
+   };
+#endif
+
+
+
+#if ! defined YYSTYPE && ! defined YYSTYPE_IS_DECLARED
+typedef union YYSTYPE
+{
+
+/* Line 1685 of yacc.c  */
+#line 148 "tptp5.y"
+int ival; double dval; char* sval; TreeNode* pval;
+
+
+/* Line 1685 of yacc.c  */
+#line 130 "tptp5.tab.h"
+} YYSTYPE;
+# define YYSTYPE_IS_TRIVIAL 1
+# define yystype YYSTYPE /* obsolescent; will be withdrawn */
+# define YYSTYPE_IS_DECLARED 1
+#endif
+
+extern YYSTYPE yylval;
+
+

scripts/mk_project.py

@@ -83,6 +83,7 @@ def init_project_def():
     set_z3py_dir('api/python')
     # Examples
     add_cpp_example('cpp_example', 'c++') 
+    add_cpp_example('z3_tptp', 'tptp') 
     add_c_example('c_example', 'c')
     add_c_example('maxsat')
     add_dotnet_example('dotnet_example', 'dotnet')

scripts/mk_util.py

@@ -931,6 +931,9 @@ class ExtraExeComponent(ExeComponent):
     def main_component(self):
         return False
 
+    def require_mem_initializer(self):
+        return False
+
 def get_so_ext():
     sysname = os.uname()[0]
     if sysname == 'Darwin':
@@ -1227,7 +1230,7 @@ class CppExampleComponent(ExampleComponent):
             out.write(' ')
             out.write(os.path.join(self.to_ex_dir, cppfile))
         out.write('\n')
-        out.write('\t%s $(LINK_OUT_FLAG)%s $(LINK_FLAGS)' % (self.compiler(), exefile))
+        out.write('\t%s $(OS_DEFINES) $(LINK_OUT_FLAG)%s $(LINK_FLAGS)' % (self.compiler(), exefile))
         # Add include dir components
         out.write(' -I%s' % get_component(API_COMPONENT).to_src_dir)
         out.write(' -I%s' % get_component(CPP_COMPONENT).to_src_dir)
@@ -1399,7 +1402,8 @@ def mk_config():
             'LINK_OUT_FLAG=/Fe\n'
             'SO_EXT=.dll\n'
             'SLINK=cl\n'
-            'SLINK_OUT_FLAG=/Fe\n')
+            'SLINK_OUT_FLAG=/Fe\n'
+	    'OS_DEFINES=/D _WINDOWS\n')
         extra_opt = ''
         if GIT_HASH:
             extra_opt = '%s /D Z3GITHASH=%s' % (extra_opt, GIT_HASH)
@@ -1447,6 +1451,7 @@ def mk_config():
                 print('Java Compiler:  %s' % JAVAC)
     else:
         global CXX, CC, GMP, CPPFLAGS, CXXFLAGS, LDFLAGS
+	OS_DEFINES = ""
         ARITH = "internal"
         check_ar()
         CXX = find_cxx_compiler()
@@ -1488,18 +1493,21 @@ def mk_config():
             SLIBFLAGS = '-dynamiclib'
         elif sysname == 'Linux':
             CXXFLAGS       = '%s -fno-strict-aliasing -D_LINUX_' % CXXFLAGS
+	    OS_DEFINES     = '-D_LINUX'
             SO_EXT         = '.so'
             LDFLAGS        = '%s -lrt' % LDFLAGS
             SLIBFLAGS      = '-shared'
             SLIBEXTRAFLAGS = '%s -lrt' % SLIBEXTRAFLAGS
         elif sysname == 'FreeBSD':
             CXXFLAGS       = '%s -fno-strict-aliasing -D_FREEBSD_' % CXXFLAGS
+	    OS_DEFINES     = '-D_FREEBSD_'
             SO_EXT         = '.so'
             LDFLAGS        = '%s -lrt' % LDFLAGS
             SLIBFLAGS      = '-shared'
             SLIBEXTRAFLAGS = '%s -lrt' % SLIBEXTRAFLAGS
         elif sysname[:6] ==  'CYGWIN':
             CXXFLAGS    = '%s -D_CYGWIN -fno-strict-aliasing' % CXXFLAGS
+	    OS_DEFINES     = '-D_CYGWIN'
             SO_EXT      = '.dll'
             SLIBFLAGS   = '-shared'
         else:
@@ -1534,6 +1542,7 @@ def mk_config():
         config.write('SLINK_FLAGS=%s\n' % SLIBFLAGS)
         config.write('SLINK_EXTRA_FLAGS=%s\n' % SLIBEXTRAFLAGS)
         config.write('SLINK_OUT_FLAG=-o \n')
+	config.write('OS_DEFINES=%s\n' % OS_DEFINES)
         if is_verbose():
             print('Host platform:  %s' % sysname)
             print('C++ Compiler:   %s' % CXX)

src/api/c++/z3++.h

@@ -204,6 +204,8 @@ namespace z3 {
         
         func_decl function(symbol const & name, unsigned arity, sort const * domain, sort const & range);
         func_decl function(char const * name, unsigned arity, sort const * domain, sort const & range);
+        func_decl function(symbol const&  name, sort_vector const& domain, sort const& range);
+        func_decl function(char const * name, sort_vector const& domain, sort const& range);
         func_decl function(char const * name, sort const & domain, sort const & range);
         func_decl function(char const * name, sort const & d1, sort const & d2, sort const & range);
         func_decl function(char const * name, sort const & d1, sort const & d2, sort const & d3, sort const & range);
@@ -429,6 +431,7 @@ namespace z3 {
 
         expr operator()() const;
         expr operator()(unsigned n, expr const * args) const;
+        expr operator()(expr_vector const& v) const;
         expr operator()(expr const & a) const;
         expr operator()(int a) const;
         expr operator()(expr const & a1, expr const & a2) const;
@@ -1516,6 +1519,22 @@ namespace z3 {
     inline func_decl context::function(char const * name, unsigned arity, sort const * domain, sort const & range) {
         return function(range.ctx().str_symbol(name), arity, domain, range);
     }
+
+    inline func_decl context::function(symbol const& name, sort_vector const& domain, sort const& range) {
+        array<Z3_sort> args(domain.size());
+        for (unsigned i = 0; i < domain.size(); i++) {
+            check_context(domain[i], range);
+            args[i] = domain[i];
+        }
+        Z3_func_decl f = Z3_mk_func_decl(m_ctx, name, domain.size(), args.ptr(), range);
+        check_error();
+        return func_decl(*this, f);
+    }
+    
+    inline func_decl context::function(char const * name, sort_vector const& domain, sort const& range) {
+        return function(range.ctx().str_symbol(name), domain, range);        
+    }
+
     
     inline func_decl context::function(char const * name, sort const & domain, sort const & range) {
         check_context(domain, range);
@@ -1602,6 +1621,16 @@ namespace z3 {
         return expr(ctx(), r);
     
     }
+    inline expr func_decl::operator()(expr_vector const& args) const {
+        array<Z3_ast> _args(args.size());
+        for (unsigned i = 0; i < args.size(); i++) {
+            check_context(*this, args[i]);
+            _args[i] = args[i];
+        }
+        Z3_ast r = Z3_mk_app(ctx(), *this, args.size(), _args.ptr());
+        check_error();
+        return expr(ctx(), r);    
+    }
     inline expr func_decl::operator()() const {
         Z3_ast r = Z3_mk_app(ctx(), *this, 0, 0);
         ctx().check_error();

src/muz/base/dl_util.h

@@ -719,7 +719,7 @@ namespace datalog {
         T& operator*() { return *m_t; }
         const T& operator*() const { return *m_t; }
         operator bool() const { return m_t!=0; }
-        T* get() { return m_t; }
+        T* get() const { return m_t; }
         /**
            \brief Remove object from \c scoped_rel without deleting it.
         */

src/muz/rel/dl_sparse_table.cpp

@@ -81,9 +81,9 @@ namespace datalog {
     }
 
     unsigned entry_storage::get_size_estimate_bytes() const {
-        unsigned sz = m_data.capacity();
+        size_t sz = m_data.capacity();
         sz += m_data_indexer.capacity()*sizeof(storage_indexer::entry);
-        return sz;
+        return static_cast<unsigned>(sz);
     }
 
     // -----------------------------------
@@ -283,7 +283,7 @@ namespace datalog {
 
     class sparse_table::general_key_indexer : public key_indexer {
         typedef svector<store_offset> offset_vector;
-        typedef u_map<offset_vector> index_map;
+        typedef size_t_map<offset_vector> index_map;
 
         index_map m_map;
         mutable entry_storage m_keys;
@@ -641,8 +641,8 @@ namespace datalog {
         unsigned t1_entry_size = t1.m_fact_size;
         unsigned t2_entry_size = t2.m_fact_size;
 
-        unsigned t1idx = 0;
+        size_t t1idx = 0;
-        unsigned t1end = t1.m_data.after_last_offset();
+        size_t t1end = t1.m_data.after_last_offset();
 
         TRACE("dl_table_relation", 
               tout << "joined_col_cnt: " << joined_col_cnt << "\n";
@@ -654,8 +654,8 @@ namespace datalog {
               );
 
         if (joined_col_cnt == 0) {
-            unsigned t2idx = 0;
+            size_t t2idx = 0;
-            unsigned t2end = t2.m_data.after_last_offset();
+            size_t t2end = t2.m_data.after_last_offset();
 
             for (; t1idx!=t1end; t1idx+=t1_entry_size) {
                 for (t2idx = 0; t2idx != t2end; t2idx += t2_entry_size) {
@@ -1064,8 +1064,8 @@ namespace datalog {
             sparse_table_plugin & plugin = t.get_plugin();
             sparse_table * res = static_cast<sparse_table *>(plugin.mk_empty(get_result_signature()));
 
-            unsigned res_fact_size = res->m_fact_size;
+            size_t res_fact_size = res->m_fact_size;
-            unsigned res_data_size = res_fact_size*t.row_count();
+            size_t res_data_size = res_fact_size*t.row_count();
             if (res_fact_size != 0 && (res_data_size / res_fact_size) != t.row_count()) {
                 throw default_exception("multiplication overflow");
             }
@@ -1084,7 +1084,7 @@ namespace datalog {
             }
 
             //and insert them into the hash-map
-            for (unsigned i=0; i!=res_data_size; i+=res_fact_size) {
+            for (size_t i = 0; i != res_data_size; i += res_fact_size) {
                 TRUSTME(res->m_data.insert_offset(i));
             }
 
@@ -1161,7 +1161,7 @@ namespace datalog {
                 }
                 if (key_modified) {
                     t2_offsets = t2_indexer.get_matching_offsets(t1_key);
-                    key_modified=false;
+                    key_modified = false;
                 }
 
                 if (t2_offsets.empty()) {
@@ -1171,12 +1171,16 @@ namespace datalog {
                     res.push_back(t1_ofs);
                 }
                 else {
-                    key_indexer::offset_iterator it = t2_offsets.begin();
+                    key_indexer::offset_iterator it  = t2_offsets.begin();
                     key_indexer::offset_iterator end = t2_offsets.end();
                     for (; it!=end; ++it) {
                         store_offset ofs = *it;
-                        if (!m_intersection_content.contains(ofs)) {
+                        unsigned offs2 = static_cast<unsigned>(ofs);
-                            m_intersection_content.insert(ofs);
+                        if (ofs != offs2) {
+                            throw default_exception("Z3 cannot perform negation with excessively large tables");
+                        }
+                        if (!m_intersection_content.contains(offs2)) {
+                            m_intersection_content.insert(offs2);
                             res.push_back(ofs);
                         }
                     }

src/muz/rel/dl_sparse_table.h

@@ -97,9 +97,9 @@ namespace datalog {
 
     class entry_storage {
     public:
-        typedef unsigned store_offset;
+        typedef size_t store_offset;
     private:
-        typedef svector<char> storage;
+        typedef svector<char, size_t> storage;
 
         class offset_hash_proc {
             storage & m_storage;
@@ -130,7 +130,7 @@ namespace datalog {
 
         unsigned m_entry_size;
         unsigned m_unique_part_size;
-        unsigned m_data_size;
+        size_t m_data_size;
         /**
            Invariant: Every or all but one blocks of length \c m_entry_size in the \c m_data vector
            are unique sequences of bytes and have their offset stored in the \c m_data_indexer hashtable. 
@@ -214,7 +214,7 @@ namespace datalog {
                 SASSERT(m_reserve==m_data_size-m_entry_size);
                 return;
             }
-            m_reserve=m_data_size;
+            m_reserve = m_data_size;
             resize_data(m_data_size+m_entry_size);
         }
 
@@ -273,7 +273,7 @@ namespace datalog {
 
 
         //the following two operations allow breaking of the object invariant!
-        void resize_data(unsigned sz) {
+        void resize_data(size_t sz) {
             m_data_size = sz;
             if (sz + sizeof(uint64) < sz) {
                 throw default_exception("overflow resizing data section for sparse table");

src/util/vector.h

@@ -37,7 +37,7 @@ Revision History:
 #pragma warning(disable:4127)
 #endif
 
-template<typename T, bool CallDestructors=true>
+template<typename T, bool CallDestructors=true, typename SZ = unsigned>
 class vector {
 #define SIZE_IDX     -1
 #define CAPACITY_IDX -2
@@ -52,13 +52,13 @@ class vector {
     }
 
     void free_memory() { 
-        memory::deallocate(reinterpret_cast<char*>(reinterpret_cast<unsigned*>(m_data) - 2));
+        memory::deallocate(reinterpret_cast<char*>(reinterpret_cast<SZ*>(m_data) - 2));
     }
 
     void expand_vector() {
         if (m_data == 0) {
-            unsigned capacity = 2;
+            SZ capacity = 2;
-            unsigned * mem    = reinterpret_cast<unsigned*>(memory::allocate(sizeof(T) * capacity + sizeof(unsigned) * 2));
+            SZ * mem    = reinterpret_cast<SZ*>(memory::allocate(sizeof(T) * capacity + sizeof(SZ) * 2));
             *mem              = capacity; 
             mem++;
             *mem              = 0;        
@@ -67,15 +67,15 @@ class vector {
         }
         else {
             SASSERT(capacity() > 0);
-            unsigned old_capacity = reinterpret_cast<unsigned *>(m_data)[CAPACITY_IDX];
+            SZ old_capacity = reinterpret_cast<SZ *>(m_data)[CAPACITY_IDX];
-            unsigned old_capacity_T = sizeof(T) * old_capacity + sizeof(unsigned) * 2;
+            SZ old_capacity_T = sizeof(T) * old_capacity + sizeof(SZ) * 2;
-            unsigned new_capacity = (3 * old_capacity + 1) >> 1;
+            SZ new_capacity = (3 * old_capacity + 1) >> 1;
-            unsigned new_capacity_T  = sizeof(T) * new_capacity + sizeof(unsigned) * 2;
+            SZ new_capacity_T = sizeof(T) * new_capacity + sizeof(SZ) * 2;
-            unsigned size         = reinterpret_cast<unsigned *>(m_data)[SIZE_IDX];
+            SZ size         = reinterpret_cast<SZ *>(m_data)[SIZE_IDX];
             if (new_capacity <= old_capacity || new_capacity_T <= old_capacity_T) {
                 throw default_exception("Overflow encountered when expanding vector");
             }
-            unsigned * mem        = reinterpret_cast<unsigned*>(memory::allocate(new_capacity_T));
+            SZ * mem        = reinterpret_cast<SZ*>(memory::allocate(new_capacity_T));
             *mem                  = new_capacity; 
             mem ++;
             *mem                  = size;         
@@ -87,9 +87,9 @@ class vector {
     }
 
     void copy_core(vector const & source) {
-        unsigned size      = source.size();
+        SZ size      = source.size();
-        unsigned capacity  = source.capacity();
+        SZ capacity  = source.capacity();
-        unsigned * mem     = reinterpret_cast<unsigned*>(memory::allocate(sizeof(T) * capacity + sizeof(unsigned) * 2));
+        SZ * mem     = reinterpret_cast<SZ*>(memory::allocate(sizeof(T) * capacity + sizeof(SZ) * 2));
         *mem = capacity; 
         mem++;
         *mem = size; 
@@ -122,8 +122,8 @@ public:
         m_data(0) {
     }
 
-    vector(unsigned s) {
+    vector(SZ s) {
-        unsigned * mem = reinterpret_cast<unsigned*>(memory::allocate(sizeof(T) * s + sizeof(unsigned) * 2));
+        SZ * mem = reinterpret_cast<SZ*>(memory::allocate(sizeof(T) * s + sizeof(SZ) * 2));
         *mem = s; 
         mem++;
         *mem = s; 
@@ -137,7 +137,7 @@ public:
         }
     }
 
-    vector(unsigned s, T const & elem):
+    vector(SZ s, T const & elem):
         m_data(0) {
         resize(s, elem);
     }
@@ -150,9 +150,9 @@ public:
         SASSERT(size() == source.size());
     }
 
-    vector(unsigned s, T const * data):
+    vector(SZ s, T const * data):
         m_data(0) {
-        for (unsigned i = 0; i < s; i++) {
+        for (SZ i = 0; i < s; i++) {
             push_back(data[i]);
         }
     }
@@ -186,26 +186,26 @@ public:
             if (CallDestructors) {
                 destroy_elements();
             }
-            reinterpret_cast<unsigned *>(m_data)[SIZE_IDX] = 0;
+            reinterpret_cast<SZ *>(m_data)[SIZE_IDX] = 0;
         }
     }
 
     bool empty() const { 
-        return m_data == 0 || reinterpret_cast<unsigned *>(m_data)[SIZE_IDX] == 0; 
+        return m_data == 0 || reinterpret_cast<SZ *>(m_data)[SIZE_IDX] == 0; 
     }
 
-    unsigned size() const { 
+    SZ size() const { 
         if (m_data == 0) {
             return 0;  
         }
-        return reinterpret_cast<unsigned *>(m_data)[SIZE_IDX]; 
+        return reinterpret_cast<SZ *>(m_data)[SIZE_IDX]; 
     }
 
-    unsigned capacity() const { 
+    SZ capacity() const { 
         if (m_data == 0) {
             return 0;
         }
-        return reinterpret_cast<unsigned *>(m_data)[CAPACITY_IDX]; 
+        return reinterpret_cast<SZ *>(m_data)[CAPACITY_IDX]; 
     }
 
     iterator begin() { 
@@ -226,41 +226,41 @@ public:
 
     void set_end(iterator it) {
         if (m_data) {
-            unsigned new_sz = static_cast<unsigned>(it - m_data);
+            SZ new_sz = static_cast<SZ>(it - m_data);
             if (CallDestructors) {
                 iterator e = end();
                 for(; it != e; ++it) {
                     it->~T();
                 }
             }
-            reinterpret_cast<unsigned *>(m_data)[SIZE_IDX] = new_sz;
+            reinterpret_cast<SZ *>(m_data)[SIZE_IDX] = new_sz;
         }
         else {
             SASSERT(it == 0);
         }
     }
 
-    T & operator[](unsigned idx) { 
+    T & operator[](SZ idx) { 
         SASSERT(idx < size()); 
         return m_data[idx]; 
     }
 
-    T const & operator[](unsigned idx) const { 
+    T const & operator[](SZ idx) const { 
         SASSERT(idx < size()); 
         return m_data[idx];
     }
 
-    T & get(unsigned idx) { 
+    T & get(SZ idx) { 
         SASSERT(idx < size()); 
         return m_data[idx]; 
     }
 
-    T const & get(unsigned idx) const { 
+    T const & get(SZ idx) const { 
         SASSERT(idx < size()); 
         return m_data[idx];
     }
 
-    void set(unsigned idx, T const & val) { 
+    void set(SZ idx, T const & val) { 
         SASSERT(idx < size()); 
         m_data[idx] = val;
     }
@@ -280,15 +280,15 @@ public:
         if (CallDestructors) {
             back().~T(); 
         }
-        reinterpret_cast<unsigned *>(m_data)[SIZE_IDX]--; 
+        reinterpret_cast<SZ *>(m_data)[SIZE_IDX]--; 
     }
 
     void push_back(T const & elem) {
-        if (m_data == 0 || reinterpret_cast<unsigned *>(m_data)[SIZE_IDX] == reinterpret_cast<unsigned *>(m_data)[CAPACITY_IDX]) {
+        if (m_data == 0 || reinterpret_cast<SZ *>(m_data)[SIZE_IDX] == reinterpret_cast<SZ *>(m_data)[CAPACITY_IDX]) {
             expand_vector();
         }
-        new (m_data + reinterpret_cast<unsigned *>(m_data)[SIZE_IDX]) T(elem); 
+        new (m_data + reinterpret_cast<SZ *>(m_data)[SIZE_IDX]) T(elem); 
-        reinterpret_cast<unsigned *>(m_data)[SIZE_IDX]++;
+        reinterpret_cast<SZ *>(m_data)[SIZE_IDX]++;
     }
 
     void insert(T const & elem) {
@@ -303,7 +303,7 @@ public:
         for(; pos != e; ++pos, ++prev) {
             *prev = *pos;
         }
-        reinterpret_cast<unsigned *>(m_data)[SIZE_IDX]--;
+        reinterpret_cast<SZ *>(m_data)[SIZE_IDX]--;
     }
 
     void erase(T const & elem) {
@@ -313,9 +313,9 @@ public:
         }
     }
 
-    void shrink(unsigned s) {
+    void shrink(SZ s) {
         if (m_data) {
-            SASSERT(s <= reinterpret_cast<unsigned *>(m_data)[SIZE_IDX]);
+            SASSERT(s <= reinterpret_cast<SZ *>(m_data)[SIZE_IDX]);
             if (CallDestructors) {
                 iterator it = m_data + s;
                 iterator e  = end();
@@ -323,21 +323,21 @@ public:
                     it->~T();
                 }
             }
-            reinterpret_cast<unsigned *>(m_data)[SIZE_IDX] = s;
+            reinterpret_cast<SZ *>(m_data)[SIZE_IDX] = s;
         }
         else {
             SASSERT(s == 0);
         }
     }
 
-    void resize(unsigned s, T const & elem=T()) {
+    void resize(SZ s, T const & elem=T()) {
-        unsigned sz = size();
+        SZ sz = size();
         if (s <= sz) { shrink(s); return; }
         while (s > capacity()) {
             expand_vector();
         }
         SASSERT(m_data != 0);
-        reinterpret_cast<unsigned *>(m_data)[SIZE_IDX] = s;
+        reinterpret_cast<SZ *>(m_data)[SIZE_IDX] = s;
         iterator it  = m_data + sz;
         iterator end = m_data + s;
         for(; it != end; ++it) {
@@ -346,13 +346,13 @@ public:
     }
 
     void append(vector<T, CallDestructors> const & other) {
-        for(unsigned i = 0; i < other.size(); ++i) {
+        for(SZ i = 0; i < other.size(); ++i) {
             push_back(other[i]);
         }
     }
 
-    void append(unsigned sz, T const * data) {
+    void append(SZ sz, T const * data) {
-        for(unsigned i = 0; i < sz; ++i) {
+        for(SZ i = 0; i < sz; ++i) {
             push_back(data[i]);
         }
     }
@@ -366,8 +366,8 @@ public:
     }
 
     void reverse() {
-        unsigned sz = size();
+        SZ sz = size();
-        for (unsigned i = 0; i < sz/2; ++i) {
+        for (SZ i = 0; i < sz/2; ++i) {
            std::swap(m_data[i], m_data[sz-i-1]);
        }
     }
@@ -392,7 +392,7 @@ public:
     }
 
     // set pos idx with elem. If idx >= size, then expand using default.
-    void setx(unsigned idx, T const & elem, T const & d) {
+    void setx(SZ idx, T const & elem, T const & d) {
         if (idx >= size()) {
             resize(idx+1, d);
         }
@@ -400,14 +400,14 @@ public:
     }
 
     // return element at position idx, if idx >= size, then return default
-    T const & get(unsigned idx, T const & d) const {
+    T const & get(SZ idx, T const & d) const {
         if (idx >= size()) {
             return d;
         }
         return m_data[idx];
     }
 
-    void reserve(unsigned s, T const & d = T()) {
+    void reserve(SZ s, T const & d = T()) {
         if (s > size())
             resize(s, d);
     }
@@ -423,14 +423,14 @@ public:
     ptr_vector(unsigned s, T * const * data):vector<T *, false>(s, const_cast<T**>(data)) {}
 };
 
-template<typename T>
+template<typename T, typename SZ = unsigned>
-class svector : public vector<T, false> {
+class svector : public vector<T, false, SZ> {
 public:
-    svector():vector<T, false>() {}
+    svector():vector<T, false, SZ>() {}
-    svector(unsigned s):vector<T, false>(s) {}
+    svector(SZ s):vector<T, false, SZ>(s) {}
-    svector(unsigned s, T const & elem):vector<T, false>(s, elem) {}
+    svector(SZ s, T const & elem):vector<T, false, SZ>(s, elem) {}
-    svector(svector const & source):vector<T, false>(source) {}
+    svector(svector const & source):vector<T, false, SZ>(source) {}
-    svector(unsigned s, T const * data):vector<T, false>(s, data) {}
+    svector(SZ s, T const * data):vector<T, false, SZ>(s, data) {}
 };
 
 typedef svector<int> int_vector;