From c816d45a7def3f7ca18fa3e94f28f7450c183a05 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 19 Jan 2020 15:58:17 -0600
Subject: [PATCH] share some equalities

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/cmd_context/basic_cmds.cpp | 17 ++---------------
 src/qe/qe_mbi.cpp              | 35 +++++++++++++++++++++++++++++-----
 src/qe/qe_mbi.h                |  1 +
 src/qe/qe_term_graph.cpp       | 10 ++++++++++
 4 files changed, 43 insertions(+), 20 deletions(-)

diff --git a/src/cmd_context/basic_cmds.cpp b/src/cmd_context/basic_cmds.cpp
index 83e3e1a44..dd30ca634 100644
--- a/src/cmd_context/basic_cmds.cpp
+++ b/src/cmd_context/basic_cmds.cpp
@@ -872,22 +872,9 @@ public:
     void execute(cmd_context & ctx) override { 
         ast_manager& m = ctx.m();
         qe::interpolator mbi(m);
-        expr_ref a(m_a, m);
-        expr_ref b(m_b, m);
         expr_ref itp(m);
-        solver_factory& sf = ctx.get_solver_factory();
-        params_ref p;
-        solver_ref sA = sf(m, p, false /* no proofs */, true, true, symbol::null);
-        solver_ref sB = sf(m, p, false /* no proofs */, true, true, symbol::null);
-        solver_ref sNotA = sf(m, p, false /* no proofs */, true, true, symbol::null);
-        sA->assert_expr(a);
-        sB->assert_expr(b);
-        qe::uflia_mbi pA(sA.get(), sNotA.get());
-        qe::prop_mbi_plugin pB(sB.get());
-        pA.set_shared(a, b);
-        pB.set_shared(a, b);
-        lbool res = mbi.pogo(pA, pB, itp);
-        ctx.regular_stream() << res << " " << itp << "\n";
+        lbool res = mbi.pogo(ctx.get_solver_factory(), m_a, m_b, itp);
+        ctx.regular_stream() << itp << "\n";
     }
 };
 
diff --git a/src/qe/qe_mbi.cpp b/src/qe/qe_mbi.cpp
index 23ef7229b..1f96f3387 100644
--- a/src/qe/qe_mbi.cpp
+++ b/src/qe/qe_mbi.cpp
@@ -33,6 +33,7 @@ Notes:
 #include "ast/for_each_expr.h"
 #include "ast/rewriter/expr_safe_replace.h"
 #include "ast/rewriter/bool_rewriter.h"
+#include "ast/rewriter/th_rewriter.h"
 #include "ast/arith_decl_plugin.h"
 #include "model/model_evaluator.h"
 #include "solver/solver.h"
@@ -307,11 +308,17 @@ namespace qe {
         auto avars = get_arith_vars(lits);
         vector<def> defs = arith_project(mdl, avars, alits);
         for (auto const& d : defs) uflits.push_back(m.mk_eq(d.var, d.term));
+        TRACE("qe", tout << "uflits: " << uflits << "\n";);
         project_euf(mdl, uflits);
         lits.reset();
         lits.append(alits);
         lits.append(uflits);
         IF_VERBOSE(10, verbose_stream() << "projection : " << lits << "\n");
+        TRACE("qe", 
+              tout << "projection: " << lits << "\n";
+              tout << "avars: " << avars << "\n";
+              tout << "alits: " << lits << "\n";
+              tout << "uflits: " << uflits << "\n";);
     }
 
     void uflia_mbi::split_arith(expr_ref_vector const& lits, 
@@ -334,6 +341,9 @@ namespace qe {
                 uflits.push_back(lit);
             }
         }
+        TRACE("qe", 
+              tout << "alits: " << alits << "\n";
+              tout << "uflits: " << uflits << "\n";);
     }
 
 
@@ -341,9 +351,6 @@ namespace qe {
     /**
        \brief add difference certificates to formula.
        
-       First version just uses an Ackerman reduction.
-
-       It should be replaced by DCert.
     */
     void uflia_mbi::add_dcert(model_ref& mdl, expr_ref_vector& lits) {        
         term_graph tg(m);
@@ -462,14 +469,14 @@ namespace qe {
                     return l_true;
                 case l_false:
                     a.block(lits);
-                    itps.push_back(mk_not(mk_and(lits)));
+                    itps.push_back(mk_and(lits));
                     break;
                 case l_undef:
                     return l_undef;
                 }
                 break;
             case l_false:
-                itp = mk_and(itps);
+                itp = mk_or(itps);
                 return l_false;
             case l_undef:
                 return l_undef;
@@ -477,4 +484,22 @@ namespace qe {
         }
     }
 
+    lbool interpolator::pogo(solver_factory& sf, expr* _a, expr* _b, expr_ref& itp) {
+        params_ref p;
+        expr_ref a(_a, m), b(_b, m);
+        th_rewriter rewrite(m);
+        rewrite(a);
+        rewrite(b);
+        solver_ref sA = sf(m, p, false /* no proofs */, true, true, symbol::null);
+        solver_ref sB = sf(m, p, false /* no proofs */, true, true, symbol::null);
+        solver_ref sNotA = sf(m, p, false /* no proofs */, true, true, symbol::null);
+        sA->assert_expr(a);
+        sB->assert_expr(b);
+        uflia_mbi pA(sA.get(), sNotA.get());
+        prop_mbi_plugin pB(sB.get());
+        pA.set_shared(a, b);
+        pB.set_shared(a, b);
+        return pogo(pA, pB, itp);
+    }
+
 };
diff --git a/src/qe/qe_mbi.h b/src/qe/qe_mbi.h
index e602f407b..72ff9dbcb 100644
--- a/src/qe/qe_mbi.h
+++ b/src/qe/qe_mbi.h
@@ -146,6 +146,7 @@ namespace qe {
         interpolator(ast_manager& m):m(m) {}
         lbool pingpong(mbi_plugin& a, mbi_plugin& b, expr_ref& itp);
         lbool pogo(mbi_plugin& a, mbi_plugin& b, expr_ref& itp);
+        lbool pogo(solver_factory& sf, expr* a, expr* b, expr_ref& itp);
     };
 
 };
diff --git a/src/qe/qe_term_graph.cpp b/src/qe/qe_term_graph.cpp
index 6bfad07d7..33a0c02bb 100644
--- a/src/qe/qe_term_graph.cpp
+++ b/src/qe/qe_term_graph.cpp
@@ -1264,6 +1264,16 @@ namespace qe {
                 }
             }
         }
+        for (auto const& terms : partitions) {
+            expr* a = nullptr;
+            for (expr* b : terms) { 
+                if (is_uninterp(b)) 
+                    if (a) 
+                        result.push_back(m.mk_eq(a, b));
+                    else 
+                        a = b;
+            }
+        }
         TRACE("qe", tout << result << "\n";);
         return result;
     }