blob: 1adbdb0b22782e0b702094d2a784dca7b121e85f (
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
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
|
# kinds -*- sh -*-
#
# For documentation on this file format, please refer to
# src/theory/builtin/kinds.
#
theory THEORY_ARRAYS ::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
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; first parameter is an array term, second is the selection index"
# store a i e is a[i] <= e
operator STORE 3 "array store; first parameter is an array term, second is the store index, third is the term to store at the index"
# storeall t e is \all i in indexType(t) <= e
constant STORE_ALL \
::CVC4::ArrayStoreAll \
::CVC4::ArrayStoreAllHashFunction \
"expr/array_store_all.h" \
"array store-all; payload is an instance of the CVC4::ArrayStoreAll class (this is not supported by arrays decision procedure yet, but it is used for returned array models)"
# used internally by array theory
operator ARR_TABLE_FUN 4 "array table function (internal-only symbol)"
# used internally for substitutions in models (e.g. the Boolean terms converter)
# The (single) argument is a lambda(x:T):U. Type of the array lambda is
# Array T of U. Thus ARRAY_LAMBDA LAMBDA(x:INT) . (read a x) is the same array
# as a. ARRAY_LAMBDA LAMBDA(x:INT) . (read a (- x 1)) is the same array as
# as a shifted over one.
operator ARRAY_LAMBDA 1 "array lambda (internal-only 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
typerule ARRAY_LAMBDA ::CVC4::theory::arrays::ArrayLambdaTypeRule
operator PARTIAL_SELECT_0 0:2 "partial array select, for internal use only"
operator PARTIAL_SELECT_1 0:2 "partial array select, for internal use only"
typerule PARTIAL_SELECT_0 ::CVC4::theory::arrays::ArrayPartialSelectTypeRule
typerule PARTIAL_SELECT_1 ::CVC4::theory::arrays::ArrayPartialSelectTypeRule
# store operations that are ordered (by index) over a store-all are constant
construle STORE ::CVC4::theory::arrays::ArrayStoreTypeRule
endtheory
|
