fixes to proof logging and checking

src/cmd_context/extra_cmds/proof_cmds.cpp

@@ -182,9 +182,9 @@ public:
         }
         m_solver->pop(1);
         std::cout << "(verified-smt"; 
-        if (proof_hint) std::cout << " " << mk_bounded_pp(proof_hint, m, 4);
+        if (proof_hint) std::cout << "\n" << mk_bounded_pp(proof_hint, m, 4);
         for (expr* arg : clause)
-            std::cout << " " << mk_bounded_pp(arg, m);
+            std::cout << "\n " << mk_bounded_pp(arg, m);
         std::cout << ")\n";
         add_clause(clause);
     }

src/sat/smt/arith_proof_checker.h

@@ -143,17 +143,13 @@ namespace arith {
             SASSERT(m_todo.empty());
             m_todo.push_back({ mul, e });
             rational coeff1;
-            expr* e1, *e2, *e3;
+            expr* e1, *e2;
             for (unsigned i = 0; i < m_todo.size(); ++i) {
                 auto [coeff, e] = m_todo[i];
-                if (a.is_mul(e, e1, e2) && a.is_numeral(e1, coeff1))
+                if (a.is_mul(e, e1, e2) && is_numeral(e1, coeff1))
                     m_todo.push_back({coeff*coeff1, e2});
-                else if (a.is_mul(e, e1, e2) && a.is_uminus(e1, e3) && a.is_numeral(e3, coeff1))
+                else if (a.is_mul(e, e1, e2) && is_numeral(e2, coeff1))
-                    m_todo.push_back({-coeff*coeff1, e2});
+                    m_todo.push_back({ coeff * coeff1, e1 });
-                else if (a.is_mul(e, e1, e2) && a.is_uminus(e2, e3) && a.is_numeral(e3, coeff1))
-                    m_todo.push_back({ -coeff * coeff1, e1 });
-                else if (a.is_mul(e, e1, e2) && a.is_numeral(e2, coeff1))
-                    m_todo.push_back({coeff*coeff1, e1});
                 else if (a.is_add(e))
                     for (expr* arg : *to_app(e))
                         m_todo.push_back({coeff, arg});
@@ -163,15 +159,21 @@ namespace arith {
                     m_todo.push_back({coeff, e1});
                     m_todo.push_back({-coeff, e2});                
                 }
-                else if (a.is_numeral(e, coeff1)) 
+                else if (is_numeral(e, coeff1)) 
                     r.m_coeff += coeff*coeff1;
-                else if (a.is_uminus(e, e1) && a.is_numeral(e1, coeff1))
-                    r.m_coeff -= coeff*coeff1;
                 else
                     add(r, e, coeff);
             }
             m_todo.reset();
         }
