1 /*++
2 Copyright (c) 2010 Microsoft Corporation
3 
4 Module Name:
5 
6     dl_interval_relation.h
7 
8 Abstract:
9 
10     Basic interval reatlion.
11 
12 Author:
13 
14     Nikolaj Bjorner (nbjorner) 2010-2-11
15 
16 Revision History:
17 
18 --*/
19 #pragma once
20 
21 
22 #include "ast/arith_decl_plugin.h"
23 #include "smt/old_interval.h"
24 #include "muz/base/dl_context.h"
25 #include "muz/rel/dl_relation_manager.h"
26 #include "muz/rel/dl_base.h"
27 #include "muz/rel/dl_vector_relation.h"
28 
29 namespace datalog {
30 
31     class interval_relation;
32 
33     class interval_relation_plugin : public relation_plugin {
34         v_dependency_manager m_dep;
35         interval             m_empty;
36         arith_util           m_arith;
37 
38         class join_fn;
39         class project_fn;
40         class rename_fn;
41         class union_fn;
42         class filter_equal_fn;
43         class filter_identical_fn;
44         class filter_interpreted_fn;
45         friend class interval_relation;
46 
47         interval unite(interval const& src1, interval const& src2);
48         interval widen(interval const& src1, interval const& src2);
49         interval meet(interval const& src1, interval const& src2, bool& is_empty);
50 
dep()51         v_dependency_manager & dep() const { return const_cast<v_dependency_manager&>(m_dep); }
52 
53     public:
54         interval_relation_plugin(relation_manager& m);
55         bool can_handle_signature(const relation_signature & s) override;
get_name()56         static symbol get_name() { return symbol("interval_relation"); }
57         relation_base * mk_empty(const relation_signature & s) override;
58         relation_base * mk_full(func_decl* p, const relation_signature & s) override;
59         relation_join_fn * mk_join_fn(const relation_base & t1, const relation_base & t2,
60             unsigned col_cnt, const unsigned * cols1, const unsigned * cols2) override;
61         relation_transformer_fn * mk_project_fn(const relation_base & t, unsigned col_cnt,
62             const unsigned * removed_cols) override;
63         relation_transformer_fn * mk_rename_fn(const relation_base & t, unsigned permutation_cycle_len,
64             const unsigned * permutation_cycle) override;
65         relation_union_fn * mk_union_fn(const relation_base & tgt, const relation_base & src,
66             const relation_base * delta) override;
67         relation_union_fn * mk_widen_fn(const relation_base & tgt, const relation_base & src,
68             const relation_base * delta) override;
69         relation_mutator_fn * mk_filter_identical_fn(const relation_base & t, unsigned col_cnt,
70             const unsigned * identical_cols) override;
71         relation_mutator_fn * mk_filter_equal_fn(const relation_base & t, const relation_element & value,
72             unsigned col) override;
73         relation_mutator_fn * mk_filter_interpreted_fn(const relation_base & t, app * condition) override;
74 
75         static bool is_empty(unsigned idx, interval const& i);
76         static bool is_infinite(interval const& i);
77 
78     private:
79         static interval_relation& get(relation_base& r);
80         static interval_relation const & get(relation_base const& r);
81 
82         bool is_linear(expr* e, unsigned& pos, unsigned& neg, rational& k, bool is_pos) const;
83 
84         // x + k <= y
85         bool is_le(app* cond, unsigned& x, rational& k, unsigned& y, bool& is_int) const;
86         // x + k < y
87         bool is_lt(app* cond, unsigned& x, rational& k, unsigned& y) const;
88         // x + k = y
89         bool is_eq(app* cond, unsigned& x, rational& k, unsigned& y) const;
90     };
91 
92 
93     class interval_relation : public vector_relation<interval> {
94         friend class interval_relation_plugin;
95         friend class interval_relation_plugin::filter_equal_fn;
96     public:
97         interval_relation(interval_relation_plugin& p, relation_signature const& s, bool is_empty);
98 
99         void add_fact(const relation_fact & f) override;
100         bool contains_fact(const relation_fact & f) const override;
101         interval_relation * clone() const override;
102         interval_relation * complement(func_decl*) const override;
103         void to_formula(expr_ref& fml) const override;
104         interval_relation_plugin& get_plugin() const;
105 
106         void filter_interpreted(app* cond);
is_precise()107         bool is_precise() const override { return false; }
108 
109     private:
110 
mk_intersect(interval const & t1,interval const & t2,bool & is_empty)111         interval mk_intersect(interval const& t1, interval const& t2, bool& is_empty) const override {
112             return get_plugin().meet(t1, t2, is_empty);
113         }
114 
mk_unite(interval const & t1,interval const & t2)115         interval mk_unite(interval const& t1, interval const& t2) const override { return get_plugin().unite(t1,t2); }
116 
mk_widen(interval const & t1,interval const & t2)117         interval mk_widen(interval const& t1, interval const& t2) const override { return get_plugin().widen(t1,t2); }
118 
is_subset_of(interval const & t1,interval const & t2)119         bool is_subset_of(interval const& t1, interval const& t2) const override { NOT_IMPLEMENTED_YET(); return false; }
120 
is_full(interval const & t)121         bool is_full(interval const& t) const override {
122             return interval_relation_plugin::is_infinite(t);
123         }
124 
is_empty(unsigned idx,interval const & t)125         bool is_empty(unsigned idx, interval const& t) const override {
126             return interval_relation_plugin::is_empty(idx, t);
127         }
128 
129         void mk_rename_elem(interval& i, unsigned col_cnt, unsigned const* cycle) override;
130 
131         void display_index(unsigned idx, interval const & i, std::ostream& out) const override;
132 
133         void mk_intersect(unsigned idx, interval const& i);
134 
135     };
136 
137 };
138 
139 
140