34242e746da58d63a4c16da4d72faaa901e3de52
1 /********************* */
2 /*! \file inference.cpp
4 ** Top contributors (to current version):
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
12 ** \brief Implementation of inference enumeration.
15 #include "theory/arith/nl/inference.h"
22 const char* toString(Inference i
)
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";
46 std::ostream
& operator<<(std::ostream
& out
, Inference i
)