#include "cvc4_public.h"
-#ifndef CVC4__API__CHECKS_H
-#define CVC4__API__CHECKS_H
+#ifndef CVC5__API__CHECKS_H
+#define CVC5__API__CHECKS_H
namespace cvc4 {
namespace api {
#include "cvc4_private_library.h"
-#ifndef CVC4__CHECK_H
-#define CVC4__CHECK_H
+#ifndef CVC5__CHECK_H
+#define CVC5__CHECK_H
#include <cstdarg>
#include <ostream>
} // namespace cvc5
-#endif /* CVC4__CHECK_H */
+#endif /* CVC5__CHECK_H */
#include "cvc4_public.h"
-#ifndef CVC4__CONFIGURATION_H
-#define CVC4__CONFIGURATION_H
+#ifndef CVC5__CONFIGURATION_H
+#define CVC5__CONFIGURATION_H
#include <string>
} // namespace cvc5
-#endif /* CVC4__CONFIGURATION_H */
+#endif /* CVC5__CONFIGURATION_H */
#include "cvc4_private.h"
-#ifndef CVC4__CONFIGURATION_PRIVATE_H
-#define CVC4__CONFIGURATION_PRIVATE_H
+#ifndef CVC5__CONFIGURATION_PRIVATE_H
+#define CVC5__CONFIGURATION_PRIVATE_H
#include <string>
} // namespace cvc5
-#endif /* CVC4__CONFIGURATION_PRIVATE_H */
+#endif /* CVC5__CONFIGURATION_PRIVATE_H */
#include "cvc4_public.h"
-#ifndef CVC4__EXCEPTION_H
-#define CVC4__EXCEPTION_H
+#ifndef CVC5__EXCEPTION_H
+#define CVC5__EXCEPTION_H
#include <exception>
#include <iosfwd>
} // namespace cvc5
-#endif /* CVC4__EXCEPTION_H */
+#endif /* CVC5__EXCEPTION_H */
#include "cvc4_public.h"
-#ifndef CVC4__LISTENER_H
-#define CVC4__LISTENER_H
+#ifndef CVC5__LISTENER_H
+#define CVC5__LISTENER_H
namespace cvc5 {
} // namespace cvc5
-#endif /* CVC4__LISTENER_H */
+#endif /* CVC5__LISTENER_H */
#include "cvc4_private.h"
-#ifndef CVC4__BASE__MAP_UTIL_H
-#define CVC4__BASE__MAP_UTIL_H
+#ifndef CVC5__BASE__MAP_UTIL_H
+#define CVC5__BASE__MAP_UTIL_H
#include "base/check.h"
} // namespace cvc5
-#endif /* CVC4__BASE__MAP_UTIL_H */
+#endif /* CVC5__BASE__MAP_UTIL_H */
#include "cvc4_public.h"
-#ifndef CVC4__SMT__MODAL_EXCEPTION_H
-#define CVC4__SMT__MODAL_EXCEPTION_H
+#ifndef CVC5__SMT__MODAL_EXCEPTION_H
+#define CVC5__SMT__MODAL_EXCEPTION_H
#include "base/exception.h"
} // namespace cvc5
-#endif /* CVC4__SMT__MODAL_EXCEPTION_H */
+#endif /* CVC5__SMT__MODAL_EXCEPTION_H */
#include "cvc4_private_library.h"
-#ifndef CVC4__OUTPUT_H
-#define CVC4__OUTPUT_H
+#ifndef CVC5__OUTPUT_H
+#define CVC5__OUTPUT_H
#include <cstdio>
#include <ios>
} // namespace cvc5
-#endif /* CVC4__OUTPUT_H */
+#endif /* CVC5__OUTPUT_H */
#include "cvc4_private.h"
-#ifndef CVC4__UTIL__BACKTRACKABLE_H
-#define CVC4__UTIL__BACKTRACKABLE_H
+#ifndef CVC5__UTIL__BACKTRACKABLE_H
+#define CVC5__UTIL__BACKTRACKABLE_H
#include <cstdlib>
#include <vector>
} // namespace cvc5
-#endif /* CVC4__UTIL__BACKTRACKABLE_H */
+#endif /* CVC5__UTIL__BACKTRACKABLE_H */
#include "cvc4_private.h"
-#ifndef CVC4__CONTEXT__CDHASHMAP_H
-#define CVC4__CONTEXT__CDHASHMAP_H
+#ifndef CVC5__CONTEXT__CDHASHMAP_H
+#define CVC5__CONTEXT__CDHASHMAP_H
#include <functional>
#include <iterator>
} // namespace context
} // namespace cvc5
-#endif /* CVC4__CONTEXT__CDHASHMAP_H */
+#endif /* CVC5__CONTEXT__CDHASHMAP_H */
#include "cvc4_public.h"
-#ifndef CVC4__CONTEXT__CDHASHMAP_FORWARD_H
-#define CVC4__CONTEXT__CDHASHMAP_FORWARD_H
+#ifndef CVC5__CONTEXT__CDHASHMAP_FORWARD_H
+#define CVC5__CONTEXT__CDHASHMAP_FORWARD_H
#include <functional>
/// \endcond
-#endif /* CVC4__CONTEXT__CDHASHMAP_FORWARD_H */
+#endif /* CVC5__CONTEXT__CDHASHMAP_FORWARD_H */
#include "cvc4_private.h"
-#ifndef CVC4__CONTEXT__CDHASHSET_H
-#define CVC4__CONTEXT__CDHASHSET_H
+#ifndef CVC5__CONTEXT__CDHASHSET_H
+#define CVC5__CONTEXT__CDHASHSET_H
#include "base/check.h"
#include "context/cdinsert_hashmap.h"
} // namespace context
} // namespace cvc5
-#endif /* CVC4__CONTEXT__CDHASHSET_H */
+#endif /* CVC5__CONTEXT__CDHASHSET_H */
#include "cvc4_public.h"
-#ifndef CVC4__CONTEXT__CDSET_FORWARD_H
-#define CVC4__CONTEXT__CDSET_FORWARD_H
+#ifndef CVC5__CONTEXT__CDSET_FORWARD_H
+#define CVC5__CONTEXT__CDSET_FORWARD_H
#include <functional>
} // namespace context
} // namespace cvc5
-#endif /* CVC4__CONTEXT__CDSET_FORWARD_H */
+#endif /* CVC5__CONTEXT__CDSET_FORWARD_H */
#include "cvc4_public.h"
-#ifndef CVC4__CONTEXT__CDINSERT_HASHMAP_FORWARD_H
-#define CVC4__CONTEXT__CDINSERT_HASHMAP_FORWARD_H
+#ifndef CVC5__CONTEXT__CDINSERT_HASHMAP_FORWARD_H
+#define CVC5__CONTEXT__CDINSERT_HASHMAP_FORWARD_H
#include <functional>
} // namespace context
} // namespace cvc5
-#endif /* CVC4__CONTEXT__CDINSERT_HASHMAP_FORWARD_H */
+#endif /* CVC5__CONTEXT__CDINSERT_HASHMAP_FORWARD_H */
#include "cvc4_private.h"
-#ifndef CVC4__CONTEXT__CDLIST_H
-#define CVC4__CONTEXT__CDLIST_H
+#ifndef CVC5__CONTEXT__CDLIST_H
+#define CVC5__CONTEXT__CDLIST_H
#include <cstring>
#include <iterator>
} // namespace context
} // namespace cvc5
-#endif /* CVC4__CONTEXT__CDLIST_H */
+#endif /* CVC5__CONTEXT__CDLIST_H */
#include "cvc4_public.h"
-#ifndef CVC4__CONTEXT__CDLIST_FORWARD_H
-#define CVC4__CONTEXT__CDLIST_FORWARD_H
+#ifndef CVC5__CONTEXT__CDLIST_FORWARD_H
+#define CVC5__CONTEXT__CDLIST_FORWARD_H
#include <memory>
} // namespace context
} // namespace cvc5
-#endif /* CVC4__CONTEXT__CDLIST_FORWARD_H */
+#endif /* CVC5__CONTEXT__CDLIST_FORWARD_H */
#include "cvc4_private.h"
-#ifndef CVC4__CONTEXT__CDO_H
-#define CVC4__CONTEXT__CDO_H
+#ifndef CVC5__CONTEXT__CDO_H
+#define CVC5__CONTEXT__CDO_H
#include "context/context.h"
} // namespace context
} // namespace cvc5
-#endif /* CVC4__CONTEXT__CDO_H */
+#endif /* CVC5__CONTEXT__CDO_H */
#include "cvc4_private.h"
-#ifndef CVC4__CONTEXT__CDQUEUE_H
-#define CVC4__CONTEXT__CDQUEUE_H
+#ifndef CVC5__CONTEXT__CDQUEUE_H
+#define CVC5__CONTEXT__CDQUEUE_H
#include "context/context.h"
#include "context/cdlist.h"
} // namespace context
} // namespace cvc5
-#endif /* CVC4__CONTEXT__CDQUEUE_H */
+#endif /* CVC5__CONTEXT__CDQUEUE_H */
#include "cvc4_private.h"
-#ifndef CVC4__CONTEXT__CDTRAIL_QUEUE_H
-#define CVC4__CONTEXT__CDTRAIL_QUEUE_H
+#ifndef CVC5__CONTEXT__CDTRAIL_QUEUE_H
+#define CVC5__CONTEXT__CDTRAIL_QUEUE_H
#include "context/cdlist.h"
#include "context/cdo.h"
} // namespace context
} // namespace cvc5
-#endif /* CVC4__CONTEXT__CDTRAIL_QUEUE_H */
+#endif /* CVC5__CONTEXT__CDTRAIL_QUEUE_H */
#include "cvc4_private.h"
-#ifndef CVC4__CONTEXT__CONTEXT_H
-#define CVC4__CONTEXT__CONTEXT_H
+#ifndef CVC5__CONTEXT__CONTEXT_H
+#define CVC5__CONTEXT__CONTEXT_H
#include <cstdlib>
#include <iostream>
} // namespace context
} // namespace cvc5
-#endif /* CVC4__CONTEXT__CONTEXT_H */
+#endif /* CVC5__CONTEXT__CONTEXT_H */
#include "cvc4_private.h"
-#ifndef CVC4__CONTEXT__CONTEXT_MM_H
-#define CVC4__CONTEXT__CONTEXT_MM_H
+#ifndef CVC5__CONTEXT__CONTEXT_MM_H
+#define CVC5__CONTEXT__CONTEXT_MM_H
#ifndef CVC4_DEBUG_CONTEXT_MEMORY_MANAGER
#include <deque>
} // namespace context
} // namespace cvc5
-#endif /* CVC4__CONTEXT__CONTEXT_MM_H */
+#endif /* CVC5__CONTEXT__CONTEXT_MM_H */
#include "cvc4_private.h"
-#ifndef CVC4__DECISION__DECISION_ATTRIBUTES_H
-#define CVC4__DECISION__DECISION_ATTRIBUTES_H
+#ifndef CVC5__DECISION__DECISION_ATTRIBUTES_H
+#define CVC5__DECISION__DECISION_ATTRIBUTES_H
#include "options/decision_weight.h"
#include "expr/attribute.h"
} // namespace decision
} // namespace cvc5
-#endif /* CVC4__DECISION__DECISION_ATTRIBUTES_H */
+#endif /* CVC5__DECISION__DECISION_ATTRIBUTES_H */
#include "cvc4_private.h"
-#ifndef CVC4__DECISION__DECISION_ENGINE_H
-#define CVC4__DECISION__DECISION_ENGINE_H
+#ifndef CVC5__DECISION__DECISION_ENGINE_H
+#define CVC5__DECISION__DECISION_ENGINE_H
#include "base/output.h"
#include "context/cdo.h"
} // namespace cvc5
-#endif /* CVC4__DECISION__DECISION_ENGINE_H */
+#endif /* CVC5__DECISION__DECISION_ENGINE_H */
#include "cvc4_private.h"
-#ifndef CVC4__DECISION__DECISION_STRATEGY_H
-#define CVC4__DECISION__DECISION_STRATEGY_H
+#ifndef CVC5__DECISION__DECISION_STRATEGY_H
+#define CVC5__DECISION__DECISION_STRATEGY_H
#include <vector>
} // namespace decision
} // namespace cvc5
-#endif /* CVC4__DECISION__DECISION_STRATEGY_H */
+#endif /* CVC5__DECISION__DECISION_STRATEGY_H */
#include "cvc4_private.h"
-#ifndef CVC4__DECISION__JUSTIFICATION_HEURISTIC
-#define CVC4__DECISION__JUSTIFICATION_HEURISTIC
+#ifndef CVC5__DECISION__JUSTIFICATION_HEURISTIC
+#define CVC5__DECISION__JUSTIFICATION_HEURISTIC
#include <unordered_set>
#include <utility>
}/* namespace decision */
} // namespace cvc5
-#endif /* CVC4__DECISION__JUSTIFICATION_HEURISTIC */
+#endif /* CVC5__DECISION__JUSTIFICATION_HEURISTIC */
#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>
} // namespace cvc5
-#endif /* CVC4__ARRAY_STORE_ALL_H */
+#endif /* CVC5__ARRAY_STORE_ALL_H */
#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>
} // namespace cvc5
-#endif /* CVC4__ASCRIPTION_TYPE_H */
+#endif /* CVC5__ASCRIPTION_TYPE_H */
#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"
} // namespace cvc5
-#endif /* CVC4__EXPR__ATTRIBUTE_H */
+#endif /* CVC5__EXPR__ATTRIBUTE_H */
# 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>
} // namespace expr
} // namespace cvc5
-#endif /* CVC4__EXPR__ATTRIBUTE_INTERNALS_H */
+#endif /* CVC5__EXPR__ATTRIBUTE_INTERNALS_H */
#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>
} // namespace cvc5
-#endif /* CVC4__EXPR__BOUND_VAR_MANAGER_H */
+#endif /* CVC5__EXPR__BOUND_VAR_MANAGER_H */
#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"
} // namespace cvc5
-#endif /* CVC4__EXPR__BUFFERED_PROOF_GENERATOR_H */
+#endif /* CVC5__EXPR__BUFFERED_PROOF_GENERATOR_H */
#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>
} // namespace cvc5
-#endif /* CVC4__DATATYPE_H */
+#endif /* CVC5__DATATYPE_H */
#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>
#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>
#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"
#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>
} // namespace cvc5
-#endif /* CVC4__EMPTY_BAG_H */
+#endif /* CVC5__EMPTY_BAG_H */
#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>
} // namespace cvc5
-#endif /* CVC4__EMPTY_SET_H */
+#endif /* CVC5__EMPTY_SET_H */
#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>
} // namespace cvc5
-#endif /* CVC4__EXPR__EXPR_IOMANIP_H */
+#endif /* CVC5__EXPR__EXPR_IOMANIP_H */
#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>
} // namespace cvc5
-#endif /* CVC4__KIND_MAP_H */
+#endif /* CVC5__KIND_MAP_H */
#include "cvc4_public.h"
-#ifndef CVC4__KIND_H
-#define CVC4__KIND_H
+#ifndef CVC5__KIND_H
+#define CVC5__KIND_H
#include <iosfwd>
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__KIND_H */
+#endif /* CVC5__KIND_H */
#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"
} // namespace cvc5
-#endif /* CVC4__EXPR__LAZY_PROOF_H */
+#endif /* CVC5__EXPR__LAZY_PROOF_H */
#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>
} // namespace cvc5
-#endif /* CVC4__EXPR__LAZY_PROOF_CHAIN_H */
+#endif /* CVC5__EXPR__LAZY_PROOF_CHAIN_H */
#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>
} // namespace expr
} // namespace cvc5
-#endif /* CVC4__THEORY__QUANTIFIERS__CANDIDATE_REWRITE_FILTER_H */
+#endif /* CVC5__THEORY__QUANTIFIERS__CANDIDATE_REWRITE_FILTER_H */
#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>
#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 {
} // namespace cvc5
-#endif /* CVC4__NODE_MANAGER_NEEDS_CONSTANT_MAP */
+#endif /* CVC5__NODE_MANAGER_NEEDS_CONSTANT_MAP */
// 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>
} // namespace cvc5
-#endif /* CVC4__NODE_H */
+#endif /* CVC5__NODE_H */
#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>
/* 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>
} // namespace cvc5
-#endif /* CVC4__NODE_BUILDER_H */
+#endif /* CVC5__NODE_BUILDER_H */
#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>
} // 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"
} // namespace cvc5
-#endif /* CVC4__NODE_MANAGER_H */
+#endif /* CVC5__NODE_MANAGER_H */
#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>
} // namespace expr
} // namespace cvc5
-#endif /* CVC4__EXPR__NODE_SELF_ITERATOR_H */
+#endif /* CVC5__EXPR__NODE_SELF_ITERATOR_H */
#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>
} // namespace cvc5
-#endif // CVC4__EXPR__NODE_TRAVERSAL_H
+#endif // CVC5__EXPR__NODE_TRAVERSAL_H
#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"
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__EXPR__NODE_TRIE_H */
+#endif /* CVC5__EXPR__NODE_TRIE_H */
// 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>
} // namespace cvc5
-#endif /* CVC4__EXPR__NODE_VALUE_H */
+#endif /* CVC5__EXPR__NODE_VALUE_H */
#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>
} // namespace cvc5
-#endif /* CVC4__EXPR__PROOF_MANAGER_H */
+#endif /* CVC5__EXPR__PROOF_MANAGER_H */
#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>
} // namespace cvc5
-#endif /* CVC4__EXPR__PROOF_CHECKER_H */
+#endif /* CVC5__EXPR__PROOF_CHECKER_H */
#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"
const char* ctx);
} // namespace cvc5
-#endif /* CVC4__EXPR__PROOF_ENSURE_CLOSED_H */
+#endif /* CVC5__EXPR__PROOF_ENSURE_CLOSED_H */
#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"
} // namespace cvc5
-#endif /* CVC4__EXPR__PROOF_GENERATOR_H */
+#endif /* CVC5__EXPR__PROOF_GENERATOR_H */
#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>
} // namespace cvc5
-#endif /* CVC4__EXPR__PROOF_NODE_H */
+#endif /* CVC5__EXPR__PROOF_NODE_H */
#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>
} // namespace expr
} // namespace cvc5
-#endif /* CVC4__EXPR__PROOF_NODE_ALGORITHM_H */
+#endif /* CVC5__EXPR__PROOF_NODE_ALGORITHM_H */
#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>
} // namespace cvc5
-#endif /* CVC4__EXPR__PROOF_NODE_H */
+#endif /* CVC5__EXPR__PROOF_NODE_H */
#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>
} // namespace cvc5
-#endif /* CVC4__EXPR__PROOF_RULE_H */
+#endif /* CVC5__EXPR__PROOF_RULE_H */
#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>
#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>
} // namespace cvc5
-#endif /* CVC4__EXPR__PROOF_RULE_H */
+#endif /* CVC5__EXPR__PROOF_RULE_H */
#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>
} // namespace cvc5
-#endif /* CVC4__EXPR__LAZY_PROOF_SET_H */
+#endif /* CVC5__EXPR__LAZY_PROOF_SET_H */
#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>
} // namespace cvc5
-#endif /* CVC4__EXPR__PROOF_STEP_BUFFER_H */
+#endif /* CVC5__EXPR__PROOF_STEP_BUFFER_H */
#include "cvc4_public.h"
-#ifndef CVC4__RECORD_H
-#define CVC4__RECORD_H
+#ifndef CVC5__RECORD_H
+#define CVC5__RECORD_H
#include <iostream>
#include <string>
} // namespace cvc5
-#endif /* CVC4__RECORD_H */
+#endif /* CVC5__RECORD_H */
#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>
} // namespace cvc5
-#endif /* CVC4__EXPR__SEQUENCE_H */
+#endif /* CVC5__EXPR__SEQUENCE_H */
#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>
} // namespace cvc5
-#endif /* CVC4__EXPR__PROOF_SKOLEM_CACHE_H */
+#endif /* CVC5__EXPR__PROOF_SKOLEM_CACHE_H */
** \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>
} // namespace cvc5
-#endif /* CVC4__EXPR__SUBS_H */
+#endif /* CVC5__EXPR__SUBS_H */
**/
#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>
#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>
} // namespace cvc5
-#endif /* CVC4__EXPR__SYMBOL_MANAGER_H */
+#endif /* CVC5__EXPR__SYMBOL_MANAGER_H */
#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>
} // namespace cvc5
-#endif /* CVC4__SYMBOL_TABLE_H */
+#endif /* CVC5__SYMBOL_TABLE_H */
#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"
} // namespace cvc5
-#endif /* CVC4__EXPR__TCONV_SEQ_PROOF_GENERATOR_H */
+#endif /* CVC5__EXPR__TCONV_SEQ_PROOF_GENERATOR_H */
#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"
} // namespace expr
} // namespace cvc5
-#endif /* CVC4__EXPR__TERM_CANONIZE_H */
+#endif /* CVC5__EXPR__TERM_CANONIZE_H */
#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"
} // namespace cvc5
-#endif /* CVC4__EXPR__TERM_CONVERSION_PROOF_GENERATOR_H */
+#endif /* CVC5__EXPR__TERM_CONVERSION_PROOF_GENERATOR_H */
#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"
} // namespace cvc5
-#endif /* CVC4__EXPR__TERM_CONVERSION_PROOF_GENERATOR_H */
+#endif /* CVC5__EXPR__TERM_CONVERSION_PROOF_GENERATOR_H */
#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"
} // namespace cvc5
-#endif /* CVC4__EXPR__TERM_CONTEXT_STACK_H */
+#endif /* CVC5__EXPR__TERM_CONTEXT_STACK_H */
#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"
} // namespace cvc5
-#endif /* CVC4__EXPR__TERM_CONVERSION_PROOF_GENERATOR_H */
+#endif /* CVC5__EXPR__TERM_CONVERSION_PROOF_GENERATOR_H */
// 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 {
} // namespace expr
} // namespace cvc5
-#endif /* CVC4__EXPR__TYPE_CHECKER_H */
+#endif /* CVC5__EXPR__TYPE_CHECKER_H */
#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>
} // namespace cvc5
-#endif /* CVC4__MATCHER_H */
+#endif /* CVC5__MATCHER_H */
// 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>
} // namespace cvc5
-#endif /* CVC4__NODE_H */
+#endif /* CVC5__NODE_H */
#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>
} // namespace kind
} // namespace cvc5
-#endif /* CVC4__TYPE_PROPERTIES_H */
+#endif /* CVC5__TYPE_PROPERTIES_H */
#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>
} // namespace cvc5
-#endif /* CVC4__UNINTERPRETED_CONSTANT_H */
+#endif /* CVC5__UNINTERPRETED_CONSTANT_H */
#include "cvc4_private_library.h"
-#ifndef CVC4__LIB__CLOCK_GETTIME_H
-#define CVC4__LIB__CLOCK_GETTIME_H
+#ifndef CVC5__LIB__CLOCK_GETTIME_H
+#define CVC5__LIB__CLOCK_GETTIME_H
#include "lib/replacements.h"
#endif /* __cplusplus */
#endif /* HAVE_CLOCK_GETTIME */
-#endif /*CVC4__LIB__CLOCK_GETTIME_H */
+#endif /*CVC5__LIB__CLOCK_GETTIME_H */
#include "cvc4_private.h"
-#ifndef CVC4__LIB__FFS_H
-#define CVC4__LIB__FFS_H
+#ifndef CVC5__LIB__FFS_H
+#define CVC5__LIB__FFS_H
//We include this for HAVE_FFS
#include "cvc4autoconfig.h"
#endif /* __cplusplus */
#endif /* HAVE_FFS */
-#endif /* CVC4__LIB__FFS_H */
+#endif /* CVC5__LIB__FFS_H */
** Common header for replacement function sources.
**/
-#ifndef CVC4__LIB__REPLACEMENTS_H
-#define CVC4__LIB__REPLACEMENTS_H
+#ifndef CVC5__LIB__REPLACEMENTS_H
+#define CVC5__LIB__REPLACEMENTS_H
#if (defined(__BUILDING_CVC4LIB) || defined(__BUILDING_CVC4LIB_UNIT_TEST)) && !defined(__BUILDING_STATISTICS_FOR_EXPORT)
# include "cvc4_private.h"
# endif
#endif
-#endif /* CVC4__LIB__REPLACEMENTS_H */
+#endif /* CVC5__LIB__REPLACEMENTS_H */
#include "cvc4_private.h"
-#ifndef CVC4__LIB__STRTOK_R_H
-#define CVC4__LIB__STRTOK_R_H
+#ifndef CVC5__LIB__STRTOK_R_H
+#define CVC5__LIB__STRTOK_R_H
#ifdef HAVE_STRTOK_R
#endif /* __cplusplus */
#endif /* HAVE_STRTOK_R */
-#endif /* CVC4__LIB__STRTOK_R_H */
+#endif /* CVC5__LIB__STRTOK_R_H */
** \brief An additional layer between commands and invoking them.
**/
-#ifndef CVC4__MAIN__COMMAND_EXECUTOR_H
-#define CVC4__MAIN__COMMAND_EXECUTOR_H
+#ifndef CVC5__MAIN__COMMAND_EXECUTOR_H
+#define CVC5__MAIN__COMMAND_EXECUTOR_H
#include <iosfwd>
#include <string>
} // namespace main
} // namespace cvc5
-#endif /* CVC4__MAIN__COMMAND_EXECUTOR_H */
+#endif /* CVC5__MAIN__COMMAND_EXECUTOR_H */
** \brief Interactive shell for CVC4
**/
-#ifndef CVC4__INTERACTIVE_SHELL_H
-#define CVC4__INTERACTIVE_SHELL_H
+#ifndef CVC5__INTERACTIVE_SHELL_H
+#define CVC5__INTERACTIVE_SHELL_H
#include <iosfwd>
#include <string>
} // namespace cvc5
-#endif /* CVC4__INTERACTIVE_SHELL_H */
+#endif /* CVC5__INTERACTIVE_SHELL_H */
#include "cvc4autoconfig.h"
#include "options/options.h"
-#ifndef CVC4__MAIN__MAIN_H
-#define CVC4__MAIN__MAIN_H
+#ifndef CVC5__MAIN__MAIN_H
+#define CVC5__MAIN__MAIN_H
namespace cvc5 {
namespace main {
int runCvc4(int argc, char* argv[], cvc5::Options&);
void printUsage(cvc5::Options&, bool full = false);
-#endif /* CVC4__MAIN__MAIN_H */
+#endif /* CVC5__MAIN__MAIN_H */
** Implementation of signal handlers.
**/
-#ifndef CVC4__MAIN__SIGNAL_HANDLERS_H
-#define CVC4__MAIN__SIGNAL_HANDLERS_H
+#ifndef CVC5__MAIN__SIGNAL_HANDLERS_H
+#define CVC5__MAIN__SIGNAL_HANDLERS_H
namespace cvc5 {
namespace main {
} // namespace main
} // namespace cvc5
-#endif /* CVC4__MAIN__SIGNAL_HANDLERS_H */
+#endif /* CVC5__MAIN__SIGNAL_HANDLERS_H */
** Implementation of time limits that are imposed by the --tlimit option.
**/
-#ifndef CVC4__MAIN__TIME_LIMIT_H
-#define CVC4__MAIN__TIME_LIMIT_H
+#ifndef CVC5__MAIN__TIME_LIMIT_H
+#define CVC5__MAIN__TIME_LIMIT_H
#include "options/options.h"
} // namespace main
} // namespace cvc5
-#endif /* CVC4__MAIN__TIME_LIMIT_H */
+#endif /* CVC5__MAIN__TIME_LIMIT_H */
** \brief Optimizer for BitVector type
**/
-#ifndef CVC4__OMT__BITVECTOR_OPTIMIZER_H
-#define CVC4__OMT__BITVECTOR_OPTIMIZER_H
+#ifndef CVC5__OMT__BITVECTOR_OPTIMIZER_H
+#define CVC5__OMT__BITVECTOR_OPTIMIZER_H
#include "omt/omt_optimizer.h"
} // namespace cvc5::omt
-#endif /* CVC4__OMT__BITVECTOR_OPTIMIZER_H */
+#endif /* CVC5__OMT__BITVECTOR_OPTIMIZER_H */
** \brief Optimizer for Integer type
**/
-#ifndef CVC4__OMT__INTEGER_OPTIMIZER_H
-#define CVC4__OMT__INTEGER_OPTIMIZER_H
+#ifndef CVC5__OMT__INTEGER_OPTIMIZER_H
+#define CVC5__OMT__INTEGER_OPTIMIZER_H
#include "omt/omt_optimizer.h"
} // namespace cvc5::omt
-#endif /* CVC4__OMT__INTEGER_OPTIMIZER_H */
+#endif /* CVC5__OMT__INTEGER_OPTIMIZER_H */
** \brief The base class for optimizers of individual CVC4 type
**/
-#ifndef CVC4__OMT__OMT_OPTIMIZER_H
-#define CVC4__OMT__OMT_OPTIMIZER_H
+#ifndef CVC5__OMT__OMT_OPTIMIZER_H
+#define CVC5__OMT__OMT_OPTIMIZER_H
#include "smt/optimization_solver.h"
} // namespace cvc5::omt
-#endif /* CVC4__OMT__OMT_OPTIMIZER_H */
+#endif /* CVC5__OMT__OMT_OPTIMIZER_H */
#include "cvc4_private.h"
-#ifndef CVC4__BASE_HANDLERS_H
-#define CVC4__BASE_HANDLERS_H
+#ifndef CVC5__BASE_HANDLERS_H
+#define CVC5__BASE_HANDLERS_H
#include <iostream>
#include <string>
} // namespace options
} // namespace cvc5
-#endif /* CVC4__BASE_HANDLERS_H */
+#endif /* CVC5__BASE_HANDLERS_H */
#include "cvc4_private.h"
-#ifndef CVC4__OPTIONS__DECISION_WEIGHT_H
-#define CVC4__OPTIONS__DECISION_WEIGHT_H
+#ifndef CVC5__OPTIONS__DECISION_WEIGHT_H
+#define CVC5__OPTIONS__DECISION_WEIGHT_H
namespace cvc5 {
namespace decision {
} // namespace decision
} // namespace cvc5
-#endif /* CVC4__OPTIONS__DECISION_WEIGHT_H */
+#endif /* CVC5__OPTIONS__DECISION_WEIGHT_H */
#include "cvc4_public.h"
-#ifndef CVC4__LANGUAGE_H
-#define CVC4__LANGUAGE_H
+#ifndef CVC5__LANGUAGE_H
+#define CVC5__LANGUAGE_H
#include <ostream>
#include <string>
} // namespace language
} // namespace cvc5
-#endif /* CVC4__LANGUAGE_H */
+#endif /* CVC5__LANGUAGE_H */
#include "cvc4_private.h"
-#ifndef CVC4__OPTIONS__${id}$_H
-#define CVC4__OPTIONS__${id}$_H
+#ifndef CVC5__OPTIONS__${id}$_H
+#define CVC5__OPTIONS__${id}$_H
#include "options/options.h"
} // namespace options
} // namespace cvc5
-#endif /* CVC4__OPTIONS__${id}$_H */
+#endif /* CVC5__OPTIONS__${id}$_H */
//clang-format on
#include "cvc4_private.h"
-#ifndef CVC4__OPEN_OSTREAM_H
-#define CVC4__OPEN_OSTREAM_H
+#ifndef CVC5__OPEN_OSTREAM_H
+#define CVC5__OPEN_OSTREAM_H
#include <iosfwd>
#include <map>
} // namespace cvc5
-#endif /* CVC4__OPEN_OSTREAM_H */
+#endif /* CVC5__OPEN_OSTREAM_H */
#include "cvc4_public.h"
-#ifndef CVC4__OPTION_EXCEPTION_H
-#define CVC4__OPTION_EXCEPTION_H
+#ifndef CVC5__OPTION_EXCEPTION_H
+#define CVC5__OPTION_EXCEPTION_H
#include "base/exception.h"
#include "cvc4_export.h"
} // namespace cvc5
-#endif /* CVC4__OPTION_EXCEPTION_H */
+#endif /* CVC5__OPTION_EXCEPTION_H */
#include "cvc4_public.h"
-#ifndef CVC4__OPTIONS__OPTIONS_H
-#define CVC4__OPTIONS__OPTIONS_H
+#ifndef CVC5__OPTIONS__OPTIONS_H
+#define CVC5__OPTIONS__OPTIONS_H
#include <fstream>
#include <ostream>
} // namespace cvc5
-#endif /* CVC4__OPTIONS__OPTIONS_H */
+#endif /* CVC5__OPTIONS__OPTIONS_H */
#include "cvc4_private.h"
-#ifndef CVC4__OPTIONS__OPTIONS_HANDLER_H
-#define CVC4__OPTIONS__OPTIONS_HANDLER_H
+#ifndef CVC5__OPTIONS__OPTIONS_HANDLER_H
+#define CVC5__OPTIONS__OPTIONS_HANDLER_H
#include <ostream>
#include <string>
} // namespace options
} // namespace cvc5
-#endif /* CVC4__OPTIONS__OPTIONS_HANDLER_H */
+#endif /* CVC5__OPTIONS__OPTIONS_HANDLER_H */
#include "cvc4_private.h"
-#ifndef CVC4__OPTIONS__OPTIONS_HOLDER_H
-#define CVC4__OPTIONS__OPTIONS_HOLDER_H
+#ifndef CVC5__OPTIONS__OPTIONS_HOLDER_H
+#define CVC5__OPTIONS__OPTIONS_HOLDER_H
// clang-format off
${headers_module}$
} // namespace options
} // namespace cvc5
-#endif /* CVC4__OPTIONS__OPTIONS_HOLDER_H */
+#endif /* CVC5__OPTIONS__OPTIONS_HOLDER_H */
// clang-format on
#include "cvc4_private.h"
-#ifndef CVC4__OPTIONS__OPTIONS_LISTENER_H
-#define CVC4__OPTIONS__OPTIONS_LISTENER_H
+#ifndef CVC5__OPTIONS__OPTIONS_LISTENER_H
+#define CVC5__OPTIONS__OPTIONS_LISTENER_H
#include <string>
} // namespace cvc5
-#endif /* CVC4__OPTIONS__OPTION_LISTENER_H */
+#endif /* CVC5__OPTIONS__OPTION_LISTENER_H */
#include "cvc4_public.h"
-#ifndef CVC4__PRINTER__MODES_H
-#define CVC4__PRINTER__MODES_H
+#ifndef CVC5__PRINTER__MODES_H
+#define CVC5__PRINTER__MODES_H
#include <iostream>
} // namespace cvc5
-#endif /* CVC4__PRINTER__MODEL_FORMAT_H */
+#endif /* CVC5__PRINTER__MODEL_FORMAT_H */
#include "cvc4_public.h"
-#ifndef CVC4__OPTIONS__SET_LANGUAGE_H
-#define CVC4__OPTIONS__SET_LANGUAGE_H
+#ifndef CVC5__OPTIONS__SET_LANGUAGE_H
+#define CVC5__OPTIONS__SET_LANGUAGE_H
#include <iostream>
} // namespace language
} // namespace cvc5
-#endif /* CVC4__OPTIONS__SET_LANGUAGE_H */
+#endif /* CVC5__OPTIONS__SET_LANGUAGE_H */
** Base for ANTLR parser classes.
**/
-#ifndef CVC4__PARSER__ANTLR_INPUT_H
-#define CVC4__PARSER__ANTLR_INPUT_H
+#ifndef CVC5__PARSER__ANTLR_INPUT_H
+#define CVC5__PARSER__ANTLR_INPUT_H
#include <antlr3.h>
} // namespace parser
} // namespace cvc5
-#endif /* CVC4__PARSER__ANTLR_INPUT_H */
+#endif /* CVC5__PARSER__ANTLR_INPUT_H */
#include "cvc4parser_private.h"
-#ifndef CVC4__PARSER__ANTLR_LINE_BUFFERED_INPUT_H
-#define CVC4__PARSER__ANTLR_LINE_BUFFERED_INPUT_H
+#ifndef CVC5__PARSER__ANTLR_LINE_BUFFERED_INPUT_H
+#define CVC5__PARSER__ANTLR_LINE_BUFFERED_INPUT_H
#include <antlr3.h>
#include <istream>
} // namespace parser
} // namespace cvc5
-#endif /* CVC4__PARSER__ANTLR_LINE_BUFFERED_INPUT_H */
+#endif /* CVC5__PARSER__ANTLR_LINE_BUFFERED_INPUT_H */
** \todo document this file
**/
-#ifndef CVC4__PARSER__ANTLR_TRACING_H
-#define CVC4__PARSER__ANTLR_TRACING_H
+#ifndef CVC5__PARSER__ANTLR_TRACING_H
+#define CVC5__PARSER__ANTLR_TRACING_H
// only enable the hack with -DCVC4_TRACE_ANTLR
#ifdef CVC4_TRACE_ANTLR
#endif /* CVC4_TRACE_ANTLR */
-#endif /* CVC4__PARSER__ANTLR_TRACING_H */
+#endif /* CVC5__PARSER__ANTLR_TRACING_H */
#include "cvc4parser_private.h"
-#ifndef CVC4__PARSER__BOUNDED_TOKEN_BUFFER_H
-#define CVC4__PARSER__BOUNDED_TOKEN_BUFFER_H
+#ifndef CVC5__PARSER__BOUNDED_TOKEN_BUFFER_H
+#define CVC5__PARSER__BOUNDED_TOKEN_BUFFER_H
#include <antlr3defs.h>
} // namespace parser
} // namespace cvc5
-#endif /* CVC4__PARSER__BOUNDED_TOKEN_BUFFER_H */
+#endif /* CVC5__PARSER__BOUNDED_TOKEN_BUFFER_H */
#include "cvc4parser_private.h"
-#ifndef CVC4__PARSER__BOUNDED_TOKEN_FACTORY_H
-#define CVC4__PARSER__BOUNDED_TOKEN_FACTORY_H
+#ifndef CVC5__PARSER__BOUNDED_TOKEN_FACTORY_H
+#define CVC5__PARSER__BOUNDED_TOKEN_FACTORY_H
namespace cvc5 {
namespace parser {
} // namespace parser
} // namespace cvc5
-#endif /* CVC4__PARSER__BOUNDED_TOKEN_FACTORY_H */
+#endif /* CVC5__PARSER__BOUNDED_TOKEN_FACTORY_H */
#include "cvc4parser_private.h"
-#ifndef CVC4__PARSER__CVC_H
-#define CVC4__PARSER__CVC_H
+#ifndef CVC5__PARSER__CVC_H
+#define CVC5__PARSER__CVC_H
#include "api/cpp/cvc5.h"
#include "parser/parser.h"
} // namespace parser
} // namespace cvc5
-#endif /* CVC4__PARSER__CVC_H */
+#endif /* CVC5__PARSER__CVC_H */
#include "cvc4parser_private.h"
-#ifndef CVC4__PARSER__CVC_INPUT_H
-#define CVC4__PARSER__CVC_INPUT_H
+#ifndef CVC5__PARSER__CVC_INPUT_H
+#define CVC5__PARSER__CVC_INPUT_H
#include "parser/antlr_input.h"
#include "parser/cvc/CvcLexer.h"
} // namespace parser
} // namespace cvc5
-#endif /* CVC4__PARSER__CVC_INPUT_H */
+#endif /* CVC5__PARSER__CVC_INPUT_H */
#include "cvc4parser_public.h"
-#ifndef CVC4__PARSER__INPUT_H
-#define CVC4__PARSER__INPUT_H
+#ifndef CVC5__PARSER__INPUT_H
+#define CVC5__PARSER__INPUT_H
#include <stdio.h>
} // namespace parser
} // namespace cvc5
-#endif /* CVC4__PARSER__ANTLR_INPUT_H */
+#endif /* CVC5__PARSER__ANTLR_INPUT_H */
#include "cvc4parser_private.h"
-#ifndef CVC4__PARSER__LINE_BUFFER_H
-#define CVC4__PARSER__LINE_BUFFER_H
+#ifndef CVC5__PARSER__LINE_BUFFER_H
+#define CVC5__PARSER__LINE_BUFFER_H
#include <cstdlib>
#include <istream>
} // namespace parser
} // namespace cvc5
-#endif /* CVC4__PARSER__LINE_BUFFER_H */
+#endif /* CVC5__PARSER__LINE_BUFFER_H */
#include "cvc4parser_private.h"
-#ifndef CVC4__PARSER__MEMORY_MAPPED_INPUT_BUFFER_H
-#define CVC4__PARSER__MEMORY_MAPPED_INPUT_BUFFER_H
+#ifndef CVC5__PARSER__MEMORY_MAPPED_INPUT_BUFFER_H
+#define CVC5__PARSER__MEMORY_MAPPED_INPUT_BUFFER_H
#include <antlr3input.h>
#include <string>
} // namespace parser
} // namespace cvc5
-#endif /* CVC4__PARSER__MEMORY_MAPPED_INPUT_BUFFER_H */
+#endif /* CVC5__PARSER__MEMORY_MAPPED_INPUT_BUFFER_H */
#include "cvc4parser_public.h"
-#ifndef CVC4__PARSER__PARSE_OP_H
-#define CVC4__PARSER__PARSE_OP_H
+#ifndef CVC5__PARSER__PARSE_OP_H
+#define CVC5__PARSER__PARSE_OP_H
#include <string>
} // namespace cvc5
-#endif /* CVC4__PARSER__PARSE_OP_H */
+#endif /* CVC5__PARSER__PARSE_OP_H */
#include "cvc4parser_public.h"
-#ifndef CVC4__PARSER__PARSER_H
-#define CVC4__PARSER__PARSER_H
+#ifndef CVC5__PARSER__PARSER_H
+#define CVC5__PARSER__PARSER_H
#include <list>
#include <set>
} // namespace parser
} // namespace cvc5
-#endif /* CVC4__PARSER__PARSER_STATE_H */
+#endif /* CVC5__PARSER__PARSER_STATE_H */
#include "cvc4parser_public.h"
-#ifndef CVC4__PARSER__PARSER_BUILDER_H
-#define CVC4__PARSER__PARSER_BUILDER_H
+#ifndef CVC5__PARSER__PARSER_BUILDER_H
+#define CVC5__PARSER__PARSER_BUILDER_H
#include <string>
} // namespace parser
} // namespace cvc5
-#endif /* CVC4__PARSER__PARSER_BUILDER_H */
+#endif /* CVC5__PARSER__PARSER_BUILDER_H */
#include "cvc4parser_public.h"
-#ifndef CVC4__PARSER__PARSER_EXCEPTION_H
-#define CVC4__PARSER__PARSER_EXCEPTION_H
+#ifndef CVC5__PARSER__PARSER_EXCEPTION_H
+#define CVC5__PARSER__PARSER_EXCEPTION_H
#include <iostream>
#include <string>
} // namespace parser
} // namespace cvc5
-#endif /* CVC4__PARSER__PARSER_EXCEPTION_H */
+#endif /* CVC5__PARSER__PARSER_EXCEPTION_H */
#include "cvc4parser_private.h"
-#ifndef CVC4__PARSER__SMT2_H
-#define CVC4__PARSER__SMT2_H
+#ifndef CVC5__PARSER__SMT2_H
+#define CVC5__PARSER__SMT2_H
#include <sstream>
#include <stack>
} // namespace parser
} // namespace cvc5
-#endif /* CVC4__PARSER__SMT2_H */
+#endif /* CVC5__PARSER__SMT2_H */
#include "cvc4parser_private.h"
-#ifndef CVC4__PARSER__SMT2_INPUT_H
-#define CVC4__PARSER__SMT2_INPUT_H
+#ifndef CVC5__PARSER__SMT2_INPUT_H
+#define CVC5__PARSER__SMT2_INPUT_H
#include "parser/antlr_input.h"
#include "parser/smt2/Smt2Lexer.h"
} // namespace parser
} // namespace cvc5
-#endif /* CVC4__PARSER__SMT2_INPUT_H */
+#endif /* CVC5__PARSER__SMT2_INPUT_H */
#include "cvc4parser_private.h"
-#ifndef CVC4__PARSER__SYGUS_INPUT_H
-#define CVC4__PARSER__SYGUS_INPUT_H
+#ifndef CVC5__PARSER__SYGUS_INPUT_H
+#define CVC5__PARSER__SYGUS_INPUT_H
#include "parser/antlr_input.h"
#include "parser/smt2/Smt2Lexer.h"
} // namespace parser
} // namespace cvc5
-#endif /* CVC4__PARSER__SYGUS_INPUT_H */
+#endif /* CVC5__PARSER__SYGUS_INPUT_H */
#include "cvc4parser_private.h"
-#ifndef CVC4__PARSER__TPTP_H
-#define CVC4__PARSER__TPTP_H
+#ifndef CVC5__PARSER__TPTP_H
+#define CVC5__PARSER__TPTP_H
#include <unordered_map>
#include <unordered_set>
} // namespace parser
} // namespace cvc5
-#endif /* CVC4__PARSER__TPTP_INPUT_H */
+#endif /* CVC5__PARSER__TPTP_INPUT_H */
#include "cvc4parser_private.h"
-#ifndef CVC4__PARSER__TPTP_INPUT_H
-#define CVC4__PARSER__TPTP_INPUT_H
+#ifndef CVC5__PARSER__TPTP_INPUT_H
+#define CVC5__PARSER__TPTP_INPUT_H
#include "parser/antlr_input.h"
#include "parser/tptp/TptpLexer.h"
} // namespace parser
} // namespace cvc5
-#endif /* CVC4__PARSER__TPTP_INPUT_H */
+#endif /* CVC5__PARSER__TPTP_INPUT_H */
#include "cvc4_private.h"
-#ifndef CVC4__PREPROCESSING__ASSERTION_PIPELINE_H
-#define CVC4__PREPROCESSING__ASSERTION_PIPELINE_H
+#ifndef CVC5__PREPROCESSING__ASSERTION_PIPELINE_H
+#define CVC5__PREPROCESSING__ASSERTION_PIPELINE_H
#include <vector>
} // namespace preprocessing
} // namespace cvc5
-#endif /* CVC4__PREPROCESSING__ASSERTION_PIPELINE_H */
+#endif /* CVC5__PREPROCESSING__ASSERTION_PIPELINE_H */
#include "cvc4_private.h"
-#ifndef CVC4__PREPROCESSING__PASSES__ACKERMANN_H
-#define CVC4__PREPROCESSING__PASSES__ACKERMANN_H
+#ifndef CVC5__PREPROCESSING__PASSES__ACKERMANN_H
+#define CVC5__PREPROCESSING__PASSES__ACKERMANN_H
#include <unordered_map>
} // namespace preprocessing
} // namespace cvc5
-#endif /* CVC4__PREPROCESSING__PASSES__ACKERMANN_H */
+#endif /* CVC5__PREPROCESSING__PASSES__ACKERMANN_H */
#include "cvc4_private.h"
-#ifndef CVC4__PREPROCESSING__PASSES__APPLY_SUBSTS_H
-#define CVC4__PREPROCESSING__PASSES__APPLY_SUBSTS_H
+#ifndef CVC5__PREPROCESSING__PASSES__APPLY_SUBSTS_H
+#define CVC5__PREPROCESSING__PASSES__APPLY_SUBSTS_H
#include "preprocessing/preprocessing_pass.h"
#include "cvc4_private.h"
-#ifndef CVC4__PREPROCESSING__PASSES__BOOL_TO_BV_H
-#define CVC4__PREPROCESSING__PASSES__BOOL_TO_BV_H
+#ifndef CVC5__PREPROCESSING__PASSES__BOOL_TO_BV_H
+#define CVC5__PREPROCESSING__PASSES__BOOL_TO_BV_H
#include "expr/node.h"
#include "options/bv_options.h"
} // namespace preprocessing
} // namespace cvc5
-#endif /* CVC4__PREPROCESSING__PASSES__BOOL_TO_BV_H */
+#endif /* CVC5__PREPROCESSING__PASSES__BOOL_TO_BV_H */
#include "cvc4_private.h"
-#ifndef CVC4__PREPROCESSING__PASSES__BV_ABSTRACTION_H
-#define CVC4__PREPROCESSING__PASSES__BV_ABSTRACTION_H
+#ifndef CVC5__PREPROCESSING__PASSES__BV_ABSTRACTION_H
+#define CVC5__PREPROCESSING__PASSES__BV_ABSTRACTION_H
#include "preprocessing/preprocessing_pass.h"
} // namespace preprocessing
} // namespace cvc5
-#endif /* CVC4__PREPROCESSING__PASSES__BV_ABSTRACTION_H */
+#endif /* CVC5__PREPROCESSING__PASSES__BV_ABSTRACTION_H */
#include "cvc4_private.h"
-#ifndef CVC4__PREPROCESSING__PASSES__BV_EAGER_ATOMS_H
-#define CVC4__PREPROCESSING__PASSES__BV_EAGER_ATOMS_H
+#ifndef CVC5__PREPROCESSING__PASSES__BV_EAGER_ATOMS_H
+#define CVC5__PREPROCESSING__PASSES__BV_EAGER_ATOMS_H
#include "preprocessing/preprocessing_pass.h"
} // namespace preprocessing
} // namespace cvc5
-#endif /* CVC4__PREPROCESSING__PASSES__BV_EAGER_ATOMS_H */
+#endif /* CVC5__PREPROCESSING__PASSES__BV_EAGER_ATOMS_H */
#include "cvc4_private.h"
-#ifndef CVC4__PREPROCESSING__PASSES__BV_GAUSS_ELIM_H
-#define CVC4__PREPROCESSING__PASSES__BV_GAUSS_ELIM_H
+#ifndef CVC5__PREPROCESSING__PASSES__BV_GAUSS_ELIM_H
+#define CVC5__PREPROCESSING__PASSES__BV_GAUSS_ELIM_H
#include "expr/node.h"
#include "preprocessing/preprocessing_pass.h"
#include "cvc4_private.h"
-#ifndef CVC4__PREPROCESSING__PASSES__BV_INTRO_POW2_H
-#define CVC4__PREPROCESSING__PASSES__BV_INTRO_POW2_H
+#ifndef CVC5__PREPROCESSING__PASSES__BV_INTRO_POW2_H
+#define CVC5__PREPROCESSING__PASSES__BV_INTRO_POW2_H
#include "preprocessing/preprocessing_pass.h"
} // namespace preprocessing
} // namespace cvc5
-#endif /* CVC4__PREPROCESSING__PASSES__BV_INTRO_POW2_H */
+#endif /* CVC5__PREPROCESSING__PASSES__BV_INTRO_POW2_H */
#include "cvc4_private.h"
-#ifndef CVC4__PREPROCESSING__PASSES__BV_TO_BOOL_H
-#define CVC4__PREPROCESSING__PASSES__BV_TO_BOOL_H
+#ifndef CVC5__PREPROCESSING__PASSES__BV_TO_BOOL_H
+#define CVC5__PREPROCESSING__PASSES__BV_TO_BOOL_H
#include "expr/node.h"
#include "preprocessing/preprocessing_pass.h"
} // namespace preprocessing
} // namespace cvc5
-#endif /* CVC4__PREPROCESSING__PASSES__BV_TO_BOOL_H */
+#endif /* CVC5__PREPROCESSING__PASSES__BV_TO_BOOL_H */
#include "cvc4_private.h"
-#ifndef __CVC4__PREPROCESSING__PASSES__BV_TO_INT_H
-#define __CVC4__PREPROCESSING__PASSES__BV_TO_INT_H
+#ifndef __CVC5__PREPROCESSING__PASSES__BV_TO_INT_H
+#define __CVC5__PREPROCESSING__PASSES__BV_TO_INT_H
#include "context/cdhashmap.h"
#include "context/cdhashset.h"
} // namespace preprocessing
} // namespace cvc5
-#endif /* __CVC4__PREPROCESSING__PASSES__BV_TO_INT_H */
+#endif /* __CVC5__PREPROCESSING__PASSES__BV_TO_INT_H */
#include "cvc4_private.h"
-#ifndef CVC4__PREPROCESSING__PASSES__EXTENDED_REWRITER_PASS_H
-#define CVC4__PREPROCESSING__PASSES__EXTENDED_REWRITER_PASS_H
+#ifndef CVC5__PREPROCESSING__PASSES__EXTENDED_REWRITER_PASS_H
+#define CVC5__PREPROCESSING__PASSES__EXTENDED_REWRITER_PASS_H
#include "preprocessing/preprocessing_pass.h"
} // namespace preprocessing
} // namespace cvc5
-#endif /* CVC4__PREPROCESSING__PASSES__EXTENDED_REWRITER_PASS_H */
+#endif /* CVC5__PREPROCESSING__PASSES__EXTENDED_REWRITER_PASS_H */
#include "cvc4_private.h"
-#ifndef CVC4__PREPROCESSING__PASSES__FOREIGN_THEORY_REWRITE_H
-#define CVC4__PREPROCESSING__PASSES__FOREIGN_THEORY_REWRITE_H
+#ifndef CVC5__PREPROCESSING__PASSES__FOREIGN_THEORY_REWRITE_H
+#define CVC5__PREPROCESSING__PASSES__FOREIGN_THEORY_REWRITE_H
#include "context/cdhashmap.h"
#include "expr/node.h"
} // namespace preprocessing
} // namespace cvc5
-#endif /* CVC4__PREPROCESSING__PASSES__FOREIGN_THEORY_REWRITE_H */
+#endif /* CVC5__PREPROCESSING__PASSES__FOREIGN_THEORY_REWRITE_H */
** \brief Function definition processor for finite model finding
**/
-#ifndef CVC4__PREPROCESSING__PASSES__FUN_DEF_FMF_H
-#define CVC4__PREPROCESSING__PASSES__FUN_DEF_FMF_H
+#ifndef CVC5__PREPROCESSING__PASSES__FUN_DEF_FMF_H
+#define CVC5__PREPROCESSING__PASSES__FUN_DEF_FMF_H
#include <map>
#include <vector>
} // namespace preprocessing
} // namespace cvc5
-#endif /* CVC4__PREPROCESSING__PASSES__SYGUS_INFERENCE_H_ */
+#endif /* CVC5__PREPROCESSING__PASSES__SYGUS_INFERENCE_H_ */
#include "cvc4_private.h"
-#ifndef CVC4__PREPROCESSING__PASSES__GLOBAL_NEGATE_H
-#define CVC4__PREPROCESSING__PASSES__GLOBAL_NEGATE_H
+#ifndef CVC5__PREPROCESSING__PASSES__GLOBAL_NEGATE_H
+#define CVC5__PREPROCESSING__PASSES__GLOBAL_NEGATE_H
#include "expr/node.h"
#include "preprocessing/preprocessing_pass.h"
} // namespace preprocessing
} // namespace cvc5
-#endif /* CVC4__PREPROCESSING_PASSES__GLOBAL_NEGATE_H */
+#endif /* CVC5__PREPROCESSING_PASSES__GLOBAL_NEGATE_H */
#include "cvc4_private.h"
-#ifndef __CVC4__PREPROCESSING__PASSES__HO_ELIM_PASS_H
-#define __CVC4__PREPROCESSING__PASSES__HO_ELIM_PASS_H
+#ifndef __CVC5__PREPROCESSING__PASSES__HO_ELIM_PASS_H
+#define __CVC5__PREPROCESSING__PASSES__HO_ELIM_PASS_H
#include <map>
#include <unordered_map>
} // namespace preprocessing
} // namespace cvc5
-#endif /* __CVC4__PREPROCESSING__PASSES__HO_ELIM_PASS_H */
+#endif /* __CVC5__PREPROCESSING__PASSES__HO_ELIM_PASS_H */
#include "cvc4_private.h"
-#ifndef CVC4__PREPROCESSING__PASSES__INT_TO_BV_H
-#define CVC4__PREPROCESSING__PASSES__INT_TO_BV_H
+#ifndef CVC5__PREPROCESSING__PASSES__INT_TO_BV_H
+#define CVC5__PREPROCESSING__PASSES__INT_TO_BV_H
#include "preprocessing/preprocessing_pass.h"
} // namespace preprocessing
} // namespace cvc5
-#endif /* CVC4__PREPROCESSING__PASSES__INT_TO_BV_H */
+#endif /* CVC5__PREPROCESSING__PASSES__INT_TO_BV_H */
#include "cvc4_private.h"
-#ifndef CVC4__PREPROCESSING__PASSES__ITE_REMOVAL_H
-#define CVC4__PREPROCESSING__PASSES__ITE_REMOVAL_H
+#ifndef CVC5__PREPROCESSING__PASSES__ITE_REMOVAL_H
+#define CVC5__PREPROCESSING__PASSES__ITE_REMOVAL_H
#include "preprocessing/preprocessing_pass.h"
} // namespace preprocessing
} // namespace cvc5
-#endif // CVC4__PREPROCESSING__PASSES__ITE_REMOVAL_H
+#endif // CVC5__PREPROCESSING__PASSES__ITE_REMOVAL_H
#include "cvc4_private.h"
-#ifndef CVC4__PREPROCESSING__PASSES__ITE_SIMP_H
-#define CVC4__PREPROCESSING__PASSES__ITE_SIMP_H
+#ifndef CVC5__PREPROCESSING__PASSES__ITE_SIMP_H
+#define CVC5__PREPROCESSING__PASSES__ITE_SIMP_H
#include "preprocessing/preprocessing_pass.h"
#include "preprocessing/util/ite_utilities.h"
#include "cvc4_private.h"
-#ifndef CVC4__PREPROCESSING__PASSES__MIPLIB_TRICK_H
-#define CVC4__PREPROCESSING__PASSES__MIPLIB_TRICK_H
+#ifndef CVC5__PREPROCESSING__PASSES__MIPLIB_TRICK_H
+#define CVC5__PREPROCESSING__PASSES__MIPLIB_TRICK_H
#include "expr/node.h"
#include "preprocessing/preprocessing_pass.h"
} // namespace preprocessing
} // namespace cvc5
-#endif /* CVC4__PREPROCESSING__PASSES__MIPLIB_TRICK_H */
+#endif /* CVC5__PREPROCESSING__PASSES__MIPLIB_TRICK_H */
#include "cvc4_private.h"
-#ifndef CVC4__PREPROCESSING__PASSES__NL_EXT_PURIFY_H
-#define CVC4__PREPROCESSING__PASSES__NL_EXT_PURIFY_H
+#ifndef CVC5__PREPROCESSING__PASSES__NL_EXT_PURIFY_H
+#define CVC5__PREPROCESSING__PASSES__NL_EXT_PURIFY_H
#include <unordered_map>
#include <vector>
} // namespace preprocessing
} // namespace cvc5
-#endif /* CVC4__PREPROCESSING__PASSES__NL_EXT_PURIFY_H */
+#endif /* CVC5__PREPROCESSING__PASSES__NL_EXT_PURIFY_H */
#include "cvc4_private.h"
-#ifndef CVC4__PREPROCESSING__PASSES__NON_CLAUSAL_SIMP_H
-#define CVC4__PREPROCESSING__PASSES__NON_CLAUSAL_SIMP_H
+#ifndef CVC5__PREPROCESSING__PASSES__NON_CLAUSAL_SIMP_H
+#define CVC5__PREPROCESSING__PASSES__NON_CLAUSAL_SIMP_H
#include "context/cdlist.h"
#include "expr/node.h"
#include "cvc4_private.h"
-#ifndef CVC4__PREPROCESSING__PASSES__PSEUDO_BOOLEAN_PROCESSOR_H
-#define CVC4__PREPROCESSING__PASSES__PSEUDO_BOOLEAN_PROCESSOR_H
+#ifndef CVC5__PREPROCESSING__PASSES__PSEUDO_BOOLEAN_PROCESSOR_H
+#define CVC5__PREPROCESSING__PASSES__PSEUDO_BOOLEAN_PROCESSOR_H
#include <unordered_set>
#include <vector>
} // namespace preprocessing
} // namespace cvc5
-#endif // CVC4__PREPROCESSING__PASSES__PSEUDO_BOOLEAN_PROCESSOR_H
+#endif // CVC5__PREPROCESSING__PASSES__PSEUDO_BOOLEAN_PROCESSOR_H
#include "cvc4_private.h"
-#ifndef CVC4__PREPROCESSING__PASSES__QUANTIFIER_MACROS_H
-#define CVC4__PREPROCESSING__PASSES__QUANTIFIER_MACROS_H
+#ifndef CVC5__PREPROCESSING__PASSES__QUANTIFIER_MACROS_H
+#define CVC5__PREPROCESSING__PASSES__QUANTIFIER_MACROS_H
#include <map>
#include <vector>
} // preprocessing
} // namespace cvc5
-#endif /*CVC4__PREPROCESSING__PASSES__QUANTIFIER_MACROS_H */
+#endif /*CVC5__PREPROCESSING__PASSES__QUANTIFIER_MACROS_H */
#include "cvc4_private.h"
-#ifndef CVC4__PREPROCESSING__PASSES__QUANTIFIERS_PREPROCESS_H
-#define CVC4__PREPROCESSING__PASSES__QUANTIFIERS_PREPROCESS_H
+#ifndef CVC5__PREPROCESSING__PASSES__QUANTIFIERS_PREPROCESS_H
+#define CVC5__PREPROCESSING__PASSES__QUANTIFIERS_PREPROCESS_H
#include "preprocessing/preprocessing_pass.h"
} // namespace preprocessing
} // namespace cvc5
-#endif /* CVC4__PREPROCESSING__PASSES__QUANTIFIERS_PREPROCESS_H */
+#endif /* CVC5__PREPROCESSING__PASSES__QUANTIFIERS_PREPROCESS_H */
#include "cvc4_private.h"
-#ifndef CVC4__PREPROCESSING__PASSES__REAL_TO_INT_H
-#define CVC4__PREPROCESSING__PASSES__REAL_TO_INT_H
+#ifndef CVC5__PREPROCESSING__PASSES__REAL_TO_INT_H
+#define CVC5__PREPROCESSING__PASSES__REAL_TO_INT_H
#include <vector>
} // namespace preprocessing
} // namespace cvc5
-#endif /* CVC4__PREPROCESSING__PASSES__REAL_TO_INT_H */
+#endif /* CVC5__PREPROCESSING__PASSES__REAL_TO_INT_H */
#include "cvc4_private.h"
-#ifndef CVC4__PREPROCESSING__PASSES__REWRITE_H
-#define CVC4__PREPROCESSING__PASSES__REWRITE_H
+#ifndef CVC5__PREPROCESSING__PASSES__REWRITE_H
+#define CVC5__PREPROCESSING__PASSES__REWRITE_H
#include "preprocessing/preprocessing_pass.h"
} // namespace preprocessing
} // namespace cvc5
-#endif /* CVC4__PREPROCESSING__PASSES__REWRITE_H */
-
+#endif /* CVC5__PREPROCESSING__PASSES__REWRITE_H */
#include "cvc4_private.h"
-#ifndef CVC4__PREPROCESSING__PASSES__SEP_SKOLEM_EMP_H
-#define CVC4__PREPROCESSING__PASSES__SEP_SKOLEM_EMP_H
+#ifndef CVC5__PREPROCESSING__PASSES__SEP_SKOLEM_EMP_H
+#define CVC5__PREPROCESSING__PASSES__SEP_SKOLEM_EMP_H
#include "preprocessing/preprocessing_pass.h"
} // namespace preprocessing
} // namespace cvc5
-#endif /* CVC4__PREPROCESSING__PASSES__SEP_SKOLEM_EMP_H */
+#endif /* CVC5__PREPROCESSING__PASSES__SEP_SKOLEM_EMP_H */
** \brief Sort inference preprocessing pass
**/
-#ifndef CVC4__PREPROCESSING__PASSES__SORT_INFERENCE_PASS_H_
-#define CVC4__PREPROCESSING__PASSES__SORT_INFERENCE_PASS_H_
+#ifndef CVC5__PREPROCESSING__PASSES__SORT_INFERENCE_PASS_H_
+#define CVC5__PREPROCESSING__PASSES__SORT_INFERENCE_PASS_H_
#include "preprocessing/preprocessing_pass.h"
} // namespace preprocessing
} // namespace cvc5
-#endif /* CVC4__PREPROCESSING__PASSES__SORT_INFERENCE_PASS_H_ */
+#endif /* CVC5__PREPROCESSING__PASSES__SORT_INFERENCE_PASS_H_ */
#include "cvc4_private.h"
-#ifndef CVC4__PREPROCESSING__PASSES__STATIC_LEARNING_H
-#define CVC4__PREPROCESSING__PASSES__STATIC_LEARNING_H
+#ifndef CVC5__PREPROCESSING__PASSES__STATIC_LEARNING_H
+#define CVC5__PREPROCESSING__PASSES__STATIC_LEARNING_H
#include "preprocessing/preprocessing_pass.h"
} // namespace preprocessing
} // namespace cvc5
-#endif /* CVC4__PREPROCESSING__PASSES__STATIC_LEARNING_H */
+#endif /* CVC5__PREPROCESSING__PASSES__STATIC_LEARNING_H */
#include "cvc4_private.h"
-#ifndef CVC4__PREPROCESSING__PASSES__STRINGS_EAGER_PP_H
-#define CVC4__PREPROCESSING__PASSES__STRINGS_EAGER_PP_H
+#ifndef CVC5__PREPROCESSING__PASSES__STRINGS_EAGER_PP_H
+#define CVC5__PREPROCESSING__PASSES__STRINGS_EAGER_PP_H
#include "preprocessing/preprocessing_pass.h"
} // namespace preprocessing
} // namespace cvc5
-#endif /* CVC4__PREPROCESSING__PASSES__STRINGS_EAGER_PP_H */
+#endif /* CVC5__PREPROCESSING__PASSES__STRINGS_EAGER_PP_H */
** \brief SygusInference
**/
-#ifndef CVC4__PREPROCESSING__PASSES__SYGUS_INFERENCE_H_
-#define CVC4__PREPROCESSING__PASSES__SYGUS_INFERENCE_H_
+#ifndef CVC5__PREPROCESSING__PASSES__SYGUS_INFERENCE_H_
+#define CVC5__PREPROCESSING__PASSES__SYGUS_INFERENCE_H_
#include <vector>
#include "expr/node.h"
} // namespace preprocessing
} // namespace cvc5
-#endif /* CVC4__PREPROCESSING__PASSES__SYGUS_INFERENCE_H_ */
+#endif /* CVC5__PREPROCESSING__PASSES__SYGUS_INFERENCE_H_ */
** where t1 and t2 are subterms of the input.
**/
-#ifndef CVC4__PREPROCESSING__PASSES__SYNTH_REW_RULES_H
-#define CVC4__PREPROCESSING__PASSES__SYNTH_REW_RULES_H
+#ifndef CVC5__PREPROCESSING__PASSES__SYNTH_REW_RULES_H
+#define CVC5__PREPROCESSING__PASSES__SYNTH_REW_RULES_H
#include "preprocessing/preprocessing_pass.h"
} // namespace preprocessing
} // namespace cvc5
-#endif /* CVC4__PREPROCESSING__PASSES__SYNTH_REW_RULES_H */
+#endif /* CVC5__PREPROCESSING__PASSES__SYNTH_REW_RULES_H */
#include "cvc4_private.h"
-#ifndef CVC4__PREPROCESSING__PASSES__THEORY_PREPROCESS_H
-#define CVC4__PREPROCESSING__PASSES__THEORY_PREPROCESS_H
+#ifndef CVC5__PREPROCESSING__PASSES__THEORY_PREPROCESS_H
+#define CVC5__PREPROCESSING__PASSES__THEORY_PREPROCESS_H
#include "preprocessing/preprocessing_pass.h"
} // namespace preprocessing
} // namespace cvc5
-#endif /* CVC4__PREPROCESSING__PASSES__THEORY_PREPROCESS_H */
+#endif /* CVC5__PREPROCESSING__PASSES__THEORY_PREPROCESS_H */
#include "cvc4_private.h"
-#ifndef CVC4__PREPROCESSING__PASSES__THEORY_REWRITE_EQ_H
-#define CVC4__PREPROCESSING__PASSES__THEORY_REWRITE_EQ_H
+#ifndef CVC5__PREPROCESSING__PASSES__THEORY_REWRITE_EQ_H
+#define CVC5__PREPROCESSING__PASSES__THEORY_REWRITE_EQ_H
#include "expr/node.h"
#include "preprocessing/preprocessing_pass.h"
} // namespace preprocessing
} // namespace cvc5
-#endif /* CVC4__PREPROCESSING__PASSES__THEORY_REWRITE_EQ_H */
+#endif /* CVC5__PREPROCESSING__PASSES__THEORY_REWRITE_EQ_H */
#include "cvc4_private.h"
-#ifndef CVC4__PREPROCESSING_PASSES_UNCONSTRAINED_SIMPLIFIER_H
-#define CVC4__PREPROCESSING_PASSES_UNCONSTRAINED_SIMPLIFIER_H
+#ifndef CVC5__PREPROCESSING_PASSES_UNCONSTRAINED_SIMPLIFIER_H
+#define CVC5__PREPROCESSING_PASSES_UNCONSTRAINED_SIMPLIFIER_H
#include <unordered_map>
#include <unordered_set>
#include "cvc4_private.h"
-#ifndef CVC4__PREPROCESSING__PREPROCESSING_PASS_H
-#define CVC4__PREPROCESSING__PREPROCESSING_PASS_H
+#ifndef CVC5__PREPROCESSING__PREPROCESSING_PASS_H
+#define CVC5__PREPROCESSING__PREPROCESSING_PASS_H
#include <string>
} // namespace preprocessing
} // namespace cvc5
-#endif /* CVC4__PREPROCESSING__PREPROCESSING_PASS_H */
+#endif /* CVC5__PREPROCESSING__PREPROCESSING_PASS_H */
#include "cvc4_private.h"
-#ifndef CVC4__PREPROCESSING__PREPROCESSING_PASS_CONTEXT_H
-#define CVC4__PREPROCESSING__PREPROCESSING_PASS_CONTEXT_H
+#ifndef CVC5__PREPROCESSING__PREPROCESSING_PASS_CONTEXT_H
+#define CVC5__PREPROCESSING__PREPROCESSING_PASS_CONTEXT_H
#include "context/cdhashset.h"
#include "smt/smt_engine.h"
} // namespace preprocessing
} // namespace cvc5
-#endif /* CVC4__PREPROCESSING__PREPROCESSING_PASS_CONTEXT_H */
+#endif /* CVC5__PREPROCESSING__PREPROCESSING_PASS_CONTEXT_H */
**/
#include "cvc4_private.h"
-#ifndef CVC4__PREPROCESSING__PREPROCESSING_PASS_REGISTRY_H
-#define CVC4__PREPROCESSING__PREPROCESSING_PASS_REGISTRY_H
+#ifndef CVC5__PREPROCESSING__PREPROCESSING_PASS_REGISTRY_H
+#define CVC5__PREPROCESSING__PREPROCESSING_PASS_REGISTRY_H
#include <functional>
#include <string>
} // namespace preprocessing
} // namespace cvc5
-#endif /* CVC4__PREPROCESSING__PREPROCESSING_PASS_REGISTRY_H */
+#endif /* CVC5__PREPROCESSING__PREPROCESSING_PASS_REGISTRY_H */
#include "cvc4_private.h"
-#ifndef CVC4__ITE_UTILITIES_H
-#define CVC4__ITE_UTILITIES_H
+#ifndef CVC5__ITE_UTILITIES_H
+#define CVC5__ITE_UTILITIES_H
#include <unordered_map>
#include <vector>
#include "cvc4_private.h"
-#ifndef CVC4__PRINTER__AST_PRINTER_H
-#define CVC4__PRINTER__AST_PRINTER_H
+#ifndef CVC5__PRINTER__AST_PRINTER_H
+#define CVC5__PRINTER__AST_PRINTER_H
#include <iostream>
} // namespace printer
} // namespace cvc5
-#endif /* CVC4__PRINTER__AST_PRINTER_H */
+#endif /* CVC5__PRINTER__AST_PRINTER_H */
#include "cvc4_private.h"
-#ifndef CVC4__PRINTER__CVC_PRINTER_H
-#define CVC4__PRINTER__CVC_PRINTER_H
+#ifndef CVC5__PRINTER__CVC_PRINTER_H
+#define CVC5__PRINTER__CVC_PRINTER_H
#include <iostream>
} // namespace printer
} // namespace cvc5
-#endif /* CVC4__PRINTER__CVC_PRINTER_H */
+#endif /* CVC5__PRINTER__CVC_PRINTER_H */
#include "cvc4_private.h"
-#ifndef CVC4__PRINTER__LET_BINDING_H
-#define CVC4__PRINTER__LET_BINDING_H
+#ifndef CVC5__PRINTER__LET_BINDING_H
+#define CVC5__PRINTER__LET_BINDING_H
#include <vector>
#include "cvc4_private.h"
-#ifndef CVC4__PRINTER__PRINTER_H
-#define CVC4__PRINTER__PRINTER_H
+#ifndef CVC5__PRINTER__PRINTER_H
+#define CVC5__PRINTER__PRINTER_H
#include <string>
} // namespace cvc5
-#endif /* CVC4__PRINTER__PRINTER_H */
+#endif /* CVC5__PRINTER__PRINTER_H */
#include "cvc4_private.h"
-#ifndef CVC4__PRINTER__SMT2_PRINTER_H
-#define CVC4__PRINTER__SMT2_PRINTER_H
+#ifndef CVC5__PRINTER__SMT2_PRINTER_H
+#define CVC5__PRINTER__SMT2_PRINTER_H
#include "printer/printer.h"
} // namespace printer
} // namespace cvc5
-#endif /* CVC4__PRINTER__SMT2_PRINTER_H */
+#endif /* CVC5__PRINTER__SMT2_PRINTER_H */
#include "cvc4_private.h"
-#ifndef CVC4__PRINTER__TPTP_PRINTER_H
-#define CVC4__PRINTER__TPTP_PRINTER_H
+#ifndef CVC5__PRINTER__TPTP_PRINTER_H
+#define CVC5__PRINTER__TPTP_PRINTER_H
#include <iostream>
} // namespace printer
} // namespace cvc5
-#endif /* CVC4__PRINTER__TPTP_PRINTER_H */
+#endif /* CVC5__PRINTER__TPTP_PRINTER_H */
#include "cvc4_private.h"
-#ifndef CVC4__PROOF__CLAUSE_ID_H
-#define CVC4__PROOF__CLAUSE_ID_H
+#ifndef CVC5__PROOF__CLAUSE_ID_H
+#define CVC5__PROOF__CLAUSE_ID_H
namespace cvc5 {
} // namespace cvc5
-#endif /* CVC4__PROOF__CLAUSE_ID_H */
+#endif /* CVC5__PROOF__CLAUSE_ID_H */
#include "cvc4_private.h"
-#ifndef CVC4__CNF_PROOF_H
-#define CVC4__CNF_PROOF_H
+#ifndef CVC5__CNF_PROOF_H
+#define CVC5__CNF_PROOF_H
#include <unordered_map>
#include <unordered_set>
} // namespace cvc5
-#endif /* CVC4__CNF_PROOF_H */
+#endif /* CVC5__CNF_PROOF_H */
#include "cvc4_private.h"
-#ifndef CVC4__PROOF__DOT__DOT_PRINTER_H
-#define CVC4__PROOF__DOT__DOT_PRINTER_H
+#ifndef CVC5__PROOF__DOT__DOT_PRINTER_H
+#define CVC5__PROOF__DOT__DOT_PRINTER_H
#include <iostream>
#include "cvc4_private.h"
-#ifndef CVC4__PROOF_MANAGER_H
-#define CVC4__PROOF_MANAGER_H
+#ifndef CVC5__PROOF_MANAGER_H
+#define CVC5__PROOF_MANAGER_H
#include <memory>
#include <unordered_map>
} // namespace cvc5
-#endif /* CVC4__PROOF_MANAGER_H */
+#endif /* CVC5__PROOF_MANAGER_H */
#include "cvc4_private.h"
-#ifndef CVC4__SAT__PROOF_H
-#define CVC4__SAT__PROOF_H
+#ifndef CVC5__SAT__PROOF_H
+#define CVC5__SAT__PROOF_H
#include <iosfwd>
#include <set>
} // namespace cvc5
-#endif /* CVC4__SAT__PROOF_H */
+#endif /* CVC5__SAT__PROOF_H */
#include "cvc4_private.h"
-#ifndef CVC4__SAT__PROOF_IMPLEMENTATION_H
-#define CVC4__SAT__PROOF_IMPLEMENTATION_H
+#ifndef CVC5__SAT__PROOF_IMPLEMENTATION_H
+#define CVC5__SAT__PROOF_IMPLEMENTATION_H
#include "proof/clause_id.h"
#include "proof/sat_proof.h"
} // namespace cvc5
-#endif /* CVC4__SAT__PROOF_IMPLEMENTATION_H */
+#endif /* CVC5__SAT__PROOF_IMPLEMENTATION_H */
#include "cvc4_private.h"
-#ifndef CVC4__UNSAT_CORE_H
-#define CVC4__UNSAT_CORE_H
+#ifndef CVC5__UNSAT_CORE_H
+#define CVC5__UNSAT_CORE_H
#include <iosfwd>
#include <vector>
} // namespace cvc5
-#endif /* CVC4__UNSAT_CORE_H */
+#endif /* CVC5__UNSAT_CORE_H */
#include "cvc4_private.h"
-#ifndef CVC4__PROP__BVSATSOLVERNOTIFY_H
-#define CVC4__PROP__BVSATSOLVERNOTIFY_H
+#ifndef CVC5__PROP__BVSATSOLVERNOTIFY_H
+#define CVC5__PROP__BVSATSOLVERNOTIFY_H
#include "prop/sat_solver_types.h"
#include "util/resource_manager.h"
#include "cvc4_private.h"
-#ifndef CVC4__PROP__CADICAL_H
-#define CVC4__PROP__CADICAL_H
+#ifndef CVC5__PROP__CADICAL_H
+#define CVC5__PROP__CADICAL_H
#ifdef CVC4_USE_CADICAL
} // namespace cvc5
#endif // CVC4_USE_CADICAL
-#endif // CVC4__PROP__CADICAL_H
+#endif // CVC5__PROP__CADICAL_H
#include "cvc4_private.h"
-#ifndef CVC4__PROP__CNF_STREAM_H
-#define CVC4__PROP__CNF_STREAM_H
+#ifndef CVC5__PROP__CNF_STREAM_H
+#define CVC5__PROP__CNF_STREAM_H
#include "context/cdhashset.h"
#include "context/cdinsert_hashmap.h"
} // namespace prop
} // namespace cvc5
-#endif /* CVC4__PROP__CNF_STREAM_H */
+#endif /* CVC5__PROP__CNF_STREAM_H */
#include "cvc4_private.h"
-#ifndef CVC4__PROP__CRYPTOMINISAT_H
-#define CVC4__PROP__CRYPTOMINISAT_H
+#ifndef CVC5__PROP__CRYPTOMINISAT_H
+#define CVC5__PROP__CRYPTOMINISAT_H
#ifdef CVC4_USE_CRYPTOMINISAT
} // namespace cvc5
#endif // CVC4_USE_CRYPTOMINISAT
-#endif // CVC4__PROP__CRYPTOMINISAT_H
+#endif // CVC5__PROP__CRYPTOMINISAT_H
#include "cvc4_private.h"
-#ifndef CVC4__PROP__KISSAT_H
-#define CVC4__PROP__KISSAT_H
+#ifndef CVC5__PROP__KISSAT_H
+#define CVC5__PROP__KISSAT_H
#ifdef CVC4_USE_KISSAT
} // namespace cvc5
#endif // CVC4_USE_KISSAT
-#endif // CVC4__PROP__KISSAT_H
+#endif // CVC5__PROP__KISSAT_H
#include "cvc4_private.h"
-#ifndef CVC4__PROP__PROOF_CNF_STREAM_H
-#define CVC4__PROP__PROOF_CNF_STREAM_H
+#ifndef CVC5__PROP__PROOF_CNF_STREAM_H
+#define CVC5__PROP__PROOF_CNF_STREAM_H
#include "context/cdhashmap.h"
#include "expr/lazy_proof.h"
#include "cvc4_private.h"
-#ifndef CVC4__PROP__PROOF_POST_PROCESSOR_H
-#define CVC4__PROP__PROOF_POST_PROCESSOR_H
+#ifndef CVC5__PROP__PROOF_POST_PROCESSOR_H
+#define CVC5__PROP__PROOF_POST_PROCESSOR_H
#include <map>
#include <unordered_set>
#include "cvc4_private.h"
-#ifndef CVC4__PROP_ENGINE_H
-#define CVC4__PROP_ENGINE_H
+#ifndef CVC5__PROP_ENGINE_H
+#define CVC5__PROP_ENGINE_H
#include "context/cdlist.h"
#include "expr/node.h"
} // namespace prop
} // namespace cvc5
-#endif /* CVC4__PROP_ENGINE_H */
+#endif /* CVC5__PROP_ENGINE_H */
#include "cvc4_private.h"
-#ifndef CVC4__PROP_PROOF_MANAGER_H
-#define CVC4__PROP_PROOF_MANAGER_H
+#ifndef CVC5__PROP_PROOF_MANAGER_H
+#define CVC5__PROP_PROOF_MANAGER_H
#include "context/cdlist.h"
#include "expr/proof.h"
} // namespace prop
} // namespace cvc5
-#endif /* CVC4__PROP__PROOF_MANAGER_H */
+#endif /* CVC5__PROP__PROOF_MANAGER_H */
#include "cvc4_private.h"
-#ifndef CVC4__PROP__REGISTRAR_H
-#define CVC4__PROP__REGISTRAR_H
+#ifndef CVC5__PROP__REGISTRAR_H
+#define CVC5__PROP__REGISTRAR_H
namespace cvc5 {
namespace prop {
} // namespace prop
} // namespace cvc5
-#endif /* CVC4__PROP__REGISTRAR_H */
+#endif /* CVC5__PROP__REGISTRAR_H */
#include "cvc4_private.h"
-#ifndef CVC4__SAT_PROOF_MANAGER_H
-#define CVC4__SAT_PROOF_MANAGER_H
+#ifndef CVC5__SAT_PROOF_MANAGER_H
+#define CVC5__SAT_PROOF_MANAGER_H
#include "context/cdhashset.h"
#include "expr/buffered_proof_generator.h"
} // namespace prop
} // namespace cvc5
-#endif /* CVC4__SAT_PROOF_MANAGER_H */
+#endif /* CVC5__SAT_PROOF_MANAGER_H */
#include "cvc4_private.h"
-#ifndef CVC4__PROP__SAT_SOLVER_H
-#define CVC4__PROP__SAT_SOLVER_H
+#ifndef CVC5__PROP__SAT_SOLVER_H
+#define CVC5__PROP__SAT_SOLVER_H
#include <string>
} // namespace prop
} // namespace cvc5
-#endif /* CVC4__PROP__SAT_MODULE_H */
+#endif /* CVC5__PROP__SAT_MODULE_H */
#include "cvc4_private.h"
-#ifndef CVC4__PROP__SAT_SOLVER_FACTORY_H
-#define CVC4__PROP__SAT_SOLVER_FACTORY_H
+#ifndef CVC5__PROP__SAT_SOLVER_FACTORY_H
+#define CVC5__PROP__SAT_SOLVER_FACTORY_H
#include <string>
#include <vector>
} // namespace prop
} // namespace cvc5
-#endif // CVC4__PROP__SAT_SOLVER_FACTORY_H
+#endif // CVC5__PROP__SAT_SOLVER_FACTORY_H
#include "cvc4_private.h"
-#ifndef CVC4__PROP__SKOLEM_DEF_MANAGER_H
-#define CVC4__PROP__SKOLEM_DEF_MANAGER_H
+#ifndef CVC5__PROP__SKOLEM_DEF_MANAGER_H
+#define CVC5__PROP__SKOLEM_DEF_MANAGER_H
#include <iosfwd>
#include <unordered_set>
} // namespace prop
} // namespace cvc5
-#endif /* CVC4__PROP__SKOLEM_DEF_MANAGER_H */
+#endif /* CVC5__PROP__SKOLEM_DEF_MANAGER_H */
#include "cvc4_private.h"
-#ifndef CVC4__PROP__SAT_H
-#define CVC4__PROP__SAT_H
+#ifndef CVC5__PROP__SAT_H
+#define CVC5__PROP__SAT_H
// Just defining this for now, since there's no other SAT solver bindings.
// Optional blocks below will be unconditionally included
} // namespace cvc5
-#endif /* CVC4__PROP__SAT_H */
+#endif /* CVC5__PROP__SAT_H */
#include "cvc4_private.h"
-#ifndef CVC4__SMT__ABDUCTION_SOLVER_H
-#define CVC4__SMT__ABDUCTION_SOLVER_H
+#ifndef CVC5__SMT__ABDUCTION_SOLVER_H
+#define CVC5__SMT__ABDUCTION_SOLVER_H
#include "expr/node.h"
#include "expr/type_node.h"
} // namespace smt
} // namespace cvc5
-#endif /* CVC4__SMT__ABDUCTION_SOLVER_H */
+#endif /* CVC5__SMT__ABDUCTION_SOLVER_H */
#include "cvc4_private.h"
-#ifndef CVC4__SMT__ABSTRACT_VALUES_H
-#define CVC4__SMT__ABSTRACT_VALUES_H
+#ifndef CVC5__SMT__ABSTRACT_VALUES_H
+#define CVC5__SMT__ABSTRACT_VALUES_H
#include <unordered_map>
#include "cvc4_private.h"
-#ifndef CVC4__SMT__ASSERTIONS_H
-#define CVC4__SMT__ASSERTIONS_H
+#ifndef CVC5__SMT__ASSERTIONS_H
+#define CVC5__SMT__ASSERTIONS_H
#include <vector>
#include "cvc4_private.h"
-#ifndef CVC4__SMT__CHECK_MODELS_H
-#define CVC4__SMT__CHECK_MODELS_H
+#ifndef CVC5__SMT__CHECK_MODELS_H
+#define CVC5__SMT__CHECK_MODELS_H
#include "context/cdlist.h"
#include "expr/node.h"
#include "cvc4_public.h"
-#ifndef CVC4__COMMAND_H
-#define CVC4__COMMAND_H
+#ifndef CVC5__COMMAND_H
+#define CVC5__COMMAND_H
#include <iosfwd>
#include <sstream>
} // namespace cvc5
-#endif /* CVC4__COMMAND_H */
+#endif /* CVC5__COMMAND_H */
#include "cvc4_private.h"
-#ifndef CVC4__SMT__DEFINED_FUNCTION_H
-#define CVC4__SMT__DEFINED_FUNCTION_H
+#ifndef CVC5__SMT__DEFINED_FUNCTION_H
+#define CVC5__SMT__DEFINED_FUNCTION_H
#include <vector>
} // namespace smt
} // namespace cvc5
-#endif /* CVC4__SMT__DEFINED_FUNCTION_H */
+#endif /* CVC5__SMT__DEFINED_FUNCTION_H */
#include "cvc4_private.h"
-#ifndef CVC4__DUMP_H
-#define CVC4__DUMP_H
+#ifndef CVC5__DUMP_H
+#define CVC5__DUMP_H
#include "base/output.h"
} // namespace cvc5
-#endif /* CVC4__DUMP_H */
+#endif /* CVC5__DUMP_H */
#include "cvc4_private.h"
-#ifndef CVC4__SMT__DUMP_MANAGER_H
-#define CVC4__SMT__DUMP_MANAGER_H
+#ifndef CVC5__SMT__DUMP_MANAGER_H
+#define CVC5__SMT__DUMP_MANAGER_H
#include <memory>
#include <vector>
#include "cvc4_public.h"
-#ifndef CVC4__SMT__ENV_H
-#define CVC4__SMT__ENV_H
+#ifndef CVC5__SMT__ENV_H
+#define CVC5__SMT__ENV_H
#include <memory>
} // namespace cvc5
-#endif /* CVC4__SMT__ENV_H */
+#endif /* CVC5__SMT__ENV_H */
#include "cvc4_private.h"
-#ifndef CVC4__SMT__EXPAND_DEFINITIONS_H
-#define CVC4__SMT__EXPAND_DEFINITIONS_H
+#ifndef CVC5__SMT__EXPAND_DEFINITIONS_H
+#define CVC5__SMT__EXPAND_DEFINITIONS_H
#include <unordered_map>
#include "cvc4_private.h"
-#ifndef CVC4__SMT__INTERPOLATION_SOLVER_H
-#define CVC4__SMT__INTERPOLATION_SOLVER_H
+#ifndef CVC5__SMT__INTERPOLATION_SOLVER_H
+#define CVC5__SMT__INTERPOLATION_SOLVER_H
#include "expr/node.h"
#include "expr/type_node.h"
} // namespace smt
} // namespace cvc5
-#endif /* CVC4__SMT__INTERPOLATION_SOLVER_H */
+#endif /* CVC5__SMT__INTERPOLATION_SOLVER_H */
#include "cvc4_private.h"
-#ifndef CVC4__SMT__LISTENERS_H
-#define CVC4__SMT__LISTENERS_H
+#ifndef CVC5__SMT__LISTENERS_H
+#define CVC5__SMT__LISTENERS_H
#include <vector>
#include "cvc4_public.h"
-#ifndef CVC4__SMT__LOGIC_EXCEPTION_H
-#define CVC4__SMT__LOGIC_EXCEPTION_H
+#ifndef CVC5__SMT__LOGIC_EXCEPTION_H
+#define CVC5__SMT__LOGIC_EXCEPTION_H
#include "base/exception.h"
} // namespace cvc5
-#endif /* CVC4__SMT__LOGIC_EXCEPTION_H */
+#endif /* CVC5__SMT__LOGIC_EXCEPTION_H */
#include "cvc4_private.h"
-#ifndef CVC4__MANAGED_OSTREAMS_H
-#define CVC4__MANAGED_OSTREAMS_H
+#ifndef CVC5__MANAGED_OSTREAMS_H
+#define CVC5__MANAGED_OSTREAMS_H
#include <ostream>
} // namespace cvc5
-#endif /* CVC4__MANAGED_OSTREAMS_H */
+#endif /* CVC5__MANAGED_OSTREAMS_H */
#include "cvc4_private.h"
-#ifndef CVC4__MODEL_H
-#define CVC4__MODEL_H
+#ifndef CVC5__MODEL_H
+#define CVC5__MODEL_H
#include <iosfwd>
#include <vector>
} // namespace smt
} // namespace cvc5
-#endif /* CVC4__MODEL_H */
+#endif /* CVC5__MODEL_H */
#include "cvc4_private.h"
-#ifndef __CVC4__THEORY__MODEL_BLOCKER_H
-#define __CVC4__THEORY__MODEL_BLOCKER_H
+#ifndef __CVC5__THEORY__MODEL_BLOCKER_H
+#define __CVC5__THEORY__MODEL_BLOCKER_H
#include <vector>
} // namespace cvc5
-#endif /* __CVC4__THEORY__MODEL_BLOCKER_H */
+#endif /* __CVC5__THEORY__MODEL_BLOCKER_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__MODEL_CORE_BUILDER_H
-#define CVC4__THEORY__MODEL_CORE_BUILDER_H
+#ifndef CVC5__THEORY__MODEL_CORE_BUILDER_H
+#define CVC5__THEORY__MODEL_CORE_BUILDER_H
#include <vector>
} // namespace cvc5
-#endif /* CVC4__THEORY__MODEL_CORE_BUILDER_H */
+#endif /* CVC5__THEORY__MODEL_CORE_BUILDER_H */
#include "cvc4_private.h"
-#ifndef CVC4__SMT__NODE_COMMAND_H
-#define CVC4__SMT__NODE_COMMAND_H
+#ifndef CVC5__SMT__NODE_COMMAND_H
+#define CVC5__SMT__NODE_COMMAND_H
#include <string>
} // namespace cvc5
-#endif /* CVC4__SMT__NODE_COMMAND_H */
+#endif /* CVC5__SMT__NODE_COMMAND_H */
#include "cvc4_private.h"
-#ifndef CVC4__SMT__OPTIMIZATION_SOLVER_H
-#define CVC4__SMT__OPTIMIZATION_SOLVER_H
+#ifndef CVC5__SMT__OPTIMIZATION_SOLVER_H
+#define CVC5__SMT__OPTIMIZATION_SOLVER_H
#include "expr/node.h"
#include "expr/type_node.h"
} // namespace smt
} // namespace cvc5
-#endif /* CVC4__SMT__OPTIMIZATION_SOLVER_H */
+#endif /* CVC5__SMT__OPTIMIZATION_SOLVER_H */
** \brief Module for managing options of an SmtEngine.
**/
-#ifndef CVC4__SMT__OPTIONS_MANAGER_H
-#define CVC4__SMT__OPTIONS_MANAGER_H
+#ifndef CVC5__SMT__OPTIONS_MANAGER_H
+#define CVC5__SMT__OPTIONS_MANAGER_H
#include "options/options_listener.h"
#include "smt/managed_ostreams.h"
} // namespace smt
} // namespace cvc5
-#endif /* CVC4__SMT__OPTIONS_MANAGER_H */
+#endif /* CVC5__SMT__OPTIONS_MANAGER_H */
** internally.
**/
-#ifndef CVC4__SMT__OUTPUT_MANAGER_H
-#define CVC4__SMT__OUTPUT_MANAGER_H
+#ifndef CVC5__SMT__OUTPUT_MANAGER_H
+#define CVC5__SMT__OUTPUT_MANAGER_H
#include <ostream>
} // namespace cvc5
-#endif // CVC4__SMT__OUTPUT_MANAGER_H
+#endif // CVC5__SMT__OUTPUT_MANAGER_H
#include "cvc4_private.h"
-#ifndef CVC4__SMT__PREPROCESS_PROOF_GENERATOR_H
-#define CVC4__SMT__PREPROCESS_PROOF_GENERATOR_H
+#ifndef CVC5__SMT__PREPROCESS_PROOF_GENERATOR_H
+#define CVC5__SMT__PREPROCESS_PROOF_GENERATOR_H
#include "context/cdhashmap.h"
#include "expr/lazy_proof.h"
#include "cvc4_private.h"
-#ifndef CVC4__SMT__PREPROCESSOR_H
-#define CVC4__SMT__PREPROCESSOR_H
+#ifndef CVC5__SMT__PREPROCESSOR_H
+#define CVC5__SMT__PREPROCESSOR_H
#include <memory>
#include "cvc4_private.h"
-#ifndef CVC4__SMT__PROCESS_ASSERTIONS_H
-#define CVC4__SMT__PROCESS_ASSERTIONS_H
+#ifndef CVC5__SMT__PROCESS_ASSERTIONS_H
+#define CVC5__SMT__PROCESS_ASSERTIONS_H
#include <unordered_map>
#include "cvc4_private.h"
-#ifndef CVC4__SMT__PROOF_MANAGER_H
-#define CVC4__SMT__PROOF_MANAGER_H
+#ifndef CVC5__SMT__PROOF_MANAGER_H
+#define CVC5__SMT__PROOF_MANAGER_H
#include "context/cdhashmap.h"
#include "expr/node.h"
} // namespace smt
} // namespace cvc5
-#endif /* CVC4__SMT__PROOF_MANAGER_H */
+#endif /* CVC5__SMT__PROOF_MANAGER_H */
#include "cvc4_private.h"
-#ifndef CVC4__SMT__PROOF_POST_PROCESSOR_H
-#define CVC4__SMT__PROOF_POST_PROCESSOR_H
+#ifndef CVC5__SMT__PROOF_POST_PROCESSOR_H
+#define CVC5__SMT__PROOF_POST_PROCESSOR_H
#include <map>
#include <unordered_set>
#include "cvc4_private.h"
-#ifndef CVC4__SMT__QUANT_ELIM_SOLVER_H
-#define CVC4__SMT__QUANT_ELIM_SOLVER_H
+#ifndef CVC5__SMT__QUANT_ELIM_SOLVER_H
+#define CVC5__SMT__QUANT_ELIM_SOLVER_H
#include "expr/node.h"
#include "smt/assertions.h"
} // namespace smt
} // namespace cvc5
-#endif /* CVC4__SMT__QUANT_ELIM_SOLVER_H */
+#endif /* CVC5__SMT__QUANT_ELIM_SOLVER_H */
** \brief Method for setting the default options of an SMT engine.
**/
-#ifndef CVC4__SMT__SET_DEFAULTS_H
-#define CVC4__SMT__SET_DEFAULTS_H
+#ifndef CVC5__SMT__SET_DEFAULTS_H
+#define CVC5__SMT__SET_DEFAULTS_H
#include "theory/logic_info.h"
} // namespace smt
} // namespace cvc5
-#endif /* CVC4__SMT__SET_DEFAULTS_H */
+#endif /* CVC5__SMT__SET_DEFAULTS_H */
#include "cvc4_public.h"
-#ifndef CVC4__SMT_ENGINE_H
-#define CVC4__SMT_ENGINE_H
+#ifndef CVC5__SMT_ENGINE_H
+#define CVC5__SMT_ENGINE_H
#include <map>
#include <memory>
} // namespace cvc5
-#endif /* CVC4__SMT_ENGINE_H */
+#endif /* CVC5__SMT_ENGINE_H */
#include "cvc4_private.h"
-#ifndef CVC4__SMT__SMT_ENGINE_SCOPE_H
-#define CVC4__SMT__SMT_ENGINE_SCOPE_H
+#ifndef CVC5__SMT__SMT_ENGINE_SCOPE_H
+#define CVC5__SMT__SMT_ENGINE_SCOPE_H
#include "expr/node_manager.h"
} // namespace smt
} // namespace cvc5
-#endif /* CVC4__SMT__SMT_ENGINE_SCOPE_H */
+#endif /* CVC5__SMT__SMT_ENGINE_SCOPE_H */
#include "cvc4_private.h"
-#ifndef CVC4__SMT__SMT_ENGINE_STATE_H
-#define CVC4__SMT__SMT_ENGINE_STATE_H
+#ifndef CVC5__SMT__SMT_ENGINE_STATE_H
+#define CVC5__SMT__SMT_ENGINE_STATE_H
#include <string>
#include "cvc4_private.h"
-#ifndef CVC4__SMT__SMT_ENGINE_STATS_H
-#define CVC4__SMT__SMT_ENGINE_STATS_H
+#ifndef CVC5__SMT__SMT_ENGINE_STATS_H
+#define CVC5__SMT__SMT_ENGINE_STATS_H
#include "util/statistics_registry.h"
#include "util/stats_timer.h"
} // namespace smt
} // namespace cvc5
-#endif /* CVC4__SMT__SMT_ENGINE_STATS_H */
+#endif /* CVC5__SMT__SMT_ENGINE_STATS_H */
#include "cvc4_public.h"
-#ifndef CVC4__SMT__SMT_MODE_H
-#define CVC4__SMT__SMT_MODE_H
+#ifndef CVC5__SMT__SMT_MODE_H
+#define CVC5__SMT__SMT_MODE_H
#include <iosfwd>
#include "cvc4_private.h"
-#ifndef CVC4__SMT__SMT_SOLVER_H
-#define CVC4__SMT__SMT_SOLVER_H
+#ifndef CVC5__SMT__SMT_SOLVER_H
+#define CVC5__SMT__SMT_SOLVER_H
#include <vector>
} // namespace smt
} // namespace cvc5
-#endif /* CVC4__SMT__SMT_SOLVER_H */
+#endif /* CVC5__SMT__SMT_SOLVER_H */
#include "cvc4_private.h"
-#ifndef CVC4__SMT__SYGUS_SOLVER_H
-#define CVC4__SMT__SYGUS_SOLVER_H
+#ifndef CVC5__SMT__SYGUS_SOLVER_H
+#define CVC5__SMT__SYGUS_SOLVER_H
#include "context/cdo.h"
#include "expr/node.h"
} // namespace smt
} // namespace cvc5
-#endif /* CVC4__SMT__SYGUS_SOLVER_H */
+#endif /* CVC5__SMT__SYGUS_SOLVER_H */
#include "cvc4_private.h"
-#ifndef CVC4__SMT__UNSAT_CORE_MANAGER_H
-#define CVC4__SMT__UNSAT_CORE_MANAGER_H
+#ifndef CVC5__SMT__UNSAT_CORE_MANAGER_H
+#define CVC5__SMT__UNSAT_CORE_MANAGER_H
#include "context/cdlist.h"
#include "expr/node.h"
} // namespace smt
} // namespace cvc5
-#endif /* CVC4__SMT__UNSAT_CORE_MANAGER_H */
+#endif /* CVC5__SMT__UNSAT_CORE_MANAGER_H */
#include "cvc4_private.h"
-#ifndef CVC4__UPDATE_OSTREAM_H
-#define CVC4__UPDATE_OSTREAM_H
+#ifndef CVC5__UPDATE_OSTREAM_H
+#define CVC5__UPDATE_OSTREAM_H
#include <ostream>
} // namespace cvc5
-#endif /* CVC4__UPDATE_OSTREAM_H */
+#endif /* CVC5__UPDATE_OSTREAM_H */
#include "cvc4_private.h"
-#ifndef CVC4__SMT__WITNESS_FORM_H
-#define CVC4__SMT__WITNESS_FORM_H
+#ifndef CVC5__SMT__WITNESS_FORM_H
+#define CVC5__SMT__WITNESS_FORM_H
#include <unordered_set>
#include "cvc4_private.h"
-#ifndef CVC4__BOOLEAN_SIMPLIFICATION_H
-#define CVC4__BOOLEAN_SIMPLIFICATION_H
+#ifndef CVC5__BOOLEAN_SIMPLIFICATION_H
+#define CVC5__BOOLEAN_SIMPLIFICATION_H
#include <vector>
#include <algorithm>
} // namespace cvc5
-#endif /* CVC4__BOOLEAN_SIMPLIFICATION_H */
+#endif /* CVC5__BOOLEAN_SIMPLIFICATION_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__ARITH__ARITH_ITE_UTILS_H
-#define CVC4__THEORY__ARITH__ARITH_ITE_UTILS_H
+#ifndef CVC5__THEORY__ARITH__ARITH_ITE_UTILS_H
+#define CVC5__THEORY__ARITH__ARITH_ITE_UTILS_H
#include <unordered_map>
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__ARITH__ARITH_ITE_UTILS_H */
+#endif /* CVC5__THEORY__ARITH__ARITH_ITE_UTILS_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__ARITH__MSUM_H
-#define CVC4__THEORY__ARITH__MSUM_H
+#ifndef CVC5__THEORY__ARITH__MSUM_H
+#define CVC5__THEORY__ARITH__MSUM_H
#include <map>
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__ARITH__MSUM_H */
+#endif /* CVC5__THEORY__ARITH__MSUM_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__ARITH__ARITH_PREPROCESS_H
-#define CVC4__THEORY__ARITH__ARITH_PREPROCESS_H
+#ifndef CVC5__THEORY__ARITH__ARITH_PREPROCESS_H
+#define CVC5__THEORY__ARITH__ARITH_PREPROCESS_H
#include "context/cdhashmap.h"
#include "theory/arith/operator_elim.h"
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__ARITH__ARITH_REWRITER_H
-#define CVC4__THEORY__ARITH__ARITH_REWRITER_H
+#ifndef CVC5__THEORY__ARITH__ARITH_REWRITER_H
+#define CVC5__THEORY__ARITH__ARITH_REWRITER_H
#include "theory/arith/rewrites.h"
#include "theory/theory_rewriter.h"
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__ARITH__ARITH_REWRITER_H */
+#endif /* CVC5__THEORY__ARITH__ARITH_REWRITER_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__ARITH__ARITH_STATE_H
-#define CVC4__THEORY__ARITH__ARITH_STATE_H
+#ifndef CVC5__THEORY__ARITH__ARITH_STATE_H
+#define CVC5__THEORY__ARITH__ARITH_STATE_H
#include "theory/theory_state.h"
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__ARITH__ARITH_STATIC_LEARNER_H
-#define CVC4__THEORY__ARITH__ARITH_STATIC_LEARNER_H
+#ifndef CVC5__THEORY__ARITH__ARITH_STATIC_LEARNER_H
+#define CVC5__THEORY__ARITH__ARITH_STATIC_LEARNER_H
#include "context/cdhashmap.h"
#include "theory/arith/arith_utilities.h"
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__ARITH__ARITH_STATIC_LEARNER_H */
+#endif /* CVC5__THEORY__ARITH__ARITH_STATIC_LEARNER_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__ARITH__ARITH_UTILITIES_H
-#define CVC4__THEORY__ARITH__ARITH_UTILITIES_H
+#ifndef CVC5__THEORY__ARITH__ARITH_UTILITIES_H
+#define CVC5__THEORY__ARITH__ARITH_UTILITIES_H
#include <unordered_map>
#include <unordered_set>
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__ARITH__ARITH_UTILITIES_H */
+#endif /* CVC5__THEORY__ARITH__ARITH_UTILITIES_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__ARITH__ARITHVAR_NODE_MAP_H
-#define CVC4__THEORY__ARITH__ARITHVAR_NODE_MAP_H
-
+#ifndef CVC5__THEORY__ARITH__ARITHVAR_NODE_MAP_H
+#define CVC5__THEORY__ARITH__ARITHVAR_NODE_MAP_H
#include "theory/arith/arithvar.h"
#include "context/context.h"
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__ARITH__ARITHVAR_NODE_MAP_H */
+#endif /* CVC5__THEORY__ARITH__ARITHVAR_NODE_MAP_H */
** \brief Extract bounds on variables from theory atoms.
**/
-#ifndef CVC4__THEORY__ARITH__BOUND_INFERENCE_H
-#define CVC4__THEORY__ARITH__BOUND_INFERENCE_H
+#ifndef CVC5__THEORY__ARITH__BOUND_INFERENCE_H
+#define CVC5__THEORY__ARITH__BOUND_INFERENCE_H
#include <map>
#include <utility>
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__ARITH__CONSTRAINT_H
-#define CVC4__THEORY__ARITH__CONSTRAINT_H
+#ifndef CVC5__THEORY__ARITH__CONSTRAINT_H
+#define CVC5__THEORY__ARITH__CONSTRAINT_H
#include <unordered_map>
#include <vector>
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__ARITH__CONSTRAINT_H */
+#endif /* CVC5__THEORY__ARITH__CONSTRAINT_H */
** between header files.
**/
-#ifndef CVC4__THEORY__ARITH__CONSTRAINT_FORWARD_H
-#define CVC4__THEORY__ARITH__CONSTRAINT_FORWARD_H
+#ifndef CVC5__THEORY__ARITH__CONSTRAINT_FORWARD_H
+#define CVC5__THEORY__ARITH__CONSTRAINT_FORWARD_H
#include "cvc4_private.h"
#include <vector>
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__ARITH__CONSTRAINT_FORWARD_H */
+#endif /* CVC5__THEORY__ARITH__CONSTRAINT_FORWARD_H */
#include "cvc4_private.h"
-
-#ifndef CVC4__THEORY__ARITH__DIO_SOLVER_H
-#define CVC4__THEORY__ARITH__DIO_SOLVER_H
+#ifndef CVC5__THEORY__ARITH__DIO_SOLVER_H
+#define CVC5__THEORY__ARITH__DIO_SOLVER_H
#include <unordered_map>
#include <utility>
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__ARITH__DIO_SOLVER_H */
+#endif /* CVC5__THEORY__ARITH__DIO_SOLVER_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__ARITH__INFERENCE_MANAGER_H
-#define CVC4__THEORY__ARITH__INFERENCE_MANAGER_H
+#ifndef CVC5__THEORY__ARITH__INFERENCE_MANAGER_H
+#define CVC5__THEORY__ARITH__INFERENCE_MANAGER_H
#include <vector>
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__ARITH__NL__CAD__CDCAC_H
-#define CVC4__THEORY__ARITH__NL__CAD__CDCAC_H
+#ifndef CVC5__THEORY__ARITH__NL__CAD__CDCAC_H
+#define CVC5__THEORY__ARITH__NL__CAD__CDCAC_H
#ifdef CVC4_POLY_IMP
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__ARITH__NL__CAD__CDCAC_UTILS_H
-#define CVC4__THEORY__ARITH__NL__CAD__CDCAC_UTILS_H
+#ifndef CVC5__THEORY__ARITH__NL__CAD__CDCAC_UTILS_H
+#define CVC5__THEORY__ARITH__NL__CAD__CDCAC_UTILS_H
#ifdef CVC4_POLY_IMP
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__ARITH__NL__CAD__CONSTRAINTS_H
-#define CVC4__THEORY__ARITH__NL__CAD__CONSTRAINTS_H
+#ifndef CVC5__THEORY__ARITH__NL__CAD__CONSTRAINTS_H
+#define CVC5__THEORY__ARITH__NL__CAD__CONSTRAINTS_H
#ifdef CVC4_POLY_IMP
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__ARITH__NL__CAD_PROJECTIONS_H
-#define CVC4__THEORY__ARITH__NL__CAD_PROJECTIONS_H
+#ifndef CVC5__THEORY__ARITH__NL__CAD_PROJECTIONS_H
+#define CVC5__THEORY__ARITH__NL__CAD_PROJECTIONS_H
#ifdef CVC4_USE_POLY
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__ARITH__NL__CAD__PROOF_CHECKER_H
-#define CVC4__THEORY__ARITH__NL__CAD__PROOF_CHECKER_H
+#ifndef CVC5__THEORY__ARITH__NL__CAD__PROOF_CHECKER_H
+#define CVC5__THEORY__ARITH__NL__CAD__PROOF_CHECKER_H
#include "expr/node.h"
#include "expr/proof_checker.h"
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__STRINGS__PROOF_CHECKER_H */
+#endif /* CVC5__THEORY__STRINGS__PROOF_CHECKER_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__ARITH__NL__CAD__PROOF_GENERATOR_H
-#define CVC4__THEORY__ARITH__NL__CAD__PROOF_GENERATOR_H
+#ifndef CVC5__THEORY__ARITH__NL__CAD__PROOF_GENERATOR_H
+#define CVC5__THEORY__ARITH__NL__CAD__PROOF_GENERATOR_H
#ifdef CVC4_POLY_IMP
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__ARITH__NL__CAD__VARIABLE_ORDERING_H
-#define CVC4__THEORY__ARITH__NL__CAD__VARIABLE_ORDERING_H
+#ifndef CVC5__THEORY__ARITH__NL__CAD__VARIABLE_ORDERING_H
+#define CVC5__THEORY__ARITH__NL__CAD__VARIABLE_ORDERING_H
#ifdef CVC4_POLY_IMP
** \brief CAD-based solver based on https://arxiv.org/pdf/2003.05633.pdf.
**/
-#ifndef CVC4__THEORY__ARITH__CAD_SOLVER_H
-#define CVC4__THEORY__ARITH__CAD_SOLVER_H
+#ifndef CVC5__THEORY__ARITH__CAD_SOLVER_H
+#define CVC5__THEORY__ARITH__CAD_SOLVER_H
#include <vector>
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__ARITH__CAD_SOLVER_H */
+#endif /* CVC5__THEORY__ARITH__CAD_SOLVER_H */
** \brief Utilities for non-linear constraints
**/
-#ifndef CVC4__THEORY__ARITH__NL__EXT__CONSTRAINT_H
-#define CVC4__THEORY__ARITH__NL__EXT__CONSTRAINT_H
+#ifndef CVC5__THEORY__ARITH__NL__EXT__CONSTRAINT_H
+#define CVC5__THEORY__ARITH__NL__EXT__CONSTRAINT_H
#include <map>
#include <vector>
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__ARITH__NL_SOLVER_H */
+#endif /* CVC5__THEORY__ARITH__NL_SOLVER_H */
** \brief Common data shared by multiple checks
**/
-#ifndef CVC4__THEORY__ARITH__NL__EXT__SHARED_CHECK_DATA_H
-#define CVC4__THEORY__ARITH__NL__EXT__SHARED_CHECK_DATA_H
+#ifndef CVC5__THEORY__ARITH__NL__EXT__SHARED_CHECK_DATA_H
+#define CVC5__THEORY__ARITH__NL__EXT__SHARED_CHECK_DATA_H
#include <vector>
** \brief Check for factoring lemma
**/
-#ifndef CVC4__THEORY__ARITH__NL__EXT__FACTORING_CHECK_H
-#define CVC4__THEORY__ARITH__NL__EXT__FACTORING_CHECK_H
+#ifndef CVC5__THEORY__ARITH__NL__EXT__FACTORING_CHECK_H
+#define CVC5__THEORY__ARITH__NL__EXT__FACTORING_CHECK_H
#include <vector>
** \brief Utilities for monomials
**/
-#ifndef CVC4__THEORY__ARITH__NL__EXT__MONOMIAL_H
-#define CVC4__THEORY__ARITH__NL__EXT__MONOMIAL_H
+#ifndef CVC5__THEORY__ARITH__NL__EXT__MONOMIAL_H
+#define CVC5__THEORY__ARITH__NL__EXT__MONOMIAL_H
#include <map>
#include <vector>
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__ARITH__NL_MONOMIAL_H */
+#endif /* CVC5__THEORY__ARITH__NL_MONOMIAL_H */
** \brief Check for monomial bound inference lemmas
**/
-#ifndef CVC4__THEORY__ARITH__NL__EXT__MONOMIAL_BOUNDS_CHECK_H
-#define CVC4__THEORY__ARITH__NL__EXT__MONOMIAL_BOUNDS_CHECK_H
+#ifndef CVC5__THEORY__ARITH__NL__EXT__MONOMIAL_BOUNDS_CHECK_H
+#define CVC5__THEORY__ARITH__NL__EXT__MONOMIAL_BOUNDS_CHECK_H
#include "expr/node.h"
#include "theory/arith/nl/ext/constraint.h"
** \brief Check for some monomial lemmas
**/
-#ifndef CVC4__THEORY__ARITH__NL__EXT__MONOMIAL_CHECK_H
-#define CVC4__THEORY__ARITH__NL__EXT__MONOMIAL_CHECK_H
+#ifndef CVC5__THEORY__ARITH__NL__EXT__MONOMIAL_CHECK_H
+#define CVC5__THEORY__ARITH__NL__EXT__MONOMIAL_CHECK_H
#include "expr/node.h"
#include "theory/arith/nl/ext/monomial.h"
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__ARITH__NL__EXT__PROOF_CHECKER_H
-#define CVC4__THEORY__ARITH__NL__EXT__PROOF_CHECKER_H
+#ifndef CVC5__THEORY__ARITH__NL__EXT__PROOF_CHECKER_H
+#define CVC5__THEORY__ARITH__NL__EXT__PROOF_CHECKER_H
#include "expr/node.h"
#include "expr/proof_checker.h"
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__STRINGS__PROOF_CHECKER_H */
+#endif /* CVC5__THEORY__STRINGS__PROOF_CHECKER_H */
** \brief Check for split zero lemma
**/
-#ifndef CVC4__THEORY__ARITH__NL__EXT__SPLIT_ZERO_CHECK_H
-#define CVC4__THEORY__ARITH__NL__EXT__SPLIT_ZERO_CHECK_H
+#ifndef CVC5__THEORY__ARITH__NL__EXT__SPLIT_ZERO_CHECK_H
+#define CVC5__THEORY__ARITH__NL__EXT__SPLIT_ZERO_CHECK_H
#include "expr/node.h"
#include "context/cdhashset.h"
** \brief Check for tangent_plane lemma
**/
-#ifndef CVC4__THEORY__ARITH__NL__EXT__TANGENT_PLANE_CHECK_H
-#define CVC4__THEORY__ARITH__NL__EXT__TANGENT_PLANE_CHECK_H
+#ifndef CVC5__THEORY__ARITH__NL__EXT__TANGENT_PLANE_CHECK_H
+#define CVC5__THEORY__ARITH__NL__EXT__TANGENT_PLANE_CHECK_H
#include <map>
** \brief The extended theory callback for non-linear arithmetic
**/
-#ifndef CVC4__THEORY__ARITH__NL__EXT_THEORY_CALLBACK_H
-#define CVC4__THEORY__ARITH__NL__EXT_THEORY_CALLBACK_H
+#ifndef CVC5__THEORY__ARITH__NL__EXT_THEORY_CALLBACK_H
+#define CVC5__THEORY__ARITH__NL__EXT_THEORY_CALLBACK_H
#include "expr/node.h"
#include "theory/ext_theory.h"
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__ARITH__NL__EXT_THEORY_CALLBACK_H */
+#endif /* CVC5__THEORY__ARITH__NL__EXT_THEORY_CALLBACK_H */
** \brief Solver for integer and (IAND) constraints
**/
-#ifndef CVC4__THEORY__ARITH__NL__IAND_SOLVER_H
-#define CVC4__THEORY__ARITH__NL__IAND_SOLVER_H
+#ifndef CVC5__THEORY__ARITH__NL__IAND_SOLVER_H
+#define CVC5__THEORY__ARITH__NL__IAND_SOLVER_H
#include <map>
#include <vector>
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__ARITH__IAND_SOLVER_H */
+#endif /* CVC5__THEORY__ARITH__IAND_SOLVER_H */
** the value of iand.
**/
-#ifndef CVC4__THEORY__ARITH__IAND_TABLE_H
-#define CVC4__THEORY__ARITH__IAND_TABLE_H
+#ifndef CVC5__THEORY__ARITH__IAND_TABLE_H
+#define CVC5__THEORY__ARITH__IAND_TABLE_H
#include <map>
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__ARITH__IAND_TABLE_H */
+#endif /* CVC5__THEORY__ARITH__IAND_TABLE_H */
** \brief Represents a contraction candidate for ICP-style propagation.
**/
-#ifndef CVC4__THEORY__ARITH__ICP__CANDIDATE_H
-#define CVC4__THEORY__ARITH__ICP__CANDIDATE_H
+#ifndef CVC5__THEORY__ARITH__ICP__CANDIDATE_H
+#define CVC5__THEORY__ARITH__ICP__CANDIDATE_H
#include "cvc4_private.h"
** \brief Implements a way to track the origins of ICP-style contractions.
**/
-#ifndef CVC4__THEORY__ARITH__ICP__CONTRACTION_ORIGINS_H
-#define CVC4__THEORY__ARITH__ICP__CONTRACTION_ORIGINS_H
+#ifndef CVC5__THEORY__ARITH__ICP__CONTRACTION_ORIGINS_H
+#define CVC5__THEORY__ARITH__ICP__CONTRACTION_ORIGINS_H
#include <memory>
#include <vector>
** \brief Implements a ICP-based solver for nonlinear arithmetic.
**/
-#ifndef CVC4__THEORY__ARITH__ICP__ICP_SOLVER_H
-#define CVC4__THEORY__ARITH__ICP__ICP_SOLVER_H
+#ifndef CVC5__THEORY__ARITH__ICP__ICP_SOLVER_H
+#define CVC5__THEORY__ARITH__ICP__ICP_SOLVER_H
#include "cvc4_private.h"
** \brief Implement intersection of intervals for propagation.
**/
-#ifndef CVC4__THEORY__ARITH__ICP__INTERSECTION_H
-#define CVC4__THEORY__ARITH__ICP__INTERSECTION_H
+#ifndef CVC5__THEORY__ARITH__ICP__INTERSECTION_H
+#define CVC5__THEORY__ARITH__ICP__INTERSECTION_H
#include "cvc4_private.h"
** \brief
**/
-#ifndef CVC4__THEORY__ARITH__ICP__INTERVAL_H
-#define CVC4__THEORY__ARITH__ICP__INTERVAL_H
+#ifndef CVC5__THEORY__ARITH__ICP__INTERVAL_H
+#define CVC5__THEORY__ARITH__ICP__INTERVAL_H
#include "cvc4_private.h"
** \brief Utilities for processing lemmas from the non-linear solver
**/
-#ifndef CVC4__THEORY__ARITH__NL__NL_LEMMA_UTILS_H
-#define CVC4__THEORY__ARITH__NL__NL_LEMMA_UTILS_H
+#ifndef CVC5__THEORY__ARITH__NL__NL_LEMMA_UTILS_H
+#define CVC5__THEORY__ARITH__NL__NL_LEMMA_UTILS_H
#include <tuple>
#include <vector>
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__ARITH__NL_LEMMA_UTILS_H */
+#endif /* CVC5__THEORY__ARITH__NL_LEMMA_UTILS_H */
** \brief Model object for the non-linear extension class
**/
-#ifndef CVC4__THEORY__ARITH__NL__NL_MODEL_H
-#define CVC4__THEORY__ARITH__NL__NL_MODEL_H
+#ifndef CVC5__THEORY__ARITH__NL__NL_MODEL_H
+#define CVC5__THEORY__ARITH__NL__NL_MODEL_H
#include <map>
#include <unordered_map>
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__ARITH__NONLINEAR_EXTENSION_H */
+#endif /* CVC5__THEORY__ARITH__NONLINEAR_EXTENSION_H */
** multiplication via axiom instantiations.
**/
-#ifndef CVC4__THEORY__ARITH__NL__NONLINEAR_EXTENSION_H
-#define CVC4__THEORY__ARITH__NL__NONLINEAR_EXTENSION_H
+#ifndef CVC5__THEORY__ARITH__NL__NONLINEAR_EXTENSION_H
+#define CVC5__THEORY__ARITH__NL__NONLINEAR_EXTENSION_H
#include <map>
#include <vector>
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__ARITH__NONLINEAR_EXTENSION_H */
+#endif /* CVC5__THEORY__ARITH__NONLINEAR_EXTENSION_H */
** Utilities for converting to and from LibPoly objects.
**/
-#ifndef CVC4__THEORY__ARITH__NL__POLY_CONVERSION_H
-#define CVC4__THEORY__ARITH__NL__POLY_CONVERSION_H
+#ifndef CVC5__THEORY__ARITH__NL__POLY_CONVERSION_H
+#define CVC5__THEORY__ARITH__NL__POLY_CONVERSION_H
#include "cvc4_private.h"
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__ARITH__NL__STATS_H
-#define CVC4__THEORY__ARITH__NL__STATS_H
+#ifndef CVC5__THEORY__ARITH__NL__STATS_H
+#define CVC5__THEORY__ARITH__NL__STATS_H
#include "util/statistics_registry.h"
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__ARITH__NL__STATS_H */
+#endif /* CVC5__THEORY__ARITH__NL__STATS_H */
** \brief Strategies for the nonlinear extension
**/
-#ifndef CVC4__THEORY__ARITH__NL__STRATEGY_H
-#define CVC4__THEORY__ARITH__NL__STRATEGY_H
+#ifndef CVC5__THEORY__ARITH__NL__STRATEGY_H
+#define CVC5__THEORY__ARITH__NL__STRATEGY_H
#include <iosfwd>
#include <vector>
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__ARITH__NL__STRATEGY_H */
+#endif /* CVC5__THEORY__ARITH__NL__STRATEGY_H */
** \brief Solving for handling exponential function.
**/
-#ifndef CVC4__THEORY__ARITH__NL__TRANSCENDENTAL__EXPONENTIAL_SOLVER_H
-#define CVC4__THEORY__ARITH__NL__TRANSCENDENTAL__EXPONENTIAL_SOLVER_H
+#ifndef CVC5__THEORY__ARITH__NL__TRANSCENDENTAL__EXPONENTIAL_SOLVER_H
+#define CVC5__THEORY__ARITH__NL__TRANSCENDENTAL__EXPONENTIAL_SOLVER_H
#include <map>
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__ARITH__TRANSCENDENTAL_SOLVER_H */
+#endif /* CVC5__THEORY__ARITH__TRANSCENDENTAL_SOLVER_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__ARITH__NL__TRANSCENDENTAL__PROOF_CHECKER_H
-#define CVC4__THEORY__ARITH__NL__TRANSCENDENTAL__PROOF_CHECKER_H
+#ifndef CVC5__THEORY__ARITH__NL__TRANSCENDENTAL__PROOF_CHECKER_H
+#define CVC5__THEORY__ARITH__NL__TRANSCENDENTAL__PROOF_CHECKER_H
#include "expr/node.h"
#include "expr/proof_checker.h"
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__STRINGS__PROOF_CHECKER_H */
+#endif /* CVC5__THEORY__STRINGS__PROOF_CHECKER_H */
** \brief Solving for handling exponential function.
**/
-#ifndef CVC4__THEORY__ARITH__NL__TRANSCENDENTAL__SINE_SOLVER_H
-#define CVC4__THEORY__ARITH__NL__TRANSCENDENTAL__SINE_SOLVER_H
+#ifndef CVC5__THEORY__ARITH__NL__TRANSCENDENTAL__SINE_SOLVER_H
+#define CVC5__THEORY__ARITH__NL__TRANSCENDENTAL__SINE_SOLVER_H
#include <map>
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__ARITH__TRANSCENDENTAL_SOLVER_H */
+#endif /* CVC5__THEORY__ARITH__TRANSCENDENTAL_SOLVER_H */
** \brief Generate taylor approximations transcendental lemmas.
**/
-#ifndef CVC4__THEORY__ARITH__NL__TRANSCENDENTAL__TAYLOR_GENERATOR_H
-#define CVC4__THEORY__ARITH__NL__TRANSCENDENTAL__TAYLOR_GENERATOR_H
+#ifndef CVC5__THEORY__ARITH__NL__TRANSCENDENTAL__TAYLOR_GENERATOR_H
+#define CVC5__THEORY__ARITH__NL__TRANSCENDENTAL__TAYLOR_GENERATOR_H
#include "expr/node.h"
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__ARITH__TRANSCENDENTAL_SOLVER_H */
+#endif /* CVC5__THEORY__ARITH__TRANSCENDENTAL_SOLVER_H */
** \brief Solving for handling transcendental functions.
**/
-#ifndef CVC4__THEORY__ARITH__NL__TRANSCENDENTAL__TRANSCENDENTAL_SOLVER_H
-#define CVC4__THEORY__ARITH__NL__TRANSCENDENTAL__TRANSCENDENTAL_SOLVER_H
+#ifndef CVC5__THEORY__ARITH__NL__TRANSCENDENTAL__TRANSCENDENTAL_SOLVER_H
+#define CVC5__THEORY__ARITH__NL__TRANSCENDENTAL__TRANSCENDENTAL_SOLVER_H
#include <vector>
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__ARITH__TRANSCENDENTAL_SOLVER_H */
+#endif /* CVC5__THEORY__ARITH__TRANSCENDENTAL_SOLVER_H */
** \brief Utilities for transcendental lemmas.
**/
-#ifndef CVC4__THEORY__ARITH__NL__TRANSCENDENTAL__TRANSCENDENTAL_STATE_H
-#define CVC4__THEORY__ARITH__NL__TRANSCENDENTAL__TRANSCENDENTAL_STATE_H
+#ifndef CVC5__THEORY__ARITH__NL__TRANSCENDENTAL__TRANSCENDENTAL_STATE_H
+#define CVC5__THEORY__ARITH__NL__TRANSCENDENTAL__TRANSCENDENTAL_STATE_H
#include "expr/node.h"
#include "expr/proof_set.h"
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__ARITH__NL__TRANSCENDENTAL__TRANSCENDENTAL_STATE_H */
+#endif /* CVC5__THEORY__ARITH__NL__TRANSCENDENTAL__TRANSCENDENTAL_STATE_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__ARITH__NORMAL_FORM_H
-#define CVC4__THEORY__ARITH__NORMAL_FORM_H
+#ifndef CVC5__THEORY__ARITH__NORMAL_FORM_H
+#define CVC5__THEORY__ARITH__NORMAL_FORM_H
#include <algorithm>
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__ARITH__NORMAL_FORM_H */
+#endif /* CVC5__THEORY__ARITH__NORMAL_FORM_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__ARITH__PARTIAL_MODEL_H
-#define CVC4__THEORY__ARITH__PARTIAL_MODEL_H
+#ifndef CVC5__THEORY__ARITH__PARTIAL_MODEL_H
+#define CVC5__THEORY__ARITH__PARTIAL_MODEL_H
#include <vector>
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__ARITH__PARTIAL_MODEL_H */
+#endif /* CVC5__THEORY__ARITH__PARTIAL_MODEL_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__ARITH__PROOF_CHECKER_H
-#define CVC4__THEORY__ARITH__PROOF_CHECKER_H
+#ifndef CVC5__THEORY__ARITH__PROOF_CHECKER_H
+#define CVC5__THEORY__ARITH__PROOF_CHECKER_H
#include "expr/node.h"
#include "expr/proof_checker.h"
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__ARITH__PROOF_CHECKER_H */
+#endif /* CVC5__THEORY__ARITH__PROOF_CHECKER_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__ARITH__PROOF_MACROS_H
-#define CVC4__THEORY__ARITH__PROOF_MACROS_H
+#ifndef CVC5__THEORY__ARITH__PROOF_MACROS_H
+#define CVC5__THEORY__ARITH__PROOF_MACROS_H
#include "options/smt_options.h"
#define ARITH_NULLPROOF(x) (cvc5::options::produceProofs()) ? x : NULL
#define ARITH_PROOF_ON() cvc5::options::produceProofs()
-#endif // CVC4__THEORY__ARITH__PROOF_MACROS_H
+#endif // CVC5__THEORY__ARITH__PROOF_MACROS_H
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__ARITH__REWRITES_H
-#define CVC4__THEORY__ARITH__REWRITES_H
+#ifndef CVC5__THEORY__ARITH__REWRITES_H
+#define CVC5__THEORY__ARITH__REWRITES_H
#include <iosfwd>
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__ARITH__REWRITES_H */
+#endif /* CVC5__THEORY__ARITH__REWRITES_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__ARITH__THEORY_ARITH_TYPE_RULES_H
-#define CVC4__THEORY__ARITH__THEORY_ARITH_TYPE_RULES_H
+#ifndef CVC5__THEORY__ARITH__THEORY_ARITH_TYPE_RULES_H
+#define CVC5__THEORY__ARITH__THEORY_ARITH_TYPE_RULES_H
namespace cvc5 {
namespace theory {
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__ARITH__THEORY_ARITH_TYPE_RULES_H */
+#endif /* CVC5__THEORY__ARITH__THEORY_ARITH_TYPE_RULES_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__ARITH__TYPE_ENUMERATOR_H
-#define CVC4__THEORY__ARITH__TYPE_ENUMERATOR_H
+#ifndef CVC5__THEORY__ARITH__TYPE_ENUMERATOR_H
+#define CVC5__THEORY__ARITH__TYPE_ENUMERATOR_H
#include "expr/kind.h"
#include "expr/type_node.h"
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__ARITH__TYPE_ENUMERATOR_H */
+#endif /* CVC5__THEORY__ARITH__TYPE_ENUMERATOR_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__ARRAYS__ARRAY_INFO_H
-#define CVC4__THEORY__ARRAYS__ARRAY_INFO_H
+#ifndef CVC5__THEORY__ARRAYS__ARRAY_INFO_H
+#define CVC5__THEORY__ARRAYS__ARRAY_INFO_H
#include <tuple>
#include <unordered_map>
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__ARRAYS__ARRAY_INFO_H */
+#endif /* CVC5__THEORY__ARRAYS__ARRAY_INFO_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__ARRAYS__INFERENCE_MANAGER_H
-#define CVC4__THEORY__ARRAYS__INFERENCE_MANAGER_H
+#ifndef CVC5__THEORY__ARRAYS__INFERENCE_MANAGER_H
+#define CVC5__THEORY__ARRAYS__INFERENCE_MANAGER_H
#include "expr/node.h"
#include "expr/proof_rule.h"
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__ARRAYS__PROOF_CHECKER_H
-#define CVC4__THEORY__ARRAYS__PROOF_CHECKER_H
+#ifndef CVC5__THEORY__ARRAYS__PROOF_CHECKER_H
+#define CVC5__THEORY__ARRAYS__PROOF_CHECKER_H
#include "expr/node.h"
#include "expr/proof_checker.h"
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__ARRAYS__PROOF_CHECKER_H */
+#endif /* CVC5__THEORY__ARRAYS__PROOF_CHECKER_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__ARRAYS__SKOLEM_CACHE_H
-#define CVC4__THEORY__ARRAYS__SKOLEM_CACHE_H
+#ifndef CVC5__THEORY__ARRAYS__SKOLEM_CACHE_H
+#define CVC5__THEORY__ARRAYS__SKOLEM_CACHE_H
#include "expr/node.h"
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__ARRAYS__THEORY_ARRAYS_H
-#define CVC4__THEORY__ARRAYS__THEORY_ARRAYS_H
+#ifndef CVC5__THEORY__ARRAYS__THEORY_ARRAYS_H
+#define CVC5__THEORY__ARRAYS__THEORY_ARRAYS_H
#include <tuple>
#include <unordered_map>
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__ARRAYS__THEORY_ARRAYS_H */
+#endif /* CVC5__THEORY__ARRAYS__THEORY_ARRAYS_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__ARRAYS__THEORY_ARRAYS_REWRITER_H
-#define CVC4__THEORY__ARRAYS__THEORY_ARRAYS_REWRITER_H
+#ifndef CVC5__THEORY__ARRAYS__THEORY_ARRAYS_REWRITER_H
+#define CVC5__THEORY__ARRAYS__THEORY_ARRAYS_REWRITER_H
#include <unordered_map>
#include <unordered_set>
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__ARRAYS__THEORY_ARRAYS_REWRITER_H */
+#endif /* CVC5__THEORY__ARRAYS__THEORY_ARRAYS_REWRITER_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__ARRAYS__THEORY_ARRAYS_TYPE_RULES_H
-#define CVC4__THEORY__ARRAYS__THEORY_ARRAYS_TYPE_RULES_H
+#ifndef CVC5__THEORY__ARRAYS__THEORY_ARRAYS_TYPE_RULES_H
+#define CVC5__THEORY__ARRAYS__THEORY_ARRAYS_TYPE_RULES_H
#include "theory/arrays/theory_arrays_rewriter.h" // for array-constant attributes
#include "theory/type_enumerator.h"
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__ARRAYS__THEORY_ARRAYS_TYPE_RULES_H */
+#endif /* CVC5__THEORY__ARRAYS__THEORY_ARRAYS_TYPE_RULES_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__ARRAYS__TYPE_ENUMERATOR_H
-#define CVC4__THEORY__ARRAYS__TYPE_ENUMERATOR_H
+#ifndef CVC5__THEORY__ARRAYS__TYPE_ENUMERATOR_H
+#define CVC5__THEORY__ARRAYS__TYPE_ENUMERATOR_H
#include "theory/type_enumerator.h"
#include "expr/type_node.h"
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__ARRAYS__TYPE_ENUMERATOR_H */
+#endif /* CVC5__THEORY__ARRAYS__TYPE_ENUMERATOR_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__ARRAYS__UNION_FIND_H
-#define CVC4__THEORY__ARRAYS__UNION_FIND_H
+#ifndef CVC5__THEORY__ARRAYS__UNION_FIND_H
+#define CVC5__THEORY__ARRAYS__UNION_FIND_H
#include <utility>
#include <vector>
} // namespace theory
} // namespace cvc5
-#endif /*CVC4__THEORY__ARRAYS__UNION_FIND_H */
+#endif /*CVC5__THEORY__ARRAYS__UNION_FIND_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__ASSERTION_H
-#define CVC4__THEORY__ASSERTION_H
+#ifndef CVC5__THEORY__ASSERTION_H
+#define CVC5__THEORY__ASSERTION_H
#include "expr/node.h"
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__ASSERTION_H */
+#endif /* CVC5__THEORY__ASSERTION_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__BAG__SOLVER_H
-#define CVC4__THEORY__BAG__SOLVER_H
+#ifndef CVC5__THEORY__BAG__SOLVER_H
+#define CVC5__THEORY__BAG__SOLVER_H
#include "theory/bags/inference_generator.h"
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__BAG__SOLVER_H */
+#endif /* CVC5__THEORY__BAG__SOLVER_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__BAGS__THEORY_BAGS_REWRITER_H
-#define CVC4__THEORY__BAGS__THEORY_BAGS_REWRITER_H
+#ifndef CVC5__THEORY__BAGS__THEORY_BAGS_REWRITER_H
+#define CVC5__THEORY__BAGS__THEORY_BAGS_REWRITER_H
#include "theory/bags/rewrites.h"
#include "theory/theory_rewriter.h"
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__BAGS__THEORY_BAGS_REWRITER_H */
+#endif /* CVC5__THEORY__BAGS__THEORY_BAGS_REWRITER_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__BAGS_STATISTICS_H
-#define CVC4__THEORY__BAGS_STATISTICS_H
+#ifndef CVC5__THEORY__BAGS_STATISTICS_H
+#define CVC5__THEORY__BAGS_STATISTICS_H
#include "theory/bags/rewrites.h"
#include "util/statistics_registry.h"
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__BAGS_STATISTICS_H */
+#endif /* CVC5__THEORY__BAGS_STATISTICS_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__BAGS__INFER_INFO_H
-#define CVC4__THEORY__BAGS__INFER_INFO_H
+#ifndef CVC5__THEORY__BAGS__INFER_INFO_H
+#define CVC5__THEORY__BAGS__INFER_INFO_H
#include <map>
#include <vector>
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__BAGS__INFER_INFO_H */
+#endif /* CVC5__THEORY__BAGS__INFER_INFO_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__BAGS__INFERENCE_GENERATOR_H
-#define CVC4__THEORY__BAGS__INFERENCE_GENERATOR_H
+#ifndef CVC5__THEORY__BAGS__INFERENCE_GENERATOR_H
+#define CVC5__THEORY__BAGS__INFERENCE_GENERATOR_H
#include "expr/node.h"
#include "infer_info.h"
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__BAGS__INFERENCE_GENERATOR_H */
+#endif /* CVC5__THEORY__BAGS__INFERENCE_GENERATOR_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__BAGS__INFERENCE_MANAGER_H
-#define CVC4__THEORY__BAGS__INFERENCE_MANAGER_H
+#ifndef CVC5__THEORY__BAGS__INFERENCE_MANAGER_H
+#define CVC5__THEORY__BAGS__INFERENCE_MANAGER_H
#include "theory/inference_manager_buffered.h"
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__BAGS__INFERENCE_MANAGER_H */
+#endif /* CVC5__THEORY__BAGS__INFERENCE_MANAGER_H */
#include "cvc4_public.h"
-#ifndef CVC4__MAKE_BAG_OP_H
-#define CVC4__MAKE_BAG_OP_H
+#ifndef CVC5__MAKE_BAG_OP_H
+#define CVC5__MAKE_BAG_OP_H
#include <memory>
} // namespace cvc5
-#endif /* CVC4__MAKE_BAG_OP_H */
+#endif /* CVC5__MAKE_BAG_OP_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__BAGS__NORMAL_FORM_H
-#define CVC4__THEORY__BAGS__NORMAL_FORM_H
+#ifndef CVC5__THEORY__BAGS__NORMAL_FORM_H
+#define CVC5__THEORY__BAGS__NORMAL_FORM_H
namespace cvc5 {
namespace theory {
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__BAGS__NORMAL_FORM_H */
+#endif /* CVC5__THEORY__BAGS__NORMAL_FORM_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__BAGS__REWRITES_H
-#define CVC4__THEORY__BAGS__REWRITES_H
+#ifndef CVC5__THEORY__BAGS__REWRITES_H
+#define CVC5__THEORY__BAGS__REWRITES_H
#include <iosfwd>
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__BAGS__REWRITES_H */
+#endif /* CVC5__THEORY__BAGS__REWRITES_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__BAGS__THEORY_SOLVER_STATE_H
-#define CVC4__THEORY__BAGS__THEORY_SOLVER_STATE_H
+#ifndef CVC5__THEORY__BAGS__THEORY_SOLVER_STATE_H
+#define CVC5__THEORY__BAGS__THEORY_SOLVER_STATE_H
#include <map>
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__BAGS__THEORY_SOLVER_STATE_H */
+#endif /* CVC5__THEORY__BAGS__THEORY_SOLVER_STATE_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__BAGS__TERM_REGISTRY_H
-#define CVC4__THEORY__BAGS__TERM_REGISTRY_H
+#ifndef CVC5__THEORY__BAGS__TERM_REGISTRY_H
+#define CVC5__THEORY__BAGS__TERM_REGISTRY_H
#include <map>
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__BAGS__TERM_REGISTRY_H */
+#endif /* CVC5__THEORY__BAGS__TERM_REGISTRY_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__BAGS__THEORY_BAGS_H
-#define CVC4__THEORY__BAGS__THEORY_BAGS_H
+#ifndef CVC5__THEORY__BAGS__THEORY_BAGS_H
+#define CVC5__THEORY__BAGS__THEORY_BAGS_H
#include "theory/bags/bag_solver.h"
#include "theory/bags/bags_rewriter.h"
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__BAGS__THEORY_BAGS_H */
+#endif /* CVC5__THEORY__BAGS__THEORY_BAGS_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__BAGS__TYPE_ENUMERATOR_H
-#define CVC4__THEORY__BAGS__TYPE_ENUMERATOR_H
+#ifndef CVC5__THEORY__BAGS__TYPE_ENUMERATOR_H
+#define CVC5__THEORY__BAGS__TYPE_ENUMERATOR_H
#include "expr/type_node.h"
#include "theory/type_enumerator.h"
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__BAGS__TYPE_ENUMERATOR_H */
\ No newline at end of file
+#endif /* CVC5__THEORY__BAGS__TYPE_ENUMERATOR_H */
\ No newline at end of file
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__BAGS__THEORY_BAGS_TYPE_RULES_H
-#define CVC4__THEORY__BAGS__THEORY_BAGS_TYPE_RULES_H
+#ifndef CVC5__THEORY__BAGS__THEORY_BAGS_TYPE_RULES_H
+#define CVC5__THEORY__BAGS__THEORY_BAGS_TYPE_RULES_H
#include "expr/node.h"
#include "expr/type_node.h"
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__BAGS__THEORY_BAGS_TYPE_RULES_H */
+#endif /* CVC5__THEORY__BAGS__THEORY_BAGS_TYPE_RULES_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__BOOLEANS__CIRCUIT_PROPAGATOR_H
-#define CVC4__THEORY__BOOLEANS__CIRCUIT_PROPAGATOR_H
+#ifndef CVC5__THEORY__BOOLEANS__CIRCUIT_PROPAGATOR_H
+#define CVC5__THEORY__BOOLEANS__CIRCUIT_PROPAGATOR_H
#include <memory>
#include <unordered_map>
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__BOOLEANS__CIRCUIT_PROPAGATOR_H */
+#endif /* CVC5__THEORY__BOOLEANS__CIRCUIT_PROPAGATOR_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__BOOLEANS__PROOF_CHECKER_H
-#define CVC4__THEORY__BOOLEANS__PROOF_CHECKER_H
+#ifndef CVC5__THEORY__BOOLEANS__PROOF_CHECKER_H
+#define CVC5__THEORY__BOOLEANS__PROOF_CHECKER_H
#include "expr/node.h"
#include "expr/proof_checker.h"
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__BOOLEANS__PROOF_CHECKER_H */
+#endif /* CVC5__THEORY__BOOLEANS__PROOF_CHECKER_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__BOOLEANS__PROOF_CIRCUIT_PROPAGATOR_H
-#define CVC4__THEORY__BOOLEANS__PROOF_CIRCUIT_PROPAGATOR_H
+#ifndef CVC5__THEORY__BOOLEANS__PROOF_CIRCUIT_PROPAGATOR_H
+#define CVC5__THEORY__BOOLEANS__PROOF_CIRCUIT_PROPAGATOR_H
#include <memory>
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__BOOLEANS__THEORY_BOOL_H
-#define CVC4__THEORY__BOOLEANS__THEORY_BOOL_H
+#ifndef CVC5__THEORY__BOOLEANS__THEORY_BOOL_H
+#define CVC5__THEORY__BOOLEANS__THEORY_BOOL_H
#include "context/context.h"
#include "theory/booleans/proof_checker.h"
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__BOOLEANS__THEORY_BOOL_H */
+#endif /* CVC5__THEORY__BOOLEANS__THEORY_BOOL_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__BOOLEANS__THEORY_BOOL_REWRITER_H
-#define CVC4__THEORY__BOOLEANS__THEORY_BOOL_REWRITER_H
+#ifndef CVC5__THEORY__BOOLEANS__THEORY_BOOL_REWRITER_H
+#define CVC5__THEORY__BOOLEANS__THEORY_BOOL_REWRITER_H
#include "theory/theory_rewriter.h"
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__BOOLEANS__THEORY_BOOL_REWRITER_H */
+#endif /* CVC5__THEORY__BOOLEANS__THEORY_BOOL_REWRITER_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY_BOOL_TYPE_RULES_H
-#define CVC4__THEORY_BOOL_TYPE_RULES_H
+#ifndef CVC5__THEORY_BOOL_TYPE_RULES_H
+#define CVC5__THEORY_BOOL_TYPE_RULES_H
namespace cvc5 {
namespace theory {
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY_BOOL_TYPE_RULES_H */
+#endif /* CVC5__THEORY_BOOL_TYPE_RULES_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__BOOLEANS__TYPE_ENUMERATOR_H
-#define CVC4__THEORY__BOOLEANS__TYPE_ENUMERATOR_H
+#ifndef CVC5__THEORY__BOOLEANS__TYPE_ENUMERATOR_H
+#define CVC5__THEORY__BOOLEANS__TYPE_ENUMERATOR_H
#include "theory/type_enumerator.h"
#include "expr/type_node.h"
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__BOOLEANS__TYPE_ENUMERATOR_H */
+#endif /* CVC5__THEORY__BOOLEANS__TYPE_ENUMERATOR_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__BUILTIN__PROOF_CHECKER_H
-#define CVC4__THEORY__BUILTIN__PROOF_CHECKER_H
+#ifndef CVC5__THEORY__BUILTIN__PROOF_CHECKER_H
+#define CVC5__THEORY__BUILTIN__PROOF_CHECKER_H
#include "expr/node.h"
#include "expr/proof_checker.h"
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__BUILTIN__PROOF_CHECKER_H */
+#endif /* CVC5__THEORY__BUILTIN__PROOF_CHECKER_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__BUILTIN__THEORY_BUILTIN_H
-#define CVC4__THEORY__BUILTIN__THEORY_BUILTIN_H
+#ifndef CVC5__THEORY__BUILTIN__THEORY_BUILTIN_H
+#define CVC5__THEORY__BUILTIN__THEORY_BUILTIN_H
#include "theory/builtin/proof_checker.h"
#include "theory/builtin/theory_builtin_rewriter.h"
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__BUILTIN__THEORY_BUILTIN_H */
+#endif /* CVC5__THEORY__BUILTIN__THEORY_BUILTIN_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__BUILTIN__THEORY_BUILTIN_REWRITER_H
-#define CVC4__THEORY__BUILTIN__THEORY_BUILTIN_REWRITER_H
+#ifndef CVC5__THEORY__BUILTIN__THEORY_BUILTIN_REWRITER_H
+#define CVC5__THEORY__BUILTIN__THEORY_BUILTIN_REWRITER_H
#include "theory/theory_rewriter.h"
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__BUILTIN__THEORY_BUILTIN_REWRITER_H */
+#endif /* CVC5__THEORY__BUILTIN__THEORY_BUILTIN_REWRITER_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__BUILTIN__THEORY_BUILTIN_TYPE_RULES_H
-#define CVC4__THEORY__BUILTIN__THEORY_BUILTIN_TYPE_RULES_H
+#ifndef CVC5__THEORY__BUILTIN__THEORY_BUILTIN_TYPE_RULES_H
+#define CVC5__THEORY__BUILTIN__THEORY_BUILTIN_TYPE_RULES_H
#include "expr/node.h"
#include "expr/type_node.h"
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__BUILTIN__THEORY_BUILTIN_TYPE_RULES_H */
+#endif /* CVC5__THEORY__BUILTIN__THEORY_BUILTIN_TYPE_RULES_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__BUILTIN__TYPE_ENUMERATOR_H
-#define CVC4__THEORY__BUILTIN__TYPE_ENUMERATOR_H
+#ifndef CVC5__THEORY__BUILTIN__TYPE_ENUMERATOR_H
+#define CVC5__THEORY__BUILTIN__TYPE_ENUMERATOR_H
#include "expr/kind.h"
#include "expr/type_node.h"
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__BUILTIN_TYPE_ENUMERATOR_H */
+#endif /* CVC5__THEORY__BUILTIN_TYPE_ENUMERATOR_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__BV__ABSTRACTION_H
-#define CVC4__THEORY__BV__ABSTRACTION_H
+#ifndef CVC5__THEORY__BV__ABSTRACTION_H
+#define CVC5__THEORY__BV__ABSTRACTION_H
#include <unordered_map>
#include <unordered_set>
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__BV__BITBLAST__AIG_BITBLASTER_H
-#define CVC4__THEORY__BV__BITBLAST__AIG_BITBLASTER_H
+#ifndef CVC5__THEORY__BV__BITBLAST__AIG_BITBLASTER_H
+#define CVC5__THEORY__BV__BITBLAST__AIG_BITBLASTER_H
#include "theory/bv/bitblast/bitblaster.h"
} // namespace theory
} // namespace cvc5
-#endif // CVC4__THEORY__BV__BITBLAST__AIG_BITBLASTER_H
+#endif // CVC5__THEORY__BV__BITBLAST__AIG_BITBLASTER_H
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__BV__BITBLAST__BITBLAST_STRATEGIES_TEMPLATE_H
-#define CVC4__THEORY__BV__BITBLAST__BITBLAST_STRATEGIES_TEMPLATE_H
+#ifndef CVC5__THEORY__BV__BITBLAST__BITBLAST_STRATEGIES_TEMPLATE_H
+#define CVC5__THEORY__BV__BITBLAST__BITBLAST_STRATEGIES_TEMPLATE_H
#include <cmath>
#include <ostream>
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__BV__BITBLAST__BITBLAST_UTILS_H
-#define CVC4__THEORY__BV__BITBLAST__BITBLAST_UTILS_H
-
+#ifndef CVC5__THEORY__BV__BITBLAST__BITBLAST_UTILS_H
+#define CVC5__THEORY__BV__BITBLAST__BITBLAST_UTILS_H
#include <ostream>
#include "expr/node.h"
} // namespace theory
} // namespace cvc5
-#endif // CVC4__THEORY__BV__BITBLAST__BITBLAST_UTILS_H
+#endif // CVC5__THEORY__BV__BITBLAST__BITBLAST_UTILS_H
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__BV__BITBLAST__BITBLASTER_H
-#define CVC4__THEORY__BV__BITBLAST__BITBLASTER_H
+#ifndef CVC5__THEORY__BV__BITBLAST__BITBLASTER_H
+#define CVC5__THEORY__BV__BITBLAST__BITBLASTER_H
#include <unordered_map>
#include <unordered_set>
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__BV__BITBLAST__BITBLASTER_H */
+#endif /* CVC5__THEORY__BV__BITBLAST__BITBLASTER_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__BV__BITBLAST__EAGER_BITBLASTER_H
-#define CVC4__THEORY__BV__BITBLAST__EAGER_BITBLASTER_H
+#ifndef CVC5__THEORY__BV__BITBLAST__EAGER_BITBLASTER_H
+#define CVC5__THEORY__BV__BITBLAST__EAGER_BITBLASTER_H
#include <memory>
#include <unordered_set>
} // namespace bv
} // namespace theory
} // namespace cvc5
-#endif // CVC4__THEORY__BV__BITBLAST__EAGER_BITBLASTER_H
+#endif // CVC5__THEORY__BV__BITBLAST__EAGER_BITBLASTER_H
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__BV__BITBLAST__LAZY_BITBLASTER_H
-#define CVC4__THEORY__BV__BITBLAST__LAZY_BITBLASTER_H
+#ifndef CVC5__THEORY__BV__BITBLAST__LAZY_BITBLASTER_H
+#define CVC5__THEORY__BV__BITBLAST__LAZY_BITBLASTER_H
#include "theory/bv/bitblast/bitblaster.h"
} // namespace bv
} // namespace theory
} // namespace cvc5
-#endif // CVC4__THEORY__BV__BITBLAST__LAZY_BITBLASTER_H
+#endif // CVC5__THEORY__BV__BITBLAST__LAZY_BITBLASTER_H
**/
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__BV__BITBLAST__PROOF_BITBLASTER_H
-#define CVC4__THEORY__BV__BITBLAST__PROOF_BITBLASTER_H
+#ifndef CVC5__THEORY__BV__BITBLAST__PROOF_BITBLASTER_H
+#define CVC5__THEORY__BV__BITBLAST__PROOF_BITBLASTER_H
#include "theory/bv/bitblast/simple_bitblaster.h"
**/
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__BV__BITBLAST_SIMPLE_BITBLASTER_H
-#define CVC4__THEORY__BV__BITBLAST_SIMPLE_BITBLASTER_H
+#ifndef CVC5__THEORY__BV__BITBLAST_SIMPLE_BITBLASTER_H
+#define CVC5__THEORY__BV__BITBLAST_SIMPLE_BITBLASTER_H
#include "theory/bv/bitblast/bitblaster.h"
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__BV__BV_EAGER_SOLVER_H
-#define CVC4__THEORY__BV__BV_EAGER_SOLVER_H
+#ifndef CVC5__THEORY__BV__BV_EAGER_SOLVER_H
+#define CVC5__THEORY__BV__BV_EAGER_SOLVER_H
#include "expr/node.h"
#include "theory/bv/bv_solver_lazy.h"
} // namespace theory
} // namespace cvc5
-#endif // CVC4__THEORY__BV__BV_EAGER_SOLVER_H
+#endif // CVC5__THEORY__BV__BV_EAGER_SOLVER_H
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__BV__BV_INEQUALITY__GRAPH_H
-#define CVC4__THEORY__BV__BV_INEQUALITY__GRAPH_H
+#ifndef CVC5__THEORY__BV__BV_INEQUALITY__GRAPH_H
+#define CVC5__THEORY__BV__BV_INEQUALITY__GRAPH_H
#include <queue>
#include <unordered_map>
}
} // namespace cvc5
-#endif /* CVC4__THEORY__BV__BV_INEQUALITY__GRAPH_H */
+#endif /* CVC5__THEORY__BV__BV_INEQUALITY__GRAPH_H */
#include "cvc4_private.h"
-#ifndef CVC4__BV_QUICK_CHECK_H
-#define CVC4__BV_QUICK_CHECK_H
+#ifndef CVC5__BV_QUICK_CHECK_H
+#define CVC5__BV_QUICK_CHECK_H
#include <unordered_set>
#include <vector>
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__BV_QUICK_CHECK_H */
+#endif /* CVC5__BV_QUICK_CHECK_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__BV__BV_SOLVER_H
-#define CVC4__THEORY__BV__BV_SOLVER_H
+#ifndef CVC5__THEORY__BV__BV_SOLVER_H
+#define CVC5__THEORY__BV__BV_SOLVER_H
#include "theory/theory.h"
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__BV__BV_SOLVER_H */
+#endif /* CVC5__THEORY__BV__BV_SOLVER_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__BV__BV_SOLVER_BITBLAST_H
-#define CVC4__THEORY__BV__BV_SOLVER_BITBLAST_H
+#ifndef CVC5__THEORY__BV__BV_SOLVER_BITBLAST_H
+#define CVC5__THEORY__BV__BV_SOLVER_BITBLAST_H
#include <unordered_map>
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__BV__BV_SOLVER_LAZY_H
-#define CVC4__THEORY__BV__BV_SOLVER_LAZY_H
+#ifndef CVC5__THEORY__BV__BV_SOLVER_LAZY_H
+#define CVC5__THEORY__BV__BV_SOLVER_LAZY_H
#include <unordered_map>
#include <unordered_set>
} // namespace cvc5
-#endif /* CVC4__THEORY__BV__BV_SOLVER_LAZY_H */
+#endif /* CVC5__THEORY__BV__BV_SOLVER_LAZY_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__BV__BV_SOLVER_SIMPLE_H
-#define CVC4__THEORY__BV__BV_SOLVER_SIMPLE_H
+#ifndef CVC5__THEORY__BV__BV_SOLVER_SIMPLE_H
+#define CVC5__THEORY__BV__BV_SOLVER_SIMPLE_H
#include "theory/bv/bitblast/proof_bitblaster.h"
#include "theory/bv/bv_solver.h"
** Interface for bit-vectors sub-solvers.
**/
-#ifndef CVC4__THEORY__BV__BV_SUBTHEORY_H
-#define CVC4__THEORY__BV__BV_SUBTHEORY_H
+#ifndef CVC5__THEORY__BV__BV_SUBTHEORY_H
+#define CVC5__THEORY__BV__BV_SUBTHEORY_H
#include "cvc4_private.h"
#include "context/context.h"
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__BV__BV_SUBTHEORY_H */
+#endif /* CVC5__THEORY__BV__BV_SUBTHEORY_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__BV__BV_SUBTHEORY__INEQUALITY_H
-#define CVC4__THEORY__BV__BV_SUBTHEORY__INEQUALITY_H
+#ifndef CVC5__THEORY__BV__BV_SUBTHEORY__INEQUALITY_H
+#define CVC5__THEORY__BV__BV_SUBTHEORY__INEQUALITY_H
#include <unordered_set>
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__BV__BV_SUBTHEORY__INEQUALITY_H */
+#endif /* CVC5__THEORY__BV__BV_SUBTHEORY__INEQUALITY_H */
#include "cvc4_private.h"
-#ifndef __CVC4__THEORY__BV__INT_BLASTER__H
-#define __CVC4__THEORY__BV__INT_BLASTER__H
+#ifndef __CVC5__THEORY__BV__INT_BLASTER__H
+#define __CVC5__THEORY__BV__INT_BLASTER__H
#include "context/cdhashmap.h"
#include "context/cdhashset.h"
} // namespace cvc5
-#endif /* __CVC4__THEORY__BV__INT_BLASTER_H */
+#endif /* __CVC5__THEORY__BV__INT_BLASTER_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__BV__PROOF_CHECKER_H
-#define CVC4__THEORY__BV__PROOF_CHECKER_H
+#ifndef CVC5__THEORY__BV__PROOF_CHECKER_H
+#define CVC5__THEORY__BV__PROOF_CHECKER_H
#include "expr/node.h"
#include "expr/proof_checker.h"
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__BV__PROOF_CHECKER_H */
+#endif /* CVC5__THEORY__BV__PROOF_CHECKER_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__BV__SLICER_BV_H
-#define CVC4__THEORY__BV__SLICER_BV_H
+#ifndef CVC5__THEORY__BV__SLICER_BV_H
+#define CVC5__THEORY__BV__SLICER_BV_H
#include <string>
#include <vector>
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__BV__SLICER_BV_H */
+#endif /* CVC5__THEORY__BV__SLICER_BV_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__BV__THEORY_BV_H
-#define CVC4__THEORY__BV__THEORY_BV_H
+#ifndef CVC5__THEORY__BV__THEORY_BV_H
+#define CVC5__THEORY__BV__THEORY_BV_H
#include "theory/bv/theory_bv_rewriter.h"
#include "theory/theory.h"
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__BV__THEORY_BV_H */
+#endif /* CVC5__THEORY__BV__THEORY_BV_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__BV__THEORY_BV_REWRITER_H
-#define CVC4__THEORY__BV__THEORY_BV_REWRITER_H
+#ifndef CVC5__THEORY__BV__THEORY_BV_REWRITER_H
+#define CVC5__THEORY__BV__THEORY_BV_REWRITER_H
#include "theory/theory_rewriter.h"
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__BV__THEORY_BV_REWRITER_H */
+#endif /* CVC5__THEORY__BV__THEORY_BV_REWRITER_H */
#include <algorithm>
-#ifndef CVC4__THEORY__BV__THEORY_BV_TYPE_RULES_H
-#define CVC4__THEORY__BV__THEORY_BV_TYPE_RULES_H
+#ifndef CVC5__THEORY__BV__THEORY_BV_TYPE_RULES_H
+#define CVC5__THEORY__BV__THEORY_BV_TYPE_RULES_H
namespace cvc5 {
namespace theory {
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__BV__THEORY_BV_TYPE_RULES_H */
+#endif /* CVC5__THEORY__BV__THEORY_BV_TYPE_RULES_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__BV__TYPE_ENUMERATOR_H
-#define CVC4__THEORY__BV__TYPE_ENUMERATOR_H
+#ifndef CVC5__THEORY__BV__TYPE_ENUMERATOR_H
+#define CVC5__THEORY__BV__TYPE_ENUMERATOR_H
#include "expr/kind.h"
#include "expr/type_node.h"
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__BV__TYPE_ENUMERATOR_H */
+#endif /* CVC5__THEORY__BV__TYPE_ENUMERATOR_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__CARE_GRAPH_H
-#define CVC4__THEORY__CARE_GRAPH_H
+#ifndef CVC5__THEORY__CARE_GRAPH_H
+#define CVC5__THEORY__CARE_GRAPH_H
#include <set>
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__CARE_GRAPH_H */
+#endif /* CVC5__THEORY__CARE_GRAPH_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__COMBINATION_CARE_GRAPH__H
-#define CVC4__THEORY__COMBINATION_CARE_GRAPH__H
+#ifndef CVC5__THEORY__COMBINATION_CARE_GRAPH__H
+#define CVC5__THEORY__COMBINATION_CARE_GRAPH__H
#include <vector>
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__COMBINATION_DISTRIBUTED__H */
+#endif /* CVC5__THEORY__COMBINATION_DISTRIBUTED__H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__COMBINATION_ENGINE__H
-#define CVC4__THEORY__COMBINATION_ENGINE__H
+#ifndef CVC5__THEORY__COMBINATION_ENGINE__H
+#define CVC5__THEORY__COMBINATION_ENGINE__H
#include <vector>
#include <memory>
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__COMBINATION_DISTRIBUTED__H */
+#endif /* CVC5__THEORY__COMBINATION_DISTRIBUTED__H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__DATATYPES__DATATYPES_REWRITER_H
-#define CVC4__THEORY__DATATYPES__DATATYPES_REWRITER_H
+#ifndef CVC5__THEORY__DATATYPES__DATATYPES_REWRITER_H
+#define CVC5__THEORY__DATATYPES__DATATYPES_REWRITER_H
#include "theory/theory_rewriter.h"
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__DATATYPES__DATATYPES_REWRITER_H */
+#endif /* CVC5__THEORY__DATATYPES__DATATYPES_REWRITER_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__DATATYPES__INFER_PROOF_CONS_H
-#define CVC4__THEORY__DATATYPES__INFER_PROOF_CONS_H
+#ifndef CVC5__THEORY__DATATYPES__INFER_PROOF_CONS_H
+#define CVC5__THEORY__DATATYPES__INFER_PROOF_CONS_H
#include "context/cdhashmap.h"
#include "expr/node.h"
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__DATATYPES__INFER_PROOF_CONS_H */
+#endif /* CVC5__THEORY__DATATYPES__INFER_PROOF_CONS_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__DATATYPES__INFERENCE_H
-#define CVC4__THEORY__DATATYPES__INFERENCE_H
+#ifndef CVC5__THEORY__DATATYPES__INFERENCE_H
+#define CVC5__THEORY__DATATYPES__INFERENCE_H
#include "expr/node.h"
#include "theory/inference_id.h"
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__DATATYPES__INFERENCE_MANAGER_H
-#define CVC4__THEORY__DATATYPES__INFERENCE_MANAGER_H
+#ifndef CVC5__THEORY__DATATYPES__INFERENCE_MANAGER_H
+#define CVC5__THEORY__DATATYPES__INFERENCE_MANAGER_H
#include "expr/node.h"
#include "theory/datatypes/infer_proof_cons.h"
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__DATATYPES__PROOF_CHECKER_H
-#define CVC4__THEORY__DATATYPES__PROOF_CHECKER_H
+#ifndef CVC5__THEORY__DATATYPES__PROOF_CHECKER_H
+#define CVC5__THEORY__DATATYPES__PROOF_CHECKER_H
#include "expr/node.h"
#include "expr/proof_checker.h"
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__DATATYPES__PROOF_CHECKER_H */
+#endif /* CVC5__THEORY__DATATYPES__PROOF_CHECKER_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__STRINGS__SYGUS_DATATYPE_UTILS_H
-#define CVC4__THEORY__STRINGS__SYGUS_DATATYPE_UTILS_H
+#ifndef CVC5__THEORY__STRINGS__SYGUS_DATATYPE_UTILS_H
+#define CVC5__THEORY__STRINGS__SYGUS_DATATYPE_UTILS_H
#include <vector>
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__DATATYPES__SYGUS_EXTENSION_H
-#define CVC4__THEORY__DATATYPES__SYGUS_EXTENSION_H
+#ifndef CVC5__THEORY__DATATYPES__SYGUS_EXTENSION_H
+#define CVC5__THEORY__DATATYPES__SYGUS_EXTENSION_H
#include <iostream>
#include <map>
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__DATATYPES__SIMPLE_SYM_BREAK_H
-#define CVC4__THEORY__DATATYPES__SIMPLE_SYM_BREAK_H
+#ifndef CVC5__THEORY__DATATYPES__SIMPLE_SYM_BREAK_H
+#define CVC5__THEORY__DATATYPES__SIMPLE_SYM_BREAK_H
#include "expr/dtype.h"
#include "theory/quantifiers/sygus/term_database_sygus.h"
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__DATATYPES__SIMPLE_SYM_BREAK_H */
+#endif /* CVC5__THEORY__DATATYPES__SIMPLE_SYM_BREAK_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__DATATYPES__THEORY_DATATYPES_H
-#define CVC4__THEORY__DATATYPES__THEORY_DATATYPES_H
+#ifndef CVC5__THEORY__DATATYPES__THEORY_DATATYPES_H
+#define CVC5__THEORY__DATATYPES__THEORY_DATATYPES_H
#include <iostream>
#include <map>
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__DATATYPES__THEORY_DATATYPES_H */
+#endif /* CVC5__THEORY__DATATYPES__THEORY_DATATYPES_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__DATATYPES__THEORY_DATATYPES_TYPE_RULES_H
-#define CVC4__THEORY__DATATYPES__THEORY_DATATYPES_TYPE_RULES_H
+#ifndef CVC5__THEORY__DATATYPES__THEORY_DATATYPES_TYPE_RULES_H
+#define CVC5__THEORY__DATATYPES__THEORY_DATATYPES_TYPE_RULES_H
#include "expr/dtype.h"
#include "expr/dtype_cons.h"
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__DATATYPES__THEORY_DATATYPES_TYPE_RULES_H */
+#endif /* CVC5__THEORY__DATATYPES__THEORY_DATATYPES_TYPE_RULES_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__STRINGS__THEORY_DATATYPES_UTILS_H
-#define CVC4__THEORY__STRINGS__THEORY_DATATYPES_UTILS_H
+#ifndef CVC5__THEORY__STRINGS__THEORY_DATATYPES_UTILS_H
+#define CVC5__THEORY__STRINGS__THEORY_DATATYPES_UTILS_H
#include <vector>
#include "cvc4_public.h"
-#ifndef CVC4__PROJECT_OP_H
-#define CVC4__PROJECT_OP_H
+#ifndef CVC5__PROJECT_OP_H
+#define CVC5__PROJECT_OP_H
#include <ostream>
#include <vector>
} // namespace cvc5
-#endif /* CVC4__PROJECT_OP_H */
+#endif /* CVC5__PROJECT_OP_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__DATATYPES__TYPE_ENUMERATOR_H
-#define CVC4__THEORY__DATATYPES__TYPE_ENUMERATOR_H
+#ifndef CVC5__THEORY__DATATYPES__TYPE_ENUMERATOR_H
+#define CVC5__THEORY__DATATYPES__TYPE_ENUMERATOR_H
#include "expr/dtype.h"
#include "expr/kind.h"
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__DATATYPES__TYPE_ENUMERATOR_H */
+#endif /* CVC5__THEORY__DATATYPES__TYPE_ENUMERATOR_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__DECISION_MANAGER__H
-#define CVC4__THEORY__DECISION_MANAGER__H
+#ifndef CVC5__THEORY__DECISION_MANAGER__H
+#define CVC5__THEORY__DECISION_MANAGER__H
#include <map>
#include "context/cdlist.h"
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__DECISION_MANAGER__H */
+#endif /* CVC5__THEORY__DECISION_MANAGER__H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__DECISION_STRATEGY__H
-#define CVC4__THEORY__DECISION_STRATEGY__H
+#ifndef CVC5__THEORY__DECISION_STRATEGY__H
+#define CVC5__THEORY__DECISION_STRATEGY__H
#include "context/cdo.h"
#include "expr/node.h"
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__DECISION_STRATEGY__H */
+#endif /* CVC5__THEORY__DECISION_STRATEGY__H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__EAGER_PROOF_GENERATOR_H
-#define CVC4__THEORY__EAGER_PROOF_GENERATOR_H
+#ifndef CVC5__THEORY__EAGER_PROOF_GENERATOR_H
+#define CVC5__THEORY__EAGER_PROOF_GENERATOR_H
#include "context/cdhashmap.h"
#include "expr/node.h"
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__PROOF_GENERATOR_H */
+#endif /* CVC5__THEORY__PROOF_GENERATOR_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__EE_MANAGER__H
-#define CVC4__THEORY__EE_MANAGER__H
+#ifndef CVC5__THEORY__EE_MANAGER__H
+#define CVC5__THEORY__EE_MANAGER__H
#include <map>
#include <memory>
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__EE_MANAGER__H */
+#endif /* CVC5__THEORY__EE_MANAGER__H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__EE_MANAGER_DISTRIBUTED__H
-#define CVC4__THEORY__EE_MANAGER_DISTRIBUTED__H
+#ifndef CVC5__THEORY__EE_MANAGER_DISTRIBUTED__H
+#define CVC5__THEORY__EE_MANAGER_DISTRIBUTED__H
#include <memory>
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__EE_MANAGER_DISTRIBUTED__H */
+#endif /* CVC5__THEORY__EE_MANAGER_DISTRIBUTED__H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__EE_SETUP_INFO__H
-#define CVC4__THEORY__EE_SETUP_INFO__H
+#ifndef CVC5__THEORY__EE_SETUP_INFO__H
+#define CVC5__THEORY__EE_SETUP_INFO__H
#include <string>
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__EE_SETUP_INFO__H */
+#endif /* CVC5__THEORY__EE_SETUP_INFO__H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__ENGINE_OUTPUT_CHANNEL_H
-#define CVC4__THEORY__ENGINE_OUTPUT_CHANNEL_H
+#ifndef CVC5__THEORY__ENGINE_OUTPUT_CHANNEL_H
+#define CVC5__THEORY__ENGINE_OUTPUT_CHANNEL_H
#include "expr/node.h"
#include "theory/output_channel.h"
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__ENGINE_OUTPUT_CHANNEL_H */
+#endif /* CVC5__THEORY__ENGINE_OUTPUT_CHANNEL_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__EVALUATOR_H
-#define CVC4__THEORY__EVALUATOR_H
+#ifndef CVC5__THEORY__EVALUATOR_H
+#define CVC5__THEORY__EVALUATOR_H
#include <utility>
#include <vector>
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__EVALUATOR_H */
+#endif /* CVC5__THEORY__EVALUATOR_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__EXT_THEORY_H
-#define CVC4__THEORY__EXT_THEORY_H
+#ifndef CVC5__THEORY__EXT_THEORY_H
+#define CVC5__THEORY__EXT_THEORY_H
#include <map>
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__EXT_THEORY_H */
+#endif /* CVC5__THEORY__EXT_THEORY_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__FP__FP_CONVERTER_H
-#define CVC4__THEORY__FP__FP_CONVERTER_H
+#ifndef CVC5__THEORY__FP__FP_CONVERTER_H
+#define CVC5__THEORY__FP__FP_CONVERTER_H
#include "context/cdhashmap.h"
#include "context/cdlist.h"
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__FP__THEORY_FP_H */
+#endif /* CVC5__THEORY__FP__THEORY_FP_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__FP__THEORY_FP_H
-#define CVC4__THEORY__FP__THEORY_FP_H
+#ifndef CVC5__THEORY__FP__THEORY_FP_H
+#define CVC5__THEORY__FP__THEORY_FP_H
#include <string>
#include <utility>
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__FP__THEORY_FP_H */
+#endif /* CVC5__THEORY__FP__THEORY_FP_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__FP__THEORY_FP_REWRITER_H
-#define CVC4__THEORY__FP__THEORY_FP_REWRITER_H
+#ifndef CVC5__THEORY__FP__THEORY_FP_REWRITER_H
+#define CVC5__THEORY__FP__THEORY_FP_REWRITER_H
#include "theory/theory_rewriter.h"
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__FP__THEORY_FP_REWRITER_H */
+#endif /* CVC5__THEORY__FP__THEORY_FP_REWRITER_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__FP__THEORY_FP_TYPE_RULES_H
-#define CVC4__THEORY__FP__THEORY_FP_TYPE_RULES_H
+#ifndef CVC5__THEORY__FP__THEORY_FP_TYPE_RULES_H
+#define CVC5__THEORY__FP__THEORY_FP_TYPE_RULES_H
#include "expr/node.h"
#include "expr/type_node.h"
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__FP__TYPE_ENUMERATOR_H
-#define CVC4__THEORY__FP__TYPE_ENUMERATOR_H
+#ifndef CVC5__THEORY__FP__TYPE_ENUMERATOR_H
+#define CVC5__THEORY__FP__TYPE_ENUMERATOR_H
#include "expr/kind.h"
#include "expr/type_node.h"
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__FP__TYPE_ENUMERATOR_H */
+#endif /* CVC5__THEORY__FP__TYPE_ENUMERATOR_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__INCOMPLETE_ID_H
-#define CVC4__THEORY__INCOMPLETE_ID_H
+#ifndef CVC5__THEORY__INCOMPLETE_ID_H
+#define CVC5__THEORY__INCOMPLETE_ID_H
#include <iosfwd>
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__INCOMPLETE_ID_H */
+#endif /* CVC5__THEORY__INCOMPLETE_ID_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__INFERENCE_ID_H
-#define CVC4__THEORY__INFERENCE_ID_H
+#ifndef CVC5__THEORY__INFERENCE_ID_H
+#define CVC5__THEORY__INFERENCE_ID_H
#include <iosfwd>
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__INFERENCE_H */
+#endif /* CVC5__THEORY__INFERENCE_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__INFERENCE_MANAGER_BUFFERED_H
-#define CVC4__THEORY__INFERENCE_MANAGER_BUFFERED_H
+#ifndef CVC5__THEORY__INFERENCE_MANAGER_BUFFERED_H
+#define CVC5__THEORY__INFERENCE_MANAGER_BUFFERED_H
#include "expr/node.h"
#include "theory/theory_inference.h"
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__INTERRUPTED_H
-#define CVC4__THEORY__INTERRUPTED_H
+#ifndef CVC5__THEORY__INTERRUPTED_H
+#define CVC5__THEORY__INTERRUPTED_H
#include "base/exception.h"
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__INTERRUPTED_H */
+#endif /* CVC5__THEORY__INTERRUPTED_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__LAZY_TREE_PROOF_GENERATOR_H
-#define CVC4__THEORY__LAZY_TREE_PROOF_GENERATOR_H
+#ifndef CVC5__THEORY__LAZY_TREE_PROOF_GENERATOR_H
+#define CVC5__THEORY__LAZY_TREE_PROOF_GENERATOR_H
#include <iostream>
#include "cvc4_public.h"
-#ifndef CVC4__LOGIC_INFO_H
-#define CVC4__LOGIC_INFO_H
+#ifndef CVC5__LOGIC_INFO_H
+#define CVC5__LOGIC_INFO_H
#include <string>
#include <vector>
} // namespace cvc5
-#endif /* CVC4__LOGIC_INFO_H */
+#endif /* CVC5__LOGIC_INFO_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__MODEL_MANAGER__H
-#define CVC4__THEORY__MODEL_MANAGER__H
+#ifndef CVC5__THEORY__MODEL_MANAGER__H
+#define CVC5__THEORY__MODEL_MANAGER__H
#include <memory>
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__MODEL_MANAGER__H */
+#endif /* CVC5__THEORY__MODEL_MANAGER__H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__MODEL_MANAGER_DISTRIBUTED__H
-#define CVC4__THEORY__MODEL_MANAGER_DISTRIBUTED__H
+#ifndef CVC5__THEORY__MODEL_MANAGER_DISTRIBUTED__H
+#define CVC5__THEORY__MODEL_MANAGER_DISTRIBUTED__H
#include "theory/ee_manager.h"
#include "theory/model_manager.h"
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__MODEL_MANAGER_DISTRIBUTED__H */
+#endif /* CVC5__THEORY__MODEL_MANAGER_DISTRIBUTED__H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__OUTPUT_CHANNEL_H
-#define CVC4__THEORY__OUTPUT_CHANNEL_H
+#ifndef CVC5__THEORY__OUTPUT_CHANNEL_H
+#define CVC5__THEORY__OUTPUT_CHANNEL_H
#include "theory/incomplete_id.h"
#include "theory/trust_node.h"
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__OUTPUT_CHANNEL_H */
+#endif /* CVC5__THEORY__OUTPUT_CHANNEL_H */
#include "cvc4_private.h"
-#ifndef CVC4__ALPHA_EQUIVALENCE_H
-#define CVC4__ALPHA_EQUIVALENCE_H
+#ifndef CVC5__ALPHA_EQUIVALENCE_H
+#define CVC5__ALPHA_EQUIVALENCE_H
#include "theory/quantifiers/quant_util.h"
#include "cvc4_private.h"
-#ifndef CVC4__BV_INVERTER_H
-#define CVC4__BV_INVERTER_H
+#ifndef CVC5__BV_INVERTER_H
+#define CVC5__BV_INVERTER_H
#include <map>
#include <unordered_map>
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__BV_INVERTER_H */
+#endif /* CVC5__BV_INVERTER_H */
#include "cvc4_private.h"
-#ifndef CVC4__BV_INVERTER_UTILS_H
-#define CVC4__BV_INVERTER_UTILS_H
+#ifndef CVC5__BV_INVERTER_UTILS_H
+#define CVC5__BV_INVERTER_UTILS_H
#include "expr/node.h"
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__QUANTIFIERS__CANDIDATE_REWRITE_DATABASE_H
-#define CVC4__THEORY__QUANTIFIERS__CANDIDATE_REWRITE_DATABASE_H
+#ifndef CVC5__THEORY__QUANTIFIERS__CANDIDATE_REWRITE_DATABASE_H
+#define CVC5__THEORY__QUANTIFIERS__CANDIDATE_REWRITE_DATABASE_H
#include <vector>
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__QUANTIFIERS__CANDIDATE_REWRITE_DATABASE_H */
+#endif /* CVC5__THEORY__QUANTIFIERS__CANDIDATE_REWRITE_DATABASE_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__QUANTIFIERS__CANDIDATE_REWRITE_FILTER_H
-#define CVC4__THEORY__QUANTIFIERS__CANDIDATE_REWRITE_FILTER_H
+#ifndef CVC5__THEORY__QUANTIFIERS__CANDIDATE_REWRITE_FILTER_H
+#define CVC5__THEORY__QUANTIFIERS__CANDIDATE_REWRITE_FILTER_H
#include <map>
#include "expr/match_trie.h"
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__QUANTIFIERS__CANDIDATE_REWRITE_FILTER_H */
+#endif /* CVC5__THEORY__QUANTIFIERS__CANDIDATE_REWRITE_FILTER_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__QUANTIFIERS__CEG_ARITH_INSTANTIATOR_H
-#define CVC4__THEORY__QUANTIFIERS__CEG_ARITH_INSTANTIATOR_H
+#ifndef CVC5__THEORY__QUANTIFIERS__CEG_ARITH_INSTANTIATOR_H
+#define CVC5__THEORY__QUANTIFIERS__CEG_ARITH_INSTANTIATOR_H
#include <vector>
#include "expr/node.h"
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__QUANTIFIERS__CEG_ARITH_INSTANTIATOR_H */
+#endif /* CVC5__THEORY__QUANTIFIERS__CEG_ARITH_INSTANTIATOR_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__QUANTIFIERS__CEG_BV_INSTANTIATOR_H
-#define CVC4__THEORY__QUANTIFIERS__CEG_BV_INSTANTIATOR_H
+#ifndef CVC5__THEORY__QUANTIFIERS__CEG_BV_INSTANTIATOR_H
+#define CVC5__THEORY__QUANTIFIERS__CEG_BV_INSTANTIATOR_H
#include <unordered_map>
#include "theory/quantifiers/bv_inverter.h"
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__QUANTIFIERS__CEG_BV_INSTANTIATOR_H */
+#endif /* CVC5__THEORY__QUANTIFIERS__CEG_BV_INSTANTIATOR_H */
#include "cvc4_private.h"
-#ifndef CVC4__BV_INSTANTIATOR_UTILS_H
-#define CVC4__BV_INSTANTIATOR_UTILS_H
+#ifndef CVC5__BV_INSTANTIATOR_UTILS_H
+#define CVC5__BV_INSTANTIATOR_UTILS_H
#include "expr/attribute.h"
#include "expr/node.h"
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__QUANTIFIERS__CEG_DT_INSTANTIATOR_H
-#define CVC4__THEORY__QUANTIFIERS__CEG_DT_INSTANTIATOR_H
+#ifndef CVC5__THEORY__QUANTIFIERS__CEG_DT_INSTANTIATOR_H
+#define CVC5__THEORY__QUANTIFIERS__CEG_DT_INSTANTIATOR_H
#include "expr/node.h"
#include "theory/quantifiers/cegqi/ceg_instantiator.h"
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__QUANTIFIERS__CEG_DT_INSTANTIATOR_H */
+#endif /* CVC5__THEORY__QUANTIFIERS__CEG_DT_INSTANTIATOR_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__QUANTIFIERS__CEG_INSTANTIATOR_H
-#define CVC4__THEORY__QUANTIFIERS__CEG_INSTANTIATOR_H
+#ifndef CVC5__THEORY__QUANTIFIERS__CEG_INSTANTIATOR_H
+#define CVC5__THEORY__QUANTIFIERS__CEG_INSTANTIATOR_H
#include <vector>
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__QUANTIFIERS__INST_STRATEGY_CEGQI_H
-#define CVC4__THEORY__QUANTIFIERS__INST_STRATEGY_CEGQI_H
+#ifndef CVC5__THEORY__QUANTIFIERS__INST_STRATEGY_CEGQI_H
+#define CVC5__THEORY__QUANTIFIERS__INST_STRATEGY_CEGQI_H
#include "theory/decision_manager.h"
#include "theory/quantifiers/bv_inverter.h"
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__QUANTIFIERS__CEQGI__NESTED_QE_H
-#define CVC4__THEORY__QUANTIFIERS__CEQGI__NESTED_QE_H
+#ifndef CVC5__THEORY__QUANTIFIERS__CEQGI__NESTED_QE_H
+#define CVC5__THEORY__QUANTIFIERS__CEQGI__NESTED_QE_H
#include <unordered_set>
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__QUANTIFIERS__CEGQI__VTS_TERM_CACHE_H
-#define CVC4__THEORY__QUANTIFIERS__CEGQI__VTS_TERM_CACHE_H
+#ifndef CVC5__THEORY__QUANTIFIERS__CEGQI__VTS_TERM_CACHE_H
+#define CVC5__THEORY__QUANTIFIERS__CEGQI__VTS_TERM_CACHE_H
#include <map>
#include "expr/attribute.h"
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__QUANTIFIERS__CEGQI__VTS_TERM_CACHE_H */
+#endif /* CVC5__THEORY__QUANTIFIERS__CEGQI__VTS_TERM_CACHE_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__QUANTIFIERS__DYNAMIC_REWRITER_H
-#define CVC4__THEORY__QUANTIFIERS__DYNAMIC_REWRITER_H
+#ifndef CVC5__THEORY__QUANTIFIERS__DYNAMIC_REWRITER_H
+#define CVC5__THEORY__QUANTIFIERS__DYNAMIC_REWRITER_H
#include <map>
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__QUANTIFIERS__DYNAMIC_REWRITER_H */
+#endif /* CVC5__THEORY__QUANTIFIERS__DYNAMIC_REWRITER_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__QUANTIFIERS__CANDIDATE_GENERATOR_H
-#define CVC4__THEORY__QUANTIFIERS__CANDIDATE_GENERATOR_H
+#ifndef CVC5__THEORY__QUANTIFIERS__CANDIDATE_GENERATOR_H
+#define CVC5__THEORY__QUANTIFIERS__CANDIDATE_GENERATOR_H
#include "theory/theory.h"
#include "theory/uf/equality_engine.h"
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__QUANTIFIERS__CANDIDATE_GENERATOR_H */
+#endif /* CVC5__THEORY__QUANTIFIERS__CANDIDATE_GENERATOR_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__QUANTIFIERS__HO_TRIGGER_H
-#define CVC4__THEORY__QUANTIFIERS__HO_TRIGGER_H
+#ifndef CVC5__THEORY__QUANTIFIERS__HO_TRIGGER_H
+#define CVC5__THEORY__QUANTIFIERS__HO_TRIGGER_H
#include <map>
#include <unordered_set>
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__QUANTIFIERS__HO_TRIGGER_H */
+#endif /* CVC5__THEORY__QUANTIFIERS__HO_TRIGGER_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__QUANTIFIERS__IM_GENERATOR_H
-#define CVC4__THEORY__QUANTIFIERS__IM_GENERATOR_H
+#ifndef CVC5__THEORY__QUANTIFIERS__IM_GENERATOR_H
+#define CVC5__THEORY__QUANTIFIERS__IM_GENERATOR_H
#include <map>
#include "expr/node.h"
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__QUANTIFIERS__INST_MATCH_GENERATOR_H
-#define CVC4__THEORY__QUANTIFIERS__INST_MATCH_GENERATOR_H
+#ifndef CVC5__THEORY__QUANTIFIERS__INST_MATCH_GENERATOR_H
+#define CVC5__THEORY__QUANTIFIERS__INST_MATCH_GENERATOR_H
#include <map>
#include "expr/node.h"
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__QUANTIFIERS__INST_MATCH_GENERATOR_MULTI_H
-#define CVC4__THEORY__QUANTIFIERS__INST_MATCH_GENERATOR_MULTI_H
+#ifndef CVC5__THEORY__QUANTIFIERS__INST_MATCH_GENERATOR_MULTI_H
+#define CVC5__THEORY__QUANTIFIERS__INST_MATCH_GENERATOR_MULTI_H
#include <map>
#include <vector>
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__QUANTIFIERS__INST_MATCH_GENERATOR_MULTI_LINEAR_H
-#define CVC4__THEORY__QUANTIFIERS__INST_MATCH_GENERATOR_MULTI_LINEAR_H
+#ifndef CVC5__THEORY__QUANTIFIERS__INST_MATCH_GENERATOR_MULTI_LINEAR_H
+#define CVC5__THEORY__QUANTIFIERS__INST_MATCH_GENERATOR_MULTI_LINEAR_H
#include <vector>
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__QUANTIFIERS__INST_MATCH_GENERATOR_SIMPLE_H
-#define CVC4__THEORY__QUANTIFIERS__INST_MATCH_GENERATOR_SIMPLE_H
+#ifndef CVC5__THEORY__QUANTIFIERS__INST_MATCH_GENERATOR_SIMPLE_H
+#define CVC5__THEORY__QUANTIFIERS__INST_MATCH_GENERATOR_SIMPLE_H
#include <map>
#include <vector>
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__QUANTIFIERS__INST_STRATEGY_H
-#define CVC4__THEORY__QUANTIFIERS__INST_STRATEGY_H
+#ifndef CVC5__THEORY__QUANTIFIERS__INST_STRATEGY_H
+#define CVC5__THEORY__QUANTIFIERS__INST_STRATEGY_H
#include <vector>
#include "expr/node.h"
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__QUANTIFIERS__INSTANTIATION_ENGINE_H */
+#endif /* CVC5__THEORY__QUANTIFIERS__INSTANTIATION_ENGINE_H */
#include "cvc4_private.h"
-#ifndef CVC4__INST_STRATEGY_E_MATCHING_H
-#define CVC4__INST_STRATEGY_E_MATCHING_H
+#ifndef CVC5__INST_STRATEGY_E_MATCHING_H
+#define CVC5__INST_STRATEGY_E_MATCHING_H
#include "theory/quantifiers/ematching/inst_strategy.h"
#include "theory/quantifiers/ematching/trigger.h"
#include "cvc4_private.h"
-#ifndef CVC4__INST_STRATEGY_E_MATCHING_USER_H
-#define CVC4__INST_STRATEGY_E_MATCHING_USER_H
+#ifndef CVC5__INST_STRATEGY_E_MATCHING_USER_H
+#define CVC5__INST_STRATEGY_E_MATCHING_USER_H
#include <map>
#include "expr/node.h"
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__QUANTIFIERS__INSTANTIATION_ENGINE_H
-#define CVC4__THEORY__QUANTIFIERS__INSTANTIATION_ENGINE_H
+#ifndef CVC5__THEORY__QUANTIFIERS__INSTANTIATION_ENGINE_H
+#define CVC5__THEORY__QUANTIFIERS__INSTANTIATION_ENGINE_H
#include <vector>
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__QUANTIFIERS__INSTANTIATION_ENGINE_H */
+#endif /* CVC5__THEORY__QUANTIFIERS__INSTANTIATION_ENGINE_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__QUANTIFIERS__PATTERN_TERM_SELECTOR_H
-#define CVC4__THEORY__QUANTIFIERS__PATTERN_TERM_SELECTOR_H
+#ifndef CVC5__THEORY__QUANTIFIERS__PATTERN_TERM_SELECTOR_H
+#define CVC5__THEORY__QUANTIFIERS__PATTERN_TERM_SELECTOR_H
#include <map>
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__QUANTIFIERS__TRIGGER_H
-#define CVC4__THEORY__QUANTIFIERS__TRIGGER_H
+#ifndef CVC5__THEORY__QUANTIFIERS__TRIGGER_H
+#define CVC5__THEORY__QUANTIFIERS__TRIGGER_H
#include "expr/node.h"
#include "theory/inference_id.h"
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__QUANTIFIERS__TRIGGER_H */
+#endif /* CVC5__THEORY__QUANTIFIERS__TRIGGER_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__QUANTIFIERS__TRIGGER_DATABASE_H
-#define CVC4__THEORY__QUANTIFIERS__TRIGGER_DATABASE_H
+#ifndef CVC5__THEORY__QUANTIFIERS__TRIGGER_DATABASE_H
+#define CVC5__THEORY__QUANTIFIERS__TRIGGER_DATABASE_H
#include <vector>
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__QUANTIFIERS__TRIGGER_DATABASE_H */
+#endif /* CVC5__THEORY__QUANTIFIERS__TRIGGER_DATABASE_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__QUANTIFIERS__TRIGGER_TERM_INFO_H
-#define CVC4__THEORY__QUANTIFIERS__TRIGGER_TERM_INFO_H
+#ifndef CVC5__THEORY__QUANTIFIERS__TRIGGER_TERM_INFO_H
+#define CVC5__THEORY__QUANTIFIERS__TRIGGER_TERM_INFO_H
#include <map>
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__QUANTIFIERS__TRIGGER_TRIE_H
-#define CVC4__THEORY__QUANTIFIERS__TRIGGER_TRIE_H
+#ifndef CVC5__THEORY__QUANTIFIERS__TRIGGER_TRIE_H
+#define CVC5__THEORY__QUANTIFIERS__TRIGGER_TRIE_H
#include <vector>
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__QUANTIFIERS__TRIGGER_TRIE_H */
+#endif /* CVC5__THEORY__QUANTIFIERS__TRIGGER_TRIE_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__QUANTIFIERS__VAR_MATCH_GENERATOR_H
-#define CVC4__THEORY__QUANTIFIERS__VAR_MATCH_GENERATOR_H
+#ifndef CVC5__THEORY__QUANTIFIERS__VAR_MATCH_GENERATOR_H
+#define CVC5__THEORY__QUANTIFIERS__VAR_MATCH_GENERATOR_H
#include "expr/node.h"
#include "theory/quantifiers/ematching/inst_match_generator.h"
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__QUANTIFIERS_EQUALITY_QUERY_H
-#define CVC4__THEORY__QUANTIFIERS_EQUALITY_QUERY_H
+#ifndef CVC5__THEORY__QUANTIFIERS_EQUALITY_QUERY_H
+#define CVC5__THEORY__QUANTIFIERS_EQUALITY_QUERY_H
#include "context/cdo.h"
#include "context/context.h"
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__QUANTIFIERS_EQUALITY_QUERY_H */
+#endif /* CVC5__THEORY__QUANTIFIERS_EQUALITY_QUERY_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__QUANTIFIERS__EXPRESSION_MINER_H
-#define CVC4__THEORY__QUANTIFIERS__EXPRESSION_MINER_H
+#ifndef CVC5__THEORY__QUANTIFIERS__EXPRESSION_MINER_H
+#define CVC5__THEORY__QUANTIFIERS__EXPRESSION_MINER_H
#include <map>
#include <memory>
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__QUANTIFIERS__EXPRESSION_MINER_H */
+#endif /* CVC5__THEORY__QUANTIFIERS__EXPRESSION_MINER_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__QUANTIFIERS__EXPR_MINER_MANAGER_H
-#define CVC4__THEORY__QUANTIFIERS__EXPR_MINER_MANAGER_H
+#ifndef CVC5__THEORY__QUANTIFIERS__EXPR_MINER_MANAGER_H
+#define CVC5__THEORY__QUANTIFIERS__EXPR_MINER_MANAGER_H
#include "expr/node.h"
#include "theory/quantifiers/candidate_rewrite_database.h"
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__QUANTIFIERS__EXPR_MINER_MANAGER_H */
+#endif /* CVC5__THEORY__QUANTIFIERS__EXPR_MINER_MANAGER_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__QUANTIFIERS__EXTENDED_REWRITE_H
-#define CVC4__THEORY__QUANTIFIERS__EXTENDED_REWRITE_H
+#ifndef CVC5__THEORY__QUANTIFIERS__EXTENDED_REWRITE_H
+#define CVC5__THEORY__QUANTIFIERS__EXTENDED_REWRITE_H
#include <unordered_map>
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__QUANTIFIERS__EXTENDED_REWRITE_H */
+#endif /* CVC5__THEORY__QUANTIFIERS__EXTENDED_REWRITE_H */
#include "cvc4_private.h"
-#ifndef CVC4__FIRST_ORDER_MODEL_H
-#define CVC4__FIRST_ORDER_MODEL_H
+#ifndef CVC5__FIRST_ORDER_MODEL_H
+#define CVC5__FIRST_ORDER_MODEL_H
#include "context/cdlist.h"
#include "theory/quantifiers/equality_query.h"
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__FIRST_ORDER_MODEL_H */
+#endif /* CVC5__FIRST_ORDER_MODEL_H */
#include "cvc4_private.h"
-#ifndef CVC4__BOUNDED_INTEGERS_H
-#define CVC4__BOUNDED_INTEGERS_H
+#ifndef CVC5__BOUNDED_INTEGERS_H
+#define CVC5__BOUNDED_INTEGERS_H
#include "theory/quantifiers/quant_module.h"
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__QUANTIFIERS__FMF__FIRST_ORDER_MODEL_FMC_H
-#define CVC4__THEORY__QUANTIFIERS__FMF__FIRST_ORDER_MODEL_FMC_H
+#ifndef CVC5__THEORY__QUANTIFIERS__FMF__FIRST_ORDER_MODEL_FMC_H
+#define CVC5__THEORY__QUANTIFIERS__FMF__FIRST_ORDER_MODEL_FMC_H
#include "theory/quantifiers/first_order_model.h"
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__FIRST_ORDER_MODEL_H */
+#endif /* CVC5__FIRST_ORDER_MODEL_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__QUANTIFIERS__FULL_MODEL_CHECK_H
-#define CVC4__THEORY__QUANTIFIERS__FULL_MODEL_CHECK_H
+#ifndef CVC5__THEORY__QUANTIFIERS__FULL_MODEL_CHECK_H
+#define CVC5__THEORY__QUANTIFIERS__FULL_MODEL_CHECK_H
#include "theory/quantifiers/fmf/first_order_model_fmc.h"
#include "theory/quantifiers/fmf/model_builder.h"
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__QUANTIFIERS__FULL_MODEL_CHECK_H */
+#endif /* CVC5__THEORY__QUANTIFIERS__FULL_MODEL_CHECK_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__QUANTIFIERS__MODEL_BUILDER_H
-#define CVC4__THEORY__QUANTIFIERS__MODEL_BUILDER_H
+#ifndef CVC5__THEORY__QUANTIFIERS__MODEL_BUILDER_H
+#define CVC5__THEORY__QUANTIFIERS__MODEL_BUILDER_H
#include "expr/node.h"
#include "theory/quantifiers/inst_match.h"
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__QUANTIFIERS__MODEL_BUILDER_H */
+#endif /* CVC5__THEORY__QUANTIFIERS__MODEL_BUILDER_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__QUANTIFIERS__MODEL_ENGINE_H
-#define CVC4__THEORY__QUANTIFIERS__MODEL_ENGINE_H
+#ifndef CVC5__THEORY__QUANTIFIERS__MODEL_ENGINE_H
+#define CVC5__THEORY__QUANTIFIERS__MODEL_ENGINE_H
#include "theory/quantifiers/fmf/model_builder.h"
#include "theory/quantifiers/quant_module.h"
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__QUANTIFIERS__MODEL_ENGINE_H */
+#endif /* CVC5__THEORY__QUANTIFIERS__MODEL_ENGINE_H */
#include "cvc4_private.h"
-#ifndef CVC4__QUANTIFIERS_FUN_DEF_EVALUATOR_H
-#define CVC4__QUANTIFIERS_FUN_DEF_EVALUATOR_H
+#ifndef CVC5__QUANTIFIERS_FUN_DEF_EVALUATOR_H
+#define CVC5__QUANTIFIERS_FUN_DEF_EVALUATOR_H
#include <map>
#include <vector>
** that are not yielding useful instantiations. of quantifier instantiation.
** This is used in the term_tuple_enumerator.
**/
-#ifndef CVC4__THEORY__QUANTIFIERS__INDEX_TRIE_H
-#define CVC4__THEORY__QUANTIFIERS__INDEX_TRIE_H
+#ifndef CVC5__THEORY__QUANTIFIERS__INDEX_TRIE_H
+#define CVC5__THEORY__QUANTIFIERS__INDEX_TRIE_H
#include <algorithm>
#include <utility>
#include <vector>
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__QUANTIFIERS__INST_MATCH_H
-#define CVC4__THEORY__QUANTIFIERS__INST_MATCH_H
+#ifndef CVC5__THEORY__QUANTIFIERS__INST_MATCH_H
+#define CVC5__THEORY__QUANTIFIERS__INST_MATCH_H
#include <vector>
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__QUANTIFIERS__INST_MATCH_H */
+#endif /* CVC5__THEORY__QUANTIFIERS__INST_MATCH_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__QUANTIFIERS__INST_MATCH_TRIE_H
-#define CVC4__THEORY__QUANTIFIERS__INST_MATCH_TRIE_H
+#ifndef CVC5__THEORY__QUANTIFIERS__INST_MATCH_TRIE_H
+#define CVC5__THEORY__QUANTIFIERS__INST_MATCH_TRIE_H
#include <map>
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__QUANTIFIERS__INST_MATCH_TRIE_H */
+#endif /* CVC5__THEORY__QUANTIFIERS__INST_MATCH_TRIE_H */
#include "cvc4_private.h"
-#ifndef CVC4__INST_STRATEGY_ENUMERATIVE_H
-#define CVC4__INST_STRATEGY_ENUMERATIVE_H
+#ifndef CVC5__INST_STRATEGY_ENUMERATIVE_H
+#define CVC5__INST_STRATEGY_ENUMERATIVE_H
#include "theory/quantifiers/quant_module.h"
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__QUANTIFIERS__INSTANTIATE_H
-#define CVC4__THEORY__QUANTIFIERS__INSTANTIATE_H
+#ifndef CVC5__THEORY__QUANTIFIERS__INSTANTIATE_H
+#define CVC5__THEORY__QUANTIFIERS__INSTANTIATE_H
#include <map>
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__QUANTIFIERS__INSTANTIATE_H */
+#endif /* CVC5__THEORY__QUANTIFIERS__INSTANTIATE_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__QUANTIFIERS__INSTANTIATION_LIST_H
-#define CVC4__THEORY__QUANTIFIERS__INSTANTIATION_LIST_H
+#ifndef CVC5__THEORY__QUANTIFIERS__INSTANTIATION_LIST_H
+#define CVC5__THEORY__QUANTIFIERS__INSTANTIATION_LIST_H
#include <iosfwd>
#include <vector>
} // namespace cvc5
-#endif /* CVC4__THEORY__QUANTIFIERS__INSTANTIATION_LIST_H */
+#endif /* CVC5__THEORY__QUANTIFIERS__INSTANTIATION_LIST_H */
** \brief lazy trie
**/
-#ifndef CVC4__THEORY__QUANTIFIERS__LAZY_TRIE_H
-#define CVC4__THEORY__QUANTIFIERS__LAZY_TRIE_H
+#ifndef CVC5__THEORY__QUANTIFIERS__LAZY_TRIE_H
+#define CVC5__THEORY__QUANTIFIERS__LAZY_TRIE_H
#include "expr/node.h"
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__QUANTIFIERS__LAZY_TRIE_H */
+#endif /* CVC5__THEORY__QUANTIFIERS__LAZY_TRIE_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__QUANTIFIERS__PROOF_CHECKER_H
-#define CVC4__THEORY__QUANTIFIERS__PROOF_CHECKER_H
+#ifndef CVC5__THEORY__QUANTIFIERS__PROOF_CHECKER_H
+#define CVC5__THEORY__QUANTIFIERS__PROOF_CHECKER_H
#include "expr/node.h"
#include "expr/proof_checker.h"
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__QUANTIFIERS__PROOF_CHECKER_H */
+#endif /* CVC5__THEORY__QUANTIFIERS__PROOF_CHECKER_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__QUANTIFIERS__QUANT_BOUND_INFERENCE_H
-#define CVC4__THEORY__QUANTIFIERS__QUANT_BOUND_INFERENCE_H
+#ifndef CVC5__THEORY__QUANTIFIERS__QUANT_BOUND_INFERENCE_H
+#define CVC5__THEORY__QUANTIFIERS__QUANT_BOUND_INFERENCE_H
#include <vector>
#include "expr/node.h"
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__QUANTIFIERS__QUANT_BOUND_INFERENCE_H */
+#endif /* CVC5__THEORY__QUANTIFIERS__QUANT_BOUND_INFERENCE_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__QUANT_MODULE_H
-#define CVC4__THEORY__QUANT_MODULE_H
+#ifndef CVC5__THEORY__QUANT_MODULE_H
+#define CVC5__THEORY__QUANT_MODULE_H
#include <iostream>
#include <map>
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__QUANT_UTIL_H */
+#endif /* CVC5__THEORY__QUANT_UTIL_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__QUANT_RELEVANCE_H
-#define CVC4__THEORY__QUANT_RELEVANCE_H
+#ifndef CVC5__THEORY__QUANT_RELEVANCE_H
+#define CVC5__THEORY__QUANT_RELEVANCE_H
#include <map>
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__QUANT_RELEVANCE_H */
+#endif /* CVC5__THEORY__QUANT_RELEVANCE_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__QUANTIFIERS__QUANT_REP_BOUND_EXT_H
-#define CVC4__THEORY__QUANTIFIERS__QUANT_REP_BOUND_EXT_H
+#ifndef CVC5__THEORY__QUANTIFIERS__QUANT_REP_BOUND_EXT_H
+#define CVC5__THEORY__QUANTIFIERS__QUANT_REP_BOUND_EXT_H
#include <map>
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__FIRST_ORDER_MODEL_H */
+#endif /* CVC5__FIRST_ORDER_MODEL_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__QUANT_SPLIT_H
-#define CVC4__THEORY__QUANT_SPLIT_H
+#ifndef CVC5__THEORY__QUANT_SPLIT_H
+#define CVC5__THEORY__QUANT_SPLIT_H
#include "context/cdo.h"
#include "theory/quantifiers/quant_module.h"
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__QUANT_UTIL_H
-#define CVC4__THEORY__QUANT_UTIL_H
+#ifndef CVC5__THEORY__QUANT_UTIL_H
+#define CVC5__THEORY__QUANT_UTIL_H
#include <iostream>
#include <map>
}
} // namespace cvc5
-#endif /* CVC4__THEORY__QUANT_UTIL_H */
+#endif /* CVC5__THEORY__QUANT_UTIL_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_ATTRIBUTES_H
-#define CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_ATTRIBUTES_H
+#ifndef CVC5__THEORY__QUANTIFIERS__QUANTIFIERS_ATTRIBUTES_H
+#define CVC5__THEORY__QUANTIFIERS__QUANTIFIERS_ATTRIBUTES_H
#include "expr/attribute.h"
#include "expr/node.h"
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_INFERENCE_MANAGER_H
-#define CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_INFERENCE_MANAGER_H
+#ifndef CVC5__THEORY__QUANTIFIERS__QUANTIFIERS_INFERENCE_MANAGER_H
+#define CVC5__THEORY__QUANTIFIERS__QUANTIFIERS_INFERENCE_MANAGER_H
#include "theory/inference_manager_buffered.h"
#include "theory/quantifiers/quantifiers_state.h"
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_INFERENCE_MANAGER_H */
+#endif /* CVC5__THEORY__QUANTIFIERS__QUANTIFIERS_INFERENCE_MANAGER_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_MODULES_H
-#define CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_MODULES_H
+#ifndef CVC5__THEORY__QUANTIFIERS__QUANTIFIERS_MODULES_H
+#define CVC5__THEORY__QUANTIFIERS__QUANTIFIERS_MODULES_H
#include "theory/quantifiers/alpha_equivalence.h"
#include "theory/quantifiers/conjecture_generator.h"
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_MODULES_H */
+#endif /* CVC5__THEORY__QUANTIFIERS__QUANTIFIERS_MODULES_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_REGISTRY_H
-#define CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_REGISTRY_H
+#ifndef CVC5__THEORY__QUANTIFIERS__QUANTIFIERS_REGISTRY_H
+#define CVC5__THEORY__QUANTIFIERS__QUANTIFIERS_REGISTRY_H
#include "expr/node.h"
#include "theory/quantifiers/quant_bound_inference.h"
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_REGISTRY_H */
+#endif /* CVC5__THEORY__QUANTIFIERS__QUANTIFIERS_REGISTRY_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_REWRITER_H
-#define CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_REWRITER_H
+#ifndef CVC5__THEORY__QUANTIFIERS__QUANTIFIERS_REWRITER_H
+#define CVC5__THEORY__QUANTIFIERS__QUANTIFIERS_REWRITER_H
#include "theory/theory_rewriter.h"
#include "theory/trust_node.h"
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_REWRITER_H */
+#endif /* CVC5__THEORY__QUANTIFIERS__QUANTIFIERS_REWRITER_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_STATE_H
-#define CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_STATE_H
+#ifndef CVC5__THEORY__QUANTIFIERS__QUANTIFIERS_STATE_H
+#define CVC5__THEORY__QUANTIFIERS__QUANTIFIERS_STATE_H
#include "theory/quantifiers/quantifiers_statistics.h"
#include "theory/theory.h"
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_STATE_H */
+#endif /* CVC5__THEORY__QUANTIFIERS__QUANTIFIERS_STATE_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_STATISTICS_H
-#define CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_STATISTICS_H
+#ifndef CVC5__THEORY__QUANTIFIERS__QUANTIFIERS_STATISTICS_H
+#define CVC5__THEORY__QUANTIFIERS__QUANTIFIERS_STATISTICS_H
#include "util/statistics_registry.h"
#include "util/stats_timer.h"
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_STATISTICS_H */
+#endif /* CVC5__THEORY__QUANTIFIERS__QUANTIFIERS_STATISTICS_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__QUANTIFIERS__QUERY_GENERATOR_H
-#define CVC4__THEORY__QUANTIFIERS__QUERY_GENERATOR_H
+#ifndef CVC5__THEORY__QUANTIFIERS__QUERY_GENERATOR_H
+#define CVC5__THEORY__QUANTIFIERS__QUERY_GENERATOR_H
#include <map>
#include <unordered_set>
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__QUANTIFIERS___H */
+#endif /* CVC5__THEORY__QUANTIFIERS___H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__QUANTIFIERS__RELEVANT_DOMAIN_H
-#define CVC4__THEORY__QUANTIFIERS__RELEVANT_DOMAIN_H
+#ifndef CVC5__THEORY__QUANTIFIERS__RELEVANT_DOMAIN_H
+#define CVC5__THEORY__QUANTIFIERS__RELEVANT_DOMAIN_H
#include "theory/quantifiers/first_order_model.h"
#include "theory/quantifiers/quant_util.h"
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__QUANTIFIERS__RELEVANT_DOMAIN_H */
+#endif /* CVC5__THEORY__QUANTIFIERS__RELEVANT_DOMAIN_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__QUANTIFIERS__SINGLE_INV_PARTITION_H
-#define CVC4__THEORY__QUANTIFIERS__SINGLE_INV_PARTITION_H
+#ifndef CVC5__THEORY__QUANTIFIERS__SINGLE_INV_PARTITION_H
+#define CVC5__THEORY__QUANTIFIERS__SINGLE_INV_PARTITION_H
#include <map>
#include <vector>
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__QUANTIFIERS__SINGLE_INV_PARTITION_H */
+#endif /* CVC5__THEORY__QUANTIFIERS__SINGLE_INV_PARTITION_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__QUANTIFIERS__SKOLEMIZE_H
-#define CVC4__THEORY__QUANTIFIERS__SKOLEMIZE_H
+#ifndef CVC5__THEORY__QUANTIFIERS__SKOLEMIZE_H
+#define CVC5__THEORY__QUANTIFIERS__SKOLEMIZE_H
#include <unordered_map>
#include <unordered_set>
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__QUANTIFIERS__SKOLEMIZE_H */
+#endif /* CVC5__THEORY__QUANTIFIERS__SKOLEMIZE_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__QUANTIFIERS__SOLUTION_FILTER_H
-#define CVC4__THEORY__QUANTIFIERS__SOLUTION_FILTER_H
+#ifndef CVC5__THEORY__QUANTIFIERS__SOLUTION_FILTER_H
+#define CVC5__THEORY__QUANTIFIERS__SOLUTION_FILTER_H
#include <map>
#include <unordered_set>
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__QUANTIFIERS__SOLUTION_FILTER_H */
+#endif /* CVC5__THEORY__QUANTIFIERS__SOLUTION_FILTER_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__QUANTIFIERS__CE_GUIDED_SINGLE_INV_H
-#define CVC4__THEORY__QUANTIFIERS__CE_GUIDED_SINGLE_INV_H
+#ifndef CVC5__THEORY__QUANTIFIERS__CE_GUIDED_SINGLE_INV_H
+#define CVC5__THEORY__QUANTIFIERS__CE_GUIDED_SINGLE_INV_H
#include "context/cdlist.h"
#include "expr/subs.h"
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__QUANTIFIERS__CEGIS_H
-#define CVC4__THEORY__QUANTIFIERS__CEGIS_H
+#ifndef CVC5__THEORY__QUANTIFIERS__CEGIS_H
+#define CVC5__THEORY__QUANTIFIERS__CEGIS_H
#include <map>
#include "theory/quantifiers/sygus/sygus_module.h"
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__QUANTIFIERS__CEGIS_H */
+#endif /* CVC5__THEORY__QUANTIFIERS__CEGIS_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__QUANTIFIERS__CEGIS_CORE_CONNECTIVE_H
-#define CVC4__THEORY__QUANTIFIERS__CEGIS_CORE_CONNECTIVE_H
+#ifndef CVC5__THEORY__QUANTIFIERS__CEGIS_CORE_CONNECTIVE_H
+#define CVC5__THEORY__QUANTIFIERS__CEGIS_CORE_CONNECTIVE_H
#include <unordered_set>
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__QUANTIFIERS__SYGUS_REPAIR_CONST_H */
+#endif /* CVC5__THEORY__QUANTIFIERS__SYGUS_REPAIR_CONST_H */
**/
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__QUANTIFIERS__SYGUS__CEGIS_UNIF_H
-#define CVC4__THEORY__QUANTIFIERS__SYGUS__CEGIS_UNIF_H
+#ifndef CVC5__THEORY__QUANTIFIERS__SYGUS__CEGIS_UNIF_H
+#define CVC5__THEORY__QUANTIFIERS__SYGUS__CEGIS_UNIF_H
#include <map>
#include <vector>
**/
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__QUANTIFIERS__SYGUS__ENUM_STREAM_SUBSTITUTION_H
-#define CVC4__THEORY__QUANTIFIERS__SYGUS__ENUM_STREAM_SUBSTITUTION_H
+#ifndef CVC5__THEORY__QUANTIFIERS__SYGUS__ENUM_STREAM_SUBSTITUTION_H
+#define CVC5__THEORY__QUANTIFIERS__SYGUS__ENUM_STREAM_SUBSTITUTION_H
#include "expr/node.h"
#include "theory/quantifiers/sygus/synth_conjecture.h"
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__QUANTIFIERS__EXAMPLE_EVAL_CACHE_H
-#define CVC4__THEORY__QUANTIFIERS__EXAMPLE_EVAL_CACHE_H
+#ifndef CVC5__THEORY__QUANTIFIERS__EXAMPLE_EVAL_CACHE_H
+#define CVC5__THEORY__QUANTIFIERS__EXAMPLE_EVAL_CACHE_H
#include "expr/node_trie.h"
#include "theory/quantifiers/sygus/example_infer.h"
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__QUANTIFIERS__EXAMPLE_INFER_H
-#define CVC4__THEORY__QUANTIFIERS__EXAMPLE_INFER_H
+#ifndef CVC5__THEORY__QUANTIFIERS__EXAMPLE_INFER_H
+#define CVC5__THEORY__QUANTIFIERS__EXAMPLE_INFER_H
#include "theory/quantifiers/sygus/sygus_unif_io.h"
#include "theory/quantifiers/sygus/term_database_sygus.h"
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__QUANTIFIERS__EXAMPLE_MIN_EVAL_H
-#define CVC4__THEORY__QUANTIFIERS__EXAMPLE_MIN_EVAL_H
+#ifndef CVC5__THEORY__QUANTIFIERS__EXAMPLE_MIN_EVAL_H
+#define CVC5__THEORY__QUANTIFIERS__EXAMPLE_MIN_EVAL_H
#include <vector>
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__QUANTIFIERS__RCONS_OBLIGATION_INFO_H
-#define CVC4__THEORY__QUANTIFIERS__RCONS_OBLIGATION_INFO_H
+#ifndef CVC5__THEORY__QUANTIFIERS__RCONS_OBLIGATION_INFO_H
+#define CVC5__THEORY__QUANTIFIERS__RCONS_OBLIGATION_INFO_H
#include "expr/node.h"
} // namespace theory
} // namespace cvc5
-#endif // CVC4__THEORY__QUANTIFIERS__RCONS_OBLIGATION_INFO_H
+#endif // CVC5__THEORY__QUANTIFIERS__RCONS_OBLIGATION_INFO_H
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__QUANTIFIERS__RCONS_TYPE_INFO_H
-#define CVC4__THEORY__QUANTIFIERS__RCONS_TYPE_INFO_H
+#ifndef CVC5__THEORY__QUANTIFIERS__RCONS_TYPE_INFO_H
+#define CVC5__THEORY__QUANTIFIERS__RCONS_TYPE_INFO_H
#include "theory/quantifiers/sygus/sygus_enumerator.h"
} // namespace theory
} // namespace cvc5
-#endif // CVC4__THEORY__QUANTIFIERS__RCONS_TYPE_INFO_H
+#endif // CVC5__THEORY__QUANTIFIERS__RCONS_TYPE_INFO_H
** abduction problem.
**/
-#ifndef CVC4__THEORY__QUANTIFIERS__SYGUS_ABDUCT_H
-#define CVC4__THEORY__QUANTIFIERS__SYGUS_ABDUCT_H
+#ifndef CVC5__THEORY__QUANTIFIERS__SYGUS_ABDUCT_H
+#define CVC5__THEORY__QUANTIFIERS__SYGUS_ABDUCT_H
#include <string>
#include <vector>
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__QUANTIFIERS__SYGUS_ABDUCT_H */
+#endif /* CVC5__THEORY__QUANTIFIERS__SYGUS_ABDUCT_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__QUANTIFIERS__SYGUS_ENUMERATOR_H
-#define CVC4__THEORY__QUANTIFIERS__SYGUS_ENUMERATOR_H
+#ifndef CVC5__THEORY__QUANTIFIERS__SYGUS_ENUMERATOR_H
+#define CVC5__THEORY__QUANTIFIERS__SYGUS_ENUMERATOR_H
#include <map>
#include <unordered_set>
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__QUANTIFIERS__SYGUS_ENUMERATOR_H */
+#endif /* CVC5__THEORY__QUANTIFIERS__SYGUS_ENUMERATOR_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__QUANTIFIERS__SYGUS_ENUMERATOR_BASIC_H
-#define CVC4__THEORY__QUANTIFIERS__SYGUS_ENUMERATOR_BASIC_H
+#ifndef CVC5__THEORY__QUANTIFIERS__SYGUS_ENUMERATOR_BASIC_H
+#define CVC5__THEORY__QUANTIFIERS__SYGUS_ENUMERATOR_BASIC_H
#include <map>
#include <unordered_set>
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__QUANTIFIERS__SYGUS_ENUMERATOR_BASIC_H */
+#endif /* CVC5__THEORY__QUANTIFIERS__SYGUS_ENUMERATOR_BASIC_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__QUANTIFIERS__SYGUS_EVAL_UNFOLD_H
-#define CVC4__THEORY__QUANTIFIERS__SYGUS_EVAL_UNFOLD_H
+#ifndef CVC5__THEORY__QUANTIFIERS__SYGUS_EVAL_UNFOLD_H
+#define CVC5__THEORY__QUANTIFIERS__SYGUS_EVAL_UNFOLD_H
#include <map>
#include "expr/node.h"
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__QUANTIFIERS__SYGUS_EVAL_UNFOLD_H */
+#endif /* CVC5__THEORY__QUANTIFIERS__SYGUS_EVAL_UNFOLD_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__QUANTIFIERS__SYGUS_EXPLAIN_H
-#define CVC4__THEORY__QUANTIFIERS__SYGUS_EXPLAIN_H
+#ifndef CVC5__THEORY__QUANTIFIERS__SYGUS_EXPLAIN_H
+#define CVC5__THEORY__QUANTIFIERS__SYGUS_EXPLAIN_H
#include <vector>
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__QUANTIFIERS__SYGUS_EXPLAIN_H */
+#endif /* CVC5__THEORY__QUANTIFIERS__SYGUS_EXPLAIN_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__QUANTIFIERS__SYGUS_GRAMMAR_CONS_H
-#define CVC4__THEORY__QUANTIFIERS__SYGUS_GRAMMAR_CONS_H
+#ifndef CVC5__THEORY__QUANTIFIERS__SYGUS_GRAMMAR_CONS_H
+#define CVC5__THEORY__QUANTIFIERS__SYGUS_GRAMMAR_CONS_H
#include <map>
#include <vector>
**/
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__QUANTIFIERS__SYGUS_GRAMMAR_NORM_H
-#define CVC4__THEORY__QUANTIFIERS__SYGUS_GRAMMAR_NORM_H
+#ifndef CVC5__THEORY__QUANTIFIERS__SYGUS_GRAMMAR_NORM_H
+#define CVC5__THEORY__QUANTIFIERS__SYGUS_GRAMMAR_NORM_H
#include <map>
#include <memory>
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__QUANTIFIERS__SYGUS_GRAMMAR_RED_H
-#define CVC4__THEORY__QUANTIFIERS__SYGUS_GRAMMAR_RED_H
+#ifndef CVC5__THEORY__QUANTIFIERS__SYGUS_GRAMMAR_RED_H
+#define CVC5__THEORY__QUANTIFIERS__SYGUS_GRAMMAR_RED_H
#include <map>
#include <vector>
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__QUANTIFIERS__SYGUS_GRAMMAR_RED_H */
+#endif /* CVC5__THEORY__QUANTIFIERS__SYGUS_GRAMMAR_RED_H */
** conjecture into an interpolation problem, and solve it.
**/
-#ifndef CVC4__THEORY__QUANTIFIERS__SYGUS_INTERPOL_H
-#define CVC4__THEORY__QUANTIFIERS__SYGUS_INTERPOL_H
+#ifndef CVC5__THEORY__QUANTIFIERS__SYGUS_INTERPOL_H
+#define CVC5__THEORY__QUANTIFIERS__SYGUS_INTERPOL_H
#include <string>
#include <vector>
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__QUANTIFIERS__SYGUS_INTERPOL_H */
+#endif /* CVC5__THEORY__QUANTIFIERS__SYGUS_INTERPOL_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__QUANTIFIERS__SYGUS_INVARIANCE_H
-#define CVC4__THEORY__QUANTIFIERS__SYGUS_INVARIANCE_H
+#ifndef CVC5__THEORY__QUANTIFIERS__SYGUS_INVARIANCE_H
+#define CVC5__THEORY__QUANTIFIERS__SYGUS_INVARIANCE_H
#include <unordered_map>
#include <vector>
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__QUANTIFIERS__SYGUS_INVARIANCE_H */
+#endif /* CVC5__THEORY__QUANTIFIERS__SYGUS_INVARIANCE_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__QUANTIFIERS__SYGUS_MODULE_H
-#define CVC4__THEORY__QUANTIFIERS__SYGUS_MODULE_H
+#ifndef CVC5__THEORY__QUANTIFIERS__SYGUS_MODULE_H
+#define CVC5__THEORY__QUANTIFIERS__SYGUS_MODULE_H
#include <vector>
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__QUANTIFIERS__SYGUS_MODULE_H */
+#endif /* CVC5__THEORY__QUANTIFIERS__SYGUS_MODULE_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__QUANTIFIERS__SYGUS_PBE_H
-#define CVC4__THEORY__QUANTIFIERS__SYGUS_PBE_H
+#ifndef CVC5__THEORY__QUANTIFIERS__SYGUS_PBE_H
+#define CVC5__THEORY__QUANTIFIERS__SYGUS_PBE_H
#include "theory/quantifiers/sygus/sygus_module.h"
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__QUANTIFIERS__SYGUS_PROCESS_CONJ_H
-#define CVC4__THEORY__QUANTIFIERS__SYGUS_PROCESS_CONJ_H
+#ifndef CVC5__THEORY__QUANTIFIERS__SYGUS_PROCESS_CONJ_H
+#define CVC5__THEORY__QUANTIFIERS__SYGUS_PROCESS_CONJ_H
#include <map>
#include <unordered_map>
** \brief Sygus quantifier elimination preprocessor
**/
-#ifndef CVC4__THEORY__QUANTIFIERS__SYGUS__SYGUS_QE_PREPROC_H
-#define CVC4__THEORY__QUANTIFIERS__SYGUS__SYGUS_QE_PREPROC_H
+#ifndef CVC5__THEORY__QUANTIFIERS__SYGUS__SYGUS_QE_PREPROC_H
+#define CVC5__THEORY__QUANTIFIERS__SYGUS__SYGUS_QE_PREPROC_H
#include "expr/node.h"
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__QUANTIFIERS__SYGUS__SYGUS_QE_PREPROC_H */
+#endif /* CVC5__THEORY__QUANTIFIERS__SYGUS__SYGUS_QE_PREPROC_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__QUANTIFIERS__SYGUS_RECONSTRUCT_H
-#define CVC4__THEORY__QUANTIFIERS__SYGUS_RECONSTRUCT_H
+#ifndef CVC5__THEORY__QUANTIFIERS__SYGUS_RECONSTRUCT_H
+#define CVC5__THEORY__QUANTIFIERS__SYGUS_RECONSTRUCT_H
#include <map>
#include <vector>
} // namespace theory
} // namespace cvc5
-#endif // CVC4__THEORY__QUANTIFIERS__SYGUS_RECONSTRUCT_H
+#endif // CVC5__THEORY__QUANTIFIERS__SYGUS_RECONSTRUCT_H
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__QUANTIFIERS__SYGUS_REPAIR_CONST_H
-#define CVC4__THEORY__QUANTIFIERS__SYGUS_REPAIR_CONST_H
+#ifndef CVC5__THEORY__QUANTIFIERS__SYGUS_REPAIR_CONST_H
+#define CVC5__THEORY__QUANTIFIERS__SYGUS_REPAIR_CONST_H
#include <unordered_set>
#include "expr/node.h"
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__QUANTIFIERS__SYGUS_REPAIR_CONST_H */
+#endif /* CVC5__THEORY__QUANTIFIERS__SYGUS_REPAIR_CONST_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__QUANTIFIERS__SYGUS_STATS_H
-#define CVC4__THEORY__QUANTIFIERS__SYGUS_STATS_H
+#ifndef CVC5__THEORY__QUANTIFIERS__SYGUS_STATS_H
+#define CVC5__THEORY__QUANTIFIERS__SYGUS_STATS_H
#include "util/statistics_registry.h"
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__QUANTIFIERS__SYGUS_UNIF_H
-#define CVC4__THEORY__QUANTIFIERS__SYGUS_UNIF_H
+#ifndef CVC5__THEORY__QUANTIFIERS__SYGUS_UNIF_H
+#define CVC5__THEORY__QUANTIFIERS__SYGUS_UNIF_H
#include <map>
#include "expr/node.h"
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__QUANTIFIERS__SYGUS_UNIF_H */
+#endif /* CVC5__THEORY__QUANTIFIERS__SYGUS_UNIF_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__QUANTIFIERS__SYGUS_UNIF_IO_H
-#define CVC4__THEORY__QUANTIFIERS__SYGUS_UNIF_IO_H
+#ifndef CVC5__THEORY__QUANTIFIERS__SYGUS_UNIF_IO_H
+#define CVC5__THEORY__QUANTIFIERS__SYGUS_UNIF_IO_H
#include <map>
#include "theory/quantifiers/sygus/sygus_unif.h"
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__QUANTIFIERS__SYGUS_UNIF_IO_H */
+#endif /* CVC5__THEORY__QUANTIFIERS__SYGUS_UNIF_IO_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__QUANTIFIERS__SYGUS_UNIF_RL_H
-#define CVC4__THEORY__QUANTIFIERS__SYGUS_UNIF_RL_H
+#ifndef CVC5__THEORY__QUANTIFIERS__SYGUS_UNIF_RL_H
+#define CVC5__THEORY__QUANTIFIERS__SYGUS_UNIF_RL_H
#include <map>
#include "options/main_options.h"
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__QUANTIFIERS__SYGUS_UNIF_RL_H */
+#endif /* CVC5__THEORY__QUANTIFIERS__SYGUS_UNIF_RL_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__QUANTIFIERS__SYGUS_UNIF_STRAT_H
-#define CVC4__THEORY__QUANTIFIERS__SYGUS_UNIF_STRAT_H
+#ifndef CVC5__THEORY__QUANTIFIERS__SYGUS_UNIF_STRAT_H
+#define CVC5__THEORY__QUANTIFIERS__SYGUS_UNIF_STRAT_H
#include <map>
#include "expr/node.h"
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__QUANTIFIERS__SYGUS_UNIF_H */
+#endif /* CVC5__THEORY__QUANTIFIERS__SYGUS_UNIF_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__QUANTIFIERS__SYGUS__SYGUS_UTILS_H
-#define CVC4__THEORY__QUANTIFIERS__SYGUS__SYGUS_UTILS_H
+#ifndef CVC5__THEORY__QUANTIFIERS__SYGUS__SYGUS_UTILS_H
+#define CVC5__THEORY__QUANTIFIERS__SYGUS__SYGUS_UTILS_H
#include <vector>
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__QUANTIFIERS__SYGUS__SYGUS_UTILS_H */
+#endif /* CVC5__THEORY__QUANTIFIERS__SYGUS__SYGUS_UTILS_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__QUANTIFIERS__SYNTH_CONJECTURE_H
-#define CVC4__THEORY__QUANTIFIERS__SYNTH_CONJECTURE_H
+#ifndef CVC5__THEORY__QUANTIFIERS__SYNTH_CONJECTURE_H
+#define CVC5__THEORY__QUANTIFIERS__SYNTH_CONJECTURE_H
#include <memory>
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__QUANTIFIERS__SYNTH_ENGINE_H
-#define CVC4__THEORY__QUANTIFIERS__SYNTH_ENGINE_H
+#ifndef CVC5__THEORY__QUANTIFIERS__SYNTH_ENGINE_H
+#define CVC5__THEORY__QUANTIFIERS__SYNTH_ENGINE_H
#include "context/cdhashmap.h"
#include "theory/quantifiers/quant_module.h"
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__QUANTIFIERS__SYGUS__TEMPLATE_INFER_H
-#define CVC4__THEORY__QUANTIFIERS__SYGUS__TEMPLATE_INFER_H
+#ifndef CVC5__THEORY__QUANTIFIERS__SYGUS__TEMPLATE_INFER_H
+#define CVC5__THEORY__QUANTIFIERS__SYGUS__TEMPLATE_INFER_H
#include <map>
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__QUANTIFIERS__TERM_DATABASE_SYGUS_H
-#define CVC4__THEORY__QUANTIFIERS__TERM_DATABASE_SYGUS_H
+#ifndef CVC5__THEORY__QUANTIFIERS__TERM_DATABASE_SYGUS_H
+#define CVC5__THEORY__QUANTIFIERS__TERM_DATABASE_SYGUS_H
#include <unordered_set>
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__QUANTIFIERS__TERM_DATABASE_H */
+#endif /* CVC5__THEORY__QUANTIFIERS__TERM_DATABASE_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__QUANTIFIERS__TRANSITION_INFERENCE_H
-#define CVC4__THEORY__QUANTIFIERS__TRANSITION_INFERENCE_H
+#ifndef CVC5__THEORY__QUANTIFIERS__TRANSITION_INFERENCE_H
+#define CVC5__THEORY__QUANTIFIERS__TRANSITION_INFERENCE_H
#include <map>
#include <vector>
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__QUANTIFIERS__SYGUS__TYPE_INFO_H
-#define CVC4__THEORY__QUANTIFIERS__SYGUS__TYPE_INFO_H
+#ifndef CVC5__THEORY__QUANTIFIERS__SYGUS__TYPE_INFO_H
+#define CVC5__THEORY__QUANTIFIERS__SYGUS__TYPE_INFO_H
#include <map>
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__QUANTIFIERS__SYGUS__TYPE_INFO_H */
+#endif /* CVC5__THEORY__QUANTIFIERS__SYGUS__TYPE_INFO_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__QUANTIFIERS__SYGUS__TYPE_NODE_ID_TRIE_H
-#define CVC4__THEORY__QUANTIFIERS__SYGUS__TYPE_NODE_ID_TRIE_H
+#ifndef CVC5__THEORY__QUANTIFIERS__SYGUS__TYPE_NODE_ID_TRIE_H
+#define CVC5__THEORY__QUANTIFIERS__SYGUS__TYPE_NODE_ID_TRIE_H
#include <map>
#include <vector>
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__QUANTIFIERS__SYGUS__TYPE_NODE_ID_TRIE_H */
+#endif /* CVC5__THEORY__QUANTIFIERS__SYGUS__TYPE_NODE_ID_TRIE_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__QUANTIFIERS__SYGUS_INST_H
-#define CVC4__THEORY__QUANTIFIERS__SYGUS_INST_H
+#ifndef CVC5__THEORY__QUANTIFIERS__SYGUS_INST_H
+#define CVC5__THEORY__QUANTIFIERS__SYGUS_INST_H
#include <unordered_map>
#include <unordered_set>
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__QUANTIFIERS__SYGUS_SAMPLER_H
-#define CVC4__THEORY__QUANTIFIERS__SYGUS_SAMPLER_H
+#ifndef CVC5__THEORY__QUANTIFIERS__SYGUS_SAMPLER_H
+#define CVC5__THEORY__QUANTIFIERS__SYGUS_SAMPLER_H
#include <map>
#include "theory/evaluator.h"
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__QUANTIFIERS__SYGUS_SAMPLER_H */
+#endif /* CVC5__THEORY__QUANTIFIERS__SYGUS_SAMPLER_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__QUANTIFIERS__TERM_DATABASE_H
-#define CVC4__THEORY__QUANTIFIERS__TERM_DATABASE_H
+#ifndef CVC5__THEORY__QUANTIFIERS__TERM_DATABASE_H
+#define CVC5__THEORY__QUANTIFIERS__TERM_DATABASE_H
#include <map>
#include <unordered_map>
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__QUANTIFIERS__TERM_DATABASE_H */
+#endif /* CVC5__THEORY__QUANTIFIERS__TERM_DATABASE_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__QUANTIFIERS__TERM_ENUMERATION_H
-#define CVC4__THEORY__QUANTIFIERS__TERM_ENUMERATION_H
+#ifndef CVC5__THEORY__QUANTIFIERS__TERM_ENUMERATION_H
+#define CVC5__THEORY__QUANTIFIERS__TERM_ENUMERATION_H
#include <unordered_map>
#include <vector>
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__QUANTIFIERS__TERM_ENUMERATION_H */
+#endif /* CVC5__THEORY__QUANTIFIERS__TERM_ENUMERATION_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__QUANTIFIERS__TERM_POOLS_H
-#define CVC4__THEORY__QUANTIFIERS__TERM_POOLS_H
+#ifndef CVC5__THEORY__QUANTIFIERS__TERM_POOLS_H
+#define CVC5__THEORY__QUANTIFIERS__TERM_POOLS_H
#include <unordered_set>
#include <vector>
} // namespace theory
} // namespace CVC5
-#endif /* CVC4__THEORY__QUANTIFIERS__TERM_POOLS_H */
+#endif /* CVC5__THEORY__QUANTIFIERS__TERM_POOLS_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__QUANTIFIERS__TERM_REGISTRY_H
-#define CVC4__THEORY__QUANTIFIERS__TERM_REGISTRY_H
+#ifndef CVC5__THEORY__QUANTIFIERS__TERM_REGISTRY_H
+#define CVC5__THEORY__QUANTIFIERS__TERM_REGISTRY_H
#include <map>
#include <unordered_set>
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__QUANTIFIERS__TERM_REGISTRY_H */
+#endif /* CVC5__THEORY__QUANTIFIERS__TERM_REGISTRY_H */
** \brief Implementation of an enumeration of tuples of terms for the purpose
*of quantifier instantiation.
**/
-#ifndef CVC4__THEORY__QUANTIFIERS__TERM_TUPLE_ENUMERATOR_H
-#define CVC4__THEORY__QUANTIFIERS__TERM_TUPLE_ENUMERATOR_H
+#ifndef CVC5__THEORY__QUANTIFIERS__TERM_TUPLE_ENUMERATOR_H
+#define CVC5__THEORY__QUANTIFIERS__TERM_TUPLE_ENUMERATOR_H
#include <vector>
#include "expr/node.h"
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__QUANTIFIERS__TERM_UTIL_H
-#define CVC4__THEORY__QUANTIFIERS__TERM_UTIL_H
+#ifndef CVC5__THEORY__QUANTIFIERS__TERM_UTIL_H
+#define CVC5__THEORY__QUANTIFIERS__TERM_UTIL_H
#include <map>
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__QUANTIFIERS__TERM_UTIL_H */
+#endif /* CVC5__THEORY__QUANTIFIERS__TERM_UTIL_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__QUANTIFIERS__THEORY_QUANTIFIERS_H
-#define CVC4__THEORY__QUANTIFIERS__THEORY_QUANTIFIERS_H
+#ifndef CVC5__THEORY__QUANTIFIERS__THEORY_QUANTIFIERS_H
+#define CVC5__THEORY__QUANTIFIERS__THEORY_QUANTIFIERS_H
#include "expr/node.h"
#include "theory/quantifiers/proof_checker.h"
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__QUANTIFIERS__THEORY_QUANTIFIERS_H */
+#endif /* CVC5__THEORY__QUANTIFIERS__THEORY_QUANTIFIERS_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__QUANTIFIERS__THEORY_QUANTIFIERS_TYPE_RULES_H
-#define CVC4__THEORY__QUANTIFIERS__THEORY_QUANTIFIERS_TYPE_RULES_H
+#ifndef CVC5__THEORY__QUANTIFIERS__THEORY_QUANTIFIERS_TYPE_RULES_H
+#define CVC5__THEORY__QUANTIFIERS__THEORY_QUANTIFIERS_TYPE_RULES_H
#include "expr/node.h"
#include "expr/type_node.h"
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__QUANTIFIERS__THEORY_QUANTIFIERS_TYPE_RULES_H */
+#endif /* CVC5__THEORY__QUANTIFIERS__THEORY_QUANTIFIERS_TYPE_RULES_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__QUANTIFIERS_ENGINE_H
-#define CVC4__THEORY__QUANTIFIERS_ENGINE_H
+#ifndef CVC5__THEORY__QUANTIFIERS_ENGINE_H
+#define CVC5__THEORY__QUANTIFIERS_ENGINE_H
#include <map>
#include <unordered_map>
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__QUANTIFIERS_ENGINE_H */
+#endif /* CVC5__THEORY__QUANTIFIERS_ENGINE_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__RELEVANCE_MANAGER__H
-#define CVC4__THEORY__RELEVANCE_MANAGER__H
+#ifndef CVC5__THEORY__RELEVANCE_MANAGER__H
+#define CVC5__THEORY__RELEVANCE_MANAGER__H
#include <unordered_map>
#include <unordered_set>
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__RELEVANCE_MANAGER__H */
+#endif /* CVC5__THEORY__RELEVANCE_MANAGER__H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__REP_SET_H
-#define CVC4__THEORY__REP_SET_H
+#ifndef CVC5__THEORY__REP_SET_H
+#define CVC5__THEORY__REP_SET_H
#include <map>
#include <vector>
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__REP_SET_H */
+#endif /* CVC5__THEORY__REP_SET_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__SEP__THEORY_SEP_H
-#define CVC4__THEORY__SEP__THEORY_SEP_H
+#ifndef CVC5__THEORY__SEP__THEORY_SEP_H
+#define CVC5__THEORY__SEP__THEORY_SEP_H
#include "context/cdhashmap.h"
#include "context/cdhashset.h"
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__SEP__THEORY_SEP_H */
+#endif /* CVC5__THEORY__SEP__THEORY_SEP_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__SEP__THEORY_SEP_REWRITER_H
-#define CVC4__THEORY__SEP__THEORY_SEP_REWRITER_H
+#ifndef CVC5__THEORY__SEP__THEORY_SEP_REWRITER_H
+#define CVC5__THEORY__SEP__THEORY_SEP_REWRITER_H
#include "theory/theory_rewriter.h"
#include "theory/type_enumerator.h"
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__SEP__THEORY_SEP_REWRITER_H */
+#endif /* CVC5__THEORY__SEP__THEORY_SEP_REWRITER_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__SEP__THEORY_SEP_TYPE_RULES_H
-#define CVC4__THEORY__SEP__THEORY_SEP_TYPE_RULES_H
+#ifndef CVC5__THEORY__SEP__THEORY_SEP_TYPE_RULES_H
+#define CVC5__THEORY__SEP__THEORY_SEP_TYPE_RULES_H
namespace cvc5 {
namespace theory {
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__SEP__THEORY_SEP_TYPE_RULES_H */
+#endif /* CVC5__THEORY__SEP__THEORY_SEP_TYPE_RULES_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__SETS__CARDINALITY_EXTENSION_H
-#define CVC4__THEORY__SETS__CARDINALITY_EXTENSION_H
+#ifndef CVC5__THEORY__SETS__CARDINALITY_EXTENSION_H
+#define CVC5__THEORY__SETS__CARDINALITY_EXTENSION_H
#include "context/cdhashset.h"
#include "context/context.h"
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__SETS__INFERENCE_MANAGER_H
-#define CVC4__THEORY__SETS__INFERENCE_MANAGER_H
+#ifndef CVC5__THEORY__SETS__INFERENCE_MANAGER_H
+#define CVC5__THEORY__SETS__INFERENCE_MANAGER_H
#include "theory/inference_manager_buffered.h"
#include "theory/sets/solver_state.h"
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__SETS__INFERENCE_MANAGER_H */
+#endif /* CVC5__THEORY__SETS__INFERENCE_MANAGER_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__SETS__NORMAL_FORM_H
-#define CVC4__THEORY__SETS__NORMAL_FORM_H
+#ifndef CVC5__THEORY__SETS__NORMAL_FORM_H
+#define CVC5__THEORY__SETS__NORMAL_FORM_H
namespace cvc5 {
namespace theory {
#include "cvc4_public.h"
-#ifndef CVC4__SINGLETON_OP_H
-#define CVC4__SINGLETON_OP_H
+#ifndef CVC5__SINGLETON_OP_H
+#define CVC5__SINGLETON_OP_H
#include <memory>
} // namespace cvc5
-#endif /* CVC4__SINGLETON_OP_H */
+#endif /* CVC5__SINGLETON_OP_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__SETS__SKOLEM_CACHE_H
-#define CVC4__THEORY__SETS__SKOLEM_CACHE_H
+#ifndef CVC5__THEORY__SETS__SKOLEM_CACHE_H
+#define CVC5__THEORY__SETS__SKOLEM_CACHE_H
#include <map>
#include <unordered_set>
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__STRINGS__SKOLEM_CACHE_H */
+#endif /* CVC5__THEORY__STRINGS__SKOLEM_CACHE_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__SETS__THEORY_SOLVER_STATE_H
-#define CVC4__THEORY__SETS__THEORY_SOLVER_STATE_H
+#ifndef CVC5__THEORY__SETS__THEORY_SOLVER_STATE_H
+#define CVC5__THEORY__SETS__THEORY_SOLVER_STATE_H
#include <map>
#include <vector>
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__SETS__THEORY_SOLVER_STATE_H */
+#endif /* CVC5__THEORY__SETS__THEORY_SOLVER_STATE_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__SETS__TERM_REGISTRY_H
-#define CVC4__THEORY__SETS__TERM_REGISTRY_H
+#ifndef CVC5__THEORY__SETS__TERM_REGISTRY_H
+#define CVC5__THEORY__SETS__TERM_REGISTRY_H
#include <map>
#include <vector>
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__SETS__TERM_REGISTRY_H */
+#endif /* CVC5__THEORY__SETS__TERM_REGISTRY_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__SETS__THEORY_SETS_H
-#define CVC4__THEORY__SETS__THEORY_SETS_H
+#ifndef CVC5__THEORY__SETS__THEORY_SETS_H
+#define CVC5__THEORY__SETS__THEORY_SETS_H
#include <memory>
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__SETS__THEORY_SETS_H */
+#endif /* CVC5__THEORY__SETS__THEORY_SETS_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__SETS__THEORY_SETS_PRIVATE_H
-#define CVC4__THEORY__SETS__THEORY_SETS_PRIVATE_H
+#ifndef CVC5__THEORY__SETS__THEORY_SETS_PRIVATE_H
+#define CVC5__THEORY__SETS__THEORY_SETS_PRIVATE_H
#include "context/cdhashset.h"
#include "context/cdqueue.h"
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__SETS__THEORY_SETS_PRIVATE_H */
+#endif /* CVC5__THEORY__SETS__THEORY_SETS_PRIVATE_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__SETS__THEORY_SETS_REWRITER_H
-#define CVC4__THEORY__SETS__THEORY_SETS_REWRITER_H
+#ifndef CVC5__THEORY__SETS__THEORY_SETS_REWRITER_H
+#define CVC5__THEORY__SETS__THEORY_SETS_REWRITER_H
#include "theory/rewriter.h"
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__SETS__THEORY_SETS_REWRITER_H */
+#endif /* CVC5__THEORY__SETS__THEORY_SETS_REWRITER_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__SETS__TYPE_ENUMERATOR_H
-#define CVC4__THEORY__SETS__TYPE_ENUMERATOR_H
+#ifndef CVC5__THEORY__SETS__TYPE_ENUMERATOR_H
+#define CVC5__THEORY__SETS__TYPE_ENUMERATOR_H
#include "expr/kind.h"
#include "expr/type_node.h"
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__SETS__TYPE_ENUMERATOR_H */
+#endif /* CVC5__THEORY__SETS__TYPE_ENUMERATOR_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__SETS__THEORY_SETS_TYPE_RULES_H
-#define CVC4__THEORY__SETS__THEORY_SETS_TYPE_RULES_H
+#ifndef CVC5__THEORY__SETS__THEORY_SETS_TYPE_RULES_H
+#define CVC5__THEORY__SETS__THEORY_SETS_TYPE_RULES_H
#include <climits>
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__SETS__THEORY_SETS_TYPE_RULES_H */
+#endif /* CVC5__THEORY__SETS__THEORY_SETS_TYPE_RULES_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__SHARED_SOLVER__H
-#define CVC4__THEORY__SHARED_SOLVER__H
+#ifndef CVC5__THEORY__SHARED_SOLVER__H
+#define CVC5__THEORY__SHARED_SOLVER__H
#include "expr/node.h"
#include "theory/shared_terms_database.h"
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__SHARED_SOLVER__H */
+#endif /* CVC5__THEORY__SHARED_SOLVER__H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__SHARED_SOLVER_DISTRIBUTED__H
-#define CVC4__THEORY__SHARED_SOLVER_DISTRIBUTED__H
+#ifndef CVC5__THEORY__SHARED_SOLVER_DISTRIBUTED__H
+#define CVC5__THEORY__SHARED_SOLVER_DISTRIBUTED__H
#include "expr/node.h"
#include "theory/shared_solver.h"
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__SHARED_SOLVER_DISTRIBUTED__H */
+#endif /* CVC5__THEORY__SHARED_SOLVER_DISTRIBUTED__H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__SKOLEM_LEMMA_H
-#define CVC4__THEORY__SKOLEM_LEMMA_H
+#ifndef CVC5__THEORY__SKOLEM_LEMMA_H
+#define CVC5__THEORY__SKOLEM_LEMMA_H
#include "expr/node.h"
#include "theory/trust_node.h"
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__SKOLEM_LEMMA_H */
+#endif /* CVC5__THEORY__SKOLEM_LEMMA_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__SMT_ENGINE_SUBSOLVER_H
-#define CVC4__THEORY__SMT_ENGINE_SUBSOLVER_H
+#ifndef CVC5__THEORY__SMT_ENGINE_SUBSOLVER_H
+#define CVC5__THEORY__SMT_ENGINE_SUBSOLVER_H
#include <memory>
#include <vector>
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__SMT_ENGINE_SUBSOLVER_H */
+#endif /* CVC5__THEORY__SMT_ENGINE_SUBSOLVER_H */
#include "cvc4_private.h"
-#ifndef CVC4__SORT_INFERENCE_H
-#define CVC4__SORT_INFERENCE_H
+#ifndef CVC5__SORT_INFERENCE_H
+#define CVC5__SORT_INFERENCE_H
#include <map>
#include <vector>
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__STRINGS__ARITH_ENTAIL_H
-#define CVC4__THEORY__STRINGS__ARITH_ENTAIL_H
+#ifndef CVC5__THEORY__STRINGS__ARITH_ENTAIL_H
+#define CVC5__THEORY__STRINGS__ARITH_ENTAIL_H
#include <vector>
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__STRINGS__BASE_SOLVER_H
-#define CVC4__THEORY__STRINGS__BASE_SOLVER_H
+#ifndef CVC5__THEORY__STRINGS__BASE_SOLVER_H
+#define CVC5__THEORY__STRINGS__BASE_SOLVER_H
#include "context/cdhashset.h"
#include "context/cdlist.h"
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__STRINGS__BASE_SOLVER_H */
+#endif /* CVC5__THEORY__STRINGS__BASE_SOLVER_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__STRINGS__CORE_SOLVER_H
-#define CVC4__THEORY__STRINGS__CORE_SOLVER_H
+#ifndef CVC5__THEORY__STRINGS__CORE_SOLVER_H
+#define CVC5__THEORY__STRINGS__CORE_SOLVER_H
#include "context/cdhashset.h"
#include "context/cdlist.h"
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__STRINGS__CORE_SOLVER_H */
+#endif /* CVC5__THEORY__STRINGS__CORE_SOLVER_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__STRINGS__EAGER_SOLVER_H
-#define CVC4__THEORY__STRINGS__EAGER_SOLVER_H
+#ifndef CVC5__THEORY__STRINGS__EAGER_SOLVER_H
+#define CVC5__THEORY__STRINGS__EAGER_SOLVER_H
#include <map>
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__STRINGS__EAGER_SOLVER_H */
+#endif /* CVC5__THEORY__STRINGS__EAGER_SOLVER_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__STRINGS__EQC_INFO_H
-#define CVC4__THEORY__STRINGS__EQC_INFO_H
+#ifndef CVC5__THEORY__STRINGS__EQC_INFO_H
+#define CVC5__THEORY__STRINGS__EQC_INFO_H
#include <map>
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__STRINGS__EQC_INFO_H */
+#endif /* CVC5__THEORY__STRINGS__EQC_INFO_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__STRINGS__EXTF_SOLVER_H
-#define CVC4__THEORY__STRINGS__EXTF_SOLVER_H
+#ifndef CVC5__THEORY__STRINGS__EXTF_SOLVER_H
+#define CVC5__THEORY__STRINGS__EXTF_SOLVER_H
#include <map>
#include <vector>
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__STRINGS__EXTF_SOLVER_H */
+#endif /* CVC5__THEORY__STRINGS__EXTF_SOLVER_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__STRINGS__INFER_INFO_H
-#define CVC4__THEORY__STRINGS__INFER_INFO_H
+#ifndef CVC5__THEORY__STRINGS__INFER_INFO_H
+#define CVC5__THEORY__STRINGS__INFER_INFO_H
#include <map>
#include <vector>
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__STRINGS__INFER_INFO_H */
+#endif /* CVC5__THEORY__STRINGS__INFER_INFO_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__STRINGS__INFER_PROOF_CONS_H
-#define CVC4__THEORY__STRINGS__INFER_PROOF_CONS_H
+#ifndef CVC5__THEORY__STRINGS__INFER_PROOF_CONS_H
+#define CVC5__THEORY__STRINGS__INFER_PROOF_CONS_H
#include <vector>
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__STRINGS__INFER_PROOF_CONS_H */
+#endif /* CVC5__THEORY__STRINGS__INFER_PROOF_CONS_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__STRINGS__INFERENCE_MANAGER_H
-#define CVC4__THEORY__STRINGS__INFERENCE_MANAGER_H
+#ifndef CVC5__THEORY__STRINGS__INFERENCE_MANAGER_H
+#define CVC5__THEORY__STRINGS__INFERENCE_MANAGER_H
#include <map>
#include <vector>
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__STRINGS__NORMAL_FORM_H
-#define CVC4__THEORY__STRINGS__NORMAL_FORM_H
+#ifndef CVC5__THEORY__STRINGS__NORMAL_FORM_H
+#define CVC5__THEORY__STRINGS__NORMAL_FORM_H
#include <map>
#include <vector>
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__STRINGS__NORMAL_FORM_H */
+#endif /* CVC5__THEORY__STRINGS__NORMAL_FORM_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__STRINGS__PROOF_CHECKER_H
-#define CVC4__THEORY__STRINGS__PROOF_CHECKER_H
+#ifndef CVC5__THEORY__STRINGS__PROOF_CHECKER_H
+#define CVC5__THEORY__STRINGS__PROOF_CHECKER_H
#include "expr/node.h"
#include "expr/proof_checker.h"
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__STRINGS__PROOF_CHECKER_H */
+#endif /* CVC5__THEORY__STRINGS__PROOF_CHECKER_H */
**/
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__STRINGS__REGEXP_ELIM_H
-#define CVC4__THEORY__STRINGS__REGEXP_ELIM_H
+#ifndef CVC5__THEORY__STRINGS__REGEXP_ELIM_H
+#define CVC5__THEORY__STRINGS__REGEXP_ELIM_H
#include "expr/node.h"
#include "theory/eager_proof_generator.h"
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__STRINGS__REGEXP_ELIM_H */
+#endif /* CVC5__THEORY__STRINGS__REGEXP_ELIM_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__STRINGS__REGEXP_ENTAIL_H
-#define CVC4__THEORY__STRINGS__REGEXP_ENTAIL_H
+#ifndef CVC5__THEORY__STRINGS__REGEXP_ENTAIL_H
+#define CVC5__THEORY__STRINGS__REGEXP_ENTAIL_H
#include <climits>
#include <utility>
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__STRINGS__REGEXP_ENTAIL_H */
+#endif /* CVC5__THEORY__STRINGS__REGEXP_ENTAIL_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__STRINGS__REGEXP__OPERATION_H
-#define CVC4__THEORY__STRINGS__REGEXP__OPERATION_H
+#ifndef CVC5__THEORY__STRINGS__REGEXP__OPERATION_H
+#define CVC5__THEORY__STRINGS__REGEXP__OPERATION_H
#include <map>
#include <set>
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__STRINGS__REGEXP__OPERATION_H */
+#endif /* CVC5__THEORY__STRINGS__REGEXP__OPERATION_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__STRINGS__REGEXP_SOLVER_H
-#define CVC4__THEORY__STRINGS__REGEXP_SOLVER_H
+#ifndef CVC5__THEORY__STRINGS__REGEXP_SOLVER_H
+#define CVC5__THEORY__STRINGS__REGEXP_SOLVER_H
#include <map>
#include "context/cdhashset.h"
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__STRINGS__THEORY_STRINGS_H */
+#endif /* CVC5__THEORY__STRINGS__THEORY_STRINGS_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__STRINGS__REWRITES_H
-#define CVC4__THEORY__STRINGS__REWRITES_H
+#ifndef CVC5__THEORY__STRINGS__REWRITES_H
+#define CVC5__THEORY__STRINGS__REWRITES_H
#include <iosfwd>
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__STRINGS__REWRITES_H */
+#endif /* CVC5__THEORY__STRINGS__REWRITES_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__STRINGS__SEQUENCES_REWRITER_H
-#define CVC4__THEORY__STRINGS__SEQUENCES_REWRITER_H
+#ifndef CVC5__THEORY__STRINGS__SEQUENCES_REWRITER_H
+#define CVC5__THEORY__STRINGS__SEQUENCES_REWRITER_H
#include <vector>
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__STRINGS__SEQUENCES_REWRITER_H */
+#endif /* CVC5__THEORY__STRINGS__SEQUENCES_REWRITER_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__STRINGS__SEQUENCES_STATS_H
-#define CVC4__THEORY__STRINGS__SEQUENCES_STATS_H
+#ifndef CVC5__THEORY__STRINGS__SEQUENCES_STATS_H
+#define CVC5__THEORY__STRINGS__SEQUENCES_STATS_H
#include "expr/kind.h"
#include "theory/strings/infer_info.h"
}
} // namespace cvc5
-#endif /* CVC4__THEORY__STRINGS__SEQUENCES_STATS_H */
+#endif /* CVC5__THEORY__STRINGS__SEQUENCES_STATS_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__STRINGS__SKOLEM_CACHE_H
-#define CVC4__THEORY__STRINGS__SKOLEM_CACHE_H
+#ifndef CVC5__THEORY__STRINGS__SKOLEM_CACHE_H
+#define CVC5__THEORY__STRINGS__SKOLEM_CACHE_H
#include <map>
#include <tuple>
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__STRINGS__SKOLEM_CACHE_H */
+#endif /* CVC5__THEORY__STRINGS__SKOLEM_CACHE_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__STRINGS__SOLVER_STATE_H
-#define CVC4__THEORY__STRINGS__SOLVER_STATE_H
+#ifndef CVC5__THEORY__STRINGS__SOLVER_STATE_H
+#define CVC5__THEORY__STRINGS__SOLVER_STATE_H
#include <map>
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__STRINGS__SOLVER_STATE_H */
+#endif /* CVC5__THEORY__STRINGS__SOLVER_STATE_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__STRINGS__STRATEGY_H
-#define CVC4__THEORY__STRINGS__STRATEGY_H
+#ifndef CVC5__THEORY__STRINGS__STRATEGY_H
+#define CVC5__THEORY__STRINGS__STRATEGY_H
#include <map>
#include <vector>
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__STRINGS__STRATEGY_H */
+#endif /* CVC5__THEORY__STRINGS__STRATEGY_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__STRINGS__STRING_ENTAIL_H
-#define CVC4__THEORY__STRINGS__STRING_ENTAIL_H
+#ifndef CVC5__THEORY__STRINGS__STRING_ENTAIL_H
+#define CVC5__THEORY__STRINGS__STRING_ENTAIL_H
#include <vector>
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__STRINGS__STRING_ENTAIL_H */
+#endif /* CVC5__THEORY__STRINGS__STRING_ENTAIL_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__STRINGS__STRINGS_FMF_H
-#define CVC4__THEORY__STRINGS__STRINGS_FMF_H
+#ifndef CVC5__THEORY__STRINGS__STRINGS_FMF_H
+#define CVC5__THEORY__STRINGS__STRINGS_FMF_H
#include "context/cdhashset.h"
#include "context/cdo.h"
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__STRINGS__STRINGS_FMF_H */
+#endif /* CVC5__THEORY__STRINGS__STRINGS_FMF_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__STRINGS__STRINGS_REWRITER_H
-#define CVC4__THEORY__STRINGS__STRINGS_REWRITER_H
+#ifndef CVC5__THEORY__STRINGS__STRINGS_REWRITER_H
+#define CVC5__THEORY__STRINGS__STRINGS_REWRITER_H
#include "expr/node.h"
#include "theory/strings/sequences_rewriter.h"
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__STRINGS__STRINGS_REWRITER_H */
+#endif /* CVC5__THEORY__STRINGS__STRINGS_REWRITER_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__STRINGS__TERM_REGISTRY_H
-#define CVC4__THEORY__STRINGS__TERM_REGISTRY_H
+#ifndef CVC5__THEORY__STRINGS__TERM_REGISTRY_H
+#define CVC5__THEORY__STRINGS__TERM_REGISTRY_H
#include "context/cdhashset.h"
#include "context/cdlist.h"
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__STRINGS__TERM_REGISTRY_H */
+#endif /* CVC5__THEORY__STRINGS__TERM_REGISTRY_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__STRINGS__THEORY_STRINGS_H
-#define CVC4__THEORY__STRINGS__THEORY_STRINGS_H
+#ifndef CVC5__THEORY__STRINGS__THEORY_STRINGS_H
+#define CVC5__THEORY__STRINGS__THEORY_STRINGS_H
#include <climits>
#include <deque>
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__STRINGS__THEORY_STRINGS_H */
+#endif /* CVC5__THEORY__STRINGS__THEORY_STRINGS_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__STRINGS__PREPROCESS_H
-#define CVC4__THEORY__STRINGS__PREPROCESS_H
+#ifndef CVC5__THEORY__STRINGS__PREPROCESS_H
+#define CVC5__THEORY__STRINGS__PREPROCESS_H
#include <vector>
#include "context/cdhashmap.h"
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__STRINGS__PREPROCESS_H */
+#endif /* CVC5__THEORY__STRINGS__PREPROCESS_H */
#include "cvc4_private.h"
#include "options/strings_options.h"
-#ifndef CVC4__THEORY__STRINGS__THEORY_STRINGS_TYPE_RULES_H
-#define CVC4__THEORY__STRINGS__THEORY_STRINGS_TYPE_RULES_H
+#ifndef CVC5__THEORY__STRINGS__THEORY_STRINGS_TYPE_RULES_H
+#define CVC5__THEORY__STRINGS__THEORY_STRINGS_TYPE_RULES_H
#include "expr/sequence.h"
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__STRINGS__THEORY_STRINGS_TYPE_RULES_H */
+#endif /* CVC5__THEORY__STRINGS__THEORY_STRINGS_TYPE_RULES_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__STRINGS__THEORY_STRINGS_UTILS_H
-#define CVC4__THEORY__STRINGS__THEORY_STRINGS_UTILS_H
+#ifndef CVC5__THEORY__STRINGS__THEORY_STRINGS_UTILS_H
+#define CVC5__THEORY__STRINGS__THEORY_STRINGS_UTILS_H
#include <vector>
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__STRINGS__TYPE_ENUMERATOR_H
-#define CVC4__THEORY__STRINGS__TYPE_ENUMERATOR_H
+#ifndef CVC5__THEORY__STRINGS__TYPE_ENUMERATOR_H
+#define CVC5__THEORY__STRINGS__TYPE_ENUMERATOR_H
#include <vector>
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__STRINGS__TYPE_ENUMERATOR_H */
+#endif /* CVC5__THEORY__STRINGS__TYPE_ENUMERATOR_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__STRINGS__WORD_H
-#define CVC4__THEORY__STRINGS__WORD_H
+#ifndef CVC5__THEORY__STRINGS__WORD_H
+#define CVC5__THEORY__STRINGS__WORD_H
#include <vector>
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__SUBS_MINIMIZE_H
-#define CVC4__THEORY__SUBS_MINIMIZE_H
+#ifndef CVC5__THEORY__SUBS_MINIMIZE_H
+#define CVC5__THEORY__SUBS_MINIMIZE_H
#include <vector>
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__SUBS_MINIMIZE_H */
+#endif /* CVC5__THEORY__SUBS_MINIMIZE_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__SUBSTITUTIONS_H
-#define CVC4__THEORY__SUBSTITUTIONS_H
+#ifndef CVC5__THEORY__SUBSTITUTIONS_H
+#define CVC5__THEORY__SUBSTITUTIONS_H
//#include <algorithm>
#include <utility>
} // namespace cvc5
-#endif /* CVC4__THEORY__SUBSTITUTIONS_H */
+#endif /* CVC5__THEORY__SUBSTITUTIONS_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__THEORY_H
-#define CVC4__THEORY__THEORY_H
+#ifndef CVC5__THEORY__THEORY_H
+#define CVC5__THEORY__THEORY_H
#include <iosfwd>
#include <set>
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__THEORY_H */
+#endif /* CVC5__THEORY__THEORY_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY_ENGINE_H
-#define CVC4__THEORY_ENGINE_H
+#ifndef CVC5__THEORY_ENGINE_H
+#define CVC5__THEORY_ENGINE_H
#include <memory>
#include <vector>
} // namespace cvc5
-#endif /* CVC4__THEORY_ENGINE_H */
+#endif /* CVC5__THEORY_ENGINE_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY_ENGINE_PROOF_GENERATOR_H
-#define CVC4__THEORY_ENGINE_PROOF_GENERATOR_H
+#ifndef CVC5__THEORY_ENGINE_PROOF_GENERATOR_H
+#define CVC5__THEORY_ENGINE_PROOF_GENERATOR_H
#include <memory>
} // namespace cvc5
-#endif /* CVC4__THEORY_ENGINE_PROOF_GENERATOR_H */
+#endif /* CVC5__THEORY_ENGINE_PROOF_GENERATOR_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__THEORY_EQ_NOTIFY_H
-#define CVC4__THEORY__THEORY_EQ_NOTIFY_H
+#ifndef CVC5__THEORY__THEORY_EQ_NOTIFY_H
+#define CVC5__THEORY__THEORY_EQ_NOTIFY_H
#include "expr/node.h"
#include "theory/theory_inference_manager.h"
#include "cvc4_public.h"
-#ifndef CVC4__THEORY__THEORY_ID_H
-#define CVC4__THEORY__THEORY_ID_H
+#ifndef CVC5__THEORY__THEORY_ID_H
+#define CVC5__THEORY__THEORY_ID_H
#include <iosfwd>
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__THEORY_INFERENCE_H
-#define CVC4__THEORY__THEORY_INFERENCE_H
+#ifndef CVC5__THEORY__THEORY_INFERENCE_H
+#define CVC5__THEORY__THEORY_INFERENCE_H
#include "expr/node.h"
#include "theory/inference_id.h"
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__THEORY_INFERENCE_MANAGER_H
-#define CVC4__THEORY__THEORY_INFERENCE_MANAGER_H
+#ifndef CVC5__THEORY__THEORY_INFERENCE_MANAGER_H
+#define CVC5__THEORY__THEORY_INFERENCE_MANAGER_H
#include <memory>
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__THEORY_INFERENCE_MANAGER_H */
+#endif /* CVC5__THEORY__THEORY_INFERENCE_MANAGER_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__THEORY_MODEL_H
-#define CVC4__THEORY__THEORY_MODEL_H
+#ifndef CVC5__THEORY__THEORY_MODEL_H
+#define CVC5__THEORY__THEORY_MODEL_H
#include <unordered_map>
#include <unordered_set>
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__THEORY_MODEL_H */
+#endif /* CVC5__THEORY__THEORY_MODEL_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__THEORY_MODEL_BUILDER_H
-#define CVC4__THEORY__THEORY_MODEL_BUILDER_H
+#ifndef CVC5__THEORY__THEORY_MODEL_BUILDER_H
+#define CVC5__THEORY__THEORY_MODEL_BUILDER_H
#include <unordered_map>
#include <unordered_set>
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__THEORY_MODEL_BUILDER_H */
+#endif /* CVC5__THEORY__THEORY_MODEL_BUILDER_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__THEORY_PREPROCESSOR_H
-#define CVC4__THEORY__THEORY_PREPROCESSOR_H
+#ifndef CVC5__THEORY__THEORY_PREPROCESSOR_H
+#define CVC5__THEORY__THEORY_PREPROCESSOR_H
#include <unordered_map>
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__THEORY_PREPROCESSOR_H */
+#endif /* CVC5__THEORY__THEORY_PREPROCESSOR_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__THEORY_PROOF_STEP_BUFFER_H
-#define CVC4__THEORY__THEORY_PROOF_STEP_BUFFER_H
+#ifndef CVC5__THEORY__THEORY_PROOF_STEP_BUFFER_H
+#define CVC5__THEORY__THEORY_PROOF_STEP_BUFFER_H
#include <vector>
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__THEORY_PROOF_STEP_BUFFER_H */
+#endif /* CVC5__THEORY__THEORY_PROOF_STEP_BUFFER_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__THEORY_REWRITER_H
-#define CVC4__THEORY__THEORY_REWRITER_H
+#ifndef CVC5__THEORY__THEORY_REWRITER_H
+#define CVC5__THEORY__THEORY_REWRITER_H
#include "expr/node.h"
#include "theory/trust_node.h"
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__THEORY_REWRITER_H */
+#endif /* CVC5__THEORY__THEORY_REWRITER_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__THEORY_STATE_H
-#define CVC4__THEORY__THEORY_STATE_H
+#ifndef CVC5__THEORY__THEORY_STATE_H
+#define CVC5__THEORY__THEORY_STATE_H
#include "context/cdo.h"
#include "expr/node.h"
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__SOLVER_STATE_H */
+#endif /* CVC5__THEORY__SOLVER_STATE_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__TRUST_NODE_H
-#define CVC4__THEORY__TRUST_NODE_H
+#ifndef CVC5__THEORY__TRUST_NODE_H
+#define CVC5__THEORY__TRUST_NODE_H
#include "expr/node.h"
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__TRUST_NODE_H */
+#endif /* CVC5__THEORY__TRUST_NODE_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__TRUST_SUBSTITUTIONS_H
-#define CVC4__THEORY__TRUST_SUBSTITUTIONS_H
+#ifndef CVC5__THEORY__TRUST_SUBSTITUTIONS_H
+#define CVC5__THEORY__TRUST_SUBSTITUTIONS_H
#include "context/cdlist.h"
#include "context/context.h"
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__TRUST_SUBSTITUTIONS_H */
+#endif /* CVC5__THEORY__TRUST_SUBSTITUTIONS_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__TYPE_ENUMERATOR_H
-#define CVC4__THEORY__TYPE_ENUMERATOR_H
+#ifndef CVC5__THEORY__TYPE_ENUMERATOR_H
+#define CVC5__THEORY__TYPE_ENUMERATOR_H
#include "base/check.h"
#include "base/exception.h"
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__TYPE_ENUMERATOR_H */
+#endif /* CVC5__THEORY__TYPE_ENUMERATOR_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__TYPE_SET_H
-#define CVC4__THEORY__TYPE_SET_H
+#ifndef CVC5__THEORY__TYPE_SET_H
+#define CVC5__THEORY__TYPE_SET_H
#include <unordered_map>
#include <unordered_set>
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__TYPE_SET_H */
+#endif /* CVC5__THEORY__TYPE_SET_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY_UF_STRONG_SOLVER_H
-#define CVC4__THEORY_UF_STRONG_SOLVER_H
+#ifndef CVC5__THEORY_UF_STRONG_SOLVER_H
+#define CVC5__THEORY_UF_STRONG_SOLVER_H
#include "context/cdhashmap.h"
#include "context/context.h"
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY_UF_STRONG_SOLVER_H */
+#endif /* CVC5__THEORY_UF_STRONG_SOLVER_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__UF__EQUALITY_ENGINE_H
-#define CVC4__THEORY__UF__EQUALITY_ENGINE_H
+#ifndef CVC5__THEORY__UF__EQUALITY_ENGINE_H
+#define CVC5__THEORY__UF__EQUALITY_ENGINE_H
#include <deque>
#include <queue>
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__UF__EQUALITY_ENGINE_ITERATOR_H
-#define CVC4__THEORY__UF__EQUALITY_ENGINE_ITERATOR_H
+#ifndef CVC5__THEORY__UF__EQUALITY_ENGINE_ITERATOR_H
+#define CVC5__THEORY__UF__EQUALITY_ENGINE_ITERATOR_H
#include "expr/node.h"
#include "theory/uf/equality_engine_types.h"
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__UF__EQUALITY_ENGINE_NOTIFY_H
-#define CVC4__THEORY__UF__EQUALITY_ENGINE_NOTIFY_H
+#ifndef CVC5__THEORY__UF__EQUALITY_ENGINE_NOTIFY_H
+#define CVC5__THEORY__UF__EQUALITY_ENGINE_NOTIFY_H
#include "expr/node.h"
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__UF__EQUALITY_ENGINE_TYPES_H
-#define CVC4__THEORY__UF__EQUALITY_ENGINE_TYPES_H
+#ifndef CVC5__THEORY__UF__EQUALITY_ENGINE_TYPES_H
+#define CVC5__THEORY__UF__EQUALITY_ENGINE_TYPES_H
#include <string>
#include <iostream>
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__UF__EQUALITY_ENGINE_TYPES_H */
+#endif /* CVC5__THEORY__UF__EQUALITY_ENGINE_TYPES_H */
#include "cvc4_private.h"
-#ifndef __CVC4__THEORY__UF__HO_EXTENSION_H
-#define __CVC4__THEORY__UF__HO_EXTENSION_H
+#ifndef __CVC5__THEORY__UF__HO_EXTENSION_H
+#define __CVC5__THEORY__UF__HO_EXTENSION_H
#include "context/cdhashmap.h"
#include "context/cdhashset.h"
} // namespace theory
} // namespace cvc5
-#endif /* __CVC4__THEORY__UF__HO_EXTENSION_H */
+#endif /* __CVC5__THEORY__UF__HO_EXTENSION_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__UF__PROOF_CHECKER_H
-#define CVC4__THEORY__UF__PROOF_CHECKER_H
+#ifndef CVC5__THEORY__UF__PROOF_CHECKER_H
+#define CVC5__THEORY__UF__PROOF_CHECKER_H
#include "expr/node.h"
#include "expr/proof_checker.h"
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__UF__PROOF_CHECKER_H */
+#endif /* CVC5__THEORY__UF__PROOF_CHECKER_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__UF__PROOF_EQUALITY_ENGINE_H
-#define CVC4__THEORY__UF__PROOF_EQUALITY_ENGINE_H
+#ifndef CVC5__THEORY__UF__PROOF_EQUALITY_ENGINE_H
+#define CVC5__THEORY__UF__PROOF_EQUALITY_ENGINE_H
#include <vector>
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__STRINGS__PROOF_MANAGER_H */
+#endif /* CVC5__THEORY__STRINGS__PROOF_MANAGER_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__UF__SYMMETRY_BREAKER_H
-#define CVC4__THEORY__UF__SYMMETRY_BREAKER_H
+#ifndef CVC5__THEORY__UF__SYMMETRY_BREAKER_H
+#define CVC5__THEORY__UF__SYMMETRY_BREAKER_H
#include <iostream>
#include <list>
} // namespace cvc5
-#endif /* CVC4__THEORY__UF__SYMMETRY_BREAKER_H */
+#endif /* CVC5__THEORY__UF__SYMMETRY_BREAKER_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__UF__THEORY_UF_H
-#define CVC4__THEORY__UF__THEORY_UF_H
+#ifndef CVC5__THEORY__UF__THEORY_UF_H
+#define CVC5__THEORY__UF__THEORY_UF_H
#include "expr/node.h"
#include "expr/node_trie.h"
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__UF__THEORY_UF_H */
+#endif /* CVC5__THEORY__UF__THEORY_UF_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY_UF_MODEL_H
-#define CVC4__THEORY_UF_MODEL_H
+#ifndef CVC5__THEORY_UF_MODEL_H
+#define CVC5__THEORY_UF_MODEL_H
#include <vector>
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__UF__THEORY_UF_REWRITER_H
-#define CVC4__THEORY__UF__THEORY_UF_REWRITER_H
+#ifndef CVC5__THEORY__UF__THEORY_UF_REWRITER_H
+#define CVC5__THEORY__UF__THEORY_UF_REWRITER_H
#include "expr/node_algorithm.h"
#include "options/uf_options.h"
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__UF__THEORY_UF_REWRITER_H */
+#endif /* CVC5__THEORY__UF__THEORY_UF_REWRITER_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__UF__THEORY_UF_TYPE_RULES_H
-#define CVC4__THEORY__UF__THEORY_UF_TYPE_RULES_H
+#ifndef CVC5__THEORY__UF__THEORY_UF_TYPE_RULES_H
+#define CVC5__THEORY__UF__THEORY_UF_TYPE_RULES_H
#include <climits>
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__UF__THEORY_UF_TYPE_RULES_H */
+#endif /* CVC5__THEORY__UF__THEORY_UF_TYPE_RULES_H */
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__VALUATION_H
-#define CVC4__THEORY__VALUATION_H
+#ifndef CVC5__THEORY__VALUATION_H
+#define CVC5__THEORY__VALUATION_H
#include "context/cdlist.h"
#include "expr/node.h"
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__VALUATION_H */
+#endif /* CVC5__THEORY__VALUATION_H */
#include "cvc4_private.h"
-#ifndef CVC4__BIN_HEAP_H
-#define CVC4__BIN_HEAP_H
+#ifndef CVC5__BIN_HEAP_H
+#define CVC5__BIN_HEAP_H
#include <limits>
#include <functional>
} // namespace cvc5
-#endif /* CVC4__BIN_HEAP_H */
+#endif /* CVC5__BIN_HEAP_H */
#include "cvc4_public.h"
-#ifndef CVC4__BITVECTOR_H
-#define CVC4__BITVECTOR_H
+#ifndef CVC5__BITVECTOR_H
+#define CVC5__BITVECTOR_H
#include <iosfwd>
#include <iostream>
} // namespace cvc5
-#endif /* CVC4__BITVECTOR_H */
+#endif /* CVC5__BITVECTOR_H */
#include "cvc4_public.h"
-#ifndef CVC4__BOOL_H
-#define CVC4__BOOL_H
+#ifndef CVC5__BOOL_H
+#define CVC5__BOOL_H
namespace cvc5 {
} // namespace cvc5
-#endif /* CVC4__BOOL_H */
+#endif /* CVC5__BOOL_H */
#include "cvc4_public.h"
-#ifndef CVC4__CARDINALITY_H
-#define CVC4__CARDINALITY_H
+#ifndef CVC5__CARDINALITY_H
+#define CVC5__CARDINALITY_H
#include <iosfwd>
} // namespace cvc5
-#endif /* CVC4__CARDINALITY_H */
+#endif /* CVC5__CARDINALITY_H */
#include "cvc4_private.h"
-#ifndef CVC4__UTIL__CARDINALITY_CLASS_H
-#define CVC4__UTIL__CARDINALITY_CLASS_H
+#ifndef CVC5__UTIL__CARDINALITY_CLASS_H
+#define CVC5__UTIL__CARDINALITY_CLASS_H
#include <iosfwd>
#include "cvc4_public.h"
-#ifndef CVC4__DIVISIBLE_H
-#define CVC4__DIVISIBLE_H
+#ifndef CVC5__DIVISIBLE_H
+#define CVC5__DIVISIBLE_H
#include <iosfwd>
#include <ostream>
} // namespace cvc5
-#endif /* CVC4__DIVISIBLE_H */
+#endif /* CVC5__DIVISIBLE_H */
**/
#include "cvc4_public.h"
-#ifndef CVC4__FLOATINGPOINT_H
-#define CVC4__FLOATINGPOINT_H
+#ifndef CVC5__FLOATINGPOINT_H
+#define CVC5__FLOATINGPOINT_H
#include <memory>
} // namespace cvc5
-#endif /* CVC4__FLOATINGPOINT_H */
+#endif /* CVC5__FLOATINGPOINT_H */
**/
#include "cvc4_public.h"
-#ifndef CVC4__UTIL__FLOATINGPOINT_LITERAL_SYMFPU_H
-#define CVC4__UTIL__FLOATINGPOINT_LITERAL_SYMFPU_H
+#ifndef CVC5__UTIL__FLOATINGPOINT_LITERAL_SYMFPU_H
+#define CVC5__UTIL__FLOATINGPOINT_LITERAL_SYMFPU_H
#include "util/bitvector.h"
#include "util/floatingpoint_size.h"
#include "cvc4_private.h"
-#ifndef CVC4__UTIL__FLOATINGPOINT_LITERAL_SYMFPU_TRAITS_H
-#define CVC4__UTIL__FLOATINGPOINT_LITERAL_SYMFPU_TRAITS_H
+#ifndef CVC5__UTIL__FLOATINGPOINT_LITERAL_SYMFPU_TRAITS_H
+#define CVC5__UTIL__FLOATINGPOINT_LITERAL_SYMFPU_TRAITS_H
// clang-format off
#if @CVC4_USE_SYMFPU@
**/
#include "cvc4_public.h"
-#ifndef CVC4__FLOATINGPOINT_SIZE_H
-#define CVC4__FLOATINGPOINT_SIZE_H
+#ifndef CVC5__FLOATINGPOINT_SIZE_H
+#define CVC5__FLOATINGPOINT_SIZE_H
namespace cvc5 {
#include "cvc4_public.h"
-#ifndef CVC4__GMP_UTIL_H
-#define CVC4__GMP_UTIL_H
+#ifndef CVC5__GMP_UTIL_H
+#define CVC5__GMP_UTIL_H
#include <gmpxx.h>
} // namespace cvc5
-#endif /* CVC4__GMP_UTIL_H */
+#endif /* CVC5__GMP_UTIL_H */
#include "cvc4_public.h"
-#ifndef CVC4__HASH_H
-#define CVC4__HASH_H
+#ifndef CVC5__HASH_H
+#define CVC5__HASH_H
#include <functional>
#include <string>
} // namespace cvc5
-#endif /* CVC4__HASH_H */
+#endif /* CVC5__HASH_H */
#include "cvc4_public.h"
-#ifndef CVC4__IAND_H
-#define CVC4__IAND_H
+#ifndef CVC5__IAND_H
+#define CVC5__IAND_H
#include <iosfwd>
} // namespace cvc5
-#endif /* CVC4__IAND_H */
+#endif /* CVC5__IAND_H */
#include "cvc4_private.h"
-#ifndef CVC4__INDEX_H
-#define CVC4__INDEX_H
+#ifndef CVC5__INDEX_H
+#define CVC5__INDEX_H
namespace cvc5 {
} // namespace cvc5
-#endif /* CVC4__INDEX_H */
+#endif /* CVC5__INDEX_H */
#include "cvc4_public.h"
-#ifndef CVC4__UTIL__INDEXED_ROOT_PREDICATE_H
-#define CVC4__UTIL__INDEXED_ROOT_PREDICATE_H
+#ifndef CVC5__UTIL__INDEXED_ROOT_PREDICATE_H
+#define CVC5__UTIL__INDEXED_ROOT_PREDICATE_H
namespace cvc5 {
#include "cvc4_public.h"
-#ifndef CVC4__INTEGER_H
-#define CVC4__INTEGER_H
+#ifndef CVC5__INTEGER_H
+#define CVC5__INTEGER_H
#include <cln/input.h>
#include <cln/integer.h>
} // namespace cvc5
-#endif /* CVC4__INTEGER_H */
+#endif /* CVC5__INTEGER_H */
#include "cvc4_public.h"
-#ifndef CVC4__INTEGER_H
-#define CVC4__INTEGER_H
+#ifndef CVC5__INTEGER_H
+#define CVC5__INTEGER_H
#include <gmpxx.h>
} // namespace cvc5
-#endif /* CVC4__INTEGER_H */
+#endif /* CVC5__INTEGER_H */
**/
#include "cvc4_public.h"
-#ifndef CVC4__UTIL__MAYBE_H
-#define CVC4__UTIL__MAYBE_H
+#ifndef CVC5__UTIL__MAYBE_H
+#define CVC5__UTIL__MAYBE_H
#include <ostream>
} // namespace cvc5
-#endif /* CVC4__UTIL__MAYBE_H */
+#endif /* CVC5__UTIL__MAYBE_H */
#include "cvc4_private.h"
-#ifndef CVC4__UTIL__OSTREAM_UTIL_H
-#define CVC4__UTIL__OSTREAM_UTIL_H
+#ifndef CVC5__UTIL__OSTREAM_UTIL_H
+#define CVC5__UTIL__OSTREAM_UTIL_H
#include <ios>
#include <iosfwd>
} // namespace cvc5
-#endif /* CVC4__UTIL__OSTREAM_UTIL_H */
+#endif /* CVC5__UTIL__OSTREAM_UTIL_H */
#include "cvc4_private.h"
-#ifndef CVC4__POLY_UTIL_H
-#define CVC4__POLY_UTIL_H
+#ifndef CVC5__POLY_UTIL_H
+#define CVC5__POLY_UTIL_H
#include <vector>
#endif
-#endif /* CVC4__POLY_UTIL_H */
+#endif /* CVC5__POLY_UTIL_H */
#include "cvc4_private.h"
-#ifndef CVC4__UTIL__RANDOM_H
-#define CVC4__UTIL__RANDOM_H
+#ifndef CVC5__UTIL__RANDOM_H
+#define CVC5__UTIL__RANDOM_H
namespace cvc5 {
#include "cvc4_public.h"
-#ifndef CVC4__RATIONAL_H
-#define CVC4__RATIONAL_H
+#ifndef CVC5__RATIONAL_H
+#define CVC5__RATIONAL_H
#include <cln/dfloat.h>
#include <cln/input.h>
} // namespace cvc5
-#endif /* CVC4__RATIONAL_H */
+#endif /* CVC5__RATIONAL_H */
#include "cvc4_public.h"
-#ifndef CVC4__RATIONAL_H
-#define CVC4__RATIONAL_H
+#ifndef CVC5__RATIONAL_H
+#define CVC5__RATIONAL_H
#include <gmp.h>
} // namespace cvc5
-#endif /* CVC4__RATIONAL_H */
+#endif /* CVC5__RATIONAL_H */
#include "cvc4_private.h"
-#ifndef CVC4__REAL_ALGEBRAIC_NUMBER_H
-#define CVC4__REAL_ALGEBRAIC_NUMBER_H
+#ifndef CVC5__REAL_ALGEBRAIC_NUMBER_H
+#define CVC5__REAL_ALGEBRAIC_NUMBER_H
#include <vector>
} // namespace cvc5
-#endif /* CVC4__REAL_ALGEBRAIC_NUMBER_H */
+#endif /* CVC5__REAL_ALGEBRAIC_NUMBER_H */
#include "cvc4_public.h"
-#ifndef CVC4__UTIL__REGEXP_H
-#define CVC4__UTIL__REGEXP_H
+#ifndef CVC5__UTIL__REGEXP_H
+#define CVC5__UTIL__REGEXP_H
#include <iosfwd>
} // namespace cvc5
-#endif /* CVC4__UTIL__REGEXP_H */
+#endif /* CVC5__UTIL__REGEXP_H */
#include "cvc4_public.h"
-#ifndef CVC4__RESOURCE_MANAGER_H
-#define CVC4__RESOURCE_MANAGER_H
+#ifndef CVC5__RESOURCE_MANAGER_H
+#define CVC5__RESOURCE_MANAGER_H
#include <stdint.h>
#include <chrono>
} // namespace cvc5
-#endif /* CVC4__RESOURCE_MANAGER_H */
+#endif /* CVC5__RESOURCE_MANAGER_H */
#include "cvc4_public.h"
-#ifndef CVC4__RESULT_H
-#define CVC4__RESULT_H
+#ifndef CVC5__RESULT_H
+#define CVC5__RESULT_H
#include <iosfwd>
#include <string>
} // namespace cvc5
-#endif /* CVC4__RESULT_H */
+#endif /* CVC5__RESULT_H */
**/
#include "cvc4_public.h"
-#ifndef CVC4__ROUNDINGMODE_H
-#define CVC4__ROUNDINGMODE_H
+#ifndef CVC5__ROUNDINGMODE_H
+#define CVC5__ROUNDINGMODE_H
#include <fenv.h>
#include "cvc4_private_library.h"
-#ifndef CVC4__SAFE_PRINT_H
-#define CVC4__SAFE_PRINT_H
+#ifndef CVC5__SAFE_PRINT_H
+#define CVC5__SAFE_PRINT_H
#include <unistd.h>
} // namespace cvc5
-#endif /* CVC4__SAFE_PRINT_H */
+#endif /* CVC5__SAFE_PRINT_H */
#include "cvc4_private.h"
-#ifndef CVC4__UTIL_FLOATINGPOINT_SAMPLER_H
-#define CVC4__UTIL_FLOATINGPOINT_SAMPLER_H
+#ifndef CVC5__UTIL_FLOATINGPOINT_SAMPLER_H
+#define CVC5__UTIL_FLOATINGPOINT_SAMPLER_H
#include "util/floatingpoint.h"
} // namespace cvc5
-#endif /* CVC4__UTIL_FLOATINGPOINT_SAMPLER_H */
+#endif /* CVC5__UTIL_FLOATINGPOINT_SAMPLER_H */
#include "cvc4_public.h"
-#ifndef CVC4__SEXPR_H
-#define CVC4__SEXPR_H
+#ifndef CVC5__SEXPR_H
+#define CVC5__SEXPR_H
#include <iosfwd>
#include <string>
} // namespace cvc5
-#endif /* CVC4__SEXPR_H */
+#endif /* CVC5__SEXPR_H */
#include "cvc4_private.h"
-#ifndef CVC4__UTIL__SMT2_QUOTE_STRING_H
-#define CVC4__UTIL__SMT2_QUOTE_STRING_H
+#ifndef CVC5__UTIL__SMT2_QUOTE_STRING_H
+#define CVC5__UTIL__SMT2_QUOTE_STRING_H
#include <string>
} // namespace cvc5
-#endif /* CVC4__UTIL__SMT2_QUOTE_STRING_H */
+#endif /* CVC5__UTIL__SMT2_QUOTE_STRING_H */
#include "cvc4_public.h"
-#ifndef CVC4__STATISTICS_H
-#define CVC4__STATISTICS_H
+#ifndef CVC5__STATISTICS_H
+#define CVC5__STATISTICS_H
#include <iterator>
#include <ostream>
} // namespace cvc5
-#endif /* CVC4__STATISTICS_H */
+#endif /* CVC5__STATISTICS_H */
#include "cvc4_private_library.h"
-#ifndef CVC4__UTIL__STATISTICS_PUBLIC_H
-#define CVC4__UTIL__STATISTICS_PUBLIC_H
+#ifndef CVC5__UTIL__STATISTICS_PUBLIC_H
+#define CVC5__UTIL__STATISTICS_PUBLIC_H
namespace cvc5 {
#include "cvc4_private_library.h"
-#ifndef CVC4__UTIL__STATISTICS_REG_H
-#define CVC4__UTIL__STATISTICS_REG_H
+#ifndef CVC5__UTIL__STATISTICS_REG_H
+#define CVC5__UTIL__STATISTICS_REG_H
#include <iostream>
#include <map>
#include "cvc4_private_library.h"
-#ifndef CVC4__STATISTICS_REGISTRY_H
-#define CVC4__STATISTICS_REGISTRY_H
+#ifndef CVC5__STATISTICS_REGISTRY_H
+#define CVC5__STATISTICS_REGISTRY_H
#include <ctime>
#include <iomanip>
} // namespace cvc5
-#endif /* CVC4__STATISTICS_REGISTRY_H */
+#endif /* CVC5__STATISTICS_REGISTRY_H */
#include "cvc4_private_library.h"
-#ifndef CVC4__UTIL__STATISTICS_STATS_H
-#define CVC4__UTIL__STATISTICS_STATS_H
+#ifndef CVC5__UTIL__STATISTICS_STATS_H
+#define CVC5__UTIL__STATISTICS_STATS_H
#include <optional>
#include "cvc4_private_library.h"
-#ifndef CVC4__UTIL__STATISTICS_VALUE_H
-#define CVC4__UTIL__STATISTICS_VALUE_H
+#ifndef CVC5__UTIL__STATISTICS_VALUE_H
+#define CVC5__UTIL__STATISTICS_VALUE_H
#include <chrono>
#include <iomanip>
#include "cvc4_private_library.h"
-#ifndef CVC4__UTIL__STATS_BASE_H
-#define CVC4__UTIL__STATS_BASE_H
+#ifndef CVC5__UTIL__STATS_BASE_H
+#define CVC5__UTIL__STATS_BASE_H
#include <iomanip>
#include <sstream>
#include "cvc4_private_library.h"
-#ifndef CVC4__UTIL__STATS_HISTOGRAM_H
-#define CVC4__UTIL__STATS_HISTOGRAM_H
+#ifndef CVC5__UTIL__STATS_HISTOGRAM_H
+#define CVC5__UTIL__STATS_HISTOGRAM_H
#include <map>
#include <vector>
#include "cvc4_private_library.h"
-#ifndef CVC4__UTIL__STATS_TIMER_H
-#define CVC4__UTIL__STATS_TIMER_H
+#ifndef CVC5__UTIL__STATS_TIMER_H
+#define CVC5__UTIL__STATS_TIMER_H
#include <chrono>
#include "cvc4_private_library.h"
-#ifndef CVC4__UTIL__STATS_UTILS_H
-#define CVC4__UTIL__STATS_UTILS_H
+#ifndef CVC5__UTIL__STATS_UTILS_H
+#define CVC5__UTIL__STATS_UTILS_H
#include <iosfwd>
#include "cvc4_public.h"
-#ifndef CVC4__UTIL__STRING_H
-#define CVC4__UTIL__STRING_H
+#ifndef CVC5__UTIL__STRING_H
+#define CVC5__UTIL__STRING_H
#include <iosfwd>
#include <string>
} // namespace cvc5
-#endif /* CVC4__UTIL__STRING_H */
+#endif /* CVC5__UTIL__STRING_H */
#include "cvc4_public.h"
-#ifndef CVC4__TUPLE_H
-#define CVC4__TUPLE_H
+#ifndef CVC5__TUPLE_H
+#define CVC5__TUPLE_H
#include <iostream>
#include <vector>
} // namespace cvc5
-#endif /* CVC4__TUPLE_H */
+#endif /* CVC5__TUPLE_H */
#include "cvc4_public.h"
-#ifndef CVC4__UNSAFE_INTERRUPT_EXCEPTION_H
-#define CVC4__UNSAFE_INTERRUPT_EXCEPTION_H
+#ifndef CVC5__UNSAFE_INTERRUPT_EXCEPTION_H
+#define CVC5__UNSAFE_INTERRUPT_EXCEPTION_H
#include "base/exception.h"
#include "cvc4_export.h"
} // namespace cvc5
-#endif /* CVC4__UNSAFE_INTERRUPT_EXCEPTION_H */
+#endif /* CVC5__UNSAFE_INTERRUPT_EXCEPTION_H */
#include "cvc4_private.h"
-#ifndef CVC4__UTILITY_H
-#define CVC4__UTILITY_H
+#ifndef CVC5__UTILITY_H
+#define CVC5__UTILITY_H
#include <algorithm>
#include <fstream>
} // namespace cvc5
-#endif /* CVC4__UTILITY_H */
+#endif /* CVC5__UTILITY_H */
#include "test.h"
-#ifndef __CVC4__TEST__UNIT__MEMORY_H
-#define __CVC4__TEST__UNIT__MEMORY_H
+#ifndef __CVC5__TEST__UNIT__MEMORY_H
+#define __CVC5__TEST__UNIT__MEMORY_H
#include <string>
#include <sys/resource.h>
#undef CVC4_MEMORY_LIMITING_DISABLED_REASON
#endif /* CVC4_MEMORY_LIMITING_DISABLED_REASON */
-#endif /* __CVC4__TEST__MEMORY_H */
+#endif /* __CVC5__TEST__MEMORY_H */
** \brief Common header for API unit test.
**/
-#ifndef CVC4__TEST__UNIT__TEST_H
-#define CVC4__TEST__UNIT__TEST_H
+#ifndef CVC5__TEST__UNIT__TEST_H
+#define CVC5__TEST__UNIT__TEST_H
#include "gtest/gtest.h"
** \brief Common header for API unit test.
**/
-#ifndef CVC4__TEST__UNIT__TEST_API_H
-#define CVC4__TEST__UNIT__TEST_API_H
+#ifndef CVC5__TEST__UNIT__TEST_API_H
+#define CVC5__TEST__UNIT__TEST_API_H
#include "api/cpp/cvc5.h"
#include "gtest/gtest.h"
** \brief Header for context unit tests.
**/
-#ifndef CVC4__TEST__UNIT__TEST_CONTEXT_H
-#define CVC4__TEST__UNIT__TEST_CONTEXT_H
+#ifndef CVC5__TEST__UNIT__TEST_CONTEXT_H
+#define CVC5__TEST__UNIT__TEST_CONTEXT_H
#include "context/context.h"
#include "test.h"
** \brief Common header for Node unit tests.
**/
-#ifndef CVC4__TEST__UNIT__TEST_NODE_H
-#define CVC4__TEST__UNIT__TEST_NODE_H
+#ifndef CVC5__TEST__UNIT__TEST_NODE_H
+#define CVC5__TEST__UNIT__TEST_NODE_H
#include "expr/node_manager.h"
#include "expr/skolem_manager.h"
** \brief Common header for unit tests that need an SmtEngine.
**/
-#ifndef CVC4__TEST__UNIT__TEST_SMT_H
-#define CVC4__TEST__UNIT__TEST_SMT_H
+#ifndef CVC5__TEST__UNIT__TEST_SMT_H
+#define CVC5__TEST__UNIT__TEST_SMT_H
#include "expr/dtype_cons.h"
#include "expr/node.h"