#6646

- always enable special-relations theory to deal with default setting and push
- fix bugs related to equality and transitivity.

src/smt/smt_setup.cpp

@@ -802,7 +802,7 @@ namespace smt {
         setup_dl();
         setup_seq_str(st);
         setup_fpa();
-        if (st.m_has_sr) setup_special_relations();
+        setup_special_relations();
     }
 
     void setup::setup_unknown(static_features & st) {
@@ -818,7 +818,7 @@ namespace smt {
             setup_seq_str(st);
             setup_fpa();
             setup_recfuns();
-            if (st.m_has_sr) setup_special_relations();
+            setup_special_relations();
             return;
         }
 

src/smt/theory_special_relations.cpp

@@ -71,7 +71,7 @@ namespace smt {
         ensure_var(v1);
         ensure_var(v2);
         literal_vector ls;
-        ls.push_back(l);
+        ls.push_back(l);        
         return m_graph.add_non_strict_edge(v1, v2, ls) && m_graph.add_non_strict_edge(v2, v1, ls);
     }
 
@@ -130,6 +130,7 @@ namespace smt {
     }
 
     bool theory_special_relations::internalize_term(app * term) {
+        verbose_stream() << mk_pp(term, m) << "\n";
         return false;
     }
 
@@ -156,9 +157,8 @@ namespace smt {
     }
 
     theory_var theory_special_relations::mk_var(expr* e) {
-        if (!ctx.e_internalized(e)) {
+        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) {
@@ -582,28 +582,27 @@ namespace smt {
     lbool theory_special_relations::final_check_po(relation& r) {
         for (atom* ap : r.m_asserted_atoms) {
             atom& a = *ap;
-            if (!a.phase() && r.m_uf.find(a.v1()) == r.m_uf.find(a.v2())) {
-                // v1 !-> v2
-                // find v1 -> v3 -> v4 -> v2 path
-                r.m_explanation.reset();
-                unsigned timestamp = r.m_graph.get_timestamp();
-                bool found_path = r.m_graph.find_shortest_reachable_path(a.v1(), a.v2(), timestamp, r);
-                if (found_path) {
-                    TRACE("special_relations", tout << "check po conflict\n";);
-                    r.m_explanation.push_back(a.explanation());
-                    set_conflict(r);
-                    return l_false;
-                }
+            if (a.phase())
+                continue;
+            // v1 !-> v2
+            // find v1 -> v3 -> v4 -> v2 path
+            r.m_explanation.reset();
+            unsigned timestamp = r.m_graph.get_timestamp();
+            bool found_path = a.v1() == a.v2() || r.m_graph.find_shortest_reachable_path(a.v1(), a.v2(), timestamp, r);
+            if (found_path) {
+                TRACE("special_relations", tout << "check po conflict\n";);
+                r.m_explanation.push_back(a.explanation());
+                set_conflict(r);
+                return l_false;
             }
         }
         return l_true;
     }
 
     void theory_special_relations::propagate() {
         if (m_can_propagate) {
-            for (auto const& kv : m_relations) {
+            for (auto const& kv : m_relations) 
                 propagate(*kv.m_value);
-            }
             m_can_propagate = false;
         }
     }
@@ -1124,12 +1123,12 @@ namespace smt {
     }
 
     void theory_special_relations::display(std::ostream & out) const {
-        if (m_relations.empty()) return;
+        if (m_relations.empty())
+            return;
         out << "Theory Special Relations\n";
         display_var2enode(out);
-        for (auto const& kv : m_relations) {
+        for (auto const& kv : m_relations) 
             kv.m_value->display(*this, out);
-        }
     }
 
     void theory_special_relations::collect_asserted_po_atoms(vector<std::pair<bool_var, bool>>& atoms) const {