Reorganizing code. Added script for generating VS project files

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

src/util/cmd_context_types.cpp

@@ -0,0 +1,44 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    cmd_context_types.h
+
+Abstract:
+
+Author:
+
+    Leonardo (leonardo) 2011-04-22
+
+Notes:
+
+--*/
+#include<iostream>
+#include"cmd_context_types.h"
+
+std::ostream & operator<<(std::ostream & out, cmd_arg_kind k) {
+    switch (k) {
+    case CPK_UINT: out << "unsigned int"; break;
+    case CPK_BOOL: out << "bool"; break;
+    case CPK_DOUBLE: out << "double"; break;
+    case CPK_NUMERAL: out << "rational"; break;
+    case CPK_DECIMAL: out << "rational"; break;
+    case CPK_STRING:  out << "string"; break;
+    case CPK_OPTION_VALUE: out << "optional-value"; break;
+    case CPK_KEYWORD: out << "keyword"; break;
+    case CPK_SYMBOL: out << "symbol"; break;
+    case CPK_SYMBOL_LIST: out << "symbol-list"; break;
+    case CPK_SORT: out << "sort"; break;
+    case CPK_SORT_LIST: out << "sort-list"; break;
+    case CPK_EXPR: out << "expression"; break;
+    case CPK_EXPR_LIST: out << "expression-list"; break;
+    case CPK_FUNC_DECL: out << "declaration"; break;
+    case CPK_FUNC_DECL_LIST: out << "declaration-list"; break;
+    case CPK_SORTED_VAR: out << "sorted-variable"; break;
+    case CPK_SORTED_VAR_LIST: out << "sorted-variable-list"; break;
+    case CPK_SEXPR: out << "s-expression"; break;
+    default: out << "unknown"; break;
+    }
+    return out;
+}

src/util/cmd_context_types.h

@@ -0,0 +1,119 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    cmd_context_types.h
+
+Abstract:
+
+Author:
+
+    Leonardo (leonardo) 2011-04-22
+
+Notes:
+
+--*/
+#ifndef _CMD_CONTEXT_TYPES_H_
+#define _CMD_CONTEXT_TYPES_H_
+
+#include"symbol.h"
+#include"z3_exception.h"
+#include<sstream>
+class rational;
+class expr;
+class sort;
+class func_decl;
+class sexpr;
+class cmd_context;
+
+enum cmd_arg_kind {
+    CPK_UINT, CPK_BOOL, CPK_DOUBLE, CPK_NUMERAL, 
+    CPK_DECIMAL, CPK_STRING, CPK_OPTION_VALUE, 
+    CPK_KEYWORD,
+    CPK_SYMBOL, CPK_SYMBOL_LIST,
+    CPK_SORT,   CPK_SORT_LIST,
+    CPK_EXPR,   CPK_EXPR_LIST,
+    CPK_FUNC_DECL, CPK_FUNC_DECL_LIST,
+    CPK_SORTED_VAR, CPK_SORTED_VAR_LIST,
+    CPK_SEXPR,
+    CPK_INVALID
+};
+
+std::ostream & operator<<(std::ostream & out, cmd_arg_kind k);
+
+typedef cmd_arg_kind param_kind;
+
+class cmd_exception : public default_exception { 
+    int         m_line;
+    int         m_pos;
+
+    std::string compose(char const* msg, symbol const& s) {
+        std::stringstream stm;        
+        stm << msg << s;
+        return stm.str();
+    }
+public:
+    cmd_exception(char const * msg):default_exception(msg), m_line(-1), m_pos(-1) {}
+    cmd_exception(std::string const & msg):default_exception(msg.c_str()), m_line(-1), m_pos(-1) {}
+    cmd_exception(std::string const & msg, int line, int pos):default_exception(msg.c_str()), m_line(line), m_pos(pos) {}
+    cmd_exception(char const * msg, symbol const & s): 
+        default_exception(compose(msg,s).c_str()),m_line(-1),m_pos(-1) {}
+    cmd_exception(char const * msg, symbol const & s, int line, int pos): 
+        default_exception(compose(msg,s).c_str()),m_line(line),m_pos(pos) {}
+
+    bool has_pos() const { return m_line >= 0; }
+    int line() const { SASSERT(has_pos()); return m_line; }
+    int pos() const { SASSERT(has_pos()); return m_pos; }
+};
+
+class stop_parser_exception {
+};
+
+typedef std::pair<symbol, sort*> sorted_var;
+
+// A command may have a variable number of arguments.
+#define VAR_ARITY UINT_MAX
+
+/**
+   \brief Command abstract class.
+
+   Commands may have variable number of argumets.
+*/
+class cmd {
+    symbol m_name;
+public:
+    cmd(char const * n):m_name(n) {}
+    virtual ~cmd() {}
+    virtual void reset(cmd_context & ctx) {}
+    virtual void finalize(cmd_context & ctx) {}
+    virtual symbol get_name() const { return m_name; }
+    virtual char const * get_usage() const { return 0; }
+    virtual char const * get_descr(cmd_context & ctx) const { return 0; }
+    virtual unsigned get_arity() const { return 0; }
+
+    // command invocation
+    virtual void prepare(cmd_context & ctx) {}
+    virtual cmd_arg_kind next_arg_kind(cmd_context & ctx) const { UNREACHABLE(); return CPK_UINT; }
+    virtual void set_next_arg(cmd_context & ctx, unsigned val) { UNREACHABLE(); }
+    virtual void set_next_arg(cmd_context & ctx, bool val) { UNREACHABLE(); }
+    virtual void set_next_arg(cmd_context & ctx, rational const & val) { UNREACHABLE(); }
+    virtual void set_next_arg(cmd_context & ctx, double val) { UNREACHABLE(); }
+    virtual void set_next_arg(cmd_context & ctx, char const * val) { UNREACHABLE(); }
+    virtual void set_next_arg(cmd_context & ctx, symbol const & s) { UNREACHABLE(); }
+    virtual void set_next_arg(cmd_context & ctx, unsigned num, symbol const * slist) { UNREACHABLE(); }
+    virtual void set_next_arg(cmd_context & ctx, sort * s) { UNREACHABLE(); }
+    virtual void set_next_arg(cmd_context & ctx, unsigned num, sort * const * slist) { UNREACHABLE(); }
+    virtual void set_next_arg(cmd_context & ctx, expr * t) { UNREACHABLE(); }
+    virtual void set_next_arg(cmd_context & ctx, unsigned num, expr * const * tlist) { UNREACHABLE(); }
+    virtual void set_next_arg(cmd_context & ctx, sorted_var const & sv) { UNREACHABLE(); }
+    virtual void set_next_arg(cmd_context & ctx, unsigned num, sorted_var const * svlist) { UNREACHABLE(); }
+    virtual void set_next_arg(cmd_context & ctx, func_decl * f) { UNREACHABLE(); }
+    virtual void set_next_arg(cmd_context & ctx, unsigned num, func_decl * const * flist) { UNREACHABLE(); }
+    virtual void set_next_arg(cmd_context & ctx, sexpr * n) { UNREACHABLE(); }
+    virtual void failure_cleanup(cmd_context & ctx) {}
+    virtual void execute(cmd_context & ctx) {}
+};
+
+
+#endif

src/util/cooperate.cpp

@@ -0,0 +1,87 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    cooperate.cpp
+
+Abstract:
+
+    Cooperation support
+
+Author:
+
+    Leonardo (leonardo) 2011-05-17
+
+Notes:
+
+--*/
+#include"z3_omp.h"
+#include"cooperate.h"
+#include"trace.h"
+#include"debug.h"
+
+struct cooperation_lock {
+    omp_nest_lock_t  m_lock;
+    char const *     m_task;
+    volatile int     m_owner_thread;
+    cooperation_lock() {
+        omp_set_nested(1);
+        omp_init_nest_lock(&m_lock);
+        m_task = 0;
+        m_owner_thread = -1;
+    }
+    ~cooperation_lock() {
+        omp_destroy_nest_lock(&m_lock);
+    }
+};
+
+cooperation_lock g_lock;
+
+bool cooperation_ctx::g_cooperate = false;
+
+void cooperation_ctx::checkpoint(char const * task) {
+    SASSERT(cooperation_ctx::enabled());
+
+    int  tid      = omp_get_thread_num();
+    if (g_lock.m_owner_thread == tid) {
+        g_lock.m_owner_thread = -1;
+        omp_unset_nest_lock(&(g_lock.m_lock));
+    }
+    // this critical section is used to force the owner thread to give a chance to
+    // another thread to get the lock
+    #pragma omp critical (z3_cooperate) 
+    {
+        omp_set_nest_lock(&(g_lock.m_lock));
+        TRACE("cooperate_detail", tout << task << ", tid: " << tid << "\n";);
+        CTRACE("cooperate", g_lock.m_task != task, tout << "moving to task: " << task << "\n";);
+        g_lock.m_owner_thread = tid;
+    }
+}
+
+cooperation_section::cooperation_section() {
+    SASSERT(!cooperation_ctx::enabled());
+    SASSERT(!omp_in_parallel());
+    cooperation_ctx::g_cooperate = true;
+}
+
+cooperation_section::~cooperation_section() {
+    SASSERT(cooperation_ctx::enabled());
+    cooperation_ctx::g_cooperate = false;
+}
+
+init_task::init_task(char const * task) {
+    SASSERT(cooperation_ctx::enabled());
+    SASSERT(omp_in_parallel());
+    cooperation_ctx::checkpoint(task);
+}
+
+init_task::~init_task() {
+    int  tid      = omp_get_thread_num();
+    if (g_lock.m_owner_thread == tid) {
+        g_lock.m_owner_thread = -1;
+        omp_unset_nest_lock(&(g_lock.m_lock));
+    }
+}
+
+

