diff options
| author | Aina Niemetz <aina.niemetz@gmail.com> | 2021-03-31 15:23:17 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-03-31 22:23:17 +0000 |
| commit | a1466978fbc328507406d4a121dab4d1a1047e1d (patch) | |
| tree | 12b40f161bb4d7a6ee40c20c78a15d6cda3c1995 /src/smt_util | |
| parent | f9a9af855fb65804ff0b36e764ccd9d0fa9f87f8 (diff) | |
Rename namespace CVC4 to CVC5. (#6249)
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 b412a4418..01f1a6a5b 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 CVC4 { +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() */ -}/* CVC4 namespace */ +} // namespace CVC5 diff --git a/src/smt_util/boolean_simplification.h b/src/smt_util/boolean_simplification.h index 2b0af49c3..d9251baf5 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 CVC4 { +namespace CVC5 { /** * A class to contain a number of useful functions for simple @@ -223,6 +223,6 @@ class BooleanSimplification { };/* class BooleanSimplification */ -}/* CVC4 namespace */ +} // namespace CVC5 #endif /* CVC4__BOOLEAN_SIMPLIFICATION_H */ diff --git a/src/smt_util/nary_builder.cpp b/src/smt_util/nary_builder.cpp index fa154c245..41da7e170 100644 --- a/src/smt_util/nary_builder.cpp +++ b/src/smt_util/nary_builder.cpp @@ -20,7 +20,7 @@ using namespace std; -namespace CVC4 { +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 */ -}/* CVC4 namespace */ +} // namespace CVC5 diff --git a/src/smt_util/nary_builder.h b/src/smt_util/nary_builder.h index 54fa59edb..dc8a428d0 100644 --- a/src/smt_util/nary_builder.h +++ b/src/smt_util/nary_builder.h @@ -24,7 +24,7 @@ #include "expr/node.h" -namespace CVC4{ +namespace CVC5 { namespace util { class NaryBuilder { @@ -53,4 +53,4 @@ private: };/* class RePairAssocCommutativeOperators */ }/* util namespace */ -}/* CVC4 namespace */ +} // namespace CVC5 |