add sr

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

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

src/ast/special_relations_decl_plugin.cpp

@@ -0,0 +1,79 @@
+/*++
+Copyright (c) 2015 Microsoft Corporation
+
+Module Name:
+
+    special_relations_decl_plugin.cpp
+
+Abstract:
+
+    <abstract>
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2015-15-9.
+
+Revision History:
+
+--*/
+
+#include<sstream>
+#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<builtin_name> & 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;
+    }
+}

src/ast/special_relations_decl_plugin.h

@@ -0,0 +1,97 @@
+/*++
+Copyright (c) 2015 Microsoft Corporation
+
+Module Name:
+
+    special_relations_decl_plugin.h
+
+Abstract:
+
+    <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<builtin_name> & 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_ */

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

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<dl_var> 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<int> m_freq_hybrid;
+    int m_total_count = 0;
+    int m_run_counter = -1;
+    svector<int> m_hybrid_visited, m_hybrid_parent;
+public:
+
+    template<typename Functor>
+    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<typename Functor>
+     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<typename Functor>
-    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<typename Functor>
+    bool find_shortest_path_aux(dl_var source, dl_var target, unsigned timestamp, Functor & f, bool zero_edge) {
         svector<bfs_elem> bfs_todo;
         svector<char>     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();
+            for (edge_id e_id : edges) {
-            typename edge_id_vector::iterator end = edges.end();
-            for (; it != end; ++it) {
-                edge_id e_id = *it;
                 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<int>(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();
+            for (edge_id e_id : edges[source]) {
-            typename edge_id_vector::const_iterator end = edges[source].end();
-
-            for (; it != end; ++it) {
-                edge_id e_id = *it;
                 edge const& e = m_edges[e_id];
 
                 if (&e == &e_init) {
@@ -1569,11 +1687,9 @@ private:
                 tout << "\n";
             });
 
-        typename heap<typename dfs_state::hp_lt>::const_iterator it  = state.m_heap.begin();
+        for (auto & s : state.m_heap) {
-        typename heap<typename dfs_state::hp_lt>::const_iterator end = state.m_heap.end();
+            SASSERT(m_mark[s] != DL_PROP_UNMARKED);
-        for (; it != end; ++it) {
+            m_mark[s] = DL_PROP_UNMARKED;;
-            SASSERT(m_mark[*it] != DL_PROP_UNMARKED);
-            m_mark[*it] = DL_PROP_UNMARKED;;
         }
         state.m_heap.reset();
         SASSERT(marks_are_clear());

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 <fstream>
+
+#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<ptr_vector<expr>>& 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<func_decl, relation*>::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<func_decl, relation*>::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<parameter> 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<unsigned> 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<expr> assumptions;
+        ptr_vector<expr> literals;
+
+        int k = 1;
+        static int curr_id = 100000;
+        
+        u_map<ptr_vector<expr>> 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<func_decl, relation*>::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<func_decl, relation*>::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<func_decl, relation*>::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<func_decl, relation*>::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<dl_var> 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<dl_var> nodes;
+        num_children.resize(sz, 0);
+        svector<bool>   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<dl_var> 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<func_decl, relation*>::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<func_decl, relation*>::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<bool_var,bool> >& atoms) const {
+        obj_map<func_decl, relation*>::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);
+    }
+
+}

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<atom> 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<int_ext> graph;
+
+        typedef union_find<union_find_default_ctx> 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<scope>        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<atom*>     bool_var2atom;
+
+        special_relations_util         m_util;
+        arith_util m_autil;
+
+        atoms                          m_atoms;
+        unsigned_vector                m_atoms_lim;
+        obj_map<func_decl, relation*>  m_relations;
+        bool_var2atom                  m_bool_var2atom;
+
+        scoped_ptr<solver> m_nested_solver;
+        struct atom_hash {
+            size_t operator()(atom a) const {
+                return std::hash<int>()(a.v1()) ^ std::hash<int>()(a.v2()) ^ std::hash<bool>()(a.phase());
+            }
+        };
+        u_map<expr*> expr_cache;
+        u_map<atom*> 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<bool_var,bool> >& atoms) const;
+      void display_atom( std::ostream & out, atom& a) const;
+      void display_atom( atom& a) const;
+  //END: ASHU
+    };
+}
+
+#endif