From f0b85716a950aa52d4bd8411e9cbb309188d648a Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 18 Oct 2022 11:20:56 -0700
Subject: [PATCH] wip - proof logging fixes

---
 src/sat/smt/euf_internalize.cpp   |  3 +++
 src/sat/smt/euf_proof_checker.cpp | 24 +++++++++++++++++-------
 src/sat/smt/euf_proof_checker.h   |  4 ++--
 3 files changed, 22 insertions(+), 9 deletions(-)

diff --git a/src/sat/smt/euf_internalize.cpp b/src/sat/smt/euf_internalize.cpp
index a03af92c7..865f58fde 100644
--- a/src/sat/smt/euf_internalize.cpp
+++ b/src/sat/smt/euf_internalize.cpp
@@ -159,6 +159,9 @@ namespace euf {
             v = si.add_bool_var(e);
             s().set_external(v);
             s().set_eliminated(v, false);
+            m_bool_var2expr.reserve(v + 1, nullptr);
+            m_bool_var2expr[v] = e;
+            m_var_trail.push_back(v);
             sat::literal lit2 = literal(v, false);
             th_proof_hint* ph1 = nullptr, * ph2 = nullptr;
             if (use_drat()) {
diff --git a/src/sat/smt/euf_proof_checker.cpp b/src/sat/smt/euf_proof_checker.cpp
index 097bc7b61..9bb2cfbaa 100644
--- a/src/sat/smt/euf_proof_checker.cpp
+++ b/src/sat/smt/euf_proof_checker.cpp
@@ -391,15 +391,23 @@ namespace euf {
     }
 
 
-    void smt_proof_checker::log_verified(app* proof_hint) {
+    void smt_proof_checker::log_verified(app* proof_hint, bool success) {
+        if (!proof_hint)
+            return;
+
         symbol n = proof_hint->get_name();
-        m_hint2hit.insert_if_not_there(n, 0)++;
+        if (success)
+            m_hint2hit.insert_if_not_there(n, 0)++;
+        else
+            m_hint2miss.insert_if_not_there(n, 0)++;
         ++m_num_logs;
 
         if (m_num_logs < 100 || (m_num_logs % 1000) == 0) {
-            std::cout << "(verified";
+            std::cout << "(proofs";
             for (auto const& [k, v] : m_hint2hit)
-                std::cout << " :" << k << " " << v;
+                std::cout << " +" << k << " " << v;
+            for (auto const& [k, v] : m_hint2miss)
+                std::cout << " -" << k << " " << v;
             std::cout << ")\n";
         }
     }
@@ -424,7 +432,7 @@ namespace euf {
             
         if (is_rup(proof_hint) && check_rup(clause)) {
             if (m_check_rup) {
-                log_verified(proof_hint);
+                log_verified(proof_hint, true);
                 add_clause(clause);
             }
             return;
@@ -440,7 +448,7 @@ namespace euf {
                 }
             }
             if (units_are_rup) {
-                log_verified(proof_hint);
+                log_verified(proof_hint, true);
                 add_clause(clause);
                 return;
             }
@@ -454,11 +462,13 @@ namespace euf {
         // The VC function is a no-op if the proof hint does not have an associated vc generator.
         expr_ref_vector vc(clause);
         if (m_checker.vc(proof_hint, clause, vc)) {
-            log_verified(proof_hint);
+            log_verified(proof_hint, true);
             add_clause(clause);
             return;
         }
         
+        log_verified(proof_hint, false);
+
         ensure_solver();
         m_solver->push();
         for (expr* lit : vc)
diff --git a/src/sat/smt/euf_proof_checker.h b/src/sat/smt/euf_proof_checker.h
index 17a867104..9a84015e4 100644
--- a/src/sat/smt/euf_proof_checker.h
+++ b/src/sat/smt/euf_proof_checker.h
@@ -89,7 +89,7 @@ namespace euf {
 
         // for logging
 
-        map<symbol, unsigned, symbol_hash_proc, symbol_eq_proc> m_hint2hit;
+        map<symbol, unsigned, symbol_hash_proc, symbol_eq_proc> m_hint2hit, m_hint2miss;
         unsigned m_num_logs = 0;
         
         void add_units() {
@@ -98,7 +98,7 @@ namespace euf {
                 m_units.push_back(units[i].first);
         }
 
-        void log_verified(app* proof_hint);
+        void log_verified(app* proof_hint, bool success);
 
         void diagnose_rup_failure(expr_ref_vector const& clause);