From 1ddef117a21de30909fd1166095caaa85c39da82 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 8 Jan 2023 16:11:31 -0800
Subject: [PATCH] several fixes to proof logging in legacy solver

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/smt/smt_clause_proof.cpp  | 29 +++++++++++++++++++++++------
 src/smt/smt_clause_proof.h    |  3 +++
 src/smt/smt_model_checker.cpp |  4 +++-
 3 files changed, 29 insertions(+), 7 deletions(-)

diff --git a/src/smt/smt_clause_proof.cpp b/src/smt/smt_clause_proof.cpp
index 096a0994f..d533ae161 100644
--- a/src/smt/smt_clause_proof.cpp
+++ b/src/smt/smt_clause_proof.cpp
@@ -16,15 +16,27 @@ Revision History:
 #include "smt/smt_context.h"
 #include "ast/ast_pp.h"
 #include "ast/ast_ll_pp.h"
+#include <iostream>
 
 namespace smt {
     
     clause_proof::clause_proof(context& ctx):
         ctx(ctx), m(ctx.get_manager()), m_lits(m), m_pp(m) {
+        
         auto proof_log = ctx.get_fparams().m_proof_log;
-        m_enabled = ctx.get_fparams().m_clause_proof || proof_log.is_non_empty_string();
-        if (proof_log.is_non_empty_string()) {
-            m_pp_out = alloc(std::ofstream, proof_log.str());
+        m_has_log = proof_log.is_non_empty_string();
+        m_enabled = ctx.get_fparams().m_clause_proof || m_has_log;        
+    }
+
+    void clause_proof::init_pp_out() {
+        if (m_has_log && !m_pp_out) {
+            static unsigned id = 0;
+            auto proof_log = ctx.get_fparams().m_proof_log;
+            std::string log_name = proof_log.str();
+            if (id > 0)
+                log_name = std::to_string(id) + log_name;
+            ++id;
+            m_pp_out = alloc(std::ofstream, log_name);
             if (!*m_pp_out)
                 throw default_exception(std::string("Could not open file ") + proof_log.str());
         }
@@ -170,14 +182,18 @@ namespace smt {
             m_trail.push_back(info(st, v, p));
         if (m_on_clause_eh) 
             m_on_clause_eh(m_on_clause_ctx, p, v.size(), v.data());        
-        if (m_pp_out) {
+        if (m_has_log) {
+            init_pp_out();
             auto& out = *m_pp_out;
             for (auto* e : v)
                 declare(out, e);
             switch (st) {
             case clause_proof::status::assumption:
-                display_literals(out << "(assume", v) << ")\n";
-                break;
+                if (!p || p->get_decl()->get_name() == "assumption") {
+                    display_literals(out << "(assume", v) << ")\n";
+                    break;
+                }
+                Z3_fallthrough;
             case clause_proof::status::lemma:
             case clause_proof::status::th_lemma:
             case clause_proof::status::th_assumption:
@@ -191,6 +207,7 @@ namespace smt {
             default:
                 UNREACHABLE();
             }
+            out.flush();
         }
     }
 
diff --git a/src/smt/smt_clause_proof.h b/src/smt/smt_clause_proof.h
index 42f283f1d..b247a0454 100644
--- a/src/smt/smt_clause_proof.h
+++ b/src/smt/smt_clause_proof.h
@@ -58,10 +58,13 @@ namespace smt {
         expr_ref_vector m_lits;
         vector<info>    m_trail;
         bool            m_enabled = false;
+        bool            m_has_log = false;
         user_propagator::on_clause_eh_t m_on_clause_eh;
         void*                           m_on_clause_ctx = nullptr;
         ast_pp_util                     m_pp;
         scoped_ptr<std::ofstream>       m_pp_out;
+
+        void init_pp_out();
         
         void update(status st, expr_ref_vector& v, proof* p);
         void update(clause& c, status st, proof* p);
diff --git a/src/smt/smt_model_checker.cpp b/src/smt/smt_model_checker.cpp
index 72094f78a..61173907b 100644
--- a/src/smt/smt_model_checker.cpp
+++ b/src/smt/smt_model_checker.cpp
@@ -405,13 +405,15 @@ namespace smt {
             m_fparams->m_relevancy_lvl = 0; // no relevancy since the model checking problems are quantifier free
             m_fparams->m_case_split_strategy = CS_ACTIVITY; // avoid warning messages about smt.case_split >= 3.
             m_fparams->m_axioms2files = false;
-            m_fparams->m_lemmas2console = false;            
+            m_fparams->m_lemmas2console = false;
+            m_fparams->m_proof_log = symbol::null;
         }
         if (!m_aux_context) {
             symbol logic;
             params_ref p;
             p.set_bool("solver.axioms2files", false);
             p.set_bool("solver.lemmas2console", false);
+            p.set_sym("solver.proof.log", symbol::null);
             m_aux_context = m_context->mk_fresh(&logic, m_fparams.get(), p);
         }
     }