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