+
+        bool is_numeral(expr* e, rational& n) {
+            if (a.is_numeral(e, n))
+                return true;
+            if (a.is_uminus(e, e) && a.is_numeral(e, n))
+                return n.neg(), true;
+            return false;
+        }
         
         bool check_ineq(row& r) {
             if (r.m_coeffs.empty() && r.m_coeff > 0)
@@ -182,9 +184,12 @@ namespace arith {
         }
         
         // triangulate equalities, substitute results into m_ineq, m_conseq.
-        void reduce_eq() {
+        // check consistency of equalities (they may be inconsisent)
+        bool reduce_eq() {
             for (unsigned i = 0; i < m_eqs.size(); ++i) {
                 auto& r = m_eqs[i];
+                if (r.m_coeffs.empty() && r.m_coeff != 0)
+                    return false;
                 if (r.m_coeffs.empty())
                     continue;
                 auto [v, coeff] = *r.m_coeffs.begin();
@@ -193,6 +198,7 @@ namespace arith {
                 resolve(v, m_ineq, coeff, r);
                 resolve(v, m_conseq, coeff, r);
             }
+            return true;
         }
         
         
@@ -231,7 +237,8 @@ namespace arith {
         bool check_farkas() {
             if (check_ineq(m_ineq))
                 return true;
-            reduce_eq();
+            if (!reduce_eq())
+                return true;
             if (check_ineq(m_ineq))
                 return true;
             
@@ -244,7 +251,8 @@ namespace arith {
         // after all inequalities in ineq have been added up
         //
         bool check_bound() {
-            reduce_eq();
+            if (!reduce_eq())
+                return true;
             if (check_ineq(m_conseq))
                 return true;
             if (m_ineq.m_coeffs.empty() ||
@@ -401,8 +409,10 @@ namespace arith {
                             return false;
                         }
                         num_le = coeff.get_unsigned();
-                        if (!add_implied_ineq(false, jst))
+                        if (!add_implied_ineq(false, jst)) {
+                            IF_VERBOSE(0, display(verbose_stream() << "did not add implied eq"));
                             return false;
+                        }
                         ++j;
                         continue;
                     }
@@ -418,10 +428,24 @@ namespace arith {
                             if (num_le == 0) {
                                 // we processed all the first inequalities,
                                 // check that they imply one half of the implied equality.
-                                if (!check())
+                                if (!check()) {
-                                    return false;
+                                    // we might have added the wrong direction of the implied equality.
-                                reset();
+                                    // so try the opposite inequality.
-                                VERIFY(add_implied_ineq(true, jst));
+                                    add_implied_ineq(true, jst);
+                                    add_implied_ineq(true, jst);
+                                    if (check()) {
+                                        reset();
+                                        add_implied_ineq(false, jst);
+                                    }
+                                    else {
+                                        IF_VERBOSE(0, display(verbose_stream() << "failed to check implied eq "));
+                                        return false;
+                                    }
+                                }
+                                else {
+                                    reset();
+                                    VERIFY(add_implied_ineq(true, jst));
+                                }
                             }
                         }
                         else

src/sat/smt/euf_proof.cpp

@@ -46,7 +46,7 @@ namespace euf {
      * so it isn't necessarily an axiom over EUF,
      * We will here leave it to the EUF checker to perform resolution steps.
      */
-    void solver::log_antecedents(literal l, literal_vector const& r, eq_proof_hint* hint) {
+    void solver::log_antecedents(literal l, literal_vector const& r, th_proof_hint* hint) {
         TRACE("euf", log_antecedents(tout, l, r););
         if (!use_drat())
             return;

src/sat/smt/euf_proof_checker.cpp

@@ -19,6 +19,7 @@ Author:
 #include "ast/ast_pp.h"
 #include "ast/ast_util.h"
 #include "ast/ast_ll_pp.h"
+#include "ast/arith_decl_plugin.h"
 #include "sat/smt/euf_proof_checker.h"
 #include "sat/smt/arith_proof_checker.h"
 #include "sat/smt/q_proof_checker.h"
@@ -58,15 +59,29 @@ namespace euf {
 
     class eq_proof_checker : public proof_checker_plugin {
         ast_manager&     m;
+        arith_util       m_arith;
+        expr_ref_vector  m_trail;
         basic_union_find m_uf;
         svector<std::pair<unsigned, unsigned>> m_expr2id;
         ptr_vector<expr>                       m_id2expr;
-        svector<std::pair<expr*,expr*>> m_diseqs;
+        svector<std::pair<expr*,expr*>>        m_diseqs;
         unsigned         m_ts = 0;
         
         void merge(expr* x, expr* y) {
             m_uf.merge(expr2id(x), expr2id(y));
             IF_VERBOSE(10, verbose_stream() << "merge " << mk_bounded_pp(x, m) << " == " << mk_bounded_pp(y, m) << "\n");
+            merge_numeral(x);
+            merge_numeral(y);
+        }
+
+        void merge_numeral(expr* x) {
+            rational n;
+            expr* y;
+            if (m_arith.is_uminus(x, y) && m_arith.is_numeral(y, n)) {
+                y = m_arith.mk_numeral(-n, x->get_sort());
+                m_trail.push_back(y);
+                m_uf.merge(expr2id(x), expr2id(y));
+            }
         }
 
         bool are_equal(expr* x, expr* y) {
@@ -118,7 +133,7 @@ namespace euf {
         }                
 
     public:
-        eq_proof_checker(ast_manager& m): m(m) {}
+        eq_proof_checker(ast_manager& m): m(m), m_arith(m), m_trail(m) {}
 
         expr_ref_vector clause(app* jst) override {
             expr_ref_vector result(m);

src/sat/smt/euf_solver.cpp

@@ -200,16 +200,36 @@ namespace euf {
         s().assign(lit, sat::justification::mk_ext_justification(s().scope_lvl(), idx));
     }
 
+    /**
+    Retrieve set of literals r that imply r.
+    Since the set of literals are retrieved modulo multiple theories in a single implication
+    we lose theory specific justifications. For proof logging we use a catch all rule "smt"
+    for the case where an equality is derived using more than congruence closure.
+    To create fully decomposed justifications it will be necessary to augment the justification
+    data-structure with information about the equality that is implied by the theory.
+    Then each justification will imply an equality s = t assuming literals 'r'.
+    The theory lemma is then r -> s = t, where s = t is an equality that is available for the EUF hint.
+    The EUF hint is resolved against r -> s = t to eliminate s = t and to create the resulting explanation.
+
+    Example:
+            x - 3 = 0 => x = 3 by arithmetic
+            x = 3 => f(x) = f(3) by EUF
+            resolve to produce clause x - 3 = 0 => f(x) = f(3)
+    */
+
     void solver::get_antecedents(literal l, ext_justification_idx idx, literal_vector& r, bool probing) {
         m_egraph.begin_explain();
         m_explain.reset();
         if (use_drat() && !probing) 
             push(restore_size_trail(m_explain_cc, m_explain_cc.size()));
         auto* ext = sat::constraint_base::to_extension(idx);
+        bool has_theory = false;
         if (ext == this)
             get_antecedents(l, constraint::from_idx(idx), r, probing);
-        else
+        else {
             ext->get_antecedents(l, idx, r, probing);
+            has_theory = true;
+        }
         for (unsigned qhead = 0; qhead < m_explain.size(); ++qhead) {
             size_t* e = m_explain[qhead];
             if (is_literal(e)) 
@@ -220,10 +240,20 @@ namespace euf {
                 SASSERT(ext != this);
                 sat::literal lit = sat::null_literal;
                 ext->get_antecedents(lit, idx, r, probing);
+                has_theory = true;
             }
         }
         m_egraph.end_explain();  
-        eq_proof_hint* hint = (use_drat() && !probing) ? mk_hint(l, r) : nullptr;
+        th_proof_hint* hint = nullptr;
+        if (use_drat() && !probing) {
+            if (has_theory) {                
+                r.push_back(~l);
+                hint = mk_smt_hint(symbol("smt"), r);
+                r.pop_back();
+            }
+            else
+                hint = mk_hint(l, r);
+        }
         unsigned j = 0;
         for (sat::literal lit : r) 
             if (s().lvl(lit) > 0) r[j++] = lit;

src/sat/smt/euf_solver.h

@@ -193,7 +193,7 @@ namespace euf {
 
         // proofs
         void log_antecedents(std::ostream& out, literal l, literal_vector const& r);
-        void log_antecedents(literal l, literal_vector const& r, eq_proof_hint* hint);
+        void log_antecedents(literal l, literal_vector const& r, th_proof_hint* hint);
         void log_justification(literal l, th_explain const& jst);
 
         typedef std::pair<expr*, expr*> expr_pair;

src/sat/tactic/goal2sat.cpp

@@ -284,11 +284,15 @@ struct goal2sat::imp : public sat::sat_internalizer {
         if (v == sat::null_bool_var) {
             if (m.is_true(t)) {
                 sat::literal tt = sat::literal(mk_bool_var(t), false);
+                if (m_euf && ensure_euf()->use_drat())
+                    ensure_euf()->set_bool_var2expr(tt.var(), t);
                 mk_root_clause(tt);
                 l = sign ? ~tt : tt;
             }
             else if (m.is_false(t)) {
                 sat::literal ff = sat::literal(mk_bool_var(t), false);
+                if (m_euf && ensure_euf()->use_drat())
+                    ensure_euf()->set_bool_var2expr(ff.var(), t);
                 mk_root_clause(~ff);
                 l = sign ? ~ff : ff;
             }