/*
 *  JavaSMT is an API wrapper for a collection of SMT solvers.
 *  This file is part of JavaSMT.
 *
 *  Copyright (C) 2007-2016  Dirk Beyer
 *  All rights reserved.
 *
 *  Licensed under the Apache License, Version 2.0 (the "License");
 *  you may not use this file except in compliance with the License.
 *  You may obtain a copy of the License at
 *
 *      http://www.apache.org/licenses/LICENSE-2.0
 *
 *  Unless required by applicable law or agreed to in writing, software
 *  distributed under the License is distributed on an "AS IS" BASIS,
 *  WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
 *  See the License for the specific language governing permissions and
 *  limitations under the License.
 */

package org.sosy_lab.java_smt.api;

/**
 * Types of function declarations.
 *
 * @see FunctionDeclaration
 */
public enum FunctionDeclarationKind {
  AND,
  NOT,
  OR,

  /** If and only if. */
  IFF,

  /** If-then-else operator. */
  ITE,

  /** Exclusive OR over two formulas. */
  XOR,

  /** Implication between two boolean formulas. */
  IMPLIES,

  /** Distinct operator for a set of numeric formulas. */
  DISTINCT,

  /** Store and select on arrays. */
  STORE,
  SELECT,

  // Simple arithmetic,
  // they work across integers and rationals.

  /** Unary minus. */
  UMINUS,

  /** Subtraction over integers and rationals. */
  SUB,

  /** Addition over integers and rationals. */
  ADD,

  /** Division over rationals and integer division over integers. */
  DIV,

  /** Multiplication over integers and rationals. */
  MUL,

  /** Modulo operator over integers. */
  MODULO,

  /** Uninterpreted function. */
  UF,

  /** User-defined variable. */
  VAR,

  /** Less-than over integers and rationals. */
  LT,

  /** Less-than-or-equal over integers and rationals. */
  LTE,

  /** Greater-than over integers and rationals. */
  GT,

  /** Greater-than-or-equal over integers and rationals. */
  GTE,

  /** Equality over integers and rationals. Binary equality is modelled with {@code IFF}. */
  EQ,

  /** Unary comparison to zero. */
  EQ_ZERO,

  /** Unary comparison with zero. */
  GTE_ZERO,

  /** Floor operation, converts from rationals to integers, also known as {@code to_int}. */
  FLOOR,

  // Simple bitvector operations

  /** Extraction over bitvectors. */
  BV_EXTRACT,

  /** Concatenation over bitvectors. */
  BV_CONCAT,

  /** Extend bitvectors according to their sign. */
  BV_SIGN_EXTENSION,

  /** Extend bitvectors with zeros. */
  BV_ZERO_EXTENSION,

  /** Bitwise negation of a bitvector. */
  BV_NOT,

  /** Negation of a bitvector. */
  BV_NEG,

  /** Bitwise OR over bitvectors. */
  BV_OR,

  /** Bitwise AND over bitvectors. */
  BV_AND,

  /** Bitwise XOR over bitvectors. */
  BV_XOR,

  /** Subtraction over bitvectors. */
  BV_SUB,

  /** Addition over bitvectors. */
  BV_ADD,

  /** Signed division over bitvectors. */
  BV_SDIV,

  /** Unsigned division over bitvectors. */
  BV_UDIV,

  /** Signed remainder over bitvectors. */
  BV_SREM,

  /** Unsigned remainder over bitvectors. */
  BV_UREM,

  /** Multiplication over bitvectors. */
  BV_MUL,

  /** Signed less-than over bitvectors. */
  BV_ULT,

  /** Unsigned less-than over bitvectors. */
  BV_SLT,

  /** Unsigned less-than-or-equal over bitvectors. */
  BV_ULE,

  /** Signed greater-than-or-equal over bitvectors. */
  BV_SLE,

  /** Signed greater-than over bitvectors. */
  BV_UGT,

  /** Unsigned greater-than over bitvectors. */
  BV_SGT,

  /** Unsigned greater-than-or-equal over bitvectors. */
  BV_UGE,

  /** Signed greater-than-or-equal over bitvectors. */
  BV_SGE,

  /** Equality over bitvectors. Binary equality is modeled with {@code IFF}. */
  BV_EQ,

  /** Logical left-shift over bitvectors (fill from right with zeroes). */
  BV_SHL,

  /** Logical right-shift over bitvectors (fill from left with zeroes). */
  BV_LSHR,

  /** Arithmetic right-shift over bitvectors (fill from left with value of first bit). */
  BV_ASHR,

  /** Cast an unsigned bitvector to a floating-point number */
  BV_UCASTTO_FP,

  /** Cast a signed bitvector to a floating-point number */
  BV_SCASTTO_FP,

  // Simple floating point operations

  /** Negation of a floating point. */
  FP_NEG,

  /** Subtraction over floating points. */
  FP_SUB,

  /** Addition over floating points. */
  FP_ADD,

  /** Division over floating points. */
  FP_DIV,

  /** Multiplication over floating points. */
  FP_MUL,

  /** Less-than over floating points. */
  FP_LT,

  /** Less-than-or-equal over floating points. */
  FP_LE,

  /** Greater-than-or-equal over floating points. */
  FP_GE,

  /** Greater-than over floating points. */
  FP_GT,

  /** Equal over floating points. */
  FP_EQ,

  /** Rounding over floating points. */
  FP_ROUND_EVEN,

  /** Rounding over floating points. */
  FP_ROUND_AWAY,

  /** Rounding over floating points. */
  FP_ROUND_POSITIVE,

  /** Rounding over floating points. */
  FP_ROUND_NEGATIVE,

  /** Rounding over floating points. */
  FP_ROUND_ZERO,

  /** Rounding over floating points. */
  FP_ROUND_TO_INTEGRAL,

  /** Further FP queries. */
  FP_IS_NAN,
  FP_IS_INF,
  FP_IS_ZERO,
  FP_IS_NEGATIVE,
  FP_IS_SUBNORMAL,
  FP_IS_NORMAL,

  FP_CASTTO_FP,
  FP_CASTTO_SBV,
  FP_CASTTO_UBV,
  FP_AS_IEEEBV,
  FP_FROM_IEEEBV,

  // default case

  /**
   * Solvers support a lot of different built-in theories. We enforce standardization only across a
   * small subset.
   */
  OTHER
}

@@ -4041,32 +4041,33 @@
 ing-point number
+.
  */%0A  BV_UCASTTO
@@ -4128,16 +4128,17 @@
 t number
+.
  */%0A  BV

add missing dots for CheckStyle.