From 1894c86ee015eafbacb0730d44d625034271d6e4 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 25 Aug 2022 18:27:30 -0700
Subject: [PATCH 1/3] virtual

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/sat/sat_drat.cpp       | 14 ++++++++------
 src/sat/sat_drat.h         | 10 +++++++---
 src/sat/smt/euf_proof.cpp  | 35 ++++++++++++++++++++++++-----------
 src/sat/smt/euf_solver.cpp |  9 ++-------
 src/sat/smt/euf_solver.h   |  7 +++++--
 5 files changed, 46 insertions(+), 29 deletions(-)

diff --git a/src/sat/sat_drat.cpp b/src/sat/sat_drat.cpp
index 3b52b0f7f..0633612ad 100644
--- a/src/sat/sat_drat.cpp
+++ b/src/sat/sat_drat.cpp
@@ -35,7 +35,6 @@ namespace sat {
             if (s.get_config().m_drat_binary) 
                 std::swap(m_out, m_bout);            
         }
-        // m_print_clause = nullptr;
     }
 
     drat::~drat() {
@@ -684,6 +683,7 @@ namespace sat {
             verify(0, nullptr);
             SASSERT(m_inconsistent);
         }
+        if (m_print_clause) m_print_clause->on_clause(0, nullptr, status::redundant());
     }
     void drat::add(literal l, bool learned) {
         ++m_stats.m_num_add;
@@ -691,7 +691,7 @@ namespace sat {
         if (m_out) dump(1, &l, st);
         if (m_bout) bdump(1, &l, st);
         if (m_check) append(l, st);
-        //if (m_print_clause) m_print_clause(1, &l, st);
+        if (m_print_clause) m_print_clause->on_clause(1, &l, st);
     }
     void drat::add(literal l1, literal l2, status st) {
         if (st.is_deleted())
@@ -702,7 +702,7 @@ namespace sat {
         if (m_out) dump(2, ls, st);
         if (m_bout) bdump(2, ls, st);
         if (m_check) append(l1, l2, st);
-        //if (m_print_clause) m_print_clause(2, ls, st);
+        if (m_print_clause) m_print_clause->on_clause(2, ls, st);
     }
     void drat::add(clause& c, status st) {
         if (st.is_deleted())
@@ -712,7 +712,7 @@ namespace sat {
         if (m_out) dump(c.size(), c.begin(), st);
         if (m_bout) bdump(c.size(), c.begin(), st);
         if (m_check) append(mk_clause(c), st);
-        //if (m_print_clause) m_print_clause(c.size(), c.begin(), st);
+        if (m_print_clause) m_print_clause->on_clause(c.size(), c.begin(), st);
     }
     
     void drat::add(literal_vector const& lits, status st) {
@@ -734,7 +734,8 @@ namespace sat {
         if (m_out)
             dump(sz, lits, st);
 
-        //if (m_print_clause) m_print_clause(sz, lits, st);
+        if (m_print_clause)
+            m_print_clause->on_clause(sz, lits, st);
     }
 
     void drat::add(literal_vector const& c) {
@@ -754,7 +755,8 @@ namespace sat {
             }
             }
         }
-        // if (m_print_clause) m_print_clause(c.size(), c.data(), status::redundant());
+        if (m_print_clause)
+            m_print_clause->on_clause(c.size(), c.data(), status::redundant());
     }
 
     void drat::del(literal l) {
diff --git a/src/sat/sat_drat.h b/src/sat/sat_drat.h
index 046f0bbc9..e60e80487 100644
--- a/src/sat/sat_drat.h
+++ b/src/sat/sat_drat.h
@@ -60,6 +60,10 @@ namespace sat {
     class justification;
     class clause;
 
+    struct print_clause {
+        virtual void on_clause(unsigned, literal const*, status) = 0;
+    };
+
     class drat {
         struct stats {
             unsigned m_num_drup = 0;
@@ -73,7 +77,7 @@ namespace sat {
             watched_clause(clause* c, literal l1, literal l2):
                 m_clause(c), m_l1(l1), m_l2(l2) {}
         };
-        std::function<void(unsigned, literal const*, status)> m_print_clause;
+        print_clause* m_print_clause = nullptr;
         svector<watched_clause>   m_watched_clauses;
         typedef svector<unsigned> watch;
         solver& s;
@@ -140,8 +144,8 @@ namespace sat {
         void add(literal_vector const& c); // add learned clause
         void add(unsigned sz, literal const* lits, status st);
 
-        void set_print_clause(std::function<void(unsigned, literal const*, status)>& print_clause) {
-            // m_print_clause = print_clause;
+        void set_print_clause(print_clause& print_clause) {
+            m_print_clause = &print_clause;
         }
 
         // support for SMT - connect Boolean variables with AST nodes
diff --git a/src/sat/smt/euf_proof.cpp b/src/sat/smt/euf_proof.cpp
index 36ed50a0b..a63efb79b 100644
--- a/src/sat/smt/euf_proof.cpp
+++ b/src/sat/smt/euf_proof.cpp
@@ -29,6 +29,18 @@ namespace euf {
         m_drat_initialized = true;
     }
 
+    void solver::def_add_arg(unsigned arg) {
+        get_drat().def_add_arg(arg);
+    }
+
+    void solver::def_end() {
+        get_drat().def_end();
+    }
+
+    void solver::def_begin(char id, unsigned n, std::string const& name) {
+        get_drat().def_begin(id, n, name);
+    }
+
     void solver::drat_log_params(func_decl* f) {
         for (unsigned i = f->get_num_parameters(); i-- > 0; ) {
             auto const& p = f->get_parameter(i);
@@ -39,6 +51,7 @@ namespace euf {
                 drat_log_decl(to_func_decl(a));
         }
     }
+    
     void solver::drat_log_expr1(expr* e) {
         if (is_app(e)) {
             app* a = to_app(e);
@@ -48,14 +61,14 @@ namespace euf {
             strm << mk_ismt2_func(a->get_decl(), m);
             get_drat().def_begin('e', e->get_id(), strm.str());
             for (expr* arg : *a)
-                get_drat().def_add_arg(arg->get_id());
-            get_drat().def_end();
+                def_add_arg(arg->get_id());
+            def_end();
         }
         else if (is_var(e)) {
             var* v = to_var(e);
             get_drat().def_begin('v', v->get_id(), "" + mk_pp(e->get_sort(), m));
-            get_drat().def_add_arg(v->get_idx());
-            get_drat().def_end();
+            def_add_arg(v->get_idx());
+            def_end();
         }
         else if (is_quantifier(e)) {
             quantifier* q = to_quantifier(e);
@@ -65,8 +78,8 @@ namespace euf {
                 strm << " (" << q->get_decl_name(i) << " " << mk_pp(q->get_decl_sort(i), m) << ")";            
             strm << ")";
             get_drat().def_begin('q', q->get_id(), strm.str());
-            get_drat().def_add_arg(q->get_expr()->get_id());
-            get_drat().def_end();
+            def_add_arg(q->get_expr()->get_id());
+            def_end();
         }
         else 
             UNREACHABLE();
@@ -118,7 +131,7 @@ namespace euf {
         smt2_pp_environment_dbg env(m);
         ast_smt2_pp(strm, f, env);
         get_drat().def_begin('f', f->get_small_id(), strm.str());
-        get_drat().def_end();
+        def_end();
     }
 
     /**
@@ -188,13 +201,13 @@ namespace euf {
         drat_log_expr(a);
         drat_log_expr(b);
         get_drat().def_begin('e', eq->get_id(), std::string("="));
-        get_drat().def_add_arg(a->get_id());
-        get_drat().def_add_arg(b->get_id());
-        get_drat().def_end();
+        def_add_arg(a->get_id());
+        def_add_arg(b->get_id());
+        def_end();
         get_drat().bool_def(lit.var(), eq->get_id());
     }
 
-    void solver::log_clause(unsigned n, literal const* lits, sat::status st) {
+    void solver::on_clause(unsigned n, literal const* lits, sat::status st) {
         if (!get_config().m_lemmas2console) 
             return;
         if (!st.is_redundant() && !st.is_asserted()) 
diff --git a/src/sat/smt/euf_solver.cpp b/src/sat/smt/euf_solver.cpp
index 56480aa85..656249944 100644
--- a/src/sat/smt/euf_solver.cpp
+++ b/src/sat/smt/euf_solver.cpp
@@ -171,13 +171,8 @@ namespace euf {
         for (auto* s : m_solvers)
             s->init_search();
 
-        if (get_config().m_lemmas2console) {
-            std::function<void(unsigned, sat::literal const*, sat::status)> on_clause = 
-                [&](unsigned n, sat::literal const* lits, sat::status st) {
-                log_clause(n, lits, st);
-            };
-            get_drat().set_print_clause(on_clause);
-        }
+        if (get_config().m_lemmas2console) 
+            get_drat().set_print_clause(*this);
     }
 
     bool solver::is_external(bool_var v) {
diff --git a/src/sat/smt/euf_solver.h b/src/sat/smt/euf_solver.h
index e2cdd7862..f77954ded 100644
--- a/src/sat/smt/euf_solver.h
+++ b/src/sat/smt/euf_solver.h
@@ -60,7 +60,7 @@ namespace euf {
         std::ostream& display(std::ostream& out) const;
     };
 
-    class solver : public sat::extension, public th_internalizer, public th_decompile {
+    class solver : public sat::extension, public th_internalizer, public th_decompile, public sat::print_clause {
         typedef top_sort<euf::enode> deps_t;
         friend class ackerman;
         class user_sort;
@@ -183,7 +183,10 @@ namespace euf {
         bool m_drat_initialized{ false };
         void init_drat();
         ast_pp_util m_clause_visitor;
-        void log_clause(unsigned n, literal const* lits, sat::status st);
+        void on_clause(unsigned n, literal const* lits, sat::status st) override;
+        void def_add_arg(unsigned arg);
+        void def_end();
+        void def_begin(char id, unsigned n, std::string const& name);
 
 
         // relevancy

From 1ffbe23ee3e85dd8b4cba81a3481d8e3158f6115 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 25 Aug 2022 18:37:24 -0700
Subject: [PATCH 2/3] add virtual destructor to fix build

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/sat/sat_drat.h        |  5 +++--
 src/sat/smt/euf_proof.cpp | 19 ++++++++++++-------
 src/sat/smt/euf_solver.h  |  1 +
 3 files changed, 16 insertions(+), 9 deletions(-)

diff --git a/src/sat/sat_drat.h b/src/sat/sat_drat.h
index e60e80487..83a29c9ed 100644
--- a/src/sat/sat_drat.h
+++ b/src/sat/sat_drat.h
@@ -61,7 +61,8 @@ namespace sat {
     class clause;
 
     struct print_clause {
-        virtual void on_clause(unsigned, literal const*, status) = 0;
+        virtual ~print_clause() {}
+        virtual void on_clause(unsigned, literal const*, status) = 0;        
     };
 
     class drat {
@@ -150,12 +151,12 @@ namespace sat {
 
         // support for SMT - connect Boolean variables with AST nodes
         // associate AST node id with Boolean variable v
-        void bool_def(bool_var v, unsigned n);
 
         // 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);
 
         // ad-hoc logging until a format is developed
         void log_adhoc(std::function<void(std::ostream&)>& fn);
diff --git a/src/sat/smt/euf_proof.cpp b/src/sat/smt/euf_proof.cpp
index a63efb79b..f18e112b8 100644
--- a/src/sat/smt/euf_proof.cpp
+++ b/src/sat/smt/euf_proof.cpp
@@ -41,6 +41,11 @@ namespace euf {
         get_drat().def_begin(id, n, name);
     }
 
+    void solver::bool_def(bool_var v, unsigned n) {
+        get_drat().bool_def(v, n);
+    }
+
+
     void solver::drat_log_params(func_decl* f) {
         for (unsigned i = f->get_num_parameters(); i-- > 0; ) {
             auto const& p = f->get_parameter(i);
@@ -59,14 +64,14 @@ namespace euf {
             drat_log_decl(a->get_decl());
             std::stringstream strm;
             strm << mk_ismt2_func(a->get_decl(), m);
-            get_drat().def_begin('e', e->get_id(), strm.str());
+            def_begin('e', e->get_id(), strm.str());
             for (expr* arg : *a)
                 def_add_arg(arg->get_id());
             def_end();
         }
         else if (is_var(e)) {
             var* v = to_var(e);
-            get_drat().def_begin('v', v->get_id(), "" + mk_pp(e->get_sort(), m));
+            def_begin('v', v->get_id(), "" + mk_pp(e->get_sort(), m));
             def_add_arg(v->get_idx());
             def_end();
         }
@@ -77,7 +82,7 @@ namespace euf {
             for (unsigned i = 0; i < q->get_num_decls(); ++i) 
                 strm << " (" << q->get_decl_name(i) << " " << mk_pp(q->get_decl_sort(i), m) << ")";            
             strm << ")";
-            get_drat().def_begin('q', q->get_id(), strm.str());
+            def_begin('q', q->get_id(), strm.str());
             def_add_arg(q->get_expr()->get_id());
             def_end();
         }
@@ -116,7 +121,7 @@ namespace euf {
         if (!use_drat())
             return;
         drat_log_expr(e);
-        get_drat().bool_def(v, e->get_id());
+        bool_def(v, e->get_id());
     }
 
 
@@ -130,7 +135,7 @@ namespace euf {
         std::ostringstream strm;
         smt2_pp_environment_dbg env(m);
         ast_smt2_pp(strm, f, env);
-        get_drat().def_begin('f', f->get_small_id(), strm.str());
+        def_begin('f', f->get_small_id(), strm.str());
         def_end();
     }
 
@@ -200,11 +205,11 @@ namespace euf {
         VERIFY(m.is_eq(eq, a, b));
         drat_log_expr(a);
         drat_log_expr(b);
-        get_drat().def_begin('e', eq->get_id(), std::string("="));
+        def_begin('e', eq->get_id(), std::string("="));
         def_add_arg(a->get_id());
         def_add_arg(b->get_id());
         def_end();
-        get_drat().bool_def(lit.var(), eq->get_id());
+        bool_def(lit.var(), eq->get_id());
     }
 
     void solver::on_clause(unsigned n, literal const* lits, sat::status st) {
diff --git a/src/sat/smt/euf_solver.h b/src/sat/smt/euf_solver.h
index f77954ded..ed1ad9b92 100644
--- a/src/sat/smt/euf_solver.h
+++ b/src/sat/smt/euf_solver.h
@@ -352,6 +352,7 @@ namespace euf {
         void drat_bool_def(sat::bool_var v, expr* n);
         void drat_eq_def(sat::literal lit, expr* eq);
         void drat_log_expr(expr* n);
+        void bool_def(bool_var v, unsigned n);
         bool visit_clause(unsigned n, literal const* lits);
         void display_clause(unsigned n, literal const* lits);
         void visit_expr(expr* e);

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 3/3] 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 0633612ad..8e63b4a19 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 83a29c9ed..1ba86d724 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 f18e112b8..567f6fc1c 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 13d3e02e4..1c762cb3f 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";
         }
     }