/*++

Module Name:

    dl_mk_array_eq_rewrite.h

Abstract:
    Selects a representative for array equivalence classes.

Author:

    Julien Braine

Revision History:

--*/

#pragma once

#include "muz/base/dl_rule_transformer.h"

namespace datalog {

    class context;
    class mk_array_eq_rewrite : public rule_transformer::plugin {
       //Context objects
       ast_manager&      m;
       context&          m_ctx;
       array_util        m_a;

       //Rule set context
       const rule_set*   m_src_set;
       rule_set*         m_dst;
       rule_manager*     m_src_manager;
       unsigned          m_cnt;//Index for new variables

       expr* replace(expr* e, expr* new_val, expr* old_val);
       void instantiate_rule(const rule& r, rule_set & dest);

     public:
        mk_array_eq_rewrite(context & ctx, unsigned priority);
        rule_set * operator()(rule_set const & source) override;
        ~mk_array_eq_rewrite() override{}
    };



};