z3 / src / muz_qe / dl_mk_subsumption_checker.h

/*++
Copyright (c) 2006 Microsoft Corporation

Module Name:

    mk_subsumption_checker.h

Abstract:

    Rule transformer which checks for subsumption
    (currently just for subsumption with total relations)

Author:

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

Revision History:

--*/

#ifndef _DL_MK_SUBSUMPTION_CHECKER_H_
#define _DL_MK_SUBSUMPTION_CHECKER_H_

#include "dl_context.h"
#include "dl_rule_transformer.h"
#include "dl_rule_subsumption_index.h"

namespace datalog {

    class mk_subsumption_checker : public rule_transformer::plugin {


        ast_manager & m;
        context & m_context;

        rule_ref_vector m_ref_holder;

        func_decl_set m_total_relations;

        /** Map that for each relation contains the rule which implies its totality.
        If the totality is due to the relation containing all facts, the rule stored 
        here is zero*/
        obj_map<func_decl, rule *> m_total_relation_defining_rules;


        /**
        Contains heads of rules of shape
        R(c1,c2,...cN).
        grouped by their predicate.

        This information helps to improve the results of the 
        scan_for_relations_total_due_to_facts() function.
        */
        obj_map<func_decl, obj_hashtable<app> *> m_ground_unconditional_rule_heads;


        bool m_have_new_total_rule;
        bool m_new_total_relation_discovery_during_transformation;

        bool is_total_rule(const rule * r);



        /** Function to be called when a new total relation is discovered */
        void on_discovered_total_relation(func_decl * pred, rule * r);

        void scan_for_total_rules(const rule_set & rules);
        void scan_for_relations_total_due_to_facts();

        void collect_ground_unconditional_rule_heads(const rule_set & rules);

        /** Return false if rule is unsatisfiable */
        bool transform_rule(rule * r, rule_subsumption_index& subs_index, rule_ref & res);
        /** Return false if the rule set hasn't changed */
        bool transform_rules(const rule_set & orig, rule_set & tgt);
    public:
        mk_subsumption_checker(context & ctx, unsigned priority=31000)
            : plugin(priority),
            m(ctx.get_manager()),
            m_context(ctx),
            m_ref_holder(ctx.get_rule_manager()),
            m_new_total_relation_discovery_during_transformation(true) {}
        ~mk_subsumption_checker() {
            reset_dealloc_values(m_ground_unconditional_rule_heads);
        }

        rule_set * operator()(rule_set const & source, model_converter_ref& mc, proof_converter_ref& pc);
    };

};

#endif /* _DL_MK_SUBSUMPTION_CHECKER_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 ProjectModifiedEvent.java.
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.