more code

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

src/ast/ast_util.cpp

@@ -195,6 +195,11 @@ expr * mk_not(ast_manager & m, expr * arg) {
         return m.mk_not(arg);
 }
 
+expr_ref mk_not(expr_ref& e) {
+    return expr_ref(mk_not(e.m(), e), e.m());
+}
+
+
 expr_ref push_not(const expr_ref& e) {
     ast_manager& m = e.get_manager();
     if (!is_app(e)) {

src/ast/ast_util.h

@@ -127,6 +127,8 @@ inline expr_ref mk_or(expr_ref_vector const& args) { return expr_ref(mk_or(args.
  */
 expr * mk_not(ast_manager & m, expr * arg);
 
+expr_ref mk_not(expr_ref& e);
+
 /**
    Negate and push over conjunction or disjunction.
  */

src/qe/qe_mbi.cpp

@@ -20,17 +20,52 @@ Revision History:
 
 
 namespace qe {
+
+    euf_mbi_plugin::euf_mbi_plugin(solver* s): m_solver(s) {}
+
+    euf_mbi_plugin::~euf_mbi_plugin() {}
+
+    mbi_result euf_mbi_plugin::operator()(
+        func_decl_ref_vector const& vars, expr_ref_vector& lits, model_ref& mdl) override {
+        // really just a sketch of propositional at this point
+        scoped_push _sp(m_solver);
+        lbool r = m_solver->check_sat(lits);
+        switch (r) {
+        case l_false:
+            lits.reset();
+            m_solver->get_unsat_core(lits);
+            return mbi_unsat;
+        case l_true:
+            m_solver->get_model(mdl);
+            // update lits? to be all propositioal literals or an implicant.
+            // mdl will have map of all constants that we can walk over.
+            return mbi_sat;
+        case l_undef:
+            return mbi_undef;
+        }
+    }
+
+    void euf_mbi_plugin::block(expr_ref_vector const& lits) override {
+        m_solver->assert_expr(mk_not(mk_and(lits)));
+    }    
     
+    /**
+     * ping-pong interpolation of Gurfinkel & Vizel
+     */
     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;
+        bool turn = true;
-        expr_ref_vector itp_a(m), itp_b(m);
+        vector<expr_ref_vector> itps, blocks;
+        ipts.push_back(expr_ref_vector(m));
+        ipts.push_back(expr_ref_vector(m));
+        blocks.push_back(expr_ref_vector(m));
+        blocks.push_back(expr_ref_vector(m));
         mbi_result last_res = mbi_undef;
         while (true) {
-            auto* t1 = a_turn ? &a : &b;
+            auto* t1 = turn ? &a : &b;
-            auto* t2 = a_turn ? &b : &a;
+            auto* t2 = turn ? &b : &a;
             mbi_result next_res = (*t1)(vars, lits, mdl);
             switch (next_res) {
             case mbi_sat:     
@@ -41,21 +76,22 @@ namespace qe {
                 break; // continue
             case mbi_unsat:
                 if (last_res == mbi_unsat) {
-                    // TBD, extract the interpolants
+                    itp = mk_and(itps[turn]);
-                    // of what was blocked.
                     return l_false;
                 }
                 t2->block(lits);
+                expr_ref lemma(m.mk_not(mk_and(lits)), m);
+                blocks[turn].push_back(lemma);
+                itps[turn].push_back(m.mk_implies(mk_and(blocks[!turn]), lemma));
                 lits.reset();  // or find a prefix of lits?
-                next_res = mbi_undef;
+                next_res = mbi_undef; // hard restart.
-                a_turn = !a_turn;
                 break;
             case mbi_augment:
-                a_turn = !a_turn;
                 break;
             case mbi_undef:
                 return l_undef;                    
             }
+            turn = !turn;
             last_res = next_res;
         }
     }