fixing eufi

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

src/cmd_context/extra_cmds/dbg_cmds.cpp

@@ -435,7 +435,9 @@ public:
         sB->assert_expr(b);
         qe::prop_mbi_plugin pA(sA.get());
         qe::prop_mbi_plugin pB(sB.get());
-        lbool res = mbi.pingpong(pA, pB, vars, itp);
+        pA.set_shared(vars);
+        pB.set_shared(vars);
+        lbool res = mbi.pingpong(pA, pB, itp);
         ctx.regular_stream() << res << " " << itp << "\n";
     }
 };
@@ -485,9 +487,11 @@ public:
         sNotA->assert_expr(m.mk_not(a));
         sB->assert_expr(b);
         sNotB->assert_expr(m.mk_not(b));
-        qe::euf_mbi_plugin pA(sA.get(), sNotA.get());
+        qe::euf_arith_mbi_plugin pA(sA.get(), sNotA.get());
-        qe::euf_mbi_plugin pB(sB.get(), sNotB.get());
+        qe::euf_arith_mbi_plugin pB(sB.get(), sNotB.get());
-        lbool res = mbi.pogo(pA, pB, vars, itp);
+        pA.set_shared(vars);
+        pB.set_shared(vars);
+        lbool res = mbi.pogo(pA, pB, itp);
         ctx.regular_stream() << res << " " << itp << "\n";
     }
 };

src/qe/qe_arith.cpp

