From 458f417f44c1ef53f352899bb317e6367982fd7d Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 25 Aug 2022 19:19:13 -0700
Subject: [PATCH] move drat functionality into euf

---
 src/sat/sat_drat.cpp      | 25 -------------------------
 src/sat/sat_drat.h        |  7 +------
 src/sat/smt/euf_proof.cpp | 16 ++++++++++++----
 src/sat/smt/pb_solver.cpp |  7 +++----
 4 files changed, 16 insertions(+), 39 deletions(-)

diff --git a/src/sat/sat_drat.cpp b/src/sat/sat_drat.cpp
index 0633612ad9c..8e63b4a1936 100644
--- a/src/sat/sat_drat.cpp
+++ b/src/sat/sat_drat.cpp
@@ -255,31 +255,6 @@ namespace sat {
         }
     }
 
-    void drat::bool_def(bool_var v, unsigned n) {
-        if (m_out)
-            (*m_out) << "b " << v << " " << n << " 0\n";
-    }
-
-    void drat::def_begin(char id, unsigned n, std::string const& name) {
-        if (m_out) 
-            (*m_out) << id << " " << n << " " << name;
-    }
-
-    void drat::def_add_arg(unsigned arg) {
-        if (m_out)
-            (*m_out) << " " << arg;
-    }
-
-    void drat::def_end() {
-        if (m_out)
-            (*m_out) << " 0\n";
-    }
-
-    void drat::log_adhoc(std::function<void(std::ostream&)>& fn) {
-        if (m_out)
-            fn(*m_out);
-    }
-
     void drat::append(clause& c, status st) {
         TRACE("sat_drat", pp(tout, st) << " " << c << "\n";);
         for (literal lit : c) declare(lit);
diff --git a/src/sat/sat_drat.h b/src/sat/sat_drat.h
index 83a29c9eda7..1ba86d72499 100644
--- a/src/sat/sat_drat.h
+++ b/src/sat/sat_drat.h
@@ -153,13 +153,8 @@ namespace sat {
         // associate AST node id with Boolean variable v
 
         // declare AST node n with 'name' and arguments arg
-        void def_begin(char id, unsigned n, std::string const& name);
-        void def_add_arg(unsigned arg);
-        void def_end();
-        void bool_def(bool_var v, unsigned n);
+        std::ostream* out() { return m_out; }
 
-        // ad-hoc logging until a format is developed
-        void log_adhoc(std::function<void(std::ostream&)>& fn);
 
         bool is_cleaned(clause& c) const;        
         void del(literal l);
diff --git a/src/sat/smt/euf_proof.cpp b/src/sat/smt/euf_proof.cpp
index f18e112b802..567f6fc1ce4 100644
--- a/src/sat/smt/euf_proof.cpp
+++ b/src/sat/smt/euf_proof.cpp
@@ -30,19 +30,27 @@ namespace euf {
     }
 
     void solver::def_add_arg(unsigned arg) {
-        get_drat().def_add_arg(arg);
+        auto* out = get_drat().out();
+        if (out)
+            (*out) << " " << arg;
     }
 
     void solver::def_end() {
-        get_drat().def_end();
+        auto* out = get_drat().out();
+        if (out)
+            (*out) << " 0\n";
     }
 
     void solver::def_begin(char id, unsigned n, std::string const& name) {
-        get_drat().def_begin(id, n, name);
+        auto* out = get_drat().out();
+        if (out)
+            (*out) << id << " " << n << " " << name;
     }
 
     void solver::bool_def(bool_var v, unsigned n) {
-        get_drat().bool_def(v, n);
+        auto* out = get_drat().out();
+        if (out)
+            (*out) << "b " << v << " " << n << " 0\n";
     }
 
 
diff --git a/src/sat/smt/pb_solver.cpp b/src/sat/smt/pb_solver.cpp
index 13d3e02e41c..1c762cb3f6b 100644
--- a/src/sat/smt/pb_solver.cpp
+++ b/src/sat/smt/pb_solver.cpp
@@ -1430,10 +1430,9 @@ namespace pb {
             IF_VERBOSE(0, verbose_stream() << *c << "\n");
         VERIFY(c->well_formed());
         if (m_solver && m_solver->get_config().m_drat) {
-            std::function<void(std::ostream& out)> fn = [&](std::ostream& out) {
-                out << "c ba constraint " << *c << " 0\n";
-            };
-            m_solver->get_drat().log_adhoc(fn);
+            auto * out = s().get_drat().out();
+            if (out)
+                *out << "c ba constraint " << *c << " 0\n";
         }
     }