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
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
|
# kinds -*- sh -*-
#
# For documentation on this file format, please refer to
# src/theory/builtin/kinds.
#
theory THEORY_ARITH ::cvc5::theory::arith::TheoryArith "theory/arith/theory_arith.h"
typechecker "theory/arith/theory_arith_type_rules.h"
properties stable-infinite
properties check propagate ppStaticLearn presolve notifyRestart
rewriter ::cvc5::theory::arith::ArithRewriter "theory/arith/arith_rewriter.h"
operator PLUS 2: "arithmetic addition (N-ary)"
operator MULT 2: "arithmetic multiplication (N-ary)"
operator NONLINEAR_MULT 2: "synonym for MULT"
operator MINUS 2 "arithmetic binary subtraction operator"
operator UMINUS 1 "arithmetic unary negation"
operator DIVISION 2 "real division, division by 0 undefined (user symbol)"
operator DIVISION_TOTAL 2 "real division with interpreted division by 0 (internal symbol)"
operator INTS_DIVISION 2 "integer division, division by 0 undefined (user symbol)"
operator INTS_DIVISION_TOTAL 2 "integer division with interpreted division by 0 (internal symbol)"
operator INTS_MODULUS 2 "integer modulus, division by 0 undefined (user symbol)"
operator INTS_MODULUS_TOTAL 2 "integer modulus with interpreted division by 0 (internal symbol)"
operator ABS 1 "absolute value"
parameterized DIVISIBLE DIVISIBLE_OP 1 "divisibility-by-k predicate; first parameter is a DIVISIBLE_OP, second is integer term"
operator POW 2 "arithmetic power"
operator EXPONENTIAL 1 "exponential"
operator SINE 1 "sine"
operator COSINE 1 "consine"
operator TANGENT 1 "tangent"
operator COSECANT 1 "cosecant"
operator SECANT 1 "secant"
operator COTANGENT 1 "cotangent"
operator ARCSINE 1 "arc sine"
operator ARCCOSINE 1 "arc consine"
operator ARCTANGENT 1 "arc tangent"
operator ARCCOSECANT 1 "arc cosecant"
operator ARCSECANT 1 "arc secant"
operator ARCCOTANGENT 1 "arc cotangent"
operator SQRT 1 "square root"
constant DIVISIBLE_OP \
struct \
Divisible \
::cvc5::DivisibleHashFunction \
"util/divisible.h" \
"operator for the divisibility-by-k predicate; payload is an instance of the cvc5::Divisible class"
sort REAL_TYPE \
Cardinality::REALS \
well-founded \
"NodeManager::currentNM()->mkConst(Rational(0))" \
"expr/node_manager.h" \
"real type"
sort INTEGER_TYPE \
Cardinality::INTEGERS \
well-founded \
"NodeManager::currentNM()->mkConst(Rational(0))" \
"expr/node_manager.h" \
"integer type"
constant CONST_RATIONAL \
class \
Rational \
::cvc5::RationalHashFunction \
"util/rational.h" \
"a multiple-precision rational constant; payload is an instance of the cvc5::Rational class"
enumerator REAL_TYPE \
"::cvc5::theory::arith::RationalEnumerator" \
"theory/arith/type_enumerator.h"
enumerator INTEGER_TYPE \
"::cvc5::theory::arith::IntegerEnumerator" \
"theory/arith/type_enumerator.h"
operator LT 2 "less than, x < y"
operator LEQ 2 "less than or equal, x <= y"
operator GT 2 "greater than, x > y"
operator GEQ 2 "greater than or equal, x >= y"
# represents an indexed root predicate. See util/indexed_root_predicate.h for more documentation.
constant INDEXED_ROOT_PREDICATE_OP \
struct \
IndexedRootPredicate \
::cvc5::IndexedRootPredicateHashFunction \
"util/indexed_root_predicate.h" \
"operator for the indexed root predicate; payload is an instance of the cvc5::IndexedRootPredicate class"
parameterized INDEXED_ROOT_PREDICATE INDEXED_ROOT_PREDICATE_OP 2 "indexed root predicate; first parameter is a INDEXED_ROOT_PREDICATE_OP, second is a real variable compared to zero, third is a polynomial"
operator IS_INTEGER 1 "term-is-integer predicate (parameter is a real-sorted term)"
operator TO_INTEGER 1 "convert term to integer by the floor function (parameter is a real-sorted term)"
operator TO_REAL 1 "cast term to real (parameter is an integer-sorted term; this is a no-op in cvc5, as integer is a subtype of real)"
# CAST_TO_REAL is added to distinguish between integers casted to reals internally, and
# integers casted to reals or using the API \
# Solver::mkReal(int val) would return an internal node (CAST_TO_REAL val), but in the api it appears as term (val) \
# Solver::mkTerm(TO_REAL, Solver::mkInteger(int val)) would return both term and node (TO_REAL val) \
# This way, we avoid having 2 nested TO_REAL nodess as a result of Solver::mkTerm(TO_REAL, Solver::mkReal(int val))
operator CAST_TO_REAL 1 "cast term to real same as TO_REAL, but it is used internally, whereas TO_REAL is accessible in the API"
typerule PLUS ::cvc5::theory::arith::ArithOperatorTypeRule
typerule MULT ::cvc5::theory::arith::ArithOperatorTypeRule
typerule NONLINEAR_MULT ::cvc5::theory::arith::ArithOperatorTypeRule
typerule MINUS ::cvc5::theory::arith::ArithOperatorTypeRule
typerule UMINUS ::cvc5::theory::arith::ArithOperatorTypeRule
typerule DIVISION ::cvc5::theory::arith::ArithOperatorTypeRule
typerule POW ::cvc5::theory::arith::ArithOperatorTypeRule
typerule CONST_RATIONAL ::cvc5::theory::arith::ArithConstantTypeRule
typerule LT "SimpleTypeRule<RBool, AReal, AReal>"
typerule LEQ "SimpleTypeRule<RBool, AReal, AReal>"
typerule GT "SimpleTypeRule<RBool, AReal, AReal>"
typerule GEQ "SimpleTypeRule<RBool, AReal, AReal>"
typerule INDEXED_ROOT_PREDICATE_OP "SimpleTypeRule<RBuiltinOperator>"
typerule INDEXED_ROOT_PREDICATE ::cvc5::theory::arith::IndexedRootPredicateTypeRule
typerule TO_REAL ::cvc5::theory::arith::ArithOperatorTypeRule
typerule CAST_TO_REAL ::cvc5::theory::arith::ArithOperatorTypeRule
typerule TO_INTEGER ::cvc5::theory::arith::ArithOperatorTypeRule
typerule IS_INTEGER "SimpleTypeRule<RBool, AReal>"
typerule ABS "SimpleTypeRule<RInteger, AInteger>"
typerule INTS_DIVISION "SimpleTypeRule<RInteger, AInteger, AInteger>"
typerule INTS_MODULUS "SimpleTypeRule<RInteger, AInteger, AInteger>"
typerule DIVISIBLE "SimpleTypeRule<RBool, AInteger>"
typerule DIVISIBLE_OP "SimpleTypeRule<RBuiltinOperator>"
typerule DIVISION_TOTAL ::cvc5::theory::arith::ArithOperatorTypeRule
typerule INTS_DIVISION_TOTAL "SimpleTypeRule<RInteger, AInteger, AInteger>"
typerule INTS_MODULUS_TOTAL "SimpleTypeRule<RInteger, AInteger, AInteger>"
typerule EXPONENTIAL "SimpleTypeRule<RReal, AReal>"
typerule SINE "SimpleTypeRule<RReal, AReal>"
typerule COSINE "SimpleTypeRule<RReal, AReal>"
typerule TANGENT "SimpleTypeRule<RReal, AReal>"
typerule COSECANT "SimpleTypeRule<RReal, AReal>"
typerule SECANT "SimpleTypeRule<RReal, AReal>"
typerule COTANGENT "SimpleTypeRule<RReal, AReal>"
typerule ARCSINE "SimpleTypeRule<RReal, AReal>"
typerule ARCCOSINE "SimpleTypeRule<RReal, AReal>"
typerule ARCTANGENT "SimpleTypeRule<RReal, AReal>"
typerule ARCCOSECANT "SimpleTypeRule<RReal, AReal>"
typerule ARCSECANT "SimpleTypeRule<RReal, AReal>"
typerule ARCCOTANGENT "SimpleTypeRule<RReal, AReal>"
typerule SQRT "SimpleTypeRule<RReal, AReal>"
nullaryoperator PI "pi"
typerule PI ::cvc5::theory::arith::RealNullaryOperatorTypeRule
# Integer AND, which is parameterized by a (positive) bitwidth k.
# ((_ iand k) i1 i2) is equivalent to:
# (bv2int (bvand ((_ int2bv k) i1) ((_ int2bv k) i2)))
# for all integers i1, i2.
constant IAND_OP \
struct \
IntAnd \
"::cvc5::UnsignedHashFunction< ::cvc5::IntAnd >" \
"util/iand.h" \
"operator for integer AND; payload is an instance of the cvc5::IntAnd class"
parameterized IAND IAND_OP 2 "integer version of AND operator; first parameter is an IAND_OP, second and third are integer terms"
typerule IAND_OP ::cvc5::theory::arith::IAndOpTypeRule
typerule IAND ::cvc5::theory::arith::IAndTypeRule
endtheory
|
