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