z3-src 503.0.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
51
52
53
54
55
56
57
58
59
60
61
62
63
64

/*++
Copyright (c) 2006 Microsoft Corporation

Module Name:

    smt_quantifier_instances.h

Abstract:

    <abstract>

Author:

    Leonardo de Moura (leonardo) 2008-03-26.

Revision History:

--*/
#pragma once

namespace smt {

    class quantifier_instances;

    class quantifier_instance {
        quantifier * m_quantifier;
        double       m_cost;
        enode *      m_enodes[0];
        quantifier_instance(quantifier * q, enode * const * enodes);
        friend class quantifier_instances;
    public:
        quantifier * get_quantifier() const { return m_quantifier; }
        unsigned get_num_decls() const { return m_quantifier->get_num_decls(); }
        double get_cost() const { return m_cost; }
        enode * const * get_enodes() const { return m_enodes; }
        bool operator==(quantifier_instance const & other) const;
        unsigned hash() const;
    };


    class quantifier_instances {
        struct instance_lt {
            ptr_vector<quantifier_instance> const & m_stack;
            instance_lt(ptr_vector<quantifier_instance> const & s):
                m_stack(s) {
            }
            bool operator()(int i1, int i2) const {
                return m_stack[i1]->get_cost() < m_stack[i2]->get_cost();
            }
        };

        context &                          m_context;
        ast_manager &                      m_manager;
        obj_hashtable<quantifier_instance> m_instances;  //!< Set of instances.
        ptr_vector<quantifier_instance>    m_stack;      //!< Stack for backtracking.
        heap<instance_lt>                  m_queue;      //!< Instantiation priority queue.
        unsigned_vector                    m_scopes;
        
        
    };

};