src/util/cooperate.h

@@ -0,0 +1,50 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    cooperate.h
+
+Abstract:
+
+    Cooperation support
+
+Author:
+
+    Leonardo (leonardo) 2011-05-17
+
+Notes:
+
+--*/
+#ifndef _COOPERATE_H_
+#define _COOPERATE_H_
+
+class cooperation_section;
+
+class cooperation_ctx {
+    friend class cooperation_section;
+    static bool g_cooperate;
+public:
+    static bool enabled() { return g_cooperate; }
+    static void checkpoint(char const * task);
+};
+
+inline void cooperate(char const * task) {
+    if (cooperation_ctx::enabled()) cooperation_ctx::checkpoint(task);
+}
+
+// must be declared before "#pragma parallel" to enable cooperation 
+class cooperation_section {
+public:
+    cooperation_section();
+    ~cooperation_section();
+};
+
+// must be first declaration inside "#pragma parallel for"
+class init_task {
+public:
+    init_task(char const * task);
+    ~init_task();
+};
+
+#endif

src/util/error_codes.h

@@ -0,0 +1,37 @@
+/*++
+Copyright (c) 2006 Microsoft Corporation
+
+Module Name:
+
+    error_codes.h
+
+Abstract:
+
+    Error codes produced by Z3.
+
+Author:
+
+    Leonardo de Moura (leonardo) 2007-09-04.
+
+Revision History:
+
+--*/
+#ifndef _ERROR_CODES_H_
+#define _ERROR_CODES_H_
+
+#define ERR_OK                  0
+#define ERR_MEMOUT              101
+#define ERR_TIMEOUT             102
+#define ERR_PARSER              103
+#define ERR_UNSOUNDNESS         104
+#define ERR_INCOMPLETENESS      105
+#define ERR_INI_FILE            106 
+#define ERR_NOT_IMPLEMENTED_YET 107 
+#define ERR_OPEN_FILE           108
+#define ERR_CMD_LINE            109
+#define ERR_INTERNAL_FATAL      110
+#define ERR_TYPE_CHECK          111
+#define ERR_UNKNOWN_RESULT      112
+
+#endif /* _ERROR_CODES_H_ */
+

src/util/mpq_inf.h

@@ -21,7 +21,6 @@ Revision History:
 
 #include"mpq.h"
 #include"hash.h"
-#include"params.h"
 
 typedef std::pair<mpq, mpq> mpq_inf;
 
