diff options
author | Aina Niemetz <aina.niemetz@gmail.com> | 2021-04-09 16:14:21 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-04-09 23:14:21 +0000 |
commit | 550c49a7dd2b13ea29743458336f0c0a0fb6099a (patch) | |
tree | b06962055a5de77d39c95fc577e54c0d7d69dcfd /src/expr | |
parent | ca7e206c239d8de0f25fb23544e4923641b85d11 (diff) |
Rename CVC4__ header guards to CVC5__. (#6326)
Diffstat (limited to 'src/expr')
57 files changed, 169 insertions, 169 deletions
diff --git a/src/expr/array_store_all.h b/src/expr/array_store_all.h index 65385b0c4..49031e28a 100644 --- a/src/expr/array_store_all.h +++ b/src/expr/array_store_all.h @@ -18,8 +18,8 @@ #include "cvc4_public.h" -#ifndef CVC4__ARRAY_STORE_ALL_H -#define CVC4__ARRAY_STORE_ALL_H +#ifndef CVC5__ARRAY_STORE_ALL_H +#define CVC5__ARRAY_STORE_ALL_H #include <iosfwd> #include <memory> @@ -71,4 +71,4 @@ struct ArrayStoreAllHashFunction } // namespace cvc5 -#endif /* CVC4__ARRAY_STORE_ALL_H */ +#endif /* CVC5__ARRAY_STORE_ALL_H */ diff --git a/src/expr/ascription_type.h b/src/expr/ascription_type.h index b216a0fa1..fe6f2c23f 100644 --- a/src/expr/ascription_type.h +++ b/src/expr/ascription_type.h @@ -16,8 +16,8 @@ #include "cvc4_public.h" -#ifndef CVC4__ASCRIPTION_TYPE_H -#define CVC4__ASCRIPTION_TYPE_H +#ifndef CVC5__ASCRIPTION_TYPE_H +#define CVC5__ASCRIPTION_TYPE_H #include <iosfwd> #include <memory> @@ -62,4 +62,4 @@ std::ostream& operator<<(std::ostream& out, AscriptionType at); } // namespace cvc5 -#endif /* CVC4__ASCRIPTION_TYPE_H */ +#endif /* CVC5__ASCRIPTION_TYPE_H */ diff --git a/src/expr/attribute.h b/src/expr/attribute.h index 6156ccc2d..9f2301d7e 100644 --- a/src/expr/attribute.h +++ b/src/expr/attribute.h @@ -21,8 +21,8 @@ #include "expr/node.h" #include "expr/type_node.h" -#ifndef CVC4__EXPR__ATTRIBUTE_H -#define CVC4__EXPR__ATTRIBUTE_H +#ifndef CVC5__EXPR__ATTRIBUTE_H +#define CVC5__EXPR__ATTRIBUTE_H #include <string> #include "expr/attribute_unique_id.h" @@ -623,4 +623,4 @@ NodeManager::setAttribute(TypeNode n, const AttrKind&, } // namespace cvc5 -#endif /* CVC4__EXPR__ATTRIBUTE_H */ +#endif /* CVC5__EXPR__ATTRIBUTE_H */ diff --git a/src/expr/attribute_internals.h b/src/expr/attribute_internals.h index db3e57675..2293e4b5a 100644 --- a/src/expr/attribute_internals.h +++ b/src/expr/attribute_internals.h @@ -20,8 +20,8 @@ # error expr/attribute_internals.h should only be included by expr/attribute.h #endif /* CVC4_ATTRIBUTE_H__INCLUDING__ATTRIBUTE_INTERNALS_H */ -#ifndef CVC4__EXPR__ATTRIBUTE_INTERNALS_H -#define CVC4__EXPR__ATTRIBUTE_INTERNALS_H +#ifndef CVC5__EXPR__ATTRIBUTE_INTERNALS_H +#define CVC5__EXPR__ATTRIBUTE_INTERNALS_H #include <unordered_map> @@ -514,4 +514,4 @@ const uint64_t Attribute<T, bool, context_dep>::s_id = } // namespace expr } // namespace cvc5 -#endif /* CVC4__EXPR__ATTRIBUTE_INTERNALS_H */ +#endif /* CVC5__EXPR__ATTRIBUTE_INTERNALS_H */ diff --git a/src/expr/bound_var_manager.h b/src/expr/bound_var_manager.h index ebd107737..d1d1c1a38 100644 --- a/src/expr/bound_var_manager.h +++ b/src/expr/bound_var_manager.h @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef CVC4__EXPR__BOUND_VAR_MANAGER_H -#define CVC4__EXPR__BOUND_VAR_MANAGER_H +#ifndef CVC5__EXPR__BOUND_VAR_MANAGER_H +#define CVC5__EXPR__BOUND_VAR_MANAGER_H #include <string> #include <unordered_set> @@ -100,4 +100,4 @@ class BoundVarManager } // namespace cvc5 -#endif /* CVC4__EXPR__BOUND_VAR_MANAGER_H */ +#endif /* CVC5__EXPR__BOUND_VAR_MANAGER_H */ diff --git a/src/expr/buffered_proof_generator.h b/src/expr/buffered_proof_generator.h index 7399b3741..228af460c 100644 --- a/src/expr/buffered_proof_generator.h +++ b/src/expr/buffered_proof_generator.h @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef CVC4__EXPR__BUFFERED_PROOF_GENERATOR_H -#define CVC4__EXPR__BUFFERED_PROOF_GENERATOR_H +#ifndef CVC5__EXPR__BUFFERED_PROOF_GENERATOR_H +#define CVC5__EXPR__BUFFERED_PROOF_GENERATOR_H #include "context/cdhashmap.h" #include "expr/proof_generator.h" @@ -59,4 +59,4 @@ class BufferedProofGenerator : public ProofGenerator } // namespace cvc5 -#endif /* CVC4__EXPR__BUFFERED_PROOF_GENERATOR_H */ +#endif /* CVC5__EXPR__BUFFERED_PROOF_GENERATOR_H */ diff --git a/src/expr/datatype_index.h b/src/expr/datatype_index.h index a239c387b..ca4d6d743 100644 --- a/src/expr/datatype_index.h +++ b/src/expr/datatype_index.h @@ -14,8 +14,8 @@ #include "cvc4_public.h" -#ifndef CVC4__DATATYPE_INDEX_H -#define CVC4__DATATYPE_INDEX_H +#ifndef CVC5__DATATYPE_INDEX_H +#define CVC5__DATATYPE_INDEX_H #include <iosfwd> @@ -66,4 +66,4 @@ struct DatatypeIndexConstantHashFunction } // namespace cvc5 -#endif /* CVC4__DATATYPE_H */ +#endif /* CVC5__DATATYPE_H */ diff --git a/src/expr/dtype.h b/src/expr/dtype.h index 524702bdd..e0f37d811 100644 --- a/src/expr/dtype.h +++ b/src/expr/dtype.h @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef CVC4__EXPR__DTYPE_H -#define CVC4__EXPR__DTYPE_H +#ifndef CVC5__EXPR__DTYPE_H +#define CVC5__EXPR__DTYPE_H #include <map> #include <string> diff --git a/src/expr/dtype_cons.h b/src/expr/dtype_cons.h index d444d9261..52b0a4d69 100644 --- a/src/expr/dtype_cons.h +++ b/src/expr/dtype_cons.h @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef CVC4__EXPR__DTYPE_CONS_H -#define CVC4__EXPR__DTYPE_CONS_H +#ifndef CVC5__EXPR__DTYPE_CONS_H +#define CVC5__EXPR__DTYPE_CONS_H #include <map> #include <string> diff --git a/src/expr/dtype_selector.h b/src/expr/dtype_selector.h index d45bcf8c5..66a4f4f4f 100644 --- a/src/expr/dtype_selector.h +++ b/src/expr/dtype_selector.h @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef CVC4__EXPR__DTYPE_SELECTOR_H -#define CVC4__EXPR__DTYPE_SELECTOR_H +#ifndef CVC5__EXPR__DTYPE_SELECTOR_H +#define CVC5__EXPR__DTYPE_SELECTOR_H #include <string> #include "expr/node.h" diff --git a/src/expr/emptybag.h b/src/expr/emptybag.h index f45bd9e96..19efe3a94 100644 --- a/src/expr/emptybag.h +++ b/src/expr/emptybag.h @@ -14,8 +14,8 @@ #include "cvc4_public.h" -#ifndef CVC4__EMPTY_BAG_H -#define CVC4__EMPTY_BAG_H +#ifndef CVC5__EMPTY_BAG_H +#define CVC5__EMPTY_BAG_H #include <iosfwd> #include <memory> @@ -60,4 +60,4 @@ struct EmptyBagHashFunction } // namespace cvc5 -#endif /* CVC4__EMPTY_BAG_H */ +#endif /* CVC5__EMPTY_BAG_H */ diff --git a/src/expr/emptyset.h b/src/expr/emptyset.h index aa6d5e143..b1c00a5ad 100644 --- a/src/expr/emptyset.h +++ b/src/expr/emptyset.h @@ -17,8 +17,8 @@ #include "cvc4_public.h" -#ifndef CVC4__EMPTY_SET_H -#define CVC4__EMPTY_SET_H +#ifndef CVC5__EMPTY_SET_H +#define CVC5__EMPTY_SET_H #include <iosfwd> #include <memory> @@ -62,4 +62,4 @@ struct EmptySetHashFunction } // namespace cvc5 -#endif /* CVC4__EMPTY_SET_H */ +#endif /* CVC5__EMPTY_SET_H */ diff --git a/src/expr/expr_iomanip.h b/src/expr/expr_iomanip.h index 674d4c6fd..91b0fcc2e 100644 --- a/src/expr/expr_iomanip.h +++ b/src/expr/expr_iomanip.h @@ -16,8 +16,8 @@ #include "cvc4_public.h" -#ifndef CVC4__EXPR__EXPR_IOMANIP_H -#define CVC4__EXPR__EXPR_IOMANIP_H +#ifndef CVC5__EXPR__EXPR_IOMANIP_H +#define CVC5__EXPR__EXPR_IOMANIP_H #include <iosfwd> @@ -175,4 +175,4 @@ std::ostream& operator<<(std::ostream& out, ExprSetDepth sd); } // namespace cvc5 -#endif /* CVC4__EXPR__EXPR_IOMANIP_H */ +#endif /* CVC5__EXPR__EXPR_IOMANIP_H */ diff --git a/src/expr/kind_map.h b/src/expr/kind_map.h index 0716ff4d0..28cbf5c37 100644 --- a/src/expr/kind_map.h +++ b/src/expr/kind_map.h @@ -17,8 +17,8 @@ #include "cvc4_private.h" -#ifndef CVC4__KIND_MAP_H -#define CVC4__KIND_MAP_H +#ifndef CVC5__KIND_MAP_H +#define CVC5__KIND_MAP_H #include <bitset> @@ -53,4 +53,4 @@ class KindMap } // namespace cvc5 -#endif /* CVC4__KIND_MAP_H */ +#endif /* CVC5__KIND_MAP_H */ diff --git a/src/expr/kind_template.h b/src/expr/kind_template.h index 484e8c273..d24f46551 100644 --- a/src/expr/kind_template.h +++ b/src/expr/kind_template.h @@ -16,8 +16,8 @@ #include "cvc4_public.h" -#ifndef CVC4__KIND_H -#define CVC4__KIND_H +#ifndef CVC5__KIND_H +#define CVC5__KIND_H #include <iosfwd> @@ -104,4 +104,4 @@ namespace theory { } // namespace theory } // namespace cvc5 -#endif /* CVC4__KIND_H */ +#endif /* CVC5__KIND_H */ diff --git a/src/expr/lazy_proof.h b/src/expr/lazy_proof.h index 3ab0ca49e..b60bfd409 100644 --- a/src/expr/lazy_proof.h +++ b/src/expr/lazy_proof.h @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef CVC4__EXPR__LAZY_PROOF_H -#define CVC4__EXPR__LAZY_PROOF_H +#ifndef CVC5__EXPR__LAZY_PROOF_H +#define CVC5__EXPR__LAZY_PROOF_H #include "expr/proof.h" @@ -107,4 +107,4 @@ class LazyCDProof : public CDProof } // namespace cvc5 -#endif /* CVC4__EXPR__LAZY_PROOF_H */ +#endif /* CVC5__EXPR__LAZY_PROOF_H */ diff --git a/src/expr/lazy_proof_chain.h b/src/expr/lazy_proof_chain.h index 41488c821..87881fae1 100644 --- a/src/expr/lazy_proof_chain.h +++ b/src/expr/lazy_proof_chain.h @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef CVC4__EXPR__LAZY_PROOF_CHAIN_H -#define CVC4__EXPR__LAZY_PROOF_CHAIN_H +#ifndef CVC5__EXPR__LAZY_PROOF_CHAIN_H +#define CVC5__EXPR__LAZY_PROOF_CHAIN_H #include <vector> @@ -150,4 +150,4 @@ class LazyCDProofChain : public ProofGenerator } // namespace cvc5 -#endif /* CVC4__EXPR__LAZY_PROOF_CHAIN_H */ +#endif /* CVC5__EXPR__LAZY_PROOF_CHAIN_H */ diff --git a/src/expr/match_trie.h b/src/expr/match_trie.h index 70ce549e1..6f85d20c9 100644 --- a/src/expr/match_trie.h +++ b/src/expr/match_trie.h @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef CVC4__EXPR__MATCH_TRIE_H -#define CVC4__EXPR__MATCH_TRIE_H +#ifndef CVC5__EXPR__MATCH_TRIE_H +#define CVC5__EXPR__MATCH_TRIE_H #include <map> #include <vector> @@ -79,4 +79,4 @@ class MatchTrie } // namespace expr } // namespace cvc5 -#endif /* CVC4__THEORY__QUANTIFIERS__CANDIDATE_REWRITE_FILTER_H */ +#endif /* CVC5__THEORY__QUANTIFIERS__CANDIDATE_REWRITE_FILTER_H */ diff --git a/src/expr/metakind_template.h b/src/expr/metakind_template.h index 5c78d87d3..7f232b4e2 100644 --- a/src/expr/metakind_template.h +++ b/src/expr/metakind_template.h @@ -16,8 +16,8 @@ #include "cvc4_private.h" -#ifndef CVC4__KIND__METAKIND_H -#define CVC4__KIND__METAKIND_H +#ifndef CVC5__KIND__METAKIND_H +#define CVC5__KIND__METAKIND_H #include <iosfwd> @@ -128,11 +128,11 @@ struct NodeValuePoolEq { #include "expr/node_value.h" -#endif /* CVC4__KIND__METAKIND_H */ +#endif /* CVC5__KIND__METAKIND_H */ ${metakind_includes} -#ifdef CVC4__NODE_MANAGER_NEEDS_CONSTANT_MAP +#ifdef CVC5__NODE_MANAGER_NEEDS_CONSTANT_MAP namespace cvc5 { @@ -207,4 +207,4 @@ Kind operatorToKind(::cvc5::expr::NodeValue* nv); } // namespace cvc5 -#endif /* CVC4__NODE_MANAGER_NEEDS_CONSTANT_MAP */ +#endif /* CVC5__NODE_MANAGER_NEEDS_CONSTANT_MAP */ diff --git a/src/expr/node.h b/src/expr/node.h index fb3cf1478..b8e44a4cb 100644 --- a/src/expr/node.h +++ b/src/expr/node.h @@ -19,8 +19,8 @@ // circular dependency #include "expr/node_value.h" -#ifndef CVC4__NODE_H -#define CVC4__NODE_H +#ifndef CVC5__NODE_H +#define CVC5__NODE_H #include <iostream> #include <map> @@ -1492,4 +1492,4 @@ static void __attribute__((used)) debugPrintRawTNode(const NodeTemplate<false>& } // namespace cvc5 -#endif /* CVC4__NODE_H */ +#endif /* CVC5__NODE_H */ diff --git a/src/expr/node_algorithm.h b/src/expr/node_algorithm.h index 7ae56e5ba..09630cb28 100644 --- a/src/expr/node_algorithm.h +++ b/src/expr/node_algorithm.h @@ -18,8 +18,8 @@ #include "cvc4_private.h" -#ifndef CVC4__EXPR__NODE_ALGORITHM_H -#define CVC4__EXPR__NODE_ALGORITHM_H +#ifndef CVC5__EXPR__NODE_ALGORITHM_H +#define CVC5__EXPR__NODE_ALGORITHM_H #include <unordered_map> #include <vector> diff --git a/src/expr/node_builder.h b/src/expr/node_builder.h index 218a08766..271a217dc 100644 --- a/src/expr/node_builder.h +++ b/src/expr/node_builder.h @@ -137,8 +137,8 @@ /* strong dependency; make sure node is included first */ #include "expr/node.h" -#ifndef CVC4__NODE_BUILDER_H -#define CVC4__NODE_BUILDER_H +#ifndef CVC5__NODE_BUILDER_H +#define CVC5__NODE_BUILDER_H #include <iostream> #include <vector> @@ -407,4 +407,4 @@ std::ostream& operator<<(std::ostream& out, const NodeBuilder& nb); } // namespace cvc5 -#endif /* CVC4__NODE_BUILDER_H */ +#endif /* CVC5__NODE_BUILDER_H */ diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index 465ddf588..98eb111bc 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -23,8 +23,8 @@ #include "expr/node.h" #include "expr/type_node.h" -#ifndef CVC4__NODE_MANAGER_H -#define CVC4__NODE_MANAGER_H +#ifndef CVC5__NODE_MANAGER_H +#define CVC5__NODE_MANAGER_H #include <vector> #include <string> @@ -1197,9 +1197,9 @@ inline void NodeManager::poolRemove(expr::NodeValue* nv) { } // namespace cvc5 -#define CVC4__NODE_MANAGER_NEEDS_CONSTANT_MAP +#define CVC5__NODE_MANAGER_NEEDS_CONSTANT_MAP #include "expr/metakind.h" -#undef CVC4__NODE_MANAGER_NEEDS_CONSTANT_MAP +#undef CVC5__NODE_MANAGER_NEEDS_CONSTANT_MAP #include "expr/node_builder.h" @@ -1572,4 +1572,4 @@ NodeClass NodeManager::mkConstInternal(const T& val) { } // namespace cvc5 -#endif /* CVC4__NODE_MANAGER_H */ +#endif /* CVC5__NODE_MANAGER_H */ diff --git a/src/expr/node_self_iterator.h b/src/expr/node_self_iterator.h index d8558de97..73fecf4ef 100644 --- a/src/expr/node_self_iterator.h +++ b/src/expr/node_self_iterator.h @@ -16,8 +16,8 @@ #include "cvc4_private.h" -#ifndef CVC4__EXPR__NODE_SELF_ITERATOR_H -#define CVC4__EXPR__NODE_SELF_ITERATOR_H +#ifndef CVC5__EXPR__NODE_SELF_ITERATOR_H +#define CVC5__EXPR__NODE_SELF_ITERATOR_H #include <iterator> @@ -125,4 +125,4 @@ inline bool NodeSelfIterator::operator!=(NodeSelfIterator i) const { } // namespace expr } // namespace cvc5 -#endif /* CVC4__EXPR__NODE_SELF_ITERATOR_H */ +#endif /* CVC5__EXPR__NODE_SELF_ITERATOR_H */ diff --git a/src/expr/node_traversal.h b/src/expr/node_traversal.h index 015bcec06..4b695d2ba 100644 --- a/src/expr/node_traversal.h +++ b/src/expr/node_traversal.h @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef CVC4__EXPR__NODE_TRAVERSAL_H -#define CVC4__EXPR__NODE_TRAVERSAL_H +#ifndef CVC5__EXPR__NODE_TRAVERSAL_H +#define CVC5__EXPR__NODE_TRAVERSAL_H #include <iterator> #include <unordered_map> @@ -146,4 +146,4 @@ class NodeDfsIterable } // namespace cvc5 -#endif // CVC4__EXPR__NODE_TRAVERSAL_H +#endif // CVC5__EXPR__NODE_TRAVERSAL_H diff --git a/src/expr/node_trie.h b/src/expr/node_trie.h index 2f42b6a52..c2c686295 100644 --- a/src/expr/node_trie.h +++ b/src/expr/node_trie.h @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef CVC4__EXPR__NODE_TRIE_H -#define CVC4__EXPR__NODE_TRIE_H +#ifndef CVC5__EXPR__NODE_TRIE_H +#define CVC5__EXPR__NODE_TRIE_H #include <map> #include "expr/node.h" @@ -109,4 +109,4 @@ typedef NodeTemplateTrie<false> TNodeTrie; } // namespace theory } // namespace cvc5 -#endif /* CVC4__EXPR__NODE_TRIE_H */ +#endif /* CVC5__EXPR__NODE_TRIE_H */ diff --git a/src/expr/node_value.h b/src/expr/node_value.h index 3f4b7602e..3e1ccd67e 100644 --- a/src/expr/node_value.h +++ b/src/expr/node_value.h @@ -23,8 +23,8 @@ // circular dependency #include "expr/metakind.h" -#ifndef CVC4__EXPR__NODE_VALUE_H -#define CVC4__EXPR__NODE_VALUE_H +#ifndef CVC5__EXPR__NODE_VALUE_H +#define CVC5__EXPR__NODE_VALUE_H #include <iterator> #include <string> @@ -546,4 +546,4 @@ static void __attribute__((used)) debugPrintRawNodeValue(const expr::NodeValue* } // namespace cvc5 -#endif /* CVC4__EXPR__NODE_VALUE_H */ +#endif /* CVC5__EXPR__NODE_VALUE_H */ diff --git a/src/expr/proof.h b/src/expr/proof.h index af859df93..5cea5354e 100644 --- a/src/expr/proof.h +++ b/src/expr/proof.h @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef CVC4__EXPR__PROOF_H -#define CVC4__EXPR__PROOF_H +#ifndef CVC5__EXPR__PROOF_H +#define CVC5__EXPR__PROOF_H #include <vector> @@ -275,4 +275,4 @@ class CDProof : public ProofGenerator } // namespace cvc5 -#endif /* CVC4__EXPR__PROOF_MANAGER_H */ +#endif /* CVC5__EXPR__PROOF_MANAGER_H */ diff --git a/src/expr/proof_checker.h b/src/expr/proof_checker.h index 99f9f3ec8..06e813e2d 100644 --- a/src/expr/proof_checker.h +++ b/src/expr/proof_checker.h @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef CVC4__EXPR__PROOF_CHECKER_H -#define CVC4__EXPR__PROOF_CHECKER_H +#ifndef CVC5__EXPR__PROOF_CHECKER_H +#define CVC5__EXPR__PROOF_CHECKER_H #include <map> @@ -204,4 +204,4 @@ class ProofChecker } // namespace cvc5 -#endif /* CVC4__EXPR__PROOF_CHECKER_H */ +#endif /* CVC5__EXPR__PROOF_CHECKER_H */ diff --git a/src/expr/proof_ensure_closed.h b/src/expr/proof_ensure_closed.h index d610147d4..8a7461287 100644 --- a/src/expr/proof_ensure_closed.h +++ b/src/expr/proof_ensure_closed.h @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef CVC4__EXPR__PROOF_ENSURE_CLOSED_H -#define CVC4__EXPR__PROOF_ENSURE_CLOSED_H +#ifndef CVC5__EXPR__PROOF_ENSURE_CLOSED_H +#define CVC5__EXPR__PROOF_ENSURE_CLOSED_H #include "expr/node.h" @@ -69,4 +69,4 @@ void pfnEnsureClosedWrt(ProofNode* pn, const char* ctx); } // namespace cvc5 -#endif /* CVC4__EXPR__PROOF_ENSURE_CLOSED_H */ +#endif /* CVC5__EXPR__PROOF_ENSURE_CLOSED_H */ diff --git a/src/expr/proof_generator.h b/src/expr/proof_generator.h index 76a2c9b3b..2cc64e083 100644 --- a/src/expr/proof_generator.h +++ b/src/expr/proof_generator.h @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef CVC4__EXPR__PROOF_GENERATOR_H -#define CVC4__EXPR__PROOF_GENERATOR_H +#ifndef CVC5__EXPR__PROOF_GENERATOR_H +#define CVC5__EXPR__PROOF_GENERATOR_H #include "expr/node.h" @@ -109,4 +109,4 @@ class ProofGenerator } // namespace cvc5 -#endif /* CVC4__EXPR__PROOF_GENERATOR_H */ +#endif /* CVC5__EXPR__PROOF_GENERATOR_H */ diff --git a/src/expr/proof_node.h b/src/expr/proof_node.h index ddd8e1e27..b849e2391 100644 --- a/src/expr/proof_node.h +++ b/src/expr/proof_node.h @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef CVC4__EXPR__PROOF_NODE_H -#define CVC4__EXPR__PROOF_NODE_H +#ifndef CVC5__EXPR__PROOF_NODE_H +#define CVC5__EXPR__PROOF_NODE_H #include <vector> @@ -141,4 +141,4 @@ std::ostream& operator<<(std::ostream& out, const ProofNode& pn); } // namespace cvc5 -#endif /* CVC4__EXPR__PROOF_NODE_H */ +#endif /* CVC5__EXPR__PROOF_NODE_H */ diff --git a/src/expr/proof_node_algorithm.h b/src/expr/proof_node_algorithm.h index 01faa8a40..6aa045481 100644 --- a/src/expr/proof_node_algorithm.h +++ b/src/expr/proof_node_algorithm.h @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef CVC4__EXPR__PROOF_NODE_ALGORITHM_H -#define CVC4__EXPR__PROOF_NODE_ALGORITHM_H +#ifndef CVC5__EXPR__PROOF_NODE_ALGORITHM_H +#define CVC5__EXPR__PROOF_NODE_ALGORITHM_H #include <vector> @@ -72,4 +72,4 @@ bool containsSubproof(ProofNode* pn, } // namespace expr } // namespace cvc5 -#endif /* CVC4__EXPR__PROOF_NODE_ALGORITHM_H */ +#endif /* CVC5__EXPR__PROOF_NODE_ALGORITHM_H */ diff --git a/src/expr/proof_node_manager.h b/src/expr/proof_node_manager.h index 32513cd0d..251d43ed3 100644 --- a/src/expr/proof_node_manager.h +++ b/src/expr/proof_node_manager.h @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef CVC4__EXPR__PROOF_NODE_MANAGER_H -#define CVC4__EXPR__PROOF_NODE_MANAGER_H +#ifndef CVC5__EXPR__PROOF_NODE_MANAGER_H +#define CVC5__EXPR__PROOF_NODE_MANAGER_H #include <vector> @@ -202,4 +202,4 @@ class ProofNodeManager } // namespace cvc5 -#endif /* CVC4__EXPR__PROOF_NODE_H */ +#endif /* CVC5__EXPR__PROOF_NODE_H */ diff --git a/src/expr/proof_node_to_sexpr.h b/src/expr/proof_node_to_sexpr.h index bbbde39f6..31b04466e 100644 --- a/src/expr/proof_node_to_sexpr.h +++ b/src/expr/proof_node_to_sexpr.h @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef CVC4__EXPR__PROOF_NODE_TO_SEXPR_H -#define CVC4__EXPR__PROOF_NODE_TO_SEXPR_H +#ifndef CVC5__EXPR__PROOF_NODE_TO_SEXPR_H +#define CVC5__EXPR__PROOF_NODE_TO_SEXPR_H #include <map> @@ -66,4 +66,4 @@ class ProofNodeToSExpr } // namespace cvc5 -#endif /* CVC4__EXPR__PROOF_RULE_H */ +#endif /* CVC5__EXPR__PROOF_RULE_H */ diff --git a/src/expr/proof_node_updater.h b/src/expr/proof_node_updater.h index 268fcda5e..6f3e5b420 100644 --- a/src/expr/proof_node_updater.h +++ b/src/expr/proof_node_updater.h @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef CVC4__EXPR__PROOF_NODE_UPDATER_H -#define CVC4__EXPR__PROOF_NODE_UPDATER_H +#ifndef CVC5__EXPR__PROOF_NODE_UPDATER_H +#define CVC5__EXPR__PROOF_NODE_UPDATER_H #include <map> #include <memory> diff --git a/src/expr/proof_rule.h b/src/expr/proof_rule.h index cec85cc99..8aaf697d4 100644 --- a/src/expr/proof_rule.h +++ b/src/expr/proof_rule.h @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef CVC4__EXPR__PROOF_RULE_H -#define CVC4__EXPR__PROOF_RULE_H +#ifndef CVC5__EXPR__PROOF_RULE_H +#define CVC5__EXPR__PROOF_RULE_H #include <iosfwd> @@ -1385,4 +1385,4 @@ struct PfRuleHashFunction } // namespace cvc5 -#endif /* CVC4__EXPR__PROOF_RULE_H */ +#endif /* CVC5__EXPR__PROOF_RULE_H */ diff --git a/src/expr/proof_set.h b/src/expr/proof_set.h index 0509ed9d4..f684045c6 100644 --- a/src/expr/proof_set.h +++ b/src/expr/proof_set.h @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef CVC4__EXPR__PROOF_SET_H -#define CVC4__EXPR__PROOF_SET_H +#ifndef CVC5__EXPR__PROOF_SET_H +#define CVC5__EXPR__PROOF_SET_H #include <memory> @@ -72,4 +72,4 @@ class CDProofSet } // namespace cvc5 -#endif /* CVC4__EXPR__LAZY_PROOF_SET_H */ +#endif /* CVC5__EXPR__LAZY_PROOF_SET_H */ diff --git a/src/expr/proof_step_buffer.h b/src/expr/proof_step_buffer.h index 99a7608ff..ef57540c7 100644 --- a/src/expr/proof_step_buffer.h +++ b/src/expr/proof_step_buffer.h @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef CVC4__EXPR__PROOF_STEP_BUFFER_H -#define CVC4__EXPR__PROOF_STEP_BUFFER_H +#ifndef CVC5__EXPR__PROOF_STEP_BUFFER_H +#define CVC5__EXPR__PROOF_STEP_BUFFER_H #include <vector> @@ -94,4 +94,4 @@ class ProofStepBuffer } // namespace cvc5 -#endif /* CVC4__EXPR__PROOF_STEP_BUFFER_H */ +#endif /* CVC5__EXPR__PROOF_STEP_BUFFER_H */ diff --git a/src/expr/record.h b/src/expr/record.h index 436b5b269..fa6a34395 100644 --- a/src/expr/record.h +++ b/src/expr/record.h @@ -16,8 +16,8 @@ #include "cvc4_public.h" -#ifndef CVC4__RECORD_H -#define CVC4__RECORD_H +#ifndef CVC5__RECORD_H +#define CVC5__RECORD_H #include <iostream> #include <string> @@ -58,4 +58,4 @@ using Record = std::vector<std::pair<std::string, TypeNode>>; } // namespace cvc5 -#endif /* CVC4__RECORD_H */ +#endif /* CVC5__RECORD_H */ diff --git a/src/expr/sequence.h b/src/expr/sequence.h index e42851f58..e75c38956 100644 --- a/src/expr/sequence.h +++ b/src/expr/sequence.h @@ -14,8 +14,8 @@ #include "cvc4_public.h" -#ifndef CVC4__EXPR__SEQUENCE_H -#define CVC4__EXPR__SEQUENCE_H +#ifndef CVC5__EXPR__SEQUENCE_H +#define CVC5__EXPR__SEQUENCE_H #include <memory> #include <vector> @@ -175,4 +175,4 @@ std::ostream& operator<<(std::ostream& os, const Sequence& s); } // namespace cvc5 -#endif /* CVC4__EXPR__SEQUENCE_H */ +#endif /* CVC5__EXPR__SEQUENCE_H */ diff --git a/src/expr/skolem_manager.h b/src/expr/skolem_manager.h index 6cebee5d9..b69853a85 100644 --- a/src/expr/skolem_manager.h +++ b/src/expr/skolem_manager.h @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef CVC4__EXPR__SKOLEM_MANAGER_H -#define CVC4__EXPR__SKOLEM_MANAGER_H +#ifndef CVC5__EXPR__SKOLEM_MANAGER_H +#define CVC5__EXPR__SKOLEM_MANAGER_H #include <string> @@ -314,4 +314,4 @@ class SkolemManager } // namespace cvc5 -#endif /* CVC4__EXPR__PROOF_SKOLEM_CACHE_H */ +#endif /* CVC5__EXPR__PROOF_SKOLEM_CACHE_H */ diff --git a/src/expr/subs.h b/src/expr/subs.h index fdb8e4551..d351eeaa7 100644 --- a/src/expr/subs.h +++ b/src/expr/subs.h @@ -12,8 +12,8 @@ ** \brief Simple substitution utility **/ -#ifndef CVC4__EXPR__SUBS_H -#define CVC4__EXPR__SUBS_H +#ifndef CVC5__EXPR__SUBS_H +#define CVC5__EXPR__SUBS_H #include <map> #include <vector> @@ -82,4 +82,4 @@ std::ostream& operator<<(std::ostream& out, const Subs& s); } // namespace cvc5 -#endif /* CVC4__EXPR__SUBS_H */ +#endif /* CVC5__EXPR__SUBS_H */ diff --git a/src/expr/sygus_datatype.h b/src/expr/sygus_datatype.h index e5d1de740..b3130a028 100644 --- a/src/expr/sygus_datatype.h +++ b/src/expr/sygus_datatype.h @@ -13,8 +13,8 @@ **/ #include "cvc4_private.h" -#ifndef CVC4__EXPR__SYGUS_DATATYPE_H -#define CVC4__EXPR__SYGUS_DATATYPE_H +#ifndef CVC5__EXPR__SYGUS_DATATYPE_H +#define CVC5__EXPR__SYGUS_DATATYPE_H #include <string> #include <vector> diff --git a/src/expr/symbol_manager.h b/src/expr/symbol_manager.h index 4ff307bc2..96bc3954d 100644 --- a/src/expr/symbol_manager.h +++ b/src/expr/symbol_manager.h @@ -14,8 +14,8 @@ #include "cvc4_public.h" -#ifndef CVC4__EXPR__SYMBOL_MANAGER_H -#define CVC4__EXPR__SYMBOL_MANAGER_H +#ifndef CVC5__EXPR__SYMBOL_MANAGER_H +#define CVC5__EXPR__SYMBOL_MANAGER_H #include <map> #include <memory> @@ -158,4 +158,4 @@ class CVC4_EXPORT SymbolManager } // namespace cvc5 -#endif /* CVC4__EXPR__SYMBOL_MANAGER_H */ +#endif /* CVC5__EXPR__SYMBOL_MANAGER_H */ diff --git a/src/expr/symbol_table.h b/src/expr/symbol_table.h index fbb1969dd..98cba9ff8 100644 --- a/src/expr/symbol_table.h +++ b/src/expr/symbol_table.h @@ -16,8 +16,8 @@ #include "cvc4_public.h" -#ifndef CVC4__SYMBOL_TABLE_H -#define CVC4__SYMBOL_TABLE_H +#ifndef CVC5__SYMBOL_TABLE_H +#define CVC5__SYMBOL_TABLE_H #include <memory> #include <string> @@ -212,4 +212,4 @@ class CVC4_EXPORT SymbolTable } // namespace cvc5 -#endif /* CVC4__SYMBOL_TABLE_H */ +#endif /* CVC5__SYMBOL_TABLE_H */ diff --git a/src/expr/tconv_seq_proof_generator.h b/src/expr/tconv_seq_proof_generator.h index 151cd511d..2e14acb98 100644 --- a/src/expr/tconv_seq_proof_generator.h +++ b/src/expr/tconv_seq_proof_generator.h @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef CVC4__EXPR__TCONV_SEQ_PROOF_GENERATOR_H -#define CVC4__EXPR__TCONV_SEQ_PROOF_GENERATOR_H +#ifndef CVC5__EXPR__TCONV_SEQ_PROOF_GENERATOR_H +#define CVC5__EXPR__TCONV_SEQ_PROOF_GENERATOR_H #include "context/cdhashmap.h" #include "expr/node.h" @@ -117,4 +117,4 @@ class TConvSeqProofGenerator : public ProofGenerator } // namespace cvc5 -#endif /* CVC4__EXPR__TCONV_SEQ_PROOF_GENERATOR_H */ +#endif /* CVC5__EXPR__TCONV_SEQ_PROOF_GENERATOR_H */ diff --git a/src/expr/term_canonize.h b/src/expr/term_canonize.h index f15bb2df0..a032f3a84 100644 --- a/src/expr/term_canonize.h +++ b/src/expr/term_canonize.h @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef CVC4__EXPR__TERM_CANONIZE_H -#define CVC4__EXPR__TERM_CANONIZE_H +#ifndef CVC5__EXPR__TERM_CANONIZE_H +#define CVC5__EXPR__TERM_CANONIZE_H #include <map> #include "expr/node.h" @@ -102,4 +102,4 @@ class TermCanonize } // namespace expr } // namespace cvc5 -#endif /* CVC4__EXPR__TERM_CANONIZE_H */ +#endif /* CVC5__EXPR__TERM_CANONIZE_H */ diff --git a/src/expr/term_context.h b/src/expr/term_context.h index 062104fc2..5bdab4fca 100644 --- a/src/expr/term_context.h +++ b/src/expr/term_context.h @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef CVC4__EXPR__TERM_CONTEXT_H -#define CVC4__EXPR__TERM_CONTEXT_H +#ifndef CVC5__EXPR__TERM_CONTEXT_H +#define CVC5__EXPR__TERM_CONTEXT_H #include "expr/node.h" @@ -165,4 +165,4 @@ class PolarityTermContext : public TermContext } // namespace cvc5 -#endif /* CVC4__EXPR__TERM_CONVERSION_PROOF_GENERATOR_H */ +#endif /* CVC5__EXPR__TERM_CONVERSION_PROOF_GENERATOR_H */ diff --git a/src/expr/term_context_node.h b/src/expr/term_context_node.h index 5af435a56..1c3542b57 100644 --- a/src/expr/term_context_node.h +++ b/src/expr/term_context_node.h @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef CVC4__EXPR__TERM_CONTEXT_NODE_H -#define CVC4__EXPR__TERM_CONTEXT_NODE_H +#ifndef CVC5__EXPR__TERM_CONTEXT_NODE_H +#define CVC5__EXPR__TERM_CONTEXT_NODE_H #include "expr/node.h" @@ -76,4 +76,4 @@ class TCtxNode } // namespace cvc5 -#endif /* CVC4__EXPR__TERM_CONVERSION_PROOF_GENERATOR_H */ +#endif /* CVC5__EXPR__TERM_CONVERSION_PROOF_GENERATOR_H */ diff --git a/src/expr/term_context_stack.h b/src/expr/term_context_stack.h index 0042091ed..48892e654 100644 --- a/src/expr/term_context_stack.h +++ b/src/expr/term_context_stack.h @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef CVC4__EXPR__TERM_CONTEXT_STACK_H -#define CVC4__EXPR__TERM_CONTEXT_STACK_H +#ifndef CVC5__EXPR__TERM_CONTEXT_STACK_H +#define CVC5__EXPR__TERM_CONTEXT_STACK_H #include "expr/term_context_node.h" @@ -70,4 +70,4 @@ class TCtxStack } // namespace cvc5 -#endif /* CVC4__EXPR__TERM_CONTEXT_STACK_H */ +#endif /* CVC5__EXPR__TERM_CONTEXT_STACK_H */ diff --git a/src/expr/term_conversion_proof_generator.h b/src/expr/term_conversion_proof_generator.h index e1f2b90e8..961ac61cc 100644 --- a/src/expr/term_conversion_proof_generator.h +++ b/src/expr/term_conversion_proof_generator.h @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef CVC4__EXPR__TERM_CONVERSION_PROOF_GENERATOR_H -#define CVC4__EXPR__TERM_CONVERSION_PROOF_GENERATOR_H +#ifndef CVC5__EXPR__TERM_CONVERSION_PROOF_GENERATOR_H +#define CVC5__EXPR__TERM_CONVERSION_PROOF_GENERATOR_H #include "context/cdhashmap.h" #include "expr/lazy_proof.h" @@ -244,4 +244,4 @@ class TConvProofGenerator : public ProofGenerator } // namespace cvc5 -#endif /* CVC4__EXPR__TERM_CONVERSION_PROOF_GENERATOR_H */ +#endif /* CVC5__EXPR__TERM_CONVERSION_PROOF_GENERATOR_H */ diff --git a/src/expr/type_checker.h b/src/expr/type_checker.h index fee02de75..5b806e671 100644 --- a/src/expr/type_checker.h +++ b/src/expr/type_checker.h @@ -19,8 +19,8 @@ // ordering dependence #include "expr/node.h" -#ifndef CVC4__EXPR__TYPE_CHECKER_H -#define CVC4__EXPR__TYPE_CHECKER_H +#ifndef CVC5__EXPR__TYPE_CHECKER_H +#define CVC5__EXPR__TYPE_CHECKER_H namespace cvc5 { namespace expr { @@ -38,4 +38,4 @@ public: } // namespace expr } // namespace cvc5 -#endif /* CVC4__EXPR__TYPE_CHECKER_H */ +#endif /* CVC5__EXPR__TYPE_CHECKER_H */ diff --git a/src/expr/type_matcher.h b/src/expr/type_matcher.h index a75bb7b8b..6df955c06 100644 --- a/src/expr/type_matcher.h +++ b/src/expr/type_matcher.h @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef CVC4__EXPR__TYPE_MATCHER_H -#define CVC4__EXPR__TYPE_MATCHER_H +#ifndef CVC5__EXPR__TYPE_MATCHER_H +#define CVC5__EXPR__TYPE_MATCHER_H #include <vector> @@ -70,4 +70,4 @@ class TypeMatcher } // namespace cvc5 -#endif /* CVC4__MATCHER_H */ +#endif /* CVC5__MATCHER_H */ diff --git a/src/expr/type_node.h b/src/expr/type_node.h index f8cc5a44b..41f9afe6f 100644 --- a/src/expr/type_node.h +++ b/src/expr/type_node.h @@ -19,8 +19,8 @@ // circular dependency #include "expr/node_value.h" -#ifndef CVC4__TYPE_NODE_H -#define CVC4__TYPE_NODE_H +#ifndef CVC5__TYPE_NODE_H +#define CVC5__TYPE_NODE_H #include <iostream> #include <string> @@ -1070,4 +1070,4 @@ static void __attribute__((used)) debugPrintRawTypeNode(const TypeNode& n) { } // namespace cvc5 -#endif /* CVC4__NODE_H */ +#endif /* CVC5__NODE_H */ diff --git a/src/expr/type_properties_template.h b/src/expr/type_properties_template.h index ce2696c5b..c6fb29b71 100644 --- a/src/expr/type_properties_template.h +++ b/src/expr/type_properties_template.h @@ -16,8 +16,8 @@ #include "cvc4_private.h" -#ifndef CVC4__TYPE_PROPERTIES_H -#define CVC4__TYPE_PROPERTIES_H +#ifndef CVC5__TYPE_PROPERTIES_H +#define CVC5__TYPE_PROPERTIES_H #include <sstream> @@ -116,4 +116,4 @@ ${type_groundterms} } // namespace kind } // namespace cvc5 -#endif /* CVC4__TYPE_PROPERTIES_H */ +#endif /* CVC5__TYPE_PROPERTIES_H */ diff --git a/src/expr/uninterpreted_constant.h b/src/expr/uninterpreted_constant.h index 94d7f85ed..841b32626 100644 --- a/src/expr/uninterpreted_constant.h +++ b/src/expr/uninterpreted_constant.h @@ -16,8 +16,8 @@ #include "cvc4_public.h" -#ifndef CVC4__UNINTERPRETED_CONSTANT_H -#define CVC4__UNINTERPRETED_CONSTANT_H +#ifndef CVC5__UNINTERPRETED_CONSTANT_H +#define CVC5__UNINTERPRETED_CONSTANT_H #include <iosfwd> #include <memory> @@ -62,4 +62,4 @@ struct UninterpretedConstantHashFunction } // namespace cvc5 -#endif /* CVC4__UNINTERPRETED_CONSTANT_H */ +#endif /* CVC5__UNINTERPRETED_CONSTANT_H */ |