1 /*++
2 Copyright (c) 2012 Microsoft Corporation
3 
4 Module Name:
5 
6     replace_proof_converter.h
7 
8 Abstract:
9 
10     Proof converter to replace asserted leaves by proofs.
11 
12     Given a proof P with occurrences of [asserted fml]
13     Replace [asserted fml] by proofs whose conclusions are fml.
14 
15 Author:
16 
17     Nikolaj Bjorner (nbjorner) 2012-9-16
18 
19 Revision History:
20 
21 --*/
22 
23 #pragma once
24 
25 #include "tactic/proof_converter.h"
26 
27 class replace_proof_converter : public proof_converter {
28     ast_manager&    m;
29     proof_ref_vector m_proofs;
30 public:
31 
replace_proof_converter(ast_manager & _m)32     replace_proof_converter(ast_manager& _m): m(_m), m_proofs(m) {}
33 
~replace_proof_converter()34     ~replace_proof_converter() override {}
35 
36     proof_ref operator()(ast_manager & _m, unsigned num_source, proof * const * source) override;
37 
38     proof_converter * translate(ast_translation & translator) override;
39 
insert(proof * p)40     void insert(proof* p) { m_proofs.push_back(p); }
41 
get_manager()42     ast_manager& get_manager() { return m; }
43 
44     // run the replacements the inverse direction.
invert()45     void invert() { m_proofs.reverse(); }
46 
display(std::ostream & out)47     void display(std::ostream & out) override {}
48 
49 };
50 
51