extend dcert to disunification constraints that arithmetic theory needs to satisfy

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

src/qe/qe_mbi.cpp

@@ -46,7 +46,6 @@ Notes:
 namespace qe {
 
     void mbi_plugin::set_shared(expr* a, expr* b) {
-        TRACE("qe", tout << mk_pp(a, m) << " " << mk_pp(b, m) << "\n";);
         struct fun_proc {
             obj_hashtable<func_decl> s;
             void operator()(app* a) { if (is_uninterp(a)) s.insert(a->get_decl()); }
@@ -75,6 +74,9 @@ namespace qe {
         };
         intersect_proc symbols_in_b(*this, symbols_in_a.s);
         quick_for_each_expr(symbols_in_b, marks, b);
+        TRACE("qe", 
+              tout << mk_pp(a, m) << "\n" << mk_pp(b, m) << "\n";
+              for (func_decl* f : m_shared) tout << f->get_name() << " "; tout << "\n";);
     }
 
     lbool mbi_plugin::check(expr_ref_vector& lits, model_ref& mdl) {
@@ -350,16 +352,57 @@ namespace qe {
 
     /**
        \brief add difference certificates to formula.       
-       
     */
     void uflia_mbi::add_dcert(model_ref& mdl, expr_ref_vector& lits) {        
         term_graph tg(m);
+        add_arith_dcert(*mdl.get(), lits);
         func_decl_ref_vector shared(m_shared_trail);
         tg.set_vars(shared, false);
         lits.append(tg.dcert(*mdl.get(), lits));
         TRACE("qe", tout << "project: " << lits << "\n";);                
     }
 
+    /**
+       Add disequalities between functions that appear in arithmetic context.
+     */
+    void uflia_mbi::add_arith_dcert(model& mdl, expr_ref_vector& lits) {
+        obj_map<func_decl, ptr_vector<app>> apps;
+        arith_util a(m);
+        for (expr* e : subterms(lits)) {
+            if (a.is_int_real(e) && is_uninterp(e) && to_app(e)->get_num_args() > 0) {
+                func_decl* f = to_app(e)->get_decl();
+                auto* v = apps.insert_if_not_there2(f, ptr_vector<app>());
+                v->get_data().m_value.push_back(to_app(e));
+            }
+        }
+        for (auto const& kv : apps) {
+            ptr_vector<app> const& es = kv.m_value;
+            expr_ref_vector values(m);
+            for (expr* e : kv.m_value) values.push_back(mdl(e));
+            for (unsigned i = 0; i < es.size(); ++i) {
+                expr* v1 = values.get(i);
+                for (unsigned j = i + 1; j < es.size(); ++j) {
+                    expr* v2 = values.get(j);
+                    if (v1 != v2) {
+                        add_arith_dcert(mdl, lits, es[i], es[j]);
+                    }
+                }
+            }
+        }
+    }
+
+    void uflia_mbi::add_arith_dcert(model& mdl, expr_ref_vector& lits, app* a, app* b) {
+        arith_util arith(m);
+        SASSERT(a->get_decl() == b->get_decl());
+        for (unsigned i = a->get_num_args(); i-- > 0; ) {
+            expr* arg1 = a->get_arg(i), *arg2 = b->get_arg(i);
+            if (arith.is_int_real(arg1) && mdl(arg1) != mdl(arg2)) {
+                lits.push_back(m.mk_not(m.mk_eq(arg1, arg2)));
+                return;
+            }                
+        }
+    }
+
     /**
      * \brief project private symbols.
      */

src/qe/qe_mbi.h

@@ -123,6 +123,8 @@ namespace qe {
         void order_avars(app_ref_vector& avars);
 
         void add_dcert(model_ref& mdl, expr_ref_vector& lits);
+        void add_arith_dcert(model& mdl, expr_ref_vector& lits);
+        void add_arith_dcert(model& mdl, expr_ref_vector& lits, app* a, app* b);
         app_ref_vector get_arith_vars(expr_ref_vector const& lits);
         vector<def> arith_project(model_ref& mdl, app_ref_vector& avars, expr_ref_vector& lits);
         void project_euf(model_ref& mdl, expr_ref_vector& lits);

src/qe/qe_solve_plugin.cpp

@@ -100,7 +100,7 @@ namespace qe {
                     v = e;
                     a_val = rational(1)/a_val;
                     t = mk_term(is_int, a_val, sign, done);
-                    TRACE("qe", tout << mk_pp(lhs, m) << " " << mk_pp(rhs, m) << " " << mk_pp(e, m) << " := " << t << "\n";);
+                    TRACE("qe", tout << mk_pp(e, m) << " := " << t << "\n";);
                     return true;
                 }
                 else {
@@ -147,7 +147,7 @@ namespace qe {
         }
 
 
-        expr_ref mk_eq_core (expr *e1, expr *e2) {
+        expr_ref mk_eq_core(expr *e1, expr *e2) {
             expr_ref v(m), t(m);
             if (solve(e1, e2, v, t)) {
                 return expr_ref(m.mk_eq(v, t), m);
@@ -201,7 +201,7 @@ namespace qe {
             return a.mk_ge(arg, mk_zero());
         }
 
-        bool mk_le_core (expr *arg1, expr * arg2, expr_ref &result) {
+        bool mk_le_core(expr *arg1, expr * arg2, expr_ref &result) {
             // t <= -1  ==> t < 0 ==> ! (t >= 0)
             rational n;
             if (a.is_int (arg1) && a.is_minus_one (arg2)) {
@@ -220,16 +220,16 @@ namespace qe {
             return false;
         }
 
-        expr * mk_zero () {
+        expr * mk_zero() {
             return a.mk_numeral (rational (0), true);
         }
 
-        bool is_one (expr const * n) const {
+        bool is_one(expr const * n) const {
             rational val;
             return a.is_numeral (n, val) && val.is_one ();
         }
 
-        bool mk_ge_core (expr * arg1, expr * arg2, expr_ref &result) {
+        bool mk_ge_core(expr * arg1, expr * arg2, expr_ref &result) {
             // t >= 1 ==> t > 0 ==> ! (t <= 0)
             rational n;
             if (a.is_int (arg1) && is_one (arg2)) {

src/qe/qe_term_graph.cpp

@@ -725,9 +725,22 @@ namespace qe {
                     TRACE("qe", tout << "skipping " << mk_pp(lit, m) << "\n";);
                 }
             }
+            remove_duplicates(res);
             TRACE("qe", tout << "literals: " << res << "\n";);            
         }
 
+        void remove_duplicates(expr_ref_vector& v) {
+            obj_hashtable<expr> seen;
+            unsigned j = 0;
+            for (expr* e : v) {
+                if (!seen.contains(e)) {
+                    v[j++] = e;
+                    seen.insert(e);
+                }
+            }
+            v.shrink(j);
+        }
+
         vector<ptr_vector<term>> m_decl2terms; // terms that use function f
         ptr_vector<func_decl>    m_decls;
         
@@ -1202,22 +1215,27 @@ namespace qe {
         hashtable<pair_t, pair_t::hash, pair_t::eq> diseqs;
         expr_ref_vector result(m);        
         add_lits(lits);
-        auto const partitions = get_partition(mdl);
         svector<pair_t> todo;
+
+        // TBD: 
+        // M(f(a1 + 5)) != M(f(x1 + 5)) => a1 + 5 != x1 + 5 part of dcert.
+        // collect subterms in arith, put equal function subterms in certifiability set
+
         for (expr* e : lits) {
             expr* ne, *a, *b;
             if (m.is_not(e, ne) && m.is_eq(ne, a, b) && (is_uninterp(a) || is_uninterp(b))) {
-                todo.push_back(pair_t(a, b));
+                diseqs.insert(pair_t(a, b));
             }
             else if (is_uninterp(e)) {
-                todo.push_back(pair_t(e, m.mk_false()));
+                diseqs.insert(pair_t(e, m.mk_false()));
             }
             else if (m.is_not(e, ne) && is_uninterp(ne)) {
-                todo.push_back(pair_t(ne, m.mk_true()));
+                diseqs.insert(pair_t(ne, m.mk_true()));
             }           
         }
-        for (auto& p : todo) diseqs.insert(p);
+        for (auto& p : diseqs) todo.push_back(p);
 
+        auto const partitions = get_partition(mdl);
         obj_map<expr, unsigned> term2pid;
         unsigned id = 0;
         for (auto const& vec : partitions) {