src/theory/arith/kinds

   1 # kinds                                                               -*- sh -*-
   2 #
   3 # For documentation on this file format, please refer to
   4 # src/theory/builtin/kinds.
   5 #
   6
   7 theory THEORY_ARITH ::CVC4::theory::arith::TheoryArith "theory/arith/theory_arith.h"
   8 typechecker "theory/arith/theory_arith_type_rules.h"
   9
  10 properties stable-infinite
  11 properties check propagate ppStaticLearn presolve notifyRestart
  12
  13 rewriter ::CVC4::theory::arith::ArithRewriter "theory/arith/arith_rewriter.h"
  14
  15
  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"
  29
  30 constant DIVISIBLE_OP \
  31         ::CVC4::Divisible \
  32         ::CVC4::DivisibleHashFunction \
  33         "util/divisible.h" \
  34         "operator for the divisibility-by-k predicate"
  35
  36 sort REAL_TYPE \
  37     Cardinality::REALS \
  38     well-founded \
  39         "NodeManager::currentNM()->mkConst(Rational(0))" \
  40         "expr/node_manager.h" \
  41     "Real type"
  42 sort INTEGER_TYPE \
  43     Cardinality::INTEGERS \
  44     well-founded \
  45         "NodeManager::currentNM()->mkConst(Rational(0))" \
  46         "expr/node_manager.h" \
  47     "Integer type"
  48
  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 \
  58     true \
  59     "::CVC4::theory::arith::SubrangeProperties::mkGroundTerm(%TYPE%)" \
  60     "theory/arith/theory_arith_type_rules.h"
  61
  62 constant CONST_RATIONAL \
  63     ::CVC4::Rational \
  64     ::CVC4::RationalHashFunction \
  65     "util/rational.h" \
  66     "a multiple-precision rational constant"
  67
  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"
  77
  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"
  82
  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"
  86
  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
  93
  94 typerule CONST_RATIONAL ::CVC4::theory::arith::ArithConstantTypeRule
  95
  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
 100
 101 typerule TO_REAL ::CVC4::theory::arith::ArithOperatorTypeRule
 102 typerule TO_INTEGER ::CVC4::theory::arith::ArithOperatorTypeRule
 103 typerule IS_INTEGER ::CVC4::theory::arith::ArithUnaryPredicateTypeRule
 104
 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
 109
 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
 113
 114 endtheory