@@ -32,12 +31,12 @@ class mpq_inf_manager {
 public:
     typedef mpq_inf numeral;
 
-    mpq_inf_manager(mpq_manager<SYNCH> & _m, params_ref const & p = params_ref()):m(_m) {
-        updt_params(p);
+    mpq_inf_manager(mpq_manager<SYNCH> & _m, double inf = 0.0001):m(_m) {
+        set_inf(inf);
     }
 
-    void updt_params(params_ref const & p) {
-        m_inf = p.get_double(":infinitesimal-as-double", 0.00001);
+    void set_inf(double inf) {
+        m_inf = inf;
     }
 
     enum inf_kind { NEG=-1, ZERO, POS };

src/util/params.cpp

@@ -0,0 +1,716 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    params.cpp
+
+Abstract:
+
+    Parameters
+
+Author:
+
+    Leonardo (leonardo) 2011-05-09
+
+Notes:
+
+--*/
+#include"params.h"
+#include"rational.h"
+#include"symbol.h"
+#include"dictionary.h"
+
+struct param_descrs::imp {
+    typedef std::pair<param_kind, char const *> info;
+    dictionary<info> m_info;
+    svector<symbol> m_names;
+
+    void insert(symbol const & name, param_kind k, char const * descr) {
+        SASSERT(!name.is_numerical());
+        info i;
+        if (m_info.find(name, i)) {
+            SASSERT(i.first == k);
+            return;
+        }
+        m_info.insert(name, info(k, descr));
+        m_names.push_back(name);
+    }
+
+    void erase(symbol const & name) {
+        m_info.erase(name);
+    }
+                                    
+    param_kind get_kind(symbol const & name) const {
+        info i;
+        if (m_info.find(name, i))
+            return i.first;
+        return CPK_INVALID;
+    }
+
+    unsigned size() const {
+        return m_names.size();
+    }
+    
+    symbol get_param_name(unsigned idx) const {
+        return m_names[idx];
+    }
+
+    struct lt {
+        bool operator()(symbol const & s1, symbol const & s2) const { return strcmp(s1.bare_str(), s2.bare_str()) < 0; }
+    };
+
+    void display(std::ostream & out, unsigned indent) const {
+        svector<symbol> names;
+        dictionary<info>::iterator it  = m_info.begin();
+        dictionary<info>::iterator end = m_info.end();
+        for (; it != end; ++it) {
+            names.push_back(it->m_key);
+        }
+        std::sort(names.begin(), names.end(), lt());
+        svector<symbol>::iterator it2  = names.begin();
+        svector<symbol>::iterator end2 = names.end();
+        for (; it2 != end2; ++it2) {
+            for (unsigned i = 0; i < indent; i++) out << " ";
+            out << *it2;
+            info d;
+            d.second = 0;
+            m_info.find(*it2, d);
+            SASSERT(d.second);
+            out << " (" << d.first << ") " << d.second << "\n";
+        }
+    }
+};
+
+param_descrs::param_descrs() {
+    m_imp = alloc(imp);
+}
+
+param_descrs::~param_descrs() {
+    dealloc(m_imp);
+}
+
+void param_descrs::insert(symbol const & name, param_kind k, char const * descr) {
+    m_imp->insert(name, k, descr);
+}
+
+void param_descrs::insert(char const * name, param_kind k, char const * descr) {
+    insert(symbol(name), k, descr);
+}
+
+void param_descrs::erase(symbol const & name) {
+    m_imp->erase(name);
+}
+
+void param_descrs::erase(char const * name) {
+    erase(symbol(name));
+}
+
+param_kind param_descrs::get_kind(symbol const & name) const {
+    return m_imp->get_kind(name);
+}
+
+param_kind param_descrs::get_kind(char const * name) const {
+    return get_kind(symbol(name));
+}
+
+unsigned param_descrs::size() const {
+    return m_imp->size();
+}
+
+symbol param_descrs::get_param_name(unsigned i) const {
+    return m_imp->get_param_name(i);
+}
+
+void param_descrs::display(std::ostream & out, unsigned indent) const {
+    return m_imp->display(out, indent);
+}
+
+void insert_max_memory(param_descrs & r) {
+    r.insert(":max-memory", CPK_UINT, "(default: infty) maximum amount of memory in megabytes.");
+}
+
+void insert_max_steps(param_descrs & r) {
+    r.insert(":max-steps", CPK_UINT, "(default: infty) maximum number of steps.");
+}
+
+void insert_produce_models(param_descrs & r) {
+    r.insert(":produce-models", CPK_BOOL, "(default: false) model generation.");
+}
+
+void insert_produce_proofs(param_descrs & r) {
+    r.insert(":produce-proofs", CPK_BOOL, "(default: false) proof generation.");
+}
+
+void insert_timeout(param_descrs & r) {
+    r.insert(":timeout", CPK_UINT, "(default: infty) timeout in milliseconds.");
+}
+
+class params {
+    friend class params_ref;
+    struct value {
+        param_kind m_kind;
+        union {
+            bool          m_bool_value;
+            unsigned      m_uint_value;
+            double        m_double_value;
+            char const *  m_str_value;
+            char const *  m_sym_value;
+            rational *    m_rat_value;
+        };
+    };
+    typedef std::pair<symbol, value> entry;
+    svector<entry> m_entries;
+    unsigned       m_ref_count;
+    
+    void del_value(entry & e);
+    void del_values();
+
+public:
+    params():m_ref_count(0) {}
+    ~params() {
+        reset();
+    }
+
+    void inc_ref() { m_ref_count++; }
+    void dec_ref() { SASSERT(m_ref_count > 0); m_ref_count--; if (m_ref_count == 0) dealloc(this); }
+
+    bool empty() const { return m_entries.empty(); }
+    bool contains(symbol const & k) const;
+    bool contains(char const * k) const;
+
+    void reset();
+    void reset(symbol const & k);
+    void reset(char const * k);
+
+    void validate(param_descrs const & p) const {
+        svector<params::entry>::const_iterator it  = m_entries.begin();  
+        svector<params::entry>::const_iterator end = m_entries.end();
+        for (; it != end; ++it) {                                
+            param_kind expected = p.get_kind(it->first);
+            if (expected == CPK_INVALID)
+                throw default_exception("unknown parameter '%s'", it->first.str().c_str());
+            if (it->second.m_kind != expected) 
+                throw default_exception("parameter kind mismatch '%s'", it->first.str().c_str());
+        }
+    }
+    
+    // getters
+    bool get_bool(symbol const & k, bool _default) const;
+    bool get_bool(char const * k, bool _default) const;
+    unsigned get_uint(symbol const & k, unsigned _default) const;
+    unsigned get_uint(char const * k, unsigned _default) const;
+    double get_double(symbol const & k, double _default) const;
+    double get_double(char const * k, double _default) const;
+    char const * get_str(symbol const & k, char const * _default) const;
+    char const * get_str(char const * k, char const * _default) const;
+    rational get_rat(symbol const & k, rational const & _default) const;
+    rational get_rat(char const * k, rational const & _default) const; 
+    symbol get_sym(symbol const & k, symbol const & _default) const;
+    symbol get_sym(char const * k, symbol const & _default) const;
+
+    // setters
+    void set_bool(symbol const & k, bool v);
+    void set_bool(char const * k, bool  v);
+    void set_uint(symbol const & k, unsigned v);
+    void set_uint(char const * k, unsigned v);
+    void set_double(symbol const & k, double v);
+    void set_double(char const * k, double v);
+    void set_str(symbol const & k, char const * v);
+    void set_str(char const * k, char const * v);
+    void set_rat(symbol const & k, rational const & v);
+    void set_rat(char const * k, rational const & v); 
+    void set_sym(symbol const & k, symbol const & v);
+    void set_sym(char const * k, symbol const & v);
+
+    void display(std::ostream & out) const {
+        out << "(params";
+        svector<params::entry>::const_iterator it  = m_entries.begin();  
+        svector<params::entry>::const_iterator end = m_entries.end();
+        for (; it != end; ++it) {                                
+            out << " " << it->first;
+            switch (it->second.m_kind) {
+            case CPK_BOOL:
+                out << " " << it->second.m_bool_value;
+                break;
+            case CPK_UINT:
+                out << " " <<it->second.m_uint_value;
+                break;
+            case CPK_DOUBLE:
+                out << " " << it->second.m_double_value;
+                break;
+            case CPK_NUMERAL:
+                out << " " << *(it->second.m_rat_value);
+                break;
+            case CPK_SYMBOL:
+                out << " " << symbol::mk_symbol_from_c_ptr(it->second.m_sym_value);
+                break;
+            case CPK_STRING:
+                out << " " << it->second.m_str_value;
+                break;
+            default:
+                UNREACHABLE();
+                break;
+            }
+        }
+        out << ")";
+    }
+};
+
+params_ref::~params_ref() {
+    if (m_params)
+        m_params->dec_ref();
+}
+
+params_ref::params_ref(params_ref const & p):
+    m_params(0) {
+    operator=(p);
+}
+
+void params_ref::display(std::ostream & out) const {
+    if (m_params)
+        m_params->display(out);
+    else
+        out << "(params)";
+}
+
+void params_ref::validate(param_descrs const & p) const {
+    if (m_params)
+        m_params->validate(p);
+}
+
+params_ref & params_ref::operator=(params_ref const & p) {
+    if (p.m_params)
+        p.m_params->inc_ref();
+    if (m_params)
+        m_params->dec_ref();
+    m_params = p.m_params;
+    return *this;
+}
+
+void params_ref::copy(params_ref const & src) {
+    if (m_params == 0)
+        operator=(src);
+    else {
+        init();
+        copy_core(src.m_params);
+    }
+}
+
+void params_ref::copy_core(params const * src) {
+    if (src == 0)
+        return;
+    svector<params::entry>::const_iterator it  = src->m_entries.begin();  
+    svector<params::entry>::const_iterator end = src->m_entries.end();    
+    for (; it != end; ++it) {                                
+        switch (it->second.m_kind) {
+        case CPK_BOOL:
+            m_params->set_bool(it->first, it->second.m_bool_value);
+            break;
+        case CPK_UINT:
+            m_params->set_uint(it->first, it->second.m_uint_value);
+            break;
+        case CPK_DOUBLE:
+            m_params->set_double(it->first, it->second.m_double_value);
+            break;
+        case CPK_NUMERAL:
+            m_params->set_rat(it->first, *(it->second.m_rat_value));
+            break;
+        case CPK_SYMBOL:
+            m_params->set_sym(it->first, symbol::mk_symbol_from_c_ptr(it->second.m_sym_value));
+            break;
+        case CPK_STRING:
+            m_params->set_str(it->first, it->second.m_str_value);
+            break;
+        default:
+            UNREACHABLE();
+            break;
+        }
+    }
+}
+
+void params_ref::init() {
+    if (!m_params) {
+        m_params = alloc(params);
+        m_params->inc_ref();
+    }
+    else if (m_params->m_ref_count > 1) {
+        params * old = m_params;
+        m_params = alloc(params);
+        m_params->inc_ref();
+        copy_core(old);
+        old->dec_ref();
+    }
+    
+    SASSERT(m_params->m_ref_count == 1);
+}
+
+bool params_ref::get_bool(symbol const & k, bool _default) const { return m_params ? m_params->get_bool(k, _default) : _default; }
+bool params_ref::get_bool(char const * k, bool _default) const { return m_params ? m_params->get_bool(k, _default) : _default; }
+unsigned params_ref::get_uint(symbol const & k, unsigned _default) const { return m_params ? m_params->get_uint(k, _default) : _default; }
+unsigned params_ref::get_uint(char const * k, unsigned _default) const { return m_params ? m_params->get_uint(k, _default) : _default; }
+double params_ref::get_double(symbol const & k, double _default) const { return m_params ? m_params->get_double(k, _default) : _default; }
+double params_ref::get_double(char const * k, double _default) const { return m_params ? m_params->get_double(k, _default) : _default; }
+char const * params_ref::get_str(symbol const & k, char const * _default) const { return m_params ? m_params->get_str(k, _default) : _default; }
+char const * params_ref::get_str(char const * k, char const * _default) const { return m_params ? m_params->get_str(k, _default) : _default; }
+
+rational params_ref::get_rat(symbol const & k, rational const & _default) const { 
+    return m_params ? m_params->get_rat(k, _default) : _default; 
+}
+
+rational params_ref::get_rat(char const * k, rational const & _default) const { 
+    return m_params ? m_params->get_rat(k, _default) : _default; 
+}
+
+symbol params_ref::get_sym(symbol const & k, symbol const & _default) const { 
+    return m_params ? m_params->get_sym(k, _default) : _default; 
+}
+
+symbol params_ref::get_sym(char const * k, symbol const & _default) const { 
+    return m_params ? m_params->get_sym(k, _default) : _default; 
+}
+
+bool params_ref::empty() const {
+    if (!m_params)
+        return true;
+    return m_params->empty();
+}
+
+bool params_ref::contains(symbol const & k) const {
+    if (!m_params)
+        return false;
+    return m_params->contains(k);
+}
+
+bool params_ref::contains(char const * k) const {
+    if (!m_params)
+        return false;
+    return m_params->contains(k);
+}
+
+void params_ref::reset() {
+    if (m_params)
+        m_params->reset();
+}
+
+void params_ref::reset(symbol const & k) {
+    if (m_params)
+        m_params->reset(k);
+}
+
+void params_ref::reset(char const * k) {
+    if (m_params)
+        m_params->reset(k);
+}
+
+void params_ref::set_bool(symbol const & k, bool v) {
+    init();
+    m_params->set_bool(k, v);
+}
+
+void params_ref::set_bool(char const * k, bool  v) {
+    init();
+    m_params->set_bool(k, v);
+}
+
+void params_ref::set_uint(symbol const & k, unsigned v) {
+    init();
+    m_params->set_uint(k, v);
+}
+
+void params_ref::set_uint(char const * k, unsigned v) {
+    init();
+    m_params->set_uint(k, v);
+}
+
+void params_ref::set_double(symbol const & k, double v) {
+    init();
+    m_params->set_double(k, v);
+}
+
+void params_ref::set_double(char const * k, double v) {
+    init();
+    m_params->set_double(k, v);
+}
+
+void params_ref::set_str(symbol const & k, char const * v) {
+    init();
+    m_params->set_str(k, v);
+}
+
+void params_ref::set_str(char const * k, char const * v) {
+    init();
+    m_params->set_str(k, v);
+}
+
+void params_ref::set_rat(symbol const & k, rational const & v) {
+    init();
+    m_params->set_rat(k, v);
+}
+
+void params_ref::set_rat(char const * k, rational const & v) {
+    init();
+    m_params->set_rat(k, v);
+}
+
+void params_ref::set_sym(symbol const & k, symbol const & v) {
+    init();
+    m_params->set_sym(k, v);
+}
+
+void params_ref::set_sym(char const * k, symbol const & v) {
+    init();
+    m_params->set_sym(k, v);
+}
+
+
+void params::del_value(entry & e) {
+    switch (e.second.m_kind) {
+    case CPK_NUMERAL:
+        if (e.second.m_kind == CPK_NUMERAL)
+            dealloc(e.second.m_rat_value);
+        break;
+    default:
+        return;
+    }
+}
+
+#define TRAVERSE_ENTRIES(CODE) {                        \
+    svector<entry>::iterator it  = m_entries.begin();   \
+    svector<entry>::iterator end = m_entries.end();     \
+    for (; it != end; ++it) {                           \
+        CODE                                            \
+    }                                                   \
+}
+
+#define TRAVERSE_CONST_ENTRIES(CODE) {                          \
+    svector<entry>::const_iterator it  = m_entries.begin();     \
+    svector<entry>::const_iterator end = m_entries.end();       \
+    for (; it != end; ++it) {                                   \
+        CODE                                                    \
+    }                                                           \
+}
+
+void params::del_values() {
+    TRAVERSE_ENTRIES(del_value(*it););
+}
+
+#define CONTAINS(k) {                                           \
+    if (empty())                                                \
+        return false;                                           \
+    TRAVERSE_CONST_ENTRIES(if (it->first == k) return true;);   \
+    return false;                                               \
+}
+
+bool params::contains(symbol const & k) const {
+    CONTAINS(k);
+}
+ 
+bool params::contains(char const * k) const {
+    CONTAINS(k);
+}
+
+void params::reset() {
+    del_values();
+    m_entries.finalize();
+    SASSERT(empty());
+}
+
+#define RESET(k) {                              \
+    if (empty()) return;                        \
+    TRAVERSE_ENTRIES(if (it->first == k) {      \
+        svector<entry>::iterator it2 = it;      \
+        del_value(*it2);                        \
+        ++it;                                   \
+        for (; it != end; ++it, ++it2) {        \
+            *it2 = *it;                         \
+        }                                       \
+        m_entries.pop_back();                   \
+        return;                                 \
+    });                                         \
+}
+
+void params::reset(symbol const & k) {
+    RESET(k);
+}
+
+void params::reset(char const * k) {
+    RESET(k);
+}
+
+#define GET_VALUE(MATCH_CODE, KIND) {                                           \
+    if (empty()) return _default;                                                \
+    TRAVERSE_CONST_ENTRIES(if (it->first == k && it->second.m_kind == KIND) {   \
+        MATCH_CODE                                                              \
+    });                                                                         \
+    return _default;                                                             \
+}
+    
+#define GET_SIMPLE_VALUE(FIELD_NAME, KIND) GET_VALUE(return it->second.FIELD_NAME;, KIND)
+
+bool params::get_bool(symbol const & k, bool _default) const {
+    GET_SIMPLE_VALUE(m_bool_value, CPK_BOOL);
+}
+
+bool params::get_bool(char const * k, bool _default) const {
+    GET_SIMPLE_VALUE(m_bool_value, CPK_BOOL);
+}
+
+unsigned params::get_uint(symbol const & k, unsigned _default) const {
+    GET_SIMPLE_VALUE(m_uint_value, CPK_UINT);
+}
+
+unsigned params::get_uint(char const * k, unsigned _default) const {
+    GET_SIMPLE_VALUE(m_uint_value, CPK_UINT);
+}
+
+double params::get_double(symbol const & k, double _default) const {
+    GET_SIMPLE_VALUE(m_double_value, CPK_DOUBLE);
+}
+
+double params::get_double(char const * k, double _default) const {
+    GET_SIMPLE_VALUE(m_double_value, CPK_DOUBLE);
+}
+
+char const * params::get_str(symbol const & k, char const * _default) const {
+    GET_SIMPLE_VALUE(m_str_value, CPK_STRING);
+}
+
+char const * params::get_str(char const * k, char const * _default) const {
+    GET_SIMPLE_VALUE(m_str_value, CPK_STRING);
+}
+
+rational params::get_rat(symbol const & k, rational const & _default) const {
+    if (empty()) return _default;                                               
+    TRAVERSE_CONST_ENTRIES(if (it->first == k) {
+            if (it->second.m_kind == CPK_NUMERAL) {   
+                return *(it->second.m_rat_value);
+            }
+            if (it->second.m_kind == CPK_UINT) {
+                return rational(static_cast<int>(it->second.m_uint_value));
+            }
+        });
+    return _default;                                                            
+}
+
+rational params::get_rat(char const * k, rational const & _default) const {
+    if (empty()) return _default;                                               
+    TRAVERSE_CONST_ENTRIES(if (it->first == k) {
+            if (it->second.m_kind == CPK_NUMERAL) {   
+                return *(it->second.m_rat_value);
+            }
+            if (it->second.m_kind == CPK_UINT) {
+                return rational(static_cast<int>(it->second.m_uint_value));
+            }
+        });
+    return _default;                                                            
+}
+
+symbol params::get_sym(symbol const & k, symbol const & _default) const {
+    GET_VALUE(return symbol::mk_symbol_from_c_ptr(it->second.m_sym_value);, CPK_SYMBOL);
+}
+
+symbol params::get_sym(char const * k, symbol const & _default) const {
+    GET_VALUE(return symbol::mk_symbol_from_c_ptr(it->second.m_sym_value);, CPK_SYMBOL);
+}
+
+#define SET_VALUE(MATCH_CODE, ADD_CODE) {       \
+    TRAVERSE_ENTRIES(if (it->first == k) {      \
+        MATCH_CODE                              \
+        return;                                 \
+    });                                         \
+    ADD_CODE                                    \
+}
+
+#define SET_SIMPLE_VALUE(FIELD_NAME, KIND) SET_VALUE({  \
+    del_value(*it);                                     \
+    it->second.m_kind = KIND;                           \
+    it->second.FIELD_NAME = v;                          \
+},                                                      \
+{                                                       \
+    entry new_entry;                                    \
+    new_entry.first  = symbol(k);                       \
+    new_entry.second.m_kind = KIND;                     \
+    new_entry.second.FIELD_NAME = v;                    \
+    m_entries.push_back(new_entry);                     \
+})
+
+// setters
+void params::set_bool(symbol const & k, bool v) {
+    SET_SIMPLE_VALUE(m_bool_value, CPK_BOOL);
+}
+
+void params::set_bool(char const * k, bool  v) {
+    SET_SIMPLE_VALUE(m_bool_value, CPK_BOOL);
+}
+ 
+void params::set_uint(symbol const & k, unsigned v) {
+    SET_SIMPLE_VALUE(m_uint_value, CPK_UINT);
+}
+
+void params::set_uint(char const * k, unsigned v) {
+    SET_SIMPLE_VALUE(m_uint_value, CPK_UINT);
+}
+
+void params::set_double(symbol const & k, double v) {
+    SET_SIMPLE_VALUE(m_double_value, CPK_DOUBLE);
+}
+
+void params::set_double(char const * k, double v) {
+    SET_SIMPLE_VALUE(m_double_value, CPK_DOUBLE);
+}
+
+void params::set_str(symbol const & k, char const * v) {
+    SET_SIMPLE_VALUE(m_str_value, CPK_STRING);
+}
+
+void params::set_str(char const * k, char const * v) {
+    SET_SIMPLE_VALUE(m_str_value, CPK_STRING);
+}
+
+#define SET_RAT_VALUE() SET_VALUE({                             \
+    if (it->second.m_kind != CPK_NUMERAL) {                     \
+        del_value(*it);                                         \
+        it->second.m_kind = CPK_NUMERAL;                        \
+        it->second.m_rat_value = alloc(rational);               \
+    }                                                           \
+    *(it->second.m_rat_value) = v;                              \
+},                                                              \
+{                                                               \
+    entry new_entry;                                            \
+    new_entry.first  = symbol(k);                               \
+    new_entry.second.m_kind = CPK_NUMERAL;                      \
+    new_entry.second.m_rat_value = alloc(rational);             \
+    *(new_entry.second.m_rat_value) = v;                        \
+    m_entries.push_back(new_entry);                             \
+})
+
+void params::set_rat(symbol const & k, rational const & v) {
+    SET_RAT_VALUE();
+}
+
+void params::set_rat(char const * k, rational const & v) {
+    SET_RAT_VALUE();
+}
+
+#define SET_SYM_VALUE() SET_VALUE({                     \
+    del_value(*it);                                     \
+    it->second.m_kind = CPK_SYMBOL;                     \
+    it->second.m_sym_value = v.bare_str();              \
+},                                                      \
+{                                                       \
+    entry new_entry;                                    \
+    new_entry.first  = symbol(k);                       \
+    new_entry.second.m_kind = CPK_SYMBOL;               \
+    new_entry.second.m_sym_value = v.bare_str();        \
+    m_entries.push_back(new_entry);                     \
+})
+
+void params::set_sym(symbol const & k, symbol const & v) {
+    SET_SYM_VALUE();
+}
+
+void params::set_sym(char const * k, symbol const & v) {
+    SET_SYM_VALUE();
+}
+

