From 5fc0f56281318080be0fb1cf67af869b40aaaaed Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Fri, 8 Jun 2018 17:03:24 -0700
Subject: [PATCH] sketch mbi

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/qe/qe_mbi.cpp | 62 ++++++++++++++++++++++++++++++++
 src/qe/qe_mbi.h   | 90 +++++++++++++++++++++++++++++++++++++++++++++++
 2 files changed, 152 insertions(+)
 create mode 100644 src/qe/qe_mbi.cpp
 create mode 100644 src/qe/qe_mbi.h

diff --git a/src/qe/qe_mbi.cpp b/src/qe/qe_mbi.cpp
new file mode 100644
index 000000000..13b9067ee
--- /dev/null
+++ b/src/qe/qe_mbi.cpp
@@ -0,0 +1,62 @@
+/*++
+Copyright (c) 2018 Microsoft Corporation
+
+Module Name:
+
+    qe_mbi.cpp
+
+Abstract:
+
+    Model-based interpolation utilities
+
+Author:
+
+    Nikolaj Bjorner (nbjorner), Arie Gurfinkel 2018-6-8
+
+Revision History:
+
+
+--*/
+
+
+namespace qe {
+    
+    lbool interpolator::binary(mbi_plugin& a, mbi_plugin& b, func_decl_ref_vector const& vars, expr_ref& itp) {
+        ast_manager& m = vars.get_manager();
+        model_ref mdl;
+        literal_vector lits(m);
+        bool a_turn = true;
+        expr_ref_vector itp_a(m), itp_b(m);
+        mbi_result last_res = mbi_undef;
+        while (true) {
+            auto* t1 = a_turn ? &a : &b;
+            auto* t2 = a_turn ? &b : &a;
+            mbi_result next_res = (*t1)(vars, lits, mdl);
+            switch (next_res) {
+            case mbi_sat:     
+                if (last_res == mbi_sat) {
+                    itp = nullptr;
+                    return l_true;
+                }
+                break; // continue
+            case mbi_unsat:
+                if (last_res == mbi_unsat) {
+                    // TBD, extract the interpolants
+                    // of what was blocked.
+                    return l_false;
+                }
+                t2->block(lits);
+                lits.reset();  // or find a prefix of lits?
+                next_res = mbi_undef;
+                a_turn = !a_turn;
+                break;
+            case mbi_augment:
+                a_turn = !a_turn;
+                break;
+            case mbi_undef:
+                return l_undef;                    
+            }
+            last_res = next_res;
+        }
+    }
+};
diff --git a/src/qe/qe_mbi.h b/src/qe/qe_mbi.h
new file mode 100644
index 000000000..4aad92f82
--- /dev/null
+++ b/src/qe/qe_mbi.h
@@ -0,0 +1,90 @@
+/*++
+Copyright (c) 2018 Microsoft Corporation
+
+Module Name:
+
+    qe_mbi.h
+
+Abstract:
+
+    Model-based interpolation utilities
+
+Author:
+
+    Nikolaj Bjorner (nbjorner), Arie Gurfinkel 2018-6-8
+
+Revision History:
+
+
+--*/
+
+#pragma once
+
+namespace qe {
+    enum mbi_result {
+        mbi_sat,
+        mbi_unsat,
+        mbi_augment,
+        mbi_undef,
+    };
+
+    class mbi_plugin {
+        virtual ~mbi_plugin();
+        /**
+         * \brief Utility that works modulo a background state.
+         * - vars
+         *   variables to preferrably project onto (other variables would require quantification to fit interpolation signature)
+         * - lits 
+         *   set of literals to check satisfiability with respect to.
+         * - mdl
+         *   optional model for caller. 
+         * on return:
+         * - mbi_sat:
+         *   populates mdl with a satisfying state, and lits with implicant for background state.
+         * - mbi_unsat:
+         *   populates lits to be inconsistent with background state. 
+         *   For all practical purposes it is a weakening of lits or even a subset of lits.
+         * - mbi_augment:
+         *   populates lits with strengthening of lits (superset) 
+         * - mbi_undef:
+         *   inconclusive, 
+         */
+        virtual mbi_result operator()(func_decl_ref_vector const& vars, expr_ref_vector& lits, model_ref& mdl) = 0;
+
+        /**
+         * \brief Block conjunction of lits from future mbi_augment or mbi_sat.
+         */
+        virtual void block(expr_ref_vector const& lits) = 0;
+    };
+
+    class euf_mbi_plugin : mbi_plugin {
+        solver_ref m_solver;
+    public:
+        euf_mbi_plugin(solver* s);
+        ~euf_mbi_plugin() override {}
+        mbi_result operator()(func_decl_ref_vector const& vars, expr_ref_vector& lits, model_ref& mdl) override;
+        void block(expr_ref_vector const& lits) override;
+    };
+
+    /**
+     * use cases for interpolation.
+     */
+    class interpolator {
+        static lbool binary(mbi_plugin& a, mbi_plugin& b, func_decl_ref_vector const& vars, expr_ref& itp);
+    };
+
+#if 0
+    TBD some other scenario, e.g., Farkas, Cute/Beautiful/maybe even Selfless
+
+    class solver_mbi_plugin : public mbi_plugin {
+        solver_ref m_solver;
+    public:
+        solver_mbi_plugin(solver* s);
+        ~solver_mbi_plugin() override {}
+        mbi_result operator()(func_decl_ref_vector const& vars, expr_ref_vector& lits, model_ref& mdl) override;
+        void block(expr_ref_vector const& lits) override;
+    };
+
+
+#endif
+};