checkpoint

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

src/util/fvi.h

@@ -1,214 +0,0 @@
-/*++
-Copyright (c) 2006 Microsoft Corporation
-
-Module Name:
-
-    fvi.h
-
-Abstract:
-
-    Feature Vector Indexing.
-
-Author:
-
-    Leonardo de Moura (leonardo) 2008-02-01.
-
-Revision History:
-
---*/
-#ifndef _FVI_H_
-#define _FVI_H_
-
-#include"splay_tree_map.h"
-#include"hashtable.h"
-#include"vector.h"
-
-/**
-   \brief A feature vector indexing for objects of type T *.
-
-   ToVector is a functor for converting T into a vector of natural numbers.
-   It should provide a method:
-      - void operator(T * d, unsigned * f);
-      This method should fill the vector f with the features of d.
-
-   Hash: functor for computing the hashcode of T *.
-
-   Eq  : functor for comparing T pointers.
-*/
-template<typename T, typename ToVector, typename Hash, typename Eq=ptr_eq<T> >
-class fvi : private ToVector {
-public:
-    struct statistics {
-        unsigned m_size;
-        unsigned m_num_nodes;
-        unsigned m_num_leaves;
-        unsigned m_min_leaf_size;
-        unsigned m_avg_leaf_size;
-        unsigned m_max_leaf_size;
-        statistics() { reset(); }
-
-        void reset() { 
-            m_size = m_num_nodes = m_num_leaves = m_avg_leaf_size = m_max_leaf_size = 0;
-            m_min_leaf_size = UINT_MAX;
-        }
-    };
-    
-private:
-    struct ucompare {
-        int operator()(unsigned i1, unsigned i2) const {
-            if (i1 < i2) return -1;
-            if (i1 > i2) return  1;
-            return 0;
-        }
-    };
-
-    struct node {
-        node() {}
-        virtual ~node() {}
-        virtual bool is_leaf() const = 0;
-    };
-
-    typedef splay_tree_map<unsigned, node *, ucompare> children;
-
-    struct non_leaf : public node {
-        children m_children;
-        non_leaf() {}
-
-        struct delete_children {
-            void operator()(unsigned k, node * n) const {
-                dealloc(n);
-            }
-        };
-
-        virtual ~non_leaf() {
-            delete_children visitor;
-            m_children.visit(visitor);
-            m_children.reset();
-        }
-
-        virtual bool is_leaf() const { return false; }
-    };
-
-    typedef ptr_hashtable<T, Hash, Eq>     set;
-  
-    struct leaf : public node {
-        set   m_set;
-        leaf() {}
-        virtual ~leaf() {}
-        virtual bool is_leaf() const { return true; }
-    };
-
-    unsigned          m_num_features;
-    svector<unsigned> m_tmp_buffer;
-    non_leaf *        m_root;
-
-    struct stop {};
-
-    template<typename Visitor>
-    void visit_leaf(leaf * n, Visitor & v, bool le) const {
-        typename set::iterator it  = n->m_set.begin();
-        typename set::iterator end = n->m_set.end();
-        for (; it != end; ++it)
-            if (!v(*it))
-                throw stop();
-    }
-
-    template<typename Visitor>
-    struct non_leaf_visitor {
-        fvi const & m_owner;        
-        unsigned    m_fidx;
-        Visitor &   m_visitor;
-        bool        m_le;
-
-        non_leaf_visitor(fvi const & o, unsigned fidx, Visitor & v, bool le):
-            m_owner(o), m_fidx(fidx), m_visitor(v), m_le(le) {}
-        
-        void operator()(unsigned k, node * n) {
-            if (n->is_leaf())
-                m_owner.visit_leaf(static_cast<leaf*>(n), m_visitor, m_le);
-            else
-                m_owner.visit_non_leaf(static_cast<non_leaf*>(n), m_fidx + 1, m_visitor, m_le);
-        }
-    };
-        
-    template<typename Visitor>
-    void visit_non_leaf(non_leaf * n, unsigned fidx, Visitor & v, bool le) const {
-        // Remark: this function is recursive, but there is no risk
-        // of stack overflow since the number of features is small.
-        non_leaf_visitor<Visitor> v2(*this, fidx, v, le);
-        if (le)
-            n->m_children.visit_le(v2, m_tmp_buffer[fidx]);
-        else
-            n->m_children.visit_ge(v2, m_tmp_buffer[fidx]);
-    }
-
-#ifdef Z3DEBUG
-    bool m_visiting;
-#endif
-
-    void to_fvector(T * d) const {
-        fvi * _this = const_cast<fvi *>(this);
-        _this->ToVector::operator()(d, _this->m_tmp_buffer.c_ptr()); 
-    }
-    
-    struct non_leaf_stat_visitor {
-        fvi const &  m_owner;        
-        statistics & m_stats;
-        non_leaf_stat_visitor(fvi const & o, statistics & st):m_owner(o), m_stats(st) {}
-        void operator()(unsigned k, node * n);
-    };
-
-    void stats(leaf * n, statistics & result) const;
-    void stats(non_leaf * n, statistics & result) const;
-
-    struct non_leaf_collect_visitor {
-        fvi const &     m_owner;
-        ptr_vector<T> & m_elems;
-        non_leaf_collect_visitor(fvi const & o, ptr_vector<T> & elems):m_owner(o), m_elems(elems) {}
-        void operator()(unsigned k, node * n);
-    };
-
-    void collect(leaf * n, ptr_vector<T> & result) const;
-    void collect(non_leaf * n, ptr_vector<T> & result) const;
-
-public:
-    fvi(unsigned num_features, ToVector const & t = ToVector());
-    ~fvi() { reset(); dealloc(m_root); }
-
-    void insert(T * d);
-    bool contains(T * d) const;
-    void erase(T * d);
-    void reset();
-
-    /**
-       \brief Traverse the elements that have features  smaller (greater) or equal than the one of the given element.
-
-       For each visited element the following method of v is executed:
-
-       - bool operator()(T * d)
-
-       If false is returned, the traversal is aborted.
-       
-       \warning The object cannot be updated during the traversal.
-    */
-    template<typename Visitor>
-    void visit(T * d, Visitor & v, bool le = true) const {
-        DEBUG_CODE(const_cast<fvi*>(this)->m_visiting = true;);
-        to_fvector(d);
-        try {
-            visit_non_leaf(m_root, 0, v, le);
-        }
-        catch (stop) {
-        }
-        DEBUG_CODE(const_cast<fvi*>(this)->m_visiting = false;);
-    }
-
-    void stats(statistics & result) const;
-
-    /**
-       \brief Copy to result the set of elements stored in the index.
-    */
-    void collect(ptr_vector<T> & result) const;
-};
-
-#endif /* _FVI_H_ */

src/util/fvi_def.h

@@ -1,199 +0,0 @@
-/*++
-Copyright (c) 2006 Microsoft Corporation
-
-Module Name:
-
-    fvi_def.h
-
-Abstract:
-
-    Feature Vector Indexing.
-
-Author:
-
-    Leonardo de Moura (leonardo) 2008-02-01.
-
-Revision History:
-
---*/
-#ifndef _FVI_DEF_H_
-#define _FVI_DEF_H_
-
-#include"fvi.h"
-#include"splay_tree_def.h"
-#include"buffer.h"
-
-template<typename T, typename ToVector, typename Hash, typename Eq>
-fvi<T, ToVector, Hash, Eq>::fvi(unsigned num_features, ToVector const & t):
-    ToVector(t),
-    m_num_features(num_features),
-    m_root(0) {
-    m_tmp_buffer.resize(num_features, 0);
-    m_root = alloc(non_leaf);
-    SASSERT(num_features >= 2);
-    DEBUG_CODE(m_visiting = false;);
-}
-
-template<typename T, typename ToVector, typename Hash, typename Eq>
-void fvi<T, ToVector, Hash, Eq>::reset() {
-    SASSERT(!m_visiting);
-    dealloc(m_root);
-    m_root = alloc(non_leaf);
-}
-
-template<typename T, typename ToVector, typename Hash, typename Eq>
-void fvi<T, ToVector, Hash, Eq>::insert(T * d) {
-    SASSERT(!m_visiting);
-    to_fvector(d);
-    non_leaf * n = m_root;
-    unsigned i = 0;
-    for (; i < m_num_features - 1; i++) {
-        node * child = 0;
-        if (!n->m_children.find(m_tmp_buffer[i], child)) { 
-            child = alloc(non_leaf);
-            n->m_children.insert(m_tmp_buffer[i], child);
-        }
-        SASSERT(child);
-        SASSERT(!child->is_leaf());
-        n = static_cast<non_leaf*>(child);
-    }
-    node * l = 0;
-    SASSERT(i == m_num_features - 1);
-    if (!n->m_children.find(m_tmp_buffer[i], l)) {
-        l = alloc(leaf);
-        n->m_children.insert(m_tmp_buffer[i], l);
-    }
-    SASSERT(l);
-    SASSERT(l->is_leaf());
-    static_cast<leaf*>(l)->m_set.insert(d);
-}
-    
-template<typename T, typename ToVector, typename Hash, typename Eq>
-bool fvi<T, ToVector, Hash, Eq>::contains(T * d) const {
-    to_fvector(d);
-    non_leaf * n = m_root;
-    node * child;
-    unsigned i = 0;
-    for (; i < m_num_features - 1; i++) {        
-        if (!n->m_children.find(m_tmp_buffer[i], child))
-            return false;
-        SASSERT(child);
-        SASSERT(!child->is_leaf());
-        n = static_cast<non_leaf*>(child);
-    }
-    SASSERT(i == m_num_features - 1);
-    return 
-        n->m_children.find(m_tmp_buffer[i], child) &&
-        static_cast<leaf*>(child)->m_set.contains(d);
-}
-
-template<typename T, typename ToVector, typename Hash, typename Eq>
-void fvi<T, ToVector, Hash, Eq>::erase(T * d) {
-    SASSERT(!m_visiting);
-    SASSERT(contains(d));
-    ptr_buffer<non_leaf> path;
-    to_fvector(d);
-    non_leaf * n = m_root;
-    node * child;
-    unsigned i = 0;
-    for (; i < m_num_features - 1; i++) {        
-        path.push_back(n);
-        if (!n->m_children.find(m_tmp_buffer[i], child)) {
-            UNREACHABLE();
-        }
-        SASSERT(child);
-        SASSERT(!child->is_leaf());
-        n = static_cast<non_leaf*>(child);
-    }
-    path.push_back(n);    
-    SASSERT(i == m_num_features - 1);
-    if (!n->m_children.find(m_tmp_buffer[i], child)) {
-        UNREACHABLE();
-    }
-    SASSERT(child);
-    SASSERT(child->is_leaf());
-    leaf * l = static_cast<leaf*>(child);
-    l->m_set.erase(d);
-    if (l->m_set.empty()) {
-        dealloc(l);
-        while (true) {
-            non_leaf * n = path.back();
-            n->m_children.erase(m_tmp_buffer[i]);
-            path.pop_back();
-            i--;
-            if (!n->m_children.empty() || n == m_root)
-                break;
-            dealloc(n);
-        }
-    }
-}
-
-template<typename T, typename ToVector, typename Hash, typename Eq>
-void fvi<T, ToVector, Hash, Eq>::non_leaf_stat_visitor::operator()(unsigned k, node * n) {
-    if (n->is_leaf())
-        m_owner.stats(static_cast<leaf*>(n), m_stats);
-    else
-        m_owner.stats(static_cast<non_leaf*>(n), m_stats);
-}
-
-template<typename T, typename ToVector, typename Hash, typename Eq>
-void fvi<T, ToVector, Hash, Eq>::stats(leaf * n, statistics & result) const {
-    unsigned sz = n->m_set.size();
-    result.m_size += sz;
-    if (sz > result.m_max_leaf_size)
-        result.m_max_leaf_size = sz;
-    if (sz < result.m_min_leaf_size)
-        result.m_min_leaf_size = sz;
-    result.m_num_leaves ++;
-    result.m_num_nodes ++;
-}
-
-template<typename T, typename ToVector, typename Hash, typename Eq>
-void fvi<T, ToVector, Hash, Eq>::stats(non_leaf * n, statistics & result) const {
-    result.m_num_nodes++;
-    // Remark: this function is recursive, but there is no risk
-    // of stack overflow since the number of features is small.
-    non_leaf_stat_visitor v(*this, result);
-    n->m_children.visit(v);
-}
-
-template<typename T, typename ToVector, typename Hash, typename Eq>
-void fvi<T, ToVector, Hash, Eq>::stats(statistics & result) const {
-    result.reset();
-    stats(m_root, result);
-    if (m_root->m_children.empty())
-        result.m_min_leaf_size = 0;
-    if (result.m_num_leaves > 0)
-        result.m_avg_leaf_size = result.m_size / result.m_num_leaves;
-}
-
-template<typename T, typename ToVector, typename Hash, typename Eq>
-void fvi<T, ToVector, Hash, Eq>::non_leaf_collect_visitor::operator()(unsigned k, node * n) {
-    if (n->is_leaf())
-        m_owner.collect(static_cast<leaf*>(n), m_elems);
-    else
-        m_owner.collect(static_cast<non_leaf*>(n), m_elems);
-}
-
-template<typename T, typename ToVector, typename Hash, typename Eq>
-void fvi<T, ToVector, Hash, Eq>::collect(leaf * n, ptr_vector<T> & result) const {
-    typename set::iterator it  = n->m_set.begin();
-    typename set::iterator end = n->m_set.end();
-    for (; it != end; ++it)
-        result.push_back(*it);
-}
-
-template<typename T, typename ToVector, typename Hash, typename Eq>
-void fvi<T, ToVector, Hash, Eq>::collect(non_leaf * n, ptr_vector<T> & result) const {
-    // Remark: this function is recursive, but there is no risk
-    // of stack overflow since the number of features is small.
-    non_leaf_collect_visitor v(*this, result);
-    n->m_children.visit(v);
-}
-
-template<typename T, typename ToVector, typename Hash, typename Eq>
-void fvi<T, ToVector, Hash, Eq>::collect(ptr_vector<T> & result) const {
-    collect(m_root, result);
-}
-
-#endif /* _FVI_DEF_H_ */

