summaryrefslogtreecommitdiff
path: root/src/expr/kind_template.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/expr/kind_template.h')
-rw-r--r--src/expr/kind_template.h22
1 files changed, 11 insertions, 11 deletions
diff --git a/src/expr/kind_template.h b/src/expr/kind_template.h
index 4661cfa15..484e8c273 100644
--- a/src/expr/kind_template.h
+++ b/src/expr/kind_template.h
@@ -24,7 +24,7 @@
#include "base/exception.h"
#include "theory/theory_id.h"
-namespace CVC5 {
+namespace cvc5 {
namespace kind {
enum Kind_t
@@ -39,7 +39,7 @@ enum Kind_t
// import Kind into the "CVC4" namespace but keep the individual kind
// constants under kind::
-typedef ::CVC5::kind::Kind_t Kind;
+typedef ::cvc5::kind::Kind_t Kind;
namespace kind {
@@ -52,7 +52,7 @@ namespace kind {
* @param k The kind
* @return The name of the kind
*/
-const char* toString(CVC5::Kind k);
+const char* toString(cvc5::Kind k);
/**
* Writes a kind name to a stream.
@@ -61,17 +61,17 @@ const char* toString(CVC5::Kind k);
* @param k The kind to write to the stream
* @return The stream
*/
-std::ostream& operator<<(std::ostream&, CVC5::Kind);
+std::ostream& operator<<(std::ostream&, cvc5::Kind);
/** Returns true if the given kind is associative. This is used by ExprManager to
* decide whether it's safe to modify big expressions by changing the grouping of
* the arguments. */
/* TODO: This could be generated. */
-bool isAssociative(::CVC5::Kind k);
-std::string kindToString(::CVC5::Kind k);
+bool isAssociative(::cvc5::Kind k);
+std::string kindToString(::cvc5::Kind k);
struct KindHashFunction {
- inline size_t operator()(::CVC5::Kind k) const { return k; }
+ inline size_t operator()(::cvc5::Kind k) const { return k; }
};/* struct KindHashFunction */
} // namespace kind
@@ -97,11 +97,11 @@ std::ostream& operator<<(std::ostream& out, TypeConstant typeConstant);
namespace theory {
-::CVC5::theory::TheoryId kindToTheoryId(::CVC5::Kind k);
-::CVC5::theory::TheoryId typeConstantToTheoryId(
- ::CVC5::TypeConstant typeConstant);
+::cvc5::theory::TheoryId kindToTheoryId(::cvc5::Kind k);
+::cvc5::theory::TheoryId typeConstantToTheoryId(
+ ::cvc5::TypeConstant typeConstant);
} // namespace theory
-} // namespace CVC5
+} // namespace cvc5
#endif /* CVC4__KIND_H */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback