move common routines for quantifiers

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

src/ast/CMakeLists.txt

@@ -14,6 +14,7 @@ z3_add_component(ast
     ast_translation.cpp
     ast_util.cpp
     bv_decl_plugin.cpp
+    cached_var_subst.cpp
     char_decl_plugin.cpp
     datatype_decl_plugin.cpp
     decl_collector.cpp
@@ -37,6 +38,7 @@ z3_add_component(ast
     occurs.cpp
     pb_decl_plugin.cpp
     pp.cpp
+    quantifier_stat.cpp
     recfun_decl_plugin.cpp
     reg_decl_plugins.cpp
     seq_decl_plugin.cpp

src/ast/cached_var_subst.cpp

@@ -0,0 +1,99 @@
+/*++
+Copyright (c) 2006 Microsoft Corporation
+
+Module Name:
+
+    cached_var_subst.cpp
+
+Abstract:
+
+    <abstract>
+
+Author:
+
+    Leonardo de Moura (leonardo) 2009-01-23.
+
+Revision History:
+
+--*/
+#include "ast/cached_var_subst.h"
+#include "ast/rewriter/rewriter_def.h"
+
+bool cached_var_subst::key_eq_proc::operator()(cached_var_subst::key * k1, cached_var_subst::key * k2) const {
+    if (k1->m_qa != k2->m_qa)
+        return false;
+    if (k1->m_num_bindings != k2->m_num_bindings)
+        return false;
+    for (unsigned i = 0; i < k1->m_num_bindings; i++)
+        if (k1->m_bindings[i] != k2->m_bindings[i])
+            return false;
+    return true;
+}
+
+cached_var_subst::cached_var_subst(ast_manager & _m):
+    m(_m),
+    m_proc(m),
+    m_refs(m) {
+}
+
+void cached_var_subst::reset() {
+    m_refs.reset();
+    m_instances.reset();
+    m_region.reset();
+    m_new_keys.reset();
+    m_key = nullptr;
+}
+
+expr** cached_var_subst::operator()(quantifier* qa, unsigned num_bindings) {
+    m_new_keys.reserve(num_bindings+1, 0);
+    m_key = m_new_keys[num_bindings];
+    if (m_key == nullptr)
+        m_key = static_cast<key*>(m_region.allocate(sizeof(key) + sizeof(expr*)*num_bindings));
+    m_key->m_qa           = qa;
+    m_key->m_num_bindings = num_bindings;
+    return m_key->m_bindings;
+}
+
+
+expr_ref cached_var_subst::operator()() {
+    expr_ref result(m);
+
+    auto* entry = m_instances.insert_if_not_there3(m_key, nullptr);
+    unsigned num_bindings = m_key->m_num_bindings;
+    if (entry->get_data().m_key != m_key) {
+        SASSERT(entry->get_data().m_value != 0);
+        // entry was already there
+        m_new_keys[num_bindings] = m_key; // recycle key
+        result = entry->get_data().m_value;
+        SCTRACE("bindings", is_trace_enabled("coming_from_quant"), tout << "(cache)\n";
+                for (unsigned i = 0; i < num_bindings; i++) 
+                    if (m_key->m_bindings[i]) 
+                        tout << i << ": " << mk_ismt2_pp(m_key->m_bindings[i], result.m()) << ";\n";
+                tout.flush(););
+        return result;
+    }
+
+    SASSERT(entry->get_data().m_value == 0);
+    try {
+        result = m_proc(m_key->m_qa->get_expr(), m_key->m_num_bindings, m_key->m_bindings);
+    }
+    catch (...) {
+        // CMW: The var_subst reducer was interrupted and m_instances is
+        // in an inconsistent state; we need to remove (m_key, 0).
+        m_instances.remove(m_key);
+        throw; 
+    }
+
+    // cache result
+    entry->get_data().m_value = result;
+
+    // remove key from cache
+    m_new_keys[num_bindings] = nullptr;
+
+    // increment reference counters
+    m_refs.push_back(m_key->m_qa);
+    for (unsigned i = 0; i < m_key->m_num_bindings; i++)
+        m_refs.push_back(m_key->m_bindings[i]);
+    m_refs.push_back(result);
+    return result;
+}

src/ast/cached_var_subst.h

@@ -0,0 +1,53 @@
+/*++
+Copyright (c) 2006 Microsoft Corporation
+
+Module Name:
+
+    cached_var_subst.h
+
+Abstract:
+
+    <abstract>
+
+Author:
+
+    Leonardo de Moura (leonardo) 2009-01-23.
+
+Revision History:
+
+--*/
+#pragma once
+
+#include "ast/rewriter/var_subst.h"
+#include "util/map.h"
+
+class cached_var_subst {
+    struct key {
+        quantifier * m_qa;
+        unsigned     m_num_bindings;
+        expr *       m_bindings[0];
+    };
+    struct key_hash_proc {
+        unsigned operator()(key * k) const {
+            return string_hash(reinterpret_cast<char const *>(k->m_bindings), sizeof(expr *) * k->m_num_bindings, k->m_qa->get_id());
+        }
+    };
+    struct key_eq_proc {
+        bool operator()(key * k1, key * k2) const;
+    };
+    typedef map<key *, expr *, key_hash_proc, key_eq_proc> instances;
+    ast_manager&     m;
+    var_subst        m_proc;
+    expr_ref_vector  m_refs;
+    instances        m_instances;
+    region           m_region;
+    ptr_vector<key>  m_new_keys; // mapping from num_bindings -> next key
+    key*             m_key { nullptr };
+public:
+    cached_var_subst(ast_manager & m);
+    expr** operator()(quantifier * qa, unsigned num_bindings);
+    expr_ref operator()();
+    void reset();
+};
+
+

src/ast/quantifier_stat.cpp

@@ -0,0 +1,119 @@
+/*++
+Copyright (c) 2006 Microsoft Corporation
+
+Module Name:
+
+    smt_quantifier_stat.cpp
+
+Abstract:
+
+    <abstract>
+
+Author:
+
+    Leonardo de Moura (leonardo) 2008-02-20.
+
+Revision History:
+
+--*/
+#include "ast/quantifier_stat.h"
+
+namespace q {
+
+    quantifier_stat::quantifier_stat(unsigned generation):
+        m_size(0),
+        m_depth(0),
+        m_generation(generation),
+        m_case_split_factor(1),
+        m_num_nested_quantifiers(0),
+        m_num_instances(0),
+        m_num_instances_checker_sat(0),
+        m_num_instances_simplify_true(0),
+        m_num_instances_curr_search(0),
+        m_num_instances_curr_branch(0),
+        m_max_generation(0),
+        m_max_cost(0.0f) {
+    }
+
+    quantifier_stat_gen::quantifier_stat_gen(ast_manager & m, region & r):
+        m_manager(m),
+        m_region(r) {
+    }
+
+    void quantifier_stat_gen::reset() {
+        m_already_found.reset();
+        m_todo.reset();
+        m_case_split_factor = 1;
+    }
+
+    quantifier_stat * quantifier_stat_gen::operator()(quantifier * q, unsigned generation) {
+        reset();
+        quantifier_stat * r = new (m_region) quantifier_stat(generation);
+        m_todo.push_back(entry(q->get_expr()));
+        while (!m_todo.empty()) {
+            entry & e       = m_todo.back();
+            expr * n        = e.m_expr;
+            unsigned depth  = e.m_depth;
+            bool depth_only = e.m_depth_only;
+            m_todo.pop_back();
+            unsigned old_depth;
+            if (m_already_found.find(n, old_depth)) {
+                if (old_depth >= depth)
+                    continue;
+                depth_only  = true;
+            }
+            m_already_found.insert(n, depth);
+            if (depth >= r->m_depth) 
+                r->m_depth = depth;
+            if (!depth_only) {
+                r->m_size++;
+                if (is_quantifier(n))
+                    r->m_num_nested_quantifiers ++;
+                if (is_app(n) && to_app(n)->get_family_id() == m_manager.get_basic_family_id()) {
+                    unsigned num_args = to_app(n)->get_num_args();
+                    // Remark: I'm approximating the case_split factor.
+                    // I'm also ignoring the case split factor due to theories.
+                    switch (to_app(n)->get_decl_kind()) {
+                    case OP_OR:
+                        if (depth == 0)
+                            m_case_split_factor *= num_args;
+                        else
+                            m_case_split_factor *= (num_args + 1);
+                        break;
+                    case OP_AND:
+                        if (depth > 0)
+                            m_case_split_factor *= (num_args + 1);
+                        break;
+                    case OP_EQ:
+                        if (m_manager.is_iff(n)) {
+                            if (depth == 0)
+                                m_case_split_factor *= 4;
+                            else
+                                m_case_split_factor *= 9;
+                        }
+                        break;
+                    case OP_ITE:
+                        if (depth == 0)
+                            m_case_split_factor *= 4;
+                        else
+                            m_case_split_factor *= 9;
+                        break;
+                    default:
+                        break;
+                    }
+                }
+            }
+            if (is_app(n)) {
+                unsigned j = to_app(n)->get_num_args();
+                while (j > 0) {
+                    --j;
+                    m_todo.push_back(entry(to_app(n)->get_arg(j), depth + 1, depth_only));
+                }
+            }
+        }
+        r->m_case_split_factor = m_case_split_factor.get_value();
+        return r;
+    }
+
+};
+

src/ast/quantifier_stat.h

@@ -0,0 +1,154 @@
+/*++
+Copyright (c) 2006 Microsoft Corporation
+
+Module Name:
+
+    quantifier_stat.h
+
+Abstract:
+
+    <abstract>
+
+Author:
+
+    Leonardo de Moura (leonardo) 2008-02-20.
+
+Revision History:
+
+--*/
+#pragma once
+
+#include "ast/ast.h"
+#include "util/obj_hashtable.h"
+#include "util/approx_nat.h"
+#include "util/region.h"
+
+namespace q {
+    
+    /**
+       \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_checker_sat;
+        unsigned m_num_instances_simplify_true;
+        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);
+    public:
+
+        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_simplify_true() const {
+            return m_num_instances_simplify_true;
+        }
+        unsigned get_num_instances_checker_sat() const {
+            return m_num_instances_checker_sat;
+        }
+
+        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_simplify_true() {
+            m_num_instances_simplify_true++;
+        }
+
+        void inc_num_instances_checker_sat() {
+            m_num_instances_checker_sat++;
+        }
+        
+        void inc_num_instances() {
+            m_num_instances++;
+            m_num_instances_curr_search++;
+        }
+
+        void inc_num_instances_curr_branch() {
+            m_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(nullptr), 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();
+        
+    public:
+        quantifier_stat_gen(ast_manager & m, region & r);
+        quantifier_stat * operator()(quantifier * q, unsigned generation);
+    };
+
+};
+
+