src/util/hashtable.h

@@ -21,7 +21,7 @@ Revision History:
 #include"debug.h"
 #include<ostream>
 #include"util.h"
-#include"limits.h"
+#include<limits.h>
 #include"memory_manager.h"
 #include"hash.h"
 

src/util/instruction_count.cpp

@@ -1,5 +1,5 @@
 #ifdef _WINDOWS
-#include "windows.h"
+#include <windows.h>
 #endif
 #include "instruction_count.h"
 

src/util/mpz.cpp

@@ -23,16 +23,7 @@ Revision History:
 #include"hash.h"
 #include"bit_util.h"
 
-#if defined(_MP_MSBIGNUM)
-#define COMPILER COMPILER_VC
-#ifndef NDEBUG
-#define NDEBUG
-#endif
-#ifdef ARRAYSIZE
-#undef ARRAYSIZE
-#endif
-#include "..\msbig_rational\msbignum.h"
-#elif defined(_MP_INTERNAL)
+#if defined(_MP_INTERNAL)
 #include"mpn.h"
 #elif defined(_MP_GMP)
 #include<gmp.h>

src/util/nat_set.h

@@ -19,8 +19,8 @@ Revision History:
 #ifndef _NAT_SET_H_
 #define _NAT_SET_H_
 
+#include<limits.h>
 #include"vector.h"
