From 76b1ddb967b57be5bd0bf7c255f2ba85c3da5359 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 14 Feb 2014 14:29:33 -0800 Subject: [PATCH] feat(kernel): add difference constraint solver with backtracking support, and justification generation, this solver will be used to check the satisfiability of universe level constraints Signed-off-by: Leonardo de Moura --- src/kernel/CMakeLists.txt | 2 +- src/kernel/diff_cnstrs.cpp | 325 +++++++++++++++++++++++++++++++ src/kernel/diff_cnstrs.h | 122 ++++++++++++ src/tests/kernel/CMakeLists.txt | 9 +- src/tests/kernel/diff_cnstrs.cpp | 56 ++++++ 5 files changed, 510 insertions(+), 4 deletions(-) create mode 100644 src/kernel/diff_cnstrs.cpp create mode 100644 src/kernel/diff_cnstrs.h create mode 100644 src/tests/kernel/diff_cnstrs.cpp diff --git a/src/kernel/CMakeLists.txt b/src/kernel/CMakeLists.txt index f4352fd02..1299b396a 100644 --- a/src/kernel/CMakeLists.txt +++ b/src/kernel/CMakeLists.txt @@ -1,4 +1,4 @@ -add_library(kernel level.cpp +add_library(kernel level.cpp diff_cnstrs.cpp # expr.cpp # free_vars.cpp abstract.cpp instantiate.cpp # normalizer.cpp context.cpp level.cpp object.cpp environment.cpp diff --git a/src/kernel/diff_cnstrs.cpp b/src/kernel/diff_cnstrs.cpp new file mode 100644 index 000000000..6073402a7 --- /dev/null +++ b/src/kernel/diff_cnstrs.cpp @@ -0,0 +1,325 @@ +/* +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 +#include +#include +#include +#include "util/hash.h" +#include "util/safe_arith.h" +#include "kernel/diff_cnstrs.h" + +namespace lean { + +struct diff_cnstrs::imp { + typedef int edge_id; + static constexpr edge_id null_edge_id = -1; + + struct edge_jst { + bool m_propagation; + union { + justification m_asserted; + edge_id m_implied_by; + }; + edge_jst():m_propagation(false), m_asserted(nullptr) {} + edge_jst(justification jst):m_propagation(false), m_asserted(jst) {} + edge_jst(edge_id e_id):m_propagation(true), m_implied_by(e_id) {} + }; + + struct edge { + node m_source; + node m_target; + distance m_distance; + edge_jst m_justification; + edge(node s, node t, distance d, edge_jst const & j): + m_source(s), m_target(t), m_distance(d), m_justification(j) {} + }; + + enum class trail_kind { MkNode, AddEdge, DisableNode }; + + struct trail { + trail_kind m_kind; + union { + edge_id m_old_edge_id; + node m_disabled_node; // node that was disabled + }; + trail(trail_kind k):m_kind(k) {} + }; + + typedef std::pair node_pair; + struct node_pair_hash { unsigned operator()(node_pair const & p) const { return hash(p.first, p.second); } }; + typedef std::unordered_map, edge_id, node_pair_hash, std::equal_to> distances; + typedef std::vector edge_ids; + + new_eq_eh m_eh; + std::vector m_edges; // vector/trail of all edges + std::vector m_enabled; // map node -> bool + std::vector m_incoming_edges; // map node -> incoming edges + std::vector m_outgoing_edges; // map node -> outgoing edges + distances m_distances; // map node*node -> edge + std::vector m_trail_stack; // trail/undo stack + std::vector m_scopes; + + imp(new_eq_eh const & eh):m_eh(eh) {} + + imp(imp const & s, new_eq_eh const & eh): + m_eh(eh), + m_edges(s.m_edges), + m_enabled(s.m_enabled), + m_incoming_edges(s.m_incoming_edges), + m_outgoing_edges(s.m_outgoing_edges), + m_distances(s.m_distances) { + // the trail (aka backtracking stack) is not copied + } + + void push_mk_node_trail() { + m_trail_stack.push_back(trail(trail_kind::MkNode)); + } + + void push_new_edge_trail(edge_id old_edge = null_edge_id) { + trail t(trail_kind::AddEdge); + t.m_old_edge_id = old_edge; + m_trail_stack.push_back(t); + } + + void push_disable_node_trail(node n) { + trail t(trail_kind::DisableNode); + t.m_disabled_node = n; + m_trail_stack.push_back(t); + } + + void undo_mk_node() { + lean_assert(!m_enabled.empty()); + lean_assert(!m_incoming_edges.empty()); + lean_assert(!m_outgoing_edges.empty()); + lean_assert(m_incoming_edges.back().empty()); + lean_assert(m_outgoing_edges.back().empty()); + m_incoming_edges.pop_back(); + m_outgoing_edges.pop_back(); + m_enabled.pop_back(); + } + + void undo_disable_node(node n) { + lean_assert(n < m_enabled.size()); + lean_assert(!m_enabled[n]); + m_enabled[n] = true; + } + + void undo_add_edge(edge_id old_e_id) { + lean_assert(!m_edges.empty()); + edge_id e_id = m_edges.size() - 1; + auto & e = m_edges.back(); + node s = e.m_source; + node t = e.m_target; + auto & out = m_outgoing_edges[s]; + auto & in = m_incoming_edges[t]; + lean_assert_eq(m_distances[node_pair(s, t)], e_id); + if (old_e_id == null_edge_id) { + m_distances.erase(node_pair(s, t)); + in.erase(std::remove(in.begin(), in.end(), e_id), in.end()); + out.erase(std::remove(out.begin(), out.end(), e_id), out.end()); + } else { + m_distances[node_pair(s, t)] = old_e_id; + std::replace(in.begin(), in.end(), e_id, old_e_id); + std::replace(out.begin(), out.end(), e_id, old_e_id); + } + m_edges.pop_back(); + } + + void push() { + m_scopes.push_back(m_trail_stack.size()); + } + + void pop(unsigned num_scopes) { + unsigned lvl = m_scopes.size(); + lean_assert(num_scopes <= lvl); + unsigned new_lvl = lvl - num_scopes; + unsigned old_trail_sz = m_scopes[new_lvl]; + unsigned i = m_trail_stack.size(); + while (i > old_trail_sz) { + --i; + trail const & t = m_trail_stack.back(); + switch (t.m_kind) { + case trail_kind::MkNode: undo_mk_node(); break; + case trail_kind::AddEdge: undo_add_edge(t.m_old_edge_id); break; + case trail_kind::DisableNode: undo_disable_node(t.m_disabled_node); break; + } + m_trail_stack.pop_back(); + } + lean_assert(m_trail_stack.size() == old_trail_sz); + m_scopes.resize(new_lvl); + } + + void disable_node(node n) { + lean_assert(n < m_enabled.size()); + lean_assert(m_enabled[n]); + m_enabled[n] = false; + push_disable_node_trail(n); + } + + bool is_enabled(node n) const { + lean_assert(n < m_enabled.size()); + return m_enabled[n]; + } + + optional get_distance(node s, node t) const { + auto it = m_distances.find(node_pair(s, t)); + if (it == m_distances.end()) + return optional(); + else + return optional(m_edges[it->second].m_distance); + } + + bool is_implied(node s, node t, distance d) const { + auto d1 = get_distance(s, t); + return d1 && *d1 >= d; + } + + bool is_consistent(node s, node t, distance d) const { + // we just check if t >= s - d + 1 is not implied + return !is_implied(t, s, safe_sub(1, d)); + } + + void check_new_eq(edge const & e) { + if (e.m_distance == 0 && e.m_source != e.m_target) { + auto d = get_distance(e.m_target, e.m_source); + if (d && *d == 0) { + // new implied equality + m_eh(e.m_source, e.m_target); + } + } + } + + bool add_edge_core(edge const & e) { + node s = e.m_source; + node t = e.m_target; + auto it = m_distances.find(node_pair(s, t)); + if (it == m_distances.end()) { + edge_id e_id = m_edges.size(); + m_edges.push_back(e); + m_distances[node_pair(s, t)] = e_id; + m_incoming_edges[t].push_back(e_id); + m_outgoing_edges[s].push_back(e_id); + push_new_edge_trail(null_edge_id); + check_new_eq(e); + return true; + } else { + edge_id old_e_id = it->second; + distance d = e.m_distance; + if (d > m_edges[old_e_id].m_distance) { + edge_id e_id = m_edges.size(); + m_edges.push_back(e); + it->second = e_id; + auto & in = m_incoming_edges[t]; + auto & out = m_outgoing_edges[s]; + std::replace(in.begin(), in.end(), old_e_id, e_id); + std::replace(out.begin(), out.end(), old_e_id, e_id); + push_new_edge_trail(old_e_id); + check_new_eq(e); + return true; + } else { + return false; // redundant edge + } + } + } + + bool add_edge_core(node s, node t, distance d, edge_jst const & j) { + return add_edge_core(edge(s, t, d, j)); + } + + node mk_node() { + node n = m_enabled.size(); + m_enabled.push_back(true); + m_incoming_edges.push_back(edge_ids()); + m_outgoing_edges.push_back(edge_ids()); + push_mk_node_trail(); + add_edge_core(n, n, 0, edge_jst()); + lean_assert(*get_distance(n, n) == 0); + return n; + } + + void add_edge(node s, node t, distance d, justification j) { + lean_assert(is_enabled(s)); + lean_assert(is_enabled(t)); + lean_assert(is_consistent(s, t, d)); + if (is_implied(s, t, d)) + return; // redundant + edge_id new_e_id = m_edges.size(); + edge_jst prop_jst(new_e_id); + buffer to_add; + to_add.push_back(edge(s, t, d, edge_jst(j))); + for (auto in_id : m_incoming_edges[s]) { + edge & e = m_edges[in_id]; + if (is_enabled(e.m_source) && e.m_source != s) + to_add.emplace_back(e.m_source, t, safe_add(e.m_distance, d), prop_jst); + } + for (auto out_id : m_outgoing_edges[t]) { + edge & e = m_edges[out_id]; + if (is_enabled(e.m_target) && t != e.m_target) + to_add.emplace_back(s, e.m_target, safe_add(e.m_distance, d), prop_jst); + } + for (auto const & e : to_add) { + auto old_d = get_distance(e.m_source, e.m_target); + if (!old_d || e.m_distance > *old_d) + add_edge_core(e); + } + } + + void explain(node s, node t, buffer & js) const { + if (s != t) { + buffer todo; + todo.push_back(node_pair(s, t)); + while (!todo.empty()) { + node s = todo.back().first; + node t = todo.back().second; + edge_id e_id = m_distances.find(todo.back())->second; + todo.pop_back(); + edge const & e = m_edges[e_id]; + edge_jst j = e.m_justification; + if (!j.m_propagation && j.m_asserted != nullptr) { + js.push_back(j.m_asserted); + } else { + edge const & e1 = m_edges[j.m_implied_by]; + if (e1.m_source != e1.m_target) + todo.push_back(node_pair(e1.m_source, e1.m_target)); + if (s != e1.m_source) + todo.push_back(node_pair(s, e1.m_source)); + if (e1.m_target != t) + todo.push_back(node_pair(e1.m_target, t)); + } + } + } + } + + void display(std::ostream & out) const { + for (node n = 0; n < m_outgoing_edges.size(); n++) { + if (is_enabled(n)) { + for (edge_id e_id : m_outgoing_edges[n]) { + auto const & e = m_edges[e_id]; + lean_assert(e.m_source == n); + if (e.m_target != n && is_enabled(e.m_target)) + out << "n" << n << " + " << e.m_distance << " <= n" << e.m_target << "\n"; + } + } + } + } +}; + +diff_cnstrs::diff_cnstrs(new_eq_eh const & eh):m_ptr(new imp(eh)) {} +diff_cnstrs::diff_cnstrs(diff_cnstrs const & s, new_eq_eh const & eh):m_ptr(new imp(*s.m_ptr, eh)) {} +diff_cnstrs::~diff_cnstrs() {} +diff_cnstrs::node diff_cnstrs::mk_node() { return m_ptr->mk_node(); } +void diff_cnstrs::add_edge(node s, node t, distance d, justification j) { m_ptr->add_edge(s, t, d, j); } +void diff_cnstrs::disable_node(node n) { m_ptr->disable_node(n); } +void diff_cnstrs::push() { m_ptr->push(); } +void diff_cnstrs::pop(unsigned num_scopes) { m_ptr->pop(num_scopes); } +optional diff_cnstrs::get_distance(node s, node t) const { return m_ptr->get_distance(s, t); } +bool diff_cnstrs::is_enabled(node n) const { return m_ptr->is_enabled(n); } +void diff_cnstrs::explain(node s, node t, buffer & js) const { m_ptr->explain(s, t, js); } +bool diff_cnstrs::is_implied(node s, node t, distance d) const { return m_ptr->is_implied(s, t, d); } +bool diff_cnstrs::is_consistent(node s, node t, distance d) const { return m_ptr->is_consistent(s, t, d); } +void diff_cnstrs::display(std::ostream & out) const { m_ptr->display(out); } +} diff --git a/src/kernel/diff_cnstrs.h b/src/kernel/diff_cnstrs.h new file mode 100644 index 000000000..4efdb0dcc --- /dev/null +++ b/src/kernel/diff_cnstrs.h @@ -0,0 +1,122 @@ +/* +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 +#include "util/optional.h" +#include "util/buffer.h" + +namespace lean { +class diff_cnstrs { + struct imp; + std::unique_ptr m_ptr; +public: + typedef unsigned node; + /** + \brief The justifications are "opaque" to this module. + From the point of view of this module, they are just markers. + */ + typedef void * justification; + typedef int distance; + /** + \brief Event handler for implied equalities. + */ + typedef std::function new_eq_eh; + /** + \brief Create an empty set of constraints. The "customer" can provide + an event handler that will be invoked whenever an equality between two nodes + is inferred. + */ + diff_cnstrs(new_eq_eh const & eh = [](node, node) {}); + diff_cnstrs(diff_cnstrs const & s, new_eq_eh const & eh = [](node, node) {}); + ~diff_cnstrs(); + + + /** + \brief Create a new node. + */ + node mk_node(); + + /** + \brief Disable a node created using \c mk_node. + + \remark We cannot add edges between disabled nodes. + + \pre is_enabled(n) + */ + void disable_node(node n); + + /** + \brief Return true iff the given node is enabled. + */ + bool is_enabled(node n) const; + + /** + \brief Add an edge s -d-> t with justification \c j. + The edge can be viewed as an inequality s + d <= t. + + \remark This method assumes that the new edge would not produce + a "positive cycle". A positive cycle in the graph is an "inconsistency" + of the form k <= 0, where \c k is a positive number. + + \pre is_consistent(s, t, d) + \pre is_enabled(s) + \pre is_enabled(t) + */ + void add_edge(node s, node t, distance d, justification j); + + /** + \brief Create a backtracking point. + */ + void push(); + + /** + \brief Restore backtracking point. This method undoes the \c mk_node, + \c disable_node and \c add_edge operations between + this call and the matching \c push. + */ + void pop(unsigned num_scopes = 1); + + /** + \brief Return the distance between \c s and \c t. + If the result is none, then the distance is "infinite", i.e., + there is no path between \c s and \c t. + + The distance \c d between \c s and \c t can be viewed as + an inequality s + d <= t, and this is the "best" + inequality implied by the already added edges. By best, + we mean, forall d1 > d, !is_implied(s, t, d1) + */ + optional get_distance(node s, node t) const; + + /** + \brief Return true iff the already added edges imply + that distance between \c s and \c t is at least \c d + */ + bool is_implied(node s, node t, distance d) const; + + /** + \brief Return true iff by adding the edge s -d-> t we don't + create a positive cycle. + This method is equivalent to !is_implied(t, s, 1-d) + */ + bool is_consistent(node s, node t, distance d) const; + + /** + \brief Return a "justification" for get_distance(s, t). + The distance is implied by a subset of edges added using + \c add_edge. This method collect the justification for each one + of theses edges in \c js. + */ + void explain(node s, node t, buffer & js) const; + + /** + \brief Display the distances between all ones. This used only + for debugging purposes. + */ + void display(std::ostream & out) const; +}; +} diff --git a/src/tests/kernel/CMakeLists.txt b/src/tests/kernel/CMakeLists.txt index b6bdbe9e6..846efb4ab 100644 --- a/src/tests/kernel/CMakeLists.txt +++ b/src/tests/kernel/CMakeLists.txt @@ -1,3 +1,9 @@ +add_executable(level level.cpp) +target_link_libraries(level ${EXTRA_LIBS}) +add_test(level ${CMAKE_CURRENT_BINARY_DIR}/level) +add_executable(diff_cnstrs diff_cnstrs.cpp) +target_link_libraries(diff_cnstrs ${EXTRA_LIBS}) +add_test(diff_cnstrs ${CMAKE_CURRENT_BINARY_DIR}/diff_cnstrs) # add_executable(expr expr.cpp) # target_link_libraries(expr ${EXTRA_LIBS}) # add_test(expr ${CMAKE_CURRENT_BINARY_DIR}/expr) @@ -12,9 +18,6 @@ # add_executable(free_vars free_vars.cpp) # target_link_libraries(free_vars ${EXTRA_LIBS}) # add_test(free_vars ${CMAKE_CURRENT_BINARY_DIR}/free_vars) -add_executable(level level.cpp) -target_link_libraries(level ${EXTRA_LIBS}) -add_test(level ${CMAKE_CURRENT_BINARY_DIR}/level) # add_executable(replace replace.cpp) # target_link_libraries(replace ${EXTRA_LIBS}) # add_test(replace ${CMAKE_CURRENT_BINARY_DIR}/replace) diff --git a/src/tests/kernel/diff_cnstrs.cpp b/src/tests/kernel/diff_cnstrs.cpp new file mode 100644 index 000000000..51fe5b082 --- /dev/null +++ b/src/tests/kernel/diff_cnstrs.cpp @@ -0,0 +1,56 @@ +/* +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/diff_cnstrs.h" +using namespace lean; +typedef diff_cnstrs::node node; +static void tst1() { + diff_cnstrs c([](node n1, node n2) { std::cout << "New equality: n" << n1 << " n" << n2 << "\n";}); + node n0 = c.mk_node(); + node n1 = c.mk_node(); + node n2 = c.mk_node(); + int j1; int j2; + c.add_edge(n0, n1, 10, &j1); + c.display(std::cout); + std::cout << "====\n"; + c.add_edge(n1, n2, 20, &j2); + c.push(); + c.display(std::cout); + node n3 = c.mk_node(); + node n4 = c.mk_node(); + int j3, j4, j5; + c.add_edge(n2, n3, 0, &j3); + c.add_edge(n3, n4, 0, &j4); + c.add_edge(n4, n2, 0, &j5); + std::cout << "====\n"; + c.display(std::cout); + buffer js; + c.explain(n2, n4, js); + lean_assert(js.size() == 2); + lean_assert(js[0] == &j3 || js[0] == &j4); + lean_assert(js[1] == &j3 || js[1] == &j4); + lean_assert(c.is_implied(n1, n4, 10)); + lean_assert(c.is_consistent(n1, n4, 100)); + lean_assert(!c.is_consistent(n4, n1, 0)); + c.disable_node(n1); + lean_assert(c.is_enabled(n0)); + lean_assert(!c.is_enabled(n1)); + node n5 = c.mk_node(); + c.add_edge(n2, n5, 100, &j5); + std::cout << "====\n"; + c.display(std::cout); + c.pop(); + std::cout << "====\n"; + c.display(std::cout); +} + +int main() { + save_stack_info(); + tst1(); + return has_violations() ? 1 : 0; +} +