re-organize muz_qe into separate units

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

src/muz/rel/dl_interval_relation.cpp

@@ -0,0 +1,653 @@
+/*++
+Copyright (c) 2010 Microsoft Corporation
+
+Module Name:
+
+    dl_interval_relation.cpp
+
+Abstract:
+
+    Basic interval reatlion.
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2010-2-11
+
+Revision History:
+
+--*/
+
+#include "debug.h"
+#include "optional.h"
+#include "ast_pp.h"
+#include "dl_interval_relation.h"
+#include "dl_relation_manager.h"
+#include "bool_rewriter.h"
+
+
+namespace datalog {
+    // -------------------------
+    // interval_relation_plugin
+
+    interval_relation_plugin::interval_relation_plugin(relation_manager& m):
+        relation_plugin(interval_relation_plugin::get_name(), m), 
+        m_empty(m_dep),
+        m_arith(get_ast_manager()) {
+    }
+
+    bool interval_relation_plugin::can_handle_signature(const relation_signature & sig) {
+        for (unsigned i = 0; i < sig.size(); ++i) {
+            if (!m_arith.is_int(sig[i]) && !m_arith.is_real(sig[i])) {
+                return false;
+            }
+        }
+        return true;
+    }
+
+
+    relation_base * interval_relation_plugin::mk_empty(const relation_signature & s) {
+        return alloc(interval_relation, *this, s, true);
+    }
+
+    relation_base * interval_relation_plugin::mk_full(func_decl* p, const relation_signature & s) {        
+        return alloc(interval_relation, *this, s, false);
+    }
+
+    class interval_relation_plugin::join_fn : public convenient_relation_join_fn {
+    public:
+        join_fn(const relation_signature & o1_sig, const relation_signature & o2_sig, unsigned col_cnt,
+                const unsigned * cols1, const unsigned * cols2) 
+            : convenient_relation_join_fn(o1_sig, o2_sig, col_cnt, cols1, cols2){
+        }
+
+        virtual relation_base * operator()(const relation_base & _r1, const relation_base & _r2) {
+            interval_relation const& r1 = get(_r1);
+            interval_relation const& r2 = get(_r2);
+            interval_relation_plugin& p = r1.get_plugin();
+            interval_relation* result = dynamic_cast<interval_relation*>(p.mk_full(0, get_result_signature()));            
+            result->mk_join(r1, r2, m_cols1.size(), m_cols1.c_ptr(), m_cols2.c_ptr());
+            return result;
+        }
+    };
+
+    relation_join_fn * interval_relation_plugin::mk_join_fn(const relation_base & r1, const relation_base & r2,
+            unsigned col_cnt, const unsigned * cols1, const unsigned * cols2) {
+        if (!check_kind(r1) || !check_kind(r2)) {
+            return 0;
+        }
+        return alloc(join_fn, r1.get_signature(), r2.get_signature(), col_cnt, cols1, cols2);
+    }
+
+
+    class interval_relation_plugin::project_fn : public convenient_relation_project_fn {
+    public:
+        project_fn(const relation_signature & orig_sig, unsigned removed_col_cnt, const unsigned * removed_cols) 
+            : convenient_relation_project_fn(orig_sig, removed_col_cnt, removed_cols) {
+        }
+
+        virtual relation_base * operator()(const relation_base & _r) {
+            interval_relation const& r = get(_r);
+            interval_relation_plugin& p = r.get_plugin();
+            interval_relation* result = dynamic_cast<interval_relation*>(p.mk_full(0, get_result_signature()));            
+            result->mk_project(r, m_removed_cols.size(), m_removed_cols.c_ptr());
+            return result;
+        }
+    };
+
+    relation_transformer_fn * interval_relation_plugin::mk_project_fn(const relation_base & r, 
+            unsigned col_cnt, const unsigned * removed_cols) {
+        return alloc(project_fn, r.get_signature(), col_cnt, removed_cols);
+    }
+   
+    class interval_relation_plugin::rename_fn : public convenient_relation_rename_fn {
+    public:
+        rename_fn(const relation_signature & orig_sig, unsigned cycle_len, const unsigned * cycle) 
+            : convenient_relation_rename_fn(orig_sig, cycle_len, cycle) {
+        }
+
+        virtual relation_base * operator()(const relation_base & _r) {
+            interval_relation const& r = get(_r);
+            interval_relation_plugin& p = r.get_plugin();
+            interval_relation* result = dynamic_cast<interval_relation*>(p.mk_full(0, get_result_signature()));
+            result->mk_rename(r, m_cycle.size(), m_cycle.c_ptr());
+            return result;
+        }
+    };
+
+    relation_transformer_fn * interval_relation_plugin::mk_rename_fn(const relation_base & r, 
+            unsigned cycle_len, const unsigned * permutation_cycle) {
+        if(!check_kind(r)) {
+            return 0;
+        }
+        return alloc(rename_fn, r.get_signature(), cycle_len, permutation_cycle);
+    }
+     
+    interval interval_relation_plugin::unite(interval const& src1, interval const& src2) {
+        bool l_open = src1.is_lower_open();
+        bool r_open = src1.is_upper_open();
+        ext_numeral low = src1.inf();
+        ext_numeral high = src1.sup();
+        if (src2.inf() < low || (src2.inf() == low && l_open)) {
+            low = src2.inf();
+            l_open = src2.is_lower_open();
+        }
+        if (src2.sup() > high || (src2.sup() == high && r_open)) {
+            high = src2.sup();
+            r_open = src2.is_upper_open();
+        }
+        return interval(dep(), low, l_open, 0, high, r_open, 0);
+    }
+
+    interval interval_relation_plugin::widen(interval const& src1, interval const& src2) {
+        bool l_open = src1.is_lower_open();
+        bool r_open = src1.is_upper_open();
+        ext_numeral low = src1.inf();
+        ext_numeral high = src1.sup();
+        
+        if (src2.inf() < low || (low == src2.inf() && l_open && !src2.is_lower_open())) {
+            low = ext_numeral(false);
+            l_open = true;
+        }
+        if (high < src2.sup() || (src2.sup() == high && !r_open && src2.is_upper_open())) {
+            high = ext_numeral(true);
+            r_open = true;
+        }
+        return interval(dep(), low, l_open, 0, high, r_open, 0);
+    }
+
+    interval interval_relation_plugin::meet(interval const& src1, interval const& src2, bool& isempty) {
+        isempty = false;
+        if (is_empty(0, src1) || is_infinite(src2)) {
+            return src1;
+        }
+        if (is_empty(0, src2) || is_infinite(src1)) {
+            return src2;
+        }
+        bool l_open = src1.is_lower_open();
+        bool r_open = src1.is_upper_open();
+        ext_numeral low = src1.inf();
+        ext_numeral high = src1.sup();
+        if (src2.inf() > low || (src2.inf() == low && !l_open)) {
+            low = src2.inf();
+            l_open = src2.is_lower_open();
+        }
+        if (src2.sup() < high || (src2.sup() == high && !r_open)) {
+            high = src2.sup();
+            r_open = src2.is_upper_open();
+        }
+        if (low > high || (low == high && (l_open || r_open))) {
+            isempty = true;
+            return interval(dep());
+        }
+        else {
+            return interval(dep(), low, l_open, 0, high, r_open, 0);
+        }
+    }
+    
+    bool interval_relation_plugin::is_infinite(interval const& i) {
+        return i.plus_infinity() && i.minus_infinity();
+    }
+
+    bool interval_relation_plugin::is_empty(unsigned, interval const& i) {
+        return i.sup() < i.inf();
+    }
+
+    class interval_relation_plugin::union_fn : public relation_union_fn {
+        bool                      m_is_widen;
+    public:
+        union_fn(bool is_widen) :
+            m_is_widen(is_widen) {            
+        }
+
+        virtual void operator()(relation_base & _r, const relation_base & _src, relation_base * _delta) {
+
+            TRACE("interval_relation", _r.display(tout << "dst:\n"); _src.display(tout  << "src:\n"););
+
+            interval_relation& r = get(_r);
+            interval_relation const& src = get(_src);
+            if (_delta) {
+                interval_relation& d = get(*_delta);
+                r.mk_union(src, &d, m_is_widen);
+            }
+            else {
+                r.mk_union(src, 0, m_is_widen);
+            }            
+        }
+    };
+
+    relation_union_fn * interval_relation_plugin::mk_union_fn(const relation_base & tgt, const relation_base & src,
+        const relation_base * delta) {
+        if (!check_kind(tgt) || !check_kind(src) || (delta && !check_kind(*delta))) {
+            return 0;
+        }
+        return alloc(union_fn, false);
+    }
+
+    relation_union_fn * interval_relation_plugin::mk_widen_fn(
+        const relation_base & tgt, const relation_base & src, 
+        const relation_base * delta) {
+        if (!check_kind(tgt) || !check_kind(src) || (delta && !check_kind(*delta))) {
+            return 0;
+        }
+        return alloc(union_fn, true);
+    }
+
+    class interval_relation_plugin::filter_identical_fn : public relation_mutator_fn {
+        unsigned_vector m_identical_cols;
+    public:
+        filter_identical_fn(unsigned col_cnt, const unsigned * identical_cols) 
+            : m_identical_cols(col_cnt, identical_cols) {}
+
+        virtual void operator()(relation_base & r) {
+            interval_relation & pr = get(r);
+            for (unsigned i = 1; i < m_identical_cols.size(); ++i) {
+                unsigned c1 = m_identical_cols[0];
+                unsigned c2 = m_identical_cols[i];
+                pr.equate(c1, c2);
+            }
+        }
+    };
+
+    relation_mutator_fn * interval_relation_plugin::mk_filter_identical_fn(
+        const relation_base & t, unsigned col_cnt, const unsigned * identical_cols) {
+        if(!check_kind(t)) {
+            return 0;
+        }
+        return alloc(filter_identical_fn, col_cnt, identical_cols);
+    }
+
+
+    class interval_relation_plugin::filter_equal_fn : public relation_mutator_fn {
+        unsigned m_col;
+        rational m_value;
+    public:
+        filter_equal_fn(relation_manager & m, const relation_element & value, unsigned col) 
+            : m_col(col) {
+            arith_util arith(m.get_context().get_manager());
+            VERIFY(arith.is_numeral(value, m_value));            
+        }
+
+        virtual void operator()(relation_base & _r) {
+            interval_relation & r = get(_r);
+            interval_relation_plugin & p = r.get_plugin();
+            r.mk_intersect(m_col, interval(p.dep(), m_value));
+            TRACE("interval_relation", tout << m_value << "\n"; r.display(tout););            
+        }
+    };
+
+    relation_mutator_fn * interval_relation_plugin::mk_filter_equal_fn(const relation_base & r, 
+        const relation_element & value, unsigned col) {
+        if(check_kind(r)) {
+            return alloc(filter_equal_fn, get_manager(), value, col);
+        }
+        return 0;
+    }
+
+
+    class interval_relation_plugin::filter_interpreted_fn : public relation_mutator_fn {
+        app_ref m_cond;
+    public:
+        filter_interpreted_fn(interval_relation const& t, app* cond):
+            m_cond(cond, t.get_plugin().get_ast_manager()) {
+        }
+
+        void operator()(relation_base& t) {
+            get(t).filter_interpreted(m_cond);
+            TRACE("interval_relation", tout << mk_pp(m_cond, m_cond.get_manager()) << "\n"; t.display(tout););
+        }
+    };
+
+    relation_mutator_fn * interval_relation_plugin::mk_filter_interpreted_fn(const relation_base & t, app * condition) {
+        if (check_kind(t)) {
+            return alloc(filter_interpreted_fn, get(t), condition);
+        }
+        return 0;
+    }
+
+    interval_relation& interval_relation_plugin::get(relation_base& r) {
+        return dynamic_cast<interval_relation&>(r);
+    }
+
+    interval_relation const & interval_relation_plugin::get(relation_base const& r) {
+        return dynamic_cast<interval_relation const&>(r);
+    }
+
+    // -----------------------
+    // interval_relation
+
+    interval_relation::interval_relation(interval_relation_plugin& p, relation_signature const& s, bool is_empty):
+        vector_relation<interval>(p, s, is_empty, interval(p.dep())) 
+    {
+        TRACE("interval_relation", tout << s.size() << "\n";);
+    }    
+
+    void interval_relation::add_fact(const relation_fact & f) {
+        interval_relation r(get_plugin(), get_signature(), false);
+        ast_manager& m = get_plugin().get_ast_manager();        
+        for (unsigned i = 0; i < f.size(); ++i) {
+            app_ref eq(m);
+            expr* e = f[i];
+            eq = m.mk_eq(m.mk_var(i, m.get_sort(e)), e);
+            r.filter_interpreted(eq.get());
+        }            
+        mk_union(r, 0, false);
+    }
+
+    bool interval_relation::contains_fact(const relation_fact & f) const {
+        SASSERT(f.size() == get_signature().size());
+        interval_relation_plugin& p = get_plugin();
+
+        for (unsigned i = 0; i < f.size(); ++i) {
+            if (f[i] != f[find(i)]) {
+                return false;
+            }
+            interval const& iv = (*this)[i];
+            if (p.is_infinite(iv)) {
+                continue;
+            }
+            rational v;
+            if (p.m_arith.is_numeral(f[i], v)) {
+                if (!iv.contains(v)) {
+                    return false;
+                }
+            }
+            else {
+                // TBD: may or must?
+            }
+        }
+        return true;
+    }
+
+    interval_relation * interval_relation::clone() const {
+        interval_relation* result = alloc(interval_relation, get_plugin(), get_signature(), empty());
+        result->copy(*this);
+        return result;
+    }
+
+    interval_relation * interval_relation::complement(func_decl*) const {
+        UNREACHABLE();
+        return 0;
+    }
+
+    void interval_relation::to_formula(expr_ref& fml) const {
+        ast_manager& m = get_plugin().get_ast_manager();
+        arith_util& arith = get_plugin().m_arith;
+        expr_ref_vector conjs(m);
+        relation_signature const& sig = get_signature();
+        for (unsigned i = 0; i < sig.size(); ++i) {
+            if (i != find(i)) {
+                conjs.push_back(m.mk_eq(m.mk_var(i, sig[i]), 
+                                        m.mk_var(find(i), sig[find(i)])));
+                continue;
+            }            
+            interval const& iv = (*this)[i];
+            sort* ty = sig[i];
+            expr_ref var(m.mk_var(i, ty), m);
+            if (!iv.minus_infinity()) {
+                expr* lo = arith.mk_numeral(iv.get_lower_value(), ty);
+                if (iv.is_lower_open()) {
+                    conjs.push_back(arith.mk_lt(lo, var));
+                }
+                else {
+                    conjs.push_back(arith.mk_le(lo, var));
+                }
+            }
+            if (!iv.plus_infinity()) {
+                expr* hi = arith.mk_numeral(iv.get_upper_value(), ty);
+                if (iv.is_upper_open()) {
+                    conjs.push_back(arith.mk_lt(var, hi));
+                }
+                else {
+                    conjs.push_back(arith.mk_le(var, hi));
+                }
+            }
+        }
+        bool_rewriter br(m);
+        br.mk_and(conjs.size(), conjs.c_ptr(), fml);
+    }
+
+
+    void interval_relation::display_index(unsigned i, interval const& j, std::ostream & out) const {
+        out << i << " in " << j << "\n";                
+    }
+
+    interval_relation_plugin& interval_relation::get_plugin() const {
+        return static_cast<interval_relation_plugin &>(relation_base::get_plugin());        
+    }
+
+    void interval_relation::mk_intersect(unsigned idx, interval const& i) {
+        bool isempty;
+        (*this)[idx] = mk_intersect((*this)[idx], i, isempty);
+        if (isempty || is_empty(idx, (*this)[idx])) {
+            set_empty();
+        }
+    }
+
+    void interval_relation::mk_rename_elem(interval& i, unsigned, unsigned const* ) {
+
+    }
+
+    void interval_relation::filter_interpreted(app* cond) {
+        interval_relation_plugin& p = get_plugin();
+        rational k;
+        unsigned x, y;
+        if (p.is_lt(cond, x, k, y)) {
+            // 0 < x - y + k
+            if (x == UINT_MAX) {
+                // y < k
+                mk_intersect(y, interval(p.dep(), k, true, false, 0));
+                return;
+            }
+            if (y == UINT_MAX) {
+                // -k < x
+                mk_intersect(x, interval(p.dep(), -k, true, true, 0));
+                return;
+            }
+            // y < x + k
+            ext_numeral x_hi = (*this)[x].sup();
+            ext_numeral y_lo = (*this)[y].inf();
+            if (!x_hi.is_infinite()) {
+                mk_intersect(y, interval(p.dep(), k + x_hi.to_rational(), true, false, 0));
+            }
+            if (!y_lo.is_infinite()) {
+                mk_intersect(x, interval(p.dep(), y_lo.to_rational() - k, true, true, 0));
+            }
+            return;
+        }
+        bool is_int = false;
+        if (p.is_le(cond, x, k, y, is_int)) {
+            // 0 <= x - y + k
+            if (x == UINT_MAX) {
+                // y <= k
+                mk_intersect(y, interval(p.dep(), k, false, false, 0));
+                return;
+            }
+            if (y == UINT_MAX) {
+                // -k <= x
+                mk_intersect(x, interval(p.dep(), -k, false, true, 0));
+                return;
+            }
+            ext_numeral x_hi = (*this)[x].sup();
+            ext_numeral y_lo = (*this)[y].inf();
+            if (!x_hi.is_infinite()) {
+                mk_intersect(y, interval(p.dep(), k + x_hi.to_rational(), false, false, 0));
+            }
+            if (!y_lo.is_infinite()) {
+                mk_intersect(x, interval(p.dep(), y_lo.to_rational() - k, false, true, 0));
+            }
+            return;
+        }
+        if (p.is_eq(cond, x, k, y)) {
+            // y = x + k
+            if (x == UINT_MAX) {
+                SASSERT(y != UINT_MAX);
+                mk_intersect(y, interval(p.dep(), k));
+                return;
+            }
+            if (y == UINT_MAX) {
+                // x = - k
+                SASSERT(x != UINT_MAX);
+                mk_intersect(x, interval(p.dep(), -k));
+                return;
+            }
+            interval x_i = (*this)[x];
+            interval y_i = (*this)[y];
+            x_i += interval(p.dep(), k);
+            y_i -= interval(p.dep(), k);
+            mk_intersect(x, y_i);
+            mk_intersect(y, x_i);
+        }
+        if (get_plugin().get_ast_manager().is_false(cond)) {
+            set_empty();
+        }
+    }
+
+    bool interval_relation_plugin::is_linear(expr* e, unsigned& neg, unsigned& pos, rational& k, bool is_pos) const {
+#define SET_VAR(_idx_)                              \
+            if (is_pos &&pos == UINT_MAX) {         \
+                pos = _idx_;                        \
+                return true;                        \
+            }                                       \
+            if (!is_pos && neg == UINT_MAX) {       \
+                neg = _idx_;                        \
+                return true;                        \
+            }                                       \
+            else {                                  \
+                return false;                       \
+            }                   
+
+        if (is_var(e)) {
+            SET_VAR(to_var(e)->get_idx());
+        }
+        if (!is_app(e)) {
+            return false;
+        }
+        app* a = to_app(e);
+ 
+        if (m_arith.is_add(e)) {
+            for (unsigned i = 0; i < a->get_num_args(); ++i) {
+                if (!is_linear(a->get_arg(i), neg, pos, k, is_pos)) return false;
+            }
+            return true;
+        }
+        if (m_arith.is_sub(e)) {
+            SASSERT(a->get_num_args() == 2);
+            return 
+                is_linear(a->get_arg(0), neg, pos, k, is_pos) &&
+                is_linear(a->get_arg(1), neg, pos, k, !is_pos);
+        }
+        rational k1;
+        SASSERT(!m_arith.is_mul(e) || a->get_num_args() == 2);
+        if (m_arith.is_mul(e) &&
+            m_arith.is_numeral(a->get_arg(0), k1) && 
+            k1.is_minus_one() &&
+            is_var(a->get_arg(1))) {
+            SET_VAR(to_var(a->get_arg(1))->get_idx());                
+        }
+        
+        if (m_arith.is_numeral(e, k1)) {
+            if (is_pos) {
+                k += k1;
+            }
+            else {
+                k -= k1;
+            }
+            return true;
+        }
+        return false;
+    }
+
+    // 0 <= x - y + k
+    bool interval_relation_plugin::is_le(app* cond, unsigned& x, rational& k, unsigned& y, bool& is_int) const {
+        ast_manager& m = get_ast_manager();
+        k.reset();
+        x = UINT_MAX;
+        y = UINT_MAX;
+
+        if (m_arith.is_le(cond)) {
+            is_int = m_arith.is_int(cond->get_arg(0));
+            if (!is_linear(cond->get_arg(0), y, x, k, false)) return false;
+            if (!is_linear(cond->get_arg(1), y, x, k, true)) return false;
+            return (x != UINT_MAX || y != UINT_MAX);
+        }
+        if (m_arith.is_ge(cond)) {
+            is_int = m_arith.is_int(cond->get_arg(0));
+            if (!is_linear(cond->get_arg(0), y, x, k, true)) return false;
+            if (!is_linear(cond->get_arg(1), y, x, k, false)) return false;
+            return (x != UINT_MAX || y != UINT_MAX);
+        }
+        if (m_arith.is_lt(cond) && m_arith.is_int(cond->get_arg(0))) {
+            is_int = true;
+            if (!is_linear(cond->get_arg(0), y, x, k, false)) return false;
+            if (!is_linear(cond->get_arg(1), y, x, k, true)) return false;
+            k -= rational::one();
+            return (x != UINT_MAX || y != UINT_MAX);
+        }
+        if (m_arith.is_gt(cond) && m_arith.is_int(cond->get_arg(0))) {
+            is_int = true;
+            if (!is_linear(cond->get_arg(0), y, x, k, true)) return false;
+            if (!is_linear(cond->get_arg(1), y, x, k, false)) return false;
+            k += rational::one();
+            return (x != UINT_MAX || y != UINT_MAX);
+        }
+        if (m.is_not(cond) && is_app(cond->get_arg(0))) {
+            //     not (0 <= x - y + k) 
+            // <=>
+            //     0 > x - y + k
+            // <=>
+            //     0 <= y - x - k - 1
+            if (is_le(to_app(cond->get_arg(0)), x, k, y, is_int) && is_int) {
+                k.neg();
+                k -= rational::one();
+                std::swap(x, y);
+                return true;
+            }
+            //     not (0 < x - y + k) 
+            // <=>
+            //     0 >= x - y + k
+            // <=>
+            //     0 <= y - x - k 
+            if (is_lt(to_app(cond->get_arg(0)), x, k, y)) {
+                is_int = false;
+                k.neg();
+                std::swap(x, y);
+                return true;
+            }
+        }
+        return false;
+    }
+
+    // 0 < x - y + k
+    bool interval_relation_plugin::is_lt(app* cond, unsigned& x, rational& k, unsigned& y) const {
+        k.reset();
+        x = UINT_MAX;
+        y = UINT_MAX;
+        if (m_arith.is_lt(cond) && m_arith.is_real(cond->get_arg(0))) {
+            if (!is_linear(cond->get_arg(0), y, x, k, false)) return false;
+            if (!is_linear(cond->get_arg(1), y, x, k, true)) return false;
+            return (x != UINT_MAX || y != UINT_MAX);
+        }
+        if (m_arith.is_gt(cond) && m_arith.is_real(cond->get_arg(0))) {
+            if (!is_linear(cond->get_arg(0), y, x, k, true)) return false;
+            if (!is_linear(cond->get_arg(1), y, x, k, false)) return false;
+            return (x != UINT_MAX || y != UINT_MAX);
+        }
+        return false;
+    }
+
+    // 0 = x - y + k 
+    bool interval_relation_plugin::is_eq(app* cond, unsigned& x, rational& k, unsigned& y) const {
+        ast_manager& m = get_ast_manager();
+        k.reset();
+        x = UINT_MAX;
+        y = UINT_MAX;
+        if (m.is_eq(cond)) {
+            if (!is_linear(cond->get_arg(0), y, x, k, false)) return false;
+            if (!is_linear(cond->get_arg(1), y, x, k, true)) return false;
+            return (x != UINT_MAX || y != UINT_MAX);
+        }
+        return false;
+    }
+
+};
+