src/theory/arith/nl/inference.cpp

   1 /*********************                                                        */
   2 /*! \file inference.cpp
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Andrew Reynolds
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
   8  ** in the top-level source directory) and their institutional affiliations.
   9  ** All rights reserved.  See the file COPYING in the top-level source
  10  ** directory for licensing information.\endverbatim
  11  **
  12  ** \brief Implementation of inference enumeration.
  13  **/
  14
  15 #include "theory/arith/nl/inference.h"
  16
  17 namespace CVC4 {
  18 namespace theory {
  19 namespace arith {
  20 namespace nl {
  21
  22 const char* toString(Inference i)
  23 {
  24   switch (i)
  25   {
  26     case Inference::CONGRUENCE: return "CONGRUENCE";
  27     case Inference::SHARED_TERM_VALUE_SPLIT: return "SHARED_TERM_VALUE_SPLIT";
  28     case Inference::SPLIT_ZERO: return "SPLIT_ZERO";
  29     case Inference::SIGN: return "SIGN";
  30     case Inference::COMPARISON: return "COMPARISON";
  31     case Inference::INFER_BOUNDS: return "INFER_BOUNDS";
  32     case Inference::INFER_BOUNDS_NT: return "INFER_BOUNDS_NT";
  33     case Inference::FACTOR: return "FACTOR";
  34     case Inference::RES_INFER_BOUNDS: return "RES_INFER_BOUNDS";
  35     case Inference::TANGENT_PLANE: return "TANGENT_PLANE";
  36     case Inference::T_PURIFY_ARG: return "T_PURIFY_ARG";
  37     case Inference::T_INIT_REFINE: return "T_INIT_REFINE";
  38     case Inference::T_PI_BOUND: return "T_PI_BOUND";
  39     case Inference::T_MONOTONICITY: return "T_MONOTONICITY";
  40     case Inference::T_SECANT: return "T_SECANT";
  41     case Inference::T_TANGENT: return "T_TANGENT";
  42     default: return "?";
  43   }
  44 }
  45
  46 std::ostream& operator<<(std::ostream& out, Inference i)
  47 {
  48   out << toString(i);
  49   return out;
  50 }
  51
  52 }  // namespace nl
  53 }  // namespace arith
  54 }  // namespace theory
  55 }  // namespace CVC4