add hint verification, combine bounds/farkas into one rule

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

scripts/nightly.yaml

@@ -104,25 +104,26 @@ stages:
         artifactName: '$(name)Build'
         targetPath: $(Build.ArtifactStagingDirectory)
 
-#  - job: MuslLinuxBuild
+  - job: MuslLinuxBuild
-#    variables:
+    condition: eq(0,1)
-#      python: "/opt/python/cp310-cp310/bin/python"
+    variables:
-#      name: MuslLinux
+      python: "/opt/python/cp310-cp310/bin/python"
-#    displayName: "MuslLinux build"
+      name: MuslLinux
-#    pool:
+    displayName: "MuslLinux build"
-#      vmImage: "Ubuntu-18.04"
+    pool:
-#    container: "quay.io/pypa/musllinux_1_1_x86_64:latest"
+      vmImage: "Ubuntu-18.04"
-#    steps:
+    container: "quay.io/pypa/musllinux_1_1_x86_64:latest"
-#    - script: $(python) scripts/mk_unix_dist.py --nodotnet --nojava
+    steps:
-#    - script: git clone https://github.com/z3prover/z3test z3test
+    - script: $(python) scripts/mk_unix_dist.py --nodotnet --nojava
-#    - script: $(python) z3test/scripts/test_benchmarks.py build-dist/z3 z3test/regressions/smt2
+    - script: git clone https://github.com/z3prover/z3test z3test
-#    - script: cp dist/*.zip $(Build.ArtifactStagingDirectory)/
+    - script: $(python) z3test/scripts/test_benchmarks.py build-dist/z3 z3test/regressions/smt2
-#    - task: PublishPipelineArtifact@0
+    - script: cp dist/*.zip $(Build.ArtifactStagingDirectory)/
-#      inputs:
+    - task: PublishPipelineArtifact@0
-#        artifactName: '$(name)Build'
+      inputs:
-#        targetPath: $(Build.ArtifactStagingDirectory)
+        artifactName: '$(name)Build'
+        targetPath: $(Build.ArtifactStagingDirectory)
 
-  - job: Windows32
+- job: Windows32
     displayName: "Windows 32-bit build"
     pool:
       vmImage: "windows-latest"

src/sat/dimacs.cpp

@@ -115,7 +115,6 @@ static void read_clause(Buffer & in, std::ostream& err, sat::literal_vector & li
 template<typename Buffer>
 static void read_pragma(Buffer & in, std::ostream& err, std::string& p, sat::proof_hint& h) {
     skip_whitespace(in);
-    h.reset();
     if (*in != 'p')
         return;
     ++in;
@@ -307,6 +306,7 @@ namespace dimacs {
         loop:
             skip_whitespace(in);
             m_record.m_pragma.clear();
+            m_record.m_hint.reset();
             switch (*in) {
             case EOF:
                 return false;                

src/sat/sat_drat.cpp

@@ -918,9 +918,6 @@ 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;
@@ -949,11 +946,6 @@ namespace sat {
                 s += 6;
                 return true;
             }
-            if (0 == strncmp(s, "bound", 5)) {
-                h.m_ty = hint_type::bound_h;
-                s += 5;
-                return true;
-            }
             return false;
         };
 

src/sat/sat_types.h

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

src/sat/smt/arith_diagnostics.cpp

@@ -81,13 +81,14 @@ namespace arith {
     }
 
     /**
-     * Assumption:
+     * It may be necessary to use the following assumption when checking Farkas claims
+     * generated from bounds propagation:
      * A bound literal ax <= b is explained by a set of weighted literals
      * r1*(a1*x <= b1) + .... + r_k*(a_k*x <= b_k), where r_i > 0
      * such that there is a r >= 1
      * (r1*a1+..+r_k*a_k) = r*a, (r1*b1+..+r_k*b_k) <= r*b
      */
-    sat::proof_hint const* solver::explain(sat::hint_type ty) {
+    sat::proof_hint const* solver::explain(sat::hint_type ty, sat::literal lit) {
         if (!ctx.use_drat())
             return nullptr;
         m_bounds_pragma.m_ty = ty;
@@ -105,6 +106,8 @@ namespace arith {
             }
             case equality_source: {
                 auto [u, v] = m_equalities[idx];
+                ctx.drat_log_expr(u->get_expr());
+                ctx.drat_log_expr(v->get_expr());
                 m_bounds_pragma.m_eqs.push_back({ev.coeff(), u->get_expr_id(), v->get_expr_id()});
                 break;
             }
@@ -112,6 +115,8 @@ namespace arith {
                 break;
             }
         }
+        if (lit != sat::null_literal)
+            m_bounds_pragma.m_literals.push_back({rational(1), ~lit});
         return &m_bounds_pragma;
     }
 }

src/sat/smt/arith_solver.cpp

@@ -263,7 +263,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::bound_h));
+            assign(lit, m_core, m_eqs, explain(sat::hint_type::farkas_h, lit));
         }
 
         if (should_refine_bounds() && first)