src/util/params.h

@@ -0,0 +1,112 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    params.h
+
+Abstract:
+
+    Parameters.
+
+Author:
+
+    Leonardo (leonardo) 2011-04-22
+
+Notes:
+
+--*/
+#ifndef _PARAMS_H_
+#define _PARAMS_H_
+
+#include"cmd_context_types.h"
+#include"vector.h"
+
+typedef cmd_arg_kind param_kind;
+
+class params;
+class param_descrs;
+
+class params_ref {
+    params * m_params;
+    void init();
+    void copy_core(params const * p);
+public:
+    params_ref():m_params(0) {}
+    params_ref(params_ref const & p);
+    ~params_ref();
+
+    params_ref & operator=(params_ref const & p);
+    
+    // copy params from p
+    void copy(params_ref const & src);
+    void append(params_ref const & src) { copy(src); }
+     
+    bool get_bool(symbol const & k, bool _default) const;
+    bool get_bool(char const * k, bool _default) const;
+    unsigned get_uint(symbol const & k, unsigned _default) const;
+    unsigned get_uint(char const * k, unsigned _default) const;
+    double get_double(symbol const & k, double _default) const;
+    double get_double(char const * k, double _default) const;
+    char const * get_str(symbol const & k, char const * _default) const;
+    char const * get_str(char const * k, char const * _default) const;
+    rational get_rat(symbol const & k, rational const & _default) const;
+    rational get_rat(char const * k, rational const & _default) const;
+    symbol get_sym(symbol const & k, symbol const & _default) const;
+    symbol get_sym(char const * k, symbol const & _default) const;
+
+    bool empty() const;
+    bool contains(symbol const & k) const;
+    bool contains(char const * k) const;
+
+    void reset();
+    void reset(symbol const & k);
+    void reset(char const * k);
+
+    void set_bool(symbol const & k, bool v);
+    void set_bool(char const * k, bool  v);
+    void set_uint(symbol const & k, unsigned v);
+    void set_uint(char const * k, unsigned v);
+    void set_double(symbol const & k, double v);
+    void set_double(char const * k, double v);
+    void set_str(symbol const & k, char const * v);
+    void set_str(char const * k, char const * v);
+    void set_rat(symbol const & k, rational const & v);
+    void set_rat(char const * k, rational const & v); 
+    void set_sym(symbol const & k, symbol const & v);
+    void set_sym(char const * k, symbol const & v);
+
+    void display(std::ostream & out) const;
+
+    void validate(param_descrs const & p) const;
+};
+
+inline std::ostream & operator<<(std::ostream & out, params_ref const & ref) {
+    ref.display(out);
+    return out;
+}
+
+class param_descrs {
+    struct imp;
+    imp *  m_imp;
+public:
+    param_descrs();
+    ~param_descrs();
+    void insert(char const * name, param_kind k, char const * descr);
+    void insert(symbol const & name, param_kind k, char const * descr);
+    void erase(char const * name);
+    void erase(symbol const & name);
+    param_kind get_kind(char const * name) const;
+    param_kind get_kind(symbol const & name) const;
+    void display(std::ostream & out, unsigned indent = 0) const;
+    unsigned size() const; 
+    symbol get_param_name(unsigned idx) const;
+};
+
+void insert_max_memory(param_descrs & r);
+void insert_max_steps(param_descrs & r);
+void insert_produce_models(param_descrs & r);
+void insert_produce_proofs(param_descrs & r);
+void insert_timeout(param_descrs & r);
+
+#endif

