updates

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

src/qe/qe_mbi.cpp

@@ -19,12 +19,32 @@ Revision History:
 --*/
 
 #include "ast/ast_util.h"
+#include "ast/rewriter/bool_rewriter.h"
 #include "solver/solver.h"
 #include "qe/qe_mbi.h"
 
 
 namespace qe {
 
+    lbool mbi_plugin::check(func_decl_ref_vector const& vars, expr_ref_vector& lits, model_ref& mdl) {
+        SASSERT(lits.empty());
+        while (true) {
+            switch ((*this)(vars, lits, mdl)) {
+            case mbi_sat:
+                return l_true;
+            case mbi_unsat:
+                if (lits.empty()) return l_false;
+                block(lits);
+                break;
+            case mbi_undef:
+                return l_undef;
+            case mbi_augment:
+                break;
+            }
+        }
+    }
+
+
     // -------------------------------
     // prop_mbi
 
@@ -116,6 +136,7 @@ namespace qe {
         blocks.push_back(expr_ref_vector(m));
         blocks.push_back(expr_ref_vector(m));
         mbi_result last_res = mbi_undef;
+        bool_rewriter rw(m);
         while (true) {
             auto* t1 = turn ? &a : &b;
             auto* t2 = turn ? &b : &a;
@@ -156,10 +177,32 @@ namespace qe {
     }
 
     /**
-     * TBD: also implement the one-sided versions that create clausal interpolants.
+     * One-sided pogo creates clausal interpolants.
+     * It creates a set of consequences of b that are inconsistent with a.
      */
     lbool interpolator::pogo(mbi_plugin& a, mbi_plugin& b, func_decl_ref_vector const& vars, expr_ref& itp) {
-        NOT_IMPLEMENTED_YET();
+        expr_ref_vector lits(m), itps(m);
+        while (true) {
+            model_ref mdl;
+            lits.reset();
+            switch (a.check(vars, lits, mdl)) {
+            case l_true:
+                switch (b.check(vars, lits, mdl)) {
+                case l_true:
+                    return l_true;
+                case l_false:
+                    a.block(lits);
+                    itps.push_back(mk_not(mk_and(lits)));
+                    break;
+                case l_undef:
                     return l_undef;
                 }
+            case l_false:
+                itp = mk_and(itps);
+                return l_false;
+            case l_undef:
+                return l_undef;
+            }
+        }
+    }
 };

src/qe/qe_mbi.h

@@ -56,6 +56,12 @@ namespace qe {
          * \brief Block conjunction of lits from future mbi_augment or mbi_sat.
          */
         virtual void block(expr_ref_vector const& lits) = 0;
+
+        /**
+         * \brief perform a full check, consume internal auguments if necessary.
+         */
+        lbool check(func_decl_ref_vector const& vars, expr_ref_vector& lits, model_ref& mdl);
+
     };
 
     class prop_mbi_plugin : public mbi_plugin {

src/qe/qe_term_graph.cpp

@@ -395,7 +395,7 @@ namespace qe {
     
     void term_graph::internalize_eq(expr *a1, expr* a2) {
         SASSERT(m_merge.empty());
-        merge(internalize_term(a1)->get_root(), internalize_term(a2)->get_root());
+        merge(*internalize_term(a1), *internalize_term(a2));
         merge_flush();
         SASSERT(m_merge.empty());
     }
@@ -424,13 +424,11 @@ namespace qe {
         m_term2app.reset();
         m_pinned.reset();  
         
-        SASSERT(t1.is_root());
-        SASSERT(t2.is_root());
+        term *a = &t1.get_root();
+        term *b = &t2.get_root();
         
-        if (&t1 == &t2) return;
+        if (a == b) return;
         
-        term *a = &t1;
-        term *b = &t2;
         if (a->get_class_size() > b->get_class_size()) {
             std::swap(a, b);
         }