z3-src 503.2.0

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
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50

/*++
Copyright (c) 2006 Microsoft Corporation

Module Name:

    macro_finder.h

Abstract:

    <abstract>

Author:

    Leonardo de Moura (leonardo) 2010-04-05.

Revision History:

--*/
#pragma once

#include "ast/macros/macro_manager.h"


/**
   \brief Macro finder is responsible for finding universally quantified sub-formulas that can be used
   as macros.
*/
class macro_finder {
    ast_manager &               m;
    macro_manager &             m_macro_manager;
    macro_util &                m_util;
    arith_util                  m_autil;
    bool expand_macros(expr_ref_vector const& exprs, proof_ref_vector const& prs, expr_dependency_ref_vector const & deps, 
                       expr_ref_vector & new_exprs, proof_ref_vector & new_prs, expr_dependency_ref_vector& new_deps);
    bool expand_macros(unsigned n, justified_expr const * fmls, vector<justified_expr>& new_fmls);
    bool is_arith_macro(expr * n, proof * pr, expr_ref_vector & new_exprs, proof_ref_vector & new_prs);
    bool is_arith_macro(expr * n, proof * pr, vector<justified_expr>& new_fmls);
    bool is_arith_macro(expr * n, proof * pr, bool deps_valid, expr_dependency * dep, expr_ref_vector & new_exprs, proof_ref_vector & new_prs, expr_dependency_ref_vector & new_deps);

    bool is_macro(expr * n, app_ref & head, expr_ref & def);

    void revert_unsafe_macros(vector<justified_expr>& new_fmls);

public:
    macro_finder(ast_manager & m, macro_manager & mm);
    void operator()(expr_ref_vector const& exprs, proof_ref_vector const& prs, expr_dependency_ref_vector const& deps, expr_ref_vector & new_exprs, proof_ref_vector & new_prs, expr_dependency_ref_vector & new_deps);
    void operator()(unsigned n, justified_expr const* fmls, vector<justified_expr>& new_fmls);
};