diff options
author | Aina Niemetz <aina.niemetz@gmail.com> | 2021-04-01 09:56:14 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-04-01 16:56:14 +0000 |
commit | 05a53a2ac405bcd18a84024247145f161809c3b0 (patch) | |
tree | 34241c0a82f79d717ddbfbb0c294f9a09c7edb0c /src/theory/bags | |
parent | afaf4413775ff7d6054a5893f1397ad908e0773c (diff) |
Rename namespace CVC5 to cvc5. (#6258)
Diffstat (limited to 'src/theory/bags')
29 files changed, 93 insertions, 93 deletions
diff --git a/src/theory/bags/bag_solver.cpp b/src/theory/bags/bag_solver.cpp index fd80a03f7..478ce58cd 100644 --- a/src/theory/bags/bag_solver.cpp +++ b/src/theory/bags/bag_solver.cpp @@ -24,10 +24,10 @@ #include "theory/uf/equality_engine_iterator.h" using namespace std; -using namespace CVC5::context; -using namespace CVC5::kind; +using namespace cvc5::context; +using namespace cvc5::kind; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace bags { @@ -212,4 +212,4 @@ void BagSolver::checkDisequalBagTerms() } // namespace bags } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/bags/bag_solver.h b/src/theory/bags/bag_solver.h index 9d0e597dd..5cd7ed338 100644 --- a/src/theory/bags/bag_solver.h +++ b/src/theory/bags/bag_solver.h @@ -19,7 +19,7 @@ #include "theory/bags/inference_generator.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace bags { @@ -90,6 +90,6 @@ class BagSolver } // namespace bags } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__THEORY__BAG__SOLVER_H */ diff --git a/src/theory/bags/bags_rewriter.cpp b/src/theory/bags/bags_rewriter.cpp index ccee08aab..f4670f8be 100644 --- a/src/theory/bags/bags_rewriter.cpp +++ b/src/theory/bags/bags_rewriter.cpp @@ -16,9 +16,9 @@ #include "theory/bags/normal_form.h" -using namespace CVC5::kind; +using namespace cvc5::kind; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace bags { @@ -503,4 +503,4 @@ BagsRewriteResponse BagsRewriter::postRewriteEqual(const TNode& n) const } // namespace bags } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/bags/bags_rewriter.h b/src/theory/bags/bags_rewriter.h index 4552ed9da..bc66d7efa 100644 --- a/src/theory/bags/bags_rewriter.h +++ b/src/theory/bags/bags_rewriter.h @@ -22,7 +22,7 @@ #include "util/statistics_registry.h" #include "util/stats_histogram.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace bags { @@ -223,6 +223,6 @@ class BagsRewriter : public TheoryRewriter } // namespace bags } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__THEORY__BAGS__THEORY_BAGS_REWRITER_H */ diff --git a/src/theory/bags/bags_statistics.cpp b/src/theory/bags/bags_statistics.cpp index 369831c70..6c88ffb43 100644 --- a/src/theory/bags/bags_statistics.cpp +++ b/src/theory/bags/bags_statistics.cpp @@ -16,7 +16,7 @@ #include "smt/smt_statistics_registry.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace bags { @@ -32,4 +32,4 @@ BagsStatistics::~BagsStatistics() } // namespace bags } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/bags/bags_statistics.h b/src/theory/bags/bags_statistics.h index e0a1c4133..ac60fbc3e 100644 --- a/src/theory/bags/bags_statistics.h +++ b/src/theory/bags/bags_statistics.h @@ -21,7 +21,7 @@ #include "util/statistics_registry.h" #include "util/stats_histogram.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace bags { @@ -40,6 +40,6 @@ class BagsStatistics } // namespace bags } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__THEORY__BAGS_STATISTICS_H */ diff --git a/src/theory/bags/infer_info.cpp b/src/theory/bags/infer_info.cpp index 444597eb5..c0fac0753 100644 --- a/src/theory/bags/infer_info.cpp +++ b/src/theory/bags/infer_info.cpp @@ -16,7 +16,7 @@ #include "theory/bags/inference_manager.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace bags { @@ -79,4 +79,4 @@ std::ostream& operator<<(std::ostream& out, const InferInfo& ii) } // namespace bags } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/bags/infer_info.h b/src/theory/bags/infer_info.h index 18765bbe7..508c49fe5 100644 --- a/src/theory/bags/infer_info.h +++ b/src/theory/bags/infer_info.h @@ -24,7 +24,7 @@ #include "theory/inference_id.h" #include "theory/theory_inference.h" -namespace CVC5 { +namespace cvc5 { namespace theory { class TheoryInferenceManager; @@ -85,6 +85,6 @@ std::ostream& operator<<(std::ostream& out, const InferInfo& ii); } // namespace bags } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__THEORY__BAGS__INFER_INFO_H */ diff --git a/src/theory/bags/inference_generator.cpp b/src/theory/bags/inference_generator.cpp index 2f6a36b9c..57a306820 100644 --- a/src/theory/bags/inference_generator.cpp +++ b/src/theory/bags/inference_generator.cpp @@ -21,7 +21,7 @@ #include "theory/bags/solver_state.h" #include "theory/uf/equality_engine.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace bags { @@ -270,4 +270,4 @@ Node InferenceGenerator::getMultiplicityTerm(Node element, Node bag) } // namespace bags } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/bags/inference_generator.h b/src/theory/bags/inference_generator.h index 4f0b498c2..baa391f38 100644 --- a/src/theory/bags/inference_generator.h +++ b/src/theory/bags/inference_generator.h @@ -20,7 +20,7 @@ #include "expr/node.h" #include "infer_info.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace bags { @@ -188,6 +188,6 @@ class InferenceGenerator } // namespace bags } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__THEORY__BAGS__INFERENCE_GENERATOR_H */ diff --git a/src/theory/bags/inference_manager.cpp b/src/theory/bags/inference_manager.cpp index 3fa425f7a..422fb53d0 100644 --- a/src/theory/bags/inference_manager.cpp +++ b/src/theory/bags/inference_manager.cpp @@ -17,9 +17,9 @@ #include "theory/bags/solver_state.h" using namespace std; -using namespace CVC5::kind; +using namespace cvc5::kind; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace bags { @@ -48,4 +48,4 @@ void InferenceManager::doPending() } // namespace bags } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/bags/inference_manager.h b/src/theory/bags/inference_manager.h index 34f6621aa..68d923889 100644 --- a/src/theory/bags/inference_manager.h +++ b/src/theory/bags/inference_manager.h @@ -19,7 +19,7 @@ #include "theory/inference_manager_buffered.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace bags { @@ -63,6 +63,6 @@ class InferenceManager : public InferenceManagerBuffered } // namespace bags } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__THEORY__BAGS__INFERENCE_MANAGER_H */ diff --git a/src/theory/bags/kinds b/src/theory/bags/kinds index dd8eacfb5..038e7dd7f 100644 --- a/src/theory/bags/kinds +++ b/src/theory/bags/kinds @@ -5,10 +5,10 @@ # theory THEORY_BAGS \ - ::CVC5::theory::bags::TheoryBags \ + ::cvc5::theory::bags::TheoryBags \ "theory/bags/theory_bags.h" typechecker "theory/bags/theory_bags_type_rules.h" -rewriter ::CVC5::theory::bags::BagsRewriter \ +rewriter ::cvc5::theory::bags::BagsRewriter \ "theory/bags/bags_rewriter.h" properties parametric @@ -16,22 +16,22 @@ properties check presolve # constants constant EMPTYBAG \ - ::CVC5::EmptyBag \ - ::CVC5::EmptyBagHashFunction \ + ::cvc5::EmptyBag \ + ::cvc5::EmptyBagHashFunction \ "expr/emptybag.h" \ - "the empty bag constant; payload is an instance of the CVC5::EmptyBag class" + "the empty bag constant; payload is an instance of the cvc5::EmptyBag class" # the type operator BAG_TYPE 1 "bag type, takes as parameter the type of the elements" cardinality BAG_TYPE \ - "::CVC5::theory::bags::BagsProperties::computeCardinality(%TYPE%)" \ + "::cvc5::theory::bags::BagsProperties::computeCardinality(%TYPE%)" \ "theory/bags/theory_bags_type_rules.h" well-founded BAG_TYPE \ - "::CVC5::theory::bags::BagsProperties::isWellFounded(%TYPE%)" \ - "::CVC5::theory::bags::BagsProperties::mkGroundTerm(%TYPE%)" \ + "::cvc5::theory::bags::BagsProperties::isWellFounded(%TYPE%)" \ + "::cvc5::theory::bags::BagsProperties::mkGroundTerm(%TYPE%)" \ "theory/bags/theory_bags_type_rules.h" enumerator BAG_TYPE \ - "::CVC5::theory::bags::BagEnumerator" \ + "::cvc5::theory::bags::BagEnumerator" \ "theory/bags/theory_bags_type_enumerator.h" # operators @@ -50,10 +50,10 @@ operator BAG_COUNT 2 "multiplicity of an element in a bag" operator DUPLICATE_REMOVAL 1 "eliminate duplicates in a bag (also known as the delta operator,or the squash operator)" constant MK_BAG_OP \ - ::CVC5::MakeBagOp \ - ::CVC5::MakeBagOpHashFunction \ + ::cvc5::MakeBagOp \ + ::cvc5::MakeBagOpHashFunction \ "theory/bags/make_bag_op.h" \ - "operator for MK_BAG; payload is an instance of the CVC5::MakeBagOp class" + "operator for MK_BAG; payload is an instance of the cvc5::MakeBagOp class" parameterized MK_BAG MK_BAG_OP 2 \ "constructs a bag from one element along with its multiplicity" @@ -70,24 +70,24 @@ operator BAG_TO_SET 1 "converts a bag to a set" # If the bag has cardinality > 1, then (choose A) will deterministically return an element in A. operator BAG_CHOOSE 1 "return an element in the bag given as a parameter" -typerule UNION_MAX ::CVC5::theory::bags::BinaryOperatorTypeRule -typerule UNION_DISJOINT ::CVC5::theory::bags::BinaryOperatorTypeRule -typerule INTERSECTION_MIN ::CVC5::theory::bags::BinaryOperatorTypeRule -typerule DIFFERENCE_SUBTRACT ::CVC5::theory::bags::BinaryOperatorTypeRule -typerule DIFFERENCE_REMOVE ::CVC5::theory::bags::BinaryOperatorTypeRule -typerule SUBBAG ::CVC5::theory::bags::SubBagTypeRule -typerule BAG_COUNT ::CVC5::theory::bags::CountTypeRule -typerule DUPLICATE_REMOVAL ::CVC5::theory::bags::DuplicateRemovalTypeRule +typerule UNION_MAX ::cvc5::theory::bags::BinaryOperatorTypeRule +typerule UNION_DISJOINT ::cvc5::theory::bags::BinaryOperatorTypeRule +typerule INTERSECTION_MIN ::cvc5::theory::bags::BinaryOperatorTypeRule +typerule DIFFERENCE_SUBTRACT ::cvc5::theory::bags::BinaryOperatorTypeRule +typerule DIFFERENCE_REMOVE ::cvc5::theory::bags::BinaryOperatorTypeRule +typerule SUBBAG ::cvc5::theory::bags::SubBagTypeRule +typerule BAG_COUNT ::cvc5::theory::bags::CountTypeRule +typerule DUPLICATE_REMOVAL ::cvc5::theory::bags::DuplicateRemovalTypeRule typerule MK_BAG_OP "SimpleTypeRule<RBuiltinOperator>" -typerule MK_BAG ::CVC5::theory::bags::MkBagTypeRule -typerule EMPTYBAG ::CVC5::theory::bags::EmptyBagTypeRule -typerule BAG_CARD ::CVC5::theory::bags::CardTypeRule -typerule BAG_CHOOSE ::CVC5::theory::bags::ChooseTypeRule -typerule BAG_IS_SINGLETON ::CVC5::theory::bags::IsSingletonTypeRule -typerule BAG_FROM_SET ::CVC5::theory::bags::FromSetTypeRule -typerule BAG_TO_SET ::CVC5::theory::bags::ToSetTypeRule +typerule MK_BAG ::cvc5::theory::bags::MkBagTypeRule +typerule EMPTYBAG ::cvc5::theory::bags::EmptyBagTypeRule +typerule BAG_CARD ::cvc5::theory::bags::CardTypeRule +typerule BAG_CHOOSE ::cvc5::theory::bags::ChooseTypeRule +typerule BAG_IS_SINGLETON ::cvc5::theory::bags::IsSingletonTypeRule +typerule BAG_FROM_SET ::cvc5::theory::bags::FromSetTypeRule +typerule BAG_TO_SET ::cvc5::theory::bags::ToSetTypeRule -construle UNION_DISJOINT ::CVC5::theory::bags::BinaryOperatorTypeRule -construle MK_BAG ::CVC5::theory::bags::MkBagTypeRule +construle UNION_DISJOINT ::cvc5::theory::bags::BinaryOperatorTypeRule +construle MK_BAG ::cvc5::theory::bags::MkBagTypeRule endtheory diff --git a/src/theory/bags/make_bag_op.cpp b/src/theory/bags/make_bag_op.cpp index 15e3a30c7..168379390 100644 --- a/src/theory/bags/make_bag_op.cpp +++ b/src/theory/bags/make_bag_op.cpp @@ -18,7 +18,7 @@ #include "expr/type_node.h" -namespace CVC5 { +namespace cvc5 { std::ostream& operator<<(std::ostream& out, const MakeBagOp& op) { @@ -46,4 +46,4 @@ bool MakeBagOp::operator==(const MakeBagOp& op) const return getType() == op.getType(); } -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/bags/make_bag_op.h b/src/theory/bags/make_bag_op.h index 4c2a3e933..44b105225 100644 --- a/src/theory/bags/make_bag_op.h +++ b/src/theory/bags/make_bag_op.h @@ -19,7 +19,7 @@ #include <memory> -namespace CVC5 { +namespace cvc5 { class TypeNode; @@ -57,6 +57,6 @@ struct MakeBagOpHashFunction size_t operator()(const MakeBagOp& op) const; }; /* struct MakeBagOpHashFunction */ -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__MAKE_BAG_OP_H */ diff --git a/src/theory/bags/normal_form.cpp b/src/theory/bags/normal_form.cpp index 5952b66d8..1773346f0 100644 --- a/src/theory/bags/normal_form.cpp +++ b/src/theory/bags/normal_form.cpp @@ -16,9 +16,9 @@ #include "theory/sets/normal_form.h" #include "theory/type_enumerator.h" -using namespace CVC5::kind; +using namespace cvc5::kind; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace bags { @@ -674,4 +674,4 @@ Node NormalForm::evaluateToSet(TNode n) } // namespace bags } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/bags/normal_form.h b/src/theory/bags/normal_form.h index 1c7f05d8e..5b5591133 100644 --- a/src/theory/bags/normal_form.h +++ b/src/theory/bags/normal_form.h @@ -19,7 +19,7 @@ #ifndef CVC4__THEORY__BAGS__NORMAL_FORM_H #define CVC4__THEORY__BAGS__NORMAL_FORM_H -namespace CVC5 { +namespace cvc5 { namespace theory { namespace bags { @@ -192,6 +192,6 @@ class NormalForm }; } // namespace bags } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__THEORY__BAGS__NORMAL_FORM_H */ diff --git a/src/theory/bags/rewrites.cpp b/src/theory/bags/rewrites.cpp index d0299d52a..4d6929346 100644 --- a/src/theory/bags/rewrites.cpp +++ b/src/theory/bags/rewrites.cpp @@ -16,7 +16,7 @@ #include <iostream> -namespace CVC5 { +namespace cvc5 { namespace theory { namespace bags { @@ -79,4 +79,4 @@ std::ostream& operator<<(std::ostream& out, Rewrite r) } // namespace bags } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/bags/rewrites.h b/src/theory/bags/rewrites.h index 9e7bb54fa..aa49c71fb 100644 --- a/src/theory/bags/rewrites.h +++ b/src/theory/bags/rewrites.h @@ -19,7 +19,7 @@ #include <iosfwd> -namespace CVC5 { +namespace cvc5 { namespace theory { namespace bags { @@ -92,6 +92,6 @@ std::ostream& operator<<(std::ostream& out, Rewrite r); } // namespace bags } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__THEORY__BAGS__REWRITES_H */ diff --git a/src/theory/bags/solver_state.cpp b/src/theory/bags/solver_state.cpp index 4011a3fc4..aa714a61b 100644 --- a/src/theory/bags/solver_state.cpp +++ b/src/theory/bags/solver_state.cpp @@ -20,9 +20,9 @@ #include "theory/uf/equality_engine.h" using namespace std; -using namespace CVC5::kind; +using namespace cvc5::kind; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace bags { @@ -136,4 +136,4 @@ void SolverState::collectDisequalBagTerms() } // namespace bags } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/bags/solver_state.h b/src/theory/bags/solver_state.h index e6b2a2504..e7c09db8f 100644 --- a/src/theory/bags/solver_state.h +++ b/src/theory/bags/solver_state.h @@ -21,7 +21,7 @@ #include "theory/theory_state.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace bags { @@ -90,6 +90,6 @@ class SolverState : public TheoryState } // namespace bags } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__THEORY__BAGS__THEORY_SOLVER_STATE_H */ diff --git a/src/theory/bags/term_registry.cpp b/src/theory/bags/term_registry.cpp index 072655834..dd3820c82 100644 --- a/src/theory/bags/term_registry.cpp +++ b/src/theory/bags/term_registry.cpp @@ -18,9 +18,9 @@ #include "theory/bags/solver_state.h" using namespace std; -using namespace CVC5::kind; +using namespace cvc5::kind; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace bags { @@ -45,4 +45,4 @@ Node TermRegistry::getEmptyBag(TypeNode tn) } // namespace bags } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/bags/term_registry.h b/src/theory/bags/term_registry.h index adf97fd5f..ab519b100 100644 --- a/src/theory/bags/term_registry.h +++ b/src/theory/bags/term_registry.h @@ -22,7 +22,7 @@ #include "context/cdhashmap.h" #include "expr/node.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace bags { @@ -59,6 +59,6 @@ class TermRegistry } // namespace bags } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__THEORY__BAGS__TERM_REGISTRY_H */ diff --git a/src/theory/bags/theory_bags.cpp b/src/theory/bags/theory_bags.cpp index f91fd40f0..bea83ce40 100644 --- a/src/theory/bags/theory_bags.cpp +++ b/src/theory/bags/theory_bags.cpp @@ -19,9 +19,9 @@ #include "theory/rewriter.h" #include "theory/theory_model.h" -using namespace CVC5::kind; +using namespace cvc5::kind; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace bags { @@ -262,4 +262,4 @@ void TheoryBags::NotifyClass::eqNotifyDisequal(TNode n1, TNode n2, TNode reason) } // namespace bags } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/bags/theory_bags.h b/src/theory/bags/theory_bags.h index 6bd9ddc65..7bb6111bd 100644 --- a/src/theory/bags/theory_bags.h +++ b/src/theory/bags/theory_bags.h @@ -27,7 +27,7 @@ #include "theory/theory.h" #include "theory/theory_eq_notify.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace bags { @@ -114,6 +114,6 @@ class TheoryBags : public Theory } // namespace bags } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__THEORY__BAGS__THEORY_BAGS_H */ diff --git a/src/theory/bags/theory_bags_type_enumerator.cpp b/src/theory/bags/theory_bags_type_enumerator.cpp index 02494727c..f34d304fb 100644 --- a/src/theory/bags/theory_bags_type_enumerator.cpp +++ b/src/theory/bags/theory_bags_type_enumerator.cpp @@ -18,7 +18,7 @@ #include "theory/rewriter.h" #include "theory_bags_type_enumerator.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace bags { @@ -83,4 +83,4 @@ bool BagEnumerator::isFinished() } // namespace bags } // namespace theory -} // namespace CVC5
\ No newline at end of file +} // namespace cvc5
\ No newline at end of file diff --git a/src/theory/bags/theory_bags_type_enumerator.h b/src/theory/bags/theory_bags_type_enumerator.h index c13946388..bdf57213d 100644 --- a/src/theory/bags/theory_bags_type_enumerator.h +++ b/src/theory/bags/theory_bags_type_enumerator.h @@ -20,7 +20,7 @@ #include "expr/type_node.h" #include "theory/type_enumerator.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace bags { @@ -86,6 +86,6 @@ class BagEnumerator : public TypeEnumeratorBase<BagEnumerator> } // namespace bags } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__THEORY__BAGS__TYPE_ENUMERATOR_H */
\ No newline at end of file diff --git a/src/theory/bags/theory_bags_type_rules.cpp b/src/theory/bags/theory_bags_type_rules.cpp index 2acbb1e27..f198d68e9 100644 --- a/src/theory/bags/theory_bags_type_rules.cpp +++ b/src/theory/bags/theory_bags_type_rules.cpp @@ -19,7 +19,7 @@ #include "base/check.h" #include "theory/bags/normal_form.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace bags { @@ -279,4 +279,4 @@ TypeNode ToSetTypeRule::computeType(NodeManager* nodeManager, } } // namespace bags } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/bags/theory_bags_type_rules.h b/src/theory/bags/theory_bags_type_rules.h index dd93186ad..f48001c5e 100644 --- a/src/theory/bags/theory_bags_type_rules.h +++ b/src/theory/bags/theory_bags_type_rules.h @@ -20,7 +20,7 @@ #include "expr/node.h" #include "expr/type_node.h" -namespace CVC5 { +namespace cvc5 { class NodeManager; @@ -102,6 +102,6 @@ struct BagsProperties } // namespace bags } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__THEORY__BAGS__THEORY_BAGS_TYPE_RULES_H */ |