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/theory/bags | |
parent | f9a9af855fb65804ff0b36e764ccd9d0fa9f87f8 (diff) |
Rename namespace CVC4 to CVC5. (#6249)
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 a7a0f8796..fd80a03f7 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 CVC4::context; -using namespace CVC4::kind; +using namespace CVC5::context; +using namespace CVC5::kind; -namespace CVC4 { +namespace CVC5 { namespace theory { namespace bags { @@ -212,4 +212,4 @@ void BagSolver::checkDisequalBagTerms() } // namespace bags } // namespace theory -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/theory/bags/bag_solver.h b/src/theory/bags/bag_solver.h index 914a12ae2..9d0e597dd 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 CVC4 { +namespace CVC5 { namespace theory { namespace bags { @@ -90,6 +90,6 @@ class BagSolver } // namespace bags } // namespace theory -} // namespace CVC4 +} // 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 54b279e66..ccee08aab 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 CVC4::kind; +using namespace CVC5::kind; -namespace CVC4 { +namespace CVC5 { namespace theory { namespace bags { @@ -503,4 +503,4 @@ BagsRewriteResponse BagsRewriter::postRewriteEqual(const TNode& n) const } // namespace bags } // namespace theory -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/theory/bags/bags_rewriter.h b/src/theory/bags/bags_rewriter.h index 6c440c512..4552ed9da 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 CVC4 { +namespace CVC5 { namespace theory { namespace bags { @@ -223,6 +223,6 @@ class BagsRewriter : public TheoryRewriter } // namespace bags } // namespace theory -} // namespace CVC4 +} // 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 8ec686d87..369831c70 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 CVC4 { +namespace CVC5 { namespace theory { namespace bags { @@ -32,4 +32,4 @@ BagsStatistics::~BagsStatistics() } // namespace bags } // namespace theory -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/theory/bags/bags_statistics.h b/src/theory/bags/bags_statistics.h index c8f7ed420..e0a1c4133 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 CVC4 { +namespace CVC5 { namespace theory { namespace bags { @@ -40,6 +40,6 @@ class BagsStatistics } // namespace bags } // namespace theory -} // namespace CVC4 +} // 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 d7638c89c..444597eb5 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 CVC4 { +namespace CVC5 { namespace theory { namespace bags { @@ -79,4 +79,4 @@ std::ostream& operator<<(std::ostream& out, const InferInfo& ii) } // namespace bags } // namespace theory -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/theory/bags/infer_info.h b/src/theory/bags/infer_info.h index c76f74c0c..18765bbe7 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 CVC4 { +namespace CVC5 { namespace theory { class TheoryInferenceManager; @@ -85,6 +85,6 @@ std::ostream& operator<<(std::ostream& out, const InferInfo& ii); } // namespace bags } // namespace theory -} // namespace CVC4 +} // 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 0d56080c4..2f6a36b9c 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 CVC4 { +namespace CVC5 { namespace theory { namespace bags { @@ -270,4 +270,4 @@ Node InferenceGenerator::getMultiplicityTerm(Node element, Node bag) } // namespace bags } // namespace theory -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/theory/bags/inference_generator.h b/src/theory/bags/inference_generator.h index bfaf5d0fc..4f0b498c2 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 CVC4 { +namespace CVC5 { namespace theory { namespace bags { @@ -188,6 +188,6 @@ class InferenceGenerator } // namespace bags } // namespace theory -} // namespace CVC4 +} // 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 dcc5387e9..3fa425f7a 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 CVC4::kind; +using namespace CVC5::kind; -namespace CVC4 { +namespace CVC5 { namespace theory { namespace bags { @@ -48,4 +48,4 @@ void InferenceManager::doPending() } // namespace bags } // namespace theory -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/theory/bags/inference_manager.h b/src/theory/bags/inference_manager.h index d74d3c189..34f6621aa 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 CVC4 { +namespace CVC5 { namespace theory { namespace bags { @@ -63,6 +63,6 @@ class InferenceManager : public InferenceManagerBuffered } // namespace bags } // namespace theory -} // namespace CVC4 +} // namespace CVC5 #endif /* CVC4__THEORY__BAGS__INFERENCE_MANAGER_H */ diff --git a/src/theory/bags/kinds b/src/theory/bags/kinds index f84b811e7..cd53484eb 100644 --- a/src/theory/bags/kinds +++ b/src/theory/bags/kinds @@ -5,10 +5,10 @@ # theory THEORY_BAGS \ - ::CVC4::theory::bags::TheoryBags \ + ::CVC5::theory::bags::TheoryBags \ "theory/bags/theory_bags.h" typechecker "theory/bags/theory_bags_type_rules.h" -rewriter ::CVC4::theory::bags::BagsRewriter \ +rewriter ::CVC5::theory::bags::BagsRewriter \ "theory/bags/bags_rewriter.h" properties parametric @@ -16,22 +16,22 @@ properties check propagate presolve # constants constant EMPTYBAG \ - ::CVC4::EmptyBag \ - ::CVC4::EmptyBagHashFunction \ + ::CVC5::EmptyBag \ + ::CVC5::EmptyBagHashFunction \ "expr/emptybag.h" \ - "the empty bag constant; payload is an instance of the CVC4::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 \ - "::CVC4::theory::bags::BagsProperties::computeCardinality(%TYPE%)" \ + "::CVC5::theory::bags::BagsProperties::computeCardinality(%TYPE%)" \ "theory/bags/theory_bags_type_rules.h" well-founded BAG_TYPE \ - "::CVC4::theory::bags::BagsProperties::isWellFounded(%TYPE%)" \ - "::CVC4::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 \ - "::CVC4::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 \ - ::CVC4::MakeBagOp \ - ::CVC4::MakeBagOpHashFunction \ + ::CVC5::MakeBagOp \ + ::CVC5::MakeBagOpHashFunction \ "theory/bags/make_bag_op.h" \ - "operator for MK_BAG; payload is an instance of the CVC4::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 ::CVC4::theory::bags::BinaryOperatorTypeRule -typerule UNION_DISJOINT ::CVC4::theory::bags::BinaryOperatorTypeRule -typerule INTERSECTION_MIN ::CVC4::theory::bags::BinaryOperatorTypeRule -typerule DIFFERENCE_SUBTRACT ::CVC4::theory::bags::BinaryOperatorTypeRule -typerule DIFFERENCE_REMOVE ::CVC4::theory::bags::BinaryOperatorTypeRule -typerule SUBBAG ::CVC4::theory::bags::SubBagTypeRule -typerule BAG_COUNT ::CVC4::theory::bags::CountTypeRule -typerule DUPLICATE_REMOVAL ::CVC4::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 ::CVC4::theory::bags::MkBagTypeRule -typerule EMPTYBAG ::CVC4::theory::bags::EmptyBagTypeRule -typerule BAG_CARD ::CVC4::theory::bags::CardTypeRule -typerule BAG_CHOOSE ::CVC4::theory::bags::ChooseTypeRule -typerule BAG_IS_SINGLETON ::CVC4::theory::bags::IsSingletonTypeRule -typerule BAG_FROM_SET ::CVC4::theory::bags::FromSetTypeRule -typerule BAG_TO_SET ::CVC4::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 ::CVC4::theory::bags::BinaryOperatorTypeRule -construle MK_BAG ::CVC4::theory::bags::MkBagTypeRule +construle UNION_DISJOINT ::CVC5::theory::bags::BinaryOperatorTypeRule +construle MK_BAG ::CVC5::theory::bags::MkBagTypeRule endtheory
\ No newline at end of file diff --git a/src/theory/bags/make_bag_op.cpp b/src/theory/bags/make_bag_op.cpp index 92cf49203..15e3a30c7 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 CVC4 { +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 CVC4 +} // namespace CVC5 diff --git a/src/theory/bags/make_bag_op.h b/src/theory/bags/make_bag_op.h index e8610e7db..4c2a3e933 100644 --- a/src/theory/bags/make_bag_op.h +++ b/src/theory/bags/make_bag_op.h @@ -19,7 +19,7 @@ #include <memory> -namespace CVC4 { +namespace CVC5 { class TypeNode; @@ -57,6 +57,6 @@ struct MakeBagOpHashFunction size_t operator()(const MakeBagOp& op) const; }; /* struct MakeBagOpHashFunction */ -} // namespace CVC4 +} // 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 ad723d293..5952b66d8 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 CVC4::kind; +using namespace CVC5::kind; -namespace CVC4 { +namespace CVC5 { namespace theory { namespace bags { @@ -674,4 +674,4 @@ Node NormalForm::evaluateToSet(TNode n) } // namespace bags } // namespace theory -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/theory/bags/normal_form.h b/src/theory/bags/normal_form.h index a779d3321..1c7f05d8e 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 CVC4 { +namespace CVC5 { namespace theory { namespace bags { @@ -192,6 +192,6 @@ class NormalForm }; } // namespace bags } // namespace theory -} // namespace CVC4 +} // namespace CVC5 #endif /* CVC4__THEORY__BAGS__NORMAL_FORM_H */ diff --git a/src/theory/bags/rewrites.cpp b/src/theory/bags/rewrites.cpp index ab2ca2901..d0299d52a 100644 --- a/src/theory/bags/rewrites.cpp +++ b/src/theory/bags/rewrites.cpp @@ -16,7 +16,7 @@ #include <iostream> -namespace CVC4 { +namespace CVC5 { namespace theory { namespace bags { @@ -79,4 +79,4 @@ std::ostream& operator<<(std::ostream& out, Rewrite r) } // namespace bags } // namespace theory -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/theory/bags/rewrites.h b/src/theory/bags/rewrites.h index 5d0b8a087..9e7bb54fa 100644 --- a/src/theory/bags/rewrites.h +++ b/src/theory/bags/rewrites.h @@ -19,7 +19,7 @@ #include <iosfwd> -namespace CVC4 { +namespace CVC5 { namespace theory { namespace bags { @@ -92,6 +92,6 @@ std::ostream& operator<<(std::ostream& out, Rewrite r); } // namespace bags } // namespace theory -} // namespace CVC4 +} // 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 4fead8ab7..4011a3fc4 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 CVC4::kind; +using namespace CVC5::kind; -namespace CVC4 { +namespace CVC5 { namespace theory { namespace bags { @@ -136,4 +136,4 @@ void SolverState::collectDisequalBagTerms() } // namespace bags } // namespace theory -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/theory/bags/solver_state.h b/src/theory/bags/solver_state.h index d8820d8c4..e6b2a2504 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 CVC4 { +namespace CVC5 { namespace theory { namespace bags { @@ -90,6 +90,6 @@ class SolverState : public TheoryState } // namespace bags } // namespace theory -} // namespace CVC4 +} // 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 192fd6809..072655834 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 CVC4::kind; +using namespace CVC5::kind; -namespace CVC4 { +namespace CVC5 { namespace theory { namespace bags { @@ -45,4 +45,4 @@ Node TermRegistry::getEmptyBag(TypeNode tn) } // namespace bags } // namespace theory -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/theory/bags/term_registry.h b/src/theory/bags/term_registry.h index 87e61a026..adf97fd5f 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 CVC4 { +namespace CVC5 { namespace theory { namespace bags { @@ -59,6 +59,6 @@ class TermRegistry } // namespace bags } // namespace theory -} // namespace CVC4 +} // 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 2950739e4..f91fd40f0 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 CVC4::kind; +using namespace CVC5::kind; -namespace CVC4 { +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 CVC4 +} // namespace CVC5 diff --git a/src/theory/bags/theory_bags.h b/src/theory/bags/theory_bags.h index df64c3f1c..6bd9ddc65 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 CVC4 { +namespace CVC5 { namespace theory { namespace bags { @@ -114,6 +114,6 @@ class TheoryBags : public Theory } // namespace bags } // namespace theory -} // namespace CVC4 +} // 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 d9284b862..02494727c 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 CVC4 { +namespace CVC5 { namespace theory { namespace bags { @@ -83,4 +83,4 @@ bool BagEnumerator::isFinished() } // namespace bags } // namespace theory -} // namespace CVC4
\ 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 aa59a72e6..c13946388 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 CVC4 { +namespace CVC5 { namespace theory { namespace bags { @@ -86,6 +86,6 @@ class BagEnumerator : public TypeEnumeratorBase<BagEnumerator> } // namespace bags } // namespace theory -} // namespace CVC4 +} // 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 5a97155fc..2acbb1e27 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 CVC4 { +namespace CVC5 { namespace theory { namespace bags { @@ -279,4 +279,4 @@ TypeNode ToSetTypeRule::computeType(NodeManager* nodeManager, } } // namespace bags } // namespace theory -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/theory/bags/theory_bags_type_rules.h b/src/theory/bags/theory_bags_type_rules.h index 41e1164c2..dd93186ad 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 CVC4 { +namespace CVC5 { class NodeManager; @@ -102,6 +102,6 @@ struct BagsProperties } // namespace bags } // namespace theory -} // namespace CVC4 +} // namespace CVC5 #endif /* CVC4__THEORY__BAGS__THEORY_BAGS_TYPE_RULES_H */ |