# kinds                                                               -*- sh -*-
#
# For documentation on this file format, please refer to
# src/theory/builtin/kinds.
#

theory THEORY_ARRAY ::CVC4::theory::arrays::TheoryArrays "theory/arrays/theory_arrays.h"

properties polite stable-infinite 

rewriter ::CVC4::theory::arrays::TheoryArraysRewriter "theory/arrays/theory_arrays_rewriter.h"

operator ARRAY_TYPE 2 "array type"

# select a i  is  a[i]
operator SELECT 2 "array select"

# store a i e  is  a[i] <= e
operator STORE 3 "array store"

endtheory