Add support files

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

src/util/debug.cpp

@@ -0,0 +1,101 @@
+/*
+Copyright (c) 2013 Microsoft Corporation. All rights reserved. 
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura 
+*/
+#include "debug.h"
+#include <iostream>
+#include <sstream>
+#include <set>
+#include <string>
+#include <memory>
+
+#ifndef _WINDOWS
+// Support for pid
+#include<unistd.h>
+#endif
+
+namespace lean {
+
+static volatile bool                          g_enable_assertions = true;
+static std::unique_ptr<std::set<std::string>> g_enabled_debug_tags;
+
+void enable_assertions(bool f) {
+    g_enable_assertions = f;
+}
+
+bool assertions_enabled() {
+    return g_enable_assertions;
+}
+
+void notify_assertion_violation(const char * fileName, int line, const char * condition) {
+    std::cerr << "LEAN ASSERTION VIOLATION\n";
+    std::cerr << "File: " << fileName << "\n";
+    std::cerr << "Line: " << line << "\n";
+    std::cerr << condition << "\n";
+    std::cerr.flush();
+}
+
+void enable_debug(char const * tag) {
+    if (!g_enabled_debug_tags)
+        g_enabled_debug_tags.reset(new std::set<std::string>());
+    g_enabled_debug_tags->insert(tag);
+}
+
+void disable_debug(char const * tag) {
+    if (g_enabled_debug_tags)
+        g_enabled_debug_tags->erase(tag);
+}
+
+bool is_debug_enabled(const char * tag) {
+    return g_enabled_debug_tags && g_enabled_debug_tags->find(tag) != g_enabled_debug_tags->end();
+}
+
+void invoke_debugger() {
+    int * x = 0;
+    for (;;) {
+        #ifdef _WINDOWS
+        std::cerr << "(C)ontinue, (A)bort, (S)top\n";
+        #else
+        std::cerr << "(C)ontinue, (A)bort, (S)top, Invoke (G)DB\n";
+        #endif
+        char result;
+        std::cin >> result;
+        switch(result) {
+        case 'C':
+        case 'c':
+            return;
+        case 'A':
+        case 'a':
+            exit(1);
+        case 'S':
+        case 's':
+            // force seg fault...
+            *x = 0;
+            return;
+        #ifndef _WINDOWS
+        case 'G':
+        case 'g': {
+            std::cerr << "INVOKING GDB...\n";
+            std::ostringstream buffer;
+            buffer << "gdb -nw /proc/" << getpid() << "/exe " << getpid();
+            if (system(buffer.str().c_str()) == 0) {
+                std::cerr << "continuing the execution...\n";
+            }
+            else {
+                std::cerr << "ERROR STARTING GDB...\n";
+                // forcing seg fault.
+                int * x = 0;
+                *x = 0;
+            }
+            return;
+        }
+        #endif
+        default:
+            std::cerr << "INVALID COMMAND\n";
+        }
+    }
+}
+
+}

src/util/debug.h

@@ -0,0 +1,42 @@
+/*
+Copyright (c) 2013 Microsoft Corporation. All rights reserved. 
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura 
+*/
+#pragma once
+
+#ifndef __has_builtin
+#define __has_builtin(x) 0
+#endif
+
+#ifdef LEAN_DEBUG
+#define DEBUG_CODE(CODE) CODE
+#else
+#define DEBUG_CODE(CODE) 
+#endif
+
+#define lean_assert(COND) DEBUG_CODE({if (!(COND)) { lean::notify_assertion_violation(__FILE__, __LINE__, #COND); lean::invoke_debugger(); }})
+#define lean_cond_assert(TAG, COND) DEBUG_CODE({if (lean::is_debug_enabled(TAG) && !(COND)) { lean::notify_assertion_violation(__FILE__, __LINE__, #COND); lean::invoke_debugger(); }})
+
+#if __has_builtin(__builtin_unreachable)
+#define lean_unreachable() __builtin_unreachable()
+#else
+#define lean_unreachable() DEBUG_CODE({lean::notify_assertion_violation(__FILE__, __LINE__, "UNREACHABLE CODE WAS REACHED."); lean::invoke_debugger();})
+#endif
+
+#ifdef LEAN_DEBUG
+#define lean_verify(COND) if (!(COND)) { lean::notify_assertion_violation(__FILE__, __LINE__, #COND); lean::invoke_debugger(); }
+#else
+#define lean_verify(COND) (COND)
+#endif
+
+namespace lean {
+ 
+void notify_assertion_violation(char const * file_name, int line, char const * condition);
+void enable_debug(char const * tag);
+void disable_debug(char const * tag);
+bool is_debug_enabled(char const * tag);
+void invoke_debugger();
+
+}

src/util/exception.cpp

@@ -0,0 +1,27 @@
+/*
+Copyright (c) 2013 Microsoft Corporation. All rights reserved. 
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura 
+*/
+#include "exception.h"
+
+namespace lean {
+
+exception::exception(char const * msg):m_msg(msg) {
+}
+
+exception::exception(std::string const & msg):m_msg(msg) {
+}
+
+exception::exception(exception const & e):m_msg(e.m_msg) {
+}
+
+exception::~exception() {
+}
+
+char const * exception::what() const noexcept {
+    return m_msg.c_str();
+}
+
+}

src/util/exception.h

@@ -0,0 +1,23 @@
+/*
+Copyright (c) 2013 Microsoft Corporation. All rights reserved. 
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura 
+*/
+#pragma once
+#include <exception>
+#include <string>
+
+namespace lean {
+
+class exception : public std::exception {
+    std::string m_msg;
+public:
+    exception(char const * msg);
+    exception(std::string const & msg);
+    exception(exception const & ex);
+    virtual ~exception();
+    virtual char const * what() const noexcept;
+};
+
+}

src/util/name.cpp

@@ -0,0 +1,229 @@
+/*
+Copyright (c) 2013 Microsoft Corporation. All rights reserved. 
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura 
+*/
+#include <cstring>
+#include "name.h"
+#include "debug.h"
+
+namespace lean {
+
+constexpr char const * anonymous_str = "[anonymous]";
+
+struct name::imp {
+    bool     m_is_string;
+    unsigned m_rc;
+    imp *    m_prefix;
+    union {
+        char * m_str;
+        unsigned m_k;
+    };
+
+    void inc_ref() { m_rc++; }
+
+    void dec_ref() { 
+        imp * curr = this;
+        while (curr) {
+            lean_assert(curr->m_rc > 0); 
+            curr->m_rc--; 
+            if (curr->m_rc == 0) {
+                imp * p = curr->m_prefix;
+                if (curr->m_is_string)
+                    delete[] reinterpret_cast<char*>(curr);
+                else
+                    delete curr;
+                curr = p;
+            }
+            else {
+                curr = 0;
+            }
+        }
+    }
+
+    imp(bool s, imp * p):m_is_string(s), m_rc(1), m_prefix(p) { if (p) p->inc_ref(); }
+
+    static void display_core(std::ostream & out, char const * sep, imp * p) {
+        lean_assert(p != nullptr);
+        if (p->m_prefix) {
+            display_core(out, sep, p->m_prefix);
+            out << sep;
+        }
+        if (p->m_is_string) 
+            out << p->m_str;
+        else
+            out << p->m_k;
+    }
+
+    static void display(std::ostream & out, char const * sep, imp * p) {
+        if (p == nullptr)
+            out << anonymous_str;
+        else
+            display_core(out, sep, p);
+    }
+};
+
+name::name(imp * p) {
+    m_imp = p;
+    if (m_imp)
+        m_imp->inc_ref();
+}
+
+name::name() {
+    m_imp = nullptr;
+}
+
+name::name(name const & prefix, char const * name) {
+    size_t sz  = strlen(name);
+    lean_assert(sz < 1u<<31);
+    char * mem = new char[sizeof(imp) + sz + 1];
+    m_imp      = new (mem) imp(true, prefix.m_imp);
+    memcpy(mem + sizeof(imp), name, sz + 1);
+    m_imp->m_str       = mem + sizeof(imp);
+}
+
+name::name(name const & prefix, unsigned k) {
+    m_imp      = new imp(false, prefix.m_imp);
+    m_imp->m_k = k;
+}
+
+name::name(char const * n):name(name(), n) {
+}
+
+name::name(unsigned k):name(name(), k) {
+}
+
+name::name(name const & other):m_imp(other.m_imp) {
+    m_imp->inc_ref();
+}
+
+name::name(name && other):m_imp(other.m_imp) {
+    other.m_imp = 0;
+}
+
+name::~name() {
+    if (m_imp)
+        m_imp->dec_ref();
+}
+
+name & name::operator=(name const & other) {
+    if (other.m_imp) 
+        other.m_imp->inc_ref();
+    if (m_imp)
+        m_imp->dec_ref();
+    m_imp = other.m_imp;
+    return *this;
+}
+
+name & name::operator=(name && other) {
+    lean_assert(this != &other);
+    if (m_imp)
+        m_imp->dec_ref();
+    m_imp       = other.m_imp;
+    other.m_imp = 0;
+    return *this;
+}
+
+name::kind name::get_kind() const {
+    if (m_imp == nullptr) 
+        return kind::ANONYMOUS;
+    else 
+        return m_imp->m_is_string ? kind::STRING : kind::NUMERAL;
+}
+
+unsigned name::get_numeral() const {
+    lean_assert(is_numeral());
+    return m_imp->m_k;
+}
+
+char const * name::get_string() const {
+    lean_assert(is_string());
+    return m_imp->m_str;
+}
+
+bool name::operator==(name const & other) const {
+    imp * i1 = m_imp;
+    imp * i2 = other.m_imp;
+    while (true) {
+        if (i1 == i2)
+            return true;
+        if ((i1 == nullptr) != (i2 == nullptr))
+            return false;
+        lean_assert(i1 != nullptr);
+        lean_assert(i2 != nullptr);
+        if (i1->m_is_string != i2->m_is_string)
+            return false;
+        if (m_imp->m_is_string) {
+            if (strcmp(get_string(), other.get_string()) != 0)
+                return false;
+        }
+        else {
+            if (get_numeral() != other.get_numeral())
+                return false;
+        }
+        i1 = i1->m_prefix;
+        i2 = i2->m_prefix;
+    }
+}
+
+bool name::is_atomic() const {
+    return m_imp == nullptr || m_imp->m_prefix == nullptr;
+}
+
+name name::get_prefix() const {
+    lean_assert(!is_atomic());
+    return name(m_imp->m_prefix);
+}
+
+static unsigned num_digits(unsigned k) {
+    if (k == 0)
+        return 1;
+    int r = 0; 
+    while (k != 0) { 
+        k /= 10; 
+        r++; 
+    }
+    return r;
+}
+
+size_t name::size(char const * sep) const {
+    if (m_imp == nullptr) {
+        return strlen(anonymous_str);
+    }
+    else {
+        imp * i       = m_imp;
+        size_t sep_sz = strlen(sep);
+        size_t r      = 0;
+        while (true) {
+            if (i->m_is_string) {
+                r += strlen(i->m_str);
+            }
+            else {
+                r += num_digits(i->m_k);
+            }
+            if (i->m_prefix) {
+                r += sep_sz;
+                i  = i->m_prefix;
+            }
+            else {
+                break;
+            }
+        }
+        return r;
+    }
+}
+
+std::ostream & operator<<(std::ostream & out, name const & n) {
+    name::imp::display(out, default_name_separator, n.m_imp);
+    return out;
+}
+
+name::sep::sep(name const & n, char const * s):m_name(n), m_sep(s) {}
+
+std::ostream & operator<<(std::ostream & out, name::sep const & s) {
+    name::imp::display(out, s.m_sep, s.m_name.m_imp);
+    return out;
+}
+
+}

src/util/name.h

@@ -0,0 +1,58 @@
+/*
+Copyright (c) 2013 Microsoft Corporation. All rights reserved. 
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura 
+*/
+#pragma once
+#include <iostream>
+
+namespace lean {
+
+constexpr char const * default_name_separator = "::";
+
+/**
+   \brief Hierarchical names.
+*/
+class name {
+    enum class kind { ANONYMOUS, STRING, NUMERAL };
+    struct imp;
+    imp * m_imp;
+    name(imp * p);
+public:
+    name();
+    name(char const * name);
+    name(unsigned k);
+    name(name const & prefix, char const * name);
+    name(name const & prefix, unsigned k);
+    name(name const & other);
+    name(name && other);
+    ~name();
+    name & operator=(name const & other);
+    name & operator=(name && other);
+    bool operator==(name const & other) const;
+    bool operator!=(name const & other) const { return !operator==(other); }
+    kind get_kind() const;
+    bool is_anonymous() const { return get_kind() == kind::ANONYMOUS; }
+    bool is_string() const { return get_kind() == kind::STRING; }
+    bool is_numeral() const { return get_kind() == kind::NUMERAL; }
+    unsigned get_numeral() const;
+    char const * get_string() const;
+    bool is_atomic() const;
+    name get_prefix() const;
+    /**
+       \brief Size of the this name (in characters) when using the given separator.
+    */
+    size_t size(char const * sep = default_name_separator) const;
+    friend std::ostream & operator<<(std::ostream & out, name const & n);
+    class sep {
+        name const & m_name;
+        char const * m_sep;
+    public:
+        sep(name const & n, char const * s);
+        friend std::ostream & operator<<(std::ostream & out, sep const & s);
+    };
+    friend std::ostream & operator<<(std::ostream & out, sep const & s);
+};
+
+}

