From 6cc6ffcde22d6894956b5adcb9e17d1ffdc49169 Mon Sep 17 00:00:00 2001
From: Arie Gurfinkel <arie.gurfinkel@uwaterloo.ca>
Date: Sun, 11 Nov 2018 08:26:00 -0500
Subject: [PATCH] Fix display_certificate in spacer

This is expected to work now
(query q1 :print-certificate true)
---
 src/muz/spacer/spacer_context.cpp | 28 ++++++++++++++++------------
 src/muz/spacer/spacer_context.h   |  7 +++++--
 2 files changed, 21 insertions(+), 14 deletions(-)

diff --git a/src/muz/spacer/spacer_context.cpp b/src/muz/spacer/spacer_context.cpp
index fd16e99f6..bbb06f719 100644
--- a/src/muz/spacer/spacer_context.cpp
+++ b/src/muz/spacer/spacer_context.cpp
@@ -2366,11 +2366,6 @@ void context::updt_params() {
     }
 }
 
-void context::display_certificate(std::ostream& out) const {
-    proof_ref pr = get_proof();
-    out << pr;
-}
-
 void context::reset()
 {
     TRACE("spacer", tout << "\n";);
@@ -2747,7 +2742,7 @@ lbool context::solve(unsigned from_lvl)
     if (m_last_result == l_true) {
         m_stats.m_cex_depth = get_cex_depth ();
     }
- 
+
     if (m_params.print_statistics ()) {
         statistics st;
         collect_statistics (st);
@@ -2931,10 +2926,6 @@ expr_ref context::get_answer()
     }
 }
 
-/**
-   \brief Retrieve satisfying assignment with explanation.
-*/
-expr_ref context::mk_sat_answer() {return get_ground_sat_answer();}
 
 
 expr_ref context::mk_unsat_answer() const
@@ -2957,8 +2948,7 @@ proof_ref context::get_ground_refutation() {
     ground_sat_answer_op op(*this);
     return op(*m_query);
 }
-expr_ref context::get_ground_sat_answer()
-{
+expr_ref context::get_ground_sat_answer() const {
     if (m_last_result != l_true) {
         IF_VERBOSE(0, verbose_stream()
                    << "Sat answer unavailable when result is false\n";);
@@ -3086,6 +3076,20 @@ expr_ref context::get_ground_sat_answer()
     return expr_ref(m.mk_and(cex.size(), cex.c_ptr()), m);
 }
 
+void context::display_certificate(std::ostream &out) const {
+    switch(m_last_result) {
+    case l_false:
+        out << mk_pp(mk_unsat_answer(), m);
+        break;
+    case l_true:
+        out << mk_pp(mk_sat_answer(), m);
+        break;
+    case l_undef:
+        out << "unknown";
+        break;
+    }
+}
+
 ///this is where everything starts
 lbool context::solve_core (unsigned from_lvl)
 {
diff --git a/src/muz/spacer/spacer_context.h b/src/muz/spacer/spacer_context.h
index 8dd13cf63..494de1c23 100644
--- a/src/muz/spacer/spacer_context.h
+++ b/src/muz/spacer/spacer_context.h
@@ -1007,7 +1007,10 @@ class context {
                          const vector<bool>& reach_pred_used,
                          pob_ref_buffer &out);
 
-    expr_ref mk_sat_answer();
+    /**
+       \brief Retrieve satisfying assignment with explanation.
+    */
+    expr_ref mk_sat_answer() const {return get_ground_sat_answer();}
     expr_ref mk_unsat_answer() const;
     unsigned get_cex_depth ();
 
@@ -1083,7 +1086,7 @@ public:
      * get bottom-up (from query) sequence of ground predicate instances
      * (for e.g. P(0,1,0,0,3)) that together form a ground derivation to query
      */
-    expr_ref get_ground_sat_answer ();
+    expr_ref get_ground_sat_answer () const;
     proof_ref get_ground_refutation();
     void get_rules_along_trace (datalog::rule_ref_vector& rules);