debugging mbi

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

src/ast/for_each_expr.h

@@ -128,6 +128,20 @@ void for_each_expr(ForEachProc & proc, expr * n) {
     for_each_expr_core<ForEachProc, expr_mark, false, false>(proc, visited, n);
 }
 
+template<typename ForEachProc>
+void for_each_expr(ForEachProc & proc, unsigned n, expr * const* es) {
+    expr_mark visited;
+    for (unsigned i = 0; i < n; ++i) 
+        for_each_expr_core<ForEachProc, expr_mark, false, false>(proc, visited, es[i]);
+}
+
+template<typename ForEachProc>
+void for_each_expr(ForEachProc & proc, expr_ref_vector const& es) {
+    expr_mark visited;
+    for (expr* e : es) 
+        for_each_expr_core<ForEachProc, expr_mark, false, false>(proc, visited, e);
+}
+
 template<typename ForEachProc>
 void quick_for_each_expr(ForEachProc & proc, expr_fast_mark1 & visited, expr * n) {
     for_each_expr_core<ForEachProc, expr_fast_mark1, false, false>(proc, visited, n);

src/math/simplex/model_based_opt.cpp

@@ -523,18 +523,26 @@ namespace opt {
         rational slack = (abs_src_c - rational::one()) * (abs_dst_c - rational::one());
         rational dst_val = dst.m_value - x_val*dst_c;
         rational src_val = src.m_value - x_val*src_c;
-        bool use_case1 = 
+        rational distance = src_c * dst_val + dst_c * src_val + slack; 
-            (src_c * dst_val + dst_c * src_val + slack).is_nonpos() 
+        bool use_case1 = distance.is_nonpos() || abs_src_c.is_one() || abs_dst_c.is_one();
-            || abs_src_c.is_one() 
+
-            || abs_dst_c.is_one();
+        if (distance.is_nonpos() && !abs_src_c.is_one() && !abs_dst_c.is_one()) {
+            unsigned r = copy_row(row_src);
+            mul_add(false, r, rational::one(), row_dst);
+            del_var(r, x);
+            add(r, slack);
+            TRACE("qe", tout << m_rows[r];);
+            SASSERT(!m_rows[r].m_value.is_pos());
+        }
 
         if (use_case1) {
+            TRACE("opt", tout << "slack: " << slack << " " << src_c << " " << dst_val << " " << dst_c << " " << src_val << "\n";);
             // dst <- abs_src_c*dst + abs_dst_c*src - slack
             mul(row_dst, abs_src_c);
             sub(row_dst, slack);
-            mul_add(false, row_dst, abs_dst_c, row_src);
+            mul_add(false, row_dst, abs_dst_c, row_src);            
             return;
-        }
+        }        
 
         //
         // create finite disjunction for |b|.                                
@@ -555,6 +563,7 @@ namespace opt {
         //    exists z in [0 .. |b|-2] . |b| | (z + s) && a*n_sign(b)(s + z) + |b|t <= 0
         //
 
+        TRACE("qe", tout << "finite disjunction " << distance << " " << src_c << " " << dst_c << "\n";); 
         vector<var> coeffs;
         if (abs_dst_c <= abs_src_c) {
             rational z = mod(dst_val, abs_dst_c);
@@ -611,6 +620,21 @@ namespace opt {
         r.m_value -= c;
     }
 
+    void model_based_opt::del_var(unsigned dst, unsigned x) {
+        row& r = m_rows[dst];
+        unsigned j = 0; 
+        for (var & v : r.m_vars) {
+            if (v.m_id == x) {
+                r.m_value -= eval(x)*r.m_coeff;
+            }
+            else {
+                r.m_vars[j++] = v;
+            }
+        }
+        r.m_vars.shrink(j);
+    }
+
+
     void model_based_opt::normalize(unsigned row_id) {
         row& r = m_rows[row_id];
         if (r.m_vars.empty()) return;

src/math/simplex/model_based_opt.h

@@ -120,6 +120,8 @@ namespace opt {
 
         void sub(unsigned dst, rational const& c);
 
+        void del_var(unsigned dst, unsigned x);
+
         void set_row(unsigned row_id, vector<var> const& coeffs, rational const& c, rational const& m, ineq_type rel);       
 
         void add_constraint(vector<var> const& coeffs, rational const& c, rational const& m, ineq_type r);

src/qe/qe_arith.cpp

@@ -417,7 +417,7 @@ namespace qe {
                     ts.push_back(t);
                 }
                 t = mk_add(ts);
-                s = a.mk_numeral(-r.m_coeff, a.is_int(t));
+                s = a.mk_numeral(-r.m_coeff, r.m_coeff.is_int() && a.is_int(t));
                 switch (r.m_type) {
                 case opt::t_lt: t = a.mk_lt(t, s); break;
                 case opt::t_le: t = a.mk_le(t, s); break;
@@ -445,7 +445,8 @@ namespace qe {
                     for (var const& v : d.m_vars) {
                         ts.push_back(var2expr(index2expr, v));
                     }
-                    ts.push_back(a.mk_numeral(d.m_coeff, is_int));
+                    if (!d.m_coeff.is_zero()) 
+                        ts.push_back(a.mk_numeral(d.m_coeff, is_int));
                     t = mk_add(ts);
                     if (!d.m_div.is_one() && is_int) {
                         t = a.mk_idiv(t, a.mk_numeral(d.m_div, is_int));
@@ -461,10 +462,12 @@ namespace qe {
         }        
 
         expr_ref mk_add(expr_ref_vector const& ts) {
-            if (ts.size() == 1) {
+            switch (ts.size()) {
+            case 0:
+                return expr_ref(a.mk_int(0), m);
+            case 1:
                 return expr_ref(ts.get(0), m);
-            }
+            default:
-            else {
                 return expr_ref(a.mk_add(ts.size(), ts.c_ptr()), m);
             }
         }

src/qe/qe_mbi.cpp

@@ -259,12 +259,11 @@ 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& shared):
+        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 : shared) m_exclude.insert(f);
         }
         void operator()(app* a) {
-            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);
             }
@@ -291,17 +290,7 @@ namespace qe {
         }
     }
 
-    mbi_result euf_arith_mbi_plugin::operator()(expr_ref_vector& lits, model_ref& mdl) {
+    bool euf_arith_mbi_plugin::get_literals(model_ref& mdl, expr_ref_vector& lits) {
-        lbool r = m_solver->check_sat(lits);
-
-        switch (r) {
-        case l_false:
-            lits.reset();
-            m_solver->get_unsat_core(lits);
-            // optionally minimize core using superposition.
-            return mbi_unsat;
-        case l_true: {
-            m_solver->get_model(mdl);
             model_evaluator mev(*mdl.get());
             lits.reset();
             for (expr* e : m_atoms) {
@@ -313,49 +302,65 @@ namespace qe {
                 }
             }
             TRACE("qe", tout << "atoms from model: " << lits << "\n";);
-            r = m_dual_solver->check_sat(lits);
+        lbool r = m_dual_solver->check_sat(lits);
-            expr_ref_vector core(m);
+        if (l_false == r) {
-            term_graph tg(m);
-            switch (r) {
-            case l_false: {
                 // use the dual solver to find a 'small' implicant
-                m_dual_solver->get_unsat_core(core);
-                TRACE("qe", tout << "core: " << core << "\n";);
                 lits.reset();
-                lits.append(core);
+            m_dual_solver->get_unsat_core(lits);
+            return true;
+        }
+        else {
+            return false;
+        }
+    }
+
+    app_ref_vector euf_arith_mbi_plugin::get_arith_vars(expr_ref_vector const& lits) {
                 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);
+                is_arith_var_proc _proc(avars, m_shared);        
-                for (expr* l : lits) quick_for_each_expr(_proc, l);
+        for_each_expr(_proc, lits);                
-                TRACE("qe", tout << "vars: " << avars << " lits: " << lits << "\n";);
+        return avars;
+    }
 
-                // 1. project arithmetic variables using mdl that satisfies core.
+    mbi_result euf_arith_mbi_plugin::operator()(expr_ref_vector& lits, model_ref& mdl) {
-                //    ground any remaining arithmetic variables using model.
+        lbool r = m_solver->check_sat(lits);
-                arith_project_plugin ap(m);
-                ap.set_check_purified(false);
 
-                auto defs = ap.project(*mdl.get(), avars, lits);
+        switch (r) {
-                // 2. Add the projected definitions to the remaining (euf) literals
+        case l_false:
-                for (auto const& def : defs) {
+            lits.reset();
-                    lits.push_back(m.mk_eq(def.var, def.term));
+            m_solver->get_unsat_core(lits);
-                }
+            TRACE("qe", tout << "unsat core: " << lits << "\n";);
-                TRACE("qe", tout << "# arith defs" << defs.size() << " avars: " << avars << " " << lits << "\n";);
+            // optionally minimize core using superposition.
-
+            return mbi_unsat;
-                // 3. Project the remaining literals with respect to EUF.
+        case l_true: {
-                tg.set_vars(m_shared, false);
+            m_solver->get_model(mdl);
-                tg.add_lits(lits);
+            if (!get_literals(mdl, lits)) {
-                lits.reset();
-                lits.append(tg.project(*mdl));
-                TRACE("qe", tout << "project: " << lits << "\n";);
-                return mbi_sat;
-            }
-            case l_undef:
-                return mbi_undef;
-            case l_true:
-                UNREACHABLE();
                 return mbi_undef;
             }
+            app_ref_vector avars = get_arith_vars(lits);
+
+            TRACE("qe", tout << "vars: " << avars << " lits: " << lits << "\n";);
+
+            // 1. project arithmetic variables using mdl that satisfies core.
+            //    ground any remaining arithmetic variables using model.
+            arith_project_plugin ap(m);
+            ap.set_check_purified(false);
+
+            auto defs = ap.project(*mdl.get(), avars, lits);
+            // 2. Add the projected definitions to the remaining (euf) literals
+            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.
+            term_graph tg(m);
+            tg.set_vars(m_shared, false);
+            tg.add_lits(lits);
+            lits.reset();
+            //lits.append(tg.project(*mdl));
+            lits.append(tg.project());
+            TRACE("qe", tout << "project: " << lits << "\n";);
             return mbi_sat;
         }
         default:
@@ -448,6 +453,7 @@ namespace qe {
                 case l_undef:
                     return l_undef;
                 }
+                break;
             case l_false:
                 itp = mk_and(itps);
                 return l_false;

src/qe/qe_mbi.h

@@ -109,6 +109,10 @@ namespace qe {
         solver_ref   m_dual_solver;
         struct is_atom_proc;
         struct is_arith_var_proc;
+
+        app_ref_vector get_arith_vars(expr_ref_vector const& lits);
+        bool get_literals(model_ref& mdl, expr_ref_vector& lits);
+
     public:
         euf_arith_mbi_plugin(solver* s, solver* sNot);
         ~euf_arith_mbi_plugin() override {}