z3-src 415.4.4

Source distribution of the Z3 SMT solver, for use as a build dependency
Documentation 
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

 /*++
 Copyright (c) 2016 Microsoft Corporation

 Module Name:

  mk_extract_proc.h

 Abstract:


 Author:

 Mikolas Janota (MikolasJanota)

 Revision History:
 --*/
#pragma once
#include "ast/ast.h"
#include "ast/bv_decl_plugin.h"
class mk_extract_proc {
    bv_util &     m_util;
    unsigned      m_high;
    unsigned      m_low;
    sort *        m_domain;
    func_decl *   m_f_cached;
public:
    mk_extract_proc(bv_util & u);
    ~mk_extract_proc();
    app * operator()(unsigned high, unsigned low, expr * arg);
    ast_manager & m() { return m_util.get_manager(); }
    bv_util & bvutil() { return m_util; }
};