@@ -378,7 +378,7 @@ namespace arith {
         reset_evidence();
         m_explanation.clear();
         lp().explain_implied_bound(be, m_bp);
-        assign(bound, m_core, m_eqs, explain(sat::hint_type::bound_h));
+        assign(bound, m_core, m_eqs, explain(sat::hint_type::farkas_h, bound));
     }
 
 
@@ -1177,7 +1177,7 @@ namespace arith {
             app_ref b = mk_bound(m_lia->get_term(), m_lia->get_offset(), !m_lia->is_upper());
             IF_VERBOSE(4, verbose_stream() << "cut " << b << "\n");
             literal lit = expr2literal(b);
-            assign(lit, m_core, m_eqs, explain(sat::hint_type::cut_h));
+            assign(lit, m_core, m_eqs, explain(sat::hint_type::cut_h, lit));
             lia_check = l_false;
             break;
         }

src/sat/smt/arith_solver.h

@@ -421,7 +421,7 @@ namespace arith {
 
         sat::proof_hint m_bounds_pragma;
         sat::proof_hint m_farkas2;
-        sat::proof_hint const* explain(sat::hint_type ty);
+        sat::proof_hint const* explain(sat::hint_type ty, sat::literal lit = sat::null_literal);
 
 
     public:

src/sat/smt/euf_solver.h

@@ -176,7 +176,6 @@ namespace euf {
         void log_antecedents(literal l, literal_vector const& r);
         void log_justification(literal l, th_explain const& jst);
         void drat_log_decl(func_decl* f);
-        void drat_log_expr(expr* n);
         void drat_log_expr1(expr* n);
         ptr_vector<expr> m_drat_todo;
         obj_hashtable<ast> m_drat_asts;
@@ -345,6 +344,7 @@ namespace euf {
         sat::drat& get_drat() { return s().get_drat(); }
         void drat_bool_def(sat::bool_var v, expr* n);
         void drat_eq_def(sat::literal lit, expr* eq);
+        void drat_log_expr(expr* n);
 
         // decompile
         bool extract_pb(std::function<void(unsigned sz, literal const* c, unsigned k)>& card,

src/shell/drat_frontend.cpp

@@ -160,16 +160,15 @@ public:
         // m_drat.add(lits, st);
     }
 
-    void validate_hint(sat::literal_vector const& lits, sat::proof_hint const& hint) {
+    void validate_hint(expr_ref_vector const& exprs, sat::literal_vector const& lits, sat::proof_hint const& hint) {
-        return; // remove when testing this
+        // return; // remove when testing this
         proof_checker pc(m);
         arith_util autil(m);
         switch (hint.m_ty) {
         case sat::hint_type::null_h:
             break;
-        case sat::hint_type::bound_h: {
+        case sat::hint_type::cut_h:
-            // TODO: combine bound_h and farkas_h into a single rule
+        case sat::hint_type::farkas_h: {
-            // TODO: use proof_checker.cpp check_arith_proof to check farkas claim
             expr_ref sum(m);
             bool is_strict = false;
             vector<rational> coeffs;
@@ -178,6 +177,10 @@ public:
                 coeffs.push_back(coeff);
                 lc = lcm(lc, denominator(coeff)); 
             }
+            for (auto const& [coeff, a, b]: hint.m_eqs) {
+                coeffs.push_back(coeff);
+                lc = lcm(lc, denominator(coeff)); 
+            }
             if (!lc.is_one())
                 for (auto& coeff : coeffs)
                     coeff *= lc;
@@ -186,13 +189,25 @@ public:
             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 << "Failed checking hint " << e << "\n";
+                    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];
+                coeffs.push_back(coeff);
+                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;
+                }
+                ++i;
+            }
+
             if (!sum.get()) {
-                std::cout << "no summation\n";
+                std::cout << "p no summation\n";
                 return;
             }
 
@@ -204,16 +219,14 @@ public:
             th_rewriter rw(m);
             rw(sum);
             if (!m.is_false(sum)) {
-                std::cout << "Lemma not simplified " << sum << "\n";
+                std::cout << "p hint not verified " << sum << "\n";
                 return;
             }
+            std::cout << "p hint verified\n";
             break;
         }
-        case sat::hint_type::farkas_h:
+        default:
-            std::cout << "FARKAS\n";
+            UNREACHABLE();
-            break;
-        case sat::hint_type::cut_h:
-            std::cout << "CUT\n";
             break;
         }
     }
@@ -405,7 +418,7 @@ static void verify_smt(char const* drat_file, char const* smt_file) {
         switch (r.m_tag) {
         case dimacs::drat_record::tag_t::is_clause:
             checker.add(r.m_lits, r.m_status);
-            checker.validate_hint(r.m_lits, r.m_hint);
+            checker.validate_hint(exprs, r.m_lits, r.m_hint);
             if (drat_checker.inconsistent()) {
                 std::cout << "inconsistent\n";
                 return;