1 /*++
2 Copyright (c) 2012 Microsoft Corporation
3 
4 Module Name:
5 
6     rel_context.h
7 
8 Abstract:
9 
10     context for relational datalog engine.
11 
12 Author:
13 
14     Nikolaj Bjorner (nbjorner) 2012-12-3.
15 
16 Revision History:
17 
18     Extracted from dl_context
19 
20 --*/
21 #pragma once
22 #include "ast/ast.h"
23 #include "muz/rel/dl_relation_manager.h"
24 #include "muz/rel/dl_instruction.h"
25 #include "muz/base/dl_engine_base.h"
26 #include "muz/base/dl_context.h"
27 #include "util/lbool.h"
28 
29 namespace datalog {
30 
31     class context;
32     typedef vector<std::pair<func_decl*,relation_fact> > fact_vector;
33 
34     class rel_context : public rel_context_base {
35         context&           m_context;
36         ast_manager&       m;
37         relation_manager   m_rmanager;
38         expr_ref           m_answer;
39         relation_base *    m_last_result_relation;
40         fact_vector        m_table_facts;
41         execution_context  m_ectx;
42         instruction_block  m_code;
43         double             m_sw;
44 
45         class scoped_query;
46 
47         void reset_negated_tables();
48 
49         relation_plugin & get_ordinary_relation_plugin(symbol relation_name);
50 
51         lbool saturate(scoped_query& sq);
52 
53         void setup_default_relation();
54 
55     public:
56         rel_context(context& ctx);
57 
58         ~rel_context() override;
59 
60         relation_manager & get_rmanager() override;
61         const relation_manager & get_rmanager() const override;
get_manager()62         ast_manager& get_manager() const { return m; }
get_context()63         context&     get_context() const { return m_context; }
64         relation_base & get_relation(func_decl * pred) override;
65         relation_base * try_get_relation(func_decl * pred) const override;
66         bool is_empty_relation(func_decl* pred) const override;
67         expr_ref try_get_formula(func_decl * pred) const override;
get_answer()68         expr_ref get_answer() override { return m_answer; }
69 
70         bool output_profile() const override;
71 
72         lbool query(expr* q) override;
73         lbool query(unsigned num_rels, func_decl * const* rels) override;
74 
75         void set_predicate_representation(func_decl * pred, unsigned relation_name_cnt,
76                                           symbol const * relation_names) override;
77 
78         void inherit_predicate_kind(func_decl* new_pred, func_decl* orig_pred) override;
79 
80         void collect_statistics(statistics& st) const override;
81 
82         void updt_params() override;
83 
84         /**
85            \brief Restrict the set of used predicates to \c res.
86 
87            The function deallocates unused relations, it does not deal with rules.
88          */
89         void restrict_predicates(func_decl_set const& predicates) override;
90 
91         void transform_rules() override;
92 
93         model_ref get_model() override;
94 
95         bool try_get_size(func_decl* pred, unsigned& rel_size) const override;
96         /**
97            \brief query result if it contains fact.
98          */
99         bool result_contains_fact(relation_fact const& f) override;
100 
collect_non_empty_predicates(func_decl_set & ps)101         void collect_non_empty_predicates(func_decl_set& ps) override {
102             return get_rmanager().collect_non_empty_predicates(ps);
103         }
104 
105         /** \brief add facts to relation
106         */
107         void add_fact(func_decl* pred, relation_fact const& fact) override;
108         void add_fact(func_decl* pred, table_fact const& fact) override;
109 
110         /** \brief check if facts were added to relation
111         */
112         bool has_facts(func_decl * pred) const override;
113 
114         /**
115            \brief Store the relation \c rel under the predicate \c pred. The \c context object
116            takes over the ownership of the relation object.
117         */
118         void store_relation(func_decl * pred, relation_base * rel) override;
119 
120         void display_output_facts(rule_set const& rules, std::ostream & out) const override;
121         void display_facts(std::ostream & out) const override;
122 
123         void display_profile(std::ostream& out) override;
124 
125         lbool saturate() override;
126 
127     };
128 };
129 
130