1 /*++
2 Copyright (c) 2016 Microsoft Corporation
3
4 Module Name:
5
6 mk_extract_proc.cpp
7
8 Abstract:
9
10
11 Author:
12
13 Mikolas Janota (MikolasJanota)
14
15 Revision History:
16 --*/
17 #include "ast/rewriter/mk_extract_proc.h"
mk_extract_proc(bv_util & u)18 mk_extract_proc::mk_extract_proc(bv_util & u):
19 m_util(u),
20 m_high(0),
21 m_low(UINT_MAX),
22 m_domain(nullptr),
23 m_f_cached(nullptr) {
24 }
25
~mk_extract_proc()26 mk_extract_proc::~mk_extract_proc() {
27 if (m_f_cached) {
28 // m_f_cached has a reference to m_domain, so, I don't need to inc_ref m_domain
29 ast_manager & m = m_util.get_manager();
30 m.dec_ref(m_f_cached);
31 }
32 }
33
operator ()(unsigned high,unsigned low,expr * arg)34 app * mk_extract_proc::operator()(unsigned high, unsigned low, expr * arg) {
35 ast_manager & m = m_util.get_manager();
36 sort * s = arg->get_sort();
37 if (m_low == low && m_high == high && m_domain == s)
38 return m.mk_app(m_f_cached, arg);
39 // m_f_cached has a reference to m_domain, so, I don't need to inc_ref m_domain
40 if (m_f_cached)
41 m.dec_ref(m_f_cached);
42 app * r = to_app(m_util.mk_extract(high, low, arg));
43 m_high = high;
44 m_low = low;
45 m_domain = s;
46 m_f_cached = r->get_decl();
47 m.inc_ref(m_f_cached);
48 return r;
49 }
50