mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-04 13:21:22 +00:00
Code Activity

Fix display_certificate in spacer

Browse source 
This is expected to work now
(query q1 :print-certificate true)
This commit is contained in:
Arie Gurfinkel 2018-11-11 08:26:00 -05:00
parent 58d93d8907
commit 6cc6ffcde2
2 changed files with 21 additions and 14 deletions
Download patch file Download diff file Expand all files Collapse all files

28
src/muz/spacer/spacer_context.cpp
View file

@ -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() void context::reset()
{ {
TRACE("spacer", tout << "\n";); TRACE("spacer", tout << "\n";);
@ -2747,7 +2742,7 @@ lbool context::solve(unsigned from_lvl)
if (m_last_result == l_true) { if (m_last_result == l_true) {
m_stats.m_cex_depth = get_cex_depth (); m_stats.m_cex_depth = get_cex_depth ();
} }
if (m_params.print_statistics ()) { if (m_params.print_statistics ()) {
statistics st; statistics st;
collect_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 expr_ref context::mk_unsat_answer() const
@ -2957,8 +2948,7 @@ proof_ref context::get_ground_refutation() {
ground_sat_answer_op op(*this); ground_sat_answer_op op(*this);
return op(*m_query); 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 (m_last_result != l_true) {
IF_VERBOSE(0, verbose_stream() IF_VERBOSE(0, verbose_stream()
<< "Sat answer unavailable when result is false\n";); << "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); 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 ///this is where everything starts
lbool context::solve_core (unsigned from_lvl) lbool context::solve_core (unsigned from_lvl)
{ {

7
src/muz/spacer/spacer_context.h
View file

@ -1007,7 +1007,10 @@ class context {
const vector<bool>& reach_pred_used, const vector<bool>& reach_pred_used,
pob_ref_buffer &out); 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; expr_ref mk_unsat_answer() const;
unsigned get_cex_depth (); unsigned get_cex_depth ();
@ -1083,7 +1086,7 @@ public:
* get bottom-up (from query) sequence of ground predicate instances * 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 * (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(); proof_ref get_ground_refutation();
void get_rules_along_trace (datalog::rule_ref_vector& rules); void get_rules_along_trace (datalog::rule_ref_vector& rules);