@@ -257,7 +257,7 @@ namespace qe {
         };
 
         bool is_arith(expr* e) {
-            return a.is_int(e) || a.is_real(e);
+            return a.is_int_real(e);
         }
 
         rational n_sign(rational const& b) {
@@ -276,7 +276,7 @@ namespace qe {
         bool operator()(model& model, app* v, app_ref_vector& vars, expr_ref_vector& lits) {
             app_ref_vector vs(m);
             vs.push_back(v);
-            (*this)(model, vs, lits);
+            project(model, vs, lits, false);
             return vs.empty();
         }
 
@@ -284,14 +284,6 @@ namespace qe {
         typedef opt::model_based_opt::row row;
         typedef vector<var> vars;
 
-        vector<def> project(model& model, app_ref_vector& vars, expr_ref_vector& lits) {
-            return project(model, vars, lits, true);
-        }
-
-        void operator()(model& model, app_ref_vector& vars, expr_ref_vector& fmls) {
-            project(model, vars, fmls, false);
-        }
-
         expr_ref var2expr(ptr_vector<expr> const& index2expr, var const& v) {
             expr_ref t(index2expr[v.m_id], m);
             if (!v.m_coeff.is_one()) {
@@ -581,11 +573,11 @@ namespace qe {
     }
 
     void arith_project_plugin::operator()(model& model, app_ref_vector& vars, expr_ref_vector& lits) {
-        (*m_imp)(model, vars, lits);
+        m_imp->project(model, vars, lits, false);
     }
 
     vector<def> arith_project_plugin::project(model& model, app_ref_vector& vars, expr_ref_vector& lits) {
-        return m_imp->project(model, vars, lits);
+        return m_imp->project(model, vars, lits, true);
     }
 
     void arith_project_plugin::set_check_purified(bool check_purified) {

src/qe/qe_mbi.cpp

@@ -87,9 +87,9 @@ Notes:
 
 namespace qe {
 
-    lbool mbi_plugin::check(func_decl_ref_vector const& vars, expr_ref_vector& lits, model_ref& mdl) {
+    lbool mbi_plugin::check(expr_ref_vector& lits, model_ref& mdl) {
         while (true) {
-            switch ((*this)(vars, lits, mdl)) {
+            switch ((*this)(lits, mdl)) {
             case mbi_sat:
                 return l_true;
             case mbi_unsat:
@@ -106,12 +106,11 @@ namespace qe {
     // -------------------------------
     // prop_mbi
 
-    prop_mbi_plugin::prop_mbi_plugin(solver* s): m_solver(s) {}
+    prop_mbi_plugin::prop_mbi_plugin(solver* s): mbi_plugin(s->get_manager()), m_solver(s) {}
 
     // sketch of propositional
 
-    mbi_result prop_mbi_plugin::operator()(func_decl_ref_vector const& vars, expr_ref_vector& lits, model_ref& mdl)  {
+    mbi_result prop_mbi_plugin::operator()(expr_ref_vector& lits, model_ref& mdl)  {
-        ast_manager& m = lits.m();
         lbool r = m_solver->check_sat(lits);
         switch (r) {
         case l_false:
@@ -123,7 +122,7 @@ namespace qe {
             lits.reset();
             for (unsigned i = 0, sz = mdl->get_num_constants(); i < sz; ++i) {
                 func_decl* c = mdl->get_constant(i);
-                if (vars.contains(c)) {
+                if (m_shared.contains(c)) {
                     if (m.is_true(mdl->get_const_interp(c))) {
                         lits.push_back(m.mk_const(c));
                     }
@@ -161,7 +160,7 @@ namespace qe {
     };
 
     euf_mbi_plugin::euf_mbi_plugin(solver* s, solver* sNot):
-        m(s->get_manager()),
+        mbi_plugin(s->get_manager()),
         m_atoms(m),
         m_solver(s),
         m_dual_solver(sNot) {
@@ -178,7 +177,7 @@ namespace qe {
         }
     }
 
-    mbi_result euf_mbi_plugin::operator()(func_decl_ref_vector const& vars, expr_ref_vector& lits, model_ref& mdl) {
+    mbi_result euf_mbi_plugin::operator()(expr_ref_vector& lits, model_ref& mdl) {
         lbool r = m_solver->check_sat(lits);
         switch (r) {
         case l_false:
@@ -208,7 +207,7 @@ namespace qe {
                 m_dual_solver->get_unsat_core(core);
                 TRACE("qe", tout << "core: " << core << "\n";);
                 // project the implicant onto vars
-                tg.set_vars(vars, false);
+                tg.set_vars(m_shared, false);
                 tg.add_lits(core);
                 lits.reset();
                 lits.append(tg.project(*mdl));
@@ -260,12 +259,13 @@ namespace qe {
         app_ref_vector& m_vars;
         arith_util      arith;
         obj_hashtable<func_decl> m_exclude;
-        is_arith_var_proc(app_ref_vector& vars, func_decl_ref_vector const& excl): 
+        is_arith_var_proc(app_ref_vector& vars, func_decl_ref_vector const& shared): 
             m(vars.m()), m_vars(vars), arith(m) {
-            for (func_decl* f : excl) m_exclude.insert(f);
+            for (func_decl* f : shared) m_exclude.insert(f);
         }
         void operator()(app* a) {
-            if (arith.is_int_real(a) && a->get_family_id() != a->get_family_id() && !m_exclude.contains(a->get_decl())) {
+            TRACE("qe", tout << expr_ref(a, m) << " " << arith.is_int_real(a) << " " << a->get_family_id() << "\n";);
+            if (arith.is_int_real(a) && a->get_family_id() != arith.get_family_id() && !m_exclude.contains(a->get_decl())) {
                 m_vars.push_back(a);
             }
         }
@@ -274,7 +274,7 @@ namespace qe {
     };
 
     euf_arith_mbi_plugin::euf_arith_mbi_plugin(solver* s, solver* sNot):
-        m(s->get_manager()),
+        mbi_plugin(s->get_manager()),
         m_atoms(m),
         m_solver(s),
         m_dual_solver(sNot) {
@@ -291,13 +291,9 @@ namespace qe {
         }
     }
 
-    mbi_result euf_arith_mbi_plugin::operator()(func_decl_ref_vector const& vars, expr_ref_vector& lits, model_ref& mdl) {
+    mbi_result euf_arith_mbi_plugin::operator()(expr_ref_vector& lits, model_ref& mdl) {
         lbool r = m_solver->check_sat(lits);
 
-        // populate set of arithmetic variables to be projected.
-        app_ref_vector avars(m);
-        is_arith_var_proc _proc(avars, vars);
-        for (expr* l : lits) quick_for_each_expr(_proc, l);
         switch (r) {
         case l_false:
             lits.reset();
@@ -328,6 +324,11 @@ namespace qe {
                 lits.reset();
                 lits.append(core);
                 arith_util a(m);
+                // populate set of arithmetic variables to be projected.
+                app_ref_vector avars(m);
+                is_arith_var_proc _proc(avars, m_shared);        
+                for (expr* l : lits) quick_for_each_expr(_proc, l);
+                TRACE("qe", tout << "vars: " << avars << " lits: " << lits << "\n";);
 
                 // 1. project arithmetic variables using mdl that satisfies core.
                 //    ground any remaining arithmetic variables using model.
@@ -339,9 +340,10 @@ namespace qe {
                 for (auto const& def : defs) {
                     lits.push_back(m.mk_eq(def.var, def.term));
                 }
+                TRACE("qe", tout << "# arith defs" << defs.size() << " avars: " << avars << " " << lits << "\n";);
 
                 // 3. Project the remaining literals with respect to EUF.
-                tg.set_vars(vars, false);
+                tg.set_vars(m_shared, false);
                 tg.add_lits(lits);
                 lits.reset();
                 lits.append(tg.project(*mdl));
@@ -375,7 +377,7 @@ namespace qe {
      * ping-pong interpolation of Gurfinkel & Vizel
      * compute a binary interpolant.
      */
-    lbool interpolator::pingpong(mbi_plugin& a, mbi_plugin& b, func_decl_ref_vector const& vars, expr_ref& itp) {
+    lbool interpolator::pingpong(mbi_plugin& a, mbi_plugin& b, expr_ref& itp) {
         model_ref mdl;
         expr_ref_vector lits(m);
         bool turn = true;
@@ -389,7 +391,7 @@ namespace qe {
         while (true) {
             auto* t1 = turn ? &a : &b;
             auto* t2 = turn ? &b : &a;
-            mbi_result next_res = (*t1)(vars, lits, mdl);
+            mbi_result next_res = (*t1)(lits, mdl);
             switch (next_res) {
             case mbi_sat:
                 if (last_res == mbi_sat) {
@@ -429,14 +431,14 @@ namespace qe {
      * 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) {
+    lbool interpolator::pogo(mbi_plugin& a, mbi_plugin& b, expr_ref& itp) {
         expr_ref_vector lits(m), itps(m);
         while (true) {
             model_ref mdl;
             lits.reset();
-            switch (a.check(vars, lits, mdl)) {
+            switch (a.check(lits, mdl)) {
             case l_true:
-                switch (b.check(vars, lits, mdl)) {
+                switch (b.check(lits, mdl)) {
                 case l_true:
                     return l_true;
                 case l_false:

src/qe/qe_mbi.h

@@ -29,8 +29,21 @@ namespace qe {
     };
 
     class mbi_plugin {
+    protected:
+        ast_manager& m;
+        func_decl_ref_vector m_shared;
     public:
+        mbi_plugin(ast_manager& m): m(m), m_shared(m) {}
         virtual ~mbi_plugin() {}
+
+        /**
+         * Set the shared symbols.
+         */
+        virtual void set_shared(func_decl_ref_vector const& vars) { 
+            m_shared.reset(); 
+            m_shared.append(vars); 
+        }
+
         /**
          * \brief Utility that works modulo a background state.
          * - vars
@@ -50,7 +63,7 @@ namespace qe {
          * - mbi_undef:
          *   inconclusive,
          */
-        virtual mbi_result operator()(func_decl_ref_vector const& vars, expr_ref_vector& lits, model_ref& mdl) = 0;
+        virtual mbi_result operator()(expr_ref_vector& lits, model_ref& mdl) = 0;
 
         /**
          * \brief Block conjunction of lits from future mbi_augment or mbi_sat.
@@ -60,7 +73,7 @@ namespace qe {
         /**
          * \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);
+        lbool check(expr_ref_vector& lits, model_ref& mdl);
 
     };
 
@@ -69,12 +82,11 @@ namespace qe {
     public:
         prop_mbi_plugin(solver* s);
         ~prop_mbi_plugin() override {}
-        mbi_result operator()(func_decl_ref_vector const& vars, expr_ref_vector& lits, model_ref& mdl) override;
+        mbi_result operator()(expr_ref_vector& lits, model_ref& mdl) override;
         void block(expr_ref_vector const& lits) override;
     };
 
     class euf_mbi_plugin : public mbi_plugin {
-        ast_manager& m;
         expr_ref_vector m_atoms;
         solver_ref   m_solver;
         solver_ref   m_dual_solver;
@@ -82,12 +94,11 @@ namespace qe {
     public:
         euf_mbi_plugin(solver* s, solver* sNot);
         ~euf_mbi_plugin() override {}
-        mbi_result operator()(func_decl_ref_vector const& vars, expr_ref_vector& lits, model_ref& mdl) override;
+        mbi_result operator()(expr_ref_vector& lits, model_ref& mdl) override;
         void block(expr_ref_vector const& lits) override;
     };
 
-    class euf_arith_mbi_plugin : mbi_plugin {
+    class euf_arith_mbi_plugin : public mbi_plugin {
-        ast_manager& m;
         expr_ref_vector m_atoms;
         solver_ref   m_solver;
         solver_ref   m_dual_solver;
@@ -96,7 +107,7 @@ namespace qe {
     public:
         euf_arith_mbi_plugin(solver* s, solver* sNot);
         ~euf_arith_mbi_plugin() override {}
-        mbi_result operator()(func_decl_ref_vector const& vars, expr_ref_vector& lits, model_ref& mdl) override;
+        mbi_result operator()(expr_ref_vector& lits, model_ref& mdl) override;
         void block(expr_ref_vector const& lits) override;
     };
 
@@ -107,8 +118,8 @@ namespace qe {
         ast_manager&         m;
     public:
         interpolator(ast_manager& m):m(m) {}
-        lbool pingpong(mbi_plugin& a, mbi_plugin& b, func_decl_ref_vector const& vars, expr_ref& itp);
+        lbool pingpong(mbi_plugin& a, mbi_plugin& b, expr_ref& itp);
-        lbool pogo(mbi_plugin& a, mbi_plugin& b, func_decl_ref_vector const& vars, expr_ref& itp);
+        lbool pogo(mbi_plugin& a, mbi_plugin& b, expr_ref& itp);
     };
 
 };

src/qe/qe_term_graph.cpp

@@ -761,11 +761,15 @@ namespace qe {
                         val2rep.insert(val, rep);
                     }
                 }
+                // TBD: this ignores types, need one use of 'distinct' per sort.
+                // TBD: probably ignore distinct on values
+                // TBD: ignore distinct on Booleans
                 ptr_buffer<expr> reps;
                 for (auto &kv : val2rep) {
                     reps.push_back(kv.m_value);
+                    std::cout << mk_pp(kv.m_value, m) << "\n";
                 }
-                res.push_back(m.mk_distinct(reps.size(), reps.c_ptr()));
+                // res.push_back(m.mk_distinct(reps.size(), reps.c_ptr()));
             }
 
         public: