Implement get_proof() in bmc and spacer engines

Z3Prover · Aug 12, 2019 · 375c0ff · 375c0ff
1 parent 876cfb4
commit 375c0ff
Show file tree

Hide file tree

Showing 4 changed files with 8 additions and 8 deletions.
diff --git a/src/muz/bmc/dl_bmc_engine.cpp b/src/muz/bmc/dl_bmc_engine.cpp
@@ -1537,10 +1537,14 @@ namespace datalog {
         // m_solver->reset_statistics();
     }
 
-    expr_ref bmc::get_answer() {
+    expr_ref bmc::get_answer()  {
         return m_answer;
     }
 
+    proof_ref bmc::get_proof() {
+        return proof_ref(to_app(m_answer), m);
+    }
+
     void bmc::get_rules_along_trace(datalog::rule_ref_vector& rules) {
         rules.append(m_rule_trace);
     }

diff --git a/src/muz/bmc/dl_bmc_engine.h b/src/muz/bmc/dl_bmc_engine.h
@@ -63,7 +63,8 @@ namespace datalog {
         void reset_statistics() override;
         void get_rules_along_trace(datalog::rule_ref_vector& rules) override;
 
-        expr_ref get_answer() override;
+        expr_ref get_answer()  override;
+        proof_ref get_proof() override; 
 
         // direct access to (new) non-linear compiler.
         void compile(rule_set const& rules, expr_ref_vector& fmls, unsigned level);

diff --git a/src/muz/spacer/spacer_context.cpp b/src/muz/spacer/spacer_context.cpp
@@ -2909,11 +2909,6 @@ model_ref context::get_model()
     return model;
 }
 
-proof_ref context::get_proof() const
-{
-    return proof_ref (m);
-}
-
 expr_ref context::get_answer()
 {
     switch(m_last_result) {

diff --git a/src/muz/spacer/spacer_context.h b/src/muz/spacer/spacer_context.h
@@ -1109,7 +1109,7 @@ class context {
     expr_ref get_reachable (func_decl* p);
     void add_invariant (func_decl *pred, expr* property);
     model_ref get_model();
-    proof_ref get_proof() const;
+    proof_ref get_proof() const {return get_ground_refutation();}
 
     expr_ref get_constraints (unsigned lvl);
     void add_constraint (expr *c, unsigned lvl);