From 3125c19049d441de58943fa4556aca55bc52bcc5 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 24 Mar 2019 18:44:46 -0700 Subject: [PATCH 01/19] add sr Signed-off-by: Nikolaj Bjorner --- src/ast/CMakeLists.txt | 1 + src/ast/special_relations_decl_plugin.cpp | 79 ++ src/ast/special_relations_decl_plugin.h | 97 +++ src/smt/CMakeLists.txt | 1 + src/smt/diff_logic.h | 148 +++- src/smt/theory_special_relations.cpp | 905 ++++++++++++++++++++++ src/smt/theory_special_relations.h | 198 +++++ 7 files changed, 1413 insertions(+), 16 deletions(-) create mode 100644 src/ast/special_relations_decl_plugin.cpp create mode 100644 src/ast/special_relations_decl_plugin.h create mode 100644 src/smt/theory_special_relations.cpp create mode 100644 src/smt/theory_special_relations.h diff --git a/src/ast/CMakeLists.txt b/src/ast/CMakeLists.txt index 56ab78b8a..0bcc4d847 100644 --- a/src/ast/CMakeLists.txt +++ b/src/ast/CMakeLists.txt @@ -41,6 +41,7 @@ z3_add_component(ast reg_decl_plugins.cpp seq_decl_plugin.cpp shared_occs.cpp + special_relations_decl_plugin.cpp static_features.cpp used_vars.cpp well_sorted.cpp diff --git a/src/ast/special_relations_decl_plugin.cpp b/src/ast/special_relations_decl_plugin.cpp new file mode 100644 index 000000000..6bb5734e5 --- /dev/null +++ b/src/ast/special_relations_decl_plugin.cpp @@ -0,0 +1,79 @@ +/*++ +Copyright (c) 2015 Microsoft Corporation + +Module Name: + + special_relations_decl_plugin.cpp + +Abstract: + + + +Author: + + Nikolaj Bjorner (nbjorner) 2015-15-9. + +Revision History: + +--*/ + +#include +#include"ast.h" +#include"special_relations_decl_plugin.h" + + + +special_relations_decl_plugin::special_relations_decl_plugin(): + m_lo("linear-order"), + m_po("partial-order"), + m_po_ao("partial-order-already-ordered"), + m_plo("piecewise-linear-order"), + m_to("tree-order") +{} + +func_decl * special_relations_decl_plugin::mk_func_decl( + decl_kind k, unsigned num_parameters, parameter const * parameters, + unsigned arity, sort * const * domain, sort * range) +{ + if (arity != 2) { + m_manager->raise_exception("special relations should have arity 2"); + return 0; + } + if (domain[0] != domain[1]) { + m_manager->raise_exception("argument sort missmatch"); + return 0; + } + func_decl_info info(m_family_id, k, num_parameters, parameters); + symbol name; + switch(k) { + case OP_SPECIAL_RELATION_PO: name = m_po; break; + case OP_SPECIAL_RELATION_PO_AO: name = m_po_ao; break; + case OP_SPECIAL_RELATION_LO: name = m_lo; break; + case OP_SPECIAL_RELATION_PLO: name = m_plo; break; + case OP_SPECIAL_RELATION_TO: name = m_to; break; + } + return m_manager->mk_func_decl(name, arity, domain, m_manager->mk_bool_sort(), info); +} + +void special_relations_decl_plugin::get_op_names(svector & op_names, symbol const & logic) { + if (logic == symbol::null) { + op_names.push_back(builtin_name(m_po.bare_str(), OP_SPECIAL_RELATION_PO)); + op_names.push_back(builtin_name(m_po_ao.bare_str(), OP_SPECIAL_RELATION_PO_AO)); + op_names.push_back(builtin_name(m_lo.bare_str(), OP_SPECIAL_RELATION_LO)); + op_names.push_back(builtin_name(m_plo.bare_str(), OP_SPECIAL_RELATION_PLO)); + op_names.push_back(builtin_name(m_to.bare_str(), OP_SPECIAL_RELATION_TO)); + } +} + +sr_property special_relations_util::get_property(func_decl* f) const { + switch (f->get_decl_kind()) { + case OP_SPECIAL_RELATION_PO: return sr_po; + case OP_SPECIAL_RELATION_PO_AO: return sr_po; // still partial ordered + case OP_SPECIAL_RELATION_LO: return sr_lo; + case OP_SPECIAL_RELATION_PLO: return sr_plo; + case OP_SPECIAL_RELATION_TO: return sr_to; + default: + UNREACHABLE(); + return sr_po; + } +} diff --git a/src/ast/special_relations_decl_plugin.h b/src/ast/special_relations_decl_plugin.h new file mode 100644 index 000000000..068382b23 --- /dev/null +++ b/src/ast/special_relations_decl_plugin.h @@ -0,0 +1,97 @@ +/*++ +Copyright (c) 2015 Microsoft Corporation + +Module Name: + + special_relations_decl_plugin.h + +Abstract: + + + +Author: + + Nikolaj Bjorner (nbjorner) 2015-15-9. + Ashutosh Gupta 2016 + +Revision History: + +--*/ +#ifndef SPECIAL_RELATIONS_DECL_PLUGIN_H_ +#define SPECIAL_RELATIONS_DECL_PLUGIN_H_ + +#include"ast.h" + + + +enum special_relations_op_kind { + OP_SPECIAL_RELATION_LO, + OP_SPECIAL_RELATION_PO, + OP_SPECIAL_RELATION_PO_AO, + OP_SPECIAL_RELATION_PLO, + OP_SPECIAL_RELATION_TO, + LAST_SPECIAL_RELATIONS_OP +}; + +class special_relations_decl_plugin : public decl_plugin { + symbol m_lo; + symbol m_po; + symbol m_po_ao; + symbol m_plo; + symbol m_to; +public: + special_relations_decl_plugin(); + virtual ~special_relations_decl_plugin() {} + + virtual decl_plugin * mk_fresh() { + return alloc(special_relations_decl_plugin); + } + + virtual func_decl * mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters, + unsigned arity, sort * const * domain, sort * range); + + virtual void get_op_names(svector & op_names, symbol const & logic); + + + virtual sort * mk_sort(decl_kind k, unsigned num_parameters, parameter const * parameters) { return 0; } +}; + +enum sr_property { + sr_transitive = 0x01, // Rxy & Ryz -> Rxz + sr_reflexive = 0x02, // Rxx + sr_antisymmetric = 0x04, // Rxy & Ryx -> x = y + sr_lefttree = 0x08, // Ryx & Rzx -> Ryz | Rzy + sr_righttree = 0x10, // Rxy & Rxz -> Ryx | Rzy + sr_po = 0x01 | 0x02 | 0x04, // partial order + sr_lo = 0x01 | 0x02 | 0x04 | 0x08 | 0x10, // linear order + sr_plo = 0x01 | 0x02 | 0x04 | 0x20, // piecewise linear order + sr_to = 0x01 | 0x02 | 0x04 | 0x10, // right-tree +}; + +class special_relations_util { + ast_manager& m; + family_id m_fid; +public: + special_relations_util(ast_manager& m) : m(m), m_fid(m.get_family_id("special_relations")) {} + + bool is_special_relation(func_decl* f) const { return f->get_family_id() == m_fid; } + bool is_special_relation(app* e) const { return is_special_relation(e->get_decl()); } + sr_property get_property(func_decl* f) const; + sr_property get_property(app* e) const { return get_property(e->get_decl()); } + + bool is_lo(expr const * e) const { return is_app_of(e, m_fid, OP_SPECIAL_RELATION_LO); } + bool is_po(expr const * e) const { return is_app_of(e, m_fid, OP_SPECIAL_RELATION_PO); } + bool is_po_ao(expr const * e) const { return is_app_of(e, m_fid, OP_SPECIAL_RELATION_PO_AO); } + bool is_plo(expr const * e) const { return is_app_of(e, m_fid, OP_SPECIAL_RELATION_PLO); } + bool is_to(expr const * e) const { return is_app_of(e, m_fid, OP_SPECIAL_RELATION_TO); } + + app * mk_lo (expr * arg1, expr * arg2) { return m.mk_app( m_fid, OP_SPECIAL_RELATION_LO, arg1, arg2); } + app * mk_po (expr * arg1, expr * arg2) { return m.mk_app( m_fid, OP_SPECIAL_RELATION_PO, arg1, arg2); } + app * mk_po_ao (expr * arg1, expr * arg2) { return m.mk_app( m_fid, OP_SPECIAL_RELATION_PO_AO, arg1, arg2); } + app * mk_plo(expr * arg1, expr * arg2) { return m.mk_app( m_fid, OP_SPECIAL_RELATION_PLO, arg1, arg2); } + app * mk_to (expr * arg1, expr * arg2) { return m.mk_app( m_fid, OP_SPECIAL_RELATION_TO, arg1, arg2); } + +}; + + +#endif /* SPECIAL_RELATIONS_DECL_PLUGIN_H_ */ diff --git a/src/smt/CMakeLists.txt b/src/smt/CMakeLists.txt index 52d3a5943..adc348633 100644 --- a/src/smt/CMakeLists.txt +++ b/src/smt/CMakeLists.txt @@ -62,6 +62,7 @@ z3_add_component(smt theory_pb.cpp theory_recfun.cpp theory_seq.cpp + theory_special_relations.cpp theory_str.cpp theory_utvpi.cpp theory_wmaxsat.cpp diff --git a/src/smt/diff_logic.h b/src/smt/diff_logic.h index 44e858219..f3ce7fb13 100644 --- a/src/smt/diff_logic.h +++ b/src/smt/diff_logic.h @@ -296,6 +296,9 @@ public: numeral const& get_weight(edge_id id) const { return m_edges[id].get_weight(); } + edge_id_vector const& get_out_edges(dl_var v) const { return m_out_edges[v]; } + + edge_id_vector const& get_in_edges(dl_var v) const { return m_in_edges[v]; } private: // An assignment is almost feasible if all but edge with idt edge are feasible. @@ -661,6 +664,113 @@ public: } } + bool can_reach(dl_var src, dl_var dst) { + uint_set target, visited; + target.insert(dst); + return reachable(src, target, visited, dst); + } + + bool reachable(dl_var start, uint_set const& target, uint_set& visited, dl_var& dst) { + visited.reset(); + svector nodes; + nodes.push_back(start); + for (dl_var n : nodes) { + if (visited.contains(n)) continue; + visited.insert(n); + edge_id_vector & edges = m_out_edges[n]; + for (edge_id e_id : edges) { + edge & e = m_edges[e_id]; + if (e.is_enabled()) { + dst = e.get_target(); + if (target.contains(dst)) { + return true; + } + nodes.push_back(dst); + } + } + } + return false; + } + +private: + svector m_freq_hybrid; + int m_total_count = 0; + int m_run_counter = -1; + svector m_hybrid_visited, m_hybrid_parent; +public: + + template + bool find_path(dl_var source, dl_var target, unsigned timestamp, Functor & f) { + auto zero_edge = true; + unsigned bfs_head = 0; + int_vector bfs_todo; + int_vector dfs_todo; + m_hybrid_visited.resize(m_assignment.size(), m_run_counter++); + m_hybrid_parent.resize(m_assignment.size(), -1); + bfs_todo.push_back(source); + m_hybrid_parent[source] = -1; + m_hybrid_visited[source] = m_run_counter; + numeral gamma; + while (bfs_head < bfs_todo.size() || !dfs_todo.empty()) { + m_total_count++; + dl_var v; + if (!dfs_todo.empty()) { + v = dfs_todo.back(); + dfs_todo.pop_back(); + } + else { + v = bfs_todo[bfs_head++]; + } + + edge_id_vector & edges = m_out_edges[v]; + for (edge_id e_id : edges) { + edge & e = m_edges[e_id]; + SASSERT(e.get_source() == v); + if (!e.is_enabled()) { + continue; + } + set_gamma(e, gamma); + if ((gamma.is_one() || (!zero_edge && gamma.is_neg())) + && e.get_timestamp() < timestamp) { + dl_var curr_target = e.get_target(); + if (curr_target == target) { + f(e.get_explanation()); + m_freq_hybrid[e_id]++; + for (;;) { + int p = m_hybrid_parent[v]; + if (p == -1) + return true; + + edge_id eid; + bool ret = get_edge_id(p, v, eid); + if (eid == null_edge_id || !ret) { + return true; + } + else { + edge & e = m_edges[eid]; + f(e.get_explanation()); + m_freq_hybrid[eid]++; + v = p; + } + } + } + else if (m_hybrid_visited[curr_target] != m_run_counter) { + if (m_freq_hybrid[e_id] > 1) { + dfs_todo.push_back(curr_target); + } + else { + bfs_todo.push_back(curr_target); + } + m_hybrid_visited[curr_target] = m_run_counter; + m_hybrid_parent[curr_target] = v; + } + } + } + } + return false; + + } + // // Create fresh literals obtained by resolving a pair (or more) // literals associated with the edges. @@ -1274,8 +1384,22 @@ public: // Find the shortest path from source to target using (normalized) zero edges with timestamp less than the given timestamp. // The functor f is applied on every explanation attached to the edges in the shortest path. // Return true if the path exists, false otherwise. + + + // Return true if the path exists, false otherwise. + template + bool find_shortest_zero_edge_path(dl_var source, dl_var target, unsigned timestamp, Functor & f) { + return find_shortest_path_aux(source, target, timestamp, f, true); + } + template - bool find_shortest_zero_edge_path(dl_var source, dl_var target, unsigned timestamp, Functor & f) { + bool find_shortest_reachable_path(dl_var source, dl_var target, unsigned timestamp, Functor & f) { + return find_shortest_path_aux(source, target, timestamp, f, false); + } + + + template + bool find_shortest_path_aux(dl_var source, dl_var target, unsigned timestamp, Functor & f, bool zero_edge) { svector bfs_todo; svector bfs_mark; bfs_mark.resize(m_assignment.size(), false); @@ -1292,10 +1416,7 @@ public: dl_var v = curr.m_var; TRACE("dl_bfs", tout << "processing: " << v << "\n";); edge_id_vector & edges = m_out_edges[v]; - typename edge_id_vector::iterator it = edges.begin(); - typename edge_id_vector::iterator end = edges.end(); - for (; it != end; ++it) { - edge_id e_id = *it; + for (edge_id e_id : edges) { edge & e = m_edges[e_id]; SASSERT(e.get_source() == v); if (!e.is_enabled()) { @@ -1303,7 +1424,8 @@ public: } set_gamma(e, gamma); TRACE("dl_bfs", tout << "processing edge: "; display_edge(tout, e); tout << "gamma: " << gamma << "\n";); - if (gamma.is_zero() && e.get_timestamp() < timestamp) { + if ((gamma.is_one() || (!zero_edge && gamma.is_neg())) && e.get_timestamp() < timestamp) { + // if (gamma.is_zero() && e.get_timestamp() < timestamp) dl_var curr_target = e.get_target(); TRACE("dl_bfs", tout << "curr_target: " << curr_target << ", mark: " << static_cast(bfs_mark[curr_target]) << "\n";); @@ -1477,11 +1599,7 @@ private: } TRACE("diff_logic", tout << "source: " << source << "\n";); - typename edge_id_vector::const_iterator it = edges[source].begin(); - typename edge_id_vector::const_iterator end = edges[source].end(); - - for (; it != end; ++it) { - edge_id e_id = *it; + for (edge_id e_id : edges[source]) { edge const& e = m_edges[e_id]; if (&e == &e_init) { @@ -1569,11 +1687,9 @@ private: tout << "\n"; }); - typename heap::const_iterator it = state.m_heap.begin(); - typename heap::const_iterator end = state.m_heap.end(); - for (; it != end; ++it) { - SASSERT(m_mark[*it] != DL_PROP_UNMARKED); - m_mark[*it] = DL_PROP_UNMARKED;; + for (auto & s : state.m_heap) { + SASSERT(m_mark[s] != DL_PROP_UNMARKED); + m_mark[s] = DL_PROP_UNMARKED;; } state.m_heap.reset(); SASSERT(marks_are_clear()); diff --git a/src/smt/theory_special_relations.cpp b/src/smt/theory_special_relations.cpp new file mode 100644 index 000000000..c58ffb24a --- /dev/null +++ b/src/smt/theory_special_relations.cpp @@ -0,0 +1,905 @@ +/*++ +Copyright (c) 2015 Microsoft Corporation + +Module Name: + + theory_special_relations.cpp + +Abstract: + + Special Relations theory plugin. + +Author: + + Nikolaj Bjorner (nbjorner) 2015-9-16 + Ashutosh Gupta 2016 + +Notes: + +--*/ + +#include + +#include "smt/smt_context.h" +#include "smt/theory_arith.h" +#include "smt/theory_special_relations.h" +#include "smt/smt_solver.h" +#include "solver/solver.h" +#include "ast/reg_decl_plugins.h" +#include "ast/ast_pp.h" + +static constexpr bool KVEC = false; +static constexpr bool HYBRID_SEARCH = false; + +namespace smt { + + void theory_special_relations::relation::push() { + m_scopes.push_back(scope()); + scope& s = m_scopes.back(); + s.m_asserted_atoms_lim = m_asserted_atoms.size(); + s.m_asserted_qhead_old = m_asserted_qhead; + if (!KVEC) { + m_graph.push(); + } + m_ufctx.get_trail_stack().push_scope(); + } + + void theory_special_relations::relation::pop(unsigned num_scopes) { + unsigned new_lvl = m_scopes.size() - num_scopes; + scope& s = m_scopes[new_lvl]; + m_asserted_atoms.shrink(s.m_asserted_atoms_lim); + m_asserted_qhead = s.m_asserted_qhead_old; + m_scopes.shrink(new_lvl); + if (!KVEC) { + m_graph.pop(num_scopes); + } + m_ufctx.get_trail_stack().pop_scope(num_scopes); + } + + void theory_special_relations::relation::ensure_var(theory_var v) { + while ((unsigned)v > m_uf.mk_var()); + if ((unsigned)v >= m_graph.get_num_nodes()) { + m_graph.init_var(v); + } + } + + bool theory_special_relations::relation::new_eq_eh(literal l, theory_var v1, theory_var v2) { + ensure_var(v1); + ensure_var(v2); + literal_vector ls; + ls.push_back(l); + return + m_graph.enable_edge(m_graph.add_edge(v1, v2, s_integer(1), ls)) && + m_graph.enable_edge(m_graph.add_edge(v2, v1, s_integer(1), ls)); + } + + theory_special_relations::theory_special_relations(ast_manager& m): + theory(m.mk_family_id("special_relations")), + m_util(m), m_autil(m) { + params_ref params; + params.set_bool("model", true); + params.set_bool("unsat_core", true); + m_nested_solver = mk_smt_solver(m, params, symbol("QF_LRA")); + m_int_sort = m_autil.mk_real(); + } + + theory_special_relations::~theory_special_relations() { + reset_eh(); + m_nested_solver = nullptr; + } + + theory * theory_special_relations::mk_fresh(context * new_ctx) { + return alloc(theory_special_relations, new_ctx->get_manager()); + } + + static void populate_k_vars(int v, int k, u_map>& map, int& curr_id, ast_manager& m, sort** int_sort) { + int need = !map.contains(v) ? k : k - map[v].size(); + for (auto i = 0; i < need; ++i) { + auto *fd = m.mk_func_decl(symbol(curr_id++), 0, int_sort, *int_sort); + map[v].push_back(m.mk_app(fd, unsigned(0), nullptr)); + } + } + + bool theory_special_relations::internalize_atom(app * atm, bool gate_ctx) { + TRACE("special_relations", tout << mk_pp(atm, get_manager()) << "\n";); + SASSERT(m_util.is_special_relation(atm)); + relation* r = 0; + if (!m_relations.find(atm->get_decl(), r)) { + //todo: push pop may get misaligned if the following alloc happens after push + r = alloc(relation, m_util.get_property(atm), atm->get_decl()); + m_relations.insert(atm->get_decl(), r); + } + context& ctx = get_context(); + expr* arg0 = atm->get_arg(0); + expr* arg1 = atm->get_arg(1); + theory_var v0 = mk_var(arg0); + theory_var v1 = mk_var(arg1); + bool_var v = ctx.mk_bool_var(atm); + ctx.set_var_theory(v, get_id()); + atom* a = alloc(atom, v, *r, v0, v1); + m_atoms.push_back(a); + //std::cerr << "INTER : " << a->v1() << ' ' << a->v2() << ' ' << gate_ctx << "\n"; + m_bool_var2atom.insert(v, a); + return true; + } + + theory_var theory_special_relations::mk_var(expr* e) { + context& ctx = get_context(); + if (!ctx.e_internalized(e)) { + ctx.internalize(e, false); + } + enode * n = ctx.get_enode(e); + theory_var v = n->get_th_var(get_id()); + if (null_theory_var == v) { + v = theory::mk_var(n); + ctx.attach_th_var(n, this, v); + } + return v; + } + + void theory_special_relations::new_eq_eh(theory_var v1, theory_var v2) { + context& ctx = get_context(); + app_ref eq(get_manager()); + app* t1 = get_enode(v1)->get_owner(); + app* t2 = get_enode(v2)->get_owner(); + eq = get_manager().mk_eq(t1, t2); + VERIFY(internalize_atom(eq, false)); + literal l(ctx.get_literal(eq)); + obj_map::iterator it = m_relations.begin(), end = m_relations.end(); + for (; !ctx.inconsistent() && it != end; ++it) { + relation& r = *it->m_value; + if (!r.new_eq_eh(l, v1, v2)) { + set_neg_cycle_conflict(r); + break; + } + } + } + + final_check_status theory_special_relations::final_check_eh() { + TRACE("special_relations", tout << "\n";); + obj_map::iterator it = m_relations.begin(), end = m_relations.end(); + lbool r = l_true; + for (; it != end && r == l_true; ++it) { + r = final_check(*it->m_value); + } + switch (r) { + case l_undef: + return FC_GIVEUP; + case l_false: + return FC_CONTINUE; + default: + break; + } + it = m_relations.begin(); + bool new_equality = false; + for (; it != end; ++it) { + if (extract_equalities(*it->m_value)) { + new_equality = true; + } + } + if (new_equality) { + return FC_CONTINUE; + } + else { + return FC_DONE; + } + } + + lbool theory_special_relations::final_check_lo(relation& r) { + // all constraints are saturated by propagation. + return l_true; + } + + enode* theory_special_relations::ensure_enode(expr* e) { + context& ctx = get_context(); + if (!ctx.e_internalized(e)) { + ctx.internalize(e, false); + } + enode* n = ctx.get_enode(e); + ctx.mark_as_relevant(n); + return n; + } + + literal theory_special_relations::mk_literal(expr* _e) { + expr_ref e(_e, get_manager()); + context& ctx = get_context(); + ensure_enode(e); + return ctx.get_literal(e); + } + + theory_var theory_special_relations::mk_var(enode* n) { + if (is_attached_to_var(n)) { + return n->get_th_var(get_id()); + } + else { + theory_var v = theory::mk_var(n); + get_context().attach_th_var(n, this, v); + get_context().mark_as_relevant(n); + return v; + } + } + + lbool theory_special_relations::final_check_plo(relation& r) { + // + // ensure that !Rxy -> Ryx between connected components + // (where Rzx & Rzy or Rxz & Ryz for some z) + // + lbool res = l_true; + for (unsigned i = 0; res == l_true && i < r.m_asserted_atoms.size(); ++i) { + atom& a = *r.m_asserted_atoms[i]; + if (!a.phase() && r.m_uf.find(a.v1()) == r.m_uf.find(a.v2())) { + res = enable(a); + } + } + return res; + } + + lbool theory_special_relations::final_check_to(relation& r) { + uint_set visited, target; + lbool res = l_true; + for (unsigned i = 0; res == l_true && i < r.m_asserted_atoms.size(); ++i) { + atom& a = *r.m_asserted_atoms[i]; + if (!a.phase() && r.m_uf.find(a.v1()) == r.m_uf.find(a.v2())) { + target.reset(); + theory_var w; + // v2 !<= v1 is asserted + target.insert(a.v2()); + if (r.m_graph.reachable(a.v1(), visited, target, w)) { + // we already have v1 <= v2 + continue; + } + target.reset(); + if (r.m_graph.reachable(a.v2(), target, visited, w)) { + // there is a common successor + // v1 <= w + // v2 <= w + // v1 !<= v2 + // -> v1 <= w & v2 <= w & v1 !<= v2 -> v2 <= v1 + unsigned timestamp = r.m_graph.get_timestamp(); + r.m_explanation.reset(); + r.m_graph.find_shortest_reachable_path(a.v1(), w, timestamp, r); + r.m_graph.find_shortest_reachable_path(a.v2(), w, timestamp, r); + r.m_explanation.push_back(a.explanation()); + literal_vector const& lits = r.m_explanation; + if (!r.m_graph.enable_edge(r.m_graph.add_edge(a.v2(), a.v1(), s_integer(0), lits))) { + set_neg_cycle_conflict(r); + res = l_false; + } + } + // TODO: check if algorithm correctly produces all constraints. + // e.g., if we add an edge, do we have to repeat the loop? + // + } + } + return res; + } + + lbool theory_special_relations::enable(atom& a) { + if (!a.enable()) { + relation& r = a.get_relation(); + set_neg_cycle_conflict(r); + return l_false; + } + else { + return l_true; + } + } + + void theory_special_relations::set_neg_cycle_conflict(relation& r) { + r.m_explanation.reset(); + r.m_graph.traverse_neg_cycle2(false, r); + set_conflict(r); + } + + void theory_special_relations::set_conflict(relation& r) { + literal_vector const& lits = r.m_explanation; + context & ctx = get_context(); + vector params; + ctx.set_conflict( + ctx.mk_justification( + ext_theory_conflict_justification( + get_id(), ctx.get_region(), + lits.size(), lits.c_ptr(), 0, 0, params.size(), params.c_ptr()))); + } + + lbool theory_special_relations::final_check(relation& r) { + // timer m_timer_fc; //for debugging + // static unsigned call_count = 0; + // static double total_call_times = 0.0; + // m_timer_fc.start(); + // call_count++; + + lbool res = propagate(r); + if (res != l_true) return res; + switch (r.m_property) { + case sr_lo: + res = final_check_lo(r); + break; + case sr_po: + res = final_check_po(r); + break; + case sr_plo: + res = final_check_plo(r); + break; + case sr_to: + res = final_check_to(r); + break; + default: + UNREACHABLE(); + res = l_undef; + } + + return res; + } + + bool theory_special_relations::extract_equalities(relation& r) { + bool new_eq = false; + int_vector scc_id; + u_map roots; + context& ctx = get_context(); + r.m_graph.compute_zero_edge_scc(scc_id); + for (unsigned i = 0, j = 0; i < scc_id.size(); ++i) { + if (scc_id[i] == -1) { + continue; + } + enode* n = get_enode(i); + if (roots.find(scc_id[i], j)) { + enode* m = get_enode(j); + if (n->get_root() != m->get_root()) { + new_eq = true; + unsigned timestamp = r.m_graph.get_timestamp(); + r.m_explanation.reset(); + r.m_graph.find_shortest_zero_edge_path(i, j, timestamp, r); + r.m_graph.find_shortest_zero_edge_path(j, i, timestamp, r); + eq_justification js(ctx.mk_justification(theory_axiom_justification(get_id(), ctx.get_region(), r.m_explanation.size(), r.m_explanation.c_ptr()))); + ctx.assign_eq(n, m, js); + } + } + else { + roots.insert(scc_id[i], i); + } + } + return new_eq; + } + + /* + \brief Propagation for piecewise linear orders + */ + lbool theory_special_relations::propagate_plo(atom& a) { + lbool res = l_true; + relation& r = a.get_relation(); + if (a.phase()) { + r.m_uf.merge(a.v1(), a.v2()); + res = enable(a); + } + else if (r.m_uf.find(a.v1()) == r.m_uf.find(a.v2())) { + res = enable(a); + } + return res; + } + + lbool theory_special_relations::propagate_po(atom& a) { + lbool res = l_true; + relation& r = a.get_relation(); + if (a.phase()) { + r.m_uf.merge(a.v1(), a.v2()); + res = enable(a); + } + return res; + } + + lbool theory_special_relations::final_check_po(relation& r) { + if (!KVEC) { + lbool res = l_true; + for (unsigned i = 0; res == l_true && i < r.m_asserted_atoms.size(); ++i) { + atom& a = *r.m_asserted_atoms[i]; + if (!a.phase() && r.m_uf.find(a.v1()) == r.m_uf.find(a.v2())) { + // v1 !-> v2 + // find v1 -> v3 -> v4 -> v2 path + r.m_explanation.reset(); + unsigned timestamp = r.m_graph.get_timestamp(); + auto found_path = HYBRID_SEARCH ? + r.m_graph.find_path(a.v1(), a.v2(), timestamp, r) : + r.m_graph.find_shortest_reachable_path(a.v1(), a.v2(), timestamp, r); + if (found_path) { + r.m_explanation.push_back(a.explanation()); + set_conflict(r); + res = l_false; + } + } + } + return res; + } + context& ctx = get_context(); + ast_manager& m = ctx.get_manager(); + + ptr_vector assumptions; + ptr_vector literals; + + int k = 1; + static int curr_id = 100000; + + u_map> map; + lbool res = l_true; + for (atom * ap : r.m_asserted_atoms) { + if (res != l_true) break; + atom a = *ap; + if (a.phase()) { + continue; + // assumptions.push_back(b); + r.m_uf.merge(a.v1(), a.v2()); + } + } + for (atom * ap : r.m_asserted_atoms) { + if (res != l_true) break; + atom a = *ap; + if (a.phase()) + continue; + if (r.m_uf.find(a.v1()) != r.m_uf.find(a.v2())) { + continue; + } + populate_k_vars(a.v1(), k, map, curr_id, m, &m_int_sort); + populate_k_vars(a.v2(), k, map, curr_id, m, &m_int_sort); + + literals.push_back(m_autil.mk_lt(map[a.v1()][0], map[a.v2()][0])); + + auto bool_sort = m.mk_bool_sort(); + auto b_func = m.mk_func_decl(symbol(curr_id++), 0, &bool_sort, bool_sort); + auto b = m.mk_app(b_func, unsigned(0), nullptr); + + auto f = m.mk_implies( b, m.mk_not(literals.back()) ); + m_nested_solver->assert_expr(f); + atom_cache.insert(b->get_id(), &a); + assumptions.push_back(b); + r.m_explanation.reset(); + if (m_nested_solver->check_sat(assumptions.size(), assumptions.c_ptr()) == l_false) { + expr_ref_vector unsat_core(m); + m_nested_solver->get_unsat_core(unsat_core); + for (expr* e : unsat_core) { + atom& a = *atom_cache[e->get_id()]; + r.m_explanation.push_back(a.explanation()); + } + for (auto e : r.m_explanation) { + std::cerr << "EX " << e.hash() << "\n"; + } + set_conflict(r); + res = l_false; + } + assumptions.pop_back(); + } + return res; + } + + lbool theory_special_relations::propagate(relation& r) { + lbool res = l_true; + while (res == l_true && r.m_asserted_qhead < r.m_asserted_atoms.size()) { + atom& a = *r.m_asserted_atoms[r.m_asserted_qhead]; + switch (r.m_property) { + case sr_lo: + res = enable(a); + break; + case sr_plo: + res = propagate_plo(a); + break; + case sr_po: + res = propagate_po(a); + break; + default: + if (a.phase()) { + res = enable(a); + } + break; + } + ++r.m_asserted_qhead; + } + return res; + } + + void theory_special_relations::reset_eh() { + obj_map::iterator it = m_relations.begin(), end = m_relations.end(); + for (; it != end; ++it) { + dealloc(it->m_value); + } + m_relations.reset(); + del_atoms(0); + } + + void theory_special_relations::assign_eh(bool_var v, bool is_true) { + TRACE("special_relations", tout << "assign bv" << v << " " << (is_true?" <- true":" <- false") << "\n";); + atom* a = 0; + VERIFY(m_bool_var2atom.find(v, a)); + a->set_phase(is_true); + a->get_relation().m_asserted_atoms.push_back(a); + //std::cerr << "ASSIGN: " << a->v1() << ' ' << a->v2() << "\n"; + } + + void theory_special_relations::push_scope_eh() { + obj_map::iterator it = m_relations.begin(), end = m_relations.end(); + for (; it != end; ++it) { + it->m_value->push(); + } + m_atoms_lim.push_back(m_atoms.size()); + } + + void theory_special_relations::pop_scope_eh(unsigned num_scopes) { + obj_map::iterator it = m_relations.begin(), end = m_relations.end(); + for (; it != end; ++it) { + it->m_value->pop(num_scopes); + } + unsigned new_lvl = m_atoms_lim.size() - num_scopes; + del_atoms(m_atoms_lim[new_lvl]); + } + + void theory_special_relations::del_atoms(unsigned old_size) { + atoms::iterator begin = m_atoms.begin() + old_size; + atoms::iterator it = m_atoms.end(); + while (it != begin) { + --it; + atom * a = *it; + m_bool_var2atom.erase(a->var()); + dealloc(a); + } + m_atoms.shrink(old_size); + } + + + void theory_special_relations::collect_statistics(::statistics & st) const { + obj_map::iterator it = m_relations.begin(), end = m_relations.end(); + for (; it != end; ++it) { + it->m_value->m_graph.collect_statistics(st); + } + } + + model_value_proc * theory_special_relations::mk_value(enode * n, model_generator & mg) { + UNREACHABLE(); + return 0; + } + + void theory_special_relations::ensure_strict(graph& g) { + unsigned sz = g.get_num_edges(); + for (unsigned i = 0; i < sz; ++i) { + if (!g.is_enabled(i)) continue; + if (g.get_weight(i) != s_integer(0)) continue; + dl_var src = g.get_source(i); + dl_var dst = g.get_target(i); + if (get_enode(src)->get_root() == get_enode(dst)->get_root()) continue; + VERIFY(g.enable_edge(g.add_edge(src, dst, s_integer(-2), literal_vector()))); + } + TRACE("special_relations", g.display(tout);); + } + + void theory_special_relations::ensure_tree(graph& g) { + unsigned sz = g.get_num_nodes(); + for (unsigned i = 0; i < sz; ++i) { + int_vector const& edges = g.get_in_edges(i); + for (unsigned j = 0; j < edges.size(); ++j) { + edge_id e1 = edges[j]; + if (g.is_enabled(e1)) { + SASSERT (i == g.get_target(e1)); + dl_var src1 = g.get_source(e1); + for (unsigned k = j + 1; k < edges.size(); ++k) { + edge_id e2 = edges[k]; + if (g.is_enabled(e2)) { + dl_var src2 = g.get_source(e2); + if (get_enode(src1)->get_root() == get_enode(src2)->get_root()) continue; + if (!disconnected(g, src1, src2)) continue; + VERIFY(g.enable_edge(g.add_edge(src1, src2, s_integer(-2), literal_vector()))); + } + } + } + } + } + TRACE("special_relations", g.display(tout);); + } + + bool theory_special_relations::disconnected(graph const& g, dl_var u, dl_var v) const { + s_integer val_u = g.get_assignment(u); + s_integer val_v = g.get_assignment(v); + if (val_u == val_v) return u != v; + if (val_u < val_v) { + std::swap(u, v); + std::swap(val_u, val_v); + } + SASSERT(val_u > val_v); + svector todo; + todo.push_back(u); + while (!todo.empty()) { + u = todo.back(); + todo.pop_back(); + if (u == v) { + return false; + } + SASSERT(g.get_assignment(u) <= val_u); + if (g.get_assignment(u) <= val_v) { + continue; + } + int_vector const& edges = g.get_out_edges(u); + for (unsigned i = 0; i < edges.size(); ++i) { + edge_id e = edges[i]; + if (is_strict_neighbour_edge(g, e)) { + todo.push_back(g.get_target(e)); + } + } + } + return true; + } + + expr_ref theory_special_relations::mk_inj(relation& r, model_generator& mg) { + // context& ctx = get_context(); + ast_manager& m = get_manager(); + r.push(); + ensure_strict(r.m_graph); + func_decl_ref fn(m); + expr_ref result(m); + arith_util arith(m); + sort* const* ty = r.decl()->get_domain(); + fn = m.mk_fresh_func_decl("inj", 1, ty, arith.mk_int()); + unsigned sz = r.m_graph.get_num_nodes(); + func_interp* fi = alloc(func_interp, m, 1); + for (unsigned i = 0; i < sz; ++i) { + s_integer val = r.m_graph.get_assignment(i); + expr* arg = get_enode(i)->get_owner(); + fi->insert_new_entry(&arg, arith.mk_numeral(val.to_rational(), true)); + } + TRACE("special_relations", r.m_graph.display(tout);); + r.pop(1); + fi->set_else(arith.mk_numeral(rational(0), true)); + mg.get_model().register_decl(fn, fi); + result = arith.mk_le(m.mk_app(fn,m.mk_var(0, *ty)), m.mk_app(fn, m.mk_var(1, *ty))); + return result; + } + + expr_ref theory_special_relations::mk_class(relation& r, model_generator& mg) { + //context& ctx = get_context(); + ast_manager& m = get_manager(); + expr_ref result(m); + func_decl_ref fn(m); + arith_util arith(m); + func_interp* fi = alloc(func_interp, m, 1); + sort* const* ty = r.decl()->get_domain(); + fn = m.mk_fresh_func_decl("class", 1, ty, arith.mk_int()); + unsigned sz = r.m_graph.get_num_nodes(); + for (unsigned i = 0; i < sz; ++i) { + unsigned val = r.m_uf.find(i); + expr* arg = get_enode(i)->get_owner(); + fi->insert_new_entry(&arg, arith.mk_numeral(rational(val), true)); + } + fi->set_else(arith.mk_numeral(rational(0), true)); + mg.get_model().register_decl(fn, fi); + result = m.mk_eq(m.mk_app(fn, m.mk_var(0, *ty)), m.mk_app(fn, m.mk_var(1, *ty))); + return result; + } + + expr_ref theory_special_relations::mk_interval(relation& r, model_generator& mg, unsigned_vector & lo, unsigned_vector& hi) { + graph const& g = r.m_graph; + //context& ctx = get_context(); + ast_manager& m = get_manager(); + expr_ref result(m); + func_decl_ref lofn(m), hifn(m); + arith_util arith(m); + func_interp* lofi = alloc(func_interp, m, 1); + func_interp* hifi = alloc(func_interp, m, 1); + sort* const* ty = r.decl()->get_domain(); + lofn = m.mk_fresh_func_decl("lo", 1, ty, arith.mk_int()); + hifn = m.mk_fresh_func_decl("hi", 1, ty, arith.mk_int()); + unsigned sz = g.get_num_nodes(); + for (unsigned i = 0; i < sz; ++i) { + expr* arg = get_enode(i)->get_owner(); + lofi->insert_new_entry(&arg, arith.mk_numeral(rational(lo[i]), true)); + hifi->insert_new_entry(&arg, arith.mk_numeral(rational(hi[i]), true)); + } + lofi->set_else(arith.mk_numeral(rational(0), true)); + hifi->set_else(arith.mk_numeral(rational(0), true)); + mg.get_model().register_decl(lofn, lofi); + mg.get_model().register_decl(hifn, hifi); + result = m.mk_and(arith.mk_le(m.mk_app(lofn, m.mk_var(0, *ty)), m.mk_app(lofn, m.mk_var(1, *ty))), + arith.mk_le(m.mk_app(hifn, m.mk_var(1, *ty)), m.mk_app(hifn, m.mk_var(0, *ty)))); + return result; + } + + void theory_special_relations::init_model_lo(relation& r, model_generator& m) { + expr_ref inj = mk_inj(r, m); + func_interp* fi = alloc(func_interp, get_manager(), 2); + fi->set_else(inj); + m.get_model().register_decl(r.decl(), fi); + } + + void theory_special_relations::init_model_plo(relation& r, model_generator& m) { + expr_ref inj = mk_inj(r, m); + expr_ref cls = mk_class(r, m); + func_interp* fi = alloc(func_interp, get_manager(), 2); + fi->set_else(get_manager().mk_and(inj, cls)); + m.get_model().register_decl(r.decl(), fi); + } + + void theory_special_relations::init_model_po(relation& r, model_generator& mg) { + // NOT_IMPLEMENTED_YET(); + } + + /** + \brief map each node to an interval of numbers, such that + the children are proper sub-intervals. + Then the <= relation becomes interval containment. + + 1. For each vertex, count the number of nodes below it in the transitive closure. + Store the result in num_children. + 2. Identify each root. + 3. Process children, assigning unique (and disjoint) intervals. + 4. Extract interpretation. + + + */ + + void theory_special_relations::init_model_to(relation& r, model_generator& mg) { + unsigned_vector num_children, lo, hi; + graph const& g = r.m_graph; + r.push(); + ensure_strict(r.m_graph); + ensure_tree(r.m_graph); + count_children(g, num_children); + assign_interval(g, num_children, lo, hi); + expr_ref iv = mk_interval(r, mg, lo, hi); + r.pop(1); + func_interp* fi = alloc(func_interp, get_manager(), 2); + fi->set_else(iv); + mg.get_model().register_decl(r.decl(), fi); + } + + bool theory_special_relations::is_neighbour_edge(graph const& g, edge_id edge) const { + CTRACE("special_relations_verbose", g.is_enabled(edge), + tout << edge << ": " << g.get_source(edge) << " " << g.get_target(edge) << " "; + tout << (g.get_assignment(g.get_source(edge)) - g.get_assignment(g.get_target(edge))) << "\n";); + + return + g.is_enabled(edge) && + g.get_assignment(g.get_source(edge)) - g.get_assignment(g.get_target(edge)) == s_integer(1); + } + + bool theory_special_relations::is_strict_neighbour_edge(graph const& g, edge_id e) const { + return is_neighbour_edge(g, e) && g.get_weight(e) != s_integer(0); + } + + void theory_special_relations::count_children(graph const& g, unsigned_vector& num_children) { + unsigned sz = g.get_num_nodes(); + svector nodes; + num_children.resize(sz, 0); + svector processed(sz, false); + for (unsigned i = 0; i < sz; ++i) nodes.push_back(i); + while (!nodes.empty()) { + dl_var v = nodes.back(); + if (processed[v]) { + nodes.pop_back(); + continue; + } + unsigned nc = 1; + bool all_p = true; + int_vector const& edges = g.get_out_edges(v); + for (unsigned i = 0; i < edges.size(); ++i) { + edge_id e = edges[i]; + if (is_strict_neighbour_edge(g, e)) { + dl_var dst = g.get_target(e); + TRACE("special_relations", tout << v << " -> " << dst << "\n";); + if (!processed[dst]) { + all_p = false; + nodes.push_back(dst); + } + nc += num_children[dst]; + } + } + if (all_p) { + nodes.pop_back(); + num_children[v] = nc; + processed[v] = true; + } + } + TRACE("special_relations", + for (unsigned i = 0; i < sz; ++i) { + tout << i << ": " << num_children[i] << "\n"; + }); + } + + void theory_special_relations::assign_interval(graph const& g, unsigned_vector const& num_children, unsigned_vector& lo, unsigned_vector& hi) { + svector nodes; + unsigned sz = g.get_num_nodes(); + lo.resize(sz, 0); + hi.resize(sz, 0); + unsigned offset = 0; + for (unsigned i = 0; i < sz; ++i) { + bool is_root = true; + int_vector const& edges = g.get_in_edges(i); + for (unsigned j = 0; is_root && j < edges.size(); ++j) { + is_root = !g.is_enabled(edges[j]); + } + if (is_root) { + lo[i] = offset; + hi[i] = offset + num_children[i] - 1; + offset = hi[i] + 1; + nodes.push_back(i); + } + } + while (!nodes.empty()) { + dl_var v = nodes.back(); + int_vector const& edges = g.get_out_edges(v); + unsigned l = lo[v]; + unsigned h = hi[v]; + (void)h; + nodes.pop_back(); + for (unsigned i = 0; i < edges.size(); ++i) { + SASSERT(l <= h); + if (is_strict_neighbour_edge(g, edges[i])) { + dl_var dst = g.get_target(edges[i]); + lo[dst] = l; + hi[dst] = l + num_children[dst] - 1; + l = hi[dst] + 1; + nodes.push_back(dst); + } + } + SASSERT(l == h); + } + } + + void theory_special_relations::init_model(model_generator & m) { + obj_map::iterator it = m_relations.begin(), end = m_relations.end(); + for (; it != end; ++it) { + switch (it->m_value->m_property) { + case sr_lo: + init_model_lo(*it->m_value, m); + break; + case sr_plo: + init_model_plo(*it->m_value, m); + break; + case sr_to: + init_model_to(*it->m_value, m); + break; + case sr_po: + init_model_po(*it->m_value, m); + break; + default: + UNREACHABLE(); //ASHU: added to remove warning! Should be supported! + } + } + } + + void theory_special_relations::display(std::ostream & out) const { + if (m_relations.empty()) return; + out << "Theory Special Relations\n"; + display_var2enode(out); + obj_map::iterator it = m_relations.begin(), end = m_relations.end(); + for (; it != end; ++it) { + out << mk_pp(it->m_value->decl(), get_manager()) << ":\n"; + it->m_value->m_graph.display(out); + it->m_value->m_uf.display(out); + for (unsigned i = 0; i < it->m_value->m_asserted_atoms.size(); ++i){ + atom& a = *it->m_value->m_asserted_atoms[i]; + display_atom( out, a ); + } + } + } + + void theory_special_relations::collect_asserted_po_atoms( vector< std::pair >& atoms) const { + obj_map::iterator it = m_relations.begin(), end = m_relations.end(); + for (; it != end; ++it) { + relation& r = *(it->m_value ); + if( r.m_property != sr_po ) continue; + // SASSERT( r.m_asserted_qhead == r.m_asserted_atoms.size() ); + for (unsigned i = 0; i < r.m_asserted_atoms.size(); ++i) { + atom& a = *r.m_asserted_atoms[i]; + atoms.push_back( std::make_pair(a.var(),a.phase()) ); + } + } + } + + void theory_special_relations::display_atom( std::ostream & out, atom& a ) const { + context& ctx = get_context(); + expr* e = ctx.bool_var2expr( a.var() ); + if( !a.phase() ) out << "(not "; + out << mk_pp( e, get_manager()); + if( !a.phase() ) out << ")"; + out << "\n"; + } + + void theory_special_relations::display_atom( atom& a) const { + display_atom( std::cerr, a); + } + +} diff --git a/src/smt/theory_special_relations.h b/src/smt/theory_special_relations.h new file mode 100644 index 000000000..dbb339d3c --- /dev/null +++ b/src/smt/theory_special_relations.h @@ -0,0 +1,198 @@ +/*++ +Copyright (c) 2015 Microsoft Corporation + +Module Name: + + theory_special_relations.h + +Abstract: + + Special Relations theory plugin. + +Author: + + Nikolaj Bjorner (nbjorner) 2015-9-16 + +Notes: + +--*/ + +#include "ast/special_relations_decl_plugin.h" +#include "smt/smt_theory.h" +#include "smt/theory_diff_logic.h" +#include "util/union_find.h" +#include "solver/solver.h" + +#ifndef THEORY_SPECIAL_RELATIONS_H_ +#define THEORY_SPECIAL_RELATIONS_H_ + +namespace smt { + class theory_special_relations : public theory { + + + struct relation; + + class atom { + bool_var m_bvar; + relation& m_relation; + bool m_phase; + theory_var m_v1; + theory_var m_v2; + edge_id m_pos; + edge_id m_neg; + public: + atom(bool_var b, relation& r, theory_var v1, theory_var v2): + m_bvar(b), + m_relation(r), + m_phase(true), + m_v1(v1), + m_v2(v2) + { + r.ensure_var(v1); + r.ensure_var(v2); + literal_vector ls; + ls.push_back(literal(b, false)); + m_pos = r.m_graph.add_edge(v1, v2, s_integer(1), ls); // v2 <= v1 + ls[0] = literal(b, true); + m_neg = r.m_graph.add_edge(v2, v1, s_integer(-2), ls); // v1 <= v2 - 1 + } + bool_var var() const { return m_bvar;} + relation& get_relation() const { return m_relation; } + bool phase() { return m_phase; } + void set_phase(bool b) { m_phase = b; } + theory_var v1() { return m_v1; } + theory_var v2() { return m_v2; } + literal explanation() { return literal(m_bvar, !m_phase); } + bool enable() { + edge_id edge = m_phase?m_pos:m_neg; + return m_relation.m_graph.enable_edge(edge); + } + }; + typedef ptr_vector atoms; + + struct scope { + unsigned m_asserted_atoms_lim; + unsigned m_asserted_qhead_old; + }; + + struct int_ext : public sidl_ext { + typedef literal_vector explanation; + }; + typedef dl_graph graph; + + typedef union_find union_find_t; + + struct relation { + sr_property m_property; + func_decl* m_decl; + atoms m_asserted_atoms; // set of asserted atoms + unsigned m_asserted_qhead; + svector m_scopes; + graph m_graph; + union_find_default_ctx m_ufctx; + union_find_t m_uf; + literal_vector m_explanation; + + relation(sr_property p, func_decl* d): m_property(p), m_decl(d), m_asserted_qhead(0), m_uf(m_ufctx) {} + + func_decl* decl() { return m_decl; } + void push(); + void pop(unsigned num_scopes); + void ensure_var(theory_var v); + bool new_eq_eh(literal l, theory_var v1, theory_var v2); + void operator()(literal_vector const & ex) { + m_explanation.append(ex); + } + void new_edge(dl_var src, dl_var dst, unsigned num_edges, edge_id const* edges) {} + }; + + + + + typedef u_map bool_var2atom; + + special_relations_util m_util; + arith_util m_autil; + + atoms m_atoms; + unsigned_vector m_atoms_lim; + obj_map m_relations; + bool_var2atom m_bool_var2atom; + + scoped_ptr m_nested_solver; + struct atom_hash { + size_t operator()(atom a) const { + return std::hash()(a.v1()) ^ std::hash()(a.v2()) ^ std::hash()(a.phase()); + } + }; + u_map expr_cache; + u_map atom_cache; + sort* m_int_sort; + + void del_atoms(unsigned old_size); + lbool final_check(relation& r); + lbool final_check_po(relation& r); + lbool final_check_lo(relation& r); + lbool final_check_plo(relation& r); + lbool final_check_to(relation& r); + lbool propagate(relation& r); + lbool enable(atom& a); + bool extract_equalities(relation& r); + void set_neg_cycle_conflict(relation& r); + void set_conflict(relation& r); + lbool propagate_plo(atom& a); + lbool propagate_po(atom& a); //ASHU: added to modify po solving + theory_var mk_var(expr* e); + void count_children(graph const& g, unsigned_vector& num_children); + void ensure_strict(graph& g); + void ensure_tree(graph& g); + void assign_interval(graph const& g, unsigned_vector const& num_children, unsigned_vector& lo, unsigned_vector& hi); + expr_ref mk_inj(relation& r, model_generator& m); + expr_ref mk_class(relation& r, model_generator& m); + expr_ref mk_interval(relation& r, model_generator& mg, unsigned_vector & lo, unsigned_vector& hi); + void init_model_lo(relation& r, model_generator& m); + void init_model_to(relation& r, model_generator& m); + void init_model_po(relation& r, model_generator& m); + void init_model_plo(relation& r, model_generator& m); + bool is_neighbour_edge(graph const& g, edge_id id) const; + bool is_strict_neighbour_edge(graph const& g, edge_id id) const; + bool disconnected(graph const& g, dl_var u, dl_var v) const; + + public: + theory_special_relations(ast_manager& m); + virtual ~theory_special_relations(); + + virtual theory * mk_fresh(context * new_ctx); + virtual bool internalize_atom(app * atom, bool gate_ctx); + virtual bool internalize_term(app * term) { UNREACHABLE(); return false; } + virtual void new_eq_eh(theory_var v1, theory_var v2); + virtual void new_diseq_eh(theory_var v1, theory_var v2) {} + virtual bool use_diseqs() const { return false; } + virtual bool build_models() const { return true; } + virtual final_check_status final_check_eh(); + virtual void reset_eh(); + virtual void assign_eh(bool_var v, bool is_true); + virtual void init_search_eh() {} + virtual void push_scope_eh(); + virtual void pop_scope_eh(unsigned num_scopes); + virtual void restart_eh() {} + virtual void collect_statistics(::statistics & st) const; + virtual model_value_proc * mk_value(enode * n, model_generator & mg); + virtual void init_model(model_generator & m); + virtual bool can_propagate() { return false; } + virtual void propagate() {} + virtual void display(std::ostream & out) const; + + literal mk_literal(expr* _e); + enode* ensure_enode(expr* e); + theory_var mk_var(enode* n); + + //BEGIN: ASHU + void collect_asserted_po_atoms( vector< std::pair >& atoms) const; + void display_atom( std::ostream & out, atom& a) const; + void display_atom( atom& a) const; + //END: ASHU + }; +} + +#endif From 0fa4aaa62526da0bd49e3e92fdb043b2399486f6 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 24 Mar 2019 19:10:30 -0700 Subject: [PATCH 02/19] use for pattern Signed-off-by: Nikolaj Bjorner --- src/smt/diff_logic.h | 127 ++++++--------------------- src/smt/theory_special_relations.cpp | 10 +-- 2 files changed, 34 insertions(+), 103 deletions(-) diff --git a/src/smt/diff_logic.h b/src/smt/diff_logic.h index f3ce7fb13..5ea27d4c9 100644 --- a/src/smt/diff_logic.h +++ b/src/smt/diff_logic.h @@ -228,10 +228,7 @@ class dl_graph { int n = m_out_edges.size(); for (dl_var id = 0; id < n; id++) { const edge_id_vector & e_ids = m_out_edges[id]; - edge_id_vector::const_iterator it = e_ids.begin(); - edge_id_vector::const_iterator end = e_ids.end(); - for (; it != end; ++it) { - edge_id e_id = *it; + for (edge_id e_id : e_ids) { SASSERT(static_cast(e_id) <= m_edges.size()); const edge & e = m_edges[e_id]; SASSERT(e.get_source() == id); @@ -239,10 +236,7 @@ class dl_graph { } for (dl_var id = 0; id < n; id++) { const edge_id_vector & e_ids = m_in_edges[id]; - edge_id_vector::const_iterator it = e_ids.begin(); - edge_id_vector::const_iterator end = e_ids.end(); - for (; it != end; ++it) { - edge_id e_id = *it; + for (edge_id e_id : e_ids) { SASSERT(static_cast(e_id) <= m_edges.size()); const edge & e = m_edges[e_id]; SASSERT(e.get_target() == id); @@ -337,10 +331,8 @@ private: } void reset_marks() { - dl_var_vector::iterator it = m_visited.begin(); - dl_var_vector::iterator end = m_visited.end(); - for (; it != end; ++it) { - m_mark[*it] = DL_UNMARKED; + for (dl_var v : m_visited) { + m_mark[v] = DL_UNMARKED; } m_visited.reset(); } @@ -392,10 +384,7 @@ private: return false; } - typename edge_id_vector::iterator it = m_out_edges[source].begin(); - typename edge_id_vector::iterator end = m_out_edges[source].end(); - for (; it != end; ++it) { - edge_id e_id = *it; + for (edge_id e_id : m_out_edges[source]) { edge & e = m_edges[e_id]; SASSERT(e.get_source() == source); if (!e.is_enabled()) { @@ -445,10 +434,7 @@ private: dl_var src = e->get_source(); dl_var dst = e->get_target(); numeral w = e->get_weight(); - typename edge_id_vector::iterator it = m_out_edges[src].begin(); - typename edge_id_vector::iterator end = m_out_edges[src].end(); - for (; it != end; ++it) { - edge_id e_id = *it; + for (edge_id e_id : m_out_edges[src]) { edge const& e2 = m_edges[e_id]; if (e2.get_target() == dst && e2.is_enabled() && // or at least not be inconsistent with current choices @@ -598,10 +584,7 @@ public: // // search for edges that can reduce size of negative cycle. // - typename edge_id_vector::iterator it = m_out_edges[src].begin(); - typename edge_id_vector::iterator end = m_out_edges[src].end(); - for (; it != end; ++it) { - edge_id e_id2 = *it; + for (edge_id e_id2 : m_out_edges[src]) { edge const& e2 = m_edges[e_id2]; dl_var src2 = e2.get_target(); if (e_id2 == e_id || !e2.is_enabled()) { @@ -905,10 +888,8 @@ public: SASSERT(is_feasible()); if (!m_assignment[v].is_zero()) { numeral k = m_assignment[v]; - typename assignment::iterator it = m_assignment.begin(); - typename assignment::iterator end = m_assignment.end(); - for (; it != end; ++it) { - *it -= k; + for (auto& a : m_assignment) { + a -= k; } SASSERT(is_feasible()); } @@ -963,10 +944,7 @@ public: void display_agl(std::ostream & out) const { uint_set vars; - typename edges::const_iterator it = m_edges.begin(); - typename edges::const_iterator end = m_edges.end(); - for (; it != end; ++it) { - edge const& e = *it; + for (edge const& e : m_edges) { if (e.is_enabled()) { vars.insert(e.get_source()); vars.insert(e.get_target()); @@ -980,9 +958,7 @@ public: out << "\"" << v << "\" [label=\"" << v << ":" << m_assignment[v] << "\"]\n"; } } - it = m_edges.begin(); - for (; it != end; ++it) { - edge const& e = *it; + for (edge const& e : m_edges) { if (e.is_enabled()) { out << "\"" << e.get_source() << "\"->\"" << e.get_target() << "\"[label=\"" << e.get_weight() << "\"]\n"; } @@ -998,10 +974,7 @@ public: } void display_edges(std::ostream & out) const { - typename edges::const_iterator it = m_edges.begin(); - typename edges::const_iterator end = m_edges.end(); - for (; it != end; ++it) { - edge const& e = *it; + for (edge const& e : m_edges) { if (e.is_enabled()) { display_edge(out, e); } @@ -1030,11 +1003,8 @@ public: // If there is such edge, then the weight is stored in w and the explanation in ex. bool get_edge_weight(dl_var source, dl_var target, numeral & w, explanation & ex) { edge_id_vector & edges = m_out_edges[source]; - typename edge_id_vector::iterator it = edges.begin(); - typename edge_id_vector::iterator end = edges.end(); bool found = false; - for (; it != end; ++it) { - edge_id e_id = *it; + for (edge_id e_id : edges) { edge & e = m_edges[e_id]; if (e.is_enabled() && e.get_target() == target && (!found || e.get_weight() < w)) { w = e.get_weight(); @@ -1049,12 +1019,10 @@ public: // If there is such edge, return its edge_id in parameter id. bool get_edge_id(dl_var source, dl_var target, edge_id & id) const { edge_id_vector const & edges = m_out_edges[source]; - typename edge_id_vector::const_iterator it = edges.begin(); - typename edge_id_vector::const_iterator end = edges.end(); - for (; it != end; ++it) { - id = *it; - edge const & e = m_edges[id]; + for (edge_id e_id : edges) { + edge const & e = m_edges[e_id]; if (e.get_target() == target) { + id = e_id; return true; } } @@ -1068,18 +1036,14 @@ public: void get_neighbours_undirected(dl_var current, svector & neighbours) { neighbours.reset(); edge_id_vector & out_edges = m_out_edges[current]; - typename edge_id_vector::iterator it = out_edges.begin(), end = out_edges.end(); - for (; it != end; ++it) { - edge_id e_id = *it; + for (edge_id e_id : out_edges) { edge & e = m_edges[e_id]; SASSERT(e.get_source() == current); dl_var neighbour = e.get_target(); neighbours.push_back(neighbour); } edge_id_vector & in_edges = m_in_edges[current]; - typename edge_id_vector::iterator it2 = in_edges.begin(), end2 = in_edges.end(); - for (; it2 != end2; ++it2) { - edge_id e_id = *it2; + for (edge_id e_id : in_edges) { edge & e = m_edges[e_id]; SASSERT(e.get_target() == current); dl_var neighbour = e.get_source(); @@ -1162,10 +1126,7 @@ public: template void enumerate_edges(dl_var source, dl_var target, Functor& f) { edge_id_vector & edges = m_out_edges[source]; - typename edge_id_vector::iterator it = edges.begin(); - typename edge_id_vector::iterator end = edges.end(); - for (; it != end; ++it) { - edge_id e_id = *it; + for (edge_id e_id : edges) { edge const& e = m_edges[e_id]; if (e.get_target() == target) { f(e.get_weight(), e.get_explanation()); @@ -1222,10 +1183,7 @@ public: m_roots.push_back(v); numeral gamma; edge_id_vector & edges = m_out_edges[v]; - typename edge_id_vector::iterator it = edges.begin(); - typename edge_id_vector::iterator end = edges.end(); - for (; it != end; ++it) { - edge_id e_id = *it; + for (edge_id e_id : edges) { edge & e = m_edges[e_id]; if (!e.is_enabled()) { continue; @@ -1278,10 +1236,7 @@ public: for (unsigned i = 0; i < succ.size(); ++i) { v = succ[i]; edge_id_vector & edges = m_out_edges[v]; - typename edge_id_vector::iterator it = edges.begin(); - typename edge_id_vector::iterator end = edges.end(); - for (; it != end; ++it) { - edge_id e_id = *it; + for (edge_id e_id : edges) { edge & e = m_edges[e_id]; if (!e.is_enabled()) { continue; @@ -1708,11 +1663,8 @@ private: for (unsigned i = 0; i < src.m_visited.size(); ++i) { dl_var c = src.m_visited[i]; - typename edge_id_vector::const_iterator it = edges[c].begin(); - typename edge_id_vector::const_iterator end = edges[c].end(); numeral n1 = n0 + src.m_delta[c] - m_assignment[c]; - for (; it != end; ++it) { - edge_id e_id = *it; + for (edge_id e_id : edges[c]) { edge const& e1 = m_edges[e_id]; SASSERT(c == e1.get_source()); if (e1.is_enabled()) { @@ -1760,13 +1712,10 @@ public: edge_id_vector& out_edges = m_out_edges[src]; edge_id_vector& in_edges = m_in_edges[dst]; numeral w = e1.get_weight(); - typename edge_id_vector::const_iterator it, end; if (out_edges.size() < in_edges.size()) { - end = out_edges.end(); - for (it = out_edges.begin(); it != end; ++it) { + for (edge_id e_id : out_edges) { ++m_stats.m_implied_literal_cost; - edge_id e_id = *it; edge const& e2 = m_edges[e_id]; if (e_id != id && !e2.is_enabled() && e2.get_target() == dst && e2.get_weight() >= w) { subsumed.push_back(e_id); @@ -1775,10 +1724,8 @@ public: } } else { - end = in_edges.end(); - for (it = in_edges.begin(); it != end; ++it) { + for (edge_id e_id : in_edges) { ++m_stats.m_implied_literal_cost; - edge_id e_id = *it; edge const& e2 = m_edges[e_id]; if (e_id != id && !e2.is_enabled() && e2.get_source() == src && e2.get_weight() >= w) { subsumed.push_back(e_id); @@ -1812,20 +1759,14 @@ public: find_subsumed1(id, subsumed); typename edge_id_vector::const_iterator it, end, it3, end3; - it = m_in_edges[src].begin(); - end = m_in_edges[src].end(); - for (; it != end; ++it) { - edge_id e_id = *it; + for (edge_id e_id : m_in_edges[src]) { edge const& e2 = m_edges[e_id]; if (!e2.is_enabled() || e2.get_source() == dst) { continue; } w2 = e2.get_weight() + w; - it3 = m_out_edges[e2.get_source()].begin(); - end3 = m_out_edges[e2.get_source()].end(); - for (; it3 != end3; ++it3) { + for (edge_id e_id3 : m_out_edges[e2.get_source()]) { ++m_stats.m_implied_literal_cost; - edge_id e_id3 = *it3; edge const& e3 = m_edges[e_id3]; if (e3.is_enabled() || e3.get_target() != dst) { continue; @@ -1836,21 +1777,15 @@ public: } } } - it = m_out_edges[dst].begin(); - end = m_out_edges[dst].end(); - for (; it != end; ++it) { - edge_id e_id = *it; + for (edge_id e_id : m_out_edges[dst]) { edge const& e2 = m_edges[e_id]; if (!e2.is_enabled() || e2.get_target() == src) { continue; } w2 = e2.get_weight() + w; - it3 = m_in_edges[e2.get_target()].begin(); - end3 = m_in_edges[e2.get_target()].end(); - for (; it3 != end3; ++it3) { + for (edge_id e_id2 : m_in_edges[e2.get_target()]) { ++m_stats.m_implied_literal_cost; - edge_id e_id3 = *it3; edge const& e3 = m_edges[e_id3]; if (e3.is_enabled() || e3.get_source() != src) { continue; @@ -1899,11 +1834,7 @@ public: m_mark[v] = DL_PROCESSED; TRACE("diff_logic", tout << v << "\n";); - typename edge_id_vector::iterator it = m_out_edges[v].begin(); - typename edge_id_vector::iterator end = m_out_edges[v].end(); - - for (; it != end; ++it) { - edge_id e_id = *it; + for (edge_id e_id : m_out_edges[v]) { edge const& e = m_edges[e_id]; if (!e.is_enabled() || e.get_timestamp() > timestamp) { continue; diff --git a/src/smt/theory_special_relations.cpp b/src/smt/theory_special_relations.cpp index c58ffb24a..a5a6ce13a 100644 --- a/src/smt/theory_special_relations.cpp +++ b/src/smt/theory_special_relations.cpp @@ -92,10 +92,10 @@ namespace smt { return alloc(theory_special_relations, new_ctx->get_manager()); } - static void populate_k_vars(int v, int k, u_map>& map, int& curr_id, ast_manager& m, sort** int_sort) { + static void populate_k_vars(int v, int k, u_map>& map, int& curr_id, ast_manager& m, sort* int_sort) { int need = !map.contains(v) ? k : k - map[v].size(); for (auto i = 0; i < need; ++i) { - auto *fd = m.mk_func_decl(symbol(curr_id++), 0, int_sort, *int_sort); + auto *fd = m.mk_const_decl(symbol(curr_id++), int_sort); map[v].push_back(m.mk_app(fd, unsigned(0), nullptr)); } } @@ -438,13 +438,13 @@ namespace smt { if (r.m_uf.find(a.v1()) != r.m_uf.find(a.v2())) { continue; } - populate_k_vars(a.v1(), k, map, curr_id, m, &m_int_sort); - populate_k_vars(a.v2(), k, map, curr_id, m, &m_int_sort); + populate_k_vars(a.v1(), k, map, curr_id, m, m_int_sort); + populate_k_vars(a.v2(), k, map, curr_id, m, m_int_sort); literals.push_back(m_autil.mk_lt(map[a.v1()][0], map[a.v2()][0])); auto bool_sort = m.mk_bool_sort(); - auto b_func = m.mk_func_decl(symbol(curr_id++), 0, &bool_sort, bool_sort); + auto b_func = m.mk_const_decl(symbol(curr_id++), bool_sort); auto b = m.mk_app(b_func, unsigned(0), nullptr); auto f = m.mk_implies( b, m.mk_not(literals.back()) ); From 4603c647a7bbf2d9dfa8bf3f02093a2de4a31a20 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 24 Mar 2019 19:21:54 -0700 Subject: [PATCH 03/19] use override Signed-off-by: Nikolaj Bjorner --- src/smt/theory_special_relations.cpp | 4 --- src/smt/theory_special_relations.h | 50 +++++++++++++--------------- 2 files changed, 24 insertions(+), 30 deletions(-) diff --git a/src/smt/theory_special_relations.cpp b/src/smt/theory_special_relations.cpp index a5a6ce13a..e1a42403d 100644 --- a/src/smt/theory_special_relations.cpp +++ b/src/smt/theory_special_relations.cpp @@ -898,8 +898,4 @@ namespace smt { out << "\n"; } - void theory_special_relations::display_atom( atom& a) const { - display_atom( std::cerr, a); - } - } diff --git a/src/smt/theory_special_relations.h b/src/smt/theory_special_relations.h index dbb339d3c..90b6a7bbf 100644 --- a/src/smt/theory_special_relations.h +++ b/src/smt/theory_special_relations.h @@ -160,38 +160,36 @@ namespace smt { public: theory_special_relations(ast_manager& m); - virtual ~theory_special_relations(); + ~theory_special_relations() override; - virtual theory * mk_fresh(context * new_ctx); - virtual bool internalize_atom(app * atom, bool gate_ctx); - virtual bool internalize_term(app * term) { UNREACHABLE(); return false; } - virtual void new_eq_eh(theory_var v1, theory_var v2); - virtual void new_diseq_eh(theory_var v1, theory_var v2) {} - virtual bool use_diseqs() const { return false; } - virtual bool build_models() const { return true; } - virtual final_check_status final_check_eh(); - virtual void reset_eh(); - virtual void assign_eh(bool_var v, bool is_true); - virtual void init_search_eh() {} - virtual void push_scope_eh(); - virtual void pop_scope_eh(unsigned num_scopes); - virtual void restart_eh() {} - virtual void collect_statistics(::statistics & st) const; - virtual model_value_proc * mk_value(enode * n, model_generator & mg); - virtual void init_model(model_generator & m); - virtual bool can_propagate() { return false; } - virtual void propagate() {} - virtual void display(std::ostream & out) const; + theory * mk_fresh(context * new_ctx) override; + bool internalize_atom(app * atom, bool gate_ctx) override; + bool internalize_term(app * term) override { UNREACHABLE(); return false; } + void new_eq_eh(theory_var v1, theory_var v2) override; + void new_diseq_eh(theory_var v1, theory_var v2) override {} + bool use_diseqs() const override { return false; } + bool build_models() const override { return true; } + final_check_status final_check_eh() override; + void reset_eh() override; + void assign_eh(bool_var v, bool is_true) override; + void init_search_eh() override {} + void push_scope_eh() override; + void pop_scope_eh(unsigned num_scopes) override; + void restart_eh() override {} + void collect_statistics(::statistics & st) const override; + model_value_proc * mk_value(enode * n, model_generator & mg) override; + void init_model(model_generator & m) override; + bool can_propagate() override { return false; } + void propagate() override {} + void display(std::ostream & out) const override; literal mk_literal(expr* _e); enode* ensure_enode(expr* e); theory_var mk_var(enode* n); - //BEGIN: ASHU - void collect_asserted_po_atoms( vector< std::pair >& atoms) const; - void display_atom( std::ostream & out, atom& a) const; - void display_atom( atom& a) const; - //END: ASHU + void collect_asserted_po_atoms( vector< std::pair >& atoms) const; + void display_atom( std::ostream & out, atom& a) const; + }; } From ceb4c985bfdf2372860f27868262417cf5182a05 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 24 Mar 2019 20:21:22 -0700 Subject: [PATCH 04/19] tidy Signed-off-by: Nikolaj Bjorner --- src/smt/diff_logic.h | 91 ++++++++++++++---------------- src/smt/theory_special_relations.h | 28 ++++----- 2 files changed, 55 insertions(+), 64 deletions(-) diff --git a/src/smt/diff_logic.h b/src/smt/diff_logic.h index 5ea27d4c9..29b1050df 100644 --- a/src/smt/diff_logic.h +++ b/src/smt/diff_logic.h @@ -324,10 +324,11 @@ private: // Store in gamma the normalized weight. The normalized weight is given // by the formula // m_assignment[e.get_source()] - m_assignment[e.get_target()] + e.get_weight() - void set_gamma(const edge & e, numeral & gamma) { + numeral& set_gamma(const edge & e, numeral & gamma) { gamma = m_assignment[e.get_source()]; gamma -= m_assignment[e.get_target()]; gamma += e.get_weight(); + return gamma; } void reset_marks() { @@ -373,7 +374,7 @@ private: TRACE("arith", tout << id << "\n";); dl_var source = target; - for(;;) { + while (true) { ++m_stats.m_propagation_cost; if (m_mark[root] != DL_UNMARKED) { // negative cycle was found @@ -680,8 +681,14 @@ private: int m_total_count = 0; int m_run_counter = -1; svector m_hybrid_visited, m_hybrid_parent; + + bool is_connected(numeral const& gamma, bool zero_edge, edge const& e, unsigned timestamp) const { + return (gamma.is_one() || (!zero_edge && gamma.is_neg())) && e.get_timestamp() < timestamp; + } + public: + template bool find_path(dl_var source, dl_var target, unsigned timestamp, Functor & f) { auto zero_edge = true; @@ -713,13 +720,12 @@ public: continue; } set_gamma(e, gamma); - if ((gamma.is_one() || (!zero_edge && gamma.is_neg())) - && e.get_timestamp() < timestamp) { + if (is_connected(gamma, zero_edge, e, timestamp)) { dl_var curr_target = e.get_target(); if (curr_target == target) { f(e.get_explanation()); m_freq_hybrid[e_id]++; - for (;;) { + while (true) { int p = m_hybrid_parent[v]; if (p == -1) return true; @@ -981,12 +987,12 @@ public: } } - void display_edge(std::ostream & out, edge_id id) const { - display_edge(out, m_edges[id]); + std::ostream& display_edge(std::ostream & out, edge_id id) const { + return display_edge(out, m_edges[id]); } - void display_edge(std::ostream & out, const edge & e) const { - out << e.get_explanation() << " (<= (- $" << e.get_target() << " $" << e.get_source() << ") " << e.get_weight() << ") " << e.get_timestamp() << "\n"; + std::ostream& display_edge(std::ostream & out, const edge & e) const { + return out << e.get_explanation() << " (<= (- $" << e.get_target() << " $" << e.get_source() << ") " << e.get_weight() << ") " << e.get_timestamp() << "\n"; } template @@ -1233,17 +1239,11 @@ public: m_dfs_time[v] = 0; succ.push_back(v); numeral gamma; - for (unsigned i = 0; i < succ.size(); ++i) { - v = succ[i]; - edge_id_vector & edges = m_out_edges[v]; - for (edge_id e_id : edges) { - edge & e = m_edges[e_id]; - if (!e.is_enabled()) { - continue; - } - SASSERT(e.get_source() == v); - set_gamma(e, gamma); - if (gamma.is_zero()) { + for (dl_var w : succ) { + for (edge_id e_id : m_out_edges[w]) { + edge & e = m_edges[e_id]; + if (e.is_enabled() && set_gamma(e, gamma).is_zero()) { + SASSERT(e.get_source() == w); dl_var target = e.get_target(); if (m_dfs_time[target] == -1) { succ.push_back(target); @@ -1334,40 +1334,37 @@ private: m_edge_id(e) { } }; - + public: // Find the shortest path from source to target using (normalized) zero edges with timestamp less than the given timestamp. // The functor f is applied on every explanation attached to the edges in the shortest path. // Return true if the path exists, false otherwise. - - - // Return true if the path exists, false otherwise. - template - bool find_shortest_zero_edge_path(dl_var source, dl_var target, unsigned timestamp, Functor & f) { - return find_shortest_path_aux(source, target, timestamp, f, true); - } + + + // Return true if the path exists, false otherwise. + template + bool find_shortest_zero_edge_path(dl_var source, dl_var target, unsigned timestamp, Functor & f) { + return find_shortest_path_aux(source, target, timestamp, f, true); + } template bool find_shortest_reachable_path(dl_var source, dl_var target, unsigned timestamp, Functor & f) { return find_shortest_path_aux(source, target, timestamp, f, false); } - template bool find_shortest_path_aux(dl_var source, dl_var target, unsigned timestamp, Functor & f, bool zero_edge) { svector bfs_todo; - svector bfs_mark; + svector bfs_mark; bfs_mark.resize(m_assignment.size(), false); bfs_todo.push_back(bfs_elem(source, -1, null_edge_id)); bfs_mark[source] = true; - unsigned m_head = 0; numeral gamma; - while (m_head < bfs_todo.size()) { - bfs_elem & curr = bfs_todo[m_head]; - int parent_idx = m_head; - m_head++; + for (unsigned head = 0; head < bfs_todo.size(); ++head) { + bfs_elem & curr = bfs_todo[head]; + int parent_idx = head; dl_var v = curr.m_var; TRACE("dl_bfs", tout << "processing: " << v << "\n";); edge_id_vector & edges = m_out_edges[v]; @@ -1378,18 +1375,16 @@ public: continue; } set_gamma(e, gamma); - TRACE("dl_bfs", tout << "processing edge: "; display_edge(tout, e); tout << "gamma: " << gamma << "\n";); - if ((gamma.is_one() || (!zero_edge && gamma.is_neg())) && e.get_timestamp() < timestamp) { - // if (gamma.is_zero() && e.get_timestamp() < timestamp) + TRACE("dl_bfs", display_edge(tout << "processing edge: ", e) << " gamma: " << gamma << "\n";); + if (is_connected(gamma, zero_edge, e, timestamp)) { dl_var curr_target = e.get_target(); - TRACE("dl_bfs", tout << "curr_target: " << curr_target << - ", mark: " << static_cast(bfs_mark[curr_target]) << "\n";); + TRACE("dl_bfs", tout << "curr_target: " << curr_target << ", mark: " << bfs_mark[curr_target] << "\n";); if (curr_target == target) { TRACE("dl_bfs", tout << "found path\n";); TRACE("dl_eq_bug", tout << "path: " << source << " --> " << target << "\n"; display_edge(tout, e); int tmp_parent_idx = parent_idx; - for (;;) { + while (true) { bfs_elem & curr = bfs_todo[tmp_parent_idx]; if (curr.m_edge_id == null_edge_id) { break; @@ -1399,11 +1394,10 @@ public: display_edge(tout, e); tmp_parent_idx = curr.m_parent_idx; } - tout.flush(); }); TRACE("dl_eq_bug", display_edge(tout, e);); f(e.get_explanation()); - for (;;) { + while (true) { SASSERT(parent_idx >= 0); bfs_elem & curr = bfs_todo[parent_idx]; if (curr.m_edge_id == null_edge_id) { @@ -1417,11 +1411,9 @@ public: } } } - else { - if (!bfs_mark[curr_target]) { - bfs_todo.push_back(bfs_elem(curr_target, parent_idx, e_id)); - bfs_mark[curr_target] = true; - } + else if (!bfs_mark[curr_target]) { + bfs_todo.push_back(bfs_elem(curr_target, parent_idx, e_id)); + bfs_mark[curr_target] = true; } } } @@ -1507,8 +1499,7 @@ private: numeral get_reduced_weight(dfs_state& state, dl_var n, edge const& e) { numeral gamma; - set_gamma(e, gamma); - return state.m_delta[n] + gamma; + return state.m_delta[n] + set_gamma(e, gamma); } template diff --git a/src/smt/theory_special_relations.h b/src/smt/theory_special_relations.h index 90b6a7bbf..74e9d38bf 100644 --- a/src/smt/theory_special_relations.h +++ b/src/smt/theory_special_relations.h @@ -58,11 +58,11 @@ namespace smt { } bool_var var() const { return m_bvar;} relation& get_relation() const { return m_relation; } - bool phase() { return m_phase; } + bool phase() const { return m_phase; } void set_phase(bool b) { m_phase = b; } - theory_var v1() { return m_v1; } - theory_var v2() { return m_v2; } - literal explanation() { return literal(m_bvar, !m_phase); } + theory_var v1() const { return m_v1; } + theory_var v2() const { return m_v2; } + literal explanation() const { return literal(m_bvar, !m_phase); } bool enable() { edge_id edge = m_phase?m_pos:m_neg; return m_relation.m_graph.enable_edge(edge); @@ -112,16 +112,16 @@ namespace smt { typedef u_map bool_var2atom; special_relations_util m_util; - arith_util m_autil; - + arith_util m_autil; atoms m_atoms; unsigned_vector m_atoms_lim; obj_map m_relations; bool_var2atom m_bool_var2atom; scoped_ptr m_nested_solver; + struct atom_hash { - size_t operator()(atom a) const { + size_t operator()(atom const& a) const { return std::hash()(a.v1()) ^ std::hash()(a.v2()) ^ std::hash()(a.phase()); } }; @@ -158,6 +158,13 @@ namespace smt { bool is_strict_neighbour_edge(graph const& g, edge_id id) const; bool disconnected(graph const& g, dl_var u, dl_var v) const; + literal mk_literal(expr* _e); + enode* ensure_enode(expr* e); + theory_var mk_var(enode* n); + + void collect_asserted_po_atoms(vector< std::pair >& atoms) const; + void display_atom(std::ostream & out, atom& a) const; + public: theory_special_relations(ast_manager& m); ~theory_special_relations() override; @@ -182,13 +189,6 @@ namespace smt { bool can_propagate() override { return false; } void propagate() override {} void display(std::ostream & out) const override; - - literal mk_literal(expr* _e); - enode* ensure_enode(expr* e); - theory_var mk_var(enode* n); - - void collect_asserted_po_atoms( vector< std::pair >& atoms) const; - void display_atom( std::ostream & out, atom& a) const; }; } From e4bf1663b62bd4d8024e96d9eeecad66eae011b1 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 24 Mar 2019 20:47:02 -0700 Subject: [PATCH 05/19] na Signed-off-by: Nikolaj Bjorner --- src/smt/diff_logic.h | 2 +- src/smt/theory_special_relations.cpp | 110 +++++++++++---------------- 2 files changed, 46 insertions(+), 66 deletions(-) diff --git a/src/smt/diff_logic.h b/src/smt/diff_logic.h index 29b1050df..8544a2384 100644 --- a/src/smt/diff_logic.h +++ b/src/smt/diff_logic.h @@ -1365,7 +1365,7 @@ public: for (unsigned head = 0; head < bfs_todo.size(); ++head) { bfs_elem & curr = bfs_todo[head]; int parent_idx = head; - dl_var v = curr.m_var; + dl_var v = curr.m_var; TRACE("dl_bfs", tout << "processing: " << v << "\n";); edge_id_vector & edges = m_out_edges[v]; for (edge_id e_id : edges) { diff --git a/src/smt/theory_special_relations.cpp b/src/smt/theory_special_relations.cpp index e1a42403d..e0201c25c 100644 --- a/src/smt/theory_special_relations.cpp +++ b/src/smt/theory_special_relations.cpp @@ -157,23 +157,20 @@ namespace smt { final_check_status theory_special_relations::final_check_eh() { TRACE("special_relations", tout << "\n";); - obj_map::iterator it = m_relations.begin(), end = m_relations.end(); - lbool r = l_true; - for (; it != end && r == l_true; ++it) { - r = final_check(*it->m_value); + for (auto const& kv : m_relations) { + lbool r = final_check(*kv.m_value); + switch (r) { + case l_undef: + return FC_GIVEUP; + case l_false: + return FC_CONTINUE; + default: + break; + } } - switch (r) { - case l_undef: - return FC_GIVEUP; - case l_false: - return FC_CONTINUE; - default: - break; - } - it = m_relations.begin(); bool new_equality = false; - for (; it != end; ++it) { - if (extract_equalities(*it->m_value)) { + for (auto const& kv : m_relations) { + if (extract_equalities(*kv.m_value)) { new_equality = true; } } @@ -421,6 +418,7 @@ namespace smt { u_map> map; lbool res = l_true; + // TBD: non-functional code? for (atom * ap : r.m_asserted_atoms) { if (res != l_true) break; atom a = *ap; @@ -449,7 +447,7 @@ namespace smt { auto f = m.mk_implies( b, m.mk_not(literals.back()) ); m_nested_solver->assert_expr(f); - atom_cache.insert(b->get_id(), &a); + atom_cache.insert(b->get_id(), ap); assumptions.push_back(b); r.m_explanation.reset(); if (m_nested_solver->check_sat(assumptions.size(), assumptions.c_ptr()) == l_false) { @@ -496,9 +494,8 @@ namespace smt { } void theory_special_relations::reset_eh() { - obj_map::iterator it = m_relations.begin(), end = m_relations.end(); - for (; it != end; ++it) { - dealloc(it->m_value); + for (auto const& kv : m_relations) { + dealloc(kv.m_value); } m_relations.reset(); del_atoms(0); @@ -510,21 +507,18 @@ namespace smt { VERIFY(m_bool_var2atom.find(v, a)); a->set_phase(is_true); a->get_relation().m_asserted_atoms.push_back(a); - //std::cerr << "ASSIGN: " << a->v1() << ' ' << a->v2() << "\n"; } void theory_special_relations::push_scope_eh() { - obj_map::iterator it = m_relations.begin(), end = m_relations.end(); - for (; it != end; ++it) { - it->m_value->push(); + for (auto const& kv : m_relations) { + kv.m_value->push(); } m_atoms_lim.push_back(m_atoms.size()); } void theory_special_relations::pop_scope_eh(unsigned num_scopes) { - obj_map::iterator it = m_relations.begin(), end = m_relations.end(); - for (; it != end; ++it) { - it->m_value->pop(num_scopes); + for (auto const& kv : m_relations) { + kv.m_value->pop(num_scopes); } unsigned new_lvl = m_atoms_lim.size() - num_scopes; del_atoms(m_atoms_lim[new_lvl]); @@ -544,9 +538,8 @@ namespace smt { void theory_special_relations::collect_statistics(::statistics & st) const { - obj_map::iterator it = m_relations.begin(), end = m_relations.end(); - for (; it != end; ++it) { - it->m_value->m_graph.collect_statistics(st); + for (auto const& kv : m_relations) { + kv.m_value->m_graph.collect_statistics(st); } } @@ -613,9 +606,7 @@ namespace smt { if (g.get_assignment(u) <= val_v) { continue; } - int_vector const& edges = g.get_out_edges(u); - for (unsigned i = 0; i < edges.size(); ++i) { - edge_id e = edges[i]; + for (edge_id e : g.get_out_edges(u)) { if (is_strict_neighbour_edge(g, e)) { todo.push_back(g.get_target(e)); } @@ -773,9 +764,7 @@ namespace smt { } unsigned nc = 1; bool all_p = true; - int_vector const& edges = g.get_out_edges(v); - for (unsigned i = 0; i < edges.size(); ++i) { - edge_id e = edges[i]; + for (edge_id e : g.get_out_edges(v)) { if (is_strict_neighbour_edge(g, e)) { dl_var dst = g.get_target(e); TRACE("special_relations", tout << v << " -> " << dst << "\n";); @@ -839,23 +828,22 @@ namespace smt { } void theory_special_relations::init_model(model_generator & m) { - obj_map::iterator it = m_relations.begin(), end = m_relations.end(); - for (; it != end; ++it) { - switch (it->m_value->m_property) { + for (auto const& kv : m_relations) { + switch (kv.m_value->m_property) { case sr_lo: - init_model_lo(*it->m_value, m); + init_model_lo(*kv.m_value, m); break; case sr_plo: - init_model_plo(*it->m_value, m); + init_model_plo(*kv.m_value, m); break; case sr_to: - init_model_to(*it->m_value, m); + init_model_to(*kv.m_value, m); break; case sr_po: - init_model_po(*it->m_value, m); + init_model_po(*kv.m_value, m); break; default: - UNREACHABLE(); //ASHU: added to remove warning! Should be supported! + UNREACHABLE(); //ASHU: added to remove warning! Should be supported! } } } @@ -864,38 +852,30 @@ namespace smt { if (m_relations.empty()) return; out << "Theory Special Relations\n"; display_var2enode(out); - obj_map::iterator it = m_relations.begin(), end = m_relations.end(); - for (; it != end; ++it) { - out << mk_pp(it->m_value->decl(), get_manager()) << ":\n"; - it->m_value->m_graph.display(out); - it->m_value->m_uf.display(out); - for (unsigned i = 0; i < it->m_value->m_asserted_atoms.size(); ++i){ - atom& a = *it->m_value->m_asserted_atoms[i]; - display_atom( out, a ); + for (auto const& kv : m_relations) { + out << mk_pp(kv.m_value->decl(), get_manager()) << ":\n"; + kv.m_value->m_graph.display(out); + kv.m_value->m_uf.display(out); + for (atom* ap : kv.m_value->m_asserted_atoms) { + display_atom(out, *ap); } } } - void theory_special_relations::collect_asserted_po_atoms( vector< std::pair >& atoms) const { - obj_map::iterator it = m_relations.begin(), end = m_relations.end(); - for (; it != end; ++it) { - relation& r = *(it->m_value ); - if( r.m_property != sr_po ) continue; - // SASSERT( r.m_asserted_qhead == r.m_asserted_atoms.size() ); - for (unsigned i = 0; i < r.m_asserted_atoms.size(); ++i) { - atom& a = *r.m_asserted_atoms[i]; - atoms.push_back( std::make_pair(a.var(),a.phase()) ); + void theory_special_relations::collect_asserted_po_atoms(vector>& atoms) const { + for (auto const& kv : m_relations) { + relation& r = *kv.m_value; + if (r.m_property != sr_po) continue; + for (atom* ap : r.m_asserted_atoms) { + atoms.push_back(std::make_pair(ap->var(), ap->phase())); } } } - void theory_special_relations::display_atom( std::ostream & out, atom& a ) const { + void theory_special_relations::display_atom(std::ostream & out, atom& a) const { context& ctx = get_context(); expr* e = ctx.bool_var2expr( a.var() ); - if( !a.phase() ) out << "(not "; - out << mk_pp( e, get_manager()); - if( !a.phase() ) out << ")"; - out << "\n"; + out << (a.phase() ? "" : "(not ") << mk_pp(e, get_manager()) << (a.phase() ? "" : ")") << "\n"; } } From f83b32e6c3879e780555f119b60ba211db3f39c6 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 25 Mar 2019 03:36:30 -0700 Subject: [PATCH 06/19] remove unused code Signed-off-by: Nikolaj Bjorner --- src/smt/theory_special_relations.cpp | 110 +++++---------------------- src/smt/theory_special_relations.h | 12 --- 2 files changed, 17 insertions(+), 105 deletions(-) diff --git a/src/smt/theory_special_relations.cpp b/src/smt/theory_special_relations.cpp index e0201c25c..9e1579570 100644 --- a/src/smt/theory_special_relations.cpp +++ b/src/smt/theory_special_relations.cpp @@ -28,7 +28,6 @@ Notes: #include "ast/reg_decl_plugins.h" #include "ast/ast_pp.h" -static constexpr bool KVEC = false; static constexpr bool HYBRID_SEARCH = false; namespace smt { @@ -38,9 +37,7 @@ namespace smt { scope& s = m_scopes.back(); s.m_asserted_atoms_lim = m_asserted_atoms.size(); s.m_asserted_qhead_old = m_asserted_qhead; - if (!KVEC) { - m_graph.push(); - } + m_graph.push(); m_ufctx.get_trail_stack().push_scope(); } @@ -50,9 +47,7 @@ namespace smt { m_asserted_atoms.shrink(s.m_asserted_atoms_lim); m_asserted_qhead = s.m_asserted_qhead_old; m_scopes.shrink(new_lvl); - if (!KVEC) { - m_graph.pop(num_scopes); - } + m_graph.pop(num_scopes); m_ufctx.get_trail_stack().pop_scope(num_scopes); } @@ -75,17 +70,11 @@ namespace smt { theory_special_relations::theory_special_relations(ast_manager& m): theory(m.mk_family_id("special_relations")), - m_util(m), m_autil(m) { - params_ref params; - params.set_bool("model", true); - params.set_bool("unsat_core", true); - m_nested_solver = mk_smt_solver(m, params, symbol("QF_LRA")); - m_int_sort = m_autil.mk_real(); + m_util(m) { } theory_special_relations::~theory_special_relations() { reset_eh(); - m_nested_solver = nullptr; } theory * theory_special_relations::mk_fresh(context * new_ctx) { @@ -118,7 +107,7 @@ namespace smt { ctx.set_var_theory(v, get_id()); atom* a = alloc(atom, v, *r, v0, v1); m_atoms.push_back(a); - //std::cerr << "INTER : " << a->v1() << ' ' << a->v2() << ' ' << gate_ctx << "\n"; + TRACE("sr", tout << "INTER : " << a->v1() << ' ' << a->v2() << ' ' << gate_ctx << "\n";); m_bool_var2atom.insert(v, a); return true; } @@ -386,86 +375,22 @@ namespace smt { } lbool theory_special_relations::final_check_po(relation& r) { - if (!KVEC) { - lbool res = l_true; - for (unsigned i = 0; res == l_true && i < r.m_asserted_atoms.size(); ++i) { - atom& a = *r.m_asserted_atoms[i]; - if (!a.phase() && r.m_uf.find(a.v1()) == r.m_uf.find(a.v2())) { - // v1 !-> v2 - // find v1 -> v3 -> v4 -> v2 path - r.m_explanation.reset(); - unsigned timestamp = r.m_graph.get_timestamp(); - auto found_path = HYBRID_SEARCH ? - r.m_graph.find_path(a.v1(), a.v2(), timestamp, r) : - r.m_graph.find_shortest_reachable_path(a.v1(), a.v2(), timestamp, r); - if (found_path) { - r.m_explanation.push_back(a.explanation()); - set_conflict(r); - res = l_false; - } - } - } - return res; - } - context& ctx = get_context(); - ast_manager& m = ctx.get_manager(); - - ptr_vector assumptions; - ptr_vector literals; - - int k = 1; - static int curr_id = 100000; - - u_map> map; - lbool res = l_true; - // TBD: non-functional code? - for (atom * ap : r.m_asserted_atoms) { - if (res != l_true) break; - atom a = *ap; - if (a.phase()) { - continue; - // assumptions.push_back(b); - r.m_uf.merge(a.v1(), a.v2()); - } - } - for (atom * ap : r.m_asserted_atoms) { - if (res != l_true) break; - atom a = *ap; - if (a.phase()) - continue; - if (r.m_uf.find(a.v1()) != r.m_uf.find(a.v2())) { - continue; - } - populate_k_vars(a.v1(), k, map, curr_id, m, m_int_sort); - populate_k_vars(a.v2(), k, map, curr_id, m, m_int_sort); - - literals.push_back(m_autil.mk_lt(map[a.v1()][0], map[a.v2()][0])); - - auto bool_sort = m.mk_bool_sort(); - auto b_func = m.mk_const_decl(symbol(curr_id++), bool_sort); - auto b = m.mk_app(b_func, unsigned(0), nullptr); - - auto f = m.mk_implies( b, m.mk_not(literals.back()) ); - m_nested_solver->assert_expr(f); - atom_cache.insert(b->get_id(), ap); - assumptions.push_back(b); - r.m_explanation.reset(); - if (m_nested_solver->check_sat(assumptions.size(), assumptions.c_ptr()) == l_false) { - expr_ref_vector unsat_core(m); - m_nested_solver->get_unsat_core(unsat_core); - for (expr* e : unsat_core) { - atom& a = *atom_cache[e->get_id()]; + for (atom* ap : r.m_asserted_atoms) { + atom& a = *ap; + if (!a.phase() && r.m_uf.find(a.v1()) == r.m_uf.find(a.v2())) { + // v1 !-> v2 + // find v1 -> v3 -> v4 -> v2 path + r.m_explanation.reset(); + unsigned timestamp = r.m_graph.get_timestamp(); + bool found_path = r.m_graph.find_shortest_reachable_path(a.v1(), a.v2(), timestamp, r); + if (found_path) { r.m_explanation.push_back(a.explanation()); + set_conflict(r); + return l_false; } - for (auto e : r.m_explanation) { - std::cerr << "EX " << e.hash() << "\n"; - } - set_conflict(r); - res = l_false; } - assumptions.pop_back(); } - return res; + return l_true; } lbool theory_special_relations::propagate(relation& r) { @@ -503,8 +428,7 @@ namespace smt { void theory_special_relations::assign_eh(bool_var v, bool is_true) { TRACE("special_relations", tout << "assign bv" << v << " " << (is_true?" <- true":" <- false") << "\n";); - atom* a = 0; - VERIFY(m_bool_var2atom.find(v, a)); + atom* a = m_bool_var2atom[v]; a->set_phase(is_true); a->get_relation().m_asserted_atoms.push_back(a); } diff --git a/src/smt/theory_special_relations.h b/src/smt/theory_special_relations.h index 74e9d38bf..e9e5668f3 100644 --- a/src/smt/theory_special_relations.h +++ b/src/smt/theory_special_relations.h @@ -112,22 +112,10 @@ namespace smt { typedef u_map bool_var2atom; special_relations_util m_util; - arith_util m_autil; atoms m_atoms; unsigned_vector m_atoms_lim; obj_map m_relations; bool_var2atom m_bool_var2atom; - - scoped_ptr m_nested_solver; - - struct atom_hash { - size_t operator()(atom const& a) const { - return std::hash()(a.v1()) ^ std::hash()(a.v2()) ^ std::hash()(a.phase()); - } - }; - u_map expr_cache; - u_map atom_cache; - sort* m_int_sort; void del_atoms(unsigned old_size); lbool final_check(relation& r); From 31969b503729f12b15ef070f6e9101f187c8da7b Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 25 Mar 2019 04:43:47 -0700 Subject: [PATCH 07/19] tidy Signed-off-by: Nikolaj Bjorner --- src/smt/theory_special_relations.cpp | 103 +++++++++++---------------- src/smt/theory_special_relations.h | 13 +++- 2 files changed, 53 insertions(+), 63 deletions(-) diff --git a/src/smt/theory_special_relations.cpp b/src/smt/theory_special_relations.cpp index 9e1579570..95cfb410e 100644 --- a/src/smt/theory_special_relations.cpp +++ b/src/smt/theory_special_relations.cpp @@ -28,8 +28,6 @@ Notes: #include "ast/reg_decl_plugins.h" #include "ast/ast_pp.h" -static constexpr bool HYBRID_SEARCH = false; - namespace smt { void theory_special_relations::relation::push() { @@ -63,9 +61,7 @@ namespace smt { ensure_var(v2); literal_vector ls; ls.push_back(l); - return - m_graph.enable_edge(m_graph.add_edge(v1, v2, s_integer(1), ls)) && - m_graph.enable_edge(m_graph.add_edge(v2, v1, s_integer(1), ls)); + return m_graph.add_non_strict_edge(v1, v2, ls) && m_graph.add_non_strict_edge(v2, v1, ls); } theory_special_relations::theory_special_relations(ast_manager& m): @@ -81,22 +77,13 @@ namespace smt { return alloc(theory_special_relations, new_ctx->get_manager()); } - static void populate_k_vars(int v, int k, u_map>& map, int& curr_id, ast_manager& m, sort* int_sort) { - int need = !map.contains(v) ? k : k - map[v].size(); - for (auto i = 0; i < need; ++i) { - auto *fd = m.mk_const_decl(symbol(curr_id++), int_sort); - map[v].push_back(m.mk_app(fd, unsigned(0), nullptr)); - } - } - bool theory_special_relations::internalize_atom(app * atm, bool gate_ctx) { - TRACE("special_relations", tout << mk_pp(atm, get_manager()) << "\n";); SASSERT(m_util.is_special_relation(atm)); relation* r = 0; if (!m_relations.find(atm->get_decl(), r)) { - //todo: push pop may get misaligned if the following alloc happens after push r = alloc(relation, m_util.get_property(atm), atm->get_decl()); m_relations.insert(atm->get_decl(), r); + for (unsigned i = 0; i < m_atoms_lim.size(); ++i) r->push(); } context& ctx = get_context(); expr* arg0 = atm->get_arg(0); @@ -107,7 +94,7 @@ namespace smt { ctx.set_var_theory(v, get_id()); atom* a = alloc(atom, v, *r, v0, v1); m_atoms.push_back(a); - TRACE("sr", tout << "INTER : " << a->v1() << ' ' << a->v2() << ' ' << gate_ctx << "\n";); + TRACE("special_relations", tout << mk_pp(atm, get_manager()) << " : " << a->v1() << ' ' << a->v2() << ' ' << gate_ctx << "\n";); m_bool_var2atom.insert(v, a); return true; } @@ -222,42 +209,39 @@ namespace smt { lbool theory_special_relations::final_check_to(relation& r) { uint_set visited, target; - lbool res = l_true; - for (unsigned i = 0; res == l_true && i < r.m_asserted_atoms.size(); ++i) { - atom& a = *r.m_asserted_atoms[i]; - if (!a.phase() && r.m_uf.find(a.v1()) == r.m_uf.find(a.v2())) { - target.reset(); - theory_var w; - // v2 !<= v1 is asserted - target.insert(a.v2()); - if (r.m_graph.reachable(a.v1(), visited, target, w)) { - // we already have v1 <= v2 - continue; + for (atom* ap : r.m_asserted_atoms) { + atom& a = *ap; + if (a.phase() || r.m_uf.find(a.v1()) != r.m_uf.find(a.v2())) { + continue; + } + target.reset(); + theory_var w; + // v2 !<= v1 is asserted + target.insert(a.v2()); + if (r.m_graph.reachable(a.v1(), visited, target, w)) { + // we already have v1 <= v2 + continue; + } + target.reset(); + if (r.m_graph.reachable(a.v2(), target, visited, w)) { + // there is a common successor + // v1 <= w + // v2 <= w + // v1 !<= v2 + // -> v1 <= w & v2 <= w & v1 !<= v2 -> v2 <= v1 + unsigned timestamp = r.m_graph.get_timestamp(); + r.m_explanation.reset(); + r.m_graph.find_shortest_reachable_path(a.v1(), w, timestamp, r); + r.m_graph.find_shortest_reachable_path(a.v2(), w, timestamp, r); + r.m_explanation.push_back(a.explanation()); + literal_vector const& lits = r.m_explanation; + if (!r.m_graph.add_non_strict_edge(a.v2(), a.v1(), lits)) { + set_neg_cycle_conflict(r); + return l_false; } - target.reset(); - if (r.m_graph.reachable(a.v2(), target, visited, w)) { - // there is a common successor - // v1 <= w - // v2 <= w - // v1 !<= v2 - // -> v1 <= w & v2 <= w & v1 !<= v2 -> v2 <= v1 - unsigned timestamp = r.m_graph.get_timestamp(); - r.m_explanation.reset(); - r.m_graph.find_shortest_reachable_path(a.v1(), w, timestamp, r); - r.m_graph.find_shortest_reachable_path(a.v2(), w, timestamp, r); - r.m_explanation.push_back(a.explanation()); - literal_vector const& lits = r.m_explanation; - if (!r.m_graph.enable_edge(r.m_graph.add_edge(a.v2(), a.v1(), s_integer(0), lits))) { - set_neg_cycle_conflict(r); - res = l_false; - } - } - // TODO: check if algorithm correctly produces all constraints. - // e.g., if we add an edge, do we have to repeat the loop? - // } } - return res; + return l_true; } lbool theory_special_relations::enable(atom& a) { @@ -289,12 +273,6 @@ namespace smt { } lbool theory_special_relations::final_check(relation& r) { - // timer m_timer_fc; //for debugging - // static unsigned call_count = 0; - // static double total_call_times = 0.0; - // m_timer_fc.start(); - // call_count++; - lbool res = propagate(r); if (res != l_true) return res; switch (r.m_property) { @@ -446,6 +424,7 @@ namespace smt { } unsigned new_lvl = m_atoms_lim.size() - num_scopes; del_atoms(m_atoms_lim[new_lvl]); + m_atoms_lim.shrink(new_lvl); } void theory_special_relations::del_atoms(unsigned old_size) { @@ -453,7 +432,7 @@ namespace smt { atoms::iterator it = m_atoms.end(); while (it != begin) { --it; - atom * a = *it; + atom* a = *it; m_bool_var2atom.erase(a->var()); dealloc(a); } @@ -469,7 +448,7 @@ namespace smt { model_value_proc * theory_special_relations::mk_value(enode * n, model_generator & mg) { UNREACHABLE(); - return 0; + return nullptr; } void theory_special_relations::ensure_strict(graph& g) { @@ -480,7 +459,7 @@ namespace smt { dl_var src = g.get_source(i); dl_var dst = g.get_target(i); if (get_enode(src)->get_root() == get_enode(dst)->get_root()) continue; - VERIFY(g.enable_edge(g.add_edge(src, dst, s_integer(-2), literal_vector()))); + VERIFY(g.add_strict_edge(src, dst, literal_vector())); } TRACE("special_relations", g.display(tout);); } @@ -498,9 +477,10 @@ namespace smt { edge_id e2 = edges[k]; if (g.is_enabled(e2)) { dl_var src2 = g.get_source(e2); - if (get_enode(src1)->get_root() == get_enode(src2)->get_root()) continue; - if (!disconnected(g, src1, src2)) continue; - VERIFY(g.enable_edge(g.add_edge(src1, src2, s_integer(-2), literal_vector()))); + if (get_enode(src1)->get_root() != get_enode(src2)->get_root() && + disconnected(g, src1, src2)) { + VERIFY(g.add_strict_edge(src1, src2, literal_vector())); + } } } } @@ -587,7 +567,6 @@ namespace smt { expr_ref theory_special_relations::mk_interval(relation& r, model_generator& mg, unsigned_vector & lo, unsigned_vector& hi) { graph const& g = r.m_graph; - //context& ctx = get_context(); ast_manager& m = get_manager(); expr_ref result(m); func_decl_ref lofn(m), hifn(m); diff --git a/src/smt/theory_special_relations.h b/src/smt/theory_special_relations.h index e9e5668f3..7c243dee0 100644 --- a/src/smt/theory_special_relations.h +++ b/src/smt/theory_special_relations.h @@ -78,7 +78,14 @@ namespace smt { struct int_ext : public sidl_ext { typedef literal_vector explanation; }; - typedef dl_graph graph; + struct graph : public dl_graph { + bool add_strict_edge(theory_var v1, theory_var v2, literal_vector const& j) { + return enable_edge(add_edge(v1, v2, s_integer(1), j)); + } + bool add_non_strict_edge(theory_var v1, theory_var v2, literal_vector const& j) { + return enable_edge(add_edge(v1, v2, s_integer(-2), j)); + } + }; typedef union_find union_find_t; @@ -104,6 +111,9 @@ namespace smt { m_explanation.append(ex); } void new_edge(dl_var src, dl_var dst, unsigned num_edges, edge_id const* edges) {} + + bool add_strict_edge(theory_var v1, theory_var v2, literal_vector const& j); + bool add_non_strict_edge(theory_var v1, theory_var v2, literal_vector const& j); }; @@ -117,6 +127,7 @@ namespace smt { obj_map m_relations; bool_var2atom m_bool_var2atom; + void del_atoms(unsigned old_size); lbool final_check(relation& r); lbool final_check_po(relation& r); From dd9aec55527413182da1f3a4d31e129d02fdb88d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 25 Mar 2019 10:40:08 -0700 Subject: [PATCH 08/19] nits Signed-off-by: Nikolaj Bjorner --- src/smt/theory_special_relations.cpp | 15 ++++----------- src/smt/theory_special_relations.h | 10 +++++----- 2 files changed, 9 insertions(+), 16 deletions(-) diff --git a/src/smt/theory_special_relations.cpp b/src/smt/theory_special_relations.cpp index 95cfb410e..03066f766 100644 --- a/src/smt/theory_special_relations.cpp +++ b/src/smt/theory_special_relations.cpp @@ -115,15 +115,11 @@ namespace smt { void theory_special_relations::new_eq_eh(theory_var v1, theory_var v2) { context& ctx = get_context(); - app_ref eq(get_manager()); app* t1 = get_enode(v1)->get_owner(); app* t2 = get_enode(v2)->get_owner(); - eq = get_manager().mk_eq(t1, t2); - VERIFY(internalize_atom(eq, false)); - literal l(ctx.get_literal(eq)); - obj_map::iterator it = m_relations.begin(), end = m_relations.end(); - for (; !ctx.inconsistent() && it != end; ++it) { - relation& r = *it->m_value; + literal eq = mk_eq(t1, t2, false); + for (auto const& kv : m_relations) { + relation& r = *kv.m_value; if (!r.new_eq_eh(l, v1, v2)) { set_neg_cycle_conflict(r); break; @@ -175,9 +171,8 @@ namespace smt { literal theory_special_relations::mk_literal(expr* _e) { expr_ref e(_e, get_manager()); - context& ctx = get_context(); ensure_enode(e); - return ctx.get_literal(e); + return get_context().get_literal(e); } theory_var theory_special_relations::mk_var(enode* n) { @@ -520,7 +515,6 @@ namespace smt { } expr_ref theory_special_relations::mk_inj(relation& r, model_generator& mg) { - // context& ctx = get_context(); ast_manager& m = get_manager(); r.push(); ensure_strict(r.m_graph); @@ -545,7 +539,6 @@ namespace smt { } expr_ref theory_special_relations::mk_class(relation& r, model_generator& mg) { - //context& ctx = get_context(); ast_manager& m = get_manager(); expr_ref result(m); func_decl_ref fn(m); diff --git a/src/smt/theory_special_relations.h b/src/smt/theory_special_relations.h index 7c243dee0..01314b362 100644 --- a/src/smt/theory_special_relations.h +++ b/src/smt/theory_special_relations.h @@ -17,14 +17,14 @@ Notes: --*/ +#ifndef THEORY_SPECIAL_RELATIONS_H_ +#define THEORY_SPECIAL_RELATIONS_H_ + #include "ast/special_relations_decl_plugin.h" #include "smt/smt_theory.h" #include "smt/theory_diff_logic.h" #include "util/union_find.h" -#include "solver/solver.h" - -#ifndef THEORY_SPECIAL_RELATIONS_H_ -#define THEORY_SPECIAL_RELATIONS_H_ +#include "util/rational.h" namespace smt { class theory_special_relations : public theory { @@ -140,7 +140,7 @@ namespace smt { void set_neg_cycle_conflict(relation& r); void set_conflict(relation& r); lbool propagate_plo(atom& a); - lbool propagate_po(atom& a); //ASHU: added to modify po solving + lbool propagate_po(atom& a); theory_var mk_var(expr* e); void count_children(graph const& g, unsigned_vector& num_children); void ensure_strict(graph& g); From 1634a21e75e9c2f7414dc9f9a979b695ac24bf07 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 25 Mar 2019 10:43:29 -0700 Subject: [PATCH 09/19] l -> eq Signed-off-by: Nikolaj Bjorner --- src/smt/theory_special_relations.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/smt/theory_special_relations.cpp b/src/smt/theory_special_relations.cpp index 03066f766..3750ce967 100644 --- a/src/smt/theory_special_relations.cpp +++ b/src/smt/theory_special_relations.cpp @@ -120,7 +120,7 @@ namespace smt { literal eq = mk_eq(t1, t2, false); for (auto const& kv : m_relations) { relation& r = *kv.m_value; - if (!r.new_eq_eh(l, v1, v2)) { + if (!r.new_eq_eh(eq, v1, v2)) { set_neg_cycle_conflict(r); break; } From c4b4744ae90322f537a6d933a61affab4e9088e4 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 25 Mar 2019 13:13:50 -0700 Subject: [PATCH 10/19] e_id3 Signed-off-by: Nikolaj Bjorner --- src/smt/diff_logic.h | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/smt/diff_logic.h b/src/smt/diff_logic.h index 8544a2384..8332baaf4 100644 --- a/src/smt/diff_logic.h +++ b/src/smt/diff_logic.h @@ -1775,7 +1775,7 @@ public: continue; } w2 = e2.get_weight() + w; - for (edge_id e_id2 : m_in_edges[e2.get_target()]) { + for (edge_id e_id3 : m_in_edges[e2.get_target()]) { ++m_stats.m_implied_literal_cost; edge const& e3 = m_edges[e_id3]; if (e3.is_enabled() || e3.get_source() != src) { From 48e0626ffebc97e0bcacd08b07deb1a22051b302 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 25 Mar 2019 17:42:27 -0700 Subject: [PATCH 11/19] add API Signed-off-by: Nikolaj Bjorner --- src/api/CMakeLists.txt | 1 + src/api/api_ast.cpp | 12 +++++ src/api/api_context.cpp | 1 + src/api/api_context.h | 3 ++ src/api/api_special_relations.cpp | 78 ++++++++++++++++++++++++++++ src/api/c++/z3++.h | 36 +++++++++++++ src/api/z3_api.h | 57 +++++++++++++++++++- src/smt/diff_logic.h | 9 ++-- src/smt/theory_special_relations.cpp | 31 ++++++----- src/smt/theory_special_relations.h | 22 ++++---- 10 files changed, 223 insertions(+), 27 deletions(-) create mode 100644 src/api/api_special_relations.cpp diff --git a/src/api/CMakeLists.txt b/src/api/CMakeLists.txt index 4a5514a7b..247d0a14c 100644 --- a/src/api/CMakeLists.txt +++ b/src/api/CMakeLists.txt @@ -61,6 +61,7 @@ z3_add_component(api api_rcf.cpp api_seq.cpp api_solver.cpp + api_special_relations.cpp api_stats.cpp api_tactic.cpp z3_replayer.cpp diff --git a/src/api/api_ast.cpp b/src/api/api_ast.cpp index cabfdb101..a8f62572a 100644 --- a/src/api/api_ast.cpp +++ b/src/api/api_ast.cpp @@ -1052,6 +1052,18 @@ extern "C" { } } + if (mk_c(c)->get_special_relations_fid() == _d->get_family_id()) { + switch(_d->get_decl_kind()) { + case OP_SPECIAL_RELATION_LO : return Z3_OP_SPECIAL_RELATION_LO; + case OP_SPECIAL_RELATION_PO : return Z3_OP_SPECIAL_RELATION_PO; + case OP_SPECIAL_RELATION_PO_AO : return Z3_OP_SPECIAL_RELATION_PO_AO; + case OP_SPECIAL_RELATION_PLO: return Z3_OP_SPECIAL_RELATION_PLO; + case OP_SPECIAL_RELATION_TO : return Z3_OP_SPECIAL_RELATION_TO; + default: UNREACHABLE(); + } + } + + if (mk_c(c)->get_bv_fid() == _d->get_family_id()) { switch(_d->get_decl_kind()) { case OP_BV_NUM: return Z3_OP_BNUM; diff --git a/src/api/api_context.cpp b/src/api/api_context.cpp index 71bebef73..811cb30ee 100644 --- a/src/api/api_context.cpp +++ b/src/api/api_context.cpp @@ -101,6 +101,7 @@ namespace api { m_datalog_fid = m().mk_family_id("datalog_relation"); m_fpa_fid = m().mk_family_id("fpa"); m_seq_fid = m().mk_family_id("seq"); + m_special_relations_fid = m().mk_family_id("special_relations"); m_dt_plugin = static_cast(m().get_plugin(m_dt_fid)); install_tactics(*this); diff --git a/src/api/api_context.h b/src/api/api_context.h index 8bd75aaa0..1c4145810 100644 --- a/src/api/api_context.h +++ b/src/api/api_context.h @@ -30,6 +30,7 @@ Revision History: #include "ast/dl_decl_plugin.h" #include "ast/fpa_decl_plugin.h" #include "ast/recfun_decl_plugin.h" +#include "ast/special_relations_decl_plugin.h" #include "smt/smt_kernel.h" #include "smt/params/smt_params.h" #include "util/event_handler.h" @@ -106,6 +107,7 @@ namespace api { family_id m_pb_fid; family_id m_fpa_fid; family_id m_seq_fid; + family_id m_special_relations_fid; datatype_decl_plugin * m_dt_plugin; std::string m_string_buffer; // temporary buffer used to cache strings sent to the "external" world. @@ -162,6 +164,7 @@ namespace api { family_id get_fpa_fid() const { return m_fpa_fid; } family_id get_seq_fid() const { return m_seq_fid; } datatype_decl_plugin * get_dt_plugin() const { return m_dt_plugin; } + family_id get_special_relations_fid() const { return m_special_relations_fid; } Z3_error_code get_error_code() const { return m_error_code; } void reset_error_code(); diff --git a/src/api/api_special_relations.cpp b/src/api/api_special_relations.cpp new file mode 100644 index 000000000..40fde5083 --- /dev/null +++ b/src/api/api_special_relations.cpp @@ -0,0 +1,78 @@ +/*++ +Copyright (c) 2019 Microsoft Corporation + +Module Name: + + api_special_relations.cpp + +Abstract: + Basic API for Special relations + +Author: + + Nikolaj Bjorner (nbjorner) 2019-03-25 + Ashutosh Gupta 2016 + +Revision History: + +--*/ + +#include +#include "api/z3.h" +#include "api/api_log_macros.h" +#include "api/api_context.h" +#include "api/api_util.h" +#include "ast/ast_pp.h" +#include "ast/special_relations_decl_plugin.h" + +extern "C" { + +#if 0 + bool Z3_API Z3_is_sr_lo(Z3_context c, Z3_ast s) { + Z3_TRY; + LOG_Z3_is_sr_lo(c, s); + RESET_ERROR_CODE(); + RETURN_Z3(mk_c(c)->sr_util().is_lo( to_expr(s) )); + Z3_CATCH_RETURN(false); + } + + bool Z3_API Z3_is_sr_po(Z3_context c, Z3_ast s) { + Z3_TRY; + LOG_Z3_is_sr_po(c, s); + RESET_ERROR_CODE(); + RETURN_Z3(mk_c(c)->sr_util().is_po( to_expr(s) )); + Z3_CATCH_RETURN(false); + } + + bool Z3_API Z3_is_sr_po_ao(Z3_context c, Z3_ast s) { + Z3_TRY; + LOG_Z3_is_sr_po_ao(c, s); + RESET_ERROR_CODE(); + RETURN_Z3(mk_c(c)->sr_util().is_po_ao( to_expr(s) )); + Z3_CATCH_RETURN(false); + } + + bool Z3_API Z3_is_sr_plo(Z3_context c, Z3_ast s) { + Z3_TRY; + LOG_Z3_is_sr_plo(c, s); + RESET_ERROR_CODE(); + RETURN_Z3(mk_c(c)->sr_util().is_plo( to_expr(s) )); + Z3_CATCH_RETURN(false); + } + + bool Z3_API Z3_is_sr_to(Z3_context c, Z3_ast s) { + Z3_TRY; + LOG_Z3_is_sr_to(c, s); + RESET_ERROR_CODE(); + RETURN_Z3(mk_c(c)->sr_util().is_to( to_expr(s) )); + Z3_CATCH_RETURN(false); + } +#endif + + MK_BINARY(Z3_mk_sr_lo , mk_c(c)->get_special_relations_fid(), OP_SPECIAL_RELATION_LO, SKIP); + MK_BINARY(Z3_mk_sr_po , mk_c(c)->get_special_relations_fid(), OP_SPECIAL_RELATION_PO, SKIP); + MK_BINARY(Z3_mk_sr_po_ao,mk_c(c)->get_special_relations_fid(), OP_SPECIAL_RELATION_PO_AO,SKIP); + MK_BINARY(Z3_mk_sr_plo, mk_c(c)->get_special_relations_fid(), OP_SPECIAL_RELATION_PLO, SKIP); + MK_BINARY(Z3_mk_sr_to , mk_c(c)->get_special_relations_fid(), OP_SPECIAL_RELATION_TO, SKIP); + +}; diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index 4992015de..e18ca9204 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -1707,6 +1707,42 @@ namespace z3 { */ inline expr sext(expr const & a, unsigned i) { return to_expr(a.ctx(), Z3_mk_sign_ext(a.ctx(), i, a)); } + inline expr sr_lo(expr const& a, expr const& b) { + check_context(a, b); + Z3_ast r = Z3_mk_sr_lo(a.ctx(), a, b); + a.check_error(); + return expr(a.ctx(), r); + } + + inline expr sr_po(expr const& a, expr const& b) { + check_context(a, b); + Z3_ast r = Z3_mk_sr_po(a.ctx(), a, b); + a.check_error(); + return expr(a.ctx(), r); + } + + inline expr sr_po_ao(expr const& a, expr const& b) { + check_context(a, b); + Z3_ast r = Z3_mk_sr_po_ao(a.ctx(), a, b); + a.check_error(); + return expr(a.ctx(), r); + } + + inline expr sr_plo(expr const& a, expr const& b) { + check_context(a, b); + Z3_ast r = Z3_mk_sr_plo(a.ctx(), a, b); + a.check_error(); + return expr(a.ctx(), r); + } + + inline expr sr_to(expr const& a, expr const& b) { + check_context(a, b); + Z3_ast r = Z3_mk_sr_to(a.ctx(), a, b); + a.check_error(); + return expr(a.ctx(), r); + } + + template class cast_ast; template<> class cast_ast { diff --git a/src/api/z3_api.h b/src/api/z3_api.h index e17378d94..6d1db22b3 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -1101,6 +1101,13 @@ typedef enum { Z3_OP_BUREM_I, Z3_OP_BSMOD_I, + // Special relations + Z3_OP_SPECIAL_RELATION_LO, + Z3_OP_SPECIAL_RELATION_PO, + Z3_OP_SPECIAL_RELATION_PO_AO, + Z3_OP_SPECIAL_RELATION_PLO, + Z3_OP_SPECIAL_RELATION_TO, + // Proofs Z3_OP_PR_UNDEF = 0x500, Z3_OP_PR_TRUE, @@ -3595,10 +3602,58 @@ extern "C" { */ Z3_ast Z3_API Z3_mk_re_full(Z3_context c, Z3_sort re); - /*@}*/ + /** @name Special relations */ + /*@{*/ + /** + \brief declare \c a and \c b are in linear order. + + \pre a and b are of same type. + + def_API('Z3_mk_sr_lo', AST ,(_in(CONTEXT), _in(AST), _in(AST))) + */ + Z3_ast Z3_API Z3_mk_sr_lo(Z3_context c, Z3_ast a, Z3_ast b); + + /** + \brief declare \c a and \c b are in partial order. + + \pre a and b are of same type. + + def_API('Z3_mk_sr_po', AST ,(_in(CONTEXT), _in(AST), _in(AST))) + */ + Z3_ast Z3_API Z3_mk_sr_po(Z3_context c, Z3_ast a, Z3_ast b); + + /** + \brief declare \c a and \c b are already partial ordered. + + \pre a and b are of same type. + + def_API('Z3_mk_sr_po_ao', AST ,(_in(CONTEXT), _in(AST), _in(AST))) + */ + Z3_ast Z3_API Z3_mk_sr_po_ao(Z3_context c, Z3_ast a, Z3_ast b); + + /** + \brief declare \c a and \c b are in piecewise linear order. + + \pre a and b are of same type. + + def_API('Z3_mk_sr_plo', AST ,(_in(CONTEXT), _in(AST), _in(AST))) + */ + Z3_ast Z3_API Z3_mk_sr_plo(Z3_context c, Z3_ast a, Z3_ast b); + + /** + \brief declare \c a and \c b are in total order. + + \pre a and b are of same type. + + def_API('Z3_mk_sr_to', AST ,(_in(CONTEXT), _in(AST), _in(AST))) + */ + Z3_ast Z3_API Z3_mk_sr_to(Z3_context c, Z3_ast a, Z3_ast b); + + /*@}*/ + /** @name Quantifiers */ /*@{*/ /** diff --git a/src/smt/diff_logic.h b/src/smt/diff_logic.h index 8332baaf4..605390cf1 100644 --- a/src/smt/diff_logic.h +++ b/src/smt/diff_logic.h @@ -683,9 +683,12 @@ private: svector m_hybrid_visited, m_hybrid_parent; bool is_connected(numeral const& gamma, bool zero_edge, edge const& e, unsigned timestamp) const { - return (gamma.is_one() || (!zero_edge && gamma.is_neg())) && e.get_timestamp() < timestamp; + return (gamma.is_zero() || (!zero_edge && gamma.is_neg())) && e.get_timestamp() < timestamp; } + int_vector bfs_todo; + int_vector dfs_todo; + public: @@ -693,8 +696,8 @@ public: bool find_path(dl_var source, dl_var target, unsigned timestamp, Functor & f) { auto zero_edge = true; unsigned bfs_head = 0; - int_vector bfs_todo; - int_vector dfs_todo; + bfs_todo.reset(); + dfs_todo.reset(); m_hybrid_visited.resize(m_assignment.size(), m_run_counter++); m_hybrid_parent.resize(m_assignment.size(), -1); bfs_todo.push_back(source); diff --git a/src/smt/theory_special_relations.cpp b/src/smt/theory_special_relations.cpp index 3750ce967..a4c73028e 100644 --- a/src/smt/theory_special_relations.cpp +++ b/src/smt/theory_special_relations.cpp @@ -213,17 +213,21 @@ namespace smt { theory_var w; // v2 !<= v1 is asserted target.insert(a.v2()); - if (r.m_graph.reachable(a.v1(), visited, target, w)) { + if (r.m_graph.reachable(a.v1(), target, visited, w)) { // we already have v1 <= v2 continue; } - target.reset(); - if (r.m_graph.reachable(a.v2(), target, visited, w)) { - // there is a common successor + // the nodes visited from v1 become target for v2 + if (r.m_graph.reachable(a.v2(), visited, target, w)) { + // we have the following: // v1 <= w // v2 <= w // v1 !<= v2 - // -> v1 <= w & v2 <= w & v1 !<= v2 -> v2 <= v1 + // + // enforce the assertion + // + // v1 <= w & v2 <= w & v1 !<= v2 -> v2 <= v1 + // unsigned timestamp = r.m_graph.get_timestamp(); r.m_explanation.reset(); r.m_graph.find_shortest_reachable_path(a.v1(), w, timestamp, r); @@ -297,7 +301,7 @@ namespace smt { u_map roots; context& ctx = get_context(); r.m_graph.compute_zero_edge_scc(scc_id); - for (unsigned i = 0, j = 0; i < scc_id.size(); ++i) { + for (unsigned i = 0, j = 0; !ctx.inconsistent() && i < scc_id.size(); ++i) { if (scc_id[i] == -1) { continue; } @@ -635,11 +639,11 @@ namespace smt { bool theory_special_relations::is_neighbour_edge(graph const& g, edge_id edge) const { CTRACE("special_relations_verbose", g.is_enabled(edge), tout << edge << ": " << g.get_source(edge) << " " << g.get_target(edge) << " "; - tout << (g.get_assignment(g.get_source(edge)) - g.get_assignment(g.get_target(edge))) << "\n";); + tout << (g.get_assignment(g.get_target(edge)) - g.get_assignment(g.get_source(edge))) << "\n";); return g.is_enabled(edge) && - g.get_assignment(g.get_source(edge)) - g.get_assignment(g.get_target(edge)) == s_integer(1); + g.get_assignment(g.get_source(edge)) + s_integer(1) == g.get_assignment(g.get_target(edge)); } bool theory_special_relations::is_strict_neighbour_edge(graph const& g, edge_id e) const { @@ -650,7 +654,7 @@ namespace smt { unsigned sz = g.get_num_nodes(); svector nodes; num_children.resize(sz, 0); - svector processed(sz, false); + svector processed(sz, false); for (unsigned i = 0; i < sz; ++i) nodes.push_back(i); while (!nodes.empty()) { dl_var v = nodes.back(); @@ -692,8 +696,8 @@ namespace smt { for (unsigned i = 0; i < sz; ++i) { bool is_root = true; int_vector const& edges = g.get_in_edges(i); - for (unsigned j = 0; is_root && j < edges.size(); ++j) { - is_root = !g.is_enabled(edges[j]); + for (edge_id e_id : edges) { + is_root &= !g.is_enabled(e_id); } if (is_root) { lo[i] = offset; @@ -739,7 +743,8 @@ namespace smt { init_model_po(*kv.m_value, m); break; default: - UNREACHABLE(); //ASHU: added to remove warning! Should be supported! + // other 28 combinations of 0x1F + NOT_IMPLEMENTED_YET(); } } } @@ -770,7 +775,7 @@ namespace smt { void theory_special_relations::display_atom(std::ostream & out, atom& a) const { context& ctx = get_context(); - expr* e = ctx.bool_var2expr( a.var() ); + expr* e = ctx.bool_var2expr(a.var()); out << (a.phase() ? "" : "(not ") << mk_pp(e, get_manager()) << (a.phase() ? "" : ")") << "\n"; } diff --git a/src/smt/theory_special_relations.h b/src/smt/theory_special_relations.h index 01314b362..312d0d20b 100644 --- a/src/smt/theory_special_relations.h +++ b/src/smt/theory_special_relations.h @@ -52,9 +52,9 @@ namespace smt { r.ensure_var(v2); literal_vector ls; ls.push_back(literal(b, false)); - m_pos = r.m_graph.add_edge(v1, v2, s_integer(1), ls); // v2 <= v1 + m_pos = r.m_graph.add_edge(v1, v2, s_integer(0), ls); // v1 <= v2 ls[0] = literal(b, true); - m_neg = r.m_graph.add_edge(v2, v1, s_integer(-2), ls); // v1 <= v2 - 1 + m_neg = r.m_graph.add_edge(v2, v1, s_integer(-1), ls); // v2 + 1 <= v1 } bool_var var() const { return m_bvar;} relation& get_relation() const { return m_relation; } @@ -80,22 +80,24 @@ namespace smt { }; struct graph : public dl_graph { bool add_strict_edge(theory_var v1, theory_var v2, literal_vector const& j) { - return enable_edge(add_edge(v1, v2, s_integer(1), j)); + // v1 + 1 <= v2 + return enable_edge(add_edge(v1, v2, s_integer(-1), j)); } bool add_non_strict_edge(theory_var v1, theory_var v2, literal_vector const& j) { - return enable_edge(add_edge(v1, v2, s_integer(-2), j)); + // v1 <= v2 + return enable_edge(add_edge(v1, v2, s_integer(0), j)); } }; typedef union_find union_find_t; struct relation { - sr_property m_property; - func_decl* m_decl; - atoms m_asserted_atoms; // set of asserted atoms - unsigned m_asserted_qhead; - svector m_scopes; - graph m_graph; + sr_property m_property; + func_decl* m_decl; + atoms m_asserted_atoms; // set of asserted atoms + unsigned m_asserted_qhead; + svector m_scopes; + graph m_graph; union_find_default_ctx m_ufctx; union_find_t m_uf; literal_vector m_explanation; From 76cd8367dcdea9dafe7e9a0c1661a41210cf20ca Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 25 Mar 2019 17:51:15 -0700 Subject: [PATCH 12/19] adding cmd_context Signed-off-by: Nikolaj Bjorner --- src/api/python/z3/z3.py | 3 +++ src/cmd_context/cmd_context.cpp | 3 +++ src/smt/smt_setup.cpp | 6 ++++++ src/smt/smt_setup.h | 1 + 4 files changed, 13 insertions(+) diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index e3995ddb5..267a24a20 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -10353,3 +10353,6 @@ def Range(lo, hi, ctx = None): lo = _coerce_seq(lo, ctx) hi = _coerce_seq(hi, ctx) return ReRef(Z3_mk_re_range(lo.ctx_ref(), lo.ast, hi.ast), lo.ctx) + +# Special Relations + diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp index 9de183ca8..9fbeced71 100644 --- a/src/cmd_context/cmd_context.cpp +++ b/src/cmd_context/cmd_context.cpp @@ -31,6 +31,7 @@ Notes: #include "ast/pb_decl_plugin.h" #include "ast/fpa_decl_plugin.h" #include "ast/csp_decl_plugin.h" +#include "ast/special_relations_decl_plugin.h" #include "ast/ast_pp.h" #include "ast/rewriter/var_subst.h" #include "ast/pp.h" @@ -687,6 +688,7 @@ void cmd_context::init_manager_core(bool new_manager) { register_plugin(symbol("fpa"), alloc(fpa_decl_plugin), logic_has_fpa()); register_plugin(symbol("datalog_relation"), alloc(datalog::dl_decl_plugin), !has_logic()); register_plugin(symbol("csp"), alloc(csp_decl_plugin), smt_logics::logic_is_csp(m_logic)); + register_plugin(symbol("special_relations"), alloc(special_relations_decl_plugin), !has_logic()); } else { // the manager was created by an external module @@ -703,6 +705,7 @@ void cmd_context::init_manager_core(bool new_manager) { load_plugin(symbol("fpa"), logic_has_fpa(), fids); load_plugin(symbol("pb"), logic_has_pb(), fids); load_plugin(symbol("csp"), smt_logics::logic_is_csp(m_logic), fids); + for (family_id fid : fids) { decl_plugin * p = m_manager->get_plugin(fid); if (p) { diff --git a/src/smt/smt_setup.cpp b/src/smt/smt_setup.cpp index 731034921..89213c86d 100644 --- a/src/smt/smt_setup.cpp +++ b/src/smt/smt_setup.cpp @@ -33,6 +33,7 @@ Revision History: #include "smt/theory_dl.h" #include "smt/theory_seq_empty.h" #include "smt/theory_seq.h" +#include "smt/theory_special_relations.h" #include "smt/theory_pb.h" #include "smt/theory_fpa.h" #include "smt/theory_str.h" @@ -935,6 +936,10 @@ namespace smt { m_context.register_plugin(alloc(smt::theory_jobscheduler, m_manager)); } + void setup::setup_special_relations() { + m_context.register_plugin(alloc(smt::theory_special_relations, m_manager)); + } + void setup::setup_unknown() { static_features st(m_manager); ptr_vector fmls; @@ -950,6 +955,7 @@ namespace smt { setup_seq_str(st); setup_card(); setup_fpa(); + setup_special_relations(); } void setup::setup_unknown(static_features & st) { diff --git a/src/smt/smt_setup.h b/src/smt/smt_setup.h index 01a143301..53186f91c 100644 --- a/src/smt/smt_setup.h +++ b/src/smt/smt_setup.h @@ -82,6 +82,7 @@ namespace smt { void setup_QF_S(); void setup_LRA(); void setup_CSP(); + void setup_special_relations(); void setup_AUFLIA(bool simple_array = true); void setup_AUFLIA(static_features const & st); void setup_AUFLIRA(bool simple_array = true); From 63c63606ee772be3378fd881c600cac34b020d89 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 25 Mar 2019 17:53:43 -0700 Subject: [PATCH 13/19] include path Signed-off-by: Nikolaj Bjorner --- src/ast/special_relations_decl_plugin.cpp | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/src/ast/special_relations_decl_plugin.cpp b/src/ast/special_relations_decl_plugin.cpp index 6bb5734e5..b5a55cbb4 100644 --- a/src/ast/special_relations_decl_plugin.cpp +++ b/src/ast/special_relations_decl_plugin.cpp @@ -17,9 +17,9 @@ Revision History: --*/ -#include -#include"ast.h" -#include"special_relations_decl_plugin.h" +#include +#include "ast/ast.h" +#include "ast/special_relations_decl_plugin.h" @@ -37,11 +37,11 @@ func_decl * special_relations_decl_plugin::mk_func_decl( { if (arity != 2) { m_manager->raise_exception("special relations should have arity 2"); - return 0; + return nullptr; } if (domain[0] != domain[1]) { m_manager->raise_exception("argument sort missmatch"); - return 0; + return nullptr; } func_decl_info info(m_family_id, k, num_parameters, parameters); symbol name; From 6c96f855db0bbbb0ac31d17b20089cb57ee55dc2 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 25 Mar 2019 17:54:05 -0700 Subject: [PATCH 14/19] include path Signed-off-by: Nikolaj Bjorner --- src/ast/special_relations_decl_plugin.h | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/src/ast/special_relations_decl_plugin.h b/src/ast/special_relations_decl_plugin.h index 068382b23..ef432dbcc 100644 --- a/src/ast/special_relations_decl_plugin.h +++ b/src/ast/special_relations_decl_plugin.h @@ -20,8 +20,7 @@ Revision History: #ifndef SPECIAL_RELATIONS_DECL_PLUGIN_H_ #define SPECIAL_RELATIONS_DECL_PLUGIN_H_ -#include"ast.h" - +#include "ast/ast.h" enum special_relations_op_kind { From 0ae3de99162ac52c79c77fcae7c9dec23285d1ba Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 25 Mar 2019 17:57:06 -0700 Subject: [PATCH 15/19] virtual -> override Signed-off-by: Nikolaj Bjorner --- src/ast/special_relations_decl_plugin.h | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/src/ast/special_relations_decl_plugin.h b/src/ast/special_relations_decl_plugin.h index ef432dbcc..e8260e154 100644 --- a/src/ast/special_relations_decl_plugin.h +++ b/src/ast/special_relations_decl_plugin.h @@ -40,19 +40,19 @@ class special_relations_decl_plugin : public decl_plugin { symbol m_to; public: special_relations_decl_plugin(); - virtual ~special_relations_decl_plugin() {} - virtual decl_plugin * mk_fresh() { + ~special_relations_decl_plugin() override {} + + decl_plugin * mk_fresh() override { return alloc(special_relations_decl_plugin); } - virtual func_decl * mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters, - unsigned arity, sort * const * domain, sort * range); + func_decl * mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters, + unsigned arity, sort * const * domain, sort * range) override; - virtual void get_op_names(svector & op_names, symbol const & logic); - - - virtual sort * mk_sort(decl_kind k, unsigned num_parameters, parameter const * parameters) { return 0; } + void get_op_names(svector & op_names, symbol const & logic) override; + + sort * mk_sort(decl_kind k, unsigned num_parameters, parameter const * parameters) override { return nullptr; } }; enum sr_property { From b89cd9aea6052711852b8dc090c5e8e21eab9e99 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 26 Mar 2019 08:15:26 -0700 Subject: [PATCH 16/19] display methods Signed-off-by: Nikolaj Bjorner --- src/smt/theory_special_relations.cpp | 22 ++++++++++++++-------- src/smt/theory_special_relations.h | 2 ++ 2 files changed, 16 insertions(+), 8 deletions(-) diff --git a/src/smt/theory_special_relations.cpp b/src/smt/theory_special_relations.cpp index a4c73028e..d56844ad9 100644 --- a/src/smt/theory_special_relations.cpp +++ b/src/smt/theory_special_relations.cpp @@ -64,6 +64,17 @@ namespace smt { return m_graph.add_non_strict_edge(v1, v2, ls) && m_graph.add_non_strict_edge(v2, v1, ls); } + std::ostream& theory_special_relations::relation::display(theory_special_relations const& th, std::ostream& out) const { + out << m_decl->get_name() << ":\n"; + m_graph.display(out); + out << "explanation: " << m_explanation << "\n"; + m_uf.display(out); + for (atom* ap : m_asserted_atoms) { + th.display_atom(out, *ap); + } + return out; + } + theory_special_relations::theory_special_relations(ast_manager& m): theory(m.mk_family_id("special_relations")), m_util(m) { @@ -94,7 +105,7 @@ namespace smt { ctx.set_var_theory(v, get_id()); atom* a = alloc(atom, v, *r, v0, v1); m_atoms.push_back(a); - TRACE("special_relations", tout << mk_pp(atm, get_manager()) << " : " << a->v1() << ' ' << a->v2() << ' ' << gate_ctx << "\n";); + TRACE("special_relations", tout << mk_pp(atm, get_manager()) << " : bv" << v << " v" << a->v1() << " v" << a->v2() << ' ' << gate_ctx << "\n";); m_bool_var2atom.insert(v, a); return true; } @@ -291,7 +302,7 @@ namespace smt { UNREACHABLE(); res = l_undef; } - + TRACE("special_relations", r.display(*this, tout);); return res; } @@ -754,12 +765,7 @@ namespace smt { out << "Theory Special Relations\n"; display_var2enode(out); for (auto const& kv : m_relations) { - out << mk_pp(kv.m_value->decl(), get_manager()) << ":\n"; - kv.m_value->m_graph.display(out); - kv.m_value->m_uf.display(out); - for (atom* ap : kv.m_value->m_asserted_atoms) { - display_atom(out, *ap); - } + kv.m_value->display(*this, out); } } diff --git a/src/smt/theory_special_relations.h b/src/smt/theory_special_relations.h index 312d0d20b..81a968e54 100644 --- a/src/smt/theory_special_relations.h +++ b/src/smt/theory_special_relations.h @@ -116,6 +116,8 @@ namespace smt { bool add_strict_edge(theory_var v1, theory_var v2, literal_vector const& j); bool add_non_strict_edge(theory_var v1, theory_var v2, literal_vector const& j); + + std::ostream& display(theory_special_relations const& sr, std::ostream& out) const; }; From fde7283bb9e496b88c072196655e3b54efaf9ae6 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 26 Mar 2019 08:39:56 -0700 Subject: [PATCH 17/19] support indexed relations Signed-off-by: Nikolaj Bjorner --- src/api/api_ast.cpp | 1 - src/api/api_special_relations.cpp | 20 +++++++++--- src/api/c++/z3++.h | 39 +++++++---------------- src/api/z3_api.h | 34 ++++++++------------ src/ast/special_relations_decl_plugin.cpp | 4 --- src/ast/special_relations_decl_plugin.h | 4 --- src/smt/theory_special_relations.cpp | 6 +++- 7 files changed, 45 insertions(+), 63 deletions(-) diff --git a/src/api/api_ast.cpp b/src/api/api_ast.cpp index a8f62572a..999ebab6b 100644 --- a/src/api/api_ast.cpp +++ b/src/api/api_ast.cpp @@ -1056,7 +1056,6 @@ extern "C" { switch(_d->get_decl_kind()) { case OP_SPECIAL_RELATION_LO : return Z3_OP_SPECIAL_RELATION_LO; case OP_SPECIAL_RELATION_PO : return Z3_OP_SPECIAL_RELATION_PO; - case OP_SPECIAL_RELATION_PO_AO : return Z3_OP_SPECIAL_RELATION_PO_AO; case OP_SPECIAL_RELATION_PLO: return Z3_OP_SPECIAL_RELATION_PLO; case OP_SPECIAL_RELATION_TO : return Z3_OP_SPECIAL_RELATION_TO; default: UNREACHABLE(); diff --git a/src/api/api_special_relations.cpp b/src/api/api_special_relations.cpp index 40fde5083..e852c2b34 100644 --- a/src/api/api_special_relations.cpp +++ b/src/api/api_special_relations.cpp @@ -68,11 +68,21 @@ extern "C" { Z3_CATCH_RETURN(false); } #endif +#define MK_TERN(NAME, FID) \ + Z3_ast Z3_API NAME(Z3_context c, unsigned index, Z3_ast a, Z3_ast b) { \ + LOG_ ##NAME(c, index, a, b); \ + Z3_TRY; \ + expr* args[2] = { to_expr(a), to_expr(b) }; \ + parameter p(index); \ + ast* a = mk_c(c)->m().mk_app(mk_c(c)->get_special_relations_fid(), FID, 1, &p, 2, args); \ + mk_c(c)->save_ast_trail(a); \ + RETURN_Z3(of_ast(a)); \ + Z3_CATCH_RETURN(nullptr); \ +} - MK_BINARY(Z3_mk_sr_lo , mk_c(c)->get_special_relations_fid(), OP_SPECIAL_RELATION_LO, SKIP); - MK_BINARY(Z3_mk_sr_po , mk_c(c)->get_special_relations_fid(), OP_SPECIAL_RELATION_PO, SKIP); - MK_BINARY(Z3_mk_sr_po_ao,mk_c(c)->get_special_relations_fid(), OP_SPECIAL_RELATION_PO_AO,SKIP); - MK_BINARY(Z3_mk_sr_plo, mk_c(c)->get_special_relations_fid(), OP_SPECIAL_RELATION_PLO, SKIP); - MK_BINARY(Z3_mk_sr_to , mk_c(c)->get_special_relations_fid(), OP_SPECIAL_RELATION_TO, SKIP); + MK_TERN(Z3_mk_linear_order, OP_SPECIAL_RELATION_LO); + MK_TERN(Z3_mk_partial_order, OP_SPECIAL_RELATION_PO); + MK_TERN(Z3_mk_piecewise_linear_order, OP_SPECIAL_RELATION_PLO); + MK_TERN(Z3_mk_tree_order, OP_SPECIAL_RELATION_TO); }; diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index e18ca9204..8df43d477 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -1707,42 +1707,27 @@ namespace z3 { */ inline expr sext(expr const & a, unsigned i) { return to_expr(a.ctx(), Z3_mk_sign_ext(a.ctx(), i, a)); } - inline expr sr_lo(expr const& a, expr const& b) { + typedef Z3_ast Z3_apply_order(Z3_context, unsigned, Z3_ast, Z3_ast); + + inline expr apply_order(Z3_apply_order app, unsigned index, expr const& a, expr const& b) { check_context(a, b); - Z3_ast r = Z3_mk_sr_lo(a.ctx(), a, b); + Z3_ast r = app(a.ctx(), index, a, b); a.check_error(); return expr(a.ctx(), r); } - - inline expr sr_po(expr const& a, expr const& b) { - check_context(a, b); - Z3_ast r = Z3_mk_sr_po(a.ctx(), a, b); - a.check_error(); - return expr(a.ctx(), r); + inline expr linear_order(unsigned index, expr const& a, expr const& b) { + return apply_order(Z3_mk_linear_order, index, a, b); } - - inline expr sr_po_ao(expr const& a, expr const& b) { - check_context(a, b); - Z3_ast r = Z3_mk_sr_po_ao(a.ctx(), a, b); - a.check_error(); - return expr(a.ctx(), r); + inline expr partial_order(unsigned index, expr const& a, expr const& b) { + return apply_order(Z3_mk_partial_order, index, a, b); } - - inline expr sr_plo(expr const& a, expr const& b) { - check_context(a, b); - Z3_ast r = Z3_mk_sr_plo(a.ctx(), a, b); - a.check_error(); - return expr(a.ctx(), r); + inline expr piecewise_linear_order(unsigned index, expr const& a, expr const& b) { + return apply_order(Z3_mk_piecewise_linear_order, index, a, b); } - - inline expr sr_to(expr const& a, expr const& b) { - check_context(a, b); - Z3_ast r = Z3_mk_sr_to(a.ctx(), a, b); - a.check_error(); - return expr(a.ctx(), r); + inline expr tree_order(unsigned index, expr const& a, expr const& b) { + return apply_order(Z3_mk_tree_order, index, a, b); } - template class cast_ast; template<> class cast_ast { diff --git a/src/api/z3_api.h b/src/api/z3_api.h index 6d1db22b3..7ba33a61d 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -3608,49 +3608,41 @@ extern "C" { /** @name Special relations */ /*@{*/ /** - \brief declare \c a and \c b are in linear order. + \brief declare \c a and \c b are in linear order over a relation indexed by \c id. \pre a and b are of same type. + - def_API('Z3_mk_sr_lo', AST ,(_in(CONTEXT), _in(AST), _in(AST))) + def_API('Z3_mk_linear_order', AST ,(_in(CONTEXT), _in(UINT), _in(AST), _in(AST))) */ - Z3_ast Z3_API Z3_mk_sr_lo(Z3_context c, Z3_ast a, Z3_ast b); + Z3_ast Z3_API Z3_mk_linear_order(Z3_context c, unsigned id, Z3_ast a, Z3_ast b); /** - \brief declare \c a and \c b are in partial order. + \brief declare \c a and \c b are in partial order over a relation indexed by \c id. \pre a and b are of same type. - def_API('Z3_mk_sr_po', AST ,(_in(CONTEXT), _in(AST), _in(AST))) + def_API('Z3_mk_partial_order', AST ,(_in(CONTEXT), _in(UINT), _in(AST), _in(AST))) */ - Z3_ast Z3_API Z3_mk_sr_po(Z3_context c, Z3_ast a, Z3_ast b); + Z3_ast Z3_API Z3_mk_partial_order(Z3_context c, unsigned id, Z3_ast a, Z3_ast b); /** - \brief declare \c a and \c b are already partial ordered. + \brief declare \c a and \c b are in piecewise linear order indexed by relation \c id. \pre a and b are of same type. - def_API('Z3_mk_sr_po_ao', AST ,(_in(CONTEXT), _in(AST), _in(AST))) + def_API('Z3_mk_piecewise_linear_order', AST ,(_in(CONTEXT), _in(UINT), _in(AST), _in(AST))) */ - Z3_ast Z3_API Z3_mk_sr_po_ao(Z3_context c, Z3_ast a, Z3_ast b); + Z3_ast Z3_API Z3_mk_piecewise_linear_order(Z3_context c, unsigned id, Z3_ast a, Z3_ast b); /** - \brief declare \c a and \c b are in piecewise linear order. + \brief declare \c a and \c b are in tree order indexed by \c id. \pre a and b are of same type. - def_API('Z3_mk_sr_plo', AST ,(_in(CONTEXT), _in(AST), _in(AST))) + def_API('Z3_mk_tree_order', AST ,(_in(CONTEXT), _in(UINT), _in(AST), _in(AST))) */ - Z3_ast Z3_API Z3_mk_sr_plo(Z3_context c, Z3_ast a, Z3_ast b); - - /** - \brief declare \c a and \c b are in total order. - - \pre a and b are of same type. - - def_API('Z3_mk_sr_to', AST ,(_in(CONTEXT), _in(AST), _in(AST))) - */ - Z3_ast Z3_API Z3_mk_sr_to(Z3_context c, Z3_ast a, Z3_ast b); + Z3_ast Z3_API Z3_mk_tree_order(Z3_context c, unsigned id, Z3_ast a, Z3_ast b); /*@}*/ diff --git a/src/ast/special_relations_decl_plugin.cpp b/src/ast/special_relations_decl_plugin.cpp index b5a55cbb4..6dd0af1b4 100644 --- a/src/ast/special_relations_decl_plugin.cpp +++ b/src/ast/special_relations_decl_plugin.cpp @@ -26,7 +26,6 @@ Revision History: special_relations_decl_plugin::special_relations_decl_plugin(): m_lo("linear-order"), m_po("partial-order"), - m_po_ao("partial-order-already-ordered"), m_plo("piecewise-linear-order"), m_to("tree-order") {} @@ -47,7 +46,6 @@ func_decl * special_relations_decl_plugin::mk_func_decl( symbol name; switch(k) { case OP_SPECIAL_RELATION_PO: name = m_po; break; - case OP_SPECIAL_RELATION_PO_AO: name = m_po_ao; break; case OP_SPECIAL_RELATION_LO: name = m_lo; break; case OP_SPECIAL_RELATION_PLO: name = m_plo; break; case OP_SPECIAL_RELATION_TO: name = m_to; break; @@ -58,7 +56,6 @@ func_decl * special_relations_decl_plugin::mk_func_decl( void special_relations_decl_plugin::get_op_names(svector & op_names, symbol const & logic) { if (logic == symbol::null) { op_names.push_back(builtin_name(m_po.bare_str(), OP_SPECIAL_RELATION_PO)); - op_names.push_back(builtin_name(m_po_ao.bare_str(), OP_SPECIAL_RELATION_PO_AO)); op_names.push_back(builtin_name(m_lo.bare_str(), OP_SPECIAL_RELATION_LO)); op_names.push_back(builtin_name(m_plo.bare_str(), OP_SPECIAL_RELATION_PLO)); op_names.push_back(builtin_name(m_to.bare_str(), OP_SPECIAL_RELATION_TO)); @@ -68,7 +65,6 @@ void special_relations_decl_plugin::get_op_names(svector & op_name sr_property special_relations_util::get_property(func_decl* f) const { switch (f->get_decl_kind()) { case OP_SPECIAL_RELATION_PO: return sr_po; - case OP_SPECIAL_RELATION_PO_AO: return sr_po; // still partial ordered case OP_SPECIAL_RELATION_LO: return sr_lo; case OP_SPECIAL_RELATION_PLO: return sr_plo; case OP_SPECIAL_RELATION_TO: return sr_to; diff --git a/src/ast/special_relations_decl_plugin.h b/src/ast/special_relations_decl_plugin.h index e8260e154..dbdd61805 100644 --- a/src/ast/special_relations_decl_plugin.h +++ b/src/ast/special_relations_decl_plugin.h @@ -26,7 +26,6 @@ Revision History: enum special_relations_op_kind { OP_SPECIAL_RELATION_LO, OP_SPECIAL_RELATION_PO, - OP_SPECIAL_RELATION_PO_AO, OP_SPECIAL_RELATION_PLO, OP_SPECIAL_RELATION_TO, LAST_SPECIAL_RELATIONS_OP @@ -35,7 +34,6 @@ enum special_relations_op_kind { class special_relations_decl_plugin : public decl_plugin { symbol m_lo; symbol m_po; - symbol m_po_ao; symbol m_plo; symbol m_to; public: @@ -80,13 +78,11 @@ public: bool is_lo(expr const * e) const { return is_app_of(e, m_fid, OP_SPECIAL_RELATION_LO); } bool is_po(expr const * e) const { return is_app_of(e, m_fid, OP_SPECIAL_RELATION_PO); } - bool is_po_ao(expr const * e) const { return is_app_of(e, m_fid, OP_SPECIAL_RELATION_PO_AO); } bool is_plo(expr const * e) const { return is_app_of(e, m_fid, OP_SPECIAL_RELATION_PLO); } bool is_to(expr const * e) const { return is_app_of(e, m_fid, OP_SPECIAL_RELATION_TO); } app * mk_lo (expr * arg1, expr * arg2) { return m.mk_app( m_fid, OP_SPECIAL_RELATION_LO, arg1, arg2); } app * mk_po (expr * arg1, expr * arg2) { return m.mk_app( m_fid, OP_SPECIAL_RELATION_PO, arg1, arg2); } - app * mk_po_ao (expr * arg1, expr * arg2) { return m.mk_app( m_fid, OP_SPECIAL_RELATION_PO_AO, arg1, arg2); } app * mk_plo(expr * arg1, expr * arg2) { return m.mk_app( m_fid, OP_SPECIAL_RELATION_PLO, arg1, arg2); } app * mk_to (expr * arg1, expr * arg2) { return m.mk_app( m_fid, OP_SPECIAL_RELATION_TO, arg1, arg2); } diff --git a/src/smt/theory_special_relations.cpp b/src/smt/theory_special_relations.cpp index d56844ad9..65d30cea6 100644 --- a/src/smt/theory_special_relations.cpp +++ b/src/smt/theory_special_relations.cpp @@ -65,7 +65,11 @@ namespace smt { } std::ostream& theory_special_relations::relation::display(theory_special_relations const& th, std::ostream& out) const { - out << m_decl->get_name() << ":\n"; + out << mk_pp(m_decl, th.get_manager()); + for (unsigned i = 0; i < m_decl->get_num_parameters(); ++i) { + th.get_manager().display(out << " ", m_decl->get_parameter(i)); + } + out << ":\n"; m_graph.display(out); out << "explanation: " << m_explanation << "\n"; m_uf.display(out); From c69e911a7990fab39b8fb9bb93d1e439ce3064d3 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 27 Mar 2019 16:59:13 -0700 Subject: [PATCH 18/19] adding po evaluator Signed-off-by: Nikolaj Bjorner --- src/api/api_datatype.cpp | 65 ++++-------- src/ast/datatype_decl_plugin.cpp | 79 +++++++++++++++ src/ast/datatype_decl_plugin.h | 6 ++ src/ast/special_relations_decl_plugin.h | 4 + src/model/model.cpp | 1 + src/model/model_core.cpp | 1 + src/smt/smt_context.cpp | 1 + src/smt/theory_special_relations.cpp | 128 +++++++++++++++++++++++- 8 files changed, 233 insertions(+), 52 deletions(-) diff --git a/src/api/api_datatype.cpp b/src/api/api_datatype.cpp index 0c2544643..d48ce76e2 100644 --- a/src/api/api_datatype.cpp +++ b/src/api/api_datatype.cpp @@ -160,69 +160,40 @@ extern "C" { LOG_Z3_mk_list_sort(c, name, elem_sort, nil_decl, is_nil_decl, cons_decl, is_cons_decl, head_decl, tail_decl); RESET_ERROR_CODE(); ast_manager& m = mk_c(c)->m(); + func_decl_ref nil(m), is_nil(m), cons(m), is_cons(m), head(m), tail(m); datatype_util& dt_util = mk_c(c)->dtutil(); mk_c(c)->reset_last_result(); - datatype_util data_util(m); - accessor_decl* head_tail[2] = { - mk_accessor_decl(m, symbol("head"), type_ref(to_sort(elem_sort))), - mk_accessor_decl(m, symbol("tail"), type_ref(0)) - }; - constructor_decl* constrs[2] = { - mk_constructor_decl(symbol("nil"), symbol("is_nil"), 0, nullptr), - // Leo: SMT 2.0 document uses 'insert' instead of cons - mk_constructor_decl(symbol("cons"), symbol("is_cons"), 2, head_tail) - }; - - sort_ref_vector sorts(m); - { - datatype_decl * decl = mk_datatype_decl(dt_util, to_symbol(name), 0, nullptr, 2, constrs); - bool is_ok = mk_c(c)->get_dt_plugin()->mk_datatypes(1, &decl, 0, nullptr, sorts); - del_datatype_decl(decl); - - if (!is_ok) { - SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); - RETURN_Z3(nullptr); - } + sort_ref s = dt_util.mk_list_datatype(to_sort(elem_sort), to_symbol(name), cons, is_cons, head, tail, nil, is_nil); + + if (!s) { + SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); + RETURN_Z3(nullptr); } - sort * s = sorts.get(0); mk_c(c)->save_multiple_ast_trail(s); - ptr_vector const& cnstrs = *data_util.get_datatype_constructors(s); - SASSERT(cnstrs.size() == 2); - func_decl* f; if (nil_decl) { - f = cnstrs[0]; - mk_c(c)->save_multiple_ast_trail(f); - *nil_decl = of_func_decl(f); + mk_c(c)->save_multiple_ast_trail(nil); + *nil_decl = of_func_decl(nil); } if (is_nil_decl) { - f = data_util.get_constructor_is(cnstrs[0]); - mk_c(c)->save_multiple_ast_trail(f); - *is_nil_decl = of_func_decl(f); + mk_c(c)->save_multiple_ast_trail(is_nil); + *is_nil_decl = of_func_decl(is_nil); } if (cons_decl) { - f = cnstrs[1]; - mk_c(c)->save_multiple_ast_trail(f); - *cons_decl = of_func_decl(f); + mk_c(c)->save_multiple_ast_trail(cons); + *cons_decl = of_func_decl(cons); } if (is_cons_decl) { - f = data_util.get_constructor_is(cnstrs[1]); - mk_c(c)->save_multiple_ast_trail(f); - *is_cons_decl = of_func_decl(f); + mk_c(c)->save_multiple_ast_trail(is_cons); + *is_cons_decl = of_func_decl(is_cons); } if (head_decl) { - ptr_vector const& acc = *data_util.get_constructor_accessors(cnstrs[1]); - SASSERT(acc.size() == 2); - f = (acc)[0]; - mk_c(c)->save_multiple_ast_trail(f); - *head_decl = of_func_decl(f); + mk_c(c)->save_multiple_ast_trail(head); + *head_decl = of_func_decl(head); } if (tail_decl) { - ptr_vector const& acc = *data_util.get_constructor_accessors(cnstrs[1]); - SASSERT(acc.size() == 2); - f = (acc)[1]; - mk_c(c)->save_multiple_ast_trail(f); - *tail_decl = of_func_decl(f); + mk_c(c)->save_multiple_ast_trail(tail); + *tail_decl = of_func_decl(tail); } RETURN_Z3_mk_list_sort(of_sort(s)); Z3_CATCH_RETURN(nullptr); diff --git a/src/ast/datatype_decl_plugin.cpp b/src/ast/datatype_decl_plugin.cpp index 146c7359f..e7a5506a8 100644 --- a/src/ast/datatype_decl_plugin.cpp +++ b/src/ast/datatype_decl_plugin.cpp @@ -1187,6 +1187,85 @@ namespace datatype { } } } + + sort_ref util::mk_list_datatype(sort* elem, symbol const& name, + func_decl_ref& cons, func_decl_ref& is_cons, + func_decl_ref& hd, func_decl_ref& tl, + func_decl_ref& nil, func_decl_ref& is_nil) { + + accessor_decl* head_tail[2] = { + mk_accessor_decl(m, symbol("head"), type_ref(elem)), + mk_accessor_decl(m, symbol("tail"), type_ref(0)) + }; + constructor_decl* constrs[2] = { + mk_constructor_decl(symbol("nil"), symbol("is_nil"), 0, nullptr), + mk_constructor_decl(symbol("cons"), symbol("is_cons"), 2, head_tail) + }; + decl::plugin& p = *get_plugin(); + + sort_ref_vector sorts(m); + datatype_decl * decl = mk_datatype_decl(*this, name, 0, nullptr, 2, constrs); + bool is_ok = p.mk_datatypes(1, &decl, 0, nullptr, sorts); + del_datatype_decl(decl); + + if (!is_ok) { + return sort_ref(m); + } + sort* s = sorts.get(0); + ptr_vector const& cnstrs = *get_datatype_constructors(s); + SASSERT(cnstrs.size() == 2); + nil = cnstrs[0]; + is_nil = get_constructor_is(cnstrs[0]); + cons = cnstrs[1]; + is_cons = get_constructor_is(cnstrs[1]); + ptr_vector const& acc = *get_constructor_accessors(cnstrs[1]); + SASSERT(acc.size() == 2); + hd = acc[0]; + tl = acc[1]; + return sort_ref(s, m); + } + + sort_ref util::mk_pair_datatype(sort* a, sort* b, func_decl_ref& fst, func_decl_ref& snd, func_decl_ref& pair) { + type_ref t1(a), t2(b); + accessor_decl* fstd = mk_accessor_decl(m, symbol("fst"), t1); + accessor_decl* sndd = mk_accessor_decl(m, symbol("snd"), t2); + accessor_decl* accd[2] = { fstd, sndd }; + auto * p = mk_constructor_decl(symbol("pair"), symbol("is-pair"), 2, accd); + auto* dt = mk_datatype_decl(*this, symbol("pair"), 0, nullptr, 1, &p); + sort_ref_vector sorts(m); + VERIFY(get_plugin()->mk_datatypes(1, &dt, 0, nullptr, sorts)); + del_datatype_decl(dt); + sort* s = sorts.get(0); + ptr_vector const& cnstrs = *get_datatype_constructors(s); + SASSERT(cnstrs.size() == 1); + ptr_vector const& acc = *get_constructor_accessors(cnstrs[0]); + SASSERT(acc.size() == 2); + fst = acc[0]; + snd = acc[1]; + pair = cnstrs[0]; + return sort_ref(s, m); + } + + sort_ref util::mk_tuple_datatype(svector> const& elems, symbol const& name, symbol const& test, func_decl_ref& tup, func_decl_ref_vector& accs) { + ptr_vector accd; + for (auto const& e : elems) { + type_ref t(e.second); + accd.push_back(mk_accessor_decl(m, e.first, t)); + } + auto* tuple = mk_constructor_decl(name, test, accd.size(), accd.c_ptr()); + auto* dt = mk_datatype_decl(*this, name, 0, nullptr, 1, &tuple); + sort_ref_vector sorts(m); + VERIFY(get_plugin()->mk_datatypes(1, &dt, 0, nullptr, sorts)); + del_datatype_decl(dt); + sort* s = sorts.get(0); + ptr_vector const& cnstrs = *get_datatype_constructors(s); + SASSERT(cnstrs.size() == 1); + ptr_vector const& acc = *get_constructor_accessors(cnstrs[0]); + for (auto* f : acc) accs.push_back(f); + tup = cnstrs[0]; + return sort_ref(s, m); + } + } datatype_decl * mk_datatype_decl(datatype_util& u, symbol const & n, unsigned num_params, sort*const* params, unsigned num_constructors, constructor_decl * const * cs) { diff --git a/src/ast/datatype_decl_plugin.h b/src/ast/datatype_decl_plugin.h index e9734ac0b..5292ab6b9 100644 --- a/src/ast/datatype_decl_plugin.h +++ b/src/ast/datatype_decl_plugin.h @@ -364,6 +364,12 @@ namespace datatype { decl::plugin* get_plugin() { return m_plugin; } void get_defs(sort* s, ptr_vector& defs); def const& get_def(sort* s) const; + sort_ref mk_list_datatype(sort* elem, symbol const& name, + func_decl_ref& cons, func_decl_ref& is_cons, + func_decl_ref& hd, func_decl_ref& tl, + func_decl_ref& nil, func_decl_ref& is_nil); + sort_ref mk_pair_datatype(sort* a, sort* b, func_decl_ref& fst, func_decl_ref& snd, func_decl_ref& pair); + sort_ref mk_tuple_datatype(svector> const& elems, symbol const& name, symbol const& test, func_decl_ref& tup, func_decl_ref_vector& accs); }; }; diff --git a/src/ast/special_relations_decl_plugin.h b/src/ast/special_relations_decl_plugin.h index dbdd61805..e8260e154 100644 --- a/src/ast/special_relations_decl_plugin.h +++ b/src/ast/special_relations_decl_plugin.h @@ -26,6 +26,7 @@ Revision History: enum special_relations_op_kind { OP_SPECIAL_RELATION_LO, OP_SPECIAL_RELATION_PO, + OP_SPECIAL_RELATION_PO_AO, OP_SPECIAL_RELATION_PLO, OP_SPECIAL_RELATION_TO, LAST_SPECIAL_RELATIONS_OP @@ -34,6 +35,7 @@ enum special_relations_op_kind { class special_relations_decl_plugin : public decl_plugin { symbol m_lo; symbol m_po; + symbol m_po_ao; symbol m_plo; symbol m_to; public: @@ -78,11 +80,13 @@ public: bool is_lo(expr const * e) const { return is_app_of(e, m_fid, OP_SPECIAL_RELATION_LO); } bool is_po(expr const * e) const { return is_app_of(e, m_fid, OP_SPECIAL_RELATION_PO); } + bool is_po_ao(expr const * e) const { return is_app_of(e, m_fid, OP_SPECIAL_RELATION_PO_AO); } bool is_plo(expr const * e) const { return is_app_of(e, m_fid, OP_SPECIAL_RELATION_PLO); } bool is_to(expr const * e) const { return is_app_of(e, m_fid, OP_SPECIAL_RELATION_TO); } app * mk_lo (expr * arg1, expr * arg2) { return m.mk_app( m_fid, OP_SPECIAL_RELATION_LO, arg1, arg2); } app * mk_po (expr * arg1, expr * arg2) { return m.mk_app( m_fid, OP_SPECIAL_RELATION_PO, arg1, arg2); } + app * mk_po_ao (expr * arg1, expr * arg2) { return m.mk_app( m_fid, OP_SPECIAL_RELATION_PO_AO, arg1, arg2); } app * mk_plo(expr * arg1, expr * arg2) { return m.mk_app( m_fid, OP_SPECIAL_RELATION_PLO, arg1, arg2); } app * mk_to (expr * arg1, expr * arg2) { return m.mk_app( m_fid, OP_SPECIAL_RELATION_TO, arg1, arg2); } diff --git a/src/model/model.cpp b/src/model/model.cpp index e6a3ffedf..aa3976cb9 100644 --- a/src/model/model.cpp +++ b/src/model/model.cpp @@ -217,6 +217,7 @@ void model::compress() { } } if (removed.empty()) break; + TRACE("model", tout << "remove\n"; for (func_decl* f : removed) tout << f->get_name() << "\n";); remove_decls(m_decls, removed); remove_decls(m_func_decls, removed); remove_decls(m_const_decls, removed); diff --git a/src/model/model_core.cpp b/src/model/model_core.cpp index d92e81421..0f811034a 100644 --- a/src/model/model_core.cpp +++ b/src/model/model_core.cpp @@ -66,6 +66,7 @@ void model_core::register_decl(func_decl * d, expr * v) { } void model_core::register_decl(func_decl * d, func_interp * fi) { + TRACE("model", tout << "register " << d->get_name() << "\n";); SASSERT(d->get_arity() > 0); SASSERT(&fi->m() == &m); decl2finterp::obj_map_entry * entry = m_finterp.insert_if_not_there2(d, nullptr); diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index 5715e067d..fc5c7e917 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -4478,6 +4478,7 @@ namespace smt { } recfun::util u(m); func_decl_ref_vector recfuns = u.get_rec_funs(); + std::cout << recfuns << "\n"; for (func_decl* f : recfuns) { auto& def = u.get_def(f); expr* rhs = def.get_rhs(); diff --git a/src/smt/theory_special_relations.cpp b/src/smt/theory_special_relations.cpp index 65d30cea6..8339c658e 100644 --- a/src/smt/theory_special_relations.cpp +++ b/src/smt/theory_special_relations.cpp @@ -26,7 +26,11 @@ Notes: #include "smt/smt_solver.h" #include "solver/solver.h" #include "ast/reg_decl_plugins.h" +#include "ast/datatype_decl_plugin.h" +#include "ast/recfun_decl_plugin.h" #include "ast/ast_pp.h" +#include "ast/rewriter/recfun_replace.h" + namespace smt { @@ -610,16 +614,130 @@ namespace smt { m.get_model().register_decl(r.decl(), fi); } - void theory_special_relations::init_model_plo(relation& r, model_generator& m) { - expr_ref inj = mk_inj(r, m); - expr_ref cls = mk_class(r, m); + void theory_special_relations::init_model_plo(relation& r, model_generator& mg) { + expr_ref inj = mk_inj(r, mg); + expr_ref cls = mk_class(r, mg); func_interp* fi = alloc(func_interp, get_manager(), 2); fi->set_else(get_manager().mk_and(inj, cls)); - m.get_model().register_decl(r.decl(), fi); + mg.get_model().register_decl(r.decl(), fi); } + /** + \brief model for a partial order, + is a recursive function that evaluates membership in partial order over + a fixed set of edges. It runs in O(e*n^2) where n is the number of vertices and e + number of edges. + + connected1(x, y, v, w, S) = + if x = v then + if y = w then (S, true) else + if w in S then (S, false) else + connected2(w, y, S u { w }, edges) + else (S, false) + + connected2(x, y, S, []) = (S, false) + connected2(x, y, S, (u,w)::edges) = + let (S, c) = connected1(x, y, u, w, S) + if c then (S, true) else connected2(x, y, S, edges) + + */ + + void theory_special_relations::init_model_po(relation& r, model_generator& mg) { - // NOT_IMPLEMENTED_YET(); + ast_manager& m = get_manager(); + sort* s = r.m_decl->get_domain(0); + context& ctx = get_context(); + datatype_util dt(m); + recfun::util rf(m); + recfun::decl::plugin& p = rf.get_plugin(); + func_decl_ref nil(m), is_nil(m), cons(m), is_cons(m), hd(m), tl(m); + sort_ref listS(dt.mk_list_datatype(s, symbol("List"), cons, is_cons, hd, tl, nil, is_nil), m); + func_decl_ref fst(m), snd(m), pair(m); + sort_ref tup(dt.mk_pair_datatype(listS, m.mk_bool_sort(), fst, snd, pair), m); + sort* dom1[5] = { s, s, listS, s, s }; + recfun::promise_def c1 = p.mk_def(symbol("connected1"), 5, dom1, tup); + sort* dom2[3] = { s, s, listS }; + recfun::promise_def c2 = p.mk_def(symbol("connected2"), 3, dom2, tup); + sort* dom3[2] = { s, listS }; + recfun::promise_def mem = p.mk_def(symbol("member"), 2, dom3, m.mk_bool_sort()); + var_ref xV(m.mk_var(1, s), m); + var_ref SV(m.mk_var(0, listS), m); + var_ref yV(m), vV(m), wV(m); + + expr* x = xV, *S = SV; + expr* T = m.mk_true(); + expr* F = m.mk_false(); + func_decl* memf = mem.get_def()->get_decl(); + func_decl* conn1 = c1.get_def()->get_decl(); + func_decl* conn2 = c2.get_def()->get_decl(); + expr_ref mem_body(m); + mem_body = m.mk_ite(m.mk_app(is_nil, S), + F, + m.mk_ite(m.mk_eq(m.mk_app(hd, S), x), + T, + m.mk_app(memf, x, m.mk_app(tl, S)))); + recfun_replace rep(m); + var* vars[2] = { xV, SV }; + p.set_definition(rep, mem, 2, vars, mem_body); + + xV = m.mk_var(4, s); + yV = m.mk_var(3, s); + SV = m.mk_var(2, listS); + vV = m.mk_var(1, s); + wV = m.mk_var(0, s); + expr* y = yV, *v = vV, *w = wV; + x = xV, S = SV; + + expr_ref ST(m.mk_app(pair, S, T), m); + expr_ref SF(m.mk_app(pair, S, F), m); + + expr_ref connected_body(m); + connected_body = + m.mk_ite(m.mk_not(m.mk_eq(x, v)), + SF, + m.mk_ite(m.mk_eq(y, w), + ST, + m.mk_ite(m.mk_app(memf, w, S), + SF, + m.mk_app(conn2, w, y, m.mk_app(cons, w, S))))); + var* vars2[5] = { xV, yV, SV, vV, wV }; + p.set_definition(rep, c1, 5, vars2, connected_body); + + xV = m.mk_var(2, s); + yV = m.mk_var(1, s); + SV = m.mk_var(0, listS); + x = xV, y = yV, S = SV; + ST = m.mk_app(pair, S, T); + SF = m.mk_app(pair, S, F); + expr_ref connected_rec_body(m); + connected_rec_body = SF; + + for (atom* ap : r.m_asserted_atoms) { + atom& a = *ap; + if (!a.phase()) continue; + SASSERT(ctx.get_assignment(a.var()) == l_true); + expr* n1 = get_enode(a.v1())->get_root()->get_owner(); + expr* n2 = get_enode(a.v2())->get_root()->get_owner(); + + expr* Sr = connected_rec_body; + expr* args[5] = { x, y, m.mk_app(fst, Sr), n1, n2}; + expr* Sc = m.mk_app(conn1, 5, args); + connected_rec_body = m.mk_ite(m.mk_app(snd, Sr), ST, Sc); + } + var* vars3[3] = { xV, yV, SV }; + p.set_definition(rep, c2, 3, vars3, connected_rec_body); + +#if 0 + // TBD: doesn't terminate with model_evaluator/rewriter + + // r.m_decl(x,y) -> snd(connected2(x,y,nil)) + + func_interp* fi = alloc(func_interp, m, 2); + fi->set_else(m.mk_app(snd, m.mk_app(conn2, x, y, m.mk_const(nil)))); + mg.get_model().register_decl(r.decl(), fi); +#endif + + } /** From 4e38e90e2b25c42be81781f8c8e4e55c88f457f9 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 28 Mar 2019 07:03:04 -0700 Subject: [PATCH 19/19] fix po model Signed-off-by: Nikolaj Bjorner --- src/smt/smt_context.cpp | 2 +- src/smt/theory_special_relations.cpp | 10 ++++------ 2 files changed, 5 insertions(+), 7 deletions(-) diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index fc5c7e917..5b18613b6 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -4478,7 +4478,6 @@ namespace smt { } recfun::util u(m); func_decl_ref_vector recfuns = u.get_rec_funs(); - std::cout << recfuns << "\n"; for (func_decl* f : recfuns) { auto& def = u.get_def(f); expr* rhs = def.get_rhs(); @@ -4500,6 +4499,7 @@ namespace smt { fi->set_else(bodyr); m_model->register_decl(f, fi); } + TRACE("model", tout << *m_model << "\n";); } }; diff --git a/src/smt/theory_special_relations.cpp b/src/smt/theory_special_relations.cpp index 8339c658e..6e8c04a97 100644 --- a/src/smt/theory_special_relations.cpp +++ b/src/smt/theory_special_relations.cpp @@ -727,16 +727,14 @@ namespace smt { var* vars3[3] = { xV, yV, SV }; p.set_definition(rep, c2, 3, vars3, connected_rec_body); -#if 0 - // TBD: doesn't terminate with model_evaluator/rewriter - // r.m_decl(x,y) -> snd(connected2(x,y,nil)) + xV = m.mk_var(0, s); + yV = m.mk_var(1, s); + x = xV, y = yV; func_interp* fi = alloc(func_interp, m, 2); - fi->set_else(m.mk_app(snd, m.mk_app(conn2, x, y, m.mk_const(nil)))); + fi->set_else(m.mk_app(snd, m.mk_app(conn2, x, y, m.mk_app(cons, x, m.mk_const(nil))))); mg.get_model().register_decl(r.decl(), fi); -#endif - }