src/util/skip_list_base.h

@@ -0,0 +1,871 @@
+/*++
+Copyright (c) 2006 Microsoft Corporation
+
+Module Name:
+
+    skip_list_base.h
+
+Abstract:
+
+    <abstract>
+
+Author:
+
+    Leonardo de Moura (leonardo) 2010-10-01.
+
+Revision History:
+
+   WARNING: IT IS NOT SAFE TO STORE KEYS, VALUES in the SKIP_LIST that need non-default constructors/destructors.
+
+--*/
+#ifndef _SKIP_LIST_BASE_H_
+#define _SKIP_LIST_BASE_H_
+
+#include<memory.h>
+#include"util.h"
+#include"memory_manager.h"
+#include"small_object_allocator.h"
+#include"trace.h"
+
+#ifdef _MSC_VER
+#pragma warning(disable : 4200)
+#endif
+
+/*
+  This file defines a base class for implementing skip-list like data-structures.
+  This base class is relies on a manager for providing some basic services.
+  The manager is a template parameter.
+
+  A Skip-list manager is responsible for:
+
+  - Providing primitives for allocating/deallocating memory
+         void * allocate(size_t size);
+         void deallocate(size_t size, void* p);
+  - Generating random skip-list levels efficiently
+         unsigned random_level(unsigned max_level);
+  - Call-backs that will be invoked when a reference for a "value" stored in the skip-list is incremented/decremented.
+         void inc_ref_eh(value const & v);
+         void dec_ref_eh(value const & h);
+*/
+
+/**
+   \brief Base class for generating random_levels.
+*/
+class random_level_manager {
+#define SL_BITS_IN_RANDOM 16
+    unsigned m_random_data;
+    unsigned m_random_bits:16;
+    unsigned m_random_left:16;
+    
+    unsigned random_value() {
+        return ((m_random_data = m_random_data * 214013L + 2531011L) >> 16) & 0xffff; 
+    }
+
+    void init_random() {
+        m_random_data = 0;
+        m_random_bits = random_value();
+        m_random_left = SL_BITS_IN_RANDOM/2;
+    }
+public:
+    random_level_manager() {
+        init_random();
+    }
+
+    unsigned random_level(unsigned max_level) {
+        unsigned level = 1;
+        unsigned b;
+        do {
+            b = m_random_bits&3; 
+            if (!b) 
+                level++;
+            m_random_bits >>= 2;
+            m_random_left--;
+            if (m_random_left == 0) {
+                m_random_bits = random_value();
+                m_random_left = SL_BITS_IN_RANDOM/2;
+            }
+        } while (!b);
+        return (level > max_level ? max_level : level);
+    }
+    
+};
+
+/**
+   \brief Basic skip-list manager. 
+   The class is parametrized by the Value type that is stored in the skip-list.
+*/
+template<typename Value>
+class sl_manager_base : public random_level_manager {
+    typedef Value value;
+
+    small_object_allocator m_alloc;
+
+public:
+    void * allocate(size_t size) {
+        return m_alloc.allocate(size);
+    }
+    
+    void deallocate(size_t size, void* p) {
+        m_alloc.deallocate(size, p);
+    }
+
+    void inc_ref_eh(value const & v) {
+        /* do nothing */
+    }
+
+    void dec_ref_eh(value const & h) {
+        /* do nothing */
+    }
+};
+
+#define SL_SIZE_NUM_BITS 12
+#define SL_CAPACITY_NUM_BITS SL_SIZE_NUM_BITS
+#define SL_MAX_CAPACITY ((1 << SL_SIZE_NUM_BITS) - 1)
+#define SL_LEVEL_NUM_BITS    8
+#define SL_MAX_LEVEL ((1 << SL_LEVEL_NUM_BITS) - 1)
+COMPILE_TIME_ASSERT(SL_SIZE_NUM_BITS == SL_CAPACITY_NUM_BITS);
+COMPILE_TIME_ASSERT(SL_SIZE_NUM_BITS + SL_CAPACITY_NUM_BITS + SL_LEVEL_NUM_BITS == 32);
+
+/**
+   \brief Base (template) class for implementing skip-list like data-structures where
+   entries are stored in buckets to improve cache behavior.
+
+   The Traits template parameter must provide:
+   
+   - a definition for the class Traits::manager
+   - a definition for the class Traits::entry which provides:
+      - a definition for the types key and value
+      - the methods: 
+          key const & begin_key() const
+          key const & end_key() const
+          value const & val() const
+          void set_begin_key(key const & k)
+          void set_end_key(key const & k)
+          void set_val(value const & v)
+          void display(ostream & out) const
+   - the maximal number of levels Traits::max_level
+   - the maximal capacity of each bucket  Traits::max_capacity
+   - the initial capacity of the first bucket Traits::initial_capacity
+   - flag for reference counting support Traits::ref_count. If this flag is true
+     the methods inc_ref_eh and dec_ref_eh in the manager object will be invoked.
+   - the methods
+        bool lt(key const & k1, key const & k2)
+        bool eq(key const & k1, key const & k2)
+        bool val_eq(value const & v1, value const & v2)
+        key succ(key const & k)   
+        key pred(key const & k)
+*/
+template<typename Traits>
+class skip_list_base : protected Traits {
+protected:
+    typedef typename Traits::entry   entry;
+public:
+    typedef typename Traits::manager manager;
+    typedef typename entry::key      key;
+    typedef typename entry::value    value;
+
+    struct bucket {
+        unsigned   m_size:SL_SIZE_NUM_BITS;          //!< number of entries stored in the bucket.
+        unsigned   m_capacity:SL_CAPACITY_NUM_BITS;  //!< capacity (number of entries) that can be stored in the bucket.
+        unsigned   m_level:SL_LEVEL_NUM_BITS; 
+        char       m_extra[0];
+    
+        static unsigned get_obj_size(unsigned num_lvls, unsigned capacity) {
+            return sizeof(bucket) + num_lvls*sizeof(bucket*) + capacity*sizeof(entry);
+        }
+
+        entry * get_entries() { return reinterpret_cast<entry*>(m_extra); }
+        entry const * get_entries() const { return reinterpret_cast<entry const *>(m_extra); }
+        
+        bucket ** next_vect() { return reinterpret_cast<bucket**>(get_entries() + m_capacity); }
+        bucket * const * next_vect() const { return reinterpret_cast<bucket* const *>(get_entries() + m_capacity); }
+    
+        bucket(unsigned lvl, unsigned capacity = Traits::max_capacity):
+            m_size(0),
+            m_capacity(capacity),
+            m_level(lvl) {
+            memset(next_vect(), 0, sizeof(bucket*)*lvl);
+        }
+    
+        unsigned level() const { return m_level; }
+        unsigned size() const { return m_size; }
+        unsigned capacity() const { return m_capacity; }
+        bool empty() const { return size() == 0; }
+        void set_size(unsigned sz) { m_size = sz; }
+        void shrink(unsigned delta) { m_size -= delta; }
+        void expand(unsigned delta) { m_size += delta; }
+        entry & first_entry() { SASSERT(!empty()); return get_entries()[0]; } 
+        entry & last_entry() { SASSERT(!empty()); return get_entries()[size() - 1]; }
+        entry const & first_entry() const { SASSERT(!empty()); return get_entries()[0]; } 
+        entry const & last_entry() const { SASSERT(!empty()); return get_entries()[size() - 1]; }
+        entry const & get(unsigned idx) const { SASSERT(idx < size()); return get_entries()[idx]; }
+        entry & get(unsigned idx) { SASSERT(idx < size()); return get_entries()[idx]; }
+        void set(unsigned idx, entry const & e) { SASSERT(idx < capacity()); get_entries()[idx] = e; }
+        bucket * get_next(unsigned idx) const { return next_vect()[idx]; }
+        void set_next(unsigned idx, bucket * bt) { SASSERT(idx < level()); next_vect()[idx] = bt; }
+    };
+
+    // Only the header bucket has zero entries.
+    bucket * m_header;
+    
+    bucket * first_bucket() const {
+        return m_header->get_next(0);
+    }
+
+#ifdef Z3DEBUG
+    /**
+       \brief (debugging only) Return the predecessor bucket of the given bucket.
+       
+       \pre bt != m_header, and bt is a bucket of the list.
+    */
+    bucket * pred_bucket(bucket * bt) const {
+        SASSERT(bt != m_header);
+        bucket * curr = m_header;
+        while (curr->get_next(0) != bt) {
+            curr = curr->get_next(0);
+            SASSERT(curr != 0); // bt is not in the list
+        }
+        return curr;
+    }
+#endif
+
+    bool lt(key const & k1, key const & k2) const { return Traits::lt(k1, k2); }
+
+    bool gt(key const & k1, key const & k2) const { return lt(k2, k1); }
+
+    bool geq(key const & k1, key const & k2) const { return !lt(k1, k2); }
+
+    bool leq(key const & k1, key const & k2) const { return !gt(k1, k2); }
+    
+    /**
+       \brief Create a new bucket of the given level.
+    */
+    static bucket * mk_bucket(manager & m, unsigned lvl, unsigned capacity = Traits::max_capacity) {
+        void * mem = m.allocate(bucket::get_obj_size(lvl, capacity));
+        return new (mem) bucket(lvl, capacity);
+    }
+
+    static bucket * mk_header(manager & m, unsigned lvl) {
+        return mk_bucket(m, lvl, 0);
+    }
+
+    static void inc_ref(manager & m, value const & v) {
+        if (Traits::ref_count)
+            m.inc_ref_eh(v);
+    }
+
+    static void dec_ref(manager & m, value const & v) {
+        if (Traits::ref_count)
+            m.dec_ref_eh(v);
+    }
+
+    /**
+       \brief Invoke dec_ref_eh for each value stored in the bucket.
+    */
+    static void dec_ref(manager & m, bucket * bt) {
+        if (Traits::ref_count) {
+            unsigned sz = bt->size();
+            for (unsigned i = 0; i < sz; i++)
+                m.dec_ref_eh(bt->get(i).val());
+        }
+    }
+
+    /**
+       \brief Deallocate the given bucket.
+       
+       \remark This method invokes dec_ref_eh for each value in the bucket.
+    */
+    template<bool DecRef>
+    static void deallocate_bucket(manager & m, bucket * bt) {
+        if (DecRef)
+            dec_ref(m, bt);
+        unsigned sz = bucket::get_obj_size(bt->level(), bt->capacity());
+        bt->~bucket();
+        m.deallocate(sz, bt);
+    }
+
+    /**
+       \brief Deallocate all buckets in the skip list.
+       
+       \remark This method invokes dec_ref_eh for each value in the list.
+    */
+    template<bool DecRef>
+    void deallocate_list(manager & m) {
+        bucket * curr = m_header;
+        while (curr != 0) {
+            bucket * old = curr;
+            curr = curr->get_next(0);
+            deallocate_bucket<DecRef>(m, old);
+        }
+    }
+
+#ifdef Z3DEBUG
+    /**
+       \brief Check the following property
+       
+       for all i \in [0, b->level()) . pred_vect[i]->get_next(i) == b
+    */
+    bool check_pred_vect(bucket * bt, bucket * pred_vect[]) {
+        if (bt == 0) 
+            return true;
+        for (unsigned i = 0; i < bt->level(); i++) {
+            SASSERT(pred_vect[i]->get_next(i) == bt);
+        }
+        return true;
+    }
+#endif
+
+    /**
+       \brief Delete the given buffer and update the forward/next pointer of the buckets in pred_vect.
+       
+       \remark This method invokes dec_ref_eh for each value in the bucket.
+    */
+    void del_bucket(manager & m, bucket * bt, bucket * pred_vect[]) {
+        SASSERT(check_pred_vect(bt, pred_vect));
+        for (unsigned i = 0; i < bt->level(); i++)
+            pred_vect[i]->set_next(i, bt->get_next(i));
+        deallocate_bucket<true>(m, bt);
+    }
+
+    /**
+       \brief Update the \c pred_vect vector from levels [0, bt->level()).
+       That is, bt will be now the "predecessor" for these levels.
+    */
+    static void update_predecessor_vector(bucket * pred_vect [], bucket * bt) {
+        unsigned lvl = bt->level();
+        for (unsigned i = 0; i < lvl; i++) {
+            pred_vect[i] = bt;
+        }
+    }
+
+    /**
+       \brief Similar to the previous method, but the updated vector is stored in new_pred_vect.
+    */
+    void update_predecessor_vector(bucket * pred_vect[], bucket * bt, bucket * new_pred_vect[]) {
+        unsigned bt_lvl = bt->level();
+        for (unsigned i = 0; i < bt_lvl; i++) {
+            new_pred_vect[i] = bt;
+        }
+        unsigned list_lvl = level();
+        for (unsigned i = bt_lvl; i < list_lvl; i++) {
+            new_pred_vect[i] = pred_vect[i];
+        }
+    }
+
+    /**
+       \brief Return the list level.
+    */
+    unsigned level() const {
+        return m_header->level();
+    }
+
+    /**
+       \brief Expand/Increase the number of levels in the header.
+    */
+    void expand_header(manager & m, unsigned new_lvl) {
+        SASSERT(new_lvl > level());
+        bucket * new_header = mk_header(m, new_lvl);
+        // copy forward pointers of the old header.
+        unsigned old_lvl    = level();
+        for (unsigned i = 0; i < old_lvl; i++)
+            new_header->set_next(i, m_header->get_next(i));
+        // update header
+        deallocate_bucket<false>(m, m_header);
+        m_header = new_header;
+    }
+
+    /**
+       \brief Increase list level to lvl if lvl > level()
+    */
+    void update_list_level(manager & m, unsigned lvl) {
+        if (lvl > level()) {
+            expand_header(m, lvl);
+        }
+    }
+
+    /**
+       \brief Increase list level (and store m_header in the new levels in pred_vect) if lvl > level().
+    */
+    void update_list_level(manager & m, unsigned lvl, bucket * pred_vect[]) {
+        if (lvl > level()) {
+            bucket * old_header = m_header;
+            unsigned old_lvl    = m_header->level();
+            expand_header(m, lvl);
+            for (unsigned i = 0; i < old_lvl; i++) {
+                if (pred_vect[i] == old_header)
+                    pred_vect[i] = m_header;
+            }
+            for (unsigned i = old_lvl; i < lvl; i++) {
+                pred_vect[i] = m_header;
+            }
+            SASSERT(level() == lvl);
+        }
+    }
+
+    /**
+       \brief Add first entry to the list.
+
+       \remark This method will invoke inc_ref_eh for e.val()
+    */
+    void insert_first_entry(manager & m, entry const & e) {
+        unsigned lvl        = m.random_level(Traits::max_level);
+        bucket * new_bucket = mk_bucket(m, lvl, Traits::initial_capacity);
+        update_list_level(m, lvl);
+        for (unsigned i = 0; i < lvl; i++) {
+            m_header->set_next(i, new_bucket);
+        }
+        inc_ref(m, e.val());
+        new_bucket->set_size(1);
+        new_bucket->set(0, e);
+    }
+
+    /**
+       \brief Expand the capacity of the first-bucket in a skip-list with only one bucket.
+       This method assumes the capacity of the first-bucket < Traits::max_capacity
+     */
+    void expand_first_bucket(manager & m) {
+        bucket * f = first_bucket();
+        SASSERT(f != 0);
+        SASSERT(f->get_next(0) == 0);
+        SASSERT(f->capacity() < Traits::max_capacity);
+        unsigned old_capacity = f->capacity();
+        SASSERT(old_capacity > 0);
+        unsigned new_capacity = old_capacity * 2;
+        if (new_capacity > Traits::max_capacity)
+            new_capacity = Traits::max_capacity;
+        unsigned lvl = f->level();
+        bucket * new_f = mk_bucket(m, lvl, new_capacity);
+        unsigned sz = f->size();
+        new_f->set_size(sz);
+        for (unsigned i = 0; i < sz; i++) 
+            new_f->set(i, f->get(i));
+        for (unsigned i = 0; i < lvl; i++)
+            m_header->set_next(i, new_f);
+        deallocate_bucket<false>(m, f);
+        SASSERT(first_bucket() == new_f);
+    }
+
+    /**
+       \brief Create a new bucket and divide the elements in bt between bt and the new bucket.
+    */
+    void splice(manager & m, bucket * bt, bucket * pred_vect[]) {
+        SASSERT(bt->capacity() == Traits::max_capacity);
+        unsigned bt_lvl         = bt->level();
+        unsigned new_bucket_lvl = m.random_level(Traits::max_level);
+        bucket * new_bucket     = mk_bucket(m, new_bucket_lvl);
+        update_list_level(m, new_bucket_lvl, pred_vect);
+        unsigned _lvl           = std::min(bt_lvl, new_bucket_lvl);
+        for (unsigned i = 0; i < _lvl; i++) {
+            new_bucket->set_next(i, bt->get_next(i));
+            bt->set_next(i, new_bucket);
+        }
+        for (unsigned i = bt_lvl; i < new_bucket_lvl; i++) {
+            new_bucket->set_next(i,   pred_vect[i]->get_next(i));
+            pred_vect[i]->set_next(i, new_bucket);
+        }
+        unsigned old_size  = bt->size();
+        SASSERT(old_size >= 2);
+        unsigned mid              = old_size/2;
+        new_bucket->set_size(old_size - mid);
+        unsigned i = mid;
+        unsigned j = 0;
+        for (; i < old_size; i++, j++) {
+            new_bucket->set(j, bt->get(i));
+        }
+        bt->set_size(mid);
+        SASSERT(!bt->empty());
+        SASSERT(!new_bucket->empty());
+    }
+    
+    /**
+       \brief Open space at position idx. The number of entries in bt is increased by one.
+
+       \remark This method will *NOT* invoke inc_ref_eh
+    */
+    void open_space(bucket * bt, unsigned idx) {
+        SASSERT(bt->size() < bt->capacity());
+        SASSERT(idx <= bt->size());
+        unsigned i = bt->size();
+        while (i > idx) {
+            bt->set(i, bt->get(i-1));
+            i--;
+        }
+        bt->expand(1);
+    }
+
+    /**
+       \brief Open two spaces at position idx. The number of entries in bt is increased by one.
+
+       \remark This method will *NOT* invoke inc_ref_eh
+    */
+    void open_2spaces(bucket * bt, unsigned idx) {
+        SASSERT(bt->size() < bt->capacity() - 1);
+        SASSERT(idx <= bt->size());
+        unsigned i = bt->size() + 1;
+        unsigned end = idx + 1;
+        while (i > end) {
+            bt->set(i, bt->get(i-2));
+            i--;
+        }
+        bt->expand(2);
+    }
+
+    /**
+       \brief Delete entry at position idx.
+
+       \remark This method will invoke dec_ref_eh for the value stored in entry at position idx.
+    */
+    void del_entry(manager & m, bucket * bt, unsigned idx) {
+        SASSERT(!bt->empty());
+        SASSERT(idx < bt->size());
+        dec_ref(m, bt->get(idx).val());
+        unsigned sz = bt->size();
+        for (unsigned i = idx; i < sz - 1; i++) {
+            bt->set(i, bt->get(i+1));
+        }
+        bt->shrink(1);
+    }
+
+    /**
+       \brief Create a copy of the skip list.
+
+       \remark This method will invoke inc_ref_eh for all values copied.
+    */
+    void clone_core(manager & m, skip_list_base * new_list) const {
+        bucket * pred_vect[Traits::max_level]; 
+        unsigned lvl = level();
+        new_list->update_list_level(m, lvl);
+        bucket * new_header = new_list->m_header;
+        for (unsigned i = 0; i < lvl; i++)
+            pred_vect[i] = new_header;
+        bucket * curr = first_bucket();
+        while (curr != 0) {
+            unsigned curr_lvl   = curr->level();
+            bucket * new_bucket = new_list->mk_bucket(m, curr_lvl, curr->capacity());
+            for (unsigned i = 0; i < curr_lvl; i++) {
+                pred_vect[i]->set_next(i, new_bucket);
+                pred_vect[i]            = new_bucket;
+            }
+            unsigned curr_sz    = curr->size();
+            for (unsigned i = 0; i < curr_sz; i++) {
+                entry const & curr_entry = curr->get(i);
+                inc_ref(m, curr_entry.val());
+                new_bucket->set(i, curr_entry);
+            }
+            new_bucket->set_size(curr_sz);
+            curr = curr->get_next(0);
+        }
+    }
+
+public:
+    skip_list_base():
+        m_header(0) {
+        SASSERT(Traits::max_capacity >= 2);
+        SASSERT(Traits::initial_capacity >= 2);
+        SASSERT(Traits::initial_capacity <= Traits::max_capacity);
+        SASSERT(Traits::max_level >= 1);
+        SASSERT(Traits::max_capacity <= SL_MAX_CAPACITY);
+        SASSERT(Traits::max_level <= SL_MAX_LEVEL);
+    }
+
+    skip_list_base(manager & m):
+        m_header(0) {
+        SASSERT(Traits::max_capacity >= 2);
+        SASSERT(Traits::initial_capacity >= 2);
+        SASSERT(Traits::initial_capacity <= Traits::max_capacity);
+        SASSERT(Traits::max_level >= 1);
+        SASSERT(Traits::max_capacity <= SL_MAX_CAPACITY);
+        SASSERT(Traits::max_level <= SL_MAX_LEVEL);
+        init(m);
+    }
+
+    ~skip_list_base() {
+        SASSERT(m_header == 0);
+    }
+
+    void deallocate(manager & m) {
+        deallocate_list<true>(m);
+        m_header = 0;
+    }
+    
+    /**
+       \brief Deallocate the list but do not invoke dec_ref_eh.
+    */
+    void deallocate_no_decref(manager & m) {
+        deallocate_list<false>(m);
+        m_header = 0;
+    }
+
+    /**
+       \brief Initialize a list that was created using the default constructor.
+       It can be used also to initialized a list deallocated using the method #deallocate.
+    */
+    void init(manager & m) {
+        SASSERT(m_header == 0);
+        m_header = mk_header(m, 1);
+    }
+
+    /**
+       \brief Remove all elements from the skip-list.
+    */
+    void reset(manager & m) {        
+        deallocate_list<true>(m);
+        m_header = mk_header(m, 1);
+    }
+
+    /**
+       \brief Remove all elements from the skip-list without invoking dec_ref_eh.
+    */
+    void reset_no_decref(manager & m) {        
+        deallocate_list<false>(m);
+        m_header = mk_header(m, 1);
+    }
+    
+    /**
+       \brief Return true if the list is empty.
+    */
+    bool empty() const {
+        SASSERT(m_header != 0);
+        return first_bucket() == 0;
+    }
+    
+protected:
+    /**
+       \brief Return the position of the bucket in the skip list.
+    */
+    unsigned get_bucket_idx(bucket const * bt) const {
+        bucket * curr = m_header;
+        unsigned pos  = 0;
+        while (curr != 0) {
+            if (curr == bt)
+                return pos;
+            pos++;
+            curr = curr->get_next(0);
+        }
+        UNREACHABLE();
+        return pos;
+    }
+
+    /**
+       \brief Display the given entry.
+    */
+    void display(std::ostream & out, entry const & e) const {
+        e.display(out);
+    }
+
+    /**
+       \brief Display a reference to the given bucket.
+    */
+    void display_bucket_ref(std::ostream & out, bucket const * bt) const {
+        if (bt == 0)
+            out << "NIL";
+        else
+            out << "#" << get_bucket_idx(bt);
+    }
+
+    /**
+       \brief Display the predecessor vector.
+    */
+    void display_predecessor_vector(std::ostream & out, bucket const * const pred_vect[]) const {
+        for (unsigned i = 0; i < level(); i++) {
+            out << i << ": ";
+            display_bucket_ref(out, pred_vect[i]);
+            if (pred_vect[i]) {
+                out << " -> ";
+                display_bucket_ref(out, pred_vect[i]->get_next(i));
+            }
+            out << "\n";
+        }
+    }
+
+    /**
+       \brief Display the successors of the given bucket.
+    */
+    void display_successors(std::ostream & out, bucket const * bt) const {
+        out << "[";
+        for (unsigned i = 0; i < bt->level(); i++) {
+            if (i > 0) out << ", ";
+            display_bucket_ref(out, bt->get_next(i));
+        }
+        out << "]";
+    }
+
+    /**
+       \brief Display the given bucket.
+    */
+    void display(std::ostream & out, bucket const * bt) const {
+        if (bt == 0) {
+            out << "NIL\n";
+            return;
+        }
+        out << "bucket ";
+        display_bucket_ref(out, bt);
+        out << ", capacity: " << bt->capacity() << "\n";
+        out << "successors: ";
+        display_successors(out, bt);
+        out << "\n";
+        out << "entries:\n";
+        for (unsigned i = 0; i < bt->size(); i++) {
+            display(out, bt->get(i));
+            out << "\n";
+        }
+        out << "----------\n";
+    }
+
+public:
+    /**
+       \brief Dump the skip list for debugging purposes. 
+       It assumes that key and value types implement operator <<.
+    */
+    void display_physical(std::ostream & out) const {
+        out << "{\nskip-list level: " << m_header->level() << "\n";
+        bucket * curr = m_header;
+        while (curr != 0) {
+            display(out, curr);
+            curr = curr->get_next(0);
+        }
+        out << "}\n";
+    }
+
+    void display(std::ostream & out) const {
+        bucket * curr = m_header;
+        while (curr != 0) {
+            unsigned sz = curr->size();
+            for (unsigned i = 0; i < sz; i++) {
+                if (i > 0)
+                    out << " ";
+                curr->get(i).display(out);
+            }
+            curr = curr->get_next(0);
+        }
+    }
+
+protected:
+    /**
+       \brief Return true if bucket b2 can be reached from b1 following get_next(i) pointers
+    */
+    bool is_reachable_at_i(bucket const * bt1, bucket const * bt2, unsigned i) const {
+        bucket * curr = bt1->get_next(i);
+        while (curr != 0) {
+            if (curr == bt2)
+                return true;
+            curr = curr->get_next(i);
+        }
+        return false;
+    }
+
+protected:
+    static void display_size_info_core(std::ostream & out, unsigned cls_size) {
+        out << "sizeof root:          " << cls_size << "\n";
+        out << "bucket max capacity:  " << Traits::max_capacity << "\n";
+        out << "bucket max level:     " << Traits::max_level << "\n";
+        out << "sizeof(bucket):       " << sizeof(bucket) << " + " << sizeof(bucket*) << "*lvl + " << sizeof(entry) << "*capacity\n";
+        out << "sizeof(usual bucket): " << (sizeof(bucket) + sizeof(entry)*Traits::max_capacity) << " + " << sizeof(bucket*) << "*lvl\n";
+        out << "sizeof(max. bucket):  " << (sizeof(bucket) + sizeof(entry)*Traits::max_capacity + sizeof(bucket*)*Traits::max_level) << "\n";
+        out << "sizeof(entry):        " << sizeof(entry) << "\n";
+        out << "sizeof empty:         " << cls_size + bucket::get_obj_size(1, 0) << "\n";;
+        out << "sizeof singleton:    [" 
+            << (cls_size + bucket::get_obj_size(1, 0) + bucket::get_obj_size(1, Traits::initial_capacity)) << ", "
+            << (cls_size + 
+                bucket::get_obj_size(Traits::max_level, 0) + 
+                bucket::get_obj_size(Traits::max_level, Traits::max_capacity)) << "]\n";
+    }
+
+public:
+    /**
+       \brief Return true if skip-list has more than k buckets (not considering the header).
+
+       \remark This method is for debugging purposes.
+    */
+    bool has_more_than_k_buckets(unsigned k) const {
+        bucket * curr = first_bucket();
+        while (curr != 0 && k > 0) {
+            curr = curr->get_next(0);
+            k--;
+        }
+        return curr != 0;
+    }
+    
+    /**
+       \brief Return true if the skip-list has more than k entries.
+    */
+    bool has_more_than_k_entries(unsigned k) const {
+        bucket * curr = first_bucket();
+        while (curr != 0 && k >= curr->size()) {
+            k -= curr->size();
+            curr = curr->get_next(0);
+        }
+        SASSERT(curr == 0 || curr->size() > k);
+        return curr != 0;
+    }
+
+protected:
+    /**
+       \brief Return the amount of memory consumed by the list.
+    */
+    unsigned memory_core(unsigned cls_size) const {
+        unsigned r    = 0;
+        r += cls_size;
+        bucket * curr = m_header;
+        while (curr != 0) {
+            r += bucket::get_obj_size(curr->level(), curr->capacity());
+            curr = curr->get_next(0);
+        }
+        return r;
+    }
+
+public:
+    /**
+       \brief Compress the buckets of the skip-list.
+       Make sure that all, but the last bucket, have at least \c load entries.
+       
+       \remark If load > Traits::max_capacity, then it assumes load = Traits::max_capacity.
+    */
+    void compress(manager & m, unsigned load = Traits::max_capacity/2) {
+        if (load > Traits::max_capacity)
+            load = Traits::max_capacity;
+        bucket * pred_vect[Traits::max_level]; 
+        update_predecessor_vector(pred_vect, m_header);
+        bucket * curr = first_bucket();
+        while (curr != 0) {
+            update_predecessor_vector(pred_vect, curr);
+            bucket * next    = curr->get_next(0);
+            while (curr->size() < load && next != 0) {
+                // steal entries of the successor bucket.
+                unsigned deficit   = load - curr->size();
+                unsigned next_size = next->size(); 
+                if (next_size <= deficit) {
+                    for (unsigned i = 0, j = curr->size(); i < next_size; i++, j++) {
+                        curr->set(j, next->get(i));
+                    }
+                    curr->expand(next_size);
+                    bucket * new_next = next->get_next(0);
+                    del_bucket(m, next, pred_vect);
+                    next = new_next;
+                    SASSERT(curr->size() <= load);
+                }
+                else {
+                    for (unsigned i = 0, j = curr->size(); i < deficit; i++, j++) {
+                        curr->set(j, next->get(i));
+                    }
+                    curr->expand(deficit);
+                    for (unsigned i = deficit, j = 0; i < next_size; i++, j++) {
+                        next->set(j, next->get(i));
+                    }
+                    next->set_size(next_size - deficit);
+                    SASSERT(curr->size() == load);
+                }
+            }
+            curr = curr->get_next(0);
+        }
+    }
+
+    void swap(skip_list_base & other) {
+        bucket * tmp   = m_header;
+        m_header       = other.m_header;
+        other.m_header = tmp;
+    }
+};
+
+
+#endif

