blob: d502c5ecb0d91b80cc590cf5ea78b9fa07b3e505 (
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
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
|
# kinds -*- sh -*-
#
# For documentation on this file format, please refer to
# src/theory/builtin/kinds.
#
theory THEORY_BV ::CVC4::theory::bv::TheoryBV "theory/bv/theory_bv.h"
typechecker "theory/bv/theory_bv_type_rules.h"
properties finite
properties check propagate
rewriter ::CVC4::theory::bv::TheoryBVRewriter "theory/bv/theory_bv_rewriter.h"
constant BITVECTOR_TYPE \
::CVC4::BitVectorSize \
"::CVC4::UnsignedHashStrategy< ::CVC4::BitVectorSize >" \
"util/bitvector.h" \
"bit-vector type"
cardinality BITVECTOR_TYPE \
"::CVC4::theory::bv::CardinalityComputer::computeCardinality(%TYPE%)" \
"theory/bv/theory_bv_type_rules.h"
constant CONST_BITVECTOR \
::CVC4::BitVector \
::CVC4::BitVectorHashStrategy \
"util/bitvector.h" \
"a fixed-width bit-vector constant"
operator BITVECTOR_CONCAT 2: "bit-vector concatenation"
operator BITVECTOR_AND 2 "bitwise and"
operator BITVECTOR_OR 2 "bitwise or"
operator BITVECTOR_XOR 2 "bitwise xor"
operator BITVECTOR_NOT 1 "bitwise not"
operator BITVECTOR_NAND 2 "bitwise nand"
operator BITVECTOR_NOR 2 "bitwise nor"
operator BITVECTOR_XNOR 2 "bitwise xnor"
operator BITVECTOR_COMP 2 "equality comparison (returns one bit)"
operator BITVECTOR_MULT 2 "bit-vector multiplication"
operator BITVECTOR_PLUS 2 "bit-vector addition"
operator BITVECTOR_SUB 2 "bit-vector subtraction"
operator BITVECTOR_NEG 1 "bit-vector unary negation"
operator BITVECTOR_UDIV 2 "bit-vector unsigned division, truncating towards 0 (undefined if divisor is 0)"
operator BITVECTOR_UREM 2 "bit-vector unsigned remainder from truncating division (undefined if divisor is 0)"
operator BITVECTOR_SDIV 2 "bit-vector 2's complement signed division"
operator BITVECTOR_SREM 2 "bit-vector 2's complement signed remainder (sign follows dividend)"
operator BITVECTOR_SMOD 2 "bit-vector 2's complement signed remainder (sign follows divisor)"
operator BITVECTOR_SHL 2 "bit-vector left shift"
operator BITVECTOR_LSHR 2 "bit-vector logical shift right"
operator BITVECTOR_ASHR 2 "bit-vector arithmetic shift right"
operator BITVECTOR_ULT 2 "bit-vector unsigned less than"
operator BITVECTOR_ULE 2 "bit-vector unsigned less than or equal"
operator BITVECTOR_UGT 2 "bit-vector unsigned greater than"
operator BITVECTOR_UGE 2 "bit-vector unsigned greater than or equal"
operator BITVECTOR_SLT 2 "bit-vector signed less than"
operator BITVECTOR_SLE 2 "bit-vector signed less than or equal"
operator BITVECTOR_SGT 2 "bit-vector signed greater than"
operator BITVECTOR_SGE 2 "signed greater than or equal"
constant BITVECTOR_EXTRACT_OP \
::CVC4::BitVectorExtract \
::CVC4::BitVectorExtractHashStrategy \
"util/bitvector.h" \
"operator for the bit-vector extract"
constant BITVECTOR_REPEAT_OP \
::CVC4::BitVectorRepeat \
"::CVC4::UnsignedHashStrategy< ::CVC4::BitVectorRepeat >" \
"util/bitvector.h" \
"operator for the bit-vector repeat"
constant BITVECTOR_ZERO_EXTEND_OP \
::CVC4::BitVectorZeroExtend \
"::CVC4::UnsignedHashStrategy< ::CVC4::BitVectorZeroExtend >" \
"util/bitvector.h" \
"operator for the bit-vector zero-extend"
constant BITVECTOR_SIGN_EXTEND_OP \
::CVC4::BitVectorSignExtend \
"::CVC4::UnsignedHashStrategy< ::CVC4::BitVectorSignExtend >" \
"util/bitvector.h" \
"operator for the bit-vector sign-extend"
constant BITVECTOR_ROTATE_LEFT_OP \
::CVC4::BitVectorRotateLeft \
"::CVC4::UnsignedHashStrategy< ::CVC4::BitVectorRotateLeft >" \
"util/bitvector.h" \
"operator for the bit-vector rotate left"
constant BITVECTOR_ROTATE_RIGHT_OP \
::CVC4::BitVectorRotateRight \
"::CVC4::UnsignedHashStrategy< ::CVC4::BitVectorRotateRight >" \
"util/bitvector.h" \
"operator for the bit-vector rotate right"
parameterized BITVECTOR_EXTRACT BITVECTOR_EXTRACT_OP 1 "bit-vector extract"
parameterized BITVECTOR_REPEAT BITVECTOR_REPEAT_OP 1 "bit-vector repeat"
parameterized BITVECTOR_ZERO_EXTEND BITVECTOR_ZERO_EXTEND_OP 1 "bit-vector zero-extend"
parameterized BITVECTOR_SIGN_EXTEND BITVECTOR_SIGN_EXTEND_OP 1 "bit-vector sign-extend"
parameterized BITVECTOR_ROTATE_LEFT BITVECTOR_ROTATE_LEFT_OP 1 "bit-vector rotate left"
parameterized BITVECTOR_ROTATE_RIGHT BITVECTOR_ROTATE_RIGHT_OP 1 "bit-vector rotate right"
typerule CONST_BITVECTOR ::CVC4::theory::bv::BitVectorConstantTypeRule
typerule BITVECTOR_AND ::CVC4::theory::bv::BitVectorFixedWidthTypeRule
typerule BITVECTOR_OR ::CVC4::theory::bv::BitVectorFixedWidthTypeRule
typerule BITVECTOR_XOR ::CVC4::theory::bv::BitVectorFixedWidthTypeRule
typerule BITVECTOR_NOT ::CVC4::theory::bv::BitVectorFixedWidthTypeRule
typerule BITVECTOR_NAND ::CVC4::theory::bv::BitVectorFixedWidthTypeRule
typerule BITVECTOR_NOR ::CVC4::theory::bv::BitVectorFixedWidthTypeRule
typerule BITVECTOR_XNOR ::CVC4::theory::bv::BitVectorFixedWidthTypeRule
typerule BITVECTOR_COMP ::CVC4::theory::bv::BitVectorCompRule
typerule BITVECTOR_MULT ::CVC4::theory::bv::BitVectorArithRule
typerule BITVECTOR_PLUS ::CVC4::theory::bv::BitVectorArithRule
typerule BITVECTOR_SUB ::CVC4::theory::bv::BitVectorArithRule
typerule BITVECTOR_NEG ::CVC4::theory::bv::BitVectorArithRule
typerule BITVECTOR_UDIV ::CVC4::theory::bv::BitVectorFixedWidthTypeRule
typerule BITVECTOR_UREM ::CVC4::theory::bv::BitVectorFixedWidthTypeRule
typerule BITVECTOR_SDIV ::CVC4::theory::bv::BitVectorFixedWidthTypeRule
typerule BITVECTOR_SREM ::CVC4::theory::bv::BitVectorFixedWidthTypeRule
typerule BITVECTOR_SMOD ::CVC4::theory::bv::BitVectorFixedWidthTypeRule
typerule BITVECTOR_SHL ::CVC4::theory::bv::BitVectorFixedWidthTypeRule
typerule BITVECTOR_LSHR ::CVC4::theory::bv::BitVectorFixedWidthTypeRule
typerule BITVECTOR_ASHR ::CVC4::theory::bv::BitVectorFixedWidthTypeRule
typerule BITVECTOR_ROTATE_LEFT ::CVC4::theory::bv::BitVectorFixedWidthTypeRule
typerule BITVECTOR_ROTATE_RIGHT ::CVC4::theory::bv::BitVectorFixedWidthTypeRule
typerule BITVECTOR_ULT ::CVC4::theory::bv::BitVectorPredicateTypeRule
typerule BITVECTOR_ULE ::CVC4::theory::bv::BitVectorPredicateTypeRule
typerule BITVECTOR_UGT ::CVC4::theory::bv::BitVectorPredicateTypeRule
typerule BITVECTOR_UGE ::CVC4::theory::bv::BitVectorPredicateTypeRule
typerule BITVECTOR_SLT ::CVC4::theory::bv::BitVectorPredicateTypeRule
typerule BITVECTOR_SLE ::CVC4::theory::bv::BitVectorPredicateTypeRule
typerule BITVECTOR_SGT ::CVC4::theory::bv::BitVectorPredicateTypeRule
typerule BITVECTOR_SGE ::CVC4::theory::bv::BitVectorPredicateTypeRule
typerule BITVECTOR_EXTRACT ::CVC4::theory::bv::BitVectorExtractTypeRule
typerule BITVECTOR_CONCAT ::CVC4::theory::bv::BitVectorConcatRule
typerule BITVECTOR_REPEAT ::CVC4::theory::bv::BitVectorRepeatTypeRule
typerule BITVECTOR_ZERO_EXTEND ::CVC4::theory::bv::BitVectorExtendTypeRule
typerule BITVECTOR_SIGN_EXTEND ::CVC4::theory::bv::BitVectorExtendTypeRule
endtheory
|
