blob: 195a600355672ac463fa22413c794cfc39444e64 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
|
# 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"
instantiator ::CVC4::theory::arrays::InstantiatorTheoryArrays "theory/arrays/theory_arrays_instantiator.h"
properties polite stable-infinite parametric
properties check propagate presolve
rewriter ::CVC4::theory::arrays::TheoryArraysRewriter "theory/arrays/theory_arrays_rewriter.h"
operator ARRAY_TYPE 2 "array type"
cardinality ARRAY_TYPE \
"::CVC4::theory::arrays::CardinalityComputer::computeCardinality(%TYPE%)" \
"theory/arrays/theory_arrays_type_rules.h"
well-founded ARRAY_TYPE false
# select a i is a[i]
operator SELECT 2 "array select"
# store a i e is a[i] <= e
operator STORE 3 "array store"
# used internally by array theory
operator ARR_TABLE_FUN 4 "array table function"
typerule SELECT ::CVC4::theory::arrays::ArraySelectTypeRule
typerule STORE ::CVC4::theory::arrays::ArrayStoreTypeRule
typerule ARR_TABLE_FUN ::CVC4::theory::arrays::ArrayTableFunTypeRule
endtheory
|