src/util/trace.cpp

@@ -0,0 +1,42 @@
+/*
+Copyright (c) 2013 Microsoft Corporation. All rights reserved. 
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura 
+*/
+
+#include "trace.h"
+#include <set>
+#include <string>
+#include <memory>
+
+#ifndef LEAN_TRACE_OUT
+#define LEAN_TRACE_OUT ".lean_trace"
+#endif  
+
+namespace lean {
+
+#ifdef LEAN_TRACE
+std::ofstream tout(LEAN_TRACE_OUT);
+std::mutex    trace_mutex;
+#endif
+    
+static std::unique_ptr<std::set<std::string>> g_enabled_trace_tags;
+
+void enable_trace(char const * tag) {
+    if (!g_enabled_trace_tags)
+        g_enabled_trace_tags.reset(new std::set<std::string>());
+    g_enabled_trace_tags->insert(tag);
+}
+
+void disable_trace(char const * tag) {
+    if (g_enabled_trace_tags) 
+        g_enabled_trace_tags->erase(tag);
+}
+
+bool is_trace_enabled(char const * tag) {
+    return g_enabled_trace_tags && g_enabled_trace_tags->find(tag) != g_enabled_trace_tags->end();
+}
+
+}
+

src/util/trace.h

@@ -0,0 +1,31 @@
+/*
+Copyright (c) 2013 Microsoft Corporation. All rights reserved. 
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura 
+*/
+#pragma once
+
+#ifdef LEAN_TRACE
+#include <fstream>
+#include <mutex>
+namespace lean {
+extern std::ofstream tout; 
+extern std::mutex    trace_mutex;
+}
+#define TRACE_CODE(CODE) { std::lock_guard<std::mutex> _lean_trace_lock_(lean::trace_mutex); CODE }
+#else
+#define TRACE_CODE(CODE) 
+#endif
+
+#define lean_trace(TAG, CODE) TRACE_CODE(if (lean::is_trace_enabled(TAG)) { lean::tout << "-------- [" << TAG << "] " << __FUNCTION__ << " " << __FILE__ << ":" << __LINE__ << " ---------\n"; CODE lean::tout << "------------------------------------------------\n"; lean::tout.flush(); })
+
+#define lean_simple_trace(TAG, CODE) TRACE_CODE(if (lean::is_trace_enabled(TAG)) { CODE lean::tout.flush(); })
+
+#define lean_cond_trace(TAG, COND, CODE) TRACE_CODE(if (lean::is_trace_enabled(TAG) && (COND)) { lean::tout << "-------- [" << TAG << "] " << __FUNCTION__ << " " << __FILE__ << ":" << __LINE__ << " ---------\n"; CODE lean::tout << "------------------------------------------------\n"; lean::tout.flush(); })
+
+namespace lean {
+void enable_trace(char const * tag);
+void disable_trace(char const * tag);
+bool is_trace_enabled(char const * tag);
+}