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/expr | |
parent | afaf4413775ff7d6054a5893f1397ad908e0773c (diff) |
Rename namespace CVC5 to cvc5. (#6258)
Diffstat (limited to 'src/expr')
115 files changed, 357 insertions, 357 deletions
diff --git a/src/expr/array_store_all.cpp b/src/expr/array_store_all.cpp index d50921598..b92ba8607 100644 --- a/src/expr/array_store_all.cpp +++ b/src/expr/array_store_all.cpp @@ -26,7 +26,7 @@ using namespace std; -namespace CVC5 { +namespace cvc5 { ArrayStoreAll::ArrayStoreAll(const TypeNode& type, const Node& value) : d_type(), d_value() @@ -115,4 +115,4 @@ size_t ArrayStoreAllHashFunction::operator()(const ArrayStoreAll& asa) const { * NodeHashFunction()(asa.getValue()); } -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/expr/array_store_all.h b/src/expr/array_store_all.h index 974f456ef..65385b0c4 100644 --- a/src/expr/array_store_all.h +++ b/src/expr/array_store_all.h @@ -24,7 +24,7 @@ #include <iosfwd> #include <memory> -namespace CVC5 { +namespace cvc5 { template <bool ref_count> class NodeTemplate; @@ -69,6 +69,6 @@ struct ArrayStoreAllHashFunction size_t operator()(const ArrayStoreAll& asa) const; }; /* struct ArrayStoreAllHashFunction */ -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__ARRAY_STORE_ALL_H */ diff --git a/src/expr/ascription_type.cpp b/src/expr/ascription_type.cpp index 6fecb2978..83254f5a5 100644 --- a/src/expr/ascription_type.cpp +++ b/src/expr/ascription_type.cpp @@ -18,7 +18,7 @@ #include "expr/type_node.h" -namespace CVC5 { +namespace cvc5 { AscriptionType::AscriptionType(TypeNode t) : d_type(new TypeNode(t)) {} @@ -55,4 +55,4 @@ std::ostream& operator<<(std::ostream& out, AscriptionType at) return out; } -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/expr/ascription_type.h b/src/expr/ascription_type.h index 5b0ff2b71..b216a0fa1 100644 --- a/src/expr/ascription_type.h +++ b/src/expr/ascription_type.h @@ -22,7 +22,7 @@ #include <iosfwd> #include <memory> -namespace CVC5 { +namespace cvc5 { class TypeNode; @@ -60,6 +60,6 @@ struct AscriptionTypeHashFunction /** An output routine for AscriptionTypes */ std::ostream& operator<<(std::ostream& out, AscriptionType at); -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__ASCRIPTION_TYPE_H */ diff --git a/src/expr/attribute.cpp b/src/expr/attribute.cpp index fe1bff897..062f0a2d2 100644 --- a/src/expr/attribute.cpp +++ b/src/expr/attribute.cpp @@ -22,7 +22,7 @@ using namespace std; -namespace CVC5 { +namespace cvc5 { namespace expr { namespace attr { @@ -116,4 +116,4 @@ void AttributeManager::deleteAttributes(const AttrIdVec& atids) { } // namespace attr } // namespace expr -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/expr/attribute.h b/src/expr/attribute.h index b3a3eb717..6156ccc2d 100644 --- a/src/expr/attribute.h +++ b/src/expr/attribute.h @@ -32,7 +32,7 @@ #include "expr/attribute_internals.h" #undef CVC4_ATTRIBUTE_H__INCLUDING__ATTRIBUTE_INTERNALS_H -namespace CVC5 { +namespace cvc5 { namespace expr { namespace attr { @@ -621,6 +621,6 @@ NodeManager::setAttribute(TypeNode n, const AttrKind&, d_attrManager->setAttribute(n.d_nv, AttrKind(), value); } -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__EXPR__ATTRIBUTE_H */ diff --git a/src/expr/attribute_internals.h b/src/expr/attribute_internals.h index bbd5455be..db3e57675 100644 --- a/src/expr/attribute_internals.h +++ b/src/expr/attribute_internals.h @@ -25,7 +25,7 @@ #include <unordered_map> -namespace CVC5 { +namespace cvc5 { namespace expr { // ATTRIBUTE HASH FUNCTIONS ==================================================== @@ -512,6 +512,6 @@ const uint64_t Attribute<T, bool, context_dep>::s_id = Attribute<T, bool, context_dep>::registerAttribute(); } // namespace expr -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__EXPR__ATTRIBUTE_INTERNALS_H */ diff --git a/src/expr/attribute_unique_id.h b/src/expr/attribute_unique_id.h index f084baaa1..b475a700d 100644 --- a/src/expr/attribute_unique_id.h +++ b/src/expr/attribute_unique_id.h @@ -21,7 +21,7 @@ // ATTRIBUTE IDs ============================================================ -namespace CVC5 { +namespace cvc5 { namespace expr { namespace attr { @@ -59,8 +59,8 @@ public: AttrTableId getTableId() const{ return d_tableId; } uint64_t getWithinTypeId() const{ return d_withinTypeId; } -}; /* CVC5::expr::attr::AttributeUniqueId */ +}; /* cvc5::expr::attr::AttributeUniqueId */ } // namespace attr } // namespace expr -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/expr/bound_var_manager.cpp b/src/expr/bound_var_manager.cpp index ca257d313..e97e559a8 100644 --- a/src/expr/bound_var_manager.cpp +++ b/src/expr/bound_var_manager.cpp @@ -16,7 +16,7 @@ #include "expr/node_manager_attributes.h" -namespace CVC5 { +namespace cvc5 { BoundVarManager::BoundVarManager() : d_keepCacheVals(false) {} @@ -53,4 +53,4 @@ Node BoundVarManager::getCacheValue(TNode cv, size_t i) return getCacheValue(cv, getCacheValue(i)); } -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/expr/bound_var_manager.h b/src/expr/bound_var_manager.h index 08705f6d2..ebd107737 100644 --- a/src/expr/bound_var_manager.h +++ b/src/expr/bound_var_manager.h @@ -22,7 +22,7 @@ #include "expr/node.h" -namespace CVC5 { +namespace cvc5 { /** * Bound variable manager. @@ -98,6 +98,6 @@ class BoundVarManager std::unordered_set<Node, NodeHashFunction> d_cacheVals; }; -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__EXPR__BOUND_VAR_MANAGER_H */ diff --git a/src/expr/buffered_proof_generator.cpp b/src/expr/buffered_proof_generator.cpp index caf6b0841..40820ea20 100644 --- a/src/expr/buffered_proof_generator.cpp +++ b/src/expr/buffered_proof_generator.cpp @@ -17,7 +17,7 @@ #include "expr/proof.h" #include "expr/proof_node_manager.h" -namespace CVC5 { +namespace cvc5 { BufferedProofGenerator::BufferedProofGenerator(context::Context* c, ProofNodeManager* pnm) @@ -80,4 +80,4 @@ std::shared_ptr<ProofNode> BufferedProofGenerator::getProofFor(Node fact) return cdp.getProofFor(fact); } -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/expr/buffered_proof_generator.h b/src/expr/buffered_proof_generator.h index db8e50274..7399b3741 100644 --- a/src/expr/buffered_proof_generator.h +++ b/src/expr/buffered_proof_generator.h @@ -20,7 +20,7 @@ #include "context/cdhashmap.h" #include "expr/proof_generator.h" -namespace CVC5 { +namespace cvc5 { class ProofNodeManager; class ProofStep; @@ -57,6 +57,6 @@ class BufferedProofGenerator : public ProofGenerator ProofNodeManager* d_pnm; }; -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__EXPR__BUFFERED_PROOF_GENERATOR_H */ diff --git a/src/expr/datatype_index.cpp b/src/expr/datatype_index.cpp index 2459c86d8..6f530529a 100644 --- a/src/expr/datatype_index.cpp +++ b/src/expr/datatype_index.cpp @@ -20,7 +20,7 @@ using namespace std; -namespace CVC5 { +namespace cvc5 { DatatypeIndexConstant::DatatypeIndexConstant(uint32_t index) : d_index(index) {} std::ostream& operator<<(std::ostream& out, const DatatypeIndexConstant& dic) @@ -34,4 +34,4 @@ size_t DatatypeIndexConstantHashFunction::operator()( return IntegerHashFunction()(dic.getIndex()); } -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/expr/datatype_index.h b/src/expr/datatype_index.h index 08d33ca83..a239c387b 100644 --- a/src/expr/datatype_index.h +++ b/src/expr/datatype_index.h @@ -19,7 +19,7 @@ #include <iosfwd> -namespace CVC5 { +namespace cvc5 { /* stores an index to Datatype residing in NodeManager */ class DatatypeIndexConstant @@ -64,6 +64,6 @@ struct DatatypeIndexConstantHashFunction size_t operator()(const DatatypeIndexConstant& dic) const; }; /* struct DatatypeIndexConstantHashFunction */ -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__DATATYPE_H */ diff --git a/src/expr/dtype.cpp b/src/expr/dtype.cpp index 35ad5ff4c..3302be018 100644 --- a/src/expr/dtype.cpp +++ b/src/expr/dtype.cpp @@ -19,9 +19,9 @@ #include "expr/node_algorithm.h" #include "expr/type_matcher.h" -using namespace CVC5::kind; +using namespace cvc5::kind; -namespace CVC5 { +namespace cvc5 { DType::DType(std::string name, bool isCo) : d_name(name), @@ -954,4 +954,4 @@ std::ostream& operator<<(std::ostream& out, const DTypeIndexConstant& dic) return out << "index_" << dic.getIndex(); } -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/expr/dtype.h b/src/expr/dtype.h index 5b6ec4a7d..524702bdd 100644 --- a/src/expr/dtype.h +++ b/src/expr/dtype.h @@ -24,7 +24,7 @@ #include "expr/node.h" #include "expr/type_node.h" -namespace CVC5 { +namespace cvc5 { // ----------------------- datatype attributes /** @@ -696,6 +696,6 @@ struct DTypeIndexConstantHashFunction std::ostream& operator<<(std::ostream& os, const DType& dt); -} // namespace CVC5 +} // namespace cvc5 #endif diff --git a/src/expr/dtype_cons.cpp b/src/expr/dtype_cons.cpp index 089d41637..59b870897 100644 --- a/src/expr/dtype_cons.cpp +++ b/src/expr/dtype_cons.cpp @@ -18,10 +18,10 @@ #include "expr/type_matcher.h" #include "options/datatypes_options.h" -using namespace CVC5::kind; -using namespace CVC5::theory; +using namespace cvc5::kind; +using namespace cvc5::theory; -namespace CVC5 { +namespace cvc5 { DTypeConstructor::DTypeConstructor(std::string name, unsigned weight) @@ -693,4 +693,4 @@ std::ostream& operator<<(std::ostream& os, const DTypeConstructor& ctor) return os; } -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/expr/dtype_cons.h b/src/expr/dtype_cons.h index 245d461b0..d444d9261 100644 --- a/src/expr/dtype_cons.h +++ b/src/expr/dtype_cons.h @@ -24,7 +24,7 @@ #include "expr/node.h" #include "expr/type_node.h" -namespace CVC5 { +namespace cvc5 { /** * The Node-level representation of a constructor for a datatype, which @@ -371,6 +371,6 @@ struct DTypeConstructorHashFunction std::ostream& operator<<(std::ostream& os, const DTypeConstructor& ctor); -} // namespace CVC5 +} // namespace cvc5 #endif diff --git a/src/expr/dtype_selector.cpp b/src/expr/dtype_selector.cpp index a276c3734..d6a3b4469 100644 --- a/src/expr/dtype_selector.cpp +++ b/src/expr/dtype_selector.cpp @@ -16,9 +16,9 @@ #include "options/set_language.h" -using namespace CVC5::kind; +using namespace cvc5::kind; -namespace CVC5 { +namespace cvc5 { DTypeSelector::DTypeSelector(std::string name, Node selector) : d_name(name), d_selector(selector), d_resolved(false) @@ -83,4 +83,4 @@ std::ostream& operator<<(std::ostream& os, const DTypeSelector& arg) return os; } -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/expr/dtype_selector.h b/src/expr/dtype_selector.h index 7404c0c96..d45bcf8c5 100644 --- a/src/expr/dtype_selector.h +++ b/src/expr/dtype_selector.h @@ -21,7 +21,7 @@ #include "expr/node.h" #include "expr/type_node.h" -namespace CVC5 { +namespace cvc5 { class DatatypeConstructorArg; class DType; @@ -90,6 +90,6 @@ class DTypeSelector std::ostream& operator<<(std::ostream& os, const DTypeSelector& arg); -} // namespace CVC5 +} // namespace cvc5 #endif diff --git a/src/expr/emptybag.cpp b/src/expr/emptybag.cpp index 0f7a3a73e..d45612a9c 100644 --- a/src/expr/emptybag.cpp +++ b/src/expr/emptybag.cpp @@ -18,7 +18,7 @@ #include "expr/type_node.h" -namespace CVC5 { +namespace cvc5 { std::ostream& operator<<(std::ostream& out, const EmptyBag& asa) { @@ -64,4 +64,4 @@ bool EmptyBag::operator<=(const EmptyBag& es) const bool EmptyBag::operator>(const EmptyBag& es) const { return !(*this <= es); } bool EmptyBag::operator>=(const EmptyBag& es) const { return !(*this < es); } -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/expr/emptybag.h b/src/expr/emptybag.h index 59060eaa8..f45bd9e96 100644 --- a/src/expr/emptybag.h +++ b/src/expr/emptybag.h @@ -20,7 +20,7 @@ #include <iosfwd> #include <memory> -namespace CVC5 { +namespace cvc5 { class TypeNode; @@ -58,6 +58,6 @@ struct EmptyBagHashFunction size_t operator()(const EmptyBag& es) const; }; /* struct EmptyBagHashFunction */ -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__EMPTY_BAG_H */ diff --git a/src/expr/emptyset.cpp b/src/expr/emptyset.cpp index 4a0bd4e51..4d6604a63 100644 --- a/src/expr/emptyset.cpp +++ b/src/expr/emptyset.cpp @@ -21,7 +21,7 @@ #include "expr/type_node.h" -namespace CVC5 { +namespace cvc5 { std::ostream& operator<<(std::ostream& out, const EmptySet& asa) { return out << "emptyset(" << asa.getType() << ')'; @@ -64,4 +64,4 @@ bool EmptySet::operator<=(const EmptySet& es) const bool EmptySet::operator>(const EmptySet& es) const { return !(*this <= es); } bool EmptySet::operator>=(const EmptySet& es) const { return !(*this < es); } -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/expr/emptyset.h b/src/expr/emptyset.h index febb4e111..aa6d5e143 100644 --- a/src/expr/emptyset.h +++ b/src/expr/emptyset.h @@ -23,7 +23,7 @@ #include <iosfwd> #include <memory> -namespace CVC5 { +namespace cvc5 { class TypeNode; @@ -60,6 +60,6 @@ struct EmptySetHashFunction size_t operator()(const EmptySet& es) const; }; /* struct EmptySetHashFunction */ -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__EMPTY_SET_H */ diff --git a/src/expr/expr_iomanip.cpp b/src/expr/expr_iomanip.cpp index 4aec28b85..4417ccb5c 100644 --- a/src/expr/expr_iomanip.cpp +++ b/src/expr/expr_iomanip.cpp @@ -22,7 +22,7 @@ #include "options/options.h" #include "options/expr_options.h" -namespace CVC5 { +namespace cvc5 { namespace expr { const int ExprSetDepth::s_iosIndex = std::ios_base::xalloc(); @@ -123,4 +123,4 @@ std::ostream& operator<<(std::ostream& out, ExprSetDepth sd) { } } // namespace expr -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/expr/expr_iomanip.h b/src/expr/expr_iomanip.h index c40840cd4..674d4c6fd 100644 --- a/src/expr/expr_iomanip.h +++ b/src/expr/expr_iomanip.h @@ -21,7 +21,7 @@ #include <iosfwd> -namespace CVC5 { +namespace cvc5 { namespace expr { /** @@ -173,6 +173,6 @@ std::ostream& operator<<(std::ostream& out, ExprSetDepth sd); } // namespace expr -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__EXPR__EXPR_IOMANIP_H */ diff --git a/src/expr/kind_map.h b/src/expr/kind_map.h index e6f6f9ca0..0716ff4d0 100644 --- a/src/expr/kind_map.h +++ b/src/expr/kind_map.h @@ -25,7 +25,7 @@ #include "base/check.h" #include "expr/kind.h" -namespace CVC5 { +namespace cvc5 { /** A very simple bitmap for Kinds */ class KindMap @@ -51,6 +51,6 @@ class KindMap std::bitset<kind::LAST_KIND> d_bits; }; -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__KIND_MAP_H */ diff --git a/src/expr/kind_template.cpp b/src/expr/kind_template.cpp index cbe979642..d9f913ddf 100644 --- a/src/expr/kind_template.cpp +++ b/src/expr/kind_template.cpp @@ -19,12 +19,12 @@ #include "expr/kind.h" -namespace CVC5 { +namespace cvc5 { namespace kind { -const char* toString(CVC5::Kind k) +const char* toString(cvc5::Kind k) { - using namespace CVC5::kind; + using namespace cvc5::kind; switch (k) { @@ -37,7 +37,7 @@ const char* toString(CVC5::Kind k) } } -std::ostream& operator<<(std::ostream& out, CVC5::Kind k) +std::ostream& operator<<(std::ostream& out, cvc5::Kind k) { out << toString(k); return out; @@ -47,7 +47,7 @@ std::ostream& operator<<(std::ostream& out, CVC5::Kind k) * 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) +bool isAssociative(::cvc5::Kind k) { switch(k) { case kind::AND: @@ -61,7 +61,7 @@ bool isAssociative(::CVC5::Kind k) } } -std::string kindToString(::CVC5::Kind k) +std::string kindToString(::cvc5::Kind k) { std::stringstream ss; ss << k; @@ -82,7 +82,7 @@ ${type_constant_descriptions} namespace theory { -TheoryId kindToTheoryId(::CVC5::Kind k) +TheoryId kindToTheoryId(::cvc5::Kind k) { switch(k) { case kind::UNDEFINED_KIND: @@ -95,7 +95,7 @@ ${kind_to_theory_id} throw IllegalArgumentException("", "k", __PRETTY_FUNCTION__, "bad kind"); } -TheoryId typeConstantToTheoryId(::CVC5::TypeConstant typeConstant) +TheoryId typeConstantToTheoryId(::cvc5::TypeConstant typeConstant) { switch (typeConstant) { @@ -107,4 +107,4 @@ ${type_constant_to_theory_id} } } // namespace theory -} // namespace CVC5 +} // namespace cvc5 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 */ diff --git a/src/expr/lazy_proof.cpp b/src/expr/lazy_proof.cpp index 701cc55dc..95ce1406c 100644 --- a/src/expr/lazy_proof.cpp +++ b/src/expr/lazy_proof.cpp @@ -18,9 +18,9 @@ #include "expr/proof_node.h" #include "expr/proof_node_manager.h" -using namespace CVC5::kind; +using namespace cvc5::kind; -namespace CVC5 { +namespace cvc5 { LazyCDProof::LazyCDProof(ProofNodeManager* pnm, ProofGenerator* dpg, @@ -228,4 +228,4 @@ bool LazyCDProof::hasGenerator(Node fact) const return it != d_gens.end(); } -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/expr/lazy_proof.h b/src/expr/lazy_proof.h index 5c0de5c5b..3ab0ca49e 100644 --- a/src/expr/lazy_proof.h +++ b/src/expr/lazy_proof.h @@ -19,7 +19,7 @@ #include "expr/proof.h" -namespace CVC5 { +namespace cvc5 { class ProofGenerator; class ProofNodeManager; @@ -105,6 +105,6 @@ class LazyCDProof : public CDProof ProofGenerator* getGeneratorFor(Node fact, bool& isSym); }; -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__EXPR__LAZY_PROOF_H */ diff --git a/src/expr/lazy_proof_chain.cpp b/src/expr/lazy_proof_chain.cpp index 3651e53e1..7f14adc38 100644 --- a/src/expr/lazy_proof_chain.cpp +++ b/src/expr/lazy_proof_chain.cpp @@ -21,7 +21,7 @@ #include "expr/proof_node_manager.h" #include "options/proof_options.h" -namespace CVC5 { +namespace cvc5 { LazyCDProofChain::LazyCDProofChain(ProofNodeManager* pnm, bool cyclic, @@ -317,4 +317,4 @@ ProofGenerator* LazyCDProofChain::getGeneratorForInternal(Node fact, bool& rec) std::string LazyCDProofChain::identify() const { return "LazyCDProofChain"; } -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/expr/lazy_proof_chain.h b/src/expr/lazy_proof_chain.h index 7482e3ca4..41488c821 100644 --- a/src/expr/lazy_proof_chain.h +++ b/src/expr/lazy_proof_chain.h @@ -22,7 +22,7 @@ #include "context/cdhashmap.h" #include "expr/proof_generator.h" -namespace CVC5 { +namespace cvc5 { class ProofNodeManager; @@ -148,6 +148,6 @@ class LazyCDProofChain : public ProofGenerator ProofGenerator* d_defGen; }; -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__EXPR__LAZY_PROOF_CHAIN_H */ diff --git a/src/expr/match_trie.cpp b/src/expr/match_trie.cpp index d3adeb50e..b014339ad 100644 --- a/src/expr/match_trie.cpp +++ b/src/expr/match_trie.cpp @@ -14,9 +14,9 @@ #include "expr/match_trie.h" -using namespace CVC5::kind; +using namespace cvc5::kind; -namespace CVC5 { +namespace cvc5 { namespace expr { bool MatchTrie::getMatches(Node n, NotifyMatch* ntm) @@ -196,4 +196,4 @@ void MatchTrie::clear() } } // namespace expr -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/expr/match_trie.h b/src/expr/match_trie.h index 45ff0c0c7..70ce549e1 100644 --- a/src/expr/match_trie.h +++ b/src/expr/match_trie.h @@ -22,7 +22,7 @@ #include "expr/node.h" -namespace CVC5 { +namespace cvc5 { namespace expr { /** A virtual class for notifications regarding matches. */ @@ -77,6 +77,6 @@ class MatchTrie }; } // namespace expr -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__THEORY__QUANTIFIERS__CANDIDATE_REWRITE_FILTER_H */ diff --git a/src/expr/metakind_template.cpp b/src/expr/metakind_template.cpp index 2f147b8b4..52502cbcd 100644 --- a/src/expr/metakind_template.cpp +++ b/src/expr/metakind_template.cpp @@ -19,7 +19,7 @@ #include <iostream> -namespace CVC5 { +namespace cvc5 { namespace kind { /** @@ -52,20 +52,20 @@ ${metakind_constantMaps} namespace kind { namespace metakind { -size_t NodeValueCompare::constHash(const ::CVC5::expr::NodeValue* nv) +size_t NodeValueCompare::constHash(const ::cvc5::expr::NodeValue* nv) { Assert(nv->getMetaKind() == kind::metakind::CONSTANT); switch (nv->d_kind) { ${metakind_constHashes} -default: Unhandled() << ::CVC5::expr::NodeValue::dKindToKind(nv->d_kind); +default: Unhandled() << ::cvc5::expr::NodeValue::dKindToKind(nv->d_kind); } } template <bool pool> -bool NodeValueCompare::compare(const ::CVC5::expr::NodeValue* nv1, - const ::CVC5::expr::NodeValue* nv2) +bool NodeValueCompare::compare(const ::cvc5::expr::NodeValue* nv1, + const ::cvc5::expr::NodeValue* nv2) { if(nv1->d_kind != nv2->d_kind) { return false; @@ -76,7 +76,7 @@ bool NodeValueCompare::compare(const ::CVC5::expr::NodeValue* nv1, switch (nv1->d_kind) { ${metakind_compares} -default: Unhandled() << ::CVC5::expr::NodeValue::dKindToKind(nv1->d_kind); +default: Unhandled() << ::cvc5::expr::NodeValue::dKindToKind(nv1->d_kind); } } @@ -84,9 +84,9 @@ default: Unhandled() << ::CVC5::expr::NodeValue::dKindToKind(nv1->d_kind); return false; } - ::CVC5::expr::NodeValue::const_nv_iterator i = nv1->nv_begin(); - ::CVC5::expr::NodeValue::const_nv_iterator j = nv2->nv_begin(); - ::CVC5::expr::NodeValue::const_nv_iterator i_end = nv1->nv_end(); + ::cvc5::expr::NodeValue::const_nv_iterator i = nv1->nv_begin(); + ::cvc5::expr::NodeValue::const_nv_iterator j = nv2->nv_begin(); + ::cvc5::expr::NodeValue::const_nv_iterator i_end = nv1->nv_end(); while(i != i_end) { if((*i) != (*j)) { @@ -100,19 +100,19 @@ default: Unhandled() << ::CVC5::expr::NodeValue::dKindToKind(nv1->d_kind); } template bool NodeValueCompare::compare<true>( - const ::CVC5::expr::NodeValue* nv1, const ::CVC5::expr::NodeValue* nv2); + const ::cvc5::expr::NodeValue* nv1, const ::cvc5::expr::NodeValue* nv2); template bool NodeValueCompare::compare<false>( - const ::CVC5::expr::NodeValue* nv1, const ::CVC5::expr::NodeValue* nv2); + const ::cvc5::expr::NodeValue* nv1, const ::cvc5::expr::NodeValue* nv2); void NodeValueConstPrinter::toStream(std::ostream& out, - const ::CVC5::expr::NodeValue* nv) + const ::cvc5::expr::NodeValue* nv) { Assert(nv->getMetaKind() == kind::metakind::CONSTANT); switch (nv->d_kind) { ${metakind_constPrinters} -default: Unhandled() << ::CVC5::expr::NodeValue::dKindToKind(nv->d_kind); +default: Unhandled() << ::cvc5::expr::NodeValue::dKindToKind(nv->d_kind); } } @@ -136,21 +136,21 @@ void NodeValueConstPrinter::toStream(std::ostream& out, TNode n) { * This doesn't support "non-inlined" NodeValues, which shouldn't need this * kind of cleanup. */ -void deleteNodeValueConstant(::CVC5::expr::NodeValue* nv) +void deleteNodeValueConstant(::cvc5::expr::NodeValue* nv) { Assert(nv->getMetaKind() == kind::metakind::CONSTANT); switch (nv->d_kind) { ${metakind_constDeleters} -default: Unhandled() << ::CVC5::expr::NodeValue::dKindToKind(nv->d_kind); +default: Unhandled() << ::cvc5::expr::NodeValue::dKindToKind(nv->d_kind); } } // re-enable the strict-aliasing warning # pragma GCC diagnostic warning "-Wstrict-aliasing" -uint32_t getMinArityForKind(::CVC5::Kind k) +uint32_t getMinArityForKind(::cvc5::Kind k) { static const unsigned lbs[] = { 0, /* NULL_EXPR */ @@ -162,7 +162,7 @@ ${metakind_lbchildren} return lbs[k]; } -uint32_t getMaxArityForKind(::CVC5::Kind k) +uint32_t getMaxArityForKind(::cvc5::Kind k) { static const unsigned ubs[] = { 0, /* NULL_EXPR */ @@ -180,7 +180,7 @@ ${metakind_ubchildren} * example, since the kind of functions is just VARIABLE, it should map * VARIABLE to APPLY_UF. */ -Kind operatorToKind(::CVC5::expr::NodeValue* nv) +Kind operatorToKind(::cvc5::expr::NodeValue* nv) { if(nv->getKind() == kind::BUILTIN) { return nv->getConst<Kind>(); @@ -197,4 +197,4 @@ ${metakind_operatorKinds} } } // namespace kind -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/expr/metakind_template.h b/src/expr/metakind_template.h index ba1b47b4a..5c78d87d3 100644 --- a/src/expr/metakind_template.h +++ b/src/expr/metakind_template.h @@ -24,7 +24,7 @@ #include "base/check.h" #include "expr/kind.h" -namespace CVC5 { +namespace cvc5 { namespace expr { class NodeValue; @@ -74,16 +74,16 @@ struct ConstantMapReverse; */ template <Kind k, bool pool> struct NodeValueConstCompare { - inline static bool compare(const ::CVC5::expr::NodeValue* x, - const ::CVC5::expr::NodeValue* y); - inline static size_t constHash(const ::CVC5::expr::NodeValue* nv); + inline static bool compare(const ::cvc5::expr::NodeValue* x, + const ::cvc5::expr::NodeValue* y); + inline static size_t constHash(const ::cvc5::expr::NodeValue* nv); };/* NodeValueConstCompare<k, pool> */ struct NodeValueCompare { template <bool pool> - static bool compare(const ::CVC5::expr::NodeValue* nv1, - const ::CVC5::expr::NodeValue* nv2); - static size_t constHash(const ::CVC5::expr::NodeValue* nv); + static bool compare(const ::cvc5::expr::NodeValue* nv1, + const ::cvc5::expr::NodeValue* nv2); + static size_t constHash(const ::cvc5::expr::NodeValue* nv); };/* struct NodeValueCompare */ /** @@ -104,9 +104,9 @@ enum MetaKind_t { } // namespace metakind -// import MetaKind into the "CVC5::kind" namespace but keep the +// import MetaKind into the "cvc5::kind" namespace but keep the // individual MetaKind constants under kind::metakind:: -typedef ::CVC5::kind::metakind::MetaKind_t MetaKind; +typedef ::cvc5::kind::metakind::MetaKind_t MetaKind; /** * Get the metakind for a particular kind. @@ -119,12 +119,12 @@ namespace expr { // Comparison predicate struct NodeValuePoolEq { inline bool operator()(const NodeValue* nv1, const NodeValue* nv2) const { - return ::CVC5::kind::metakind::NodeValueCompare::compare<true>(nv1, nv2); + return ::cvc5::kind::metakind::NodeValueCompare::compare<true>(nv1, nv2); } }; } // namespace expr -} // namespace CVC5 +} // namespace cvc5 #include "expr/node_value.h" @@ -134,7 +134,7 @@ ${metakind_includes} #ifdef CVC4__NODE_MANAGER_NEEDS_CONSTANT_MAP -namespace CVC5 { +namespace cvc5 { namespace expr { ${metakind_getConst_decls} @@ -145,7 +145,7 @@ namespace metakind { template <Kind k, bool pool> inline bool NodeValueConstCompare<k, pool>::compare( - const ::CVC5::expr::NodeValue* x, const ::CVC5::expr::NodeValue* y) + const ::cvc5::expr::NodeValue* x, const ::cvc5::expr::NodeValue* y) { typedef typename ConstantMapReverse<k>::T T; if(pool) { @@ -165,7 +165,7 @@ inline bool NodeValueConstCompare<k, pool>::compare( template <Kind k, bool pool> inline size_t NodeValueConstCompare<k, pool>::constHash( - const ::CVC5::expr::NodeValue* nv) + const ::cvc5::expr::NodeValue* nv) { typedef typename ConstantMapReverse<k>::T T; return nv->getConst<T>().hash(); @@ -174,7 +174,7 @@ inline size_t NodeValueConstCompare<k, pool>::constHash( ${metakind_constantMaps_decls} struct NodeValueConstPrinter { - static void toStream(std::ostream& out, const ::CVC5::expr::NodeValue* nv); + static void toStream(std::ostream& out, const ::cvc5::expr::NodeValue* nv); static void toStream(std::ostream& out, TNode n); }; @@ -187,12 +187,12 @@ struct NodeValueConstPrinter { * This doesn't support "non-inlined" NodeValues, which shouldn't need this * kind of cleanup. */ -void deleteNodeValueConstant(::CVC5::expr::NodeValue* nv); +void deleteNodeValueConstant(::cvc5::expr::NodeValue* nv); /** Return the minimum arity of the given kind. */ -uint32_t getMinArityForKind(::CVC5::Kind k); +uint32_t getMinArityForKind(::cvc5::Kind k); /** Return the maximum arity of the given kind. */ -uint32_t getMaxArityForKind(::CVC5::Kind k); +uint32_t getMaxArityForKind(::cvc5::Kind k); } // namespace metakind @@ -201,10 +201,10 @@ uint32_t getMaxArityForKind(::CVC5::Kind k); * example, since the kind of functions is just VARIABLE, it should map * VARIABLE to APPLY_UF. */ -Kind operatorToKind(::CVC5::expr::NodeValue* nv); +Kind operatorToKind(::cvc5::expr::NodeValue* nv); } // namespace kind -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__NODE_MANAGER_NEEDS_CONSTANT_MAP */ diff --git a/src/expr/mkexpr b/src/expr/mkexpr index cc5162fef..c5ff67a43 100755 --- a/src/expr/mkexpr +++ b/src/expr/mkexpr @@ -92,9 +92,9 @@ function theory { echo "$kf:$lineno: error: \"theory\" directive missing class or header argument" >&2 exit 1 elif ! expr "$2" : '\(::*\)' >/dev/null; then - echo "$kf:$lineno: warning: theory class \`$2' isn't fully-qualified (e.g., ::CVC5::theory::foo)" >&2 - elif ! expr "$2" : '\(::CVC5::theory::*\)' >/dev/null; then - echo "$kf:$lineno: warning: theory class not under ::CVC5::theory namespace" >&2 + echo "$kf:$lineno: warning: theory class \`$2' isn't fully-qualified (e.g., ::cvc5::theory::foo)" >&2 + elif ! expr "$2" : '\(::cvc5::theory::*\)' >/dev/null; then + echo "$kf:$lineno: warning: theory class not under ::cvc5::theory namespace" >&2 fi } @@ -226,7 +226,7 @@ template <> $2 const & Expr::getConst< $2 >() const; " getConst_implementations="${getConst_implementations} template <> $2 const & Expr::getConst() const { - PrettyCheckArgument(getKind() == ::CVC5::kind::$1, *this, \"Improper kind for getConst<$2>()\"); + PrettyCheckArgument(getKind() == ::cvc5::kind::$1, *this, \"Improper kind for getConst<$2>()\"); return d_node->getConst< $2 >(); } " diff --git a/src/expr/mkkind b/src/expr/mkkind index 3b987746a..289789a9e 100755 --- a/src/expr/mkkind +++ b/src/expr/mkkind @@ -97,9 +97,9 @@ function theory { echo "$kf:$lineno: error: \"theory\" directive missing class or header argument" >&2 exit 1 elif ! expr "$2" : '\(::*\)' >/dev/null; then - echo "$kf:$lineno: warning: theory class \`$2' isn't fully-qualified (e.g., ::CVC5::theory::foo)" >&2 - elif ! expr "$2" : '\(::CVC5::theory::*\)' >/dev/null; then - echo "$kf:$lineno: warning: theory class not under ::CVC5::theory namespace" >&2 + echo "$kf:$lineno: warning: theory class \`$2' isn't fully-qualified (e.g., ::cvc5::theory::foo)" >&2 + elif ! expr "$2" : '\(::cvc5::theory::*\)' >/dev/null; then + echo "$kf:$lineno: warning: theory class not under ::cvc5::theory namespace" >&2 fi theory_id="$1" diff --git a/src/expr/mkmetakind b/src/expr/mkmetakind index b88a70c71..7c0d110fb 100755 --- a/src/expr/mkmetakind +++ b/src/expr/mkmetakind @@ -76,9 +76,9 @@ function theory { echo "$kf:$lineno: error: \"theory\" directive missing class or header argument" >&2 exit 1 elif ! expr "$2" : '\(::*\)' >/dev/null; then - echo "$kf:$lineno: warning: theory class \`$1' isn't fully-qualified (e.g., ::CVC5::theory::foo)" >&2 - elif ! expr "$2" : '\(::CVC5::theory::*\)' >/dev/null; then - echo "$kf:$lineno: warning: theory class not under ::CVC5::theory namespace" >&2 + echo "$kf:$lineno: warning: theory class \`$1' isn't fully-qualified (e.g., ::cvc5::theory::foo)" >&2 + elif ! expr "$2" : '\(::cvc5::theory::*\)' >/dev/null; then + echo "$kf:$lineno: warning: theory class not under ::cvc5::theory namespace" >&2 fi theory_class=$1 @@ -211,12 +211,12 @@ function constant { # tricky to specify the CONST payload, like "int const*"; in any # case, this warning gives too many false positives, so disable it if ! expr "$2" : '..* ..*' >/dev/null; then - echo "$kf:$lineno: warning: constant $1 class \`$2' isn't fully-qualified (e.g., ::CVC5::Rational)" >&2 + echo "$kf:$lineno: warning: constant $1 class \`$2' isn't fully-qualified (e.g., ::cvc5::Rational)" >&2 fi fi fi if ! expr "$3" : '\(::*\)' >/dev/null; then - echo "$kf:$lineno: warning: constant $1 hasher \`$3' isn't fully-qualified (e.g., ::CVC5::RationalHashFunction)" >&2 + echo "$kf:$lineno: warning: constant $1 hasher \`$3' isn't fully-qualified (e.g., ::cvc5::RationalHashFunction)" >&2 fi # Avoid including the same header multiple times @@ -233,13 +233,13 @@ $2 const& NodeValue::getConst< $2 >() const; template <> struct ConstantMap< $2 > { // typedef $theory_class OwningTheory; - enum { kind = ::CVC5::kind::$1 }; + enum { kind = ::cvc5::kind::$1 }; };/* ConstantMap< $2 > */ template <> -struct ConstantMapReverse< ::CVC5::kind::$1 > { +struct ConstantMapReverse< ::cvc5::kind::$1 > { typedef $2 T; -};/* ConstantMapReverse< ::CVC5::kind::$1 > */ +};/* ConstantMapReverse< ::cvc5::kind::$1 > */ " metakind_constantMaps="${metakind_constantMaps} // The reinterpret_cast of d_children to \"$2 const*\" @@ -250,7 +250,7 @@ struct ConstantMapReverse< ::CVC5::kind::$1 > { template <> $2 const& NodeValue::getConst< $2 >() const { - AssertArgument(getKind() == ::CVC5::kind::$1, *this, + AssertArgument(getKind() == ::cvc5::kind::$1, *this, \"Improper kind for getConst<$2>()\"); // To support non-inlined CONSTANT-kinded NodeValues (those that are // \"constructed\" when initially checking them against the NodeManager diff --git a/src/expr/node.cpp b/src/expr/node.cpp index fa2a8860c..90d29f1eb 100644 --- a/src/expr/node.cpp +++ b/src/expr/node.cpp @@ -26,7 +26,7 @@ using namespace std; -namespace CVC5 { +namespace cvc5 { TypeCheckingExceptionPrivate::TypeCheckingExceptionPrivate(TNode node, std::string message) @@ -110,4 +110,4 @@ bool NodeTemplate<ref_count>::isConst() const { template bool NodeTemplate<true>::isConst() const; template bool NodeTemplate<false>::isConst() const; -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/expr/node.h b/src/expr/node.h index 291c2e538..29bfaa157 100644 --- a/src/expr/node.h +++ b/src/expr/node.h @@ -41,7 +41,7 @@ #include "util/hash.h" #include "util/utility.h" -namespace CVC5 { +namespace cvc5 { class TypeNode; class NodeManager; @@ -199,10 +199,10 @@ class NodeTemplate { template <unsigned nchild_thresh> friend class NodeBuilder; - friend class ::CVC5::expr::attr::AttributeManager; - friend struct ::CVC5::expr::attr::SmtAttributes; + friend class ::cvc5::expr::attr::AttributeManager; + friend struct ::cvc5::expr::attr::SmtAttributes; - friend struct ::CVC5::kind::metakind::NodeValueConstPrinter; + friend struct ::cvc5::kind::metakind::NodeValueConstPrinter; /** * Assigns the expression value and does reference counting. No assumptions @@ -951,12 +951,12 @@ std::ostream& operator<<( return out; } -} // namespace CVC5 +} // namespace cvc5 //#include "expr/attribute.h" #include "expr/node_manager.h" -namespace CVC5 { +namespace cvc5 { inline size_t NodeHashFunction::operator()(Node node) const { return node.getId(); @@ -986,7 +986,7 @@ template <class AttrKind> inline typename AttrKind::value_type NodeTemplate<ref_count>:: getAttribute(const AttrKind&) const { Assert(NodeManager::currentNM() != NULL) - << "There is no current CVC5::NodeManager associated to this thread.\n" + << "There is no current cvc5::NodeManager associated to this thread.\n" "Perhaps a public-facing function is missing a NodeManagerScope ?"; assertTNodeNotExpired(); @@ -999,7 +999,7 @@ template <class AttrKind> inline bool NodeTemplate<ref_count>:: hasAttribute(const AttrKind&) const { Assert(NodeManager::currentNM() != NULL) - << "There is no current CVC5::NodeManager associated to this thread.\n" + << "There is no current cvc5::NodeManager associated to this thread.\n" "Perhaps a public-facing function is missing a NodeManagerScope ?"; assertTNodeNotExpired(); @@ -1012,7 +1012,7 @@ template <class AttrKind> inline bool NodeTemplate<ref_count>::getAttribute(const AttrKind&, typename AttrKind::value_type& ret) const { Assert(NodeManager::currentNM() != NULL) - << "There is no current CVC5::NodeManager associated to this thread.\n" + << "There is no current cvc5::NodeManager associated to this thread.\n" "Perhaps a public-facing function is missing a NodeManagerScope ?"; assertTNodeNotExpired(); @@ -1025,7 +1025,7 @@ template <class AttrKind> inline void NodeTemplate<ref_count>:: setAttribute(const AttrKind&, const typename AttrKind::value_type& value) { Assert(NodeManager::currentNM() != NULL) - << "There is no current CVC5::NodeManager associated to this thread.\n" + << "There is no current cvc5::NodeManager associated to this thread.\n" "Perhaps a public-facing function is missing a NodeManagerScope ?"; assertTNodeNotExpired(); @@ -1225,7 +1225,7 @@ template <bool ref_count> NodeTemplate<true> NodeTemplate<ref_count>::getOperator() const { Assert(NodeManager::currentNM() != NULL) - << "There is no current CVC5::NodeManager associated to this thread.\n" + << "There is no current cvc5::NodeManager associated to this thread.\n" "Perhaps a public-facing function is missing a NodeManagerScope ?"; assertTNodeNotExpired(); @@ -1255,7 +1255,7 @@ template <bool ref_count> TypeNode NodeTemplate<ref_count>::getType(bool check) const { Assert(NodeManager::currentNM() != NULL) - << "There is no current CVC5::NodeManager associated to this thread.\n" + << "There is no current cvc5::NodeManager associated to this thread.\n" "Perhaps a public-facing function is missing a NodeManagerScope ?"; assertTNodeNotExpired(); @@ -1491,6 +1491,6 @@ static void __attribute__((used)) debugPrintRawTNode(const NodeTemplate<false>& } #endif /* CVC4_DEBUG */ -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__NODE_H */ diff --git a/src/expr/node_algorithm.cpp b/src/expr/node_algorithm.cpp index 318b7c85b..bcf74a944 100644 --- a/src/expr/node_algorithm.cpp +++ b/src/expr/node_algorithm.cpp @@ -20,7 +20,7 @@ #include "expr/attribute.h" #include "expr/dtype.h" -namespace CVC5 { +namespace cvc5 { namespace expr { bool hasSubterm(TNode n, TNode t, bool strict) @@ -764,4 +764,4 @@ bool match(Node x, } } // namespace expr -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/expr/node_algorithm.h b/src/expr/node_algorithm.h index ca1ee2e39..7ae56e5ba 100644 --- a/src/expr/node_algorithm.h +++ b/src/expr/node_algorithm.h @@ -27,7 +27,7 @@ #include "expr/node.h" #include "expr/type_node.h" -namespace CVC5 { +namespace cvc5 { namespace expr { /** @@ -235,6 +235,6 @@ bool match(Node n1, std::unordered_map<Node, Node, NodeHashFunction>& subs); } // namespace expr -} // namespace CVC5 +} // namespace cvc5 #endif diff --git a/src/expr/node_builder.h b/src/expr/node_builder.h index 724e03451..eaf5b040d 100644 --- a/src/expr/node_builder.h +++ b/src/expr/node_builder.h @@ -160,14 +160,14 @@ #include <memory> #include <vector> -namespace CVC5 { +namespace cvc5 { static const unsigned default_nchild_thresh = 10; template <unsigned nchild_thresh> class NodeBuilder; class NodeManager; -} // namespace CVC5 +} // namespace cvc5 #include "base/check.h" #include "base/output.h" @@ -175,7 +175,7 @@ class NodeManager; #include "expr/metakind.h" #include "expr/node_value.h" -namespace CVC5 { +namespace cvc5 { // Sometimes it's useful for debugging to output a NodeBuilder that // isn't yet a Node.. @@ -729,7 +729,7 @@ public: };/* class NodeBuilder<> */ -} // namespace CVC5 +} // namespace cvc5 // TODO: add templatized NodeTemplate<ref_count> to all above and // below inlines for 'const [T]Node&' arguments? Technically a lot of @@ -741,7 +741,7 @@ public: #include "expr/node_manager.h" #include "options/expr_options.h" -namespace CVC5 { +namespace cvc5 { template <unsigned nchild_thresh> void NodeBuilder<nchild_thresh>::clear(Kind k) { @@ -1324,6 +1324,6 @@ std::ostream& operator<<(std::ostream& out, const NodeBuilder<nchild_thresh>& nb return out << *nb.d_nv; } -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__NODE_BUILDER_H */ diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp index 370f0fb4c..6d2d150f5 100644 --- a/src/expr/node_manager.cpp +++ b/src/expr/node_manager.cpp @@ -35,9 +35,9 @@ #include "util/resource_manager.h" using namespace std; -using namespace CVC5::expr; +using namespace cvc5::expr; -namespace CVC5 { +namespace cvc5 { thread_local NodeManager* NodeManager::s_current = NULL; @@ -373,7 +373,7 @@ void NodeManager::reclaimZombies() { if(mk == kind::metakind::CONSTANT) { // Destroy (call the destructor for) the C++ type representing // the constant in this NodeValue. This is needed for - // e.g. CVC5::Rational, since it has a gmp internal + // e.g. cvc5::Rational, since it has a gmp internal // representation that mallocs memory and should be cleaned // up. (This won't delete a pointer value if used as a // constant, but then, you should probably use a smart-pointer @@ -678,7 +678,7 @@ std::vector<TypeNode> NodeManager::mkMutualDatatypeTypes( << "malformed selector in datatype post-resolution"; // This next one's a "hard" check, performed in non-debug builds // as well; the other ones should all be guaranteed by the - // CVC5::DType class, but this actually needs to be checked. + // cvc5::DType class, but this actually needs to be checked. AlwaysAssert(!selectorType.getRangeType().isFunctionLike()) << "cannot put function-like things in datatypes"; } @@ -1170,4 +1170,4 @@ Kind NodeManager::getKindForFunction(TNode fun) return kind::UNDEFINED_KIND; } -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index aeea179d4..857bcc25f 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -35,7 +35,7 @@ #include "expr/metakind.h" #include "expr/node_value.h" -namespace CVC5 { +namespace cvc5 { namespace api { class Solver; @@ -163,7 +163,7 @@ class NodeManager * PLUS, are APPLYs of a PLUS operator to arguments. This array * holds the set of operators for these things. A PLUS operator is * a Node with kind "BUILTIN", and if you call - * plusOperator->getConst<CVC5::Kind>(), you get kind::PLUS back. + * plusOperator->getConst<cvc5::Kind>(), you get kind::PLUS back. */ Node d_operators[kind::LAST_KIND]; @@ -660,7 +660,7 @@ class NodeManager /** * Get the (singleton) operator of an OPERATOR-kinded kind. The * returned node n will have kind BUILTIN, and calling - * n.getConst<CVC5::Kind>() will yield k. + * n.getConst<cvc5::Kind>() will yield k. */ inline TNode operatorOf(Kind k) { AssertArgument( kind::metaKindOf(k) == kind::metakind::OPERATOR, k, @@ -1203,7 +1203,7 @@ inline void NodeManager::poolRemove(expr::NodeValue* nv) { d_nodeValuePool.erase(nv);// FIXME multithreading } -} // namespace CVC5 +} // namespace cvc5 #define CVC4__NODE_MANAGER_NEEDS_CONSTANT_MAP #include "expr/metakind.h" @@ -1211,7 +1211,7 @@ inline void NodeManager::poolRemove(expr::NodeValue* nv) { #include "expr/node_builder.h" -namespace CVC5 { +namespace cvc5 { // general expression-builders @@ -1577,6 +1577,6 @@ NodeClass NodeManager::mkConstInternal(const T& val) { return NodeClass(nv); } -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__NODE_MANAGER_H */ diff --git a/src/expr/node_manager_attributes.h b/src/expr/node_manager_attributes.h index b7f6319eb..c88df3cee 100644 --- a/src/expr/node_manager_attributes.h +++ b/src/expr/node_manager_attributes.h @@ -19,7 +19,7 @@ #include "expr/attribute.h" -namespace CVC5 { +namespace cvc5 { namespace expr { // Definition of an attribute for the variable name. @@ -37,4 +37,4 @@ typedef expr::Attribute<expr::attr::TypeTag, TypeNode> TypeAttr; typedef expr::Attribute<expr::attr::TypeCheckedTag, bool> TypeCheckedAttr; } // namespace expr -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/expr/node_self_iterator.h b/src/expr/node_self_iterator.h index 831eace65..d8558de97 100644 --- a/src/expr/node_self_iterator.h +++ b/src/expr/node_self_iterator.h @@ -24,7 +24,7 @@ #include "base/check.h" #include "expr/node.h" -namespace CVC5 { +namespace cvc5 { namespace expr { class NodeSelfIterator : public std::iterator<std::input_iterator_tag, Node> { @@ -123,6 +123,6 @@ inline bool NodeSelfIterator::operator!=(NodeSelfIterator i) const { } } // namespace expr -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__EXPR__NODE_SELF_ITERATOR_H */ diff --git a/src/expr/node_traversal.cpp b/src/expr/node_traversal.cpp index c7d3ab3f8..01140a806 100644 --- a/src/expr/node_traversal.cpp +++ b/src/expr/node_traversal.cpp @@ -16,7 +16,7 @@ #include <functional> -namespace CVC5 { +namespace cvc5 { NodeDfsIterator::NodeDfsIterator(TNode n, VisitOrder order, @@ -156,4 +156,4 @@ NodeDfsIterator NodeDfsIterable::end() const return NodeDfsIterator(d_order); } -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/expr/node_traversal.h b/src/expr/node_traversal.h index 934ec6bd8..015bcec06 100644 --- a/src/expr/node_traversal.h +++ b/src/expr/node_traversal.h @@ -23,7 +23,7 @@ #include "expr/node.h" -namespace CVC5 { +namespace cvc5 { /** * Enum that represents an order in which nodes are visited. @@ -144,6 +144,6 @@ class NodeDfsIterable std::function<bool(TNode)> d_skipIf; }; -} // namespace CVC5 +} // namespace cvc5 #endif // CVC4__EXPR__NODE_TRAVERSAL_H diff --git a/src/expr/node_trie.cpp b/src/expr/node_trie.cpp index 195011c1f..5af1cef01 100644 --- a/src/expr/node_trie.cpp +++ b/src/expr/node_trie.cpp @@ -14,7 +14,7 @@ #include "expr/node_trie.h" -namespace CVC5 { +namespace cvc5 { namespace theory { template <bool ref_count> @@ -92,4 +92,4 @@ template void NodeTemplateTrie<true>::debugPrint(const char* c, unsigned depth) const; } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/expr/node_trie.h b/src/expr/node_trie.h index f765105d3..2f42b6a52 100644 --- a/src/expr/node_trie.h +++ b/src/expr/node_trie.h @@ -20,7 +20,7 @@ #include <map> #include "expr/node.h" -namespace CVC5 { +namespace cvc5 { namespace theory { /** NodeTemplate trie class @@ -107,6 +107,6 @@ typedef NodeTemplateTrie<true> NodeTrie; typedef NodeTemplateTrie<false> TNodeTrie; } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__EXPR__NODE_TRIE_H */ diff --git a/src/expr/node_value.cpp b/src/expr/node_value.cpp index 027c15a0a..7b3e413f7 100644 --- a/src/expr/node_value.cpp +++ b/src/expr/node_value.cpp @@ -31,7 +31,7 @@ using namespace std; -namespace CVC5 { +namespace cvc5 { namespace expr { string NodeValue::toString() const { @@ -95,4 +95,4 @@ NodeValue::iterator<NodeTemplate<false> > operator+( } } // namespace expr -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/expr/node_value.h b/src/expr/node_value.h index ecc054a75..3815ea5be 100644 --- a/src/expr/node_value.h +++ b/src/expr/node_value.h @@ -32,7 +32,7 @@ #include "expr/kind.h" #include "options/language.h" -namespace CVC5 { +namespace cvc5 { template <bool ref_count> class NodeTemplate; class TypeNode; @@ -45,13 +45,13 @@ namespace expr { namespace kind { namespace metakind { - template < ::CVC5::Kind k, bool pool> + template < ::cvc5::Kind k, bool pool> struct NodeValueConstCompare; struct NodeValueCompare; struct NodeValueConstPrinter; - void deleteNodeValueConstant(::CVC5::expr::NodeValue* nv); + void deleteNodeValueConstant(::cvc5::expr::NodeValue* nv); } // namespace metakind } // namespace kind @@ -63,19 +63,19 @@ namespace expr { class NodeValue { template <bool> - friend class ::CVC5::NodeTemplate; - friend class ::CVC5::TypeNode; + friend class ::cvc5::NodeTemplate; + friend class ::cvc5::TypeNode; template <unsigned nchild_thresh> - friend class ::CVC5::NodeBuilder; - friend class ::CVC5::NodeManager; + friend class ::cvc5::NodeBuilder; + friend class ::cvc5::NodeManager; template <Kind k, bool pool> - friend struct ::CVC5::kind::metakind::NodeValueConstCompare; + friend struct ::cvc5::kind::metakind::NodeValueConstCompare; - friend struct ::CVC5::kind::metakind::NodeValueCompare; - friend struct ::CVC5::kind::metakind::NodeValueConstPrinter; + friend struct ::cvc5::kind::metakind::NodeValueCompare; + friend struct ::cvc5::kind::metakind::NodeValueConstPrinter; - friend void ::CVC5::kind::metakind::deleteNodeValueConstant(NodeValue* nv); + friend void ::cvc5::kind::metakind::deleteNodeValueConstant(NodeValue* nv); friend class RefCountGuard; @@ -396,11 +396,11 @@ struct NodeValueIDEquality { inline std::ostream& operator<<(std::ostream& out, const NodeValue& nv); } // namespace expr -} // namespace CVC5 +} // namespace cvc5 #include "expr/node_manager.h" -namespace CVC5 { +namespace cvc5 { namespace expr { inline NodeValue::NodeValue(int) : @@ -497,11 +497,11 @@ inline NodeValue* NodeValue::getChild(int i) const { } } // namespace expr -} // namespace CVC5 +} // namespace cvc5 #include "expr/node.h" -namespace CVC5 { +namespace cvc5 { namespace expr { template <typename T> @@ -545,6 +545,6 @@ static void __attribute__((used)) debugPrintRawNodeValue(const expr::NodeValue* } #endif /* CVC4_DEBUG */ -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__EXPR__NODE_VALUE_H */ diff --git a/src/expr/node_visitor.h b/src/expr/node_visitor.h index a3e24772a..9816e37e8 100644 --- a/src/expr/node_visitor.h +++ b/src/expr/node_visitor.h @@ -22,7 +22,7 @@ #include "expr/node.h" -namespace CVC5 { +namespace cvc5 { /** * Traverses the nodes reverse-topologically (children before parents), @@ -123,4 +123,4 @@ public: template <typename Visitor> thread_local bool NodeVisitor<Visitor>::s_inRun = false; -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/expr/proof.cpp b/src/expr/proof.cpp index a55b3c69a..c0ba27a64 100644 --- a/src/expr/proof.cpp +++ b/src/expr/proof.cpp @@ -18,9 +18,9 @@ #include "expr/proof_node.h" #include "expr/proof_node_manager.h" -using namespace CVC5::kind; +using namespace cvc5::kind; -namespace CVC5 { +namespace cvc5 { CDProof::CDProof(ProofNodeManager* pnm, context::Context* c, @@ -455,4 +455,4 @@ Node CDProof::getSymmFact(TNode f) std::string CDProof::identify() const { return d_name; } -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/expr/proof.h b/src/expr/proof.h index 164880cea..af859df93 100644 --- a/src/expr/proof.h +++ b/src/expr/proof.h @@ -24,7 +24,7 @@ #include "expr/proof_generator.h" #include "expr/proof_step_buffer.h" -namespace CVC5 { +namespace cvc5 { class ProofNode; class ProofNodeManager; @@ -273,6 +273,6 @@ class CDProof : public ProofGenerator void notifyNewProof(Node expected); }; -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__EXPR__PROOF_MANAGER_H */ diff --git a/src/expr/proof_checker.cpp b/src/expr/proof_checker.cpp index b5955e991..ca1b96f1e 100644 --- a/src/expr/proof_checker.cpp +++ b/src/expr/proof_checker.cpp @@ -19,9 +19,9 @@ #include "options/proof_options.h" #include "smt/smt_statistics_registry.h" -using namespace CVC5::kind; +using namespace cvc5::kind; -namespace CVC5 { +namespace cvc5 { Node ProofRuleChecker::check(PfRule id, const std::vector<Node>& children, @@ -347,4 +347,4 @@ bool ProofChecker::isPedanticFailure(PfRule id, return false; } -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/expr/proof_checker.h b/src/expr/proof_checker.h index edb0fec3a..99f9f3ec8 100644 --- a/src/expr/proof_checker.h +++ b/src/expr/proof_checker.h @@ -24,7 +24,7 @@ #include "util/statistics_registry.h" #include "util/stats_histogram.h" -namespace CVC5 { +namespace cvc5 { class ProofChecker; class ProofNode; @@ -202,6 +202,6 @@ class ProofChecker bool enableOutput); }; -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__EXPR__PROOF_CHECKER_H */ diff --git a/src/expr/proof_ensure_closed.cpp b/src/expr/proof_ensure_closed.cpp index 487c52bc6..6947cfd44 100644 --- a/src/expr/proof_ensure_closed.cpp +++ b/src/expr/proof_ensure_closed.cpp @@ -22,7 +22,7 @@ #include "options/proof_options.h" #include "options/smt_options.h" -namespace CVC5 { +namespace cvc5 { /** * Ensure closed with respect to assumptions, internal version, which @@ -179,4 +179,4 @@ void pfnEnsureClosedWrt(ProofNode* pn, ensureClosedWrtInternal(Node::null(), nullptr, pn, assumps, c, ctx, false); } -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/expr/proof_ensure_closed.h b/src/expr/proof_ensure_closed.h index 40143f814..d610147d4 100644 --- a/src/expr/proof_ensure_closed.h +++ b/src/expr/proof_ensure_closed.h @@ -19,7 +19,7 @@ #include "expr/node.h" -namespace CVC5 { +namespace cvc5 { class ProofGenerator; class ProofNode; @@ -67,6 +67,6 @@ void pfnEnsureClosedWrt(ProofNode* pn, const std::vector<Node>& assumps, const char* c, const char* ctx); -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__EXPR__PROOF_ENSURE_CLOSED_H */ diff --git a/src/expr/proof_generator.cpp b/src/expr/proof_generator.cpp index 102435cea..a315ba2cd 100644 --- a/src/expr/proof_generator.cpp +++ b/src/expr/proof_generator.cpp @@ -21,7 +21,7 @@ #include "expr/proof_node_algorithm.h" #include "options/smt_options.h" -namespace CVC5 { +namespace cvc5 { std::ostream& operator<<(std::ostream& out, CDPOverwrite opol) { @@ -73,4 +73,4 @@ bool ProofGenerator::addProofTo(Node f, return false; } -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/expr/proof_generator.h b/src/expr/proof_generator.h index 446cb2c83..76a2c9b3b 100644 --- a/src/expr/proof_generator.h +++ b/src/expr/proof_generator.h @@ -19,7 +19,7 @@ #include "expr/node.h" -namespace CVC5 { +namespace cvc5 { class CDProof; class ProofNode; @@ -107,6 +107,6 @@ class ProofGenerator virtual std::string identify() const = 0; }; -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__EXPR__PROOF_GENERATOR_H */ diff --git a/src/expr/proof_node.cpp b/src/expr/proof_node.cpp index 923bdeacd..f7ad65844 100644 --- a/src/expr/proof_node.cpp +++ b/src/expr/proof_node.cpp @@ -17,7 +17,7 @@ #include "expr/proof_node_algorithm.h" #include "expr/proof_node_to_sexpr.h" -namespace CVC5 { +namespace cvc5 { ProofNode::ProofNode(PfRule id, const std::vector<std::shared_ptr<ProofNode>>& children, @@ -81,4 +81,4 @@ std::ostream& operator<<(std::ostream& out, const ProofNode& pn) return out; } -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/expr/proof_node.h b/src/expr/proof_node.h index 67600e2d0..13c7f2878 100644 --- a/src/expr/proof_node.h +++ b/src/expr/proof_node.h @@ -22,7 +22,7 @@ #include "expr/node.h" #include "expr/proof_rule.h" -namespace CVC5 { +namespace cvc5 { class ProofNodeManager; class ProofNode; @@ -141,6 +141,6 @@ inline size_t ProofNodeHashFunction::operator()( */ std::ostream& operator<<(std::ostream& out, const ProofNode& pn); -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__EXPR__PROOF_NODE_H */ diff --git a/src/expr/proof_node_algorithm.cpp b/src/expr/proof_node_algorithm.cpp index 142a9b37f..f307b78b9 100644 --- a/src/expr/proof_node_algorithm.cpp +++ b/src/expr/proof_node_algorithm.cpp @@ -16,7 +16,7 @@ #include "expr/proof_node.h" -namespace CVC5 { +namespace cvc5 { namespace expr { void getFreeAssumptions(ProofNode* pn, std::vector<Node>& assump) @@ -172,4 +172,4 @@ bool containsSubproof(ProofNode* pn, } } // namespace expr -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/expr/proof_node_algorithm.h b/src/expr/proof_node_algorithm.h index 9266c7251..01faa8a40 100644 --- a/src/expr/proof_node_algorithm.h +++ b/src/expr/proof_node_algorithm.h @@ -21,7 +21,7 @@ #include "expr/node.h" -namespace CVC5 { +namespace cvc5 { class ProofNode; @@ -70,6 +70,6 @@ bool containsSubproof(ProofNode* pn, std::unordered_set<const ProofNode*>& visited); } // namespace expr -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__EXPR__PROOF_NODE_ALGORITHM_H */ diff --git a/src/expr/proof_node_manager.cpp b/src/expr/proof_node_manager.cpp index ceb9d4eac..036c50947 100644 --- a/src/expr/proof_node_manager.cpp +++ b/src/expr/proof_node_manager.cpp @@ -23,9 +23,9 @@ #include "options/proof_options.h" #include "theory/rewriter.h" -using namespace CVC5::kind; +using namespace cvc5::kind; -namespace CVC5 { +namespace cvc5 { ProofNodeManager::ProofNodeManager(ProofChecker* pc) : d_checker(pc) @@ -356,4 +356,4 @@ bool ProofNodeManager::updateNodeInternal( return true; } -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/expr/proof_node_manager.h b/src/expr/proof_node_manager.h index 8e019818d..54d398545 100644 --- a/src/expr/proof_node_manager.h +++ b/src/expr/proof_node_manager.h @@ -22,7 +22,7 @@ #include "expr/node.h" #include "expr/proof_rule.h" -namespace CVC5 { +namespace cvc5 { class ProofChecker; class ProofNode; @@ -192,6 +192,6 @@ class ProofNodeManager bool needsCheck); }; -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__EXPR__PROOF_NODE_H */ diff --git a/src/expr/proof_node_to_sexpr.cpp b/src/expr/proof_node_to_sexpr.cpp index 7468ecb5a..b53ce368d 100644 --- a/src/expr/proof_node_to_sexpr.cpp +++ b/src/expr/proof_node_to_sexpr.cpp @@ -20,9 +20,9 @@ #include "expr/proof_node.h" #include "options/proof_options.h" -using namespace CVC5::kind; +using namespace cvc5::kind; -namespace CVC5 { +namespace cvc5 { ProofNodeToSExpr::ProofNodeToSExpr() { @@ -144,4 +144,4 @@ Node ProofNodeToSExpr::getOrMkNodeVariable(Node n) return var; } -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/expr/proof_node_to_sexpr.h b/src/expr/proof_node_to_sexpr.h index 8da094da2..bbbde39f6 100644 --- a/src/expr/proof_node_to_sexpr.h +++ b/src/expr/proof_node_to_sexpr.h @@ -22,7 +22,7 @@ #include "expr/node.h" #include "expr/proof_rule.h" -namespace CVC5 { +namespace cvc5 { class ProofNode; @@ -64,6 +64,6 @@ class ProofNodeToSExpr Node getOrMkNodeVariable(Node n); }; -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__EXPR__PROOF_RULE_H */ diff --git a/src/expr/proof_node_updater.cpp b/src/expr/proof_node_updater.cpp index 4c1883e93..933e5b999 100644 --- a/src/expr/proof_node_updater.cpp +++ b/src/expr/proof_node_updater.cpp @@ -19,7 +19,7 @@ #include "expr/proof_node_algorithm.h" #include "expr/proof_node_manager.h" -namespace CVC5 { +namespace cvc5 { ProofNodeUpdaterCallback::ProofNodeUpdaterCallback() {} ProofNodeUpdaterCallback::~ProofNodeUpdaterCallback() {} @@ -261,4 +261,4 @@ void ProofNodeUpdater::setDebugFreeAssumptions( d_debugFreeAssumps = true; } -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/expr/proof_node_updater.h b/src/expr/proof_node_updater.h index 5a22af61a..8e30f14d2 100644 --- a/src/expr/proof_node_updater.h +++ b/src/expr/proof_node_updater.h @@ -23,7 +23,7 @@ #include "expr/node.h" #include "expr/proof_node.h" -namespace CVC5 { +namespace cvc5 { class CDProof; class ProofNode; @@ -155,6 +155,6 @@ class ProofNodeUpdater bool d_autoSym; }; -} // namespace CVC5 +} // namespace cvc5 #endif diff --git a/src/expr/proof_rule.cpp b/src/expr/proof_rule.cpp index 1323520c3..8141a017c 100644 --- a/src/expr/proof_rule.cpp +++ b/src/expr/proof_rule.cpp @@ -16,7 +16,7 @@ #include <iostream> -namespace CVC5 { +namespace cvc5 { const char* toString(PfRule id) { @@ -210,4 +210,4 @@ size_t PfRuleHashFunction::operator()(PfRule id) const return static_cast<size_t>(id); } -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/expr/proof_rule.h b/src/expr/proof_rule.h index 95f97ae44..7e0fc31fe 100644 --- a/src/expr/proof_rule.h +++ b/src/expr/proof_rule.h @@ -19,7 +19,7 @@ #include <iosfwd> -namespace CVC5 { +namespace cvc5 { /** * An enumeration for proof rules. This enumeration is analogous to Kind for @@ -1379,6 +1379,6 @@ struct PfRuleHashFunction size_t operator()(PfRule id) const; }; /* struct PfRuleHashFunction */ -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__EXPR__PROOF_RULE_H */ diff --git a/src/expr/proof_set.h b/src/expr/proof_set.h index ccfac350a..0509ed9d4 100644 --- a/src/expr/proof_set.h +++ b/src/expr/proof_set.h @@ -23,7 +23,7 @@ #include "context/context.h" #include "expr/proof_node_manager.h" -namespace CVC5 { +namespace cvc5 { /** * A (context-dependent) set of proofs, which is used for memory @@ -70,6 +70,6 @@ class CDProofSet std::string d_namePrefix; }; -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__EXPR__LAZY_PROOF_SET_H */ diff --git a/src/expr/proof_step_buffer.cpp b/src/expr/proof_step_buffer.cpp index 23f0f5997..4ecee9130 100644 --- a/src/expr/proof_step_buffer.cpp +++ b/src/expr/proof_step_buffer.cpp @@ -16,9 +16,9 @@ #include "expr/proof_checker.h" -using namespace CVC5::kind; +using namespace cvc5::kind; -namespace CVC5 { +namespace cvc5 { ProofStep::ProofStep() : d_rule(PfRule::UNKNOWN) {} ProofStep::ProofStep(PfRule r, @@ -108,4 +108,4 @@ const std::vector<std::pair<Node, ProofStep>>& ProofStepBuffer::getSteps() const void ProofStepBuffer::clear() { d_steps.clear(); } -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/expr/proof_step_buffer.h b/src/expr/proof_step_buffer.h index b78d1d605..99a7608ff 100644 --- a/src/expr/proof_step_buffer.h +++ b/src/expr/proof_step_buffer.h @@ -22,7 +22,7 @@ #include "expr/node.h" #include "expr/proof_rule.h" -namespace CVC5 { +namespace cvc5 { class ProofChecker; @@ -92,6 +92,6 @@ class ProofStepBuffer std::vector<std::pair<Node, ProofStep>> d_steps; }; -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__EXPR__PROOF_STEP_BUFFER_H */ diff --git a/src/expr/record.cpp b/src/expr/record.cpp index affd2615c..367315d84 100644 --- a/src/expr/record.cpp +++ b/src/expr/record.cpp @@ -19,10 +19,10 @@ #include "base/check.h" #include "base/output.h" -namespace CVC5 { +namespace cvc5 { std::ostream& operator<<(std::ostream& out, const RecordUpdate& t) { return out << "[" << t.getField() << "]"; } -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/expr/record.h b/src/expr/record.h index d4b41b9b9..436b5b269 100644 --- a/src/expr/record.h +++ b/src/expr/record.h @@ -25,13 +25,13 @@ #include <utility> // Forward Declarations -namespace CVC5 { +namespace cvc5 { // This forward delcartion is required to resolve a cicular dependency with // Record which is a referenced in a Kind file. class TypeNode; -} // namespace CVC5 +} // namespace cvc5 -namespace CVC5 { +namespace cvc5 { // operators for record update class RecordUpdate @@ -56,6 +56,6 @@ std::ostream& operator<<(std::ostream& out, const RecordUpdate& t); using Record = std::vector<std::pair<std::string, TypeNode>>; -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__RECORD_H */ diff --git a/src/expr/sequence.cpp b/src/expr/sequence.cpp index 90b57f58d..df40c8534 100644 --- a/src/expr/sequence.cpp +++ b/src/expr/sequence.cpp @@ -22,7 +22,7 @@ using namespace std; -namespace CVC5 { +namespace cvc5 { Sequence::Sequence(const TypeNode& t, const std::vector<Node>& s) : d_type(new TypeNode(t)), d_seq(s) @@ -378,4 +378,4 @@ size_t SequenceHashFunction::operator()(const Sequence& s) const return ret; } -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/expr/sequence.h b/src/expr/sequence.h index 461adb667..e42851f58 100644 --- a/src/expr/sequence.h +++ b/src/expr/sequence.h @@ -20,7 +20,7 @@ #include <memory> #include <vector> -namespace CVC5 { +namespace cvc5 { template <bool ref_count> class NodeTemplate; @@ -36,7 +36,7 @@ class Sequence public: /** constructors for Sequence * - * Internally, a CVC5::Sequence is represented by a vector of Nodes (d_seq), + * Internally, a cvc5::Sequence is represented by a vector of Nodes (d_seq), * where each Node in this vector must be a constant. */ Sequence() = default; @@ -173,6 +173,6 @@ struct SequenceHashFunction std::ostream& operator<<(std::ostream& os, const Sequence& s); -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__EXPR__SEQUENCE_H */ diff --git a/src/expr/skolem_manager.cpp b/src/expr/skolem_manager.cpp index 2b04c0755..31c0b55cd 100644 --- a/src/expr/skolem_manager.cpp +++ b/src/expr/skolem_manager.cpp @@ -18,9 +18,9 @@ #include "expr/bound_var_manager.h" #include "expr/node_algorithm.h" -using namespace CVC5::kind; +using namespace cvc5::kind; -namespace CVC5 { +namespace cvc5 { // Attributes are global maps from Nodes to data. Thus, note that these could // be implemented as internal maps in SkolemManager. @@ -298,4 +298,4 @@ Node SkolemManager::mkSkolemInternal(Node w, return k; } -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/expr/skolem_manager.h b/src/expr/skolem_manager.h index 1078bc11f..9955c0e15 100644 --- a/src/expr/skolem_manager.h +++ b/src/expr/skolem_manager.h @@ -21,7 +21,7 @@ #include "expr/node.h" -namespace CVC5 { +namespace cvc5 { class ProofGenerator; @@ -234,6 +234,6 @@ class SkolemManager int flags = NodeManager::SKOLEM_DEFAULT); }; -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__EXPR__PROOF_SKOLEM_CACHE_H */ diff --git a/src/expr/subs.cpp b/src/expr/subs.cpp index 897c6fdba..c2138499b 100644 --- a/src/expr/subs.cpp +++ b/src/expr/subs.cpp @@ -18,7 +18,7 @@ #include "theory/rewriter.h" -namespace CVC5 { +namespace cvc5 { bool Subs::empty() const { return d_vars.empty(); } @@ -176,4 +176,4 @@ std::ostream& operator<<(std::ostream& out, const Subs& s) return out; } -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/expr/subs.h b/src/expr/subs.h index c2854bf36..fdb8e4551 100644 --- a/src/expr/subs.h +++ b/src/expr/subs.h @@ -19,7 +19,7 @@ #include <vector> #include "expr/node.h" -namespace CVC5 { +namespace cvc5 { /** * Helper substitution class. Stores a substitution in parallel vectors @@ -80,6 +80,6 @@ class Subs */ std::ostream& operator<<(std::ostream& out, const Subs& s); -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__EXPR__SUBS_H */ diff --git a/src/expr/sygus_datatype.cpp b/src/expr/sygus_datatype.cpp index 352dd157a..929c8a97c 100644 --- a/src/expr/sygus_datatype.cpp +++ b/src/expr/sygus_datatype.cpp @@ -16,9 +16,9 @@ #include <sstream> -using namespace CVC5::kind; +using namespace cvc5::kind; -namespace CVC5 { +namespace cvc5 { SygusDatatype::SygusDatatype(const std::string& name) : d_dt(DType(name)) {} @@ -99,4 +99,4 @@ const DType& SygusDatatype::getDatatype() const bool SygusDatatype::isInitialized() const { return d_dt.isSygus(); } -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/expr/sygus_datatype.h b/src/expr/sygus_datatype.h index f4635bdb3..e5d1de740 100644 --- a/src/expr/sygus_datatype.h +++ b/src/expr/sygus_datatype.h @@ -24,7 +24,7 @@ #include "expr/node.h" #include "expr/type_node.h" -namespace CVC5 { +namespace cvc5 { /** Attribute true for variables that represent any constant */ struct SygusAnyConstAttributeId @@ -134,6 +134,6 @@ class SygusDatatype DType d_dt; }; -} // namespace CVC5 +} // namespace cvc5 #endif diff --git a/src/expr/symbol_manager.cpp b/src/expr/symbol_manager.cpp index 1e99f4a68..9610e443d 100644 --- a/src/expr/symbol_manager.cpp +++ b/src/expr/symbol_manager.cpp @@ -19,9 +19,9 @@ #include "context/cdlist.h" #include "context/cdo.h" -using namespace CVC5::context; +using namespace cvc5::context; -namespace CVC5 { +namespace cvc5 { // ---------------------------------------------- SymbolManager::Implementation @@ -367,4 +367,4 @@ void SymbolManager::resetAssertions() d_symtabAllocated.resetAssertions(); } -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/expr/symbol_manager.h b/src/expr/symbol_manager.h index 6795ce3b3..0a9248f78 100644 --- a/src/expr/symbol_manager.h +++ b/src/expr/symbol_manager.h @@ -25,7 +25,7 @@ #include "cvc4_export.h" #include "expr/symbol_table.h" -namespace CVC5 { +namespace cvc5 { /** * Symbol manager, which manages: @@ -156,6 +156,6 @@ class CVC4_EXPORT SymbolManager bool d_globalDeclarations; }; -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__EXPR__SYMBOL_MANAGER_H */ diff --git a/src/expr/symbol_table.cpp b/src/expr/symbol_table.cpp index 774e2bb39..1c513fea4 100644 --- a/src/expr/symbol_table.cpp +++ b/src/expr/symbol_table.cpp @@ -28,11 +28,11 @@ #include "context/cdhashset.h" #include "context/context.h" -namespace CVC5 { +namespace cvc5 { -using ::CVC5::context::CDHashMap; -using ::CVC5::context::CDHashSet; -using ::CVC5::context::Context; +using ::cvc5::context::CDHashMap; +using ::cvc5::context::CDHashSet; +using ::cvc5::context::Context; using ::std::copy; using ::std::endl; using ::std::ostream_iterator; @@ -679,4 +679,4 @@ size_t SymbolTable::getLevel() const { return d_implementation->getLevel(); } void SymbolTable::reset() { d_implementation->reset(); } void SymbolTable::resetAssertions() { d_implementation->resetAssertions(); } -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/expr/symbol_table.h b/src/expr/symbol_table.h index 113dea704..fbb1969dd 100644 --- a/src/expr/symbol_table.h +++ b/src/expr/symbol_table.h @@ -26,7 +26,7 @@ #include "base/exception.h" #include "cvc4_export.h" -namespace CVC5 { +namespace cvc5 { namespace api { class Solver; @@ -210,6 +210,6 @@ class CVC4_EXPORT SymbolTable std::unique_ptr<Implementation> d_implementation; }; /* class SymbolTable */ -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__SYMBOL_TABLE_H */ diff --git a/src/expr/tconv_seq_proof_generator.cpp b/src/expr/tconv_seq_proof_generator.cpp index 9b099de2d..d51e07e83 100644 --- a/src/expr/tconv_seq_proof_generator.cpp +++ b/src/expr/tconv_seq_proof_generator.cpp @@ -18,7 +18,7 @@ #include "expr/proof_node_manager.h" -namespace CVC5 { +namespace cvc5 { TConvSeqProofGenerator::TConvSeqProofGenerator( ProofNodeManager* pnm, @@ -168,4 +168,4 @@ theory::TrustNode TConvSeqProofGenerator::mkTrustRewriteSequence( std::string TConvSeqProofGenerator::identify() const { return d_name; } -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/expr/tconv_seq_proof_generator.h b/src/expr/tconv_seq_proof_generator.h index a5b1de101..151cd511d 100644 --- a/src/expr/tconv_seq_proof_generator.h +++ b/src/expr/tconv_seq_proof_generator.h @@ -22,7 +22,7 @@ #include "expr/proof_generator.h" #include "theory/trust_node.h" -namespace CVC5 { +namespace cvc5 { class ProofNodeManager; @@ -115,6 +115,6 @@ class TConvSeqProofGenerator : public ProofGenerator std::string d_name; }; -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__EXPR__TCONV_SEQ_PROOF_GENERATOR_H */ diff --git a/src/expr/term_canonize.cpp b/src/expr/term_canonize.cpp index 97f3c2539..11a992d16 100644 --- a/src/expr/term_canonize.cpp +++ b/src/expr/term_canonize.cpp @@ -19,9 +19,9 @@ // TODO #1216: move the code in this include #include "theory/quantifiers/term_util.h" -using namespace CVC5::kind; +using namespace cvc5::kind; -namespace CVC5 { +namespace cvc5 { namespace expr { TermCanonize::TermCanonize() : d_op_id_count(0), d_typ_id_count(0) {} @@ -209,4 +209,4 @@ Node TermCanonize::getCanonicalTerm(TNode n, bool apply_torder, bool doHoVar) } } // namespace expr -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/expr/term_canonize.h b/src/expr/term_canonize.h index f9f0fda24..f15bb2df0 100644 --- a/src/expr/term_canonize.h +++ b/src/expr/term_canonize.h @@ -20,7 +20,7 @@ #include <map> #include "expr/node.h" -namespace CVC5 { +namespace cvc5 { namespace expr { /** TermCanonize @@ -100,6 +100,6 @@ class TermCanonize }; } // namespace expr -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__EXPR__TERM_CANONIZE_H */ diff --git a/src/expr/term_context.cpp b/src/expr/term_context.cpp index 56c38a17c..883fa3e08 100644 --- a/src/expr/term_context.cpp +++ b/src/expr/term_context.cpp @@ -14,7 +14,7 @@ #include "expr/term_context.h" -namespace CVC5 { +namespace cvc5 { uint32_t TermContext::computeValueOp(TNode t, uint32_t tval) const { @@ -132,4 +132,4 @@ void PolarityTermContext::getFlags(uint32_t val, bool& hasPol, bool& pol) pol = val == 2; } -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/expr/term_context.h b/src/expr/term_context.h index 65cdbb23e..062104fc2 100644 --- a/src/expr/term_context.h +++ b/src/expr/term_context.h @@ -19,7 +19,7 @@ #include "expr/node.h" -namespace CVC5 { +namespace cvc5 { /** * This is an abstract class for computing "term context identifiers". A term @@ -163,6 +163,6 @@ class PolarityTermContext : public TermContext static void getFlags(uint32_t val, bool& hasPol, bool& pol); }; -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__EXPR__TERM_CONVERSION_PROOF_GENERATOR_H */ diff --git a/src/expr/term_context_node.cpp b/src/expr/term_context_node.cpp index 1afc599d2..564459d37 100644 --- a/src/expr/term_context_node.cpp +++ b/src/expr/term_context_node.cpp @@ -16,7 +16,7 @@ #include "expr/term_context.h" -namespace CVC5 { +namespace cvc5 { TCtxNode::TCtxNode(Node n, const TermContext* tctx) : d_node(n), d_val(tctx->initialValue()), d_tctx(tctx) @@ -73,4 +73,4 @@ Node TCtxNode::decomposeNodeHash(Node h, uint32_t& val) return h[0]; } -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/expr/term_context_node.h b/src/expr/term_context_node.h index 67d747557..5af435a56 100644 --- a/src/expr/term_context_node.h +++ b/src/expr/term_context_node.h @@ -19,7 +19,7 @@ #include "expr/node.h" -namespace CVC5 { +namespace cvc5 { class TCtxStack; class TermContext; @@ -74,6 +74,6 @@ class TCtxNode const TermContext* d_tctx; }; -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__EXPR__TERM_CONVERSION_PROOF_GENERATOR_H */ diff --git a/src/expr/term_context_stack.cpp b/src/expr/term_context_stack.cpp index 557683498..8a0fd91c9 100644 --- a/src/expr/term_context_stack.cpp +++ b/src/expr/term_context_stack.cpp @@ -16,7 +16,7 @@ #include "expr/term_context.h" -namespace CVC5 { +namespace cvc5 { TCtxStack::TCtxStack(const TermContext* tctx) : d_tctx(tctx) {} @@ -75,4 +75,4 @@ TCtxNode TCtxStack::getCurrentNode() const return TCtxNode(curr.first, curr.second, d_tctx); } -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/expr/term_context_stack.h b/src/expr/term_context_stack.h index 34c474a52..0042091ed 100644 --- a/src/expr/term_context_stack.h +++ b/src/expr/term_context_stack.h @@ -19,7 +19,7 @@ #include "expr/term_context_node.h" -namespace CVC5 { +namespace cvc5 { /** * A stack for term-context-sensitive terms. Its main advantage is that @@ -68,6 +68,6 @@ class TCtxStack const TermContext* d_tctx; }; -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__EXPR__TERM_CONTEXT_STACK_H */ diff --git a/src/expr/term_conversion_proof_generator.cpp b/src/expr/term_conversion_proof_generator.cpp index bfdf4d188..df4708f74 100644 --- a/src/expr/term_conversion_proof_generator.cpp +++ b/src/expr/term_conversion_proof_generator.cpp @@ -21,9 +21,9 @@ #include "expr/term_context.h" #include "expr/term_context_stack.h" -using namespace CVC5::kind; +using namespace cvc5::kind; -namespace CVC5 { +namespace cvc5 { std::ostream& operator<<(std::ostream& out, TConvPolicy tcpol) { @@ -588,4 +588,4 @@ std::string TConvProofGenerator::toStringDebug() const return ss.str(); } -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/expr/term_conversion_proof_generator.h b/src/expr/term_conversion_proof_generator.h index 734ef103e..e1f2b90e8 100644 --- a/src/expr/term_conversion_proof_generator.h +++ b/src/expr/term_conversion_proof_generator.h @@ -21,7 +21,7 @@ #include "expr/lazy_proof.h" #include "expr/proof_generator.h" -namespace CVC5 { +namespace cvc5 { class ProofNodeManager; class TermContext; @@ -242,6 +242,6 @@ class TConvProofGenerator : public ProofGenerator std::string toStringDebug() const; }; -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__EXPR__TERM_CONVERSION_PROOF_GENERATOR_H */ diff --git a/src/expr/type_checker.h b/src/expr/type_checker.h index b502d8013..fee02de75 100644 --- a/src/expr/type_checker.h +++ b/src/expr/type_checker.h @@ -22,7 +22,7 @@ #ifndef CVC4__EXPR__TYPE_CHECKER_H #define CVC4__EXPR__TYPE_CHECKER_H -namespace CVC5 { +namespace cvc5 { namespace expr { class TypeChecker { @@ -36,6 +36,6 @@ public: };/* class TypeChecker */ } // namespace expr -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__EXPR__TYPE_CHECKER_H */ diff --git a/src/expr/type_checker_template.cpp b/src/expr/type_checker_template.cpp index 07dca77e2..d99d5e82d 100644 --- a/src/expr/type_checker_template.cpp +++ b/src/expr/type_checker_template.cpp @@ -23,7 +23,7 @@ ${typechecker_includes} -namespace CVC5 { +namespace cvc5 { namespace expr { TypeNode TypeChecker::computeType(NodeManager* nodeManager, TNode n, bool check) @@ -72,4 +72,4 @@ ${construles} }/* TypeChecker::computeIsConst */ } // namespace expr -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/expr/type_checker_util.h b/src/expr/type_checker_util.h index 1ca23d374..207c242b8 100644 --- a/src/expr/type_checker_util.h +++ b/src/expr/type_checker_util.h @@ -26,7 +26,7 @@ #include "expr/node_manager.h" #include "expr/type_node.h" -namespace CVC5 { +namespace cvc5 { namespace expr { /** Type check returns the builtin operator sort */ @@ -202,4 +202,4 @@ class SimpleTypeRuleVar }; } // namespace expr -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/expr/type_matcher.cpp b/src/expr/type_matcher.cpp index 76d256157..9389ce4b8 100644 --- a/src/expr/type_matcher.cpp +++ b/src/expr/type_matcher.cpp @@ -14,7 +14,7 @@ #include "type_matcher.h" -namespace CVC5 { +namespace cvc5 { TypeMatcher::TypeMatcher(TypeNode dt) { @@ -125,4 +125,4 @@ void TypeMatcher::getMatches(std::vector<TypeNode>& types) const } } -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/expr/type_matcher.h b/src/expr/type_matcher.h index 651054313..a75bb7b8b 100644 --- a/src/expr/type_matcher.h +++ b/src/expr/type_matcher.h @@ -21,7 +21,7 @@ #include "expr/type_node.h" -namespace CVC5 { +namespace cvc5 { /** * This class is used for inferring the parameters of an instantiated @@ -68,6 +68,6 @@ class TypeMatcher void addTypes(const std::vector<TypeNode>& types); }; /* class TypeMatcher */ -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__MATCHER_H */ diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp index f73bde3eb..cbade1220 100644 --- a/src/expr/type_node.cpp +++ b/src/expr/type_node.cpp @@ -25,7 +25,7 @@ using namespace std; -namespace CVC5 { +namespace cvc5 { TypeNode TypeNode::s_null( &expr::NodeValue::null() ); @@ -499,7 +499,7 @@ TypeNode TypeNode::mostCommonTypeNode(TypeNode t0, TypeNode t1){ TypeNode TypeNode::commonTypeNode(TypeNode t0, TypeNode t1, bool isLeast) { Assert(NodeManager::currentNM() != NULL) - << "There is no current CVC5::NodeManager associated to this thread.\n" + << "There is no current cvc5::NodeManager associated to this thread.\n" "Perhaps a public-facing function is missing a NodeManagerScope ?"; Assert(!t0.isNull()); @@ -717,4 +717,4 @@ TypeNode TypeNode::getBagElementType() const return (*this)[0]; } -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/expr/type_node.h b/src/expr/type_node.h index 7b752c3e5..98515be2a 100644 --- a/src/expr/type_node.h +++ b/src/expr/type_node.h @@ -32,7 +32,7 @@ #include "expr/metakind.h" #include "util/cardinality.h" -namespace CVC5 { +namespace cvc5 { class NodeManager; class DType; @@ -749,11 +749,11 @@ inline std::ostream& operator<<(std::ostream& out, const TypeNode& n) { typedef TypeNode::HashFunction TypeNodeHashFunction; -} // namespace CVC5 +} // namespace cvc5 #include "expr/node_manager.h" -namespace CVC5 { +namespace cvc5 { inline TypeNode TypeNode::substitute(const TypeNode& type, @@ -860,7 +860,7 @@ template <class AttrKind> inline typename AttrKind::value_type TypeNode:: getAttribute(const AttrKind&) const { Assert(NodeManager::currentNM() != NULL) - << "There is no current CVC5::NodeManager associated to this thread.\n" + << "There is no current cvc5::NodeManager associated to this thread.\n" "Perhaps a public-facing function is missing a NodeManagerScope ?"; return NodeManager::currentNM()->getAttribute(d_nv, AttrKind()); } @@ -869,7 +869,7 @@ template <class AttrKind> inline bool TypeNode:: hasAttribute(const AttrKind&) const { Assert(NodeManager::currentNM() != NULL) - << "There is no current CVC5::NodeManager associated to this thread.\n" + << "There is no current cvc5::NodeManager associated to this thread.\n" "Perhaps a public-facing function is missing a NodeManagerScope ?"; return NodeManager::currentNM()->hasAttribute(d_nv, AttrKind()); } @@ -877,7 +877,7 @@ hasAttribute(const AttrKind&) const { template <class AttrKind> inline bool TypeNode::getAttribute(const AttrKind&, typename AttrKind::value_type& ret) const { Assert(NodeManager::currentNM() != NULL) - << "There is no current CVC5::NodeManager associated to this thread.\n" + << "There is no current cvc5::NodeManager associated to this thread.\n" "Perhaps a public-facing function is missing a NodeManagerScope ?"; return NodeManager::currentNM()->getAttribute(d_nv, AttrKind(), ret); } @@ -886,7 +886,7 @@ template <class AttrKind> inline void TypeNode:: setAttribute(const AttrKind&, const typename AttrKind::value_type& value) { Assert(NodeManager::currentNM() != NULL) - << "There is no current CVC5::NodeManager associated to this thread.\n" + << "There is no current cvc5::NodeManager associated to this thread.\n" "Perhaps a public-facing function is missing a NodeManagerScope ?"; NodeManager::currentNM()->setAttribute(d_nv, AttrKind(), value); } @@ -1069,6 +1069,6 @@ static void __attribute__((used)) debugPrintRawTypeNode(const TypeNode& n) { } #endif /* CVC4_DEBUG */ -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__NODE_H */ diff --git a/src/expr/type_properties_template.h b/src/expr/type_properties_template.h index abf5e6173..ce2696c5b 100644 --- a/src/expr/type_properties_template.h +++ b/src/expr/type_properties_template.h @@ -29,7 +29,7 @@ ${type_properties_includes} -namespace CVC5 { +namespace cvc5 { namespace kind { /** @@ -114,6 +114,6 @@ ${type_groundterms} } /* mkGroundTerm(TypeNode) */ } // namespace kind -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__TYPE_PROPERTIES_H */ diff --git a/src/expr/uninterpreted_constant.cpp b/src/expr/uninterpreted_constant.cpp index 9d8b12264..bd934e391 100644 --- a/src/expr/uninterpreted_constant.cpp +++ b/src/expr/uninterpreted_constant.cpp @@ -26,7 +26,7 @@ using namespace std; -namespace CVC5 { +namespace cvc5 { UninterpretedConstant::UninterpretedConstant(const TypeNode& type, Integer index) @@ -95,4 +95,4 @@ size_t UninterpretedConstantHashFunction::operator()( * IntegerHashFunction()(uc.getIndex()); } -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/expr/uninterpreted_constant.h b/src/expr/uninterpreted_constant.h index 00ad68212..94d7f85ed 100644 --- a/src/expr/uninterpreted_constant.h +++ b/src/expr/uninterpreted_constant.h @@ -24,7 +24,7 @@ #include "util/integer.h" -namespace CVC5 { +namespace cvc5 { class TypeNode; @@ -60,6 +60,6 @@ struct UninterpretedConstantHashFunction size_t operator()(const UninterpretedConstant& uc) const; }; /* struct UninterpretedConstantHashFunction */ -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__UNINTERPRETED_CONSTANT_H */ |