1 /*++
2 Copyright (c) 2015 Microsoft Corporation
3
4 Module Name:
5
6 label_rewriter.cpp
7
8 Abstract:
9
10 Basic rewriting rules for removing labels.
11
12 Author:
13
14 Nikolaj Bjorner (nbjorner) 2015-19-10
15
16 Notes:
17
18 --*/
19
20 #include "ast/rewriter/rewriter.h"
21 #include "ast/rewriter/rewriter_def.h"
22 #include "ast/rewriter/label_rewriter.h"
23
24
label_rewriter(ast_manager & m)25 label_rewriter::label_rewriter(ast_manager & m) :
26 m_label_fid(m.get_label_family_id()),
27 m_rwr(m, false, *this) {}
28
~label_rewriter()29 label_rewriter::~label_rewriter() {}
30
reduce_app(func_decl * f,unsigned num,expr * const * args,expr_ref & result,proof_ref & result_pr)31 br_status label_rewriter::reduce_app(
32 func_decl * f, unsigned num, expr * const * args, expr_ref & result,
33 proof_ref & result_pr) {
34 if (is_decl_of(f, m_label_fid, OP_LABEL)) {
35 SASSERT(num == 1);
36 result = args[0];
37 return BR_DONE;
38 }
39 return BR_FAILED;
40 }
41
remove_labels(expr_ref & fml,proof_ref & pr)42 void label_rewriter::remove_labels(expr_ref& fml, proof_ref& pr) {
43 ast_manager& m = fml.get_manager();
44 expr_ref tmp(m);
45 m_rwr(fml, tmp);
46 if (pr && fml != tmp) {
47 pr = m.mk_modus_ponens(pr, m.mk_rewrite(fml, tmp));
48 }
49 fml = tmp;
50 }
51
52
53 //template class rewriter_tpl<label_rewriter>;
54