diff options
Diffstat (limited to 'src/smt_util')
-rw-r--r-- | src/smt_util/boolean_simplification.cpp | 4 | ||||
-rw-r--r-- | src/smt_util/boolean_simplification.h | 4 | ||||
-rw-r--r-- | src/smt_util/nary_builder.cpp | 4 | ||||
-rw-r--r-- | src/smt_util/nary_builder.h | 4 |
4 files changed, 8 insertions, 8 deletions
diff --git a/src/smt_util/boolean_simplification.cpp b/src/smt_util/boolean_simplification.cpp index 01f1a6a5b..6bfbede92 100644 --- a/src/smt_util/boolean_simplification.cpp +++ b/src/smt_util/boolean_simplification.cpp @@ -16,7 +16,7 @@ #include "smt_util/boolean_simplification.h" -namespace CVC5 { +namespace cvc5 { bool BooleanSimplification::push_back_associative_commute_recursive( Node n, std::vector<Node>& buffer, Kind k, Kind notK, bool negateNode) @@ -61,4 +61,4 @@ bool BooleanSimplification::push_back_associative_commute_recursive( return true; }/* BooleanSimplification::push_back_associative_commute_recursive() */ -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/smt_util/boolean_simplification.h b/src/smt_util/boolean_simplification.h index d9251baf5..de53e539c 100644 --- a/src/smt_util/boolean_simplification.h +++ b/src/smt_util/boolean_simplification.h @@ -25,7 +25,7 @@ #include "base/check.h" #include "expr/node.h" -namespace CVC5 { +namespace cvc5 { /** * A class to contain a number of useful functions for simple @@ -223,6 +223,6 @@ class BooleanSimplification { };/* class BooleanSimplification */ -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__BOOLEAN_SIMPLIFICATION_H */ diff --git a/src/smt_util/nary_builder.cpp b/src/smt_util/nary_builder.cpp index 41da7e170..efff058c5 100644 --- a/src/smt_util/nary_builder.cpp +++ b/src/smt_util/nary_builder.cpp @@ -20,7 +20,7 @@ using namespace std; -namespace CVC5 { +namespace cvc5 { namespace util { Node NaryBuilder::mkAssoc(Kind kind, const std::vector<Node>& children) @@ -202,4 +202,4 @@ Node RePairAssocCommutativeOperators::case_other(TNode n){ } }/* util namespace */ -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/smt_util/nary_builder.h b/src/smt_util/nary_builder.h index dc8a428d0..6fdc541ca 100644 --- a/src/smt_util/nary_builder.h +++ b/src/smt_util/nary_builder.h @@ -24,7 +24,7 @@ #include "expr/node.h" -namespace CVC5 { +namespace cvc5 { namespace util { class NaryBuilder { @@ -53,4 +53,4 @@ private: };/* class RePairAssocCommutativeOperators */ }/* util namespace */ -} // namespace CVC5 +} // namespace cvc5 |