wip - proof checking, add support for distinct, other fixes

src/math/lp/lar_solver.h

@@ -295,70 +295,86 @@ class lar_solver : public column_namer {
 public:
     // this function just looks at the status
     bool is_feasible() const;
+
     const map<mpq, unsigned, obj_hash<mpq>, default_eq<mpq>>& fixed_var_table_int() const {
         return m_fixed_var_table_int;
     }
+
     map<mpq, unsigned, obj_hash<mpq>, default_eq<mpq>>& fixed_var_table_int() {
         return m_fixed_var_table_int;
     }
+
     const map<mpq, unsigned, obj_hash<mpq>, default_eq<mpq>>& fixed_var_table_real() const {
         return m_fixed_var_table_real;
     }
+
     map<mpq, unsigned, obj_hash<mpq>, default_eq<mpq>>& fixed_var_table_real() {
         return m_fixed_var_table_real;
     }
 
     bool find_in_fixed_tables(const rational& mpq, bool is_int, unsigned & j) const {
-        return is_int? fixed_var_table_int().find(mpq, j) :
+        return is_int? fixed_var_table_int().find(mpq, j) : fixed_var_table_real().find(mpq, j);
-            fixed_var_table_real().find(mpq, j);
     }
     
     template <typename T> void remove_non_fixed_from_table(T&);
+
     unsigned external_to_column_index(unsigned) const;
+
     bool inside_bounds(lpvar, const impq&) const;
+
     inline void set_column_value(unsigned j, const impq& v) {
         m_mpq_lar_core_solver.m_r_solver.update_x(j, v);
     }
+
     inline void set_column_value_test(unsigned j, const impq& v) {
         set_column_value(j, v);
     }
+
     unsigned get_total_iterations() const;
+
     var_index add_named_var(unsigned ext_j, bool is_integer, const std::string&);
+
     lp_status maximize_term(unsigned j_or_term, impq &term_max);
-    inline 
+
-    core_solver_pretty_printer<lp::mpq, lp::impq> pp(std::ostream& out) const { return
+    inline core_solver_pretty_printer<lp::mpq, lp::impq> pp(std::ostream& out) const { 
-            core_solver_pretty_printer<lp::mpq, lp::impq>(m_mpq_lar_core_solver.m_r_solver, out); }
+        return core_solver_pretty_printer<lp::mpq, lp::impq>(m_mpq_lar_core_solver.m_r_solver, out); 
+    }
+
     void get_infeasibility_explanation(explanation &) const;
+
     inline void backup_x() { m_backup_x = m_mpq_lar_core_solver.m_r_x; }
+
     inline void restore_x() { m_mpq_lar_core_solver.m_r_x = m_backup_x; }
+
     template <typename T>
     void explain_implied_bound(const implied_bound & ib, lp_bound_propagator<T> & bp) {
         unsigned i = ib.m_row_or_term_index;
-        int bound_sign = ib.m_is_lower_bound? 1: -1;
+        int bound_sign = (ib.m_is_lower_bound ? 1 : -1);
-        int j_sign = (ib.m_coeff_before_j_is_pos ? 1 :-1) * bound_sign;
+        int j_sign = (ib.m_coeff_before_j_is_pos ? 1 : -1) * bound_sign;
         unsigned bound_j = ib.m_j;
-        if (tv::is_term(bound_j)) {
+        if (tv::is_term(bound_j)) 
             bound_j = m_var_register.external_to_local(bound_j);
-        }
+
-        for (auto const& r : A_r().m_rows[i]) {
+        for (auto const& r : get_row(i)) {
             unsigned j = r.var();
-            if (j == bound_j) continue;
+            if (j == bound_j) 
+                continue;
             mpq const& a = r.coeff();
-            int a_sign = is_pos(a)? 1: -1;
+            int a_sign = is_pos(a) ? 1 : -1;
             int sign = j_sign * a_sign;
             const ul_pair & ul =  m_columns_to_ul_pairs[j];
-            auto witness = sign > 0? ul.upper_bound_witness(): ul.lower_bound_witness();
+            auto witness = sign > 0 ? ul.upper_bound_witness() : ul.lower_bound_witness();
             lp_assert(is_valid(witness));
             bp.consume(a, witness);
         }
     }
 
     void set_value_for_nbasic_column(unsigned j, const impq& new_val);
+
     inline unsigned get_base_column_in_row(unsigned row_index) const {
         return m_mpq_lar_core_solver.m_r_solver.get_base_column_in_row(row_index);
     }
 
-
     // lp_assert(implied_bound_is_correctly_explained(ib, explanation)); }
     constraint_index mk_var_bound(var_index j, lconstraint_kind kind, const mpq & right_side);
     void activate_check_on_equal(constraint_index, var_index&);

src/sat/smt/CMakeLists.txt

@@ -41,7 +41,7 @@ z3_add_component(sat_smt
     q_solver.cpp
     recfun_solver.cpp
     sat_th.cpp
-    tseitin_proof_checker.cpp
+    tseitin_theory_checker.cpp
     user_solver.cpp
   COMPONENT_DEPENDENCIES
     sat

src/sat/smt/arith_theory_checker.h

@@ -241,7 +241,7 @@ namespace arith {
                 return true;
             if (check_ineq(m_ineq))
                 return true;
-            
+            IF_VERBOSE(3, display_row(verbose_stream() << "Failed to verify Farkas with reduced row ", m_ineq) << "\n");
             // convert to expression, maybe follows from a cut.
             return false;
         }
@@ -452,7 +452,9 @@ namespace arith {
                             add_ineq(coeff, arg, sign);
                     }
                     else if (m.is_eq(arg, x, y)) {
-                        if (sign) 
+                        if (is_bound && j + 1 == jst->get_num_args())
+                            add_conseq(coeff, arg, sign);
+                        else if (sign) 
                             return check(); // it should be an implied equality
                         else
                             add_eq(x, y);

src/sat/smt/distinct_theory_checker.h

@@ -0,0 +1,50 @@
+/*++
+Copyright (c) 2022 Microsoft Corporation
+
+Module Name:
+
+    distinct_proof_checker.h
+
+Abstract:
+
+    Plugin for checking distinct internalization
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2022-10-07
+
+Note:
+ 
+  First version just trusts that distinct is internalized correctly.
+
+
+--*/
+#pragma once
+
+#include "sat/smt/euf_proof_checker.h"
+#include <iostream>
+
+namespace distinct {
+
+    class theory_checker : public euf::theory_checker_plugin {
+        ast_manager& m;
+    public:
+        theory_checker(ast_manager& m): 
+            m(m) {
+        }
+
+        expr_ref_vector clause(app* jst) override { 
+            expr_ref_vector result(m); 
+            result.append(jst->get_num_args(), jst->get_args()); 
+            return result; 
+        }
+        
+        bool check(app* jst) override { return true; }
+
+        void register_plugins(euf::theory_checker& pc) override {
+            pc.register_plugin(symbol("distinct"), this);
+        }
+        
+    };
+
+}

src/sat/smt/euf_internalize.cpp

@@ -216,10 +216,9 @@ namespace euf {
     void solver::add_not_distinct_axiom(app* e, enode* const* args) {
         SASSERT(m.is_distinct(e));
         unsigned sz = e->get_num_args();
-        sat::status st = sat::status::th(m_is_redundant, m.get_basic_family_id());
 
         if (sz <= 1) {
-            s().mk_clause(0, nullptr, st);
+            s().mk_clause(0, nullptr, mk_distinct_status(0, nullptr));
             return;
         }
 
@@ -234,7 +233,7 @@ namespace euf {
                 }
             }
             add_root(lits);
-            s().mk_clause(lits, st);
+            s().mk_clause(lits, mk_distinct_status(lits));
         }
         else {
             // g(f(x_i)) = x_i
@@ -252,13 +251,13 @@ namespace euf {
                 expr_ref gapp(m.mk_app(g, fapp.get()), m);
                 expr_ref eq = mk_eq(gapp, arg);
                 sat::literal lit = mk_literal(eq);
-                s().add_clause(lit, st);
+                s().add_clause(lit, mk_distinct_status(lit));
                 eqs.push_back(mk_eq(fapp, a));
             }
             pb_util pb(m);
             expr_ref at_least2(pb.mk_at_least_k(eqs.size(), eqs.data(), 2), m);
             sat::literal lit = si.internalize(at_least2, m_is_redundant);
-            s().add_clause(lit, st);
+            s().add_clause(lit, mk_distinct_status(lit));
         }
     }
 
@@ -266,19 +265,19 @@ namespace euf {
         SASSERT(m.is_distinct(e));
         static const unsigned distinct_max_args = 32;
         unsigned sz = e->get_num_args();
-        sat::status st = sat::status::th(m_is_redundant, m.get_basic_family_id());
+        
         if (sz <= 1) 
             return;       
         sort* srt = e->get_arg(0)->get_sort();
         auto sort_sz = srt->get_num_elements();
         if (sort_sz.is_finite() && sort_sz.size() < sz)
-            s().add_clause(0, nullptr, st);
+            s().add_clause(0, nullptr, mk_tseitin_status(0, nullptr));
         else if (sz <= distinct_max_args) {
             for (unsigned i = 0; i < sz; ++i) {
                 for (unsigned j = i + 1; j < sz; ++j) {
                     expr_ref eq = mk_eq(args[i]->get_expr(), args[j]->get_expr());
                     sat::literal lit = ~mk_literal(eq);
-                    s().add_clause(lit, st);
+                    s().add_clause(lit, mk_distinct_status(lit));
                 }
             }
         }
@@ -294,20 +293,19 @@ namespace euf {
                 n->mark_interpreted();
                 expr_ref eq = mk_eq(fapp, fresh);
                 sat::literal lit = mk_literal(eq);
-                s().add_clause(lit, st);
+                s().add_clause(lit, mk_distinct_status(lit));
             }
         }
     }
 
     void solver::axiomatize_basic(enode* n) {
         expr* e = n->get_expr();
-        sat::status st = sat::status::th(m_is_redundant, m.get_basic_family_id());
         expr* c = nullptr, * th = nullptr, * el = nullptr;
         if (!m.is_bool(e) && m.is_ite(e, c, th, el)) {
             expr_ref eq_th = mk_eq(e, th);
             sat::literal lit_th = mk_literal(eq_th);
             if (th == el) {
-                s().add_clause(lit_th, st);
+                s().add_clause(lit_th, mk_tseitin_status(lit_th));
             }
             else {
                 sat::literal lit_c = mk_literal(c);

src/sat/smt/euf_proof.cpp

@@ -238,6 +238,11 @@ namespace euf {
         return sat::status::th(m_is_redundant, m.get_basic_family_id(), ph);        
     }
 
+    sat::status solver::mk_distinct_status(unsigned n, sat::literal const* lits) {
+        th_proof_hint* ph = use_drat() ? mk_smt_hint(symbol("distinct"), n, lits) : nullptr;
+        return sat::status::th(m_is_redundant, m.get_basic_family_id(), ph);
+    }
+    
     expr* smt_proof_hint::get_hint(euf::solver& s) const {
         ast_manager& m = s.get_manager();
         sort* proof = m.mk_proof_sort();

src/sat/smt/euf_proof_checker.cpp

@@ -25,7 +25,8 @@ Author:
 #include "sat/smt/euf_proof_checker.h"
 #include "sat/smt/arith_theory_checker.h"
 #include "sat/smt/q_theory_checker.h"
-#include "sat/smt/tseitin_proof_checker.h"
+#include "sat/smt/distinct_theory_checker.h"
+#include "sat/smt/tseitin_theory_checker.h"
 
 
 namespace euf {
@@ -287,6 +288,7 @@ namespace euf {
         add_plugin(alloc(eq_theory_checker, m));
         add_plugin(alloc(res_checker, m, *this));
         add_plugin(alloc(q::theory_checker, m));
+        add_plugin(alloc(distinct::theory_checker, m));
         add_plugin(alloc(smt_theory_checker_plugin, m, symbol("datatype"))); // no-op datatype proof checker
         add_plugin(alloc(tseitin::theory_checker, m));
     }
@@ -437,7 +439,7 @@ namespace euf {
         if (m_checker.check(clause, proof_hint, units)) {
             bool units_are_rup = true;
             for (expr* u : units) {
-                if (!check_rup(u)) {
+                if (!m.is_true(u) && !check_rup(u)) {
                     std::cout << "unit " << mk_bounded_pp(u, m) << " is not rup\n";
                     units_are_rup = false;
                 }

src/sat/smt/euf_solver.h

@@ -407,8 +407,13 @@ namespace euf {
         smt_proof_hint* mk_smt_clause(symbol const& n, unsigned nl, literal const* lits);
         th_proof_hint* mk_cc_proof_hint(sat::literal_vector const& ante, app* a, app* b);
         th_proof_hint* mk_tc_proof_hint(sat::literal const* ternary_clause);
+        sat::status mk_tseitin_status(sat::literal a) { return mk_tseitin_status(1, &a); }
         sat::status mk_tseitin_status(sat::literal a, sat::literal b);
         sat::status mk_tseitin_status(unsigned n, sat::literal const* lits);
+        sat::status mk_distinct_status(sat::literal a) { return mk_distinct_status(1, &a); }
+        sat::status mk_distinct_status(sat::literal a, sat::literal b) { sat::literal lits[2] = { a, b }; return mk_distinct_status(2, lits); }
+        sat::status mk_distinct_status(sat::literal_vector const& lits) { return mk_distinct_status(lits.size(), lits.data()); }
+        sat::status mk_distinct_status(unsigned n, sat::literal const* lits);
 
         scoped_ptr<std::ostream> m_proof_out;
 

src/sat/smt/tseitin_theory_checker.cpp

@@ -3,7 +3,7 @@ Copyright (c) 2022 Microsoft Corporation
 
 Module Name:
 
-    tseitin_proof_checker.cpp
+    tseitin_theory_checker.cpp
 
 Abstract:
 
@@ -27,7 +27,7 @@ TODOs:
 --*/
 
 #include "ast/ast_pp.h"
-#include "sat/smt/tseitin_proof_checker.h"
+#include "sat/smt/tseitin_theory_checker.h"
 
 namespace tseitin {
 
@@ -41,20 +41,28 @@ namespace tseitin {
     bool theory_checker::check(app* jst) {
         expr* main_expr = nullptr;
         unsigned max_depth = 0;
+        expr* a, * x, * y, * z, * u, * v;
+
         for (expr* arg : *jst) {
             unsigned arg_depth = get_depth(arg);
             if (arg_depth > max_depth) {
                 main_expr = arg;
                 max_depth = arg_depth;
             }
-            if (arg_depth == max_depth && m.is_not(main_expr)) 
+            if (arg_depth == max_depth && m.is_not(main_expr)) {
+                if (m.is_not(arg, x) && m.is_not(main_expr, y) && 
+                    is_app(x) && is_app(y) && 
+                    to_app(x)->get_num_args() < to_app(y)->get_num_args())
+                    continue;
+
                 main_expr = arg;
+            }
         }
 
         if (!main_expr)
             return false;
 
-        expr* a, * x, * y, *z, *u, *v;
+
 
         // (or (and a b) (not a) (not b))
         // (or (and (not a) b) a (not b))

src/sat/smt/tseitin_theory_checker.h

@@ -3,11 +3,11 @@ Copyright (c) 2022 Microsoft Corporation
 
 Module Name:
 
-    tseitin_proof_checker.h
+    tseitin_theory_checker.h
 
 Abstract:
 
-    Plugin for checking quantifier instantiations
+    Plugin for checking tseitin internalization
 
 Author: