diff options
Diffstat (limited to 'src/expr/kind_template.h')
-rw-r--r-- | src/expr/kind_template.h | 22 |
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 */ |