From dc8ec50137d892a70818487e9a4ac49be342890e Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 2 Jul 2018 13:53:55 -0700
Subject: [PATCH] enable proof objects for PB

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/smt/theory_pb.cpp | 30 ++++++++++++++++++++++++++----
 1 file changed, 26 insertions(+), 4 deletions(-)

diff --git a/src/smt/theory_pb.cpp b/src/smt/theory_pb.cpp
index 953ecea2c..b2f15d41e 100644
--- a/src/smt/theory_pb.cpp
+++ b/src/smt/theory_pb.cpp
@@ -752,9 +752,10 @@ namespace smt {
     class theory_pb::card_justification : public justification {
         card& m_card;
         family_id m_fid;
+        literal m_lit;
     public:
-        card_justification(card& c, family_id fid)
-            : justification(true), m_card(c), m_fid(fid) {}
+        card_justification(card& c, literal lit, family_id fid)
+            : justification(true), m_card(c), m_fid(fid), m_lit(lit) {}
 
         card& get_card() { return m_card; }
 
@@ -769,7 +770,28 @@ namespace smt {
             return m_fid;
         }
         
-        virtual proof* mk_proof(smt::conflict_resolution& cr) { return 0; }
+        virtual proof* mk_proof(smt::conflict_resolution& cr) { 
+            ptr_buffer<proof> prs;
+            ast_manager& m = cr.get_context().get_manager(); 
+            expr_ref fact(m);
+            cr.get_context().literal2expr(m_lit, fact);
+            bool all_valid = true;
+            proof* pr = nullptr;
+            pr = cr.get_proof(m_card.lit());
+            all_valid &= pr != nullptr;
+            prs.push_back(pr);
+            for (unsigned i = m_card.k(); i < m_card.size(); ++i) {
+                pr = cr.get_proof(~m_card.lit(i));
+                all_valid &= pr != nullptr;
+                prs.push_back(pr);
+            }
+            if (!all_valid) {
+                return nullptr;
+            }
+            else {
+                return m.mk_th_lemma(m_fid, fact, prs.size(), prs.c_ptr());
+            }
+        }
 
 
     };
@@ -959,7 +981,7 @@ namespace smt {
         m_stats.m_num_propagations++;
         TRACE("pb", tout << "#prop: " << c.num_propagations() << " - " << c.lit() << " => " << l << "\n";);
         SASSERT(validate_unit_propagation(c));
-        ctx.assign(l, ctx.mk_justification(card_justification(c, get_id())));
+        ctx.assign(l, ctx.mk_justification(card_justification(c, l, get_id())));
     }
 
     void theory_pb::clear_watch(card& c) {