3 # For documentation on this file format, please refer to
4 # src/theory/builtin/kinds.
7 theory THEORY_ARITH ::CVC4::theory::arith::TheoryArith "theory/arith/theory_arith.h"
8 typechecker "theory/arith/theory_arith_type_rules.h"
10 properties stable-infinite
11 properties check propagate ppStaticLearn presolve notifyRestart
13 rewriter ::CVC4::theory::arith::ArithRewriter "theory/arith/arith_rewriter.h"
16 operator PLUS 2: "arithmetic addition"
17 operator MULT 2: "arithmetic multiplication"
18 operator MINUS 2 "arithmetic binary subtraction operator"
19 operator UMINUS 1 "arithmetic unary negation"
20 operator DIVISION 2 "real division (user symbol)"
21 operator DIVISION_TOTAL 2 "real division with interpreted division by 0 (internal symbol)"
22 operator INTS_DIVISION 2 "ints division (user symbol)"
23 operator INTS_DIVISION_TOTAL 2 "ints division with interpreted division by 0 (internal symbol)"
24 operator INTS_MODULUS 2 "ints modulus (user symbol)"
25 operator INTS_MODULUS_TOTAL 2 "ints modulus with interpreted division by 0 (internal symbol)"
26 operator ABS 1 "absolute value"
27 parameterized DIVISIBLE DIVISIBLE_OP 1 "divisibility-by-k predicate"
28 operator POW 2 "arithmetic power"
30 constant DIVISIBLE_OP \
32 ::CVC4::DivisibleHashFunction \
34 "operator for the divisibility-by-k predicate"
39 "NodeManager::currentNM()->mkConst(Rational(0))" \
40 "expr/node_manager.h" \
43 Cardinality::INTEGERS \
45 "NodeManager::currentNM()->mkConst(Rational(0))" \
46 "expr/node_manager.h" \
49 constant SUBRANGE_TYPE \
50 ::CVC4::SubrangeBounds \
51 ::CVC4::SubrangeBoundsHashFunction \
52 "util/subrange_bound.h" \
53 "the type of an integer subrange"
54 cardinality SUBRANGE_TYPE \
55 "::CVC4::theory::arith::SubrangeProperties::computeCardinality(%TYPE%)" \
56 "theory/arith/theory_arith_type_rules.h"
57 well-founded SUBRANGE_TYPE \
59 "::CVC4::theory::arith::SubrangeProperties::mkGroundTerm(%TYPE%)" \
60 "theory/arith/theory_arith_type_rules.h"
62 constant CONST_RATIONAL \
64 ::CVC4::RationalHashFunction \
66 "a multiple-precision rational constant"
68 enumerator REAL_TYPE \
69 "::CVC4::theory::arith::RationalEnumerator" \
70 "theory/arith/type_enumerator.h"
71 enumerator INTEGER_TYPE \
72 "::CVC4::theory::arith::IntegerEnumerator" \
73 "theory/arith/type_enumerator.h"
74 enumerator SUBRANGE_TYPE \
75 "::CVC4::theory::arith::SubrangeEnumerator" \
76 "theory/arith/type_enumerator.h"
78 operator LT 2 "less than, x < y"
79 operator LEQ 2 "less than or equal, x <= y"
80 operator GT 2 "greater than, x > y"
81 operator GEQ 2 "greater than or equal, x >= y"
83 operator IS_INTEGER 1 "term is integer"
84 operator TO_INTEGER 1 "cast term to integer"
85 operator TO_REAL 1 "cast term to real"
87 typerule PLUS ::CVC4::theory::arith::ArithOperatorTypeRule
88 typerule MULT ::CVC4::theory::arith::ArithOperatorTypeRule
89 typerule MINUS ::CVC4::theory::arith::ArithOperatorTypeRule
90 typerule UMINUS ::CVC4::theory::arith::ArithOperatorTypeRule
91 typerule DIVISION ::CVC4::theory::arith::ArithOperatorTypeRule
92 typerule POW ::CVC4::theory::arith::ArithOperatorTypeRule
94 typerule CONST_RATIONAL ::CVC4::theory::arith::ArithConstantTypeRule
96 typerule LT ::CVC4::theory::arith::ArithPredicateTypeRule
97 typerule LEQ ::CVC4::theory::arith::ArithPredicateTypeRule
98 typerule GT ::CVC4::theory::arith::ArithPredicateTypeRule
99 typerule GEQ ::CVC4::theory::arith::ArithPredicateTypeRule
101 typerule TO_REAL ::CVC4::theory::arith::ArithOperatorTypeRule
102 typerule TO_INTEGER ::CVC4::theory::arith::ArithOperatorTypeRule
103 typerule IS_INTEGER ::CVC4::theory::arith::ArithUnaryPredicateTypeRule
105 typerule ABS ::CVC4::theory::arith::IntOperatorTypeRule
106 typerule INTS_DIVISION ::CVC4::theory::arith::IntOperatorTypeRule
107 typerule INTS_MODULUS ::CVC4::theory::arith::IntOperatorTypeRule
108 typerule DIVISIBLE ::CVC4::theory::arith::IntUnaryPredicateTypeRule
110 typerule DIVISION_TOTAL ::CVC4::theory::arith::ArithOperatorTypeRule
111 typerule INTS_DIVISION_TOTAL ::CVC4::theory::arith::IntOperatorTypeRule
112 typerule INTS_MODULUS_TOTAL ::CVC4::theory::arith::IntOperatorTypeRule