-#include"limits.h"
 
 class nat_set {
     unsigned          m_curr_timestamp;

src/util/union_find.h

@@ -1,160 +0,0 @@
-/*++
-Copyright (c) 2006 Microsoft Corporation
-
-Module Name:
-
-    union_find.h
-
-Abstract:
-
-    <abstract>
-
-Author:
-
-    Leonardo de Moura (leonardo) 2008-05-31.
-
-Revision History:
-
---*/
-#ifndef _UNION_FIND_H_
-#define _UNION_FIND_H_
-
-#include "trail.h"
-
-class union_find_default_ctx {
-public:
-    typedef trail_stack<union_find_default_ctx> _trail_stack;
-    union_find_default_ctx() : m_stack(*this) {}
-       
-    void unmerge_eh(unsigned, unsigned) {}
-    void merge_eh(unsigned, unsigned, unsigned, unsigned) {}
-    void after_merge_eh(unsigned, unsigned, unsigned, unsigned) {}
-
-    _trail_stack& get_trail_stack() { return m_stack; }
-
-private:
-    _trail_stack m_stack;
-};
-
-template<typename Ctx = union_find_default_ctx>
-class union_find {
-    Ctx &                         m_ctx;
-    trail_stack<Ctx> &            m_trail_stack;
-    svector<unsigned>             m_find;
-    svector<unsigned>             m_size;
-    svector<unsigned>             m_next;
-    
-    class mk_var_trail;
-    friend class mk_var_trail;
-
-    class mk_var_trail : public trail<Ctx> {
-        union_find & m_owner;
-    public:
-        mk_var_trail(union_find & o):m_owner(o) {}
-        virtual ~mk_var_trail() {}
-        virtual void undo(Ctx & ctx) {
-            m_owner.m_find.pop_back();
-            m_owner.m_size.pop_back();
-            m_owner.m_next.pop_back();
-        }
-    };
-
-    mk_var_trail                  m_mk_var_trail;
-
-    class merge_trail;
-    friend class merge_trail;
-
-    class merge_trail : public trail<Ctx> {
-        union_find & m_owner;
-        unsigned     m_r1;
-    public:
-        merge_trail(union_find & o, unsigned r1):m_owner(o), m_r1(r1) {}
-        virtual ~merge_trail() {}
-        virtual void undo(Ctx & ctx) { m_owner.unmerge(m_r1); }
-    };
-
-    void unmerge(unsigned r1) {
-        unsigned r2 = m_find[r1];
-        TRACE("union_find", tout << "unmerging " << r1 << " " << r2 << "\n";);
-        SASSERT(find(r2) == r2);
-        m_size[r2] -= m_size[r1];
-        m_find[r1]  = r1;
-        std::swap(m_next[r1], m_next[r2]);
-        m_ctx.unmerge_eh(r2, r1);
-        CASSERT("union_find", check_invariant());
-    }
-
-public:    
-    union_find(Ctx & ctx):m_ctx(ctx), m_trail_stack(ctx.get_trail_stack()), m_mk_var_trail(*this) {}
-
-    unsigned mk_var() {
-        unsigned r = m_find.size();
-        m_find.push_back(r);
-        m_size.push_back(1);
-        m_next.push_back(r);
-        m_trail_stack.push_ptr(&m_mk_var_trail);
-        return r;
-    }
-
-    unsigned get_num_vars() const { return m_find.size(); }
-
-    unsigned find(unsigned v) const {
-        while (true) {
-            unsigned new_v = m_find[v];
-            if (new_v == v)
-                return v;
-            v = new_v;
-        }
-    }
-
-    unsigned next(unsigned v) const { return m_next[v]; }
-
-    bool is_root(unsigned v) const { return m_find[v] == v; }
-
-    void merge(unsigned v1, unsigned v2) {
-        unsigned r1 = find(v1);
-        unsigned r2 = find(v2);
-        TRACE("union_find", tout << "merging " << r1 << " " << r2 << "\n";);
-        if (r1 == r2)
-            return;
-        if (m_size[r1] > m_size[r2])
-            std::swap(r1, r2);
-        m_ctx.merge_eh(r2, r1, v2, v1);
-        m_find[r1] = r2;
-        m_size[r2] += m_size[r1];
-        std::swap(m_next[r1], m_next[r2]);
-        m_trail_stack.push(merge_trail(*this, r1));
-        m_ctx.after_merge_eh(r2, r1, v2, v1);
-        CASSERT("union_find", check_invariant());
-    }
-
-    void display(std::ostream & out) const {
-        unsigned num = get_num_vars(); 
-        for (unsigned v = 0; v < num; v++) {
-            out << "v" << v << " --> v" << m_find[v] << "\n";
-        }
-    }
-
-#ifdef Z3DEBUG
-    bool check_invariant() const {
-        unsigned num = get_num_vars(); 
-        for (unsigned v = 0; v < num; v++) {
-            if (is_root(v)) {
-                unsigned curr = v;
-                unsigned sz   = 0;
-                do {
-                    SASSERT(find(curr) == v);
-                    sz++;
-                    curr = next(curr);
-                }
-                while (curr != v);
-                SASSERT(m_size[v] == sz);
-            }
-        }
-        return true;
-    }
-#endif
-};
-
-#endif /* _UNION_FIND_H_ */
-

src/util/util.cpp

@@ -160,7 +160,7 @@ void escaped::display(std::ostream & out) const {
 #ifdef ARRAYSIZE
 #undef ARRAYSIZE
 #endif
-#include "windows.h"
+#include <windows.h>
 #endif
 
 void z3_bound_num_procs() {

src/util/z3_omp.h

@@ -20,7 +20,7 @@ Notes:
 #define _Z3_OMP_H
 
 #ifndef _NO_OMP_
-#include"omp.h"
+#include<omp.h>
 #else
 #define omp_in_parallel() false
 #define omp_set_num_threads(SZ) ((void)0)