src/util/statistics.cpp

@@ -20,7 +20,7 @@ Notes:
 #include"map.h"
 #include"str_hashtable.h"
 #include"buffer.h"
-#include"ast_smt2_pp.h"
+#include"smt2_util.h"
 #include<iomanip>
 
 void statistics::update(char const * key, unsigned inc) {

src/util/z3_exception.cpp

@@ -0,0 +1,74 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    z3_exception.cpp
+
+Abstract:
+
+    Generic Z3 exception
+
+Author:
+
+    Leonardo (leonardo) 2012-04-12
+
+Notes:
+
+--*/
+#include<sstream>
+#include<stdarg.h>
+#include<sstream>
+#include"z3_exception.h"
+#include"warning.h"
+#include"error_codes.h"
+#include"debug.h"
+
+unsigned z3_exception::error_code() const { 
+    return ERR_OK; 
+}
+
+bool z3_exception::has_error_code() const { 
+    return error_code() != ERR_OK; 
+}
+
+z3_error::z3_error(unsigned error_code):m_error_code(error_code) { 
+    SASSERT(error_code != 0); 
+}
+
+char const * z3_error::msg() const {
+    switch (m_error_code) {
+    case ERR_MEMOUT: return "out of memory";
+    case ERR_TIMEOUT: return "timeout";
+    case ERR_PARSER: return "parser error"; 
+    case ERR_UNSOUNDNESS: return "unsoundess";
+    case ERR_INCOMPLETENESS: return "incompleteness";
+    case ERR_INI_FILE: return "invalid INI file";
+    case ERR_NOT_IMPLEMENTED_YET: return "not implemented yet";
+    case ERR_OPEN_FILE: return "open file";
+    case ERR_CMD_LINE: return "invalid command line";
+    case ERR_INTERNAL_FATAL: return "internal error";
+    case ERR_TYPE_CHECK: return "type error";
+    default: return "unknown error";
+    }
+}
+
+unsigned z3_error::error_code() const { 
+    return m_error_code; 
+}
+
+default_exception::default_exception(char const* msg, ...) {
+    std::stringstream out;
+    va_list args;
+    va_start(args, msg);
+    format2ostream(out, msg, args);
+    va_end(args);
+    m_msg = out.str();
+}
+
+default_exception::default_exception(std::string const & msg): m_msg(msg) {
+}
+
+char const * default_exception::msg() const { 
+    return m_msg.c_str(); 
+}

src/util/z3_exception.h

@@ -0,0 +1,49 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    z3_exception.h
+
+Abstract:
+
+    Generic Z3 exception
+
+Author:
+
+    Leonardo (leonardo) 2011-04-28
+
+Notes:
+
+--*/
+#ifndef _Z3_EXCEPTION_H_
+#define _Z3_EXCEPTION_H_
+
+#include<string>
+
+class z3_exception {
+public:
+    virtual ~z3_exception() {}
+    virtual char const * msg() const = 0;
+    virtual unsigned error_code() const;
+    bool has_error_code() const;
+};
+
+class z3_error : public z3_exception {
+    unsigned m_error_code;
+public:
+    z3_error(unsigned error_code);
+    virtual char const * msg() const;
+    virtual unsigned error_code() const;
+};
+
+class default_exception : public z3_exception {
+    std::string m_msg;
+public:
+    default_exception(std::string const& msg);
+    default_exception(char const* msg, ...);
+    virtual ~default_exception() {}
+    virtual char const * msg() const;
+};
+
+#endif

src/util/z3_omp.h

@@ -0,0 +1,38 @@
+/*++
+Copyright (c) 2012 Microsoft Corporation
+
+Module Name:
+
+    z3_omp.h
+
+Abstract:
+
+    Wrapper for OMP functions and data-structures
+
+Author:
+
+    Leonardo (leonardo) 2012-01-05
+
+Notes:
+
+--*/
+#ifndef _Z3_OMP_H
+#define _Z3_OMP_H
+
+#ifndef _NO_OMP_
+#include"omp.h"
+#else
+#define omp_in_parallel() false
+#define omp_set_num_threads(SZ) ((void)0)
+#define omp_get_thread_num() 0
+#define omp_get_num_procs()  1
+#define omp_set_nested(V) ((void)0)
+#define omp_init_nest_lock(L) ((void) 0)
+#define omp_destroy_nest_lock(L) ((void) 0)
+#define omp_set_nest_lock(L) ((void) 0)
+#define omp_unset_nest_lock(L) ((void) 0)
+struct omp_nest_lock_t {
+};
+#endif
+
+#endif