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

/*++
Copyright (c) 2006 Microsoft Corporation

Module Name:

    dl_rule_subsumption_index.h

Abstract:

    Subsumption index for rules.
    Currently an underapproximation (fails to identify some subsumptions).

Author:

    Krystof Hoder (t-khoder) 2011-10-10.

Revision History:

--*/

#pragma once

#include "muz/base/dl_context.h"

namespace datalog {

    class rule_subsumption_index {

        typedef obj_hashtable<app> app_set;

        ast_manager & m;
        // context & m_context;

        rule_ref_vector m_ref_holder;

        obj_map<func_decl, app_set *> m_unconditioned_heads;

        hashtable<rule *, rule_hash_proc, rule_eq_proc> m_rule_set;

        void handle_unconditioned_rule(rule * r);

    public:
        rule_subsumption_index(context & ctx) :
            m(ctx.get_manager()),
            // m_context(ctx),
            m_ref_holder(ctx.get_rule_manager()) {}

        ~rule_subsumption_index() {
            reset_dealloc_values(m_unconditioned_heads);
        }

        rule_subsumption_index(rule_subsumption_index const&) = delete;
        rule_subsumption_index& operator=(rule_subsumption_index const&) = delete;
        void add(rule * r);
        bool is_subsumed(rule * r);
        bool is_subsumed(app * query);
    };

};