fix proof checking for bounds propagation

src/math/lp/explanation.h

@@ -73,13 +73,14 @@ public:
     };
     class iterator {
         bool      m_run_on_vector;
+        mpq       m_one = one_of_type<mpq>();
         pair_vec::const_iterator    m_vi;
         ci_set::iterator            m_ci;
     public:
         cimpq operator*() const {
             return m_run_on_vector?
                 cimpq( m_vi->first, m_vi->second) :
-                cimpq( *m_ci, one_of_type<mpq>()); 
+                cimpq( *m_ci, m_one); 
         }        
         iterator operator++() {
             if (m_run_on_vector)

src/math/lp/gomory.cpp

@@ -82,7 +82,8 @@ class create_cut {
         TRACE("gomory_cut_detail", tout << "new_a = " << new_a << ", k = " << m_k << ", lcm_den = " << m_lcm_den << "\n";);
 #if SMALL_CUTS
         // if (numerator(new_a).is_big()) throw found_big(); 
-        if (numerator(new_a) > m_big_number) throw found_big(); 
+        if (numerator(new_a) > m_big_number)
+            throw found_big(); 
 #endif
     }
 
@@ -90,28 +91,24 @@ class create_cut {
         TRACE("gomory_cut_detail_real", tout << "j = " << j << ", a = " << a << ", m_k = " << m_k << "\n";);
         mpq new_a;
         if (at_lower(j)) {
-            if (a.is_pos()) {
+            if (a.is_pos()) 
                 // the delta is a (x - f) is positive it has to grow and fight m_one_minus_f
                 new_a = a / m_one_minus_f;
-            }
+            else 
-            else {
                 // the delta is negative and it works again m_f
                 new_a = - a / m_f;
-            }
             m_k.addmul(new_a, lower_bound(j).x); // is it a faster operation than
             // k += lower_bound(j).x * new_a;  
             m_ex->push_back(column_lower_bound_constraint(j));
         }
         else {
             lp_assert(at_upper(j));
-            if (a.is_pos()) {
+            if (a.is_pos()) 
                 // the delta is works again m_f
                 new_a =  - a / m_f; 
-            }
+            else 
-            else {
                 // the delta is positive works again m_one_minus_f
                 new_a =   a / m_one_minus_f; 
-            }
             m_k.addmul(new_a, upper_bound(j).x); //  k += upper_bound(j).x * new_a; 
             m_ex->push_back(column_upper_bound_constraint(j));
         }
@@ -121,7 +118,8 @@ class create_cut {
         
 #if SMALL_CUTS
         // if (numerator(new_a).is_big()) throw found_big(); 
-        if (numerator(new_a) > m_big_number) throw found_big(); 
+        if (numerator(new_a) > m_big_number)
+            throw found_big(); 
 #endif
     }
 
@@ -146,13 +144,15 @@ class create_cut {
                 if (!m_k.is_int())
                     m_k = ceil(m_k);
                 m_t.add_monomial(mpq(1), v);
-            } else {
+            }
+            else {
                 m_k /= -a;
                 if (!m_k.is_int())
                     m_k = ceil(m_k);
                 m_t.add_monomial(-mpq(1), v);
             }
-        } else {
+        }
+        else {
             m_lcm_den = lcm(m_lcm_den, denominator(m_k));
             lp_assert(m_lcm_den.is_pos());
             TRACE("gomory_cut_detail", tout << "pol.size() > 1 den: " << m_lcm_den << std::endl;);
@@ -176,14 +176,12 @@ class create_cut {
     }
 
     std::ostream& dump_coeff_val(std::ostream & out, const mpq & a) const {
-        if (a.is_int()) {
+        if (a.is_int()) 
             out << a;
-        } 
         else if ( a >= zero_of_type<mpq>())
             out << "(/ " << numerator(a) << " " << denominator(a) << ")";
-        else {
+        else 
             out << "(- (/ " <<   numerator(-a) << " " << denominator(-a) << "))";
-        }
         return out;
     }
     
@@ -197,12 +195,10 @@ class create_cut {
     
     std::ostream& dump_row_coefficients(std::ostream & out) const {
         mpq lc(1);
-        for (const auto& p : m_row) {
+        for (const auto& p : m_row) 
             lc = lcm(lc, denominator(p.coeff())); 
-        }        
+        for (const auto& p : m_row) 
-        for (const auto& p : m_row) {
             dump_coeff_val(out << " (* ", p.coeff()*lc) << " " << var_name(p.var()) << ")";
-        }
         return out;
     }
     
@@ -218,9 +214,8 @@ class create_cut {
     
     void dump_declarations(std::ostream& out) const {
         // for a column j the var name is vj
-        for (const auto & p : m_row) {
+        for (const auto & p : m_row) 
             dump_declaration(out, p.var());
-        }
         for (lar_term::ival p : m_t) {
             auto t = lia.lra.column2tv(p.column());
             if (t.is_term()) {
@@ -239,12 +234,11 @@ class create_cut {
     void dump_explanations(std::ostream& out) const {
         for (const auto & p : m_row) {            
             unsigned j = p.var();
-            if (j == m_inf_col || (!is_real(j) && p.coeff().is_int())) {
+            if (j == m_inf_col || (!is_real(j) && p.coeff().is_int())) 
                 continue;
-            }
+            else if (at_lower(j)) 
-            else if (at_lower(j)) {
                 dump_lower_bound_expl(out, j);
-            } else {
+            else {
                 lp_assert(at_upper(j));
                 dump_upper_bound_expl(out, j);
             }
@@ -252,9 +246,8 @@ class create_cut {
     }
 
     std::ostream& dump_term_coefficients(std::ostream & out) const {
-        for (lar_term::ival p : m_t) {
+        for (lar_term::ival p : m_t) 
             dump_coeff(out, p);
-        }
         return out;
     }
     
@@ -281,9 +274,8 @@ class create_cut {
 public:
     void dump(std::ostream& out) {
         out << "applying cut at:\n"; print_linear_combination_indices_only<row_strip<mpq>, mpq>(m_row, out); out << std::endl;
-        for (auto & p : m_row) {
+        for (auto & p : m_row) 
             lia.lra.print_column_info(p.var(), out);
-        }
         out << "inf_col = " << m_inf_col << std::endl;
     }
 
@@ -304,7 +296,8 @@ public:
         m_abs_max = 0;
         for (const auto & p : m_row) {
             mpq t = abs(ceil(p.coeff()));
-            if (t > m_abs_max) m_abs_max = t;
+            if (t > m_abs_max)
+                m_abs_max = t;
         }
         m_big_number = m_abs_max.expt(2);
 #endif
@@ -324,9 +317,8 @@ public:
                     m_ex->push_back(column_upper_bound_constraint(j));
                     continue;
                 }
-                if (is_real(j)) {  
+                if (is_real(j))   
                     real_case_in_gomory_cut(- p.coeff(), j);
-                } 
                 else if (!p.coeff().is_int()) {
                     some_int_columns = true;
                     m_fj = fractional_part(-p.coeff());
@@ -411,7 +403,8 @@ int gomory::find_basic_var() {
 lia_move gomory::operator()() {
     lra.move_non_basic_columns_to_bounds(true);
     int j = find_basic_var();
-    if (j == -1) return lia_move::undef;
+    if (j == -1)
+        return lia_move::undef;
     unsigned r = lia.row_of_basic_column(j);
     const row_strip<mpq>& row = lra.get_row(r);
     SASSERT(lra.row_is_correct(r));

src/sat/sat_drat.cpp

@@ -918,6 +918,9 @@ namespace sat {
         case hint_type::farkas_h:
             ous << "farkas ";
             break;
+        case hint_type::bound_h:
+            ous << "bound ";
+            break;
         case hint_type::cut_h:
             ous << "cut ";
             break;
@@ -946,6 +949,11 @@ namespace sat {
                 s += 6;
                 return true;
             }
+            if (0 == strncmp(s, "bound", 5)) {
+                h.m_ty = hint_type::bound_h;
+                s += 5;
+                return true;
+            }
             if (0 == strncmp(s, "cut", 3)) {
                 h.m_ty = hint_type::cut_h;
                 s += 3;

src/sat/sat_types.h

@@ -97,6 +97,7 @@ namespace sat {
     enum class hint_type {
         null_h,
         farkas_h,
+        bound_h,
         cut_h
     };
 

src/sat/smt/arith_diagnostics.cpp

@@ -94,7 +94,9 @@ namespace arith {
         m_bounds_pragma.m_ty = ty;
         m_bounds_pragma.m_literals.reset();
         m_bounds_pragma.m_eqs.reset();
-        for (auto ev : m_explanation) {
+        unsigned i = 0;
+        for (auto const & ev : m_explanation) {
+            ++i;
             auto idx = ev.ci();
             if (UINT_MAX == idx)
                 continue;

src/sat/smt/arith_solver.cpp

@@ -232,14 +232,13 @@ namespace arith {
         if (v == euf::null_theory_var)
             return;
 
-        TRACE("arith", tout << "v" << v << " " << be.kind() << " " << be.m_bound << "\n";);
-
         reserve_bounds(v);
 
-        if (m_unassigned_bounds[v] == 0 && !should_refine_bounds()) {
+        if (m_unassigned_bounds[v] == 0 && !should_refine_bounds()) 
-            TRACE("arith", tout << "return\n";);
             return;
-        }
+
+        TRACE("arith", tout << "lp bound v" << v << " " << be.kind() << " " << be.m_bound << "\n";);
+
         lp_bounds const& bounds = m_bounds[v];
         bool first = true;
         for (unsigned i = 0; i < bounds.size(); ++i) {
@@ -249,7 +248,7 @@ namespace arith {
             literal lit = is_bound_implied(be.kind(), be.m_bound, *b);
             if (lit == sat::null_literal) 
                 continue;
-            TRACE("arith", tout << lit << " bound: " << *b << " first: " << first << "\n";);
+            TRACE("arith", tout << "lp bound " << lit << " bound: " << *b << " first: " << first << "\n";);
 
             lp().settings().stats().m_num_of_implied_bounds++;
             if (first) {
@@ -263,7 +262,7 @@ namespace arith {
             TRACE("arith", for (auto lit : m_core) tout << lit << ": " << s().value(lit) << "\n";);
             DEBUG_CODE(for (auto lit : m_core) { VERIFY(s().value(lit) == l_true); });
             ++m_stats.m_bound_propagations1;
-            assign(lit, m_core, m_eqs, explain(sat::hint_type::farkas_h, lit));
+            assign(lit, m_core, m_eqs, explain(sat::hint_type::bound_h, lit));
         }
 
         if (should_refine_bounds() && first)

src/shell/drat_frontend.cpp

@@ -160,7 +160,7 @@ public:
         // m_drat.add(lits, st);
     }
 
-    void validate_hint(expr_ref_vector const& exprs, sat::literal_vector const& lits, sat::proof_hint const& hint) {
+    bool validate_hint(expr_ref_vector const& exprs, sat::literal_vector const& lits, sat::proof_hint const& hint) {
         // return; // remove when testing this
         proof_checker pc(m);
         arith_util autil(m);
@@ -168,16 +168,18 @@ public:
         case sat::hint_type::null_h:
             break;
         case sat::hint_type::cut_h:
+        case sat::hint_type::bound_h:
         case sat::hint_type::farkas_h: {
-            expr_ref sum(m);
+            expr_ref sum(m), last_sum(m);
             bool is_strict = false;
             vector<rational> coeffs;
             rational lc(1);
-            for (auto const& [coeff, lit] : hint.m_literals) {
+            for (auto const& [coeff, a, b]: hint.m_eqs) {
                 coeffs.push_back(coeff);
                 lc = lcm(lc, denominator(coeff)); 
             }
-            for (auto const& [coeff, a, b]: hint.m_eqs) {
+
+            for (auto const& [coeff, lit] : hint.m_literals) {
                 coeffs.push_back(coeff);
                 lc = lcm(lc, denominator(coeff)); 
             }
@@ -186,14 +188,6 @@ public:
                     coeff *= lc;
             
             unsigned i = 0;
-            for (auto const& [coeff, lit] : hint.m_literals) {
-                app_ref e(to_app(m_b2e[lit.var()]), m);
-                if (!pc.check_arith_literal(!lit.sign(), e, coeffs[i], sum, is_strict)) {
-                    std::cout << "p failed checking hint " << e << "\n";
-                    return;
-                }                    
-                ++i;
-            }
             for (auto const& [coeff, a, b]: hint.m_eqs) {
                 expr* x = exprs[a];
                 expr* y = exprs[b];
@@ -201,14 +195,41 @@ public:
                 app_ref e(m.mk_eq(x, y), m);
                 if (!pc.check_arith_literal(true, e, coeffs[i], sum, is_strict)) {
                     std::cout << "p failed checking hint " << e << "\n";
-                    return;
+                    return false;
+                }
+                ++i;
+            }
+
+            for (auto const& [coeff, lit] : hint.m_literals) {
+                last_sum = sum;
+                app_ref e(to_app(m_b2e[lit.var()]), m);
+                if (!pc.check_arith_literal(!lit.sign(), e, coeffs[i], sum, is_strict)) {
+                    std::cout << "p failed checking hint " << e << "\n";
+                    return false;
                 }                    
                 ++i;
             }
 
             if (!sum.get()) {
                 std::cout << "p no summation\n";
-                return;
+                return false;
+            }
+
+            th_rewriter rw(m);
+            if (sat::hint_type::bound_h == hint.m_ty) {
+                rw(last_sum);
+                sum = last_sum;
+                auto const& [coeff, lit] = hint.m_literals.back();
+                rational last_coeff = coeff, r;
+                expr* x, *y, *z;
+                if (autil.is_add(sum)) {                    
+                    x = to_app(sum)->get_arg(1);
+                    if (autil.is_mul(x, y, z) && autil.is_numeral(y, r)) {
+                        last_coeff = r;
+                    }
+                }
+                app_ref e(to_app(m_b2e[lit.var()]), m);
+                VERIFY(pc.check_arith_literal(!lit.sign(), e, last_coeff, sum, is_strict));                
             }
 
             if (is_strict) 
@@ -216,11 +237,29 @@ public:
             else 
                 sum = autil.mk_le(sum, autil.mk_numeral(rational(0), sum->get_sort()));
             
-            th_rewriter rw(m);
             rw(sum);
             if (!m.is_false(sum)) {
+                // check hint:
                 std::cout << "p hint not verified " << sum << "\n";
-                return;
+                auto const& [coeff, lit] = hint.m_literals.back();
+                expr_ref sum1(m);
+                bool is_strict1 = false;
+                app_ref e(to_app(m_b2e[lit.var()]), m);
+                rational coeffb = coeffs.back();
+                VERIFY(pc.check_arith_literal(!lit.sign(), e, coeffb, sum1, is_strict1));
+                std::cout << last_sum << " => ~" << sum1 << "\n";
+                for (auto const& [coeff, a, b]: hint.m_eqs) {
+                    expr* x = exprs[a];
+                    expr* y = exprs[b];
+                    app_ref e(m.mk_eq(x, y), m);
+                    std::cout << e << "\n";
+                }
+                for (auto const& [coeff, lit] : hint.m_literals) {
+                    app_ref e(to_app(m_b2e[lit.var()]), m);
+                    if (lit.sign()) e = m.mk_not(e);
+                    std::cout << e << "\n";
+                }
+                return false;
             }
             std::cout << "p hint verified\n";
             break;
@@ -229,6 +268,7 @@ public:
             UNREACHABLE();
             break;
         }
+        return true;
     }
 
     /**