feat(kernel/universe_constraints): add new class for managing universe constraints

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

src/kernel/CMakeLists.txt

@@ -3,6 +3,7 @@ add_library(kernel expr.cpp free_vars.cpp abstract.cpp instantiate.cpp
   type_checker.cpp builtin.cpp occurs.cpp metavar.cpp
   justification.cpp unification_constraint.cpp kernel_exception.cpp
   type_checker_justification.cpp pos_info_provider.cpp
-  replace_visitor.cpp update_expr.cpp io_state.cpp max_sharing.cpp)
+  replace_visitor.cpp update_expr.cpp io_state.cpp max_sharing.cpp
+  universe_constraints.cpp)
 
 target_link_libraries(kernel ${LEAN_LIBS})

src/kernel/universe_constraints.cpp

@@ -0,0 +1,77 @@
+/*
+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 "util/safe_arith.h"
+#include "util/pair.h"
+#include "util/buffer.h"
+#include "kernel/universe_constraints.h"
+
+namespace lean {
+optional<int> universe_constraints::get_distance(name const & n1, name const & n2) const {
+    auto it = m_distances.find(mk_pair(n1, n2));
+    if (it != m_distances.end())
+        return optional<int>(it->second);
+    else
+        return optional<int>();
+}
+
+void universe_constraints::add_var(name const & n) {
+    lean_assert(!get_distance(n, n));
+    m_distances[mk_pair(n, n)] = 0;
+    m_outgoing_edges[n].emplace_back(n, 0);
+    m_incoming_edges[n].emplace_back(n, 0);
+}
+
+bool universe_constraints::contains(name const & n) const {
+    return static_cast<bool>(get_distance(n, n));
+}
+
+bool universe_constraints::is_implied(name const & n1, name const & n2, int k) const {
+    auto d = get_distance(n1, n2);
+    return d && *d >= k;
+}
+
+bool universe_constraints::is_consistent(name const & n1, name const & n2, int k) const {
+    // we just check if n2 >= n1 - k + 1 is not implied
+    return !is_implied(n2, n1, safe_add(safe_sub(0, k), 1));
+}
+
+/**
+    \brief Add the pair (n, k) to entries if it does not contain an entry (n, k').
+    Otherwise, replace entry (n, k') with (n, k).
+*/
+static void updt_entry(std::vector<std::pair<name, int>> & entries, name const & n, int k) {
+    auto it = std::find_if(entries.begin(), entries.end(), [&](std::pair<name, int> const & p) { return p.first == n; });
+    if (it == entries.end())
+        entries.emplace_back(n, k);
+    else
+        it->second = k;
+}
+
+void universe_constraints::add_constraint(name const & n1, name const & n2, int k) {
+    lean_assert(contains(n1));
+    lean_assert(contains(n2));
+    lean_assert(is_consistent(n1, n2, k));
+    if (is_implied(n1, n2, k))
+        return; // redundant
+    buffer<std::tuple<name, name, int>> to_add;
+    for (auto const & in : m_incoming_edges[n1])
+        to_add.emplace_back(in.first, n2, safe_add(in.second, k));
+    for (auto const & out : m_outgoing_edges[n2])
+        to_add.emplace_back(n1, out.first, safe_add(out.second, k));
+    for (auto const & e : to_add) {
+        name const & from = std::get<0>(e);
+        name const & to   = std::get<1>(e);
+        int new_k         = std::get<2>(e);
+        auto old_k        = get_distance(from, to);
+        if (!old_k || new_k > *old_k) {
+            updt_entry(m_outgoing_edges[from], to, new_k);
+            updt_entry(m_incoming_edges[to], from, new_k);
+            m_distances[mk_pair(from, to)] = new_k;
+        }
+    }
+}
+}

src/kernel/universe_constraints.h

