z3 / src / smt / smt_quantifier_stat.h

Copyright (c) 2006 Microsoft Corporation

Module Name:





    Leonardo de Moura (leonardo) 2008-02-20.

Revision History:



namespace smt {
       \brief Store statistics for quantifiers. This information is
       used to implement heuristics for quantifier instantiation.
    class quantifier_stat {
        unsigned m_size;
        unsigned m_depth;
        unsigned m_generation;
        unsigned m_case_split_factor; //!< the product of the size of the clauses created by this quantifier.
        unsigned m_num_nested_quantifiers;
        unsigned m_num_instances;
        unsigned m_num_instances_curr_search;
        unsigned m_num_instances_curr_branch; //!< only updated if QI_TRACK_INSTANCES is true
        unsigned m_max_generation; //!< max. generation of an instance
        float    m_max_cost;

        friend class quantifier_stat_gen;

        quantifier_stat(unsigned generation);

        unsigned get_size() const { 
            return m_size; 
        unsigned get_depth() const { 
            return m_depth; 
        unsigned get_generation() const {
            return m_generation; 
        unsigned get_case_split_factor() const {
            return m_case_split_factor;

        unsigned get_num_nested_quantifiers() const {
            return m_num_nested_quantifiers;

        unsigned get_num_instances() const {
            return m_num_instances;

        unsigned get_num_instances_curr_search() const {
            return m_num_instances_curr_search;

        unsigned & get_num_instances_curr_branch() {
            return m_num_instances_curr_branch;
        void inc_num_instances() {

        void inc_num_instances_curr_branch() {

        void reset_num_instances_curr_search() {
            m_num_instances_curr_search = 0;

        void update_max_generation(unsigned g) {
            if (m_max_generation < g)
                m_max_generation = g;

        unsigned get_max_generation() const {
            return m_max_generation;

        void update_max_cost(float c) {
            if (m_max_cost < c)
                m_max_cost = c;

        float get_max_cost() const {
            return m_max_cost;

       \brief Functor used to generate quantifier statistics.
    class quantifier_stat_gen {
        struct entry {
            expr *    m_expr;
            unsigned  m_depth:31;
            bool      m_depth_only:1; //!< track only the depth of this entry.
            entry():m_expr(0), m_depth(0), m_depth_only(false) {}
            entry(expr * n, unsigned depth = 0, bool depth_only = false):m_expr(n), m_depth(depth), m_depth_only(depth_only) {}
        ast_manager &           m_manager;
        region &                m_region;
        obj_map<expr, unsigned> m_already_found; // expression to the max. depth it was reached.
        svector<entry>          m_todo;
        approx_nat              m_case_split_factor;
        void reset();
        quantifier_stat_gen(ast_manager & m, region & r);
        quantifier_stat * operator()(quantifier * q, unsigned generation);


#endif /* _SMT_QUANTIFIER_STAT_H_ */
Tip: Filter by directory path e.g. /media app.js to search for public/media/app.js.
Tip: Use camelCasing e.g. ProjME to search for
Tip: Filter by extension type e.g. /repo .js to search for all .js files in the /repo directory.
Tip: Separate your search with spaces e.g. /ssh pom.xml to search for src/ssh/pom.xml.
Tip: Use ↑ and ↓ arrow keys to navigate and return to view the file.
Tip: You can also navigate files with Ctrl+j (next) and Ctrl+k (previous) and view the file with Ctrl+o.
Tip: You can also navigate files with Alt+j (next) and Alt+k (previous) and view the file with Alt+o.