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
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79

/*++
Copyright (c) 2011 Microsoft Corporation

Module Name:

    expr2var.h

Abstract:

    The mapping between Z3 expressions and (low level) variables.
    Example of low level variables:
       - SAT solver
       - Polynomial 
       - etc.

Author:

    Leonardo (leonardo) 2011-12-23

Notes:

--*/
#pragma once

#include "ast/ast.h"
#include "util/obj_hashtable.h"

/**
   \brief The mapping between Z3 expressions and (low level) variables.
*/
class expr2var {
public:
    typedef unsigned var;
    typedef obj_map<expr, var>::key_data key_value;
    typedef key_value const* iterator;
    typedef ptr_vector<expr>::const_iterator recent_iterator;
protected:
    ast_manager &    m_manager;
    
    unsigned_vector    m_id2map;
    svector<key_value> m_mapping;
    ptr_vector<expr> m_recent_exprs;
    unsigned_vector  m_recent_lim;
    bool             m_interpreted_vars;
public:
    expr2var(ast_manager & m);
    ~expr2var();

    ast_manager & m() const { return m_manager; }

    void insert(expr * n, var v);
    
    var to_var(expr * n) const;
    
    bool is_var(expr * n) const { return m_id2map.get(n->get_id(), UINT_MAX) != UINT_MAX; }

    void display(std::ostream & out) const;
    
    void mk_inv(expr_ref_vector & var2expr) const;

    // return true if the mapping contains interpreted vars.
    bool interpreted_vars() const { return m_interpreted_vars; }
    
    iterator begin() const { return m_mapping.begin(); }
    iterator end() const { return m_mapping.end(); }

    void reset_recent() { SASSERT(m_recent_lim.empty()); m_recent_exprs.reset(); }

    // Iterators for traversing the recently registered expressions.
    // The set of recent registered expressions is reset by using reset_recent().
    recent_iterator begin_recent() const { return m_recent_exprs.begin(); }
    recent_iterator end_recent() const { return m_recent_exprs.end(); }
    
    void reset();

    void push();
    void pop(unsigned num_scopes);
};