# 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"
typechecker "theory/arrays/theory_arrays_type_rules.h"

properties polite stable-infinite parametric
properties check propagate presolve getNextDecisionRequest

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

operator ARRAY_TYPE 2 "array type"
cardinality ARRAY_TYPE \
    "::CVC4::theory::arrays::ArraysProperties::computeCardinality(%TYPE%)" \
    "theory/arrays/theory_arrays_type_rules.h"
well-founded ARRAY_TYPE \
    "::CVC4::theory::arrays::ArraysProperties::isWellFounded(%TYPE%)" \
    "::CVC4::theory::arrays::ArraysProperties::mkGroundTerm(%TYPE%)" \
    "theory/arrays/theory_arrays_type_rules.h"

enumerator ARRAY_TYPE \
    "::CVC4::theory::arrays::ArrayEnumerator" \
    "theory/arrays/type_enumerator.h"

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

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

# storeall t e  is  \all i in indexType(t) <= e
constant STORE_ALL \
    ::CVC4::ArrayStoreAll \
    ::CVC4::ArrayStoreAllHashFunction \
    "util/array_store_all.h" \
    "array store-all"

# used internally by array theory
operator ARR_TABLE_FUN 4 "array table function (internal symbol)"

typerule SELECT ::CVC4::theory::arrays::ArraySelectTypeRule
typerule STORE ::CVC4::theory::arrays::ArrayStoreTypeRule
typerule STORE_ALL ::CVC4::theory::arrays::ArrayStoreTypeRule
typerule ARR_TABLE_FUN ::CVC4::theory::arrays::ArrayTableFunTypeRule

# store operations that are ordered (by index) over a store-all are constant
construle STORE ::CVC4::theory::arrays::ArrayStoreTypeRule

endtheory