1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
/*++
Copyright (c) 2015 Microsoft Corporation
Module Name:
label_rewriter.h
Abstract:
Basic rewriting rules for labels.
Author:
Nikolaj Bjorner (nbjorner) 2015-19-10
Notes:
--*/
#pragma once
#include "ast/ast.h"
#include "ast/rewriter/rewriter_types.h"
class label_rewriter : public default_rewriter_cfg {
family_id m_label_fid;
rewriter_tpl<label_rewriter> m_rwr;
public:
label_rewriter(ast_manager & m);
br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result,
proof_ref & result_pr);
void remove_labels(expr_ref& fml, proof_ref& pr);
};