1 /********************* */
2 /*! \file kind_template.cpp
3 ** \verbatim
4 ** Top contributors (to current version):
5 ** Andres Noetzli, Morgan Deters, Dejan Jovanovic
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2019 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 [[ Add one-line brief description here ]]
13 **
14 ** [[ Add lengthier description here ]]
15 ** \todo document this file
16 **/
17
18 #include "expr/kind.h"
19
20 namespace CVC4 {
21 namespace kind {
22
operator <<(std::ostream & out,CVC4::Kind k)23 std::ostream& operator<<(std::ostream& out, CVC4::Kind k) {
24 using namespace CVC4::kind;
25
26 switch(k) {
27
28 /* special cases */
29 case UNDEFINED_KIND: out << "UNDEFINED_KIND"; break;
30 case NULL_EXPR: out << "NULL"; break;
31 ${kind_printers}
32 case LAST_KIND: out << "LAST_KIND"; break;
33 default: out << "UNKNOWNKIND!" << int(k); break;
34 }
35
36 return out;
37 }
38
39 /** Returns true if the given kind is associative. This is used by ExprManager to
40 * decide whether it's safe to modify big expressions by changing the grouping of
41 * the arguments. */
42 /* TODO: This could be generated. */
isAssociative(::CVC4::Kind k)43 bool isAssociative(::CVC4::Kind k) {
44 switch(k) {
45 case kind::AND:
46 case kind::OR:
47 case kind::MULT:
48 case kind::PLUS:
49 return true;
50
51 default:
52 return false;
53 }
54 }
55
kindToString(::CVC4::Kind k)56 std::string kindToString(::CVC4::Kind k) {
57 std::stringstream ss;
58 ss << k;
59 return ss.str();
60 }
61
62 }/* CVC4::kind namespace */
63
operator <<(std::ostream & out,TypeConstant typeConstant)64 std::ostream& operator<<(std::ostream& out, TypeConstant typeConstant) {
65 switch(typeConstant) {
66 ${type_constant_descriptions}
67 #line 68 "${template}"
68 default:
69 out << "UNKNOWN_TYPE_CONSTANT";
70 break;
71 }
72 return out;
73 }
74
75 namespace theory {
76
operator <<(std::ostream & out,TheoryId theoryId)77 std::ostream& operator<<(std::ostream& out, TheoryId theoryId) {
78 switch(theoryId) {
79 ${theory_descriptions}
80 #line 81 "${template}"
81 default:
82 out << "UNKNOWN_THEORY";
83 break;
84 }
85 return out;
86 }
87
kindToTheoryId(::CVC4::Kind k)88 TheoryId kindToTheoryId(::CVC4::Kind k) {
89 switch(k) {
90 case kind::UNDEFINED_KIND:
91 case kind::NULL_EXPR:
92 break;
93 ${kind_to_theory_id}
94 #line 95 "${template}"
95 case kind::LAST_KIND:
96 break;
97 }
98 throw IllegalArgumentException("", "k", __PRETTY_FUNCTION__, "bad kind");
99 }
100
typeConstantToTheoryId(::CVC4::TypeConstant typeConstant)101 TheoryId typeConstantToTheoryId(::CVC4::TypeConstant typeConstant) {
102 switch(typeConstant) {
103 ${type_constant_to_theory_id}
104 #line 105 "${template}"
105 case LAST_TYPE:
106 break;
107 }
108 throw IllegalArgumentException("", "k", __PRETTY_FUNCTION__, "bad type constant");
109 }
110
getStatsPrefix(TheoryId theoryId)111 std::string getStatsPrefix(TheoryId theoryId) {
112 switch(theoryId) {
113 ${theory_stats_prefixes}
114 #line 115 "${template}"
115 default:
116 break;
117 }
118 return "unknown";
119 }
120
121 }/* CVC4::theory namespace */
122 }/* CVC4 namespace */
123