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