blob: 95d1aa9c1ab04c57a0cd53f3e818b215e7838461 (
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
|
# kinds -*- sh -*-
#
# For documentation on this file format, please refer to
# src/theory/builtin/kinds.
#
theory THEORY_ARITH ::CVC4::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 ::CVC4::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 \
::CVC4::Divisible \
::CVC4::DivisibleHashFunction \
"util/divisible.h" \
"operator for the divisibility-by-k predicate; payload is an instance of the CVC4::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 \
::CVC4::Rational \
::CVC4::RationalHashFunction \
"util/rational.h" \
"a multiple-precision rational constant; payload is an instance of the CVC4::Rational class"
enumerator REAL_TYPE \
"::CVC4::theory::arith::RationalEnumerator" \
"theory/arith/type_enumerator.h"
enumerator INTEGER_TYPE \
"::CVC4::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"
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 CVC4, as integer is a subtype of real)"
typerule PLUS ::CVC4::theory::arith::ArithOperatorTypeRule
typerule MULT ::CVC4::theory::arith::ArithOperatorTypeRule
typerule NONLINEAR_MULT ::CVC4::theory::arith::ArithOperatorTypeRule
typerule MINUS ::CVC4::theory::arith::ArithOperatorTypeRule
typerule UMINUS ::CVC4::theory::arith::ArithOperatorTypeRule
typerule DIVISION ::CVC4::theory::arith::ArithOperatorTypeRule
typerule POW ::CVC4::theory::arith::ArithOperatorTypeRule
typerule CONST_RATIONAL ::CVC4::theory::arith::ArithConstantTypeRule
typerule LT ::CVC4::theory::arith::ArithPredicateTypeRule
typerule LEQ ::CVC4::theory::arith::ArithPredicateTypeRule
typerule GT ::CVC4::theory::arith::ArithPredicateTypeRule
typerule GEQ ::CVC4::theory::arith::ArithPredicateTypeRule
typerule TO_REAL ::CVC4::theory::arith::ArithOperatorTypeRule
typerule TO_INTEGER ::CVC4::theory::arith::ArithOperatorTypeRule
typerule IS_INTEGER ::CVC4::theory::arith::ArithUnaryPredicateTypeRule
typerule ABS ::CVC4::theory::arith::IntOperatorTypeRule
typerule INTS_DIVISION ::CVC4::theory::arith::IntOperatorTypeRule
typerule INTS_MODULUS ::CVC4::theory::arith::IntOperatorTypeRule
typerule DIVISIBLE ::CVC4::theory::arith::IntUnaryPredicateTypeRule
typerule DIVISIBLE_OP ::CVC4::theory::arith::DivisibleOpTypeRule
typerule DIVISION_TOTAL ::CVC4::theory::arith::ArithOperatorTypeRule
typerule INTS_DIVISION_TOTAL ::CVC4::theory::arith::IntOperatorTypeRule
typerule INTS_MODULUS_TOTAL ::CVC4::theory::arith::IntOperatorTypeRule
typerule EXPONENTIAL ::CVC4::theory::arith::RealOperatorTypeRule
typerule SINE ::CVC4::theory::arith::RealOperatorTypeRule
typerule COSINE ::CVC4::theory::arith::RealOperatorTypeRule
typerule TANGENT ::CVC4::theory::arith::RealOperatorTypeRule
typerule COSECANT ::CVC4::theory::arith::RealOperatorTypeRule
typerule SECANT ::CVC4::theory::arith::RealOperatorTypeRule
typerule COTANGENT ::CVC4::theory::arith::RealOperatorTypeRule
typerule ARCSINE ::CVC4::theory::arith::RealOperatorTypeRule
typerule ARCCOSINE ::CVC4::theory::arith::RealOperatorTypeRule
typerule ARCTANGENT ::CVC4::theory::arith::RealOperatorTypeRule
typerule ARCCOSECANT ::CVC4::theory::arith::RealOperatorTypeRule
typerule ARCSECANT ::CVC4::theory::arith::RealOperatorTypeRule
typerule ARCCOTANGENT ::CVC4::theory::arith::RealOperatorTypeRule
typerule SQRT ::CVC4::theory::arith::RealOperatorTypeRule
nullaryoperator PI "pi"
typerule PI ::CVC4::theory::arith::RealNullaryOperatorTypeRule
endtheory
|
