text: /*++
  Copyright (c) 2011 Microsoft Corporation
  
  Module Name:
  
      seq_offset_eq.h
  
  Abstract:
  
      Container for maintaining equalities between lengths of sequences.
  
  Author:
  
      Thai Minh Trinh 2017
      Nikolaj Bjorner (nbjorner) 2020-4-16
  
  --*/
  #pragma once
  
  #include "util/obj_pair_hashtable.h"
  #include "ast/seq_decl_plugin.h"
  #include "ast/arith_decl_plugin.h"
  #include "smt/smt_theory.h"
  
  namespace smt {
  
      class seq_offset_eq {
          theory&        th;
          ast_manager&   m;
          seq_util       seq;
          arith_util     a;
          obj_hashtable<enode>             m_has_offset_equality;
          obj_pair_map<enode, enode, int>  m_offset_equalities;
          int                              m_propagation_level;
  
          bool match_x_minus_y(expr* e, expr*& x, expr*& y) const;
          void len_offset(expr* e, int val);
          void prop_arith_to_len_offset();
  
      public:
  
          seq_offset_eq(theory& th, ast_manager& m);
          bool empty() const { return m_offset_equalities.empty(); }
          /**
             \brief determine if r1 = r2 + offset
           */
          bool find(enode* r1, enode* r2, int& offset) const;
          bool contains(enode* r1, enode* r2) const { int offset = 0; return find(r1, r2, offset); }
          bool contains(enode* r);
          bool propagate();
          void pop_scope_eh(unsigned num_scopes);
      };
  
  };
  
  