support or, and, implies, distinct in mbp_basic (#6867)

src/qe/mbp/mbp_arrays_tg.cpp

@@ -278,7 +278,6 @@ struct mbp_array_tg::impl {
         m_tg.get_terms(terms, false);
         for (unsigned i = 0; i < terms.size(); i++) {
             term = terms.get(i);
-            SASSERT(!m.is_distinct(term));
             if (m_seen.is_marked(term)) continue;
             if (m_tg.is_cgr(term)) continue;
             TRACE("mbp_tg", tout << "processing " << expr_ref(term, m););

src/qe/mbp/mbp_basic_tg.cpp

@@ -43,32 +43,106 @@ struct mbp_basic_tg::impl {
     void mark_seen(expr *t) { m_seen.mark(t); }
     bool is_seen(expr *t) { return m_seen.is_marked(t); }
 
-    //Split on all ite terms, irrespective of whether
-    //they contain variables/are c-ground
+    // Split on all ite terms, irrespective of whether
+    // they contain variables/are c-ground
     bool apply() {
-        if (!m_use_mdl) return false;
+        std::function<bool(expr *)> should_split, is_true, is_false;
+        if (!m_use_mdl) {
+            should_split = [&](expr *t) { return m_tg.has_val_in_class(t); };
+            is_true = [&](expr *t) {
+                return m_tg.has_val_in_class(t) && m_mdl.is_true(t);
+            };
+            is_false = [&](expr *t) {
+                return m_tg.has_val_in_class(t) && m_mdl.is_false(t);
+            };
+        } else {
+            should_split = [](expr *t) { return true; };
+            is_true = [&](expr *t) { return m_mdl.is_true(t); };
+            is_false = [&](expr *t) { return m_mdl.is_false(t); };
+        }
+
         expr *c, *th, *el;
         expr_ref nterm(m);
         bool progress = false;
         TRACE("mbp_tg", tout << "Iterating over terms of tg";);
         // Not resetting terms because get_terms calls resize on terms
         m_tg.get_terms(terms, false);
-        for (expr* term : terms) {
-            if (is_seen(term))
-                continue;
-            if (m.is_ite(term, c, th, el)) {
+        for (expr *term : terms) {
+            if (is_seen(term)) continue;
+            if (m.is_ite(term, c, th, el) && should_split(c)) {
                 mark_seen(term);
                 progress = true;
                 if (m_mdl.is_true(c)) {
                     m_tg.add_lit(c);
                     m_tg.add_eq(term, th);
-                }
-                else {
+                } else {
                     nterm = mk_not(m, c);
                     m_tg.add_lit(nterm);
                     m_tg.add_eq(term, el);
                 }
             }
+            if (m.is_implies(term, c, th)) {
+                if (is_true(th) || is_false(c)) {
+                    mark_seen(term);
+                    progress = true;
+                    if (is_true(th))
+                        m_tg.add_lit(th);
+                    else if (is_false(c))
+                        m_tg.add_lit(c);
+                    m_tg.add_eq(term, m.mk_true());
+                } else if (is_true(c) && is_false(th)) {
+                    mark_seen(term);
+                    progress = true;
+                    m_tg.add_eq(term, m.mk_false());
+                }
+            }
+            if (m.is_or(term) || m.is_and(term)) {
+                bool is_or = m.is_or(term);
+                app *c = to_app(term);
+                bool t = is_or ? any_of(*c, is_true) : all_of(*c, is_true);
+                bool f = is_or ? all_of(*c, is_false) : all_of(*c, is_false);
+                if (t || f) {
+                    mark_seen(term);
+                    progress = true;
+                    m_tg.add_eq(term, t ? m.mk_true() : m.mk_false());
+                    if (f) {
+                        for (auto a : *c) {
+                            if (is_false(a)) {
+                                m_tg.add_lit(mk_not(m, a));
+                                if (!is_or) break;
+                            }
+                        }
+                    } else {
+                        for (auto a : *c) {
+                            if (is_true(a)) {
+                                m_tg.add_lit(a);
+                                if (is_or) break;
+                            }
+                        }
+                    }
+                }
+            }
+            if (m_use_mdl && m.is_distinct(term)) {
+                mark_seen(term);
+                progress = true;
+                bool eq = false;
+                app *c = to_app(term);
+                for (auto a1 : *c) {
+                    for (auto a2 : *c) {
+                        if (a1 == a2) continue;
+                        if (m_mdl.are_equal(a1, a2)) {
+                            m_tg.add_eq(a1, a2);
+                            eq = true;
+                            break;
+                        } else
+                            m_tg.add_deq(a1, a2);
+                    }
+                }
+                if (eq)
+                    m_tg.add_eq(term, m.mk_false());
+                else
+                    m_tg.add_eq(term, m.mk_true());
+            }
         }
         return progress;
     }

src/qe/mbp/mbp_dt_tg.cpp

@@ -158,7 +158,6 @@ struct mbp_dt_tg::impl {
         m_tg.get_terms(terms, false);
         for (unsigned i = 0; i < terms.size(); i++) {
             term = terms.get(i);
-            SASSERT(!m.is_distinct(term));
             if (is_seen(term)) continue;
             if (m_tg.is_cgr(term)) continue;
             if (is_app(term) &&

src/qe/mbp/mbp_qel.cpp

@@ -178,7 +178,7 @@ class mbp_qel::impl {
 
         std::function<bool(expr *)> non_core = [&](expr *e) {
             if (is_app(e) && is_partial_eq(to_app(e))) return true;
-            if (m.is_ite(e)) return true;
+            if (m.is_ite(e) || m.is_or(e) || m.is_implies(e) || m.is_and(e) || m.is_distinct(e)) return true;
             return red_vars.is_marked(e);
         };