@@ -0,0 +1,65 @@
+/*
+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 <unordered_map>
+#include "util/name.h"
+#include "util/hash.h"
+#include "util/name_map.h"
+#include "util/optional.h"
+
+namespace lean {
+/**
+   \brief Store the set of universe constraints.
+
+   It is based on Floyd-Warshall all-pairs shortest path algorithm.
+*/
+class universe_constraints {
+    typedef std::pair<name, int> edge;
+    typedef std::vector<edge> edges;
+    typedef name_map<edges> node_to_edges;
+    typedef std::pair<name, name> name_pair;
+    struct name_pair_hash_fn {
+        unsigned operator()(name_pair const & p) const { return hash(p.first.hash(), p.second.hash()); }
+    };
+    typedef std::unordered_map<name_pair, int, name_pair_hash_fn, std::equal_to<name_pair>> distances;
+    node_to_edges m_incoming_edges;
+    node_to_edges m_outgoing_edges;
+    distances     m_distances;
+public:
+    /**
+       \brief Add a new variable.
+
+       \pre The variables does not exist in this set of constraints.
+    */
+    void add_var(name const & n);
+    /**
+       \brief Return true iff this set of constraints contains the variable n.
+       That is, it was added using add_var.
+    */
+    bool contains(name const & n) const;
+    /** \brief Return true iff n1 >= n2 + k is implied by this set of constraints. */
+    bool is_implied(name const & n1, name const & n2, int k) const ;
+    /** \brief Return true iff n1 < n2 + k is not implied by this set of constraints. */
+    bool is_consistent(name const & n1, name const & n2, int k) const;
+    /**
+        \brief Add new constraint n1 >= n2 + k.
+
+        \pre is_consistent(n1, n2, k)
+        \pre contains(n1)
+        \pre contains(n2)
+    */
+    void add_constraint(name const & n1, name const & n2, int k);
+    /**
+       \brief Return the "distance" between n1 and n2.
+       That is, the best k s.t. n1 >= n2 + k is implied by this set of constraints
+       but n1 >= n2 + k + i is not for any i > 0.
+
+       If there is no such k, then return none.
+    */
+    optional<int> get_distance(name const & n1, name const & n2) const;
+};
+}

src/tests/kernel/CMakeLists.txt

@@ -36,3 +36,6 @@ set_tests_properties(metavar PROPERTIES ENVIRONMENT "LEAN_PATH=${LEAN_BINARY_DIR
 add_executable(instantiate instantiate.cpp)
 target_link_libraries(instantiate ${EXTRA_LIBS})
 add_test(instantiate ${CMAKE_CURRENT_BINARY_DIR}/instantiate)
+add_executable(universe_constraints universe_constraints.cpp)
+target_link_libraries(universe_constraints ${EXTRA_LIBS})
+add_test(universe_constraints ${CMAKE_CURRENT_BINARY_DIR}/universe_constraints)

src/tests/kernel/universe_constraints.cpp

@@ -0,0 +1,47 @@
+/*
+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 "util/test.h"
+#include "kernel/universe_constraints.h"
+using namespace lean;
+
+static void tst1() {
+    universe_constraints uc;
+    name a("a"), b("b"), c("c"), d("d");
+    uc.add_var(a); uc.add_var(b); uc.add_var(c); uc.add_var(d);
+    lean_assert(*(uc.get_distance(a, a)) == 0);
+    lean_assert(!uc.get_distance(a, b));
+    uc.add_constraint(a, b, 1);
+    lean_assert(uc.is_consistent(a, b, 1));
+    lean_assert(*(uc.get_distance(a, b)) == 1);
+    uc.add_constraint(a, c, 1);
+    lean_assert(uc.is_consistent(b, c, 1));
+    lean_assert(*(uc.get_distance(a, c)) == 1);
+    lean_assert(uc.is_implied(a, c, 1));
+    lean_assert(!uc.is_implied(a, c, 2));
+    lean_assert(uc.is_implied(a, c, 0));
+    lean_assert(!uc.is_implied(b, c, 0));
+    lean_assert(!uc.is_implied(a, d, 3));
+    lean_assert(uc.is_consistent(a, d, 2));
+    lean_assert(uc.is_consistent(c, d, 1));
+    uc.add_constraint(c, d, 1);
+    lean_assert(*(uc.get_distance(a, d)) == 2);
+    lean_assert(uc.is_implied(a, d, 2));
+    lean_assert(!uc.is_implied(a, d, 3));
+    uc.add_constraint(b, d, 2);
+    lean_assert(*(uc.get_distance(a, d)) == 3);
+    lean_assert(uc.is_implied(a, d, 3));
+    lean_assert(!uc.is_consistent(d, a, 0));
+    lean_assert(!uc.is_consistent(d, a, -2));
+    lean_assert(uc.is_consistent(d, a, -3));
+}
+
+int main() {
+    save_stack_info();
+    tst1();
+    return has_violations() ? 1